theorem :: HAHNBAN1:11

for x, y being Element of F_Complex holds
( Re (x * y) = ((Re x) * (Re y)) - ((Im x) * (Im y)) & Im (x * y) = ((Re x) * (Im y)) + ((Re y) * (Im x)) ) by COMPLEX1:9;