let seq1, seq2 be Complex_Sequence; :: thesis: ( seq1 is bounded & seq2 is bounded implies seq1 + seq2 is bounded )
assume that
A1: seq1 is bounded and
A2: seq2 is bounded ; :: thesis: seq1 + seq2 is bounded
consider r2 being Real such that
0 < r2 and
A3: for n being Nat holds |.(seq2 . n).| < r2 by A2, COMSEQ_2:8;
consider r1 being Real such that
0 < r1 and
A4: for n being Nat holds |.(seq1 . n).| < r1 by A1, COMSEQ_2:8;
for n being Nat holds |.((seq1 + seq2) . n).| < r1 + r2
proof
let n be Nat; :: thesis: |.((seq1 + seq2) . n).| < r1 + r2
A5: n in NAT by ORDINAL1:def 12;
|.((seq1 + seq2) . n).| = |.((seq1 . n) + (seq2 . n)).| by VALUED_1:1, A5;
then A6: |.((seq1 + seq2) . n).| <= |.(seq1 . n).| + |.(seq2 . n).| by COMPLEX1:56;
|.(seq1 . n).| < r1 by A4;
then |.(seq1 . n).| + |.(seq2 . n).| < r1 + r2 by A3, XREAL_1:8;
hence |.((seq1 + seq2) . n).| < r1 + r2 by A6, XXREAL_0:2; :: thesis: verum
end;
hence seq1 + seq2 is bounded by COMSEQ_2:def 4; :: thesis: verum