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