let s be Real_Sequence; :: thesis: ( ex n being Element of NAT st s ^\ n is summable implies s is summable )
given n being Element of NAT such that A1: s ^\ n is summable ; :: thesis: s is summable
(s ^\ n) ^\ 1 is summable by A1, Th15;
then A2: Partial_Sums ((s ^\ n) ^\ 1) is convergent by Def2;
reconsider s1 = NAT --> ((Partial_Sums s) . n) as Real_Sequence ;
for k being Element of NAT holds ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k)

proof

A4: (Partial_Sums (s ^\ (n + 1))) . 0 = (s ^\ (n + 1)) . 0 by Def1
.= s . (0 + (n + 1)) by NAT_1:def 3
.= s . (n + 1) ;
defpred S₁[ Element of NAT ] means ((Partial_Sums s) ^\ (n + 1)) . $1 = ((Partial_Sums (s ^\ (n + 1))) . $1) + (s1 . $1);
((Partial_Sums s) ^\ (n + 1)) . 0 = (Partial_Sums s) . (0 + (n + 1)) by NAT_1:def 3
.= (s . (n + 1)) + ((Partial_Sums s) . n) by Def1
.= ((Partial_Sums (s ^\ (n + 1))) . 0 ) + (s1 . 0 ) by A4, FUNCOP_1:13 ;
then A5: S₁[ 0 ] ;
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: ((Partial_Sums s) ^\ (n + 1)) . k = ((Partial_Sums (s ^\ (n + 1))) . k) + (s1 . k) ; :: thesis: S₁[k + 1]
((Partial_Sums (s ^\ (n + 1))) . (k + 1)) + (s1 . (k + 1)) = (s1 . (k + 1)) + (((Partial_Sums (s ^\ (n + 1))) . k) + ((s ^\ (n + 1)) . (k + 1))) by Def1
.= ((s1 . (k + 1)) + ((Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1))
.= (((Partial_Sums s) . n) + ((Partial_Sums (s ^\ (n + 1))) . k)) + ((s ^\ (n + 1)) . (k + 1)) by FUNCOP_1:13
.= (((Partial_Sums s) ^\ (n + 1)) . k) + ((s ^\ (n + 1)) . (k + 1)) by A7, FUNCOP_1:13
.= ((Partial_Sums s) . (k + (n + 1))) + ((s ^\ (n + 1)) . (k + 1)) by NAT_1:def 3
.= ((Partial_Sums s) . (k + (n + 1))) + (s . ((k + 1) + (n + 1))) by NAT_1:def 3
.= (Partial_Sums s) . ((k + (n + 1)) + 1) by Def1
.= (Partial_Sums s) . ((k + 1) + (n + 1))
.= ((Partial_Sums s) ^\ (n + 1)) . (k + 1) by NAT_1:def 3 ;
hence S₁[k + 1] ; :: thesis: verum

end;

thus for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A6); :: thesis: verum

end;

then (Partial_Sums s) ^\ (n + 1) = (Partial_Sums (s ^\ (n + 1))) + s1 by SEQ_1:11
.= (Partial_Sums ((s ^\ n) ^\ 1)) + s1 by NAT_1:49 ;
then (Partial_Sums s) ^\ (n + 1) is convergent by A2, SEQ_2:19;
then Partial_Sums s is convergent by SEQ_4:35;
hence s is summable by Def2; :: thesis: verum