theorem :: COMSEQ_1:22

for seq being Complex_Sequence holds - (- seq) = seq ;