let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let seq be sequence of X; :: thesis: for Rseq being Real_Sequence st ( for n being Nat holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let Rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds Rseq . n = n -root ||.(seq . n).|| ) & Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable )
assume that
A1: for n being Nat holds Rseq . n = n -root ||.(seq . n).|| and
A2: ( Rseq is convergent & lim Rseq < 1 ) ; :: thesis: seq is absolutely_summable
for n being Nat holds
( ||.seq.|| . n >= 0 & Rseq . n = n -root (||.seq.|| . n) )

proof

let n be Nat; :: thesis: ( ||.seq.|| . n >= 0 & Rseq . n = n -root (||.seq.|| . n) )
||.seq.|| . n = ||.(seq . n).|| by CLVECT_2:def 3;
hence ||.seq.|| . n >= 0 by CSSPACE:44; :: thesis: Rseq . n = n -root (||.seq.|| . n)
Rseq . n = n -root ||.(seq . n).|| by A1;
hence Rseq . n = n -root (||.seq.|| . n) by CLVECT_2:def 3; :: thesis: verum

end;

then ||.seq.|| is summable by A2, SERIES_1:28;
hence seq is absolutely_summable ; :: thesis: verum