A2: for x being object st x in F1() holds
ex y being object st
( y in F2() & P1[x,y] )
proof
let x be object ; :: thesis: ( x in F1() implies ex y being object st
( y in F2() & P1[x,y] ) )

assume x in F1() ; :: thesis: ex y being object st
( y in F2() & P1[x,y] )

then consider y being Element of F2() such that
A3: P1[x,y] by A1;
take y ; :: thesis: ( y in F2() & P1[x,y] )
thus ( y in F2() & P1[x,y] ) by A3; :: thesis: verum
end;
consider f being Function such that
A4: ( dom f = F1() & rng f c= F2() & ( for x being object st x in F1() holds
P1[x,f . x] ) ) from reconsider f = f as Function of F1(),F2() by ;
take f ; :: thesis: for x being object st x in F1() holds
P1[x,f . x]

thus for x being object st x in F1() holds
P1[x,f . x] by A4; :: thesis: verum
{"ft_lang_label":"__label__en","ft_lang_prob":0.71446186,"math_prob":0.9983098,"size":748,"snap":"2019-43-2019-47","text_gpt3_token_len":309,"char_repetition_ratio":0.20026882,"word_repetition_ratio":0.32022473,"special_character_ratio":0.44385028,"punctuation_ratio":0.155,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.9986353,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2019-10-19T12:24:39Z\",\"WARC-Record-ID\":\"<urn:uuid:0a8cb90f-a3d5-4fb1-9d33-89bc3cfc21a2>\",\"Content-Length\":\"8783\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:3acf73b4-7a79-4c10-91eb-1090d094f07d>\",\"WARC-Concurrent-To\":\"<urn:uuid:3b6040a1-6a23-4ed2-ae1e-57287602bfdc>\",\"WARC-IP-Address\":\"212.33.73.131\",\"WARC-Target-URI\":\"http://mizar.uwb.edu.pl/version/current/html/proofs/monoid_1/10_1\",\"WARC-Payload-Digest\":\"sha1:Q2SH324JBMDK7SIYHKVYVNKLSWTAH3ZC\",\"WARC-Block-Digest\":\"sha1:6WVPHPBBYVUG2JF2AE46C5UN6PSTBRVJ\",\"WARC-Identified-Payload-Type\":\"application/xml\",\"warc_filename\":\"/cc_download/warc_2019/CC-MAIN-2019-43/CC-MAIN-2019-43_segments_1570986693979.65_warc_CC-MAIN-20191019114429-20191019141929-00490.warc.gz\"}"}