per cases ( F1() = {} or F1() <> {} ) ;
suppose A2: F1() = {} ; :: thesis: ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being object st x in F1() holds
P1[x,f . x] ) )
take {} ; :: thesis: ( dom {} = F1() & rng {} c= F2() & ( for x being object st x in F1() holds
P1[x,{} . x] ) )
thus ( dom {} = F1() & rng {} c= F2() & ( for x being object st x in F1() holds
P1[x,{} . x] ) ) by A2; :: thesis: verum
end;
suppose A3: F1() <> {} ; :: thesis: ex f being Function st
( dom f = F1() & rng f c= F2() & ( for x being object st x in F1() holds
P1[x,f . x] ) )
defpred S1[ object , object ] means ex D2 being set st
( D2 = $2 & ( for y being object holds
( y in D2 iff ( y in F2() & P1[$1,y] ) ) ) );
A4: for e, u1, u2 being object st e in F1() & S1[e,u1] & S1[e,u2] holds
u1 = u2
proof
let e, u1, u2 be object ; :: 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 )
given U1 being set such that A5: U1 = u1 and
A6: for y being object holds
( y in U1 iff ( y in F2() & P1[e,y] ) ) ; :: thesis: ( not S1[e,u2] or u1 = u2 )
defpred S2[ object ] means ( $1 in F2() & P1[e,$1] );
A7: for x being object holds
( x in U1 iff S2[x] ) by A6;
given U2 being set such that A8: U2 = u2 and
A9: for y being object holds
( y in U2 iff ( y in F2() & P1[e,y] ) ) ; :: thesis: u1 = u2
A10: for x being object holds
( x in U2 iff S2[x] ) by A9;
U1 = U2 from XBOOLE_0:sch 2(A7, A10);
 hence u1 = u2 by A5, A8; :: thesis: verum
end;
A11: for x being object st x in F1() holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in F1() implies ex y being object st S1[x,y] )
assume x in F1() ; :: thesis: ex y being object st S1[x,y]
defpred S2[ object ] means P1[x,$1];
consider X being set such that
A12: for y being object 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 A12; :: thesis: verum
end;
consider G being Function such that
A13: ( dom G = F1() & ( for x being object st x in F1() holds
S1[x,G . x] ) ) from FUNCT_1:sch 2(A4, A11);
reconsider D = rng G as non empty set by A13, 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 object such that
A14: ( x in dom G & X = G . x ) by Def3;
consider y being object such that
A15: ( y in F2() & P1[x,y] ) by A1, A13, A14;
S1[x,G . x] by A13, A14;
then y in X by A15, A14;
hence X <> {} ; :: thesis: verum
end;
then consider F being Function such that
A16: dom F = D and
A17: for X being set st X in D holds
F . X in X by Th110;
A18: dom (F * G) = F1() by A13, A16, RELAT_1:27;
take f = F * G; :: thesis: ( dom f = F1() & rng f c= F2() & ( for x being object st x in F1() holds
P1[x,f . x] ) )
thus dom f = F1() by A13, A16, RELAT_1:27; :: thesis: ( rng f c= F2() & ( for x being object st x in F1() holds
P1[x,f . x] ) )
rng F c= F2()
proof
let x be object ; :: 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 object such that
A19: y in dom F and
A20: x = F . y by Def3;
consider z being object such that
A21: ( z in dom G & y = G . z ) by A16, A19, Def3;
reconsider y = y as set by TARSKI:1;
A22: x in y by A16, A17, A19, A20;
S1[z,G . z] by A13, A21;
hence x in F2() by A21, A22; :: thesis: verum
end;
hence rng f c= F2() by A16, RELAT_1:28; :: thesis: for x being object st x in F1() holds
P1[x,f . x]
let x be object ; :: thesis: ( x in F1() implies P1[x,f . x] )
assume A23: x in F1() ; :: thesis: P1[x,f . x]
then ( f . x = F . (G . x) & G . x in D ) by A13, A18, Th12, Def3;
then A24: f . x in G . x by A17;
S1[x,G . x] by A13, A23;
hence P1[x,f . x] by A24; :: thesis: verum
end;
end;