theorem :: POLYEQ_3:40
for z, s being Element of COMPLEX
for n being Element of NAT st s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n holds
|.s.| = |.z.|