for A being set
for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff for a being Element of A holds o . (a,e) = a )