let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let seq be sequence of X; :: thesis: ( ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable implies seq is absolutely_summable )
A1: for n being Nat holds ||.seq.|| . n >= 0
proof
let n be Nat; :: thesis: ||.seq.|| . n >= 0
||.seq.|| . n = ||.(seq . n).|| by BHSP_2:def 3;
hence ||.seq.|| . n >= 0 by BHSP_1:28; :: thesis: verum
end;
assume ( ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable ) ; :: thesis: seq is absolutely_summable
then ||.seq.|| is summable by A1, SERIES_1:20;
hence seq is absolutely_summable ; :: thesis: verum