let s be Real_Sequence; :: thesis: ( s is summable implies ( s is convergent & lim s = 0 ) )

assume s is summable ; :: thesis: ( s is convergent & lim s = 0 )

then A1: Partial_Sums s is convergent ;

then A3: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by A2, SEQ_1:31;

then A4: s ^\ 1 is convergent by A1;

hence s is convergent by SEQ_4:21; :: thesis: lim s = 0

lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, SEQ_4:20;

then lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, SEQ_2:12

.= 0 ;

hence lim s = 0 by A3, A4, SEQ_4:22; :: thesis: verum

assume s is summable ; :: thesis: ( s is convergent & lim s = 0 )

then A1: Partial_Sums s is convergent ;

now :: thesis: for n being Nat holds ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n)

then A2:
(Partial_Sums s) ^\ 1 = (Partial_Sums s) + (s ^\ 1)
by SEQ_1:7;let n be Nat; :: thesis: ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n)

(Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by Def1;

then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3;

hence ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3; :: thesis: verum

end;(Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + (s . (n + 1)) by Def1;

then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3;

hence ((Partial_Sums s) ^\ 1) . n = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3; :: thesis: verum

now :: thesis: for n being Element of NAT holds ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = (s ^\ 1) . n

then
(s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s)) = s ^\ 1
;let n be Element of NAT ; :: thesis: ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = (s ^\ 1) . n

thus ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = ((s ^\ 1) . n) + (((Partial_Sums s) + (- (Partial_Sums s))) . n) by SEQ_1:7

.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + ((- (Partial_Sums s)) . n)) by SEQ_1:7

.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + (- ((Partial_Sums s) . n))) by SEQ_1:10

.= (s ^\ 1) . n ; :: thesis: verum

end;thus ((s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s))) . n = ((s ^\ 1) . n) + (((Partial_Sums s) + (- (Partial_Sums s))) . n) by SEQ_1:7

.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + ((- (Partial_Sums s)) . n)) by SEQ_1:7

.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + (- ((Partial_Sums s) . n))) by SEQ_1:10

.= (s ^\ 1) . n ; :: thesis: verum

then A3: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by A2, SEQ_1:31;

then A4: s ^\ 1 is convergent by A1;

hence s is convergent by SEQ_4:21; :: thesis: lim s = 0

lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, SEQ_4:20;

then lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, SEQ_2:12

.= 0 ;

hence lim s = 0 by A3, A4, SEQ_4:22; :: thesis: verum