let z be Complex; :: 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, Th5;
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 Th20
.= sqrt ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) ^2) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) ^2)) by Th20
.= sqrt ((((Re z) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2)) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) ^2)) by XCMPLX_1:76
.= sqrt ((((Re z) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2)) + (((- (Im z)) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2))) by XCMPLX_1:76
.= sqrt ((1 * (((Re z) ^2) + ((Im z) ^2))) / ((((Re z) ^2) + ((Im z) ^2)) * (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:62
.= sqrt (1 / (((Re z) ^2) + ((Im z) ^2))) by A2, XCMPLX_1:91
.= 1 / |.z.| by A3, SQUARE_1:18, SQUARE_1:30
.= |.z.| " by XCMPLX_1:215 ; :: thesis: verum

end;

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

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

end;

end;