scheme :: FUZNORM1:sch 1
ExBinOp{ F1() -> non empty real-membered set , F2( Real, Real) -> set } :
ex f being BinOp of F1() st
for a, b being Element of F1() holds f . (a,b) = F2(a,b)
provided
A2: for a, b being Element of F1() holds F2(a,b) in F1()