defpred S1[ object ] means ex c being Element of F2() st P1[$1,c];
set x = the Element of F2();
defpred S2[ Element of F1(), Element of F2()] 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 = the Element of F2() ) );
consider X being set such that
A1: for x being object holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch 1();
 for x being object st x in X holds
x in F1() by A1;
then reconsider X = X as Subset of F1() by TARSKI:def 3;
A2: for d being Element of F1() ex z being Element of F2() st S2[d,z]
proof
let d be Element of F1(); :: thesis: ex z being Element of F2() st S2[d,z]
( ( for c being Element of F2() holds P1[d,c] ) implies ex z being object 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 = the Element of F2() ) ) ) ;
hence ex z being Element of F2() st S2[d,z] ; :: thesis: verum
end;
consider g being Function of F1(),F2() such that
A3: for d being Element of F1() holds S2[d,g . d] from FUNCT_2:sch 3(A2);
 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] ) )
A4: dom g = F1() by FUNCT_2:def 1;
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:58;
hence ( d in dom f implies ex c being Element of F2() st P1[d,c] ) by A1; :: 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 by A1;
then d in (dom g) /\ X by A4, XBOOLE_0:def 4;
hence d in dom f by RELAT_1:61; :: 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:58;
then ex c being Element of F2() st P1[d,c] by A1, A5;
then P1[d,g . d] by A3;
hence P1[d,f . d] by A5, FUNCT_1:47; :: thesis: verum