let p be Real; :: thesis: ( 0 < p implies for a, ap being Real_Sequence st a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) holds

( ap is convergent & lim ap = (lim a) to_power p ) )

assume A1: 0 < p ; :: thesis: for a, ap being Real_Sequence st a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) holds

( ap is convergent & lim ap = (lim a) to_power p )

let a, ap be Real_Sequence; :: thesis: ( a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) implies ( ap is convergent & lim ap = (lim a) to_power p ) )

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: ( ap is convergent & lim ap = (lim a) to_power p )

( ap is convergent & lim ap = (lim a) to_power p ) )

assume A1: 0 < p ; :: thesis: for a, ap being Real_Sequence st a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) holds

( ap is convergent & lim ap = (lim a) to_power p )

let a, ap be Real_Sequence; :: thesis: ( a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) implies ( ap is convergent & lim ap = (lim a) to_power p ) )

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: ( ap is convergent & lim ap = (lim a) to_power p )

now :: thesis: ( ( lim a = 0 & ap is convergent & lim ap = (lim a) to_power p ) or ( lim a <> 0 & ap is convergent & lim ap = (lim a) to_power p ) )end;

hence
( ap is convergent & lim ap = (lim a) to_power p )
; :: thesis: verumper cases
( lim a = 0 or lim a <> 0 )
;

end;

case A5:
lim a = 0
; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )

end;

now :: thesis: ( ( ex n being Nat st

for m being Nat st n <= m holds

a . m = 0 & ap is convergent & lim ap = (lim a) to_power p ) or ( ( for n being Nat ex m being Nat st

( n <= m & a . m <> 0 ) ) & ap is convergent & lim ap = (lim a) to_power p ) )end;

hence
( ap is convergent & lim ap = (lim a) to_power p )
; :: thesis: verumfor m being Nat st n <= m holds

a . m = 0 & ap is convergent & lim ap = (lim a) to_power p ) or ( ( for n being Nat ex m being Nat st

( n <= m & a . m <> 0 ) ) & ap is convergent & lim ap = (lim a) to_power p ) )

per cases
( ex n being Nat st

for m being Nat st n <= m holds

a . m = 0 or for n being Nat ex m being Nat st

( n <= m & a . m <> 0 ) ) ;

end;

for m being Nat st n <= m holds

a . m = 0 or for n being Nat ex m being Nat st

( n <= m & a . m <> 0 ) ) ;

case
ex n being Nat st

for m being Nat st n <= m holds

a . m = 0 ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )

for m being Nat st n <= m holds

a . m = 0 ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )

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

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: verum

end;A6: for m being Nat st N <= m holds

a . m = 0 ;

A7: for n being Nat holds (a ^\ N) . n = 0

proof

let n be Nat; :: thesis: (a ^\ N) . n = 0

a . (n + N) = 0 by A6, NAT_1:12;

hence (a ^\ N) . n = 0 by NAT_1:def 3; :: thesis: verum

end;a . (n + N) = 0 by A6, NAT_1:12;

hence (a ^\ N) . n = 0 by NAT_1:def 3; :: thesis: verum

A8: now :: thesis: for e being Real st e > 0 holds

ex n being Nat st

for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

then A11:
ap ^\ N is convergent
by SEQ_2:def 6;ex n being Nat st

for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

let e be Real; :: thesis: ( e > 0 implies ex n being Nat st

for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e )

assume A9: e > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

let m be Nat; :: thesis: ( n <= m implies |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e )

assume n <= m ; :: thesis: |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

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: verum

end;for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e )

assume A9: e > 0 ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

reconsider n = 0 as Nat ;

take n = n; :: thesis: for m being Nat st n <= m holds

|.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

let m be Nat; :: thesis: ( n <= m implies |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e )

assume n <= m ; :: thesis: |.(((ap ^\ N) . m) - ((lim a) to_power p)).| < e

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: verum

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: verum

case A12:
for n being Nat ex m being Nat st

( n <= m & a . m <> 0 ) ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )

( n <= m & a . m <> 0 ) ; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )

