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 ;
A6: ( seq . n <> 0. X & ||.seq.|| . n = ||.(seq . n).|| ) by ;
(abs ||.seq.||) . n = |.(||.seq.|| . n).| by SEQ_1:12
.= ||.seq.|| . n by ;
hence ( ||.seq.|| . n <> 0 & rseq1 . n = ((abs ||.seq.||) . (n + 1)) / ((abs ||.seq.||) . n) ) by ; :: thesis: verum
end;
then ||.seq.|| is absolutely_summable by ;
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 ; :: thesis: verum
end;
then abs ||.seq.|| = ||.seq.|| by FUNCT_2:63;
hence seq is norm_summable by A7; :: thesis: verum