let a be real number ; :: thesis: a |^ 3 = (a * a) * a
a |^ (2 + 1) = (a |^ 2) * a by NEWTON:11;
hence a |^ 3 = (a * a) * a by WSIERP_1:2; :: thesis: verum