let k be Nat; :: thesis: for seq being ExtREAL_sequence st seq is convergent_to_finite_number holds

( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) )

let seq be ExtREAL_sequence; :: thesis: ( seq is convergent_to_finite_number implies ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) )

set seq0 = seq ^\ k;

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

then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50;

A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51;

seq is convergent by A1, MESFUNC5:def 11;

then A4: ex g being Real st

( lim seq = g & ( 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)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def 12;

then consider g being Real such that

A5: lim seq = g ;

A6: 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)).| < p

hence A9: seq ^\ k is convergent_to_finite_number by A6, MESFUNC5:def 8; :: thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )

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

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

( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) )

let seq be ExtREAL_sequence; :: thesis: ( seq is convergent_to_finite_number implies ( seq ^\ k is convergent_to_finite_number & seq ^\ k is convergent & lim seq = lim (seq ^\ k) ) )

set seq0 = seq ^\ k;

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

then A2: ( not lim seq = +infty or not seq is convergent_to_+infty ) by MESFUNC5:50;

A3: ( not lim seq = -infty or not seq is convergent_to_-infty ) by A1, MESFUNC5:51;

seq is convergent by A1, MESFUNC5:def 11;

then A4: ex g being Real st

( lim seq = g & ( 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)).| < p ) & seq is convergent_to_finite_number ) by A2, A3, MESFUNC5:def 12;

then consider g being Real such that

A5: lim seq = g ;

A6: 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)).| < p

proof

lim seq = g
by A5;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st

for m being Nat st n <= m holds

|.(((seq ^\ k) . m) - (lim seq)).| < p )

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((seq ^\ k) . m) - (lim seq)).| < p

then consider n being Nat such that

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

|.((seq . m) - (lim seq)).| < p by A4;

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

|.(((seq ^\ k) . m) - (lim seq)).| < p

end;for m being Nat st n <= m holds

|.(((seq ^\ k) . m) - (lim seq)).| < p )

assume 0 < p ; :: thesis: ex n being Nat st

for m being Nat st n <= m holds

|.(((seq ^\ k) . m) - (lim seq)).| < p

then consider n being Nat such that

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

|.((seq . m) - (lim seq)).| < p by A4;

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

|.(((seq ^\ k) . m) - (lim seq)).| < p

hereby :: thesis: verum

let m be Nat; :: thesis: ( n <= m implies |.(((seq ^\ k) . m) - (lim seq)).| < p )

assume A8: n <= m ; :: thesis: |.(((seq ^\ k) . m) - (lim seq)).| < p

m <= m + k by NAT_1:11;

then n <= m + k by A8, XXREAL_0:2;

then |.((seq . (m + k)) - (lim seq)).| < p by A7;

hence |.(((seq ^\ k) . m) - (lim seq)).| < p by NAT_1:def 3; :: thesis: verum

end;assume A8: n <= m ; :: thesis: |.(((seq ^\ k) . m) - (lim seq)).| < p

m <= m + k by NAT_1:11;

then n <= m + k by A8, XXREAL_0:2;

then |.((seq . (m + k)) - (lim seq)).| < p by A7;

hence |.(((seq ^\ k) . m) - (lim seq)).| < p by NAT_1:def 3; :: thesis: verum

hence A9: seq ^\ k is convergent_to_finite_number by A6, MESFUNC5:def 8; :: thesis: ( seq ^\ k is convergent & lim seq = lim (seq ^\ k) )

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

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