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

now :: thesis: for n being Nat holds
( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )

let n be Nat; :: thesis: ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) )
A3: 0 <= ||.seq.|| . n by Th2;
A4: 0 <= ||.seq.|| . (n + 1) by Th2;
A5: (abs ||.seq.||) . (n + 1) = |.(||.seq.|| . (n + 1)).| by SEQ_1:12
.= ||.seq.|| . (n + 1) by A4, ABSVALUE:def 1 ;
A6: ( seq . n <> 0. X & ||.seq.|| . n = ||.(seq . n).|| ) by A1, NORMSP_0:def 4;
(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12
.= ||.seq.|| . n by A3, ABSVALUE:def 1 ;
hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by A1, A5, A6, NORMSP_0:def 5; :: thesis: verum

end;

then ||.seq.|| is absolutely_summable by A2, SERIES_1:37;
then A7: abs ||.seq.|| is summable ;

now :: thesis: for n being Element of NAT holds (abs ||.seq.||) . n = ||.seq.|| . n

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

end;

then abs ||.seq.|| = ||.seq.|| by FUNCT_2:63;
hence seq is norm_summable by A7; :: thesis: verum