theorem :: COMSEQ_1:23

for seq1, seq2 being Complex_Sequence holds seq1 - (- seq2) = seq1 + seq2 ;