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: for b₁ being Element of COMPLEX holds
( b₁ = z " iff b₁ = ((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) * <i> ) )

hence for b₁ being Element of COMPLEX holds
( b₁ = z " iff b₁ = ((Re z) / (((Re z) ^2 ) + ((Im z) ^2 ))) + (((- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 ))) * <i> ) ) by Th12; :: thesis: verum

end;

suppose A1: z <> 0 ; :: thesis: for b₁ being Element of COMPLEX holds
( b₁ = z " iff b₁ = ((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 Th13;
A3: Im z9 = (- (Im z)) / (((Re z) ^2 ) + ((Im z) ^2 )) by Th28;
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 Th28
.= (((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:77
.= (((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:77
.= ((- ((Re z) * (Im z))) + ((Re z) * (Im z))) / (((Re z) ^2 ) + ((Im z) ^2 )) by XCMPLX_1:63
.= 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, Th28
.= (((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:77
.= (((Re z) ^2 ) / (((Re z) ^2 ) + ((Im z) ^2 ))) - (((Im z) * (- (Im z))) / (1 * (((Re z) ^2 ) + ((Im z) ^2 )))) by XCMPLX_1:77
.= (((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:188
.= (((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:63
.= 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 7 ;
hence for b₁ being Element of COMPLEX holds
( b₁ = z " iff b₁ = ((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;