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 )
assume that
A1: seq1 is absolutely_summable and
A2: seq2 is absolutely_summable ; :: thesis: seq1 + seq2 is absolutely_summable
A3: ||.seq1.|| is summable by A1, Def8;
||.seq2.|| is summable by A2, Def8;
then A4: ||.seq1.|| + ||.seq2.|| is summable by A3, SERIES_1:10;
for n being Element of NAT holds
( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n )

proof

let n be Element of NAT ; :: thesis: ( ||.(seq1 + seq2).|| . n >= 0 & ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n )
thus ||.(seq1 + seq2).|| . n >= 0 :: thesis: ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n

proof

||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by BHSP_2:def 3;
hence ||.(seq1 + seq2).|| . n >= 0 by BHSP_1:34; :: thesis: verum

end;

thus ||.(seq1 + seq2).|| . n <= (||.seq1.|| + ||.seq2.||) . n :: thesis: verum

proof

||.(seq1 + seq2).|| . n = ||.((seq1 + seq2) . n).|| by BHSP_2:def 3
.= ||.((seq1 . n) + (seq2 . n)).|| by NORMSP_1:def 5 ;
then ||.(seq1 + seq2).|| . n <= ||.(seq1 . n).|| + ||.(seq2 . n).|| by BHSP_1:36;
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:11; :: thesis: verum

end;

end;

then ||.(seq1 + seq2).|| is summable by A4, SERIES_1:24;
hence seq1 + seq2 is absolutely_summable by Def8; :: thesis: verum