let seq1 be Real_Sequence; :: thesis: ( seq1 is summable implies ex r being real number st
( 0 < r & ( for k being Nat holds abs (Sum (seq1 ^\ k)) < r ) ) )
assume A1: seq1 is summable ; :: thesis: ex r being real number st
( 0 < r & ( for k being Nat holds abs (Sum (seq1 ^\ k)) < r ) )
defpred S₁[ Nat] means ex r being real number st
( r >= 0 & ( for i being Nat st i <= $1 holds
abs (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 number such that
A3: r >= 0 and
A4: for i being Nat st i <= k holds
abs (Sum (seq1 ^\ i)) <= r ;
take M = max (r,(abs (Sum (seq1 ^\ (k + 1))))); :: thesis: ( M >= 0 & ( for i being Nat st i <= k + 1 holds
abs (Sum (seq1 ^\ i)) <= M ) )
thus M >= 0 by A3, XXREAL_0:25; :: thesis: for i being Nat st i <= k + 1 holds
abs (Sum (seq1 ^\ i)) <= M
let i be Nat; :: thesis: ( i <= k + 1 implies abs (Sum (seq1 ^\ i)) <= M )
assume A5: i <= k + 1 ; :: thesis: abs (Sum (seq1 ^\ i)) <= M

now

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

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

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

end;

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

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

end;

end;

end;

hence abs (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 Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs (((Partial_Sums seq1) . m) - (Sum seq1)) < 1 by A8, SEQ_2:def 7;
A10: S₁[ 0 ]

proof

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

end;

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

now

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

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

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

end;

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

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;
k1 + 1 > n by A15;
then k1 >= n by NAT_1:13;
then A16: abs (((Partial_Sums seq1) . k1) - (Sum seq1)) < 1 by A9;
Sum seq1 = ((Partial_Sums seq1) . k1) + (Sum (seq1 ^\ (k1 + 1))) by A1, SERIES_1:18;
then abs (- (Sum (seq1 ^\ (k1 + 1)))) < 1 by A16;
then A17: abs (Sum (seq1 ^\ (k1 + 1))) < 1 by COMPLEX1:138;
1 + 0 <= r1 by A11, XREAL_1:8;
hence abs (Sum (seq1 ^\ k)) < r1 by A17, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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