theorem Th94: :: SEQ_4:95

for n being Nat
for z being Element of COMPLEX n holds 0 <= |.z.|