let k be Element of 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)
A3: seq is convergent by A1, Th35;

now

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

A9: now

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

end;

A10: m1 + k = m by A8;
abs (((seq ^\ k) . m1) - (lim (seq ^\ k))) < p by A5, A9;
hence abs ((seq . m) - (lim (seq ^\ k))) < p by A10, NAT_1:def 3; :: thesis: verum

end;

hence lim seq = lim (seq ^\ k) by A3, SEQ_2:def 7; :: thesis: verum