A3: now
assume A4: F2() = {} ; :: thesis: ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
consider f being Function such that
A5: dom f c= F1() and
A6: rng f c= F2() by Lm2;
reconsider f = f as PartFunc of F1(),F2() by A5, A6, RELSET_1:11;
take f = f; :: thesis: ( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
thus for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) by A1, A4; :: thesis: for x being set st x in dom f holds
P1[x,f . x]
thus for x being set st x in dom f holds
P1[x,f . x] by A4; :: thesis: verum
end;
now
assume F2() <> {} ; :: thesis: ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
set y1 = the set ;
defpred S1[ set , set ] means ( ( ex y being set st P1[$1,y] implies P1[$1,$2] ) & ( ( for y being set holds P1[$1,y] ) implies $2 = the set ) );
A8: for x being set st x in F1() holds
ex z being set st S1[x,z]
proof
let x be set ; :: thesis: ( x in F1() implies ex z being set st S1[x,z] )
assume x in F1() ; :: thesis: ex z being set st S1[x,z]
( ( for y being set holds P1[x,y] ) implies ( ( ex y being set st P1[x,y] implies P1[x,the set ] ) & ( ( for y being set holds P1[x,y] ) implies the set = the set ) ) ) ;
hence ex z being set st S1[x,z] ; :: thesis: verum
end;
A9: for x, z1, z2 being set st x in F1() & S1[x,z1] & S1[x,z2] holds
z1 = z2 by A2;
consider g being Function such that
A10: dom g = F1() and
A11: for x being set st x in F1() holds
S1[x,g . x] from FUNCT_1:sch 2(A9, A8);
defpred S2[ set ] means ex y being set st P1[$1,y];
consider X being set such that
A12: for x being set holds
( x in X iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch 1();
set f = g | X;
A13: dom (g | X) c= F1() by A10, RELAT_1:89;
rng (g | X) c= F2()
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (g | X) or y in F2() )
assume y in rng (g | X) ; :: thesis: y in F2()
then consider x being set such that
A14: x in dom (g | X) and
A15: y = (g | X) . x by FUNCT_1:def 5;
dom (g | X) c= X by RELAT_1:87;
then ( x in F1() & ex y being set st P1[x,y] ) by A12, A14;
then ( x in F1() & P1[x,g . x] ) by A11;
then ( x in F1() & P1[x,y] ) by A14, A15, FUNCT_1:70;
hence y in F2() by A1; :: thesis: verum
end;
then reconsider f = g | X as PartFunc of F1(),F2() by A13, RELSET_1:11;
take f = f; :: thesis: ( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) )
thus for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) :: thesis: for x being set st x in dom f holds
P1[x,f . x]
proof
let x be set ; :: thesis: ( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) )
dom f c= X by RELAT_1:87;
hence ( x in dom f implies ( x in F1() & ex y being set st P1[x,y] ) ) by A12; :: thesis: ( x in F1() & ex y being set st P1[x,y] implies x in dom f )
assume ( x in F1() & ex y being set st P1[x,y] ) ; :: thesis: x in dom f
then ( x in X & x in dom g ) by A10, A12;
then x in (dom g) /\ X by XBOOLE_0:def 4;
hence x in dom f by RELAT_1:90; :: thesis: verum
end;
let x be set ; :: thesis: ( x in dom f implies P1[x,f . x] )
assume A16: x in dom f ; :: thesis: P1[x,f . x]
dom f c= X by RELAT_1:87;
then ( x in F1() & ex y being set st P1[x,y] ) by A12, A16;
then P1[x,g . x] by A11;
hence P1[x,f . x] by A16, FUNCT_1:70; :: thesis: verum
end;
hence ex f being PartFunc of F1(),F2() st
( ( for x being set holds
( x in dom f iff ( x in F1() & ex y being set st P1[x,y] ) ) ) & ( for x being set st x in dom f holds
P1[x,f . x] ) ) by A3; :: thesis: verum