defpred S1[ object , object ] means ( $1 in F1() & $2 in F2() & P1[$1,$2] );
A2:
for x, y being object st S1[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() & S1[x,y] ) ) ) & ( for x, y being object st [x,y] in dom f holds
f . (x,y) = F4(x,y) ) )
from BINOP_1:sch 6(A2);
take
f
; ( ( 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) ) )
thus
( ( 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) ) )
by A3; verum