:: deftheorem defines the_unity_wrt BINOP_1:def 8 :
for A being set
for o being BinOp of A st ex e being Element of A st e is_a_unity_wrt o holds
for b₃ being Element of A holds
( b₃ = the_unity_wrt o iff b₃ is_a_unity_wrt o );