let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 holds
seq is absolutely_summable
let seq be sequence of X; :: thesis: ( ( for n being Element of NAT holds
( seq . n <> 0. X & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) ) & Rseq is convergent & lim Rseq < 1 implies seq is absolutely_summable )
assume that
A1: for n being Element of NAT holds
( seq . n <> H₁(X) & Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| ) and
A2: Rseq is convergent and
A3: lim Rseq < 1 ; :: thesis: seq is absolutely_summable
for n being Element of NAT holds
( ||.seq.|| . n > 0 & Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) )

proof

let n be Element of NAT ; :: thesis: ( ||.seq.|| . n > 0 & Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) )
thus ||.seq.|| . n > 0 :: thesis: Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n)

proof

seq . n <> H₁(X) by A1;
then A4: ||.(seq . n).|| <> 0 by BHSP_1:32;
||.(seq . n).|| >= 0 by BHSP_1:34;
hence ||.seq.|| . n > 0 by A4, BHSP_2:def 3; :: thesis: verum

end;

thus Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) :: thesis: verum

proof

Rseq . n = ||.(seq . (n + 1)).|| / ||.(seq . n).|| by A1
.= (||.seq.|| . (n + 1)) / ||.(seq . n).|| by BHSP_2:def 3 ;
hence Rseq . n = (||.seq.|| . (n + 1)) / (||.seq.|| . n) by BHSP_2:def 3; :: thesis: verum

end;

end;

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