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