defpred S1[ set , set ] means for y being set holds
( y in $2 iff ( y in F2() & P1[$1,y] ) );
A2: for e, u1, u2 being set st e in F1() & S1[e,u1] & S1[e,u2] holds
u1 = u2
proof
let e, u1, u2 be set ; :: thesis: ( e in F1() & S1[e,u1] & S1[e,u2] implies u1 = u2 )
assume e in F1() ; :: thesis: ( not S1[e,u1] or not S1[e,u2] or u1 = u2 )
assume A4: for y being set holds
( y in u1 iff ( y in F2() & P1[e,y] ) ) ; :: thesis: ( not S1[e,u2] or u1 = u2 )
defpred S2[ set ] means ( $1 in F2() & P1[e,$1] );
A5: for x being set holds
( x in u1 iff S2[x] ) by A4;
assume A7: for y being set holds
( y in u2 iff ( y in F2() & P1[e,y] ) ) ; :: thesis: u1 = u2
A8: for x being set holds
( x in u2 iff S2[x] ) by A7;
u1 = u2 from XBOOLE_0:sch 2(A5, A8);
 hence u1 = u2 ; :: thesis: verum
end;
A9: for x being set st x in F1() holds
ex y being set st S1[x,y]
proof
let x be set ; :: thesis: ( x in F1() implies ex y being set st S1[x,y] )
assume x in F1() ; :: thesis: ex y being set st S1[x,y]
defpred S2[ set ] means P1[x,$1];
consider X being set such that
A10: for y being set holds
( y in X iff ( y in F2() & S2[y] ) ) from XBOOLE_0:sch 1();
 take X ; :: thesis: S1[x,X]
thus S1[x,X] by A10; :: thesis: verum
end;
consider G being Function such that
A11: ( dom G = F1() & ( for x being set st x in F1() holds
S1[x,G . x] ) ) from FUNCT_1:sch 2(A2, A9);
A12: now
assume F1() <> {} ; :: thesis: ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
then reconsider D = rng G as non empty set by A11, RELAT_1:65;
now
let X be set ; :: thesis: ( X in D implies X <> {} )
assume X in D ; :: thesis: X <> {}
then consider x being set such that
A13: ( x in dom G & X = G . x ) by FUNCT_1:def 5;
( ( for y being set holds
( y in X iff ( y in F2() & P1[x,y] ) ) ) & ex y being set st
( y in F2() & P1[x,y] ) ) by A1, A11, A13;
hence X <> {} ; :: thesis: verum
end;
then consider F being Function such that
A14: dom F = D and
A15: for X being set st X in D holds
F . X in X by Th28;
A16: dom (F * G) = F1() by A11, A14, RELAT_1:46;
thus ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) ) :: thesis: verum
proof
take f = F * G; :: thesis: ( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
thus dom f = F1() by A11, A14, RELAT_1:46; :: thesis: ( rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
rng F c= F2()
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F or x in F2() )
assume x in rng F ; :: thesis: x in F2()
then consider y being set such that
A17: y in dom F and
A18: x = F . y by FUNCT_1:def 5;
A19: ex z being set st
( z in dom G & y = G . z ) by A14, A17, FUNCT_1:def 5;
x in y by A14, A15, A17, A18;
hence x in F2() by A11, A19; :: thesis: verum
end;
hence rng f c= F2() by A14, RELAT_1:47; :: thesis: for x being set st x in F1() holds
P1[x,f . x]
let x be set ; :: thesis: ( x in F1() implies P1[x,f . x] )
assume A22: x in F1() ; :: thesis: P1[x,f . x]
then ( f . x = F . (G . x) & G . x in D ) by A11, A16, FUNCT_1:22, FUNCT_1:def 5;
then f . x in G . x by A15;
hence P1[x,f . x] by A11, A22; :: thesis: verum
end;
end;
now
reconsider F = {} as Function ;
assume A25: F1() = {} ; :: thesis: ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) )
thus ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) ) :: thesis: verum
proof
take F ; :: thesis: ( dom F = F1() & rng F c= F2() & ( for x being set st x in F1() holds
P1[x,F . x] ) )
thus ( dom F = F1() & rng F c= F2() & ( for x being set st x in F1() holds
P1[x,F . x] ) ) by A25, RELAT_1:60, XBOOLE_1:2; :: thesis: verum
end;
end;
hence ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being set st x in F1() holds
P1[x,f . x] ) ) by A12; :: thesis: verum