let G be Group; for a being Element of G holds
( ((1). G) * a = {a} & a * ((1). G) = {a} )
let a be Element of G; ( ((1). G) * a = {a} & a * ((1). G) = {a} )
A1:
the carrier of ((1). G) = {(1_ G)}
by Def7;
hence ((1). G) * a =
{((1_ G) * a)}
by Th18
.=
{a}
by GROUP_1:def 4
;
a * ((1). G) = {a}
thus a * ((1). G) =
{(a * (1_ G))}
by A1, Th18
.=
{a}
by GROUP_1:def 4
; verum