theorem :: COMPLEX1:11

for a being Real holds Im (a * <i>) = a