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