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