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 | A is one-to-one ;
then f is A -one-to-one by DefInj1;
hence {} is f -unambiguous by DefUnambiguous1; :: thesis: verum