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 Nat holds 0 <= a . n and
A4: for n being Nat holds ap . n = (a . n) to_power p ; :: thesis:

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

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

let n be 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 :: thesis:

let e be Real; :: thesis:
assume A9: e > 0 ; :: thesis:
reconsider n = 0 as Nat ;
take n = n; :: thesis:
let m be 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 |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e by A9, A10, ABSVALUE:2; :: 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:20, SEQ_4:21; :: thesis:

end;

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

defpred S₁[ set ] means a . $1 <> 0 ;
ex m1 being 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 Nat st $2 = n & $3 = m holds
( n < m & a . m <> 0 & ( for k being 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 Nat ;

A16: now :: thesis:

let n be Nat; :: thesis:
consider m being 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 being Nat
for x being Element of NAT ex y being Element of NAT st S₂[n,x,y]

proof

let n be Nat; :: thesis:
let x be Element of NAT ; :: thesis:
defpred S₃[ Nat] means ( x < $1 & a . $1 <> 0 );
ex m being 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 12;
hence ( l is Element of NAT & S₂[n,x,l] ) by A20; :: thesis:

end;

reconsider zz = 0 as Element of NAT ;
consider F being sequence of NAT such that
A21: ( F . 0 = In (M,NAT) & ( for n being Nat holds S₂[n,F . n,F . (n + 1)] ) ) from RECDEF_1:sch 2(A18);
rng F c= NAT by RELAT_1:def 19;
then A22: rng F c= REAL by NUMBERS:19;
dom F = NAT by FUNCT_2:def 1;
then reconsider F = F as Real_Sequence by A22, RELSET_1:4;
for n being Nat holds F . n < F . (n + 1) by A21;
then reconsider F = F as increasing sequence of NAT by SEQM_3:def 6;
A23: for n being Nat st a . n <> 0 holds
ex m being Nat st F . m = n

proof

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

proof

take M ; :: thesis:
( M <= M1 & M <> M1 ) by A14, A21, A25;
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;

A27: for n being Nat st S₄[n] holds
n <= M1 ;
consider MX being Nat such that
A28: ( S₄[MX] & ( for n being Nat st S₄[n] holds
n <= MX ) ) from NAT_1:sch 6(A27, A26);
A29: for k being Nat st MX < k & k < M1 holds
a . k = 0

proof

given k being Nat such that A30: MX < k and
A31: ( k < M1 & a . k <> 0 ) ; :: thesis:

now :: thesis:

per cases ;

case ex m being Nat st F . m = k ; :: thesis:

hence contradiction by A28, A30, A31; :: thesis:

end;

case for m being Nat holds F . m <> k ; :: thesis:

hence contradiction by A25, A31; :: thesis:

end;

hence contradiction ; :: thesis:

end;

consider m being Nat such that
A32: F . m = MX by A28;
A33: ( MX < F . (m + 1) & a . (F . (m + 1)) <> 0 ) by A21, A32;
A34: F . (m + 1) <= M1 by A21, A25, A28, A32;

now :: thesis:

assume F . (m + 1) <> M1 ; :: thesis:
then F . (m + 1) < M1 by A34, XXREAL_0:1;
hence contradiction by A29, A33; :: thesis:

end;

hence contradiction by A25; :: thesis:

end;

A35: ( a * F is convergent & lim (a * F) = 0 ) by A2, A5, SEQ_4:16, SEQ_4:17;

A36: now :: thesis:

let e be Real; :: thesis:
assume A37: 0 < e ; :: thesis:
then 0 < e to_power (1 / p) by POWER:34;
then consider n being Nat such that
A38: for m being Nat st n <= m holds
|.(((a * F) . m) - 0).| < e to_power (1 / p) by A35, SEQ_2:def 7;
reconsider k = F . n as Nat ;
take k = k; :: thesis:
let m be Nat; :: thesis:
assume A39: k <= m ; :: thesis:

now :: thesis:

per cases ;

case a . m = 0 ; :: thesis:

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

end;

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

then consider l being Nat such that
A41: m = F . l by A23;
A42: l in NAT by ORDINAL1:def 12;
n <= l by A39, A41, SEQM_3:1;
then |.(((a * F) . l) - 0).| < e to_power (1 / p) by A38;
then A43: |.(a . (F . l)).| < e to_power (1 / p) by FUNCT_2:15, A42;
A44: (a . m) to_power p = ap . m by A4;
A45: a . m > 0 by A3, A40;
then A46: 0 < ap . m by A44, POWER:34;
|.(a . m).| > 0 by A40, COMPLEX1:47;
then |.(a . m).| to_power p < (e to_power (1 / p)) to_power p by A1, A41, A43, POWER:37;
then |.(a . m).| to_power p < e to_power ((1 / p) * p) by A37, POWER:33;
then |.(a . m).| to_power p < e to_power 1 by A1, XCMPLX_1:106;
then |.(a . m).| to_power p < e by POWER:25;
then ap . m < e by A45, A44, ABSVALUE:def 1;
hence |.((ap . m) - ((lim a) to_power p)).| < e by A15, A46, ABSVALUE:def 1; :: thesis:

end;

hence |.((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 A36, SEQ_2:def 7; :: thesis:

end;

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

end;

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

A48: 0 <= lim a by A2, A3, SEQ_2:17;
ex k being Nat st rng (a ^\ k) c= dom (#R p)

proof

set e0 = lim a;
A49: (lim a) / 2 > 0 by A47, A48, XREAL_1:215;
then consider k being Nat such that
A50: for m being Nat st k <= m holds
|.((a . m) - (lim a)).| < (lim a) / 2 by A2, SEQ_2:def 7;
take k ; :: thesis:

A51: now :: thesis:

let m be Nat; :: thesis:
|.((a . (k + m)) - (lim a)).| < (lim a) / 2 by A50, NAT_1:12;
then - ((lim a) / 2) <= (a . (k + m)) - (lim a) by ABSVALUE:5;
then (- ((lim a) / 2)) + (lim a) <= ((a . (k + m)) - (lim a)) + (lim a) by XREAL_1:7;
hence 0 < (a ^\ k) . m by A49, NAT_1:def 3; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in rng (a ^\ k) ; :: thesis:
then consider n being Element of NAT such that
A52: x = (a ^\ k) . n by FUNCT_2:113;
0 < (a ^\ k) . n by A51;
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 A52, TAYLOR_1:def 4; :: thesis:

end;

then consider k being Nat such that
A53: rng (a ^\ k) c= dom (#R p) ;

now :: thesis:

let x be object ; :: 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 A53;
then A54: (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 A55: ex g being Real st
( a . (k + n) = g & g > 0 ) ;
thus ((#R p) /* (a ^\ k)) . x = (#R p) . ((a ^\ k) . n) by A53, FUNCT_2:108
.= ((a ^\ k) . n) #R p by A54, TAYLOR_1:def 4
.= (a . (k + n)) #R p by NAT_1:def 3
.= (a . (k + n)) to_power p by A55, POWER:def 2
.= ap . (k + n) by A4
.= (ap ^\ k) . x by NAT_1:def 3 ; :: thesis:

end;

then A56: (#R p) /* (a ^\ k) = ap ^\ k by FUNCT_2:12;
A57: lim (a ^\ k) = lim a by A2, SEQ_4:20;
lim a > 0 by A2, A3, A47, SEQ_2:17;
then #R p is_continuous_in lim (a ^\ k) by A57, FDIFF_1:24, TAYLOR_1:21;
then A58: ( (#R p) /* (a ^\ k) is convergent & (#R p) . (lim (a ^\ k)) = lim ((#R p) /* (a ^\ k)) ) by A2, A53, FCONT_1:def 1;
lim a in { g where g is Real : 0 < g } by A47, A48;
then lim a in right_open_halfline 0 by XXREAL_1:230;
then (#R p) . (lim (a ^\ k)) = (lim a) #R p by A57, TAYLOR_1:def 4
.= (lim a) to_power p by A47, A48, POWER:def 2 ;
hence ( ap is convergent & lim ap = (lim a) to_power p ) by A58, A56, SEQ_4:21, SEQ_4:22; :: thesis:

end;

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