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