let k be 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) )

( 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;

end;

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

end;

end;

suppose A2:
seq is convergent_to_+infty
; :: thesis: ( seq ^\ k 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 ^\ k) . m

hence A6: seq ^\ k is convergent by MESFUNC5:def 11; :: thesis: lim seq = lim (seq ^\ k)

lim seq = +infty by A1, A2, MESFUNC5:def 12;

hence lim seq = lim (seq ^\ k) by A5, A6, MESFUNC5:def 12; :: thesis: verum

end;ex n being Nat st

for m being Nat st n <= m holds

g <= (seq ^\ k) . m

proof

then A5:
seq ^\ k is convergent_to_+infty
by MESFUNC5:def 9;
let g be Real; :: 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

A3: 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

end;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

A3: 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

hence A6: seq ^\ k is convergent by MESFUNC5:def 11; :: thesis: lim seq = lim (seq ^\ k)

lim seq = +infty by A1, A2, MESFUNC5:def 12;

hence lim seq = lim (seq ^\ k) by A5, A6, MESFUNC5:def 12; :: thesis: verum

suppose A7:
seq is convergent_to_-infty
; :: thesis: ( seq ^\ k 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 ^\ k) . m <= g

hence A11: seq ^\ k is convergent by MESFUNC5:def 11; :: thesis: lim seq = lim (seq ^\ k)

lim seq = -infty by A1, A7, MESFUNC5:def 12;

hence lim seq = lim (seq ^\ k) by A10, A11, MESFUNC5:def 12; :: thesis: verum

end;ex n being Nat st

for m being Nat st n <= m holds

(seq ^\ k) . m <= g

proof

then A10:
seq ^\ k is convergent_to_-infty
by MESFUNC5:def 10;
let g be Real; :: 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

A8: for m being Nat st n <= m holds

seq . m <= g by A7, MESFUNC5:def 10;

take n ; :: thesis: for m being Nat st n <= m holds

(seq ^\ k) . m <= g

end;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

A8: for m being Nat st n <= m holds

seq . m <= g by A7, MESFUNC5:def 10;

take n ; :: thesis: for m being Nat st n <= m holds

(seq ^\ k) . m <= g

hence A11: seq ^\ k is convergent by MESFUNC5:def 11; :: thesis: lim seq = lim (seq ^\ k)

lim seq = -infty by A1, A7, MESFUNC5:def 12;

hence lim seq = lim (seq ^\ k) by A10, A11, MESFUNC5:def 12; :: thesis: verum