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