defpred S1[ set , set ] means ex X being set st
( $2 = X & ( for y being set holds
( y in X 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 )
given X being set such that A3: u1 = X and
A4: for y being set holds
( y in X 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 X iff S2[x] ) by A4;
given Y being set such that A6: u2 = Y and
A7: for y being set holds
( y in Y iff ( y in F2() & P1[e,y] ) ) ; :: thesis: u1 = u2
A8: for x being set holds
( x in Y iff S2[x] ) by A7;
X = Y from XBOOLE_0:sch 2(A5, A8);
 hence u1 = u2 by A3, A6; :: 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]
take X ; :: thesis: ( X = X & ( for y being set holds
( y in X iff ( y in F2() & P1[x,y] ) ) ) )
thus ( X = X & ( for y being set holds
( y in X iff ( y in F2() & P1[x,y] ) ) ) ) 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;
( ex Y being set st
( X = Y & ( for y being set holds
( y in Y 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;
consider z being set such that
A19: ( z in dom G & y = G . z ) by A14, A17, FUNCT_1:def 5;
consider X being set such that
A20: y = X and
A21: for x being set holds
( x in X iff ( x in F2() & P1[z,x] ) ) by A11, A19;
x in X by A14, A15, A17, A18, A20;
hence x in F2() by A21; :: 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 consider X being set such that
A23: G . x = X and
A24: for y being set holds
( y in X iff ( y in F2() & P1[x,y] ) ) by A11;
( f . x = F . X & X in D ) by A11, A16, A22, A23, FUNCT_1:22, FUNCT_1:def 5;
then f . x in X by A15;
hence P1[x,f . x] by A24; :: 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() by A25; :: thesis: ( rng F c= F2() & ( for x being set st x in F1() holds
P1[x,F . x] ) )
thus ( 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