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