let k be Nat; :: thesis:
let seq be ExtREAL_sequence; :: thesis:
set seq0 = seq ^\ k;
assume A1: seq ^\ k is convergent_to_finite_number ; :: thesis:
then A2: ( not lim (seq ^\ k) = +infty or not seq ^\ k is convergent_to_+infty ) by MESFUNC5:50;
A3: ( not lim (seq ^\ k) = -infty or not seq ^\ k is convergent_to_-infty ) by A1, MESFUNC5:51;
seq ^\ k is convergent by A1, MESFUNC5:def 11;
then A4: ex g being Real st
( lim (seq ^\ k) = g & ( for p being Real 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, A3, MESFUNC5:def 12;
then consider g being Real such that
A5: lim (seq ^\ k) = g ;
A6: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p

let p be Real; :: thesis:
assume 0 < p ; :: thesis:
then consider n being Nat such that
A7: for m being Nat st n <= m holds
|.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p by A4;
take n1 = n + k; :: thesis:

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

end;