suppose A2: F₁() = {} ; :: thesis:

take {} ; :: thesis:
thus ( dom {} = F₁() & rng {} c= F₂() & ( for x being object st x in F₁() holds
P₁[x,{} . x] ) ) by A2; :: thesis:

end;

suppose A3: F₁() <> {} ; :: thesis:

defpred S₁[ object , object ] means ex D2 being set st
( D2 = $2 & ( for y being object holds
( y in D2 iff ( y in F₂() & P₁[$1,y] ) ) ) );
A4: for e, u1, u2 being object st e in F₁() & S₁[e,u1] & S₁[e,u2] holds
u1 = u2

proof

let e, u1, u2 be object ; :: thesis:
assume e in F₁() ; :: thesis:
given U1 being set such that A5: U1 = u1 and
A6: for y being object holds
( y in U1 iff ( y in F₂() & P₁[e,y] ) ) ; :: thesis:
defpred S₂[ object ] means ( $1 in F₂() & P₁[e,$1] );
A7: for x being object holds
( x in U1 iff S₂[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 F₂() & P₁[e,y] ) ) ; :: thesis:
A10: for x being object holds
( x in U2 iff S₂[x] ) by A9;
U1 = U2 from XBOOLE_0:sch 2(A7, A10);
hence u1 = u2 by A5, A8; :: thesis:

end;

A11: for x being object st x in F₁() holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis:
assume x in F₁() ; :: thesis:
defpred S₂[ object ] means P₁[x,$1];
consider X being set such that
A12: for y being object holds
( y in X iff ( y in F₂() & S₂[y] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis:
thus S₁[x,X] by A12; :: thesis:

end;

consider G being Function such that
A13: ( dom G = F₁() & ( for x being object st x in F₁() holds
S₁[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:

let X be set ; :: thesis:
assume X in D ; :: thesis:
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 F₂() & P₁[x,y] ) by A1, A13, A14;
S₁[x,G . x] by A13, A14;
then y in X by A15, A14;
hence X <> {} ; :: thesis:

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) = F₁() by A13, A16, RELAT_1:27;
take f = F * G; :: thesis:
thus dom f = F₁() by A13, A16, RELAT_1:27; :: thesis:
rng F c= F₂()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng F ; :: thesis:
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;
S₁[z,G . z] by A13, A21;
hence x in F₂() by A21, A22; :: thesis:

end;

hence rng f c= F₂() by A16, RELAT_1:28; :: thesis:
let x be object ; :: thesis:
assume A23: x in F₁() ; :: thesis:
then ( f . x = F . (G . x) & G . x in D ) by A13, A18, Th12, Def3;
then A24: f . x in G . x by A17;
S₁[x,G . x] by A13, A23;
hence P₁[x,f . x] by A24; :: thesis:

end;