A1: z1 = (Re z1) + ((Im z1) * <i>) by Th29;
z1 - z2 = z1 + (- z2)
.= z1 + ((- (Re z2)) + ((- (Im z2)) * <i>)) by Def11
.= ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) by A1 ;
hence for b₁ being Element of COMPLEX holds
( b₁ = z1 - z2 iff b₁ = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) ) ; :: thesis: verum