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