for a being non zero Real
for a1 being Complex st a * a1 is Real holds
a1 is Real