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