:: deftheorem defines with-1-annihilating FUZNORM1:def 3 :
for A being real-membered set
for f being BinOp of A holds
( f is with-1-annihilating iff for a being Element of A holds f . (a,1) = 1 );