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

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

hence
seq1 + seq2 is bounded
by COMSEQ_2:def 4; :: thesis: verum
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;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