defpred S1[ Element of F1(), set ] means ( P1[\$1] & \$2 = F3(\$1) );
consider f being PartFunc of F1(),F2() such that
A1: for d being Element of F1() holds
( d in dom f iff ex c being Element of F2() st S1[d,c] ) and
A2: for d being Element of F1() st d in dom f holds
S1[d,f . d] from SEQ_1:sch 2();
take f ; :: thesis: ( ( for d being Element of F1() holds
( d in dom f iff P1[d] ) ) & ( for d being Element of F1() st d in dom f holds
f . d = F3(d) ) )

thus for d being Element of F1() holds
( d in dom f iff P1[d] ) :: thesis: for d being Element of F1() st d in dom f holds
f . d = F3(d)
proof
let d be Element of F1(); :: thesis: ( d in dom f iff P1[d] )
thus ( d in dom f implies P1[d] ) :: thesis: ( P1[d] implies d in dom f )
proof
assume d in dom f ; :: thesis: P1[d]
then ex c being Element of F2() st
( P1[d] & c = F3(d) ) by A1;
hence P1[d] ; :: thesis: verum
end;
assume P1[d] ; :: thesis: d in dom f
then ex c being Element of F2() st
( P1[d] & c = F3(d) ) ;
hence d in dom f by A1; :: thesis: verum
end;
thus for d being Element of F1() st d in dom f holds
f . d = F3(d) by A2; :: thesis: verum