scheme :: BINOP_1:sch 9
Sch9{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ object , object , object ] } :

ex f being Function of [:F₁(),F₂():],F₃() st
for x, y being set st x in F₁() & y in F₂() holds
P₁[x,y,f . (x,y)]

provided

A1: for x, y being set st x in F₁() & y in F₂() holds
ex z being set st
( z in F₃() & P₁[x,y,z] )