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

A1: for x being Element of F_{1}()

for y being Element of F_{2}() ex z being Element of F_{3}() st S_{1}[x,y,z]
;

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

for x being Element of F_{1}()

for y being Element of F_{2}() holds S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 3(A1); :: thesis: verum

A1: for x being Element of F

for y being Element of F

thus ex f being Function of [:F

for x being Element of F

for y being Element of F