scheme :: BINOP_1:sch 3
FuncEx2D{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , P1[ object , object , object ] } :
ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds P1[x,y,f . (x,y)]
provided
A1: for x being Element of F1()
for y being Element of F2() ex z being Element of F3() st P1[x,y,z]