let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of 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 Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let seq be sequence of X; :: thesis: ( ( for n being Element of NAT holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable implies seq is absolutely_summable )
A1: for n being Element of NAT holds ||.seq.|| . n >= 0

proof

let n be Element of 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 Element of 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 by Def8; :: thesis: verum