A2: for x, y being object st x in F1() & y in F2() & P1[x,y] holds
F4(x,y) in F3() by A1;
consider f being PartFunc of [:F1(),F2():],F3() such that
A3: ( ( for x, y being object holds
( [x,y] in dom f iff ( x in F1() & y in F2() & P1[x,y] ) ) ) & ( for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) ) from BINOP_1:sch 7(A2);
 take f ; :: thesis: ( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
thus ( ( for x being Element of F1()
for y being Element of F2() holds
( [x,y] in dom f iff P1[x,y] ) ) & ( for x being Element of F1()
for y being Element of F2() st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) ) by A3; :: thesis: verum