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