let seq1, seq2 be Complex_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded )
assume A1: ( seq1 is bounded & seq2 is bounded ) ; :: thesis: seq1 + seq2 is bounded
then consider r1 being Real such that
A2: ( 0 < r1 & ( for n being Element of NAT holds |.(seq1 . n).| < r1 ) ) by COMSEQ_2:8;
consider r2 being Real such that
A3: ( 0 < r2 & ( for n being Element of NAT holds |.(seq2 . n).| < r2 ) ) by A1, COMSEQ_2:8;
for n being Element of NAT holds |.((seq1 + seq2) . n).| < r1 + r2

proof

let n be Element of NAT ; :: thesis: |.((seq1 + seq2) . n).| < r1 + r2
|.((seq1 + seq2) . n).| = |.((seq1 . n) + (seq2 . n)).| by VALUED_1:1;
then A4: |.((seq1 + seq2) . n).| <= |.(seq1 . n).| + |.(seq2 . n).| by COMPLEX1:142;
( |.(seq1 . n).| < r1 & |.(seq2 . n).| < r2 ) by A2, A3;
then |.(seq1 . n).| + |.(seq2 . n).| < r1 + r2 by XREAL_1:10;
hence |.((seq1 + seq2) . n).| < r1 + r2 by A4, XXREAL_0:2; :: thesis: verum

end;

hence seq1 + seq2 is bounded by COMSEQ_2:def 3; :: thesis: verum