defpred S₁[ set , set ] means ( P₁[$1] & $2 = F₃($1) );
consider f being PartFunc of , such that
A1: for d being Element of F₁() holds
( d in dom f iff ex c being Element of F₂() st S₁[d,c] ) and
A2: for d being Element of F₁() st d in dom f holds
S₁[d,f /. d] from PARTFUN2:sch 1();
take f ; :: thesis: ( ( for d being Element of F₁() holds
( d in dom f iff P₁[d] ) ) & ( for d being Element of F₁() st d in dom f holds
f /. d = F₃(d) ) )
thus for d being Element of F₁() holds
( d in dom f iff P₁[d] ) :: thesis: for d being Element of F₁() st d in dom f holds
f /. d = F₃(d)

proof

let d be Element of F₁(); :: thesis: ( d in dom f iff P₁[d] )
thus ( d in dom f implies P₁[d] ) :: thesis: ( P₁[d] implies d in dom f )

proof

assume d in dom f ; :: thesis: P₁[d]
then ex c being Element of F₂() st
( P₁[d] & c = F₃(d) ) by A1;
hence P₁[d] ; :: thesis: verum

end;

assume P₁[d] ; :: thesis: d in dom f
then ex c being Element of F₂() st
( P₁[d] & c = F₃(d) ) ;
hence d in dom f by A1; :: thesis: verum

end;

thus for d being Element of F₁() st d in dom f holds
f /. d = F₃(d) by A2; :: thesis: verum