let X be RealUnitarySpace; :: thesis: for seq being sequence of X st ex k being Element of NAT st seq ^\ k is summable holds
seq is summable
let seq be sequence of X; :: thesis: ( ex k being Element of NAT st seq ^\ k is summable implies seq is summable )
given k being Element of NAT such that A1: seq ^\ k is summable ; :: thesis: seq is summable
(seq ^\ k) ^\ 1 is summable by A1, Th13;
then A2: Partial_Sums ((seq ^\ k) ^\ 1) is convergent by Def2;
reconsider seq1 = NAT --> ((Partial_Sums seq) . k) as sequence of X ;
defpred S₁[ Element of NAT ] means ((Partial_Sums seq) ^\ (k + 1)) . $1 = ((Partial_Sums (seq ^\ (k + 1))) . $1) + (seq1 . $1);
A3: (Partial_Sums (seq ^\ (k + 1))) . 0 = (seq ^\ (k + 1)) . 0 by Def1
.= seq . (0 + (k + 1)) by NAT_1:def 3
.= seq . (k + 1) ;

A4: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A5: S₁[m] ; :: thesis: S₁[m + 1]
((Partial_Sums (seq ^\ (k + 1))) . (m + 1)) + (seq1 . (m + 1)) = (seq1 . (m + 1)) + (((Partial_Sums (seq ^\ (k + 1))) . m) + ((seq ^\ (k + 1)) . (m + 1))) by Def1
.= ((seq1 . (m + 1)) + ((Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)) by RLVECT_1:def 3
.= (((Partial_Sums seq) . k) + ((Partial_Sums (seq ^\ (k + 1))) . m)) + ((seq ^\ (k + 1)) . (m + 1)) by FUNCOP_1:7
.= (((Partial_Sums seq) ^\ (k + 1)) . m) + ((seq ^\ (k + 1)) . (m + 1)) by A5, FUNCOP_1:7
.= ((Partial_Sums seq) . (m + (k + 1))) + ((seq ^\ (k + 1)) . (m + 1)) by NAT_1:def 3
.= ((Partial_Sums seq) . (m + (k + 1))) + (seq . ((m + 1) + (k + 1))) by NAT_1:def 3
.= (Partial_Sums seq) . ((m + (k + 1)) + 1) by Def1
.= (Partial_Sums seq) . ((m + 1) + (k + 1))
.= ((Partial_Sums seq) ^\ (k + 1)) . (m + 1) by NAT_1:def 3 ;
hence S₁[m + 1] ; :: thesis: verum

end;

((Partial_Sums seq) ^\ (k + 1)) . 0 = (Partial_Sums seq) . (0 + (k + 1)) by NAT_1:def 3
.= ((Partial_Sums seq) . k) + (seq . (k + 1)) by Def1
.= ((Partial_Sums (seq ^\ (k + 1))) . 0) + (seq1 . 0) by A3, FUNCOP_1:7 ;
then A6: S₁[ 0 ] ;
for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A6, A4);
then A7: (Partial_Sums seq) ^\ (k + 1) = (Partial_Sums (seq ^\ (k + 1))) + seq1 by NORMSP_1:def 2
.= (Partial_Sums ((seq ^\ k) ^\ 1)) + seq1 by BHSP_3:31 ;
seq1 is convergent by BHSP_2:1;
then (Partial_Sums seq) ^\ (k + 1) is convergent by A2, A7, BHSP_2:3;
then Partial_Sums seq is convergent by BHSP_3:37;
hence seq is summable by Def2; :: thesis: verum