defpred S_{1}[ 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_{1}[m]
;

consider M being Nat such that

A14: ( S_{1}[M] & ( for n being Nat st S_{1}[n] holds

M <= n ) ) from NAT_1:sch 5(A13);

defpred S_{2}[ 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 ;

for x being Element of NAT ex y being Element of NAT st S_{2}[n,x,y]

consider F being sequence of NAT such that

A21: ( F . 0 = In (M,NAT) & ( for n being Nat holds S_{2}[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 V46() 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

hence lim ap = (lim a) to_power p by A36, SEQ_2:def 7; :: thesis: verum

end;ex m1 being Nat st

( 0 <= m1 & a . m1 <> 0 ) by A12;

then A13: ex m being Nat st S

consider M being Nat such that

A14: ( S

M <= n ) ) from NAT_1:sch 5(A13);

defpred S

( 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: for n being Nat ex m being Nat st

( n < m & a . m <> 0 )

A18:
for n being Nat( n < m & a . m <> 0 )

let n be Nat; :: thesis: ex m being Nat st

( n < m & a . m <> 0 )

consider m being Nat such that

A17: ( n + 1 <= m & a . m <> 0 ) by A12;

take m = m; :: thesis: ( n < m & a . m <> 0 )

thus ( n < m & a . m <> 0 ) by A17, NAT_1:13; :: thesis: verum

end;( n < m & a . m <> 0 )

consider m being Nat such that

A17: ( n + 1 <= m & a . m <> 0 ) by A12;

take m = m; :: thesis: ( n < m & a . m <> 0 )

thus ( n < m & a . m <> 0 ) by A17, NAT_1:13; :: thesis: verum

for x being Element of NAT ex y being Element of NAT st S

proof

reconsider zz = 0 as Element of NAT ;
let n be Nat; :: thesis: for x being Element of NAT ex y being Element of NAT st S_{2}[n,x,y]

let x be Element of NAT ; :: thesis: ex y being Element of NAT st S_{2}[n,x,y]

defpred S_{3}[ Nat] means ( x < $1 & a . $1 <> 0 );

ex m being Nat st S_{3}[m]
by A16;

then A19: ex m being Nat st S_{3}[m]
;

consider l being Nat such that

A20: ( S_{3}[l] & ( for k being Nat st S_{3}[k] holds

l <= k ) ) from NAT_1:sch 5(A19);

take l ; :: thesis: ( l is Element of NAT & S_{2}[n,x,l] )

l in NAT by ORDINAL1:def 12;

hence ( l is Element of NAT & S_{2}[n,x,l] )
by A20; :: thesis: verum

end;let x be Element of NAT ; :: thesis: ex y being Element of NAT st S

defpred S

ex m being Nat st S

then A19: ex m being Nat st S

consider l being Nat such that

A20: ( S

l <= k ) ) from NAT_1:sch 5(A19);

take l ; :: thesis: ( l is Element of NAT & S

l in NAT by ORDINAL1:def 12;

hence ( l is Element of NAT & S

consider F being sequence of NAT such that

A21: ( F . 0 = In (M,NAT) & ( for n being Nat holds S

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 V46() 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

A35:
( a * F is convergent & lim (a * F) = 0 )
by A2, A5, SEQ_4:16, SEQ_4:17;
defpred S_{3}[ set ] means ( a . $1 <> 0 & ( for m being Nat holds F . m <> $1 ) );

assume ex n being Nat st S_{3}[n]
; :: thesis: contradiction

then A24: ex n being Nat st S_{3}[n]
;

consider M1 being Nat such that

A25: ( S_{3}[M1] & ( for n being Nat st S_{3}[n] holds

M1 <= n ) ) from NAT_1:sch 5(A24);

defpred S_{4}[ Nat] means ( $1 < M1 & a . $1 <> 0 & ex m being Nat st F . m = $1 );

A26: ex n being Nat st S_{4}[n]
_{4}[n] holds

n <= M1 ;

consider MX being Nat such that

A28: ( S_{4}[MX] & ( for n being Nat st S_{4}[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

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;

end;assume ex n being Nat st S

then A24: ex n being Nat st S

consider M1 being Nat such that

A25: ( S

M1 <= n ) ) from NAT_1:sch 5(A24);

defpred S

A26: ex n being Nat st S

proof

A27:
for n being Nat st S
take
M
; :: thesis: S_{4}[M]

( M <= M1 & M <> M1 ) by A14, A21, A25;

hence M < M1 by XXREAL_0:1; :: thesis: ( a . M <> 0 & ex m being Nat st F . m = M )

thus a . M <> 0 by A14; :: thesis: ex m being Nat st F . m = M

take 0 ; :: thesis: F . 0 = M

thus F . 0 = M by A21; :: thesis: verum

end;( M <= M1 & M <> M1 ) by A14, A21, A25;

hence M < M1 by XXREAL_0:1; :: thesis: ( a . M <> 0 & ex m being Nat st F . m = M )

thus a . M <> 0 by A14; :: thesis: ex m being Nat st F . m = M

take 0 ; :: thesis: F . 0 = M

thus F . 0 = M by A21; :: thesis: verum

n <= M1 ;

consider MX being Nat such that

A28: ( S

n <= MX ) ) from NAT_1:sch 6(A27, A26);

A29: for k being Nat st MX < k & k < M1 holds

a . k = 0

proof

consider m being Nat such that
given k being Nat such that A30:
MX < k
and

A31: ( k < M1 & a . k <> 0 ) ; :: thesis: contradiction

end;A31: ( k < M1 & a . k <> 0 ) ; :: thesis: contradiction

now :: thesis: ( ( ex m being Nat st F . m = k & contradiction ) or ( ( for m being Nat holds F . m <> k ) & contradiction ) )end;

hence
contradiction
; :: thesis: verumper cases
( ex m being Nat st F . m = k or for m being Nat holds F . m <> k )
;

end;

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: not F . (m + 1) <> M1

hence
contradiction
by A25; :: thesis: verumassume
F . (m + 1) <> M1
; :: thesis: contradiction

then F . (m + 1) < M1 by A34, XXREAL_0:1;

hence contradiction by A29, A33; :: thesis: verum

end;then F . (m + 1) < M1 by A34, XXREAL_0:1;

hence contradiction by A29, A33; :: thesis: verum

A36: now :: thesis: for e being Real st 0 < e holds

ex k being Nat st

for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e

hence
ap is convergent
by SEQ_2:def 6; :: thesis: lim ap = (lim a) to_power pex k being Nat st

for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e

let e be Real; :: thesis: ( 0 < e implies ex k being Nat st

for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e )

assume A37: 0 < e ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e

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: for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e

let m be Nat; :: thesis: ( k <= m implies |.((ap . m) - ((lim a) to_power p)).| < e )

assume A39: k <= m ; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e

end;for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e )

assume A37: 0 < e ; :: thesis: ex k being Nat st

for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e

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: for m being Nat st k <= m holds

|.((ap . m) - ((lim a) to_power p)).| < e

let m be Nat; :: thesis: ( k <= m implies |.((ap . m) - ((lim a) to_power p)).| < e )

assume A39: k <= m ; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e

now :: thesis: ( ( a . m = 0 & |.((ap . m) - ((lim a) to_power p)).| < e ) or ( a . m <> 0 & |.((ap . m) - ((lim a) to_power p)).| < e ) )end;

hence
|.((ap . m) - ((lim a) to_power p)).| < e
; :: thesis: verumper cases
( a . m = 0 or a . m <> 0 )
;

end;

case
a . m = 0
; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e

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: verum

end;.= 0 by A1, POWER:def 2 ;

hence |.((ap . m) - ((lim a) to_power p)).| < e by A15, A37, ABSVALUE:2; :: thesis: verum

case A40:
a . m <> 0
; :: thesis: |.((ap . m) - ((lim a) to_power p)).| < e

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: verum

end;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: verum

hence lim ap = (lim a) to_power p by A36, SEQ_2:def 7; :: thesis: verum

case A47:
lim a <> 0
; :: thesis: ( ap is convergent & lim ap = (lim a) to_power p )

A48:
0 <= lim a
by A2, A3, SEQ_2:17;

ex k being Nat st rng (a ^\ k) c= dom (#R p)

A53: rng (a ^\ k) c= dom (#R p) ;

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: verum

end;ex k being Nat st rng (a ^\ k) c= dom (#R p)

proof

then consider k being Nat such that
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: rng (a ^\ k) c= dom (#R p)

assume x in rng (a ^\ k) ; :: thesis: x in dom (#R p)

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: verum

end;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: rng (a ^\ k) c= dom (#R p)

A51: now :: thesis: for m being Nat holds 0 < (a ^\ k) . m

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (a ^\ k) or x in dom (#R p) )let m be Nat; :: thesis: 0 < (a ^\ k) . m

|.((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: verum

end;|.((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: verum

assume x in rng (a ^\ k) ; :: thesis: x in dom (#R p)

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: verum

A53: rng (a ^\ k) c= dom (#R p) ;

now :: thesis: for x being object st x in NAT holds

((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x

then A56:
(#R p) /* (a ^\ k) = ap ^\ k
by FUNCT_2:12;((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x

let x be object ; :: thesis: ( x in NAT implies ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x )

assume x in NAT ; :: thesis: ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x

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: verum

end;assume x in NAT ; :: thesis: ((#R p) /* (a ^\ k)) . x = (ap ^\ k) . x

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: verum

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: verum