defpred S₁[ object , object ] means ( P₁[$1] & $2 = F₃($1) );
A2: for x, y1, y2 being object st x in F₁() & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A3: for x, y being object st x in F₁() & S₁[x,y] holds
y in F₂() by A1;
consider f being PartFunc of F₁(),F₂() such that
A4: for x being object holds
( x in dom f iff ( x in F₁() & ex y being object st S₁[x,y] ) ) and
A5: for x being object st x in dom f holds
S₁[x,f . x] from PARTFUN1:sch 2(A3, A2);
take f ; :: thesis: ( ( for x being object holds
( x in dom f iff ( x in F₁() & P₁[x] ) ) ) & ( for x being object st x in dom f holds
f . x = F₃(x) ) )
thus for x being object holds
( x in dom f iff ( x in F₁() & P₁[x] ) ) :: thesis: for x being object st x in dom f holds
f . x = F₃(x)

proof

let x be object ; :: thesis: ( x in dom f iff ( x in F₁() & P₁[x] ) )
thus ( x in dom f implies ( x in F₁() & P₁[x] ) ) :: thesis: ( x in F₁() & P₁[x] implies x in dom f )

proof

assume A6: x in dom f ; :: thesis: ( x in F₁() & P₁[x] )
then ex y being object st
( P₁[x] & y = F₃(x) ) by A4;
hence ( x in F₁() & P₁[x] ) by A6; :: thesis: verum

end;

assume that
A7: x in F₁() and
A8: P₁[x] ; :: thesis: x in dom f
ex y being object st
( P₁[x] & y = F₃(x) ) by A8;
hence x in dom f by A4, A7; :: thesis: verum

end;

thus for x being object st x in dom f holds
f . x = F₃(x) by A5; :: thesis: verum