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