theorem Th91: :: SEQ_4:92

for n being Nat
for c being Element of COMPLEX
for z being Element of COMPLEX n holds abs (c * z) = |.c.| * (abs z)