let X be RealUnitarySpace; :: 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 Def1
.= ((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;
(seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1

proof

let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: K64(((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))),n) = K64((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 ; :: thesis: verum

end;

then A2: seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) by A1, BHSP_1:61;
assume seq is summable ; :: thesis: ( seq is convergent & lim seq = 0. X )
then A3: Partial_Sums seq is convergent ;
A4: seq ^\ 1 is convergent by A3, A2, BHSP_2:4;
hence seq is convergent by BHSP_3:37; :: thesis: lim seq = 0. X
lim ((Partial_Sums seq) ^\ 1) = lim (Partial_Sums seq) by A3, BHSP_3:36;
then lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) = (lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) by A3, BHSP_2:14
.= H₁(X) by RLVECT_1:15 ;
hence lim seq = 0. X by A2, A4, BHSP_3:28, BHSP_3:37; :: thesis: verum