let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Rseq being Real_Sequence 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 Rseq being Real_Sequence st ( for n being Nat holds ||.seq.|| . n <= Rseq . n ) & Rseq is summable holds
seq is absolutely_summable
let Rseq be Real_Sequence; :: 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 CLVECT_2:def 3;
hence ||.seq.|| . n >= 0 by CSSPACE:44; :: 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