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 Lm3; :: thesis: verum