let X be RealNormSpace; :: thesis: for seq, seq1 being sequence of X st seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k holds
lim seq1 = lim seq
let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & ex k being Element of NAT st seq = seq1 ^\ k implies lim seq1 = lim seq )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st seq = seq1 ^\ k ; :: thesis: lim seq1 = lim seq
consider k being Element of NAT such that
A3: seq = seq1 ^\ k by A2;

A4: now

let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
then consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
||.((seq . m) - (lim seq)).|| < p by A1, NORMSP_1:def 7;
take n = n1 + k; :: thesis: for m being Element of NAT st n <= m holds
||.((seq1 . m) - (lim seq)).|| < p
let m be Element of NAT ; :: thesis: ( n <= m implies ||.((seq1 . m) - (lim seq)).|| < p )
assume A6: n <= m ; :: thesis: ||.((seq1 . m) - (lim seq)).|| < 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 12;
m - k = ((n1 + l) + k) + (- k) by A7;
then reconsider m1 = m - k as Element of NAT ;

now

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) - (lim seq)).|| < p ) by A5;
hence ||.((seq1 . m) - (lim seq)).|| < p by A3, NAT_1:def 3; :: thesis: verum

end;

seq1 is convergent by A1, A2, Th15;
hence lim seq1 = lim seq by A4, NORMSP_1:def 7; :: thesis: verum