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