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