k
>=
1
by
NAT_1:14
;
then
(
n
^
k
>=
n
or
n
<
1 )
by
PREPOWER:12
;
then
(
(
n
^
k
)

n
>=
n

n
or
n
=
0
)
by
XREAL_1:9
,
NAT_1:14
;
then
(
n
^
k
)

n
is
Element
of
NAT
by
INT_1:3
;
hence
(
n
^
k
)

n
is
natural
;
:: thesis:
verum