for seq1, seq2 being Complex_Sequence st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded by Lm3;