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 ;

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

( 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

then A4:
s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s)
by NORMSP_1:def 3;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;(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

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