let p be Real; :: thesis:
assume A1: 0 < p ; :: thesis:
let a, ap be Real_Sequence; :: thesis:
assume that
A2: a is convergent and
A3: for n being Element of NAT holds 0 <= a . n and
A4: for n being Element of NAT holds ap . n = (a . n) to_power p ; :: thesis:

case ex n being Element of NAT st
for m being Element of NAT st n <= m holds
a . m = 0 ; :: thesis:

then consider N being Element of NAT such that
A6: for m being Element of NAT st N <= m holds
a . m = 0 ;
A7: for n being Element of NAT holds (a ^\ N) . n = 0

proof

let n be Element of NAT ; :: thesis:
a . (n + N) = 0 by A6, NAT_1:12;
hence (a ^\ N) . n = 0 by NAT_1:def 3; :: thesis:

end;

A8: now

let e be real number ; :: thesis:
assume A9: e > 0 ; :: thesis:
take n = 0 ; :: thesis:
let m be Element of NAT ; :: thesis:
assume n <= m ; :: thesis:
A10: (lim a) to_power p = 0 by A1, A5, POWER:def 2;
(ap ^\ N) . m = ap . (m + N) by NAT_1:def 3
.= (a . (m + N)) to_power p by A4
.= ((a ^\ N) . m) to_power p by NAT_1:def 3
.= 0 to_power p by A7
.= 0 by A1, POWER:def 2 ;
hence abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e by A9, A10, ABSVALUE:7; :: thesis:

end;

then A11: ap ^\ N is convergent by SEQ_2:def 6;
then (lim a) to_power p = lim (ap ^\ N) by A8, SEQ_2:def 7;
hence ( ap is convergent & lim ap = (lim a) to_power p ) by A11, SEQ_4:33, SEQ_4:35; :: thesis:

end;

case A12: for n being Element of NAT ex m being Element of NAT st
( n <= m & a . m <> 0 ) ; :: thesis:

defpred S₁[ set ] means a . $1 <> 0 ;
ex m1 being Element of NAT st
( 0 <= m1 & a . m1 <> 0 ) by A12;
then A13: ex m being Nat st S₁[m] ;
consider M being Nat such that
A14: ( S₁[M] & ( for n being Nat st S₁[n] holds
M <= n ) ) from NAT_1:sch 5(A13);
defpred S₂[ set , set , set ] means for n, m being Element of NAT st $2 = n & $3 = m holds
( n < m & a . m <> 0 & ( for k being Element of NAT st n < k & a . k <> 0 holds
m <= k ) );
A15: (lim a) to_power p = 0 by A1, A5, POWER:def 2;
reconsider M = M as Element of NAT by ORDINAL1:def 13;

A16: now

let n be Element of NAT ; :: thesis:
consider m being Element of NAT such that
A17: ( n + 1 <= m & a . m <> 0 ) by A12;
take m = m; :: thesis:
thus ( n < m & a . m <> 0 ) by A17, NAT_1:13; :: thesis:

end;

A18: for n, x being Element of NAT ex y being Element of NAT st S₂[n,x,y]

proof

let n, x be Element of NAT ; :: thesis:
defpred S₃[ Nat] means ( x < $1 & a . $1 <> 0 );
ex m being Element of NAT st S₃[m] by A16;
then A19: ex m being Nat st S₃[m] ;
consider l being Nat such that
A20: ( S₃[l] & ( for k being Nat st S₃[k] holds
l <= k ) ) from NAT_1:sch 5(A19);
take l ; :: thesis:
l in NAT by ORDINAL1:def 13;
hence ( l is Element of REAL & l is Element of NAT & S₂[n,x,l] ) by A20; :: thesis:

end;

consider F being Function of NAT ,NAT such that
A21: ( F . 0 = M & ( for n being Element of NAT holds S₂[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A18);
A22: rng F c= NAT by RELAT_1:def 19;
then A23: rng F c= REAL by XBOOLE_1:1;
A24: dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A23, RELSET_1:11;

A25: now

let n be Element of NAT ; :: thesis:
F . n in rng F by A24, FUNCT_1:def 5;
hence F . n is Element of NAT by A22; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
( F . n is Element of NAT & F . (n + 1) is Element of NAT ) by A25;
hence F . n < F . (n + 1) by A21; :: thesis:

end;

then reconsider F = F as V35() sequence of NAT by SEQM_3:def 11;
A26: for n being Element of NAT st a . n <> 0 holds
ex m being Element of NAT st F . m = n

proof

defpred S₃[ set ] means ( a . $1 <> 0 & ( for m being Element of NAT holds F . m <> $1 ) );
assume ex n being Element of NAT st S₃[n] ; :: thesis:
then A27: ex n being Nat st S₃[n] ;
consider M1 being Nat such that
A28: ( S₃[M1] & ( for n being Nat st S₃[n] holds
M1 <= n ) ) from NAT_1:sch 5(A27);
defpred S₄[ Nat] means ( $1 < M1 & a . $1 <> 0 & ex m being Element of NAT st F . m = $1 );
A29: ex n being Nat st S₄[n]

proof

take M ; :: thesis:
( M <= M1 & M <> M1 ) by A14, A21, A28;
hence M < M1 by XXREAL_0:1; :: thesis:
thus a . M <> 0 by A14; :: thesis:
take 0 ; :: thesis:
thus F . 0 = M by A21; :: thesis:

end;

A30: for n being Nat st S₄[n] holds
n <= M1 ;
consider MX being Nat such that
A31: ( S₄[MX] & ( for n being Nat st S₄[n] holds
n <= MX ) ) from NAT_1:sch 6(A30, A29);
A32: for k being Element of NAT st MX < k & k < M1 holds
a . k = 0

proof

given k being Element of NAT such that A33: MX < k and
A34: ( k < M1 & a . k <> 0 ) ; :: thesis:

now

per cases ;

case ex m being Element of NAT st F . m = k ; :: thesis:

hence contradiction by A31, A33, A34; :: thesis:

end;

case for m being Element of NAT holds F . m <> k ; :: thesis:

hence contradiction by A28, A34; :: thesis:

end;

hence contradiction ; :: thesis:

end;

consider m being Element of NAT such that
A35: F . m = MX by A31;
A36: ( MX < F . (m + 1) & a . (F . (m + 1)) <> 0 ) by A21, A35;
M1 in NAT by ORDINAL1:def 13;
then A37: F . (m + 1) <= M1 by A21, A28, A31, A35;

now

assume F . (m + 1) <> M1 ; :: thesis:
then F . (m + 1) < M1 by A37, XXREAL_0:1;
hence contradiction by A32, A36; :: thesis:

end;

hence contradiction by A28; :: thesis:

end;

A38: ( a * F is convergent & lim (a * F) = 0 ) by A2, A5, SEQ_4:29, SEQ_4:30;

A39: now

let e be real number ; :: thesis:
assume A40: 0 < e ; :: thesis:
then 0 < e to_power (1 / p) by POWER:39;
then consider n being Element of NAT such that
A41: for m being Element of NAT st n <= m holds
abs (((a * F) . m) - 0 ) < e to_power (1 / p) by A38, SEQ_2:def 7;
take k = F . n; :: thesis:
let m be Element of NAT ; :: thesis:
assume A42: k <= m ; :: thesis:

now

per cases ;

case a . m = 0 ; :: thesis:

then ap . m = 0 to_power p by A4
.= 0 by A1, POWER:def 2 ;
hence abs ((ap . m) - ((lim a) to_power p)) < e by A15, A40, ABSVALUE:7; :: thesis:

end;

case A43: a . m <> 0 ; :: thesis:

then consider l being Element of NAT such that
A44: m = F . l by A26;
n <= l by A42, A44, SEQM_3:7;
then abs (((a * F) . l) - 0 ) < e to_power (1 / p) by A41;
then A45: abs (a . (F . l)) < e to_power (1 / p) by FUNCT_2:21;
A46: (a . m) to_power p = ap . m by A4;
A47: a . m > 0 by A3, A43;
then A48: 0 < ap . m by A46, POWER:39;
abs (a . m) > 0 by A43, COMPLEX1:133;
then (abs (a . m)) to_power p < (e to_power (1 / p)) to_power p by A1, A44, A45, POWER:42;
then (abs (a . m)) to_power p < e to_power ((1 / p) * p) by A40, POWER:38;
then (abs (a . m)) to_power p < e to_power 1 by A1, XCMPLX_1:107;
then (abs (a . m)) to_power p < e by POWER:30;
then ap . m < e by A47, A46, ABSVALUE:def 1;
hence abs ((ap . m) - ((lim a) to_power p)) < e by A15, A48, ABSVALUE:def 1; :: thesis:

end;

hence abs ((ap . m) - ((lim a) to_power p)) < e ; :: thesis:

end;

hence ap is convergent by SEQ_2:def 6; :: thesis:
hence lim ap = (lim a) to_power p by A39, SEQ_2:def 7; :: thesis:

end;

hence ( ap is convergent & lim ap = (lim a) to_power p ) ; :: thesis:

end;

case A49: lim a <> 0 ; :: thesis:

A50: 0 <= lim a by A2, A3, SEQ_2:31;
ex k being Element of NAT st rng (a ^\ k) c= dom (#R p)

proof

set e0 = lim a;
A51: (lim a) / 2 > 0 by A49, A50, XREAL_1:217;
then consider k being Element of NAT such that
A52: for m being Element of NAT st k <= m holds
abs ((a . m) - (lim a)) < (lim a) / 2 by A2, SEQ_2:def 7;
take k ; :: thesis:

A53: now

let m be Element of NAT ; :: thesis:
abs ((a . (k + m)) - (lim a)) < (lim a) / 2 by A52, NAT_1:12;
then - ((lim a) / 2) <= (a . (k + m)) - (lim a) by ABSVALUE:12;
then (- ((lim a) / 2)) + (lim a) <= ((a . (k + m)) - (lim a)) + (lim a) by XREAL_1:9;
hence 0 < (a ^\ k) . m by A51, NAT_1:def 3; :: thesis:

end;

now

let x be set ; :: thesis:
assume x in rng (a ^\ k) ; :: thesis:
then consider n being Element of NAT such that
A54: x = (a ^\ k) . n by FUNCT_2:190;
0 < (a ^\ k) . n by A53;
then (a ^\ k) . n in { g where g is Real : 0 < g } ;
then (a ^\ k) . n in right_open_halfline 0 by XXREAL_1:230;
hence x in dom (#R p) by A54, TAYLOR_1:def 4; :: thesis:

end;

hence rng (a ^\ k) c= dom (#R p) by TARSKI:def 3; :: thesis:

end;

then consider k being Element of NAT such that
A55: rng (a ^\ k) c= dom (#R p) ;

now

let x be set ; :: thesis:
assume x in NAT ; :: thesis:
then reconsider n = x as Element of NAT ;
(a ^\ k) . n in rng (a ^\ k) by VALUED_0:28;
then (a ^\ k) . n in dom (#R p) by A55;
then A56: (a ^\ k) . n in right_open_halfline 0 by TAYLOR_1:def 4;
then a . (k + n) in right_open_halfline 0 by NAT_1:def 3;
then a . (k + n) in { g where g is Real : 0 < g } by XXREAL_1:230;
then A57: ex g being Real st
( a . (k + n) = g & g > 0 ) ;
thus ((#R p) /* (a ^\ k)) . x = (#R p) . ((a ^\ k) . n) by A55, FUNCT_2:185
.= ((a ^\ k) . n) #R p by A56, TAYLOR_1:def 4
.= (a . (k + n)) #R p by NAT_1:def 3
.= (a . (k + n)) to_power p by A57, POWER:def 2
.= ap . (k + n) by A4
.= (ap ^\ k) . x by NAT_1:def 3 ; :: thesis:

end;

then A58: (#R p) /* (a ^\ k) = ap ^\ k by FUNCT_2:18;
A59: lim (a ^\ k) = lim a by A2, SEQ_4:33;
lim a > 0 by A2, A3, A49, SEQ_2:31;
then #R p is_continuous_in lim (a ^\ k) by A59, FDIFF_1:32, TAYLOR_1:21;
then A60: ( (#R p) /* (a ^\ k) is convergent & (#R p) . (lim (a ^\ k)) = lim ((#R p) /* (a ^\ k)) ) by A2, A55, FCONT_1:def 1;
lim a in { g where g is Real : 0 < g } by A49, A50;
then lim a in right_open_halfline 0 by XXREAL_1:230;
then (#R p) . (lim (a ^\ k)) = (lim a) #R p by A59, TAYLOR_1:def 4
.= (lim a) to_power p by A49, A50, POWER:def 2 ;
hence ( ap is convergent & lim ap = (lim a) to_power p ) by A60, A58, SEQ_4:35, SEQ_4:36; :: thesis:

end;

hence ( ap is convergent & lim ap = (lim a) to_power p ) ; :: thesis: