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

A2: now :: thesis: for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being set st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p )
assume 0 < p ; :: thesis: ex n being set st
for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p
then consider n1 being Nat such that
A3: for m being Nat st n1 <= m holds
|.(((seq ^\ k) . m) - (lim (seq ^\ k))).| < p by A1, SEQ_2:def 7;
take n = n1 + k; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - (lim (seq ^\ k))).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - (lim (seq ^\ k))).| < p )
assume A4: n <= m ; :: thesis: |.((seq . m) - (lim (seq ^\ k))).| < p
then consider l being Nat such that
A5: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
m - k = ((n1 + l) + k) + (- k) by A5;
then consider m1 being Nat such that
A6: m1 = m - k ;

now :: thesis: n1 <= m1

assume not n1 <= m1 ; :: thesis: contradiction
then m1 + k < n1 + k by XREAL_1:6;
hence contradiction by A4, A6; :: thesis: verum

end;

then A7: |.(((seq ^\ k) . m1) - (lim (seq ^\ k))).| < p by A3;
m1 + k = m by A6;
hence |.((seq . m) - (lim (seq ^\ k))).| < p by A7, NAT_1:def 3; :: thesis: verum

end;

seq is convergent by A1, Th21;
hence lim seq = lim (seq ^\ k) by A2, SEQ_2:def 7; :: thesis: verum