reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def 2;
set k = ((Re z2) ^2) + ((Im z2) ^2);
A1: Re [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] = Re (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) + (((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>)) by Lm21
.= (Re z2) / (((Re z2) ^2) + ((Im z2) ^2)) by Th28 ;
A2: Im [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] = Im (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) + (((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>)) by Lm21
.= (- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)) by Th28 ;
z1 / z2 = z1 * (z2 ") by XCMPLX_0:def 9
.= z1 * [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] by Lm21
.= [*((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2) + ((Im z2) ^2)))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))),(((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1)))*] by A1, A2, Lm16
.= ((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2) + ((Im z2) ^2)))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * <i>) by Lm21
.= ((((Re z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2)))) - (((Im z1) / 1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) + (((((Re z1) / 1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((((Re z1) * (- (Im z2))) / (1 * (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * ((Im z1) / 1))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) - ((Im z1) * (- (Im z2)))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) * <i>) by XCMPLX_1:120
.= ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + ((((- ((Re z1) * (Im z2))) + ((Im z1) * (Re z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>) by XCMPLX_1:62
.= ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>) ;
hence for b₁ being Element of COMPLEX holds
( b₁ = z1 / z2 iff b₁ = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>) ) ; :: thesis: verum