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

lim seq1 = lim seq

let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & ex k being Nat st seq = seq1 ^\ k implies lim seq1 = lim seq )

assume that

A1: seq is convergent and

A2: ex k being Nat st seq = seq1 ^\ k ; :: thesis: lim seq1 = lim seq

consider k being Nat such that

A3: seq = seq1 ^\ k by A2;

hence lim seq1 = lim seq by A4, NORMSP_1:def 7; :: thesis: verum

lim seq1 = lim seq

let seq, seq1 be sequence of X; :: thesis: ( seq is convergent & ex k being Nat st seq = seq1 ^\ k implies lim seq1 = lim seq )

assume that

A1: seq is convergent and

A2: ex k being Nat st seq = seq1 ^\ k ; :: thesis: lim seq1 = lim seq

consider k being Nat such that

A3: seq = seq1 ^\ k by A2;

A4: now :: thesis: for p being Real st 0 < p holds

ex n being set st

for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p

seq1 is convergent
by A1, A2, Th10;ex n being set st

for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p

let p be Real; :: thesis: ( 0 < p implies ex n being set st

for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p )

assume 0 < p ; :: thesis: ex n being set st

for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p

then consider n1 being Nat such that

A5: for m being Nat st n1 <= m holds

||.((seq . m) - (lim seq)).|| < p by A1, NORMSP_1:def 7;

take n = n1 + k; :: thesis: for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p

let m be 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 Nat ;

m - k = ((n1 + l) + k) + (- k) by A7;

then reconsider m1 = m - k as Nat ;

hence ||.((seq1 . m) - (lim seq)).|| < p by A3, NAT_1:def 3; :: thesis: verum

end;for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p )

assume 0 < p ; :: thesis: ex n being set st

for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p

then consider n1 being Nat such that

A5: for m being Nat st n1 <= m holds

||.((seq . m) - (lim seq)).|| < p by A1, NORMSP_1:def 7;

take n = n1 + k; :: thesis: for m being Nat st n <= m holds

||.((seq1 . m) - (lim seq)).|| < p

let m be 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 Nat ;

m - k = ((n1 + l) + k) + (- k) by A7;

then reconsider m1 = m - k as Nat ;

now :: thesis: n1 <= m1

then
( m1 + k = m & ||.((seq . m1) - (lim seq)).|| < p )
by A5;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 < n1 + k by XREAL_1:6;

hence contradiction by A6; :: thesis: verum

hence ||.((seq1 . m) - (lim seq)).|| < p by A3, NAT_1:def 3; :: thesis: verum

hence lim seq1 = lim seq by A4, NORMSP_1:def 7; :: thesis: verum