let
K
be
Field
;
:: thesis:
for
n
being
Nat
holds
(
(
1.
(
K
,
n
)
)
@
)
~
=
1.
(
K
,
n
)
let
n
be
Nat
;
:: thesis:
(
(
1.
(
K
,
n
)
)
@
)
~
=
1.
(
K
,
n
)
(
1.
(
K
,
n
))
@
=
1.
(
K
,
n
)
by
Th10
;
hence
(
(
1.
(
K
,
n
))
@
)
~
=
1.
(
K
,
n
)
by
Th8
;
:: thesis:
verum