defpred S_{1}[ set , set ] means ( P_{1}[$1] & $2 = F_{3}($1) );

consider f being PartFunc of F_{1}(),F_{2}() such that

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

( d in dom f iff ex c being Element of F_{2}() st S_{1}[d,c] )
and

A2: for d being Element of F_{1}() st d in dom f holds

S_{1}[d,f /. d]
from PARTFUN2:sch 1();

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

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

f /. d = F_{3}(d) ) )

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

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

f /. d = F_{3}(d)_{1}() st d in dom f holds

f /. d = F_{3}(d)
by A2; :: thesis: verum

consider f being PartFunc of F

A1: for d being Element of F

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

A2: for d being Element of F

S

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

( d in dom f iff P

f /. d = F

thus for d being Element of F

( d in dom f iff P

f /. d = F

proof

thus
for d being Element of F
let d be Element of F_{1}(); :: thesis: ( d in dom f iff P_{1}[d] )

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

then ex c being Element of F_{2}() st

( P_{1}[d] & c = F_{3}(d) )
;

hence d in dom f by A1; :: thesis: verum

end;thus ( d in dom f implies P

proof

assume
P
assume
d in dom f
; :: thesis: P_{1}[d]

then ex c being Element of F_{2}() st

( P_{1}[d] & c = F_{3}(d) )
by A1;

hence P_{1}[d]
; :: thesis: verum

end;then ex c being Element of F

( P

hence P

then ex c being Element of F

( P

hence d in dom f by A1; :: thesis: verum

f /. d = F