:: deftheorem Def10 defines -unambiguous FOMODEL0:def 10 :
for D being non empty set
for f being BinOp of D
for X being set holds
( X is f -unambiguous iff for x, y, d1, d2 being set st x in X /\ D & y in X /\ D & d1 in D & d2 in D & f . (x,d1) = f . (y,d2) holds
( x = y & d1 = d2 ) );