set z' = [*(- (Re z)),(- (Im z))*];
[*(- (Re z)),(- (Im z))*] + z = [*((Re [*(- (Re z)),(- (Im z))*]) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm15
.= [*((- (Re z)) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm3
.= [*0 ,((- (Im z)) + (Im z))*] by Lm3
.= 0 by ARYTM_0:def 7 ;
hence for b₁ being Element of COMPLEX holds
( b₁ = - z iff b₁ = (- (Re z)) + ((- (Im z)) * <i> ) ) by Lm21; :: thesis: verum