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 )

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 :: thesis: ( ( ( 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 ) & ( ( 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 ) ) )

hence
( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )
by Th3; :: thesis: verum( o . (e,a) = a & o . (a,e) = a ) ) implies for a being Element of A holds o . (e,a) = a ) & ( ( 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 ) ) )

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

.= a by A2 ; :: thesis: verum

end;( 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

.= a by A2 ; :: thesis: verum