let X be RealUnitarySpace; :: thesis: for seq1, seq2 being sequence of X st seq1 is absolutely_summable & seq2 is absolutely_summable holds
seq1 + seq2 is absolutely_summable
let seq1, seq2 be sequence of X; :: thesis: ( seq1 is absolutely_summable & seq2 is absolutely_summable implies seq1 + seq2 is absolutely_summable )
A1: for n being Nat holds
( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n )

proof

let n be Nat; :: thesis: ( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n )
||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by BHSP_2:def 3;
hence ||.(seq1 + seq2).|| . n >= 0 by BHSP_1:28; :: thesis: ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n
||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by BHSP_2:def 3
.= ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def 2 ;
then ||.(seq1 + seq2).|| . n <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by BHSP_1:30;
then ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + ||.(seq2 . n).|| by BHSP_2:def 3;
then ||.(seq1 + seq2).|| . n <= (||.seq1.|| . n) + (||.seq2.|| . n) by BHSP_2:def 3;
hence ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n by SEQ_1:7; :: thesis: verum

end;

assume ( seq1 is absolutely_summable & seq2 is absolutely_summable ) ; :: thesis: seq1 + seq2 is absolutely_summable
then ( ||.seq1.|| is summable & ||.seq2.|| is summable ) ;
then ||.seq1.|| + ||.seq2.|| is summable by SERIES_1:7;
then ||.(seq1 + seq2).|| is summable by A1, SERIES_1:20;
hence seq1 + seq2 is absolutely_summable ; :: thesis: verum