scheme :: BINOP_2:sch 2
BinOpDefuniq{ F₁() -> non empty set , F₂( Element of F₁(), Element of F₁()) -> object } :

for o1, o2 being BinOp of F₁() st ( for a, b being Element of F₁() holds o1 . (a,b) = F₂(a,b) ) & ( for a, b being Element of F₁() holds o2 . (a,b) = F₂(a,b) ) holds
o1 = o2