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:

now

per cases ;

case A5: lim a = 0 ; :: thesis:

now

per cases ;

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: (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 ;
(lim a) to_power p = 0 by A1, A5, POWER:def 2;
hence abs (((ap ^\ N) . m) - ((lim a) to_power p)) < e by A9, A10, ABSVALUE:7; :: thesis:

end;

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

end;

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

then consider m1 being Element of NAT such that
A12: ( 0 <= m1 & a . m1 <> 0 ) ;
defpred S₁[ set ] means a . $1 <> 0 ;
A13: ex m being Nat st S₁[m] by A12;
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);
reconsider M = M as Element of NAT by ORDINAL1:def 13;

A15: now

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

end;

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 ) );
A17: 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 A15;
then A18: ex m being Nat st S₃[m] ;
consider l being Nat such that
A19: ( S₃[l] & ( for k being Nat st S₃[k] holds
l <= k ) ) from NAT_1:sch 5(A18);
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 A19; :: thesis:

end;

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

A22: now

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

end;

now

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

end;

then reconsider F = F as V34() sequence of NAT by SEQM_3:def 11;
A23: 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 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 Element of NAT st F . m = $1 );
A26: ex n being Nat st S₄[n]

proof

take M ; :: thesis:
A27: M <= M1 by A14, A25;
M <> M1 by A20, A25;
hence M < M1 by A27, XXREAL_0:1; :: thesis:
thus a . M <> 0 by A14; :: thesis:
take 0 ; :: thesis:
thus F . 0 = M by A20; :: thesis:

end;

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

proof

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

now

per cases ;

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

hence contradiction by A29, A31; :: thesis:

end;

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

hence contradiction by A25, A31; :: thesis:

end;

hence contradiction ; :: thesis:

end;

consider m being Element of NAT such that
A32: F . m = MX by A29;
A33: ( MX < F . (m + 1) & a . (F . (m + 1)) <> 0 & ( for k being Element of NAT st MX < k & a . k <> 0 holds
F . (m + 1) <= k ) ) by A20, A32;
M1 in NAT by ORDINAL1:def 13;
then A34: F . (m + 1) <= M1 by A20, A25, A29, A32;

now

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

end;

hence contradiction by A25; :: thesis:

end;

A36: a * F is convergent by A2, SEQ_4:29;
A37: lim (a * F) = 0 by A2, A5, SEQ_4:30;
A38: (lim a) to_power p = 0 by A1, A5, POWER:def 2;

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 A36, A37, 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 A38, A40, ABSVALUE:7; :: thesis:

end;

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

then A44: a . m > 0 by A3;
consider l being Element of NAT such that
A45: m = F . l by A23, A43;
n <= l by A42, A45, SEQM_3:7;
then abs (((a * F) . l) - 0 ) < e to_power (1 / p) by A41;
then A46: abs (a . (F . l)) < e to_power (1 / p) by FUNCT_2:21;
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, A45, A46, 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 A47: (abs (a . m)) to_power p < e by POWER:30;
A48: (a . m) to_power p = ap . m by A4;
then A49: 0 < ap . m by A44, POWER:39;
ap . m < e by A44, A47, A48, ABSVALUE:def 1;
hence abs ((ap . m) - ((lim a) to_power p)) < e by A38, A49, 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 A50: lim a <> 0 ; :: thesis:

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

proof

set e0 = lim a;
A53: (lim a) / 2 > 0 by A50, A51, XREAL_1:217;
then consider k being Element of NAT such that
A54: 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:

A55: now

let m be Element of NAT ; :: thesis:
abs ((a . (k + m)) - (lim a)) < (lim a) / 2 by A54, 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 A53, NAT_1:def 3; :: thesis:

end;

now

let x be set ; :: thesis:
assume A56: x in rng (a ^\ k) ; :: thesis:
consider n being Element of NAT such that
A57: x = (a ^\ k) . n by A56, FUNCT_2:190;
0 < (a ^\ k) . n by A55;
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 A57, 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
A58: rng (a ^\ k) c= dom (#R p) ;
A59: ( a ^\ k is convergent & lim (a ^\ k) = lim a ) by A2, SEQ_4:33;
then #R p is_differentiable_in lim (a ^\ k) by A52, TAYLOR_1:21;
then #R p is_continuous_in lim (a ^\ k) by FDIFF_1:32;
then A60: ( (#R p) /* (a ^\ k) is convergent & (#R p) . (lim (a ^\ k)) = lim ((#R p) /* (a ^\ k)) ) by A58, A59, FCONT_1:def 1;
A61: (#R p) /* (a ^\ k) = ap ^\ k

proof

now

let x be set ; :: thesis:
assume A62: x in NAT ; :: thesis:
reconsider n = x as Element of NAT by A62;
(a ^\ k) . n in rng (a ^\ k) by VALUED_0:28;
then (a ^\ k) . n in dom (#R p) by A58;
then A63: (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 consider g being Real such that
A64: ( a . (k + n) = g & g > 0 ) ;
thus ((#R p) /* (a ^\ k)) . x = (#R p) . ((a ^\ k) . n) by A58, FUNCT_2:185
.= ((a ^\ k) . n) #R p by A63, TAYLOR_1:def 4
.= (a . (k + n)) #R p by NAT_1:def 3
.= (a . (k + n)) to_power p by A64, POWER:def 2
.= ap . (k + n) by A4
.= (ap ^\ k) . x by NAT_1:def 3 ; :: thesis:

end;

hence (#R p) /* (a ^\ k) = ap ^\ k by FUNCT_2:18; :: thesis:

end;

lim a in right_open_halfline 0

proof

lim a in { g where g is Real : 0 < g } by A50, A51;
hence lim a in right_open_halfline 0 by XXREAL_1:230; :: thesis:

end;

then (#R p) . (lim (a ^\ k)) = (lim a) #R p by A59, TAYLOR_1:def 4
.= (lim a) to_power p by A50, A51, POWER:def 2 ;
hence ( ap is convergent & lim ap = (lim a) to_power p ) by A60, A61, SEQ_4:35, SEQ_4:36; :: thesis:

end;

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