let seq1 be Real_Sequence; :: thesis: ( seq1 is summable implies ex r being real number st
( 0 < r & ( for k being Element of NAT holds abs (Sum (seq1 ^\ k)) < r ) ) )
assume A1: seq1 is summable ; :: thesis: ex r being real number st
( 0 < r & ( for k being Element of NAT holds abs (Sum (seq1 ^\ k)) < r ) )
set P = Partial_Sums seq1;
( Partial_Sums seq1 is convergent & lim (Partial_Sums seq1) = Sum seq1 ) by A1, SERIES_1:def 2, SERIES_1:def 3;
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs (((Partial_Sums seq1) . m) - (Sum seq1)) < 1 by SEQ_2:def 7;
defpred S₁[ Nat] means ex r being real number st
( r >= 0 & ( for i being Element of NAT st i <= $1 holds
abs (Sum (seq1 ^\ i)) <= r ) );
A3: S₁[ 0 ]

proof

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

end;

A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider r being real number such that
A6: ( r >= 0 & ( for i being Element of 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 Element of NAT st i <= k + 1 holds
abs (Sum (seq1 ^\ i)) <= M ) )
thus M >= 0 by A6, XXREAL_0:25; :: thesis: for i being Element of NAT st i <= k + 1 holds
abs (Sum (seq1 ^\ i)) <= M
let i be Element of NAT ; :: thesis: ( i <= k + 1 implies abs (Sum (seq1 ^\ i)) <= M )
assume A7: i <= k + 1 ; :: thesis: abs (Sum (seq1 ^\ i)) <= M

now

per cases ( i = k + 1 or i <= k ) by A7, 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 i <= k ; :: thesis: abs (Sum (seq1 ^\ i)) <= M

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

end;

end;

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A3, A5);
then consider r being real number such that
A8: ( r >= 0 & ( for i being Element of NAT st i <= n holds
abs (Sum (seq1 ^\ i)) <= r ) ) ;
take r1 = r + 1; :: thesis: ( 0 < r1 & ( for k being Element of NAT holds abs (Sum (seq1 ^\ k)) < r1 ) )
r1 > 0 + 0 by A8;
hence r1 > 0 ; :: thesis: for k being Element of NAT holds abs (Sum (seq1 ^\ k)) < r1
let k be Element of NAT ; :: thesis: abs (Sum (seq1 ^\ k)) < r1

now

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

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

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

end;

suppose A9: 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 A9;
then k1 >= n by NAT_1:13;
then ( abs (((Partial_Sums seq1) . k1) - (Sum seq1)) < 1 & Sum seq1 = ((Partial_Sums seq1) . k1) + (Sum (seq1 ^\ (k1 + 1))) ) by A1, A2, SERIES_1:18;
then abs (- (Sum (seq1 ^\ (k1 + 1)))) < 1 ;
then ( abs (Sum (seq1 ^\ (k1 + 1))) < 1 & 1 + 0 <= r1 ) by A8, COMPLEX1:138, XREAL_1:8;
hence abs (Sum (seq1 ^\ k)) < r1 by XXREAL_0:2; :: thesis: verum

end;

end;

end;

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