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