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

proof

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

proof

assume A6: [x,y] in dom f ; :: thesis: ( x in F₁() & y in F₂() & P₁[x,y] )
then ex z being set st
( P₁[x,y] & z = F₄(x,y) ) by A4;
hence ( x in F₁() & y in F₂() & P₁[x,y] ) by A4, A6; :: thesis: verum

end;

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

end;

thus for x, y being set st [x,y] in dom f holds
f . x,y = F₄(x,y) by A5; :: thesis: verum