theorem Th15: :: COMSEQ_3:15

for seq1, seq2 being Complex_Sequence holds
( (Re seq1) + (Re seq2) = Re (seq1 + seq2) & (Im seq1) + (Im seq2) = Im (seq1 + seq2) )