let X be RealNormSpace; :: thesis: for s being sequence of X st s is summable holds
( s is convergent & lim s = 0. X )
let s be sequence of X; :: thesis: ( s is summable implies ( s is convergent & lim s = 0. X ) )
assume s is summable ; :: thesis: ( s is convergent & lim s = 0. X )
then A1: Partial_Sums s is convergent ;
then A2: (Partial_Sums s) ^\ 1 is convergent by Th7;
lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) by A1, Th8;
then A3: lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, A2, NORMSP_1:26
.= 0. X by RLVECT_1:15 ;

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

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 BHSP_4:def 1;
then (Partial_Sums s) . (n + 1) = ((Partial_Sums s) . n) + ((s ^\ 1) . n) by NAT_1:def 3;
then ((Partial_Sums s) ^\ 1) . n = ((s ^\ 1) . n) + ((Partial_Sums s) . n) by NAT_1:def 3;
then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (((Partial_Sums s) . n) - ((Partial_Sums s) . n)) by RLVECT_1:def 3;
then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (0. X) by RLVECT_1:15;
hence (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = (s ^\ 1) . n by RLVECT_1:4; :: thesis: verum

end;

then A4: s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by NORMSP_1:def 3;
then s ^\ 1 is convergent by A1, A2, NORMSP_1:20;
hence ( s is convergent & lim s = 0. X ) by A3, A4, Th10, Th11; :: thesis: verum