let
g
be
Element
of
G
;
:: thesis:
(
g
=
g
|^
n
iff
g
=
(
power
G
)
.
(
g
,
n
) )
|.
n
.|
=
n
by
ABSVALUE:def 1
;
hence
(
g
=
g
|^
n
iff
g
=
(
power
G
)
.
(
g
,
n
) )
by
Def5
;
:: thesis:
verum