let X be RealNormSpace; :: thesis: for seq being sequence of X
for rseq1 being Real_Sequence st ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.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 Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 holds
seq is norm_summable
let rseq1 be Real_Sequence; :: thesis: ( ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 implies seq is norm_summable )
assume A1: ( ( for n being Element of NAT holds
( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) ) & rseq1 is convergent & lim rseq1 < 1 ) ; :: thesis: seq is norm_summable

now

let n be Element of NAT ; :: thesis: ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )
A2: ( seq . n <> 0. X & rseq1 . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) ) by A1;
A3: ( 0 <= ||.seq.|| . n & 0 <= ||.seq.|| . (n + 1) ) by Th2;
A4: (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:16
.= ||.seq.|| . n by A3, ABSVALUE:def 1 ;
A5: (abs ||.seq.||) . (n + 1) = abs (||.seq.|| . (n + 1)) by SEQ_1:16
.= ||.seq.|| . (n + 1) by A3, ABSVALUE:def 1 ;
||.seq.|| . n = ||.(seq . n).|| by NORMSP_1:def 10;
hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by A2, A4, A5, NORMSP_1:def 2; :: thesis: verum

end;

then ||.seq.|| is absolutely_summable by A1, SERIES_1:42;
then A6: abs ||.seq.|| is summable by SERIES_1:def 5;

now

let n be Element of NAT ; :: thesis: (abs ||.seq.||) . n = ||.seq.|| . n
A7: 0 <= ||.seq.|| . n by Th2;
thus (abs ||.seq.||) . n = abs (||.seq.|| . n) by SEQ_1:16
.= ||.seq.|| . n by A7, ABSVALUE:def 1 ; :: thesis: verum

end;

then abs ||.seq.|| = ||.seq.|| by FUNCT_2:113;
hence seq is norm_summable by A6, Def4; :: thesis: verum