per cases ( F1() = {} or F1() <> {} ) ;
suppose A19: 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] ) )
take {} ; :: thesis: ( dom {} = F1() & rng {} c= F2() & ( for x being set st x in F1() holds
P1[x,{} . x] ) )
thus ( dom {} = F1() & rng {} c= F2() & ( for x being set st x in F1() holds
P1[x,{} . x] ) ) by A19, XBOOLE_1:2; :: thesis: verum
end;
suppose A10: 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] ) )
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 A3: 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] );
A4: for x being set holds
( x in u1 iff S2[x] ) by A3;
assume A5: for y being set holds
( y in u2 iff ( y in F2() & P1[e,y] ) ) ; :: thesis: u1 = u2
A6: for x being set holds
( x in u2 iff S2[x] ) by A5;
u1 = u2 from XBOOLE_0:sch 2(A4, A6);
 hence u1 = u2 ; :: thesis: verum
end;
A7: 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
A8: 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 A8; :: thesis: verum
end;
consider G being Function such that
A9: ( dom G = F1() & ( for x being set st x in F1() holds
S1[x,G . x] ) ) from FUNCT_1:sch 2(A2, A7);
reconsider D = rng G as non empty set by A9, A10, RELAT_1:42;
now
let X be set ; :: thesis: ( X in D implies X <> {} )
assume X in D ; :: thesis: X <> {}
then consider x being set such that
A11: ( x in dom G & X = G . x ) by Def5;
( ( 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, A9, A11;
hence X <> {} ; :: thesis: verum
end;
then consider F being Function such that
A12: dom F = D and
A13: for X being set st X in D holds
F . X in X by Th181;
A14: dom (F * G) = F1() by A9, A12, RELAT_1:27;
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 A9, A12, RELAT_1:27; :: 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
A15: y in dom F and
A16: x = F . y by Def5;
A17: ex z being set st
( z in dom G & y = G . z ) by A12, A15, Def5;
x in y by A12, A13, A15, A16;
hence x in F2() by A9, A17; :: thesis: verum
end;
hence rng f c= F2() by A12, RELAT_1:28; :: 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 A18: x in F1() ; :: thesis: P1[x,f . x]
then ( f . x = F . (G . x) & G . x in D ) by A9, A14, Th22, Def5;
then f . x in G . x by A13;
hence P1[x,f . x] by A9, A18; :: thesis: verum
end;
end;