let z1, z2 be complex number ; :: 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 Lm4
.= z2 by Lm4 ;
:: thesis: verum