let seq1 be Real_Sequence; :: thesis: ( seq1 is summable implies ex r being Real st
( 0 < r & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r ) ) )
assume A1: seq1 is summable ; :: thesis: ex r being Real st
( 0 < r & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r ) )
defpred S₁[ Nat] means ex r being Real st
( r >= 0 & ( for i being Nat st i <= $1 holds
|.(Sum (seq1 ^\ i)).| <= r ) );
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider r being Real such that
A3: r >= 0 and
A4: for i being Nat st i <= k holds
|.(Sum (seq1 ^\ i)).| <= r ;
take M = max (r,|.(Sum (seq1 ^\ (k + 1))).|); :: thesis: ( M >= 0 & ( for i being Nat st i <= k + 1 holds
|.(Sum (seq1 ^\ i)).| <= M ) )
thus M >= 0 by A3, XXREAL_0:25; :: thesis: for i being Nat st i <= k + 1 holds
|.(Sum (seq1 ^\ i)).| <= M
let i be Nat; :: thesis: ( i <= k + 1 implies |.(Sum (seq1 ^\ i)).| <= M )
assume A5: i <= k + 1 ; :: thesis: |.(Sum (seq1 ^\ i)).| <= M

now :: thesis: |.(Sum (seq1 ^\ i)).| <= M

per cases ( i = k + 1 or i <= k ) by A5, NAT_1:8;

suppose i = k + 1 ; :: thesis: |.(Sum (seq1 ^\ i)).| <= M

hence |.(Sum (seq1 ^\ i)).| <= M by XXREAL_0:25; :: thesis: verum

end;

suppose A6: i <= k ; :: thesis: |.(Sum (seq1 ^\ i)).| <= M

A7: r <= M by XXREAL_0:25;
|.(Sum (seq1 ^\ i)).| <= r by A4, A6;
hence |.(Sum (seq1 ^\ i)).| <= M by A7, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.(Sum (seq1 ^\ i)).| <= M ; :: thesis: verum

end;

set P = Partial_Sums seq1;
A8: lim (Partial_Sums seq1) = Sum seq1 by SERIES_1:def 3;
Partial_Sums seq1 is convergent by A1, SERIES_1:def 2;
then consider n being Nat such that
A9: for m being Nat st n <= m holds
|.(((Partial_Sums seq1) . m) - (Sum seq1)).| < 1 by A8, SEQ_2:def 7;
A10: S₁[ 0 ]

proof

take |.(Sum seq1).| ; :: thesis: ( |.(Sum seq1).| >= 0 & ( for i being Nat st i <= 0 holds
|.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).| ) )
thus |.(Sum seq1).| >= 0 by COMPLEX1:46; :: thesis: for i being Nat st i <= 0 holds
|.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).|
let i be Nat; :: thesis: ( i <= 0 implies |.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).| )
assume i <= 0 ; :: thesis: |.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).|
then i = 0 ;
hence |.(Sum (seq1 ^\ i)).| <= |.(Sum seq1).| by NAT_1:47; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A2);
then consider r being Real such that
A11: r >= 0 and
A12: for i being Nat st i <= n holds
|.(Sum (seq1 ^\ i)).| <= r ;
take r1 = r + 1; :: thesis: ( 0 < r1 & ( for k being Nat holds |.(Sum (seq1 ^\ k)).| < r1 ) )
thus r1 > 0 by A11; :: thesis: for k being Nat holds |.(Sum (seq1 ^\ k)).| < r1
let k be Nat; :: thesis: |.(Sum (seq1 ^\ k)).| < r1

now :: thesis: |.(Sum (seq1 ^\ k)).| < r1

per cases ( k <= n or k > n ) ;

suppose A13: k <= n ; :: thesis: |.(Sum (seq1 ^\ k)).| < r1

A14: 0 + r < r1 by XREAL_1:8;
|.(Sum (seq1 ^\ k)).| <= r by A12, A13;
hence |.(Sum (seq1 ^\ k)).| < r1 by A14, XXREAL_0:2; :: thesis: verum

end;

suppose A15: k > n ; :: thesis: |.(Sum (seq1 ^\ k)).| < r1

then reconsider k1 = k - 1 as Nat by NAT_1:20;
k1 + 1 > n by A15;
then k1 >= n by NAT_1:13;
then A16: |.(((Partial_Sums seq1) . k1) - (Sum seq1)).| < 1 by A9;
Sum seq1 = ((Partial_Sums seq1) . k1) + (Sum (seq1 ^\ (k1 + 1))) by A1, SERIES_1:15;
then |.(- (Sum (seq1 ^\ (k1 + 1)))).| < 1 by A16;
then A17: |.(Sum (seq1 ^\ (k1 + 1))).| < 1 by COMPLEX1:52;
1 + 0 <= r1 by A11, XREAL_1:6;
hence |.(Sum (seq1 ^\ k)).| < r1 by A17, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.(Sum (seq1 ^\ k)).| < r1 ; :: thesis: verum