let z be Complex; :: thesis: z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>)
reconsider z9 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) as Element of COMPLEX by XCMPLX_0:def 2;

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

suppose z = 0 ; :: thesis: z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>)

hence z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) by Th4; :: thesis: verum

end;

suppose A1: z <> 0 ; :: thesis: z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>)

then A2: ((Re z) ^2) + ((Im z) ^2) <> 0 by Th5;
A3: Im z9 = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th12;
then A4: ((Re z) * (Im z9)) + ((Re z9) * (Im z)) = (((Re z) / 1) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) + (((Re z) / (((Re z) ^2) + ((Im z) ^2))) * (Im z)) by Th12
.= (((Re z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) + ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) * (Im z)) / 1) by XCMPLX_1:76
.= (((Re z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) + ((((Im z) / 1) * (Re z)) / (((Re z) ^2) + ((Im z) ^2))) by XCMPLX_1:76
.= ((- ((Re z) * (Im z))) + ((Re z) * (Im z))) / (((Re z) ^2) + ((Im z) ^2)) by XCMPLX_1:62
.= 0 ;
A5: ((Re z) * (Re z9)) - ((Im z) * (Im z9)) = (((Re z) / 1) * ((Re z) / (((Re z) ^2) + ((Im z) ^2)))) - ((Im z) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) by A3, Th12
.= (((Re z) * (Re z)) / (1 * (((Re z) ^2) + ((Im z) ^2)))) - (((Im z) / 1) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:76
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - (((Im z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:76
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - ((- ((Im z) ^2)) / (1 * (((Re z) ^2) + ((Im z) ^2))))
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - (- (((Im z) ^2) / (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:187
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) + (((Im z) ^2) / (1 * (((Re z) ^2) + ((Im z) ^2))))
.= (((Re z) ^2) + ((Im z) ^2)) / (((Re z) ^2) + ((Im z) ^2)) by XCMPLX_1:62
.= 1 by A2, XCMPLX_1:60 ;
z * z9 = [*(((Re z) * (Re z9)) - ((Im z) * (Im z9))),(((Re z) * (Im z9)) + ((Re z9) * (Im z)))*] by Lm16
.= 1 by A5, A4, ARYTM_0:def 5 ;
hence z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) by A1, XCMPLX_0:def 7; :: thesis: verum

end;

end;