:: deftheorem defines *' COMPLEX1:def 11 :
for z being Complex holds z *' = (Re z) - ((Im z) * <i>);