let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X st ex k being Nat st seq ^\ k is summable holds
seq is summable
let seq be sequence of X; :: thesis: ( ex k being Nat st seq ^\ k is summable implies seq is summable )
given k being 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 ;
reconsider seq1 = NAT --> ((Partial_Sums seq) . k) as sequence of X ;
defpred S₁[ 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 BHSP_4:def 1
.= seq . (0 + (k + 1)) by NAT_1:def 3
.= seq . (k + 1) ;

A4: now :: thesis: for m being Nat st S₁[m] holds
S₁[m + 1]

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
A5: m in NAT by ORDINAL1:def 12;
assume A6: 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 BHSP_4:def 1
.= ((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))
.= (((Partial_Sums seq) ^\ (k + 1)) . m) + ((seq ^\ (k + 1)) . (m + 1)) by A6, FUNCOP_1:7, A5
.= ((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 BHSP_4:def 1
.= (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 BHSP_4:def 1
.= ((Partial_Sums (seq ^\ (k + 1))) . 0) + (seq1 . 0) by A3 ;
then A7: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A7, A4);
then A8: (Partial_Sums seq) ^\ (k + 1) = (Partial_Sums (seq ^\ (k + 1))) + seq1 by NORMSP_1:def 2
.= (Partial_Sums ((seq ^\ k) ^\ 1)) + seq1 by NAT_1:48 ;
seq1 is convergent by CLVECT_2:1;
then (Partial_Sums seq) ^\ (k + 1) is convergent by A2, A8, CLVECT_2:3;
then Partial_Sums seq is convergent by CLVECT_2:91;
hence seq is summable ; :: thesis: verum