z = (Re z) + ((Im z) * <i>) by COMPLEX1:13;
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