thus ( f is ext-real-functions-valued implies for x being object st x in dom f holds
f . x is ext-real-valued Function ) :: thesis: ( ( for x being object st x in dom f holds
f . x is ext-real-valued Function ) implies f is ext-real-functions-valued )
proof
assume A3: rng f is ext-real-functions-membered ; :: according to VALUED_2:def 21 :: thesis: for x being object st x in dom f holds
f . x is ext-real-valued Function

let x be object ; :: thesis: ( x in dom f implies f . x is ext-real-valued Function )
assume x in dom f ; :: thesis:
then f . x in rng f by FUNCT_1:def 3;
hence f . x is ext-real-valued Function by A3; :: thesis: verum
end;
assume A4: for x being object st x in dom f holds
f . x is ext-real-valued Function ; :: thesis:
let y be object ; :: according to VALUED_2:def 3,VALUED_2:def 21 :: thesis: ( y in rng f implies y is ext-real-valued Function )
assume y in rng f ; :: thesis:
then ex x being object st
( x in dom f & f . x = y ) by FUNCT_1:def 3;
hence y is ext-real-valued Function by A4; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.763167,"math_prob":0.99471515,"size":629,"snap":"2019-43-2019-47","text_gpt3_token_len":193,"char_repetition_ratio":0.2288,"word_repetition_ratio":0.3089431,"special_character_ratio":0.29411766,"punctuation_ratio":0.0952381,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9996099,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-14T13:40:46Z\",\"WARC-Record-ID\":\"<urn:uuid:7ceb2978-4644-4fef-bf3f-80a4bbb574c9>\",\"Content-Length\":\"10723\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:73ded81b-6988-4900-8b43-e20c84d256fc>\",\"WARC-Concurrent-To\":\"<urn:uuid:dd78194c-c4ca-4380-820a-21e4d6a51644>\",\"WARC-IP-Address\":\"212.33.73.131\",\"WARC-Target-URI\":\"http://mizar.uwb.edu.pl/version/current/html/proofs/valued_2/67_2_1\",\"WARC-Payload-Digest\":\"sha1:7WVVN4PLRCYKCFTTBM3RHHQ6BHHGAQ7K\",\"WARC-Block-Digest\":\"sha1:M5EZ2XQP5A3YPUPRLYU77AMFOW6PZ5WR\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570986653247.25_warc_CC-MAIN-20191014124230-20191014151730-00073.warc.gz\"}"}