consider M2 being Real such that
A1: M2 > 0 and
A2: for n being Nat holds ||.(seq2 . n).|| <= M2 by Def3;
consider M1 being Real such that
A3: M1 > 0 and
A4: for n being Nat holds ||.(seq1 . n).|| <= M1 by Def3;
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 A5: ||.((seq1 + seq2) . n).|| <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by BHSP_1:30;
( ||.(seq1 . n).|| <= M1 & ||.(seq2 . n).|| <= M2 ) by A4, A2;
then ||.(seq1 . n).|| + ||.(seq2 . n).|| <= M1 + M2 by XREAL_1:7;
hence ||.((seq1 + seq2) . n).|| <= M1 + M2 by A5, XXREAL_0:2; :: thesis: verum
end;
hence seq1 + seq2 is bounded by A3, A1; :: thesis: verum