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 for a being Element of A holds o . e,a = a )
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 for a being Element of A holds o . e,a = a )
let e be Element of A; :: thesis: ( o is commutative implies ( e is_a_unity_wrt o iff for a being Element of A holds o . e,a = a ) )
assume A1: o is commutative ; :: thesis: ( e is_a_unity_wrt o iff for a being Element of A holds o . e,a = a )

now

thus ( ( for a being Element of A holds
( o . e,a = a & o . a,e = a ) ) implies for a being Element of A holds o . e,a = a ) ; :: thesis: ( ( for a being Element of A holds o . e,a = a ) implies for a being Element of A holds
( o . e,a = a & o . a,e = a ) )
assume A2: for a being Element of A holds o . e,a = a ; :: thesis: for a being Element of A holds
( o . e,a = a & o . a,e = a )
let a be Element of A; :: thesis: ( o . e,a = a & o . a,e = a )
thus o . e,a = a by A2; :: thesis: o . a,e = a
thus o . a,e = o . e,a by A1, Def2
.= a by A2 ; :: thesis: verum

end;

hence ( e is_a_unity_wrt o iff for a being Element of A holds o . e,a = a ) by Th11; :: thesis: verum