let k be Element of NAT ; :: thesis: for seq being ExtREAL_sequence st seq ^\ k is convergent_to_finite_number holds
( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) )
let seq be ExtREAL_sequence; :: thesis: ( seq ^\ k is convergent_to_finite_number implies ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) ) )
assume A1: seq ^\ k is convergent_to_finite_number ; :: thesis: ( seq is convergent_to_finite_number & seq is convergent & lim seq = lim (seq ^\ k) )
set seq0 = seq ^\ k;
A2: seq ^\ k is convergent by A1, MESFUNC5:def 11;
( ( not lim (seq ^\ k) = +infty or not seq ^\ k is convergent_to_+infty ) & ( not lim (seq ^\ k) = -infty or not seq ^\ k is convergent_to_-infty ) ) by A1, MESFUNC5:56, MESFUNC5:57;
then A3: ex g being real number st
( lim (seq ^\ k) = g & ( for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p ) & seq ^\ k is convergent_to_finite_number ) by A2, MESFUNC5:def 12;
then consider g being real number such that
A4: lim (seq ^\ k) = g ;
A5: for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p

proof

let p be real number ; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p
then consider n being Nat such that
A6: for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p by A3;
take n1 = n + k; :: thesis: for m being Nat st n1 <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n1 <= m implies |.((seq . m) - (lim (seq ^\ k))).| < p )
assume A7: n1 <= m ; :: thesis: |.((seq . m) - (lim (seq ^\ k))).| < p
then A8: (n + k) - k <= m - k by XREAL_1:11;
k <= n + k by NAT_1:11;
then reconsider mk = m - k as Element of NAT by A7, INT_1:18, XXREAL_0:2;
(seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def 3;
hence |.((seq . m) - (lim (seq ^\ k))).| < p by A6, A8; :: thesis: verum

end;

end;

lim (seq ^\ k) = R_EAL g by A4;
hence A9: seq is convergent_to_finite_number by A5, MESFUNC5:def 8; :: thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )
hence seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = lim (seq ^\ k)
hence lim seq = lim (seq ^\ k) by A4, A5, A9, MESFUNC5:def 12; :: thesis: verum