let z1, z2 be Complex; :: thesis: ( Re z1 = Re z2 & Im z1 = Im z2 implies z1 = z2 )
assume ( Re z1 = Re z2 & Im z1 = Im z2 ) ; :: thesis: z1 = z2
hence z1 = [*(Re z2),(Im z2)*] by Lm3
.= z2 by Lm3 ;
:: thesis: verum