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