let A be set ; :: thesis: for o being BinOp of A
for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff e is_a_left_unity_wrt o )
let o be BinOp of A; :: thesis: for e being Element of A st o is commutative holds
( e is_a_unity_wrt o iff e is_a_left_unity_wrt o )
let e be Element of A; :: thesis: ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) )
( e is_a_left_unity_wrt o iff for a being Element of A holds o . e,a = a ) by Def5;
hence ( o is commutative implies ( e is_a_unity_wrt o iff e is_a_left_unity_wrt o ) ) by Th12; :: thesis: verum