theorem :: COMSEQ_3:20

for seq being Complex_Sequence
for z being Complex holds
( Re (z (#) seq) = ((Re z) (#) (Re seq)) - ((Im z) (#) (Im seq)) & Im (z (#) seq) = ((Re z) (#) (Im seq)) + ((Im z) (#) (Re seq)) )