theorem :: COMPLEX1:80

for z1 being Complex holds |.(1 / z1).| = 1 / |.z1.| by Th48, Th67;