let x be Nat; :: thesis: x |^ 3 = (x * x) * x
x |^ (2 + 1) = (x |^ 2) * x by NEWTON:6
.= (x * x) * x by NEWTON:81 ;
hence x |^ 3 = (x * x) * x ; :: thesis: verum