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