let
n
be
Nat
;
:: thesis:
n
|^
3
=
(
n
*
n
)
*
n
reconsider
n
=
n
as
Element
of
NAT
by
ORDINAL1:def 12
;
n
|^
(
2
+
1
)
=
(
n
|^
2
)
*
n
by
NEWTON:6
.=
(
n
*
n
)
*
n
by
WSIERP_1:1
;
hence
n
|^
3
=
(
n
*
n
)
*
n
;
:: thesis:
verum