let G be Group; for a being Element of G holds ((1). G) |^ a = (1). G
let a be Element of G; ((1). G) |^ a = (1). G
A1:
the carrier of ((1). G) = {(1_ G)}
by GROUP_2:def 7;
the carrier of (((1). G) |^ a) =
(carr ((1). G)) |^ a
by Def6
.=
{((1_ G) |^ a)}
by A1, Th37
.=
{(1_ G)}
by Th17
;
hence
((1). G) |^ a = (1). G
by GROUP_2:def 7; verum