let s be Real_Sequence; :: thesis: ( s is absolutely_summable implies s is summable )

assume s is absolutely_summable ; :: thesis: s is summable

then A1: abs s is summable ;

assume s is absolutely_summable ; :: thesis: s is summable

then A1: abs s is summable ;

now :: thesis: for r being Real st 0 < r holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

hence
s is summable
by Th21; :: thesis: verumex n being Nat st

for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st

for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r )

assume 0 < r ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

then consider n being Nat such that

A2: for m being Nat st n <= m holds

|.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| < r by A1, Th21;

take n = n; :: thesis: for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

let m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r )

assume A3: n <= m ; :: thesis: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

then A4: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| by Th34;

|.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| < r by A2, A3;

hence |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r by A4, XXREAL_0:2; :: thesis: verum

end;for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r )

assume 0 < r ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

then consider n being Nat such that

A2: for m being Nat st n <= m holds

|.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| < r by A1, Th21;

take n = n; :: thesis: for m being Nat st n <= m holds

|.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

let m be Nat; :: thesis: ( n <= m implies |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r )

assume A3: n <= m ; :: thesis: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r

then A4: |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| <= |.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| by Th34;

|.(((Partial_Sums (abs s)) . m) - ((Partial_Sums (abs s)) . n)).| < r by A2, A3;

hence |.(((Partial_Sums s) . m) - ((Partial_Sums s) . n)).| < r by A4, XXREAL_0:2; :: thesis: verum