let X be ComplexNormSpace; :: 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 by Def2;
then A2: ( (Partial_Sums s) ^\ 1 is convergent & lim ((Partial_Sums s) ^\ 1) = lim (Partial_Sums s) ) by Th13;
then A3: lim (((Partial_Sums s) ^\ 1) - (Partial_Sums s)) = (lim (Partial_Sums s)) - (lim (Partial_Sums s)) by A1, CLVECT_1:122
.= 0. X by RLVECT_1:28 ;
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 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 6;
then (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = ((s ^\ 1) . n) + (0. X) by RLVECT_1:28;
hence (((Partial_Sums s) ^\ 1) . n) - ((Partial_Sums s) . n) = (s ^\ 1) . n by RLVECT_1:10; :: thesis: verum

end;

hence s ^\ 1 = ((Partial_Sums s) ^\ 1) - (Partial_Sums s) by NORMSP_1:def 6; :: thesis: verum

end;

then s ^\ 1 is convergent by A1, A2, CLVECT_1:116;
hence ( s is convergent & lim s = 0. X ) by A3, A4, Th14, Th15; :: thesis: verum