let X be RealNormSpace; :: thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent

let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & ex k being Nat st seq = seq1 ^\ k implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Nat st seq = seq1 ^\ k ; :: thesis: seq1 is convergent
consider k being Nat such that
A3: seq = seq1 ^\ k by A2;
consider g1 being Element of X such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - g1).|| < p by A1;
take g1 ; :: according to NORMSP_1:def 6 :: thesis: for b1 being object holds
( b1 <= 0 or ex b2 being set st
for b3 being set holds
( not b2 <= b3 or not b1 <= ||.((seq1 . b3) - g1).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| ) )

assume 0 < p ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= ||.((seq1 . b2) - g1).|| )

then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
||.((seq . m) - g1).|| < p by A4;
take n = n1 + k; :: thesis: for b1 being set holds
( not n <= b1 or not p <= ||.((seq1 . b1) - g1).|| )

let m be Nat; :: thesis: ( not n <= m or not p <= ||.((seq1 . m) - g1).|| )
assume A6: n <= m ; :: thesis: not p <= ||.((seq1 . m) - g1).||
then consider l being Nat such that
A7: m = (n1 + k) + l by NAT_1:10;
reconsider l = l as Nat ;
m - k = ((n1 + l) + k) + (- k) by A7;
then reconsider m1 = m - k as Nat ;
now :: thesis: n1 <= m1
assume not n1 <= m1 ; :: thesis: contradiction
then m1 + k < n1 + k by XREAL_1:6;
hence contradiction by A6; :: thesis: verum
end;
then ( m1 + k = m & ||.((seq . m1) - g1).|| < p ) by A5;
hence not p <= ||.((seq1 . m) - g1).|| by ; :: thesis: verum