let a be Complex; :: thesis: (a * a) * a = a |^ 3
thus (a * a) * a = (a |^ 2) * a by Th1
.= a |^ (2 + 1) by NEWTON:6
.= a |^ 3 ; :: thesis: verum