theorem :: COMSEQ_1:11

for seq being Complex_Sequence holds - seq = (- 1r) (#) seq ;