let a be Real; :: thesis: Im (a * <i>) = a
thus Im (a * <i>) = ((Re a) * (Im <i>)) + ((Im a) * (Re <i>)) by Th9
.= a by Def1, Th7 ; :: thesis: verum