let a, b be real number ; :: thesis: ( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b )
reconsider a = a, b = b as 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