let z be complex number ; :: thesis: |.(- z).| = |.z.|
thus |.(- z).| = sqrt (((- (Re z)) ^2) + ((Im (- z)) ^2)) by Th34
.= sqrt (((- (Re z)) ^2) + ((- (Im z)) ^2)) by Th34
.= |.z.| ; :: thesis: verum