let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( r in rng (abs f) implies 0 < r )
set R = abs f;
assume r in rng (abs f) ; :: thesis: 0 < r
then consider x being object such that
A1: x in dom (abs f) and
A2: (abs f) . x = r by FUNCT_1:def 3;
dom (abs f) = dom f by VALUED_1:def 11;
then reconsider a = f . x as non zero Real by ;
|.a.| is positive by COMPLEX1:47;
hence 0 < r by ; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.77401924,"math_prob":0.99919885,"size":392,"snap":"2019-43-2019-47","text_gpt3_token_len":158,"char_repetition_ratio":0.13917525,"word_repetition_ratio":0.02247191,"special_character_ratio":0.4107143,"punctuation_ratio":0.20183486,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9996985,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-19T14:52:41Z\",\"WARC-Record-ID\":\"<urn:uuid:1a183225-26fd-4d71-a48b-1d456939c9be>\",\"Content-Length\":\"5953\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:4ca70feb-658b-4622-84a1-6f6f1208f49d>\",\"WARC-Concurrent-To\":\"<urn:uuid:c8b4db56-371b-4ee3-a83b-f6b2b87a42b8>\",\"WARC-IP-Address\":\"212.33.73.131\",\"WARC-Target-URI\":\"http://mizar.uwb.edu.pl/version/current/html/proofs/partfun3/70_1_1\",\"WARC-Payload-Digest\":\"sha1:FWLN6O2ZJDS67DELNFMGOZIXMEIXNGQK\",\"WARC-Block-Digest\":\"sha1:XU2FMNIPGT6VDYRYQPSHTBYSWHUNMHEZ\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570986696339.42_warc_CC-MAIN-20191019141654-20191019165154-00079.warc.gz\"}"}