defpred S_{1}[ object ] means ex c being Element of F_{2}() st P_{1}[$1,c];

set x = the Element of F_{2}();

defpred S_{2}[ object , object ] means ( ( ex c being Element of F_{2}() st P_{1}[$1,c] implies P_{1}[$1,$2] ) & ( ( for c being Element of F_{2}() holds P_{1}[$1,c] ) implies $2 = the Element of F_{2}() ) );

consider X being set such that

A1: for x being object holds

( x in X iff ( x in F_{1}() & S_{1}[x] ) )
from XBOOLE_0:sch 1();

for x being object st x in X holds

x in F_{1}()
by A1;

then reconsider X = X as Subset of F_{1}() by TARSKI:def 3;

A2: for d being Element of F_{1}() ex z being Element of F_{2}() st S_{2}[d,z]
_{1}(),F_{2}() such that

A3: for d being Element of F_{1}() holds S_{2}[d,g . d]
from FUNCT_2:sch 3(A2);

reconsider f = g | X as PartFunc of F_{1}(),F_{2}() ;

take f ; :: thesis: ( ( for d being Element of F_{1}() holds

( d in dom f iff ex c being Element of F_{2}() st P_{1}[d,c] ) ) & ( for d being Element of F_{1}() st d in dom f holds

P_{1}[d,f /. d] ) )

A4: dom g = F_{1}()
by FUNCT_2:def 1;

thus for d being Element of F_{1}() holds

( d in dom f iff ex c being Element of F_{2}() st P_{1}[d,c] )
:: thesis: for d being Element of F_{1}() st d in dom f holds

P_{1}[d,f /. d]_{1}(); :: thesis: ( d in dom f implies P_{1}[d,f /. d] )

assume A5: d in dom f ; :: thesis: P_{1}[d,f /. d]

dom f c= X by RELAT_1:58;

then ex c being Element of F_{2}() st P_{1}[d,c]
by A1, A5;

then P_{1}[d,g . d]
by A3;

then P_{1}[d,f . d]
by A5, FUNCT_1:47;

hence P_{1}[d,f /. d]
by A5, PARTFUN1:def 6; :: thesis: verum

set x = the Element of F

defpred S

consider X being set such that

A1: for x being object holds

( x in X iff ( x in F

for x being object st x in X holds

x in F

then reconsider X = X as Subset of F

A2: for d being Element of F

proof

consider g being Function of F
let d be Element of F_{1}(); :: thesis: ex z being Element of F_{2}() st S_{2}[d,z]

( ( for c being Element of F_{2}() holds P_{1}[d,c] ) implies ex z being Element of F_{2}() st

( ( ex c being Element of F_{2}() st P_{1}[d,c] implies P_{1}[d,z] ) & ( ( for c being Element of F_{2}() holds P_{1}[d,c] ) implies z = the Element of F_{2}() ) ) )
;

hence ex z being Element of F_{2}() st S_{2}[d,z]
; :: thesis: verum

end;( ( for c being Element of F

( ( ex c being Element of F

hence ex z being Element of F

A3: for d being Element of F

reconsider f = g | X as PartFunc of F

take f ; :: thesis: ( ( for d being Element of F

( d in dom f iff ex c being Element of F

P

A4: dom g = F

thus for d being Element of F

( d in dom f iff ex c being Element of F

P

proof

let d be Element of F
let d be Element of F_{1}(); :: thesis: ( d in dom f iff ex c being Element of F_{2}() st P_{1}[d,c] )

dom f c= X by RELAT_1:58;

hence ( d in dom f implies ex c being Element of F_{2}() st P_{1}[d,c] )
by A1; :: thesis: ( ex c being Element of F_{2}() st P_{1}[d,c] implies d in dom f )

assume ex c being Element of F_{2}() st P_{1}[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;dom f c= X by RELAT_1:58;

hence ( d in dom f implies ex c being Element of F

assume ex c being Element of 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

assume A5: d in dom f ; :: thesis: P

dom f c= X by RELAT_1:58;

then ex c being Element of F

then P

then P

hence P