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 (() ^\ 1) = lim () by ;
then A3: lim ((() ^\ 1) - ()) = (lim ()) - (lim ()) by
.= 0. X by RLVECT_1:15 ;
now :: thesis: for n being Nat holds ((() ^\ 1) . n) - (() . n) = (s ^\ 1) . n
let n be Nat; :: thesis: ((() ^\ 1) . n) - (() . n) = (s ^\ 1) . n
(Partial_Sums s) . (n + 1) = (() . n) + (s . (n + 1)) by BHSP_4:def 1;
then (Partial_Sums s) . (n + 1) = (() . n) + ((s ^\ 1) . n) by NAT_1:def 3;
then ((Partial_Sums s) ^\ 1) . n = ((s ^\ 1) . n) + (() . n) by NAT_1:def 3;
then (((Partial_Sums s) ^\ 1) . n) - (() . n) = ((s ^\ 1) . n) + ((() . n) - (() . n)) by RLVECT_1:def 3;
then (((Partial_Sums s) ^\ 1) . n) - (() . n) = ((s ^\ 1) . n) + (0. X) by RLVECT_1:15;
hence (((Partial_Sums s) ^\ 1) . n) - (() . n) = (s ^\ 1) . n by RLVECT_1:4; :: thesis: verum
end;
then A4: s ^\ 1 = (() ^\ 1) - () by NORMSP_1:def 3;
then s ^\ 1 is convergent by ;
hence ( s is convergent & lim s = 0. X ) by A3, A4, Th10, Th11; :: thesis: verum