consider x being Element of F2();
defpred S1[ set , set ] means ( ( ex c being Element of F2() st P1[$1,c] implies P1[$1,$2] ) & ( ( for c being Element of F2() holds P1[$1,c] ) implies $2 = x ) );
A1: for d being Element of F1() ex z being Element of F2() st S1[d,z]
proof
let d be Element of F1(); :: thesis: ex z being Element of F2() st S1[d,z]
( ( for c being Element of F2() holds P1[d,c] ) implies ex z being Element of F2() st
( ( ex c being Element of F2() st P1[d,c] implies P1[d,z] ) & ( ( for c being Element of F2() holds P1[d,c] ) implies z = x ) ) ) ;
hence ex z being Element of F2() st S1[d,z] ; :: thesis: verum
end;
consider g being Function of F1(),F2() such that
A2: for d being Element of F1() holds S1[d,g . d] from FUNCT_2:sch 3(A1);
 A3: ( dom g = F1() & rng g c= F2() ) by FUNCT_2:def 1;
defpred S2[ set ] means ex c being Element of F2() st P1[$1,c];
consider X being set such that
A4: for x being set holds
( x in X iff ( x in F1() & S2[x] ) ) from XBOOLE_0:sch 1();
 for x being set st x in X holds
x in F1() by A4;
then reconsider X = X as Subset of F1() by TARSKI:def 3;
reconsider f = g | X as PartFunc of F1(),F2() ;
take f ; :: thesis: ( ( for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) ) & ( for d being Element of F1() st d in dom f holds
P1[d,f /. d] ) )
thus for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st P1[d,c] ) :: thesis: for d being Element of F1() st d in dom f holds
P1[d,f /. d]
proof
let d be Element of F1(); :: thesis: ( d in dom f iff ex c being Element of F2() st P1[d,c] )
dom f c= X by RELAT_1:87;
hence ( d in dom f implies ex c being Element of F2() st P1[d,c] ) by A4; :: thesis: ( ex c being Element of F2() st P1[d,c] implies d in dom f )
assume ex c being Element of F2() st P1[d,c] ; :: thesis: d in dom f
then ( d in X & d in F1() ) by A4;
then d in (dom g) /\ X by A3, XBOOLE_0:def 4;
hence d in dom f by RELAT_1:90; :: thesis: verum
end;
let d be Element of F1(); :: thesis: ( d in dom f implies P1[d,f /. d] )
assume A5: d in dom f ; :: thesis: P1[d,f /. d]
dom f c= X by RELAT_1:87;
then ex c being Element of F2() st P1[d,c] by A4, A5;
then P1[d,g . d] by A2;
then P1[d,f . d] by A5, FUNCT_1:70;
hence P1[d,f /. d] by A5, PARTFUN1:def 8; :: thesis: verum