let a, b be Real; :: thesis: ( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b )
reconsider a = a, b = b as Element of REAL by XREAL_0:def 1;
a + (b * <i>) = [*a,b*] by Lm21;
hence ( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b ) by Lm2; :: thesis: verum