let a be real number ; :: thesis: Im (a * <i>) = a
a1: a in REAL by XREAL_0:def 1;
thus Im (a * <i>) = ((Re a) * (Im <i>)) + ((Im a) * (Re <i>)) by Th24
.= a by Def2, Th17, a1 ; :: thesis: verum