let
x
,
y
,
z
be
Element
of
(
opp
K
)
;
:: according to
GROUP_1:def 3
:: thesis:
(
x
*
y
)
*
z
=
x
*
(
y
*
z
)
reconsider
a
=
x
,
b
=
y
,
c
=
z
as
Element
of
K
;
thus
(
x
*
y
)
*
z
=
c
*
(
b
*
a
)
by
Lm4
.=
(
c
*
b
)
*
a
by
GROUP_1:def 3
.=
x
*
(
y
*
z
)
by
Lm4
;
:: thesis:
verum