let
G
be
Group
;
:: thesis:
for
a
being
Element
of
G
holds
[.
a
,
a
.]
=
1_
G
let
a
be
Element
of
G
;
:: thesis:
[.
a
,
a
.]
=
1_
G
thus
[.
a
,
a
.]
=
(
(
a
*
a
)
"
)
*
(
a
*
a
)
by
Th17
.=
1_
G
by
GROUP_1:def 5
;
:: thesis:
verum