theorem Th9: :: HERMITAN:9

for a, b being Element of F_Complex holds
( Re (a - b) = (Re a) - (Re b) & Im (a - b) = (Im a) - (Im b) )