let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
let seq1, seq2 be sequence of X; :: 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 M2 being Real such that
A3: M2 > 0 and
A4: for n being Nat holds ||.(seq2 . n).|| <= M2 by A2;
consider M1 being Real such that
A5: M1 > 0 and
A6: for n being Nat holds ||.(seq1 . n).|| <= M1 by A1;
now :: thesis: for n being Nat holds ||.((seq1 + seq2) . n).|| <= M1 + M2
let n be Nat; :: thesis: ||.((seq1 + seq2) . n).|| <= M1 + M2
||.((seq1 + seq2) . n).|| = ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def 2;
then A7: ||.((seq1 + seq2) . n).|| <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by CSSPACE:46;
( ||.(seq1 . n).|| <= M1 & ||.(seq2 . n).|| <= M2 ) by A6, A4;
then ||.(seq1 . n).|| + ||.(seq2 . n).|| <= M1 + M2 by XREAL_1:7;
hence ||.((seq1 + seq2) . n).|| <= M1 + M2 by A7, XXREAL_0:2; :: thesis: verum
end;
hence seq1 + seq2 is bounded by A5, A3; :: thesis: verum