let k be Element of NAT ; :: thesis: for seq being Real_Sequence st seq ^\ k is convergent holds
seq is convergent
let seq be Real_Sequence; :: thesis: ( seq ^\ k is convergent implies seq is convergent )
assume seq ^\ k is convergent ; :: thesis: seq is convergent
then consider g1 being real number such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq ^\ k) . m) - g1) < p by SEQ_2:def 6;
take g = g1; :: according to SEQ_2:def 6 :: thesis: for b₁ being set holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= abs ((seq . b₃) - g) ) )
let p be real number ; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq . b₂) - g) ) )
assume 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= abs ((seq . b₂) - g) )
then consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
abs (((seq ^\ k) . m) - g1) < p by A1;
take n = n1 + k; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= abs ((seq . b₁) - g) )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= abs ((seq . m) - g) )
assume A3: n <= m ; :: thesis: not p <= abs ((seq . m) - g)
then consider l being Nat such that
A4: 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 A4;
then consider m1 being Element of NAT such that
A5: m1 = m - k ;

now

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

end;

then A6: abs (((seq ^\ k) . m1) - g1) < p by A2;
m1 + k = m by A5;
hence not p <= abs ((seq . m) - g) by A6, NAT_1:def 3; :: thesis: verum