z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15;
hence for b₁ being Element of COMPLEX holds
( b₁ = z1 + z2 iff b₁ = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i> ) ) by Lm21; :: thesis: verum