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