let z be Element of COMPLEX ; :: thesis: |.z.| + (0 * <i> ) = ((z *' ) / (|.z.| + (0 * <i> ))) * z

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

suppose A1: |.z.| = 0 ; :: thesis: |.z.| + (0 * <i> ) = ((z *' ) / (|.z.| + (0 * <i> ))) * z

then z = 0 by COMPLEX1:131;
hence |.z.| + (0 * <i> ) = ((z *' ) / (|.z.| + (0 * <i> ))) * z by A1; :: thesis: verum

end;

suppose A2: |.z.| <> 0 ; :: thesis: |.z.| + (0 * <i> ) = ((z *' ) / (|.z.| + (0 * <i> ))) * z

A3: Im (z * (z *' )) = 0 by COMPLEX1:126;
|.z.| = |.z.| + (0 * <i> ) ;
then A4: ( Re |.z.| = |.z.| & Im |.z.| = 0 ) by COMPLEX1:28;
A5: ( ((z *' ) / |.z.|) * z = (z * (z *' )) / |.z.| & Re (z * (z *' )) = ((Re z) ^2 ) + ((Im z) ^2 ) ) by COMPLEX1:126, XCMPLX_1:75;
then A6: Im (((z *' ) / |.z.|) * z) = ((|.z.| * 0 ) - ((((Re z) ^2 ) + ((Im z) ^2 )) * 0 )) / ((|.z.| ^2 ) + (0 ^2 )) by A3, A4, COMPLEX1:82;
Re (((z *' ) / |.z.|) * z) = (((((Re z) ^2 ) + ((Im z) ^2 )) * |.z.|) + (0 * 0 )) / ((|.z.| ^2 ) + (0 ^2 )) by A5, A3, A4, COMPLEX1:82
.= (|.(z * z).| * |.z.|) / (|.z.| * |.z.|) by COMPLEX1:154
.= |.(z * z).| / |.z.| by A2, XCMPLX_1:92
.= (|.z.| * |.z.|) / |.z.| by COMPLEX1:151
.= |.z.| by A2, XCMPLX_1:90 ;
hence |.z.| + (0 * <i> ) = ((z *' ) / (|.z.| + (0 * <i> ))) * z by A6, COMPLEX1:29; :: thesis: verum

end;

end;