let
G
be
strict
Group
;
:: thesis:
for
a
being
Element
of
G
holds
(
Conjugate
(
1_
G
)
)
.
a
=
a
let
a
be
Element
of
G
;
:: thesis:
(
Conjugate
(
1_
G
)
)
.
a
=
a
thus
(
Conjugate
(
1_
G
)
)
.
a
=
a
|^
(
1_
G
)
by
Def6
.=
a
by
GROUP_3:19
;
:: thesis:
verum