for z being Element of F_Complex st z <> 0. F_Complex holds
for n being Nat holds |.(power (z,n)).| = |.z.| to_power n