let X be ComplexNormSpace; :: thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let seq be sequence of X; :: thesis: for rseq1 being Real_Sequence st ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let rseq1 be Real_Sequence; :: thesis: ( ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable )
assume A1: ( ( for n being Nat holds rseq1 . n = n -root (||.seq.|| . n) ) & rseq1 is convergent & lim rseq1 < 1 ) ; :: thesis: seq is norm_summable
for n being Nat holds ||.seq.|| . n >= 0 by Th2;
hence ||.seq.|| is summable by A1, SERIES_1:28; :: according to CLOPBAN3:def 3 :: thesis: verum