let z be Complex; :: thesis: ( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 )
z |^ 3 = z |^ (2 + 1)
.= (z |^ (1 + 1)) * z by NEWTON:6
.= ((z |^ 1) * z) * z by NEWTON:6
.= (z * z) * z ;
hence ( z |^ 3 = (z * z) * z & z |^ 3 = (z ^2) * z & z |^ 3 = z ^3 ) ; :: thesis: verum