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