let z be complex number ; :: thesis: |.(z " ).| = |.z.| "

per cases ( z <> 0 or z = 0 ) ;

suppose A1: z <> 0 ; :: thesis: |.(z " ).| = |.z.| "

set r2i2 = ((Re z) ^2 ) + ((Im z) ^2 );
A2: ((Re z) ^2 ) + ((Im z) ^2 ) <> 0 by A1, Th13;
A3: 0 <= ((Re z) ^2 ) + ((Im z) ^2 ) by Lm1;
thus |.(z " ).| = sqrt ((((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) ^2 ) + ((Im (z " )) ^2 )) by Th64
.= sqrt ((((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) ^2 ) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) ^2 )) by Th64
.= sqrt ((((Re z) ^2 ) / ((((Re z) ^2 ) + ((Im z) ^2 )) ^2 )) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) ^2 )) by XCMPLX_1:77
.= sqrt ((((Re z) ^2 ) / ((((Re z) ^2 ) + ((Im z) ^2 )) ^2 )) + (((- (Im z)) ^2 ) / ((((Re z) ^2 ) + ((Im z) ^2 )) ^2 ))) by XCMPLX_1:77
.= sqrt ((1 * (((Re z) ^2 ) + ((Im z) ^2 ))) / ((((Re z) ^2 ) + ((Im z) ^2 )) * (((Re z) ^2 ) + ((Im z) ^2 )))) by XCMPLX_1:63
.= sqrt (1 / (((Re z) ^2 ) + ((Im z) ^2 ))) by A2, XCMPLX_1:92
.= 1 / |.z.| by A3, SQUARE_1:83, SQUARE_1:99
.= |.z.| " by XCMPLX_1:217 ; :: thesis: verum

end;

suppose A4: z = 0 ; :: thesis: |.(z " ).| = |.z.| "

hence |.(z " ).| = 0 "
.= |.z.| " by A4 ;
:: thesis: verum

end;

end;