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