:: deftheorem defines -unambiguous FOMODEL0:def 2 :
for D being non empty set
for f being BinOp of D
for X being set holds
( X is f -unambiguous iff f is [:X,D:] -one-to-one );