let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st seq is summable holds
( seq is convergent & lim seq = 0. X )
let seq be sequence of X; :: thesis: ( seq is summable implies ( seq is convergent & lim seq = 0. X ) )
set PSseq = Partial_Sums seq;

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

let n be Nat; :: thesis: ((Partial_Sums seq) ^\ 1) . n = ((Partial_Sums seq) . n) + ((seq ^\ 1) . n)
(Partial_Sums seq) . (n + 1) = ((Partial_Sums seq) . n) + (seq . (n + 1)) by BHSP_4:def 1
.= ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) by NAT_1:def 3 ;
hence ((Partial_Sums seq) ^\ 1) . n = ((Partial_Sums seq) . n) + ((seq ^\ 1) . n) by NAT_1:def 3; :: thesis: verum

end;

then A1: (Partial_Sums seq) ^\ 1 = (Partial_Sums seq) + (seq ^\ 1) by NORMSP_1:def 2;

now :: thesis: for n being Element of NAT holds ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = (seq ^\ 1) . n

let n be Element of NAT ; :: thesis: ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = (seq ^\ 1) . n
thus ((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n = ((seq ^\ 1) . n) + (((Partial_Sums seq) - (Partial_Sums seq)) . n) by NORMSP_1:def 2
.= ((seq ^\ 1) . n) + (((Partial_Sums seq) . n) - ((Partial_Sums seq) . n)) by NORMSP_1:def 3
.= ((seq ^\ 1) . n) + H₁(X) by RLVECT_1:15
.= (seq ^\ 1) . n by RLVECT_1:4 ; :: thesis: verum

end;

then (seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1 by FUNCT_2:63;
then A2: seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) by A1, CSSPACE:76;
assume seq is summable ; :: thesis: ( seq is convergent & lim seq = 0. X )
then A3: Partial_Sums seq is convergent ;
then A4: (Partial_Sums seq) ^\ 1 is convergent by CLVECT_2:90;
then A5: seq ^\ 1 is convergent by A3, A2, CLVECT_2:4;
hence seq is convergent by CLVECT_2:91; :: thesis: lim seq = 0. X
lim ((Partial_Sums seq) ^\ 1) = lim (Partial_Sums seq) by A3, CLVECT_2:90;
then lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) = (lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) by A3, A4, CLVECT_2:14
.= H₁(X) by RLVECT_1:15 ;
hence lim seq = 0. X by A2, A5, CLVECT_2:84, CLVECT_2:91; :: thesis: verum