defpred S_{1}[ object , object , object ] means $3 = F_{4}($1,$2);

A2: for x, y being object st x in F_{1}() & y in F_{2}() holds

ex z being object st

( z in F_{3}() & S_{1}[x,y,z] )
by A1;

thus ex f being Function of [:F_{1}(),F_{2}():],F_{3}() st

for x, y being object st x in F_{1}() & y in F_{2}() holds

S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 1(A2); :: thesis: verum

A2: for x, y being object st x in F

ex z being object st

( z in F

thus ex f being Function of [:F

for x, y being object st x in F

S