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

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

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

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

end;

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

then A3: ( lim seq = +infty & seq is convergent_to_+infty ) by A1, MESFUNC5:def 12;
for g being real number 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 number ; :: thesis: ( 0 < g implies ex n being Nat st
for m being Nat st n <= m holds
g <= (seq ^\ k) . m )
assume 0 < g ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
g <= (seq ^\ k) . m
then consider n being Nat such that
A4: for m being Nat st n <= m holds
g <= seq . m by A2, MESFUNC5:def 9;
take n ; :: thesis: for m being Nat st n <= m holds
g <= (seq ^\ k) . m

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies g <= (seq ^\ k) . m )
assume A5: n <= m ; :: thesis: g <= (seq ^\ k) . m
m <= m + k by NAT_1:11;
then n <= m + k by A5, XXREAL_0:2;
then A6: g <= seq . (m + k) by A4;
m is Element of NAT by ORDINAL1:def 13;
hence g <= (seq ^\ k) . m by A6, NAT_1:def 3; :: thesis: verum

end;

end;

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

end;

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

then A9: ( lim seq = -infty & seq is convergent_to_-infty ) by A1, MESFUNC5:def 12;
for g being real number 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 number ; :: thesis: ( g < 0 implies ex n being Nat st
for m being Nat st n <= m holds
(seq ^\ k) . m <= g )
assume g < 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(seq ^\ k) . m <= g
then consider n being Nat such that
A10: for m being Nat st n <= m holds
seq . m <= g by A8, MESFUNC5:def 10;
take n ; :: thesis: for m being Nat st n <= m holds
(seq ^\ k) . m <= g

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies (seq ^\ k) . m <= g )
assume A11: n <= m ; :: thesis: (seq ^\ k) . m <= g
m <= m + k by NAT_1:11;
then n <= m + k by A11, XXREAL_0:2;
then A12: seq . (m + k) <= g by A10;
m is Element of NAT by ORDINAL1:def 13;
hence (seq ^\ k) . m <= g by A12, NAT_1:def 3; :: thesis: verum

end;

end;

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

end;

end;