let k be Nat; :: thesis:
let seq be ExtREAL_sequence; :: thesis:
set seq0 = seq ^\ k;
assume A1: seq is convergent ; :: thesis:

per cases by A1, MESFUNC5:def 11;

suppose seq is convergent_to_finite_number ; :: thesis:

hence ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) by Th20; :: thesis:

end;

suppose A2: seq is convergent_to_+infty ; :: thesis:

for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= (seq ^\ k) . m

proof

let g be Real; :: thesis:
assume 0 < g ; :: thesis:
then consider n being Nat such that
A3: for m being Nat st n <= m holds
g <= seq . m by A2, MESFUNC5:def 9;
take n ; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume A4: n <= m ; :: thesis:
m <= m + k by NAT_1:11;
then n <= m + k by A4, XXREAL_0:2;
then g <= seq . (m + k) by A3;
hence g <= (seq ^\ k) . m by NAT_1:def 3; :: thesis:

end;

end;

then A5: seq ^\ k is convergent_to_+infty by MESFUNC5:def 9;
hence A6: seq ^\ k is convergent by MESFUNC5:def 11; :: thesis:
lim seq = +infty by A1, A2, MESFUNC5:def 12;
hence lim seq = lim (seq ^\ k) by A5, A6, MESFUNC5:def 12; :: thesis:

end;

suppose A7: seq is convergent_to_-infty ; :: thesis:

for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(seq ^\ k) . m <= g

proof

let g be Real; :: thesis:
assume g < 0 ; :: thesis:
then consider n being Nat such that
A8: for m being Nat st n <= m holds
seq . m <= g by A7, MESFUNC5:def 10;
take n ; :: thesis:

hereby :: thesis:

let m be Nat; :: thesis:
assume A9: n <= m ; :: thesis:
m <= m + k by NAT_1:11;
then n <= m + k by A9, XXREAL_0:2;
then seq . (m + k) <= g by A8;
hence (seq ^\ k) . m <= g by NAT_1:def 3; :: thesis:

end;

end;

then A10: seq ^\ k is convergent_to_-infty by MESFUNC5:def 10;
hence A11: seq ^\ k is convergent by MESFUNC5:def 11; :: thesis:
lim seq = -infty by A1, A7, MESFUNC5:def 12;
hence lim seq = lim (seq ^\ k) by A10, A11, MESFUNC5:def 12; :: thesis:

end;

end;