theorem Th90: :: SEQ_4:91

for n being Nat
for z being Element of COMPLEX n holds abs (- z) = abs z