let D be non empty set ; :: thesis: for f being BinOp of D holds {} is f -unambiguous
let f be BinOp of D; :: thesis: {} is f -unambiguous
reconsider A = [:{},D:] as empty set ;
f is A -one-to-one ;
hence {} is f -unambiguous ; :: thesis: verum