let rseq be Real_Sequence; :: thesis: ( ( for n being Nat holds rseq . n = 0 ) implies rseq is absolutely_summable )
assume A1: for n being Nat holds rseq . n = 0 ; :: thesis: rseq is absolutely_summable
take 0 ; :: according to COMSEQ_2:def 5,SERIES_1:def 2,SERIES_1:def 4 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= |.(((Partial_Sums (abs rseq)) . b₃) - 0).| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((Partial_Sums (abs rseq)) . b₂) - 0).| ) )
assume A2: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= |.(((Partial_Sums (abs rseq)) . b₂) - 0).| )
take 0 ; :: thesis: for b₁ being set holds
( not 0 <= b₁ or not p <= |.(((Partial_Sums (abs rseq)) . b₁) - 0).| )
let m be Nat; :: thesis: ( not 0 <= m or not p <= |.(((Partial_Sums (abs rseq)) . m) - 0).| )
assume 0 <= m ; :: thesis: not p <= |.(((Partial_Sums (abs rseq)) . m) - 0).|
|.(((Partial_Sums (abs rseq)) . m) - 0).| = |.(0 - 0).| by A1, Th2
.= 0 by ABSVALUE:def 1 ;
hence |.(((Partial_Sums (abs rseq)) . m) - 0).| < p by A2; :: thesis: verum