scheme :: BINOP_2:sch 12
NBinOpDefuniq{ F1( Nat, Nat) -> object } :
for o1, o2 being BinOp of NAT st ( for a, b being Nat holds o1 . (a,b) = F1(a,b) ) & ( for a, b being Nat holds o2 . (a,b) = F1(a,b) ) holds
o1 = o2