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 by Def2;
then ( (Partial_Sums s) ^\ 1 is convergent & lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) ) by SEQ_4:33;
then A3: lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, SEQ_2:26
.= 0 ;
A4: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s)

proof

now

let n be Element of 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;

then A5: (Partial_Sums s) ^\ 1 = (Partial_Sums s) + (s ^\ 1) by SEQ_1:11;
(s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s)) = s ^\ 1

proof

now

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:11
.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + ((- (Partial_Sums s)) . n)) by SEQ_1:11
.= ((s ^\ 1) . n) + (((Partial_Sums s) . n) + (- ((Partial_Sums s) . n))) by SEQ_1:14
.= (s ^\ 1) . n ; :: thesis: verum

end;

hence (s ^\ 1) + ((Partial_Sums s) - (Partial_Sums s)) = s ^\ 1 by FUNCT_2:113; :: thesis: verum

end;

hence s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by A5, SEQ_1:39; :: thesis: verum

end;

then A6: s ^\ 1 is convergent by A1, SEQ_2:25;
hence s is convergent by SEQ_4:35; :: thesis: lim s = 0
thus lim s = 0 by A3, A4, A6, SEQ_4:36; :: thesis: verum