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:45;
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:40;
|.z.| = |.z.| + (0 * <i>) ;
then A4: ( Re |.z.| = |.z.| & Im |.z.| = 0 ) by COMPLEX1:12;
A5: ( ((z *') / |.z.|) * z = (z * (z *')) / |.z.| & Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) ) by COMPLEX1:40, XCMPLX_1:74;
then A6: Im (((z *') / |.z.|) * z) = ((|.z.| * 0) - ((((Re z) ^2) + ((Im z) ^2)) * 0)) / ((|.z.| ^2) + (0 ^2)) by A3, A4, COMPLEX1:24;
Re (((z *') / |.z.|) * z) = (((((Re z) ^2) + ((Im z) ^2)) * |.z.|) + (0 * 0)) / ((|.z.| ^2) + (0 ^2)) by A5, A3, A4, COMPLEX1:24
.= (|.(z * z).| * |.z.|) / (|.z.| * |.z.|) by COMPLEX1:68
.= |.(z * z).| / |.z.| by A2, XCMPLX_1:91
.= (|.z.| * |.z.|) / |.z.| by COMPLEX1:65
.= |.z.| by A2, XCMPLX_1:89 ;
hence |.z.| + (0 * <i>) = ((z *') / (|.z.| + (0 * <i>))) * z by A6, COMPLEX1:13; :: thesis: verum

end;

end;