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