theorem :: COMPLEX1:10

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