let X be RealUnitarySpace; :: 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 M1 being Real such that
A3: M1 > 0 and
A4: for n being Element of NAT holds ||.(seq1 . n).|| <= M1 by A1, Def3;
consider M2 being Real such that
A5: M2 > 0 and
A6: for n being Element of NAT holds ||.(seq2 . n).|| <= M2 by A2, Def3;
A7: M1 + M2 > 0 + 0 by A3, A5;

now

let n be Element of NAT ; :: thesis: ||.((seq1 + seq2) . n).|| <= M1 + M2
A8: ||.(seq1 . n).|| <= M1 by A4;
||.(seq2 . n).|| <= M2 by A6;
then A9: ||.(seq1 . n).|| + ||.(seq2 . n).|| <= M1 + M2 by A8, XREAL_1:9;
||.((seq1 + seq2) . n).|| = ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def 5;
then ||.((seq1 + seq2) . n).|| <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by BHSP_1:36;
hence ||.((seq1 + seq2) . n).|| <= M1 + M2 by A9, XXREAL_0:2; :: thesis: verum

end;

hence seq1 + seq2 is bounded by A7, Def3; :: thesis: verum