let A be 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 . (e,a) = a )
let o be 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 e be Element of A; ( 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
; ( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )
now ( ( ( 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 ) ) )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 )
;
( ( 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
;
for a being Element of A holds
( o . (e,a) = a & o . (a,e) = a )let a be
Element of
A;
( o . (e,a) = a & o . (a,e) = a )thus
o . (
e,
a)
= a
by A2;
o . (a,e) = athus o . (
a,
e) =
o . (
e,
a)
by A1
.=
a
by A2
;
verum end;
hence
( e is_a_unity_wrt o iff for a being Element of A holds o . (e,a) = a )
by Th3; verum