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;
assume seq is summable ; :: thesis: ( seq is convergent & lim seq = 0. X )
then A1: Partial_Sums seq is convergent by Def2;
then A2: ( (Partial_Sums seq) ^\ 1 is convergent & lim ((Partial_Sums seq) ^\ 1) = lim (Partial_Sums seq) ) by BHSP_3:44;
then A3: lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) = (lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) by A1, BHSP_2:14
.= H₁(X) by RLVECT_1:28 ;
A4: seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)

proof

now

let n be Element of 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 A5: (Partial_Sums seq) ^\ 1 = (Partial_Sums seq) + (seq ^\ 1) by NORMSP_1:def 5;
(seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1

proof

now

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 5
.= ((seq ^\ 1) . n) + (((Partial_Sums seq) . n) - ((Partial_Sums seq) . n)) by NORMSP_1:def 6
.= ((seq ^\ 1) . n) + H₁(X) by RLVECT_1:28
.= (seq ^\ 1) . n by RLVECT_1:10 ; :: thesis: verum

end;

hence (seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) = seq ^\ 1 by FUNCT_2:113; :: thesis: verum

end;

hence seq ^\ 1 = ((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) by A5, BHSP_1:83; :: thesis: verum

end;

then A6: seq ^\ 1 is convergent by A1, A2, BHSP_2:4;
hence seq is convergent by BHSP_3:46; :: thesis: lim seq = 0. X
thus lim seq = 0. X by A3, A4, A6, BHSP_3:33, BHSP_3:46; :: thesis: verum