let k be Nat; :: thesis: for seq being ExtREAL_sequence st seq ^\ k is convergent holds
( seq is convergent & lim seq = lim (seq ^\ k) )
let seq be ExtREAL_sequence; :: thesis: ( seq ^\ k is convergent implies ( seq is convergent & lim seq = lim (seq ^\ k) ) )
set seq0 = seq ^\ k;
assume A1: seq ^\ k is convergent ; :: thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )

per cases ( seq ^\ k is convergent_to_finite_number or seq ^\ k is convergent_to_+infty or seq ^\ k is convergent_to_-infty ) by A1, MESFUNC5:def 11;

suppose seq ^\ k is convergent_to_finite_number ; :: thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )

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

end;

suppose A2: seq ^\ k is convergent_to_+infty ; :: thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )

for g being Real st 0 < g holds
ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m

proof

let g be Real; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= seq . m
then consider n being Nat such that
A3: for m being Nat st n <= m holds
g <= (seq ^\ k) . m by A2, MESFUNC5:def 9;
take n1 = n + k; :: thesis: for m being Nat st n1 <= m holds
g <= seq . m

hereby :: thesis: verum

let m be Nat; :: thesis: ( n1 <= m implies g <= seq . m )
assume A4: n1 <= m ; :: thesis: g <= seq . m
k <= n + k by NAT_1:11;
then reconsider mk = m - k as Element of NAT by A4, INT_1:5, XXREAL_0:2;
A5: (seq ^\ k) . (m - k) = seq . (mk + k) by NAT_1:def 3;
(n + k) - k <= m - k by A4, XREAL_1:9;
hence g <= seq . m by A3, A5; :: thesis: verum

end;

end;

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

end;

suppose A8: seq ^\ k is convergent_to_-infty ; :: thesis: ( seq is convergent & lim seq = lim (seq ^\ k) )

for g being Real st g < 0 holds
ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g

proof

let g be Real; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g )
assume g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
seq . m <= g
then consider n being Nat such that
A9: for m being Nat st n <= m holds
(seq ^\ k) . m <= g by A8, MESFUNC5:def 10;
take n1 = n + k; :: thesis: for m being Nat st n1 <= m holds
seq . m <= g

hereby :: thesis: verum

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

end;

end;

then A12: seq is convergent_to_-infty by MESFUNC5:def 10;
hence A13: seq is convergent by MESFUNC5:def 11; :: thesis: lim seq = lim (seq ^\ k)
lim (seq ^\ k) = -infty by A1, A8, MESFUNC5:def 12;
hence lim seq = lim (seq ^\ k) by A12, A13, MESFUNC5:def 12; :: thesis: verum

end;

end;