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 b_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= ||.((seq1 . b_{3}) - g1).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.((seq1 . b_{2}) - g1).|| ) )

assume 0 < p ; :: thesis: ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.((seq1 . b_{2}) - 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 b_{1} being set holds

( not n <= b_{1} or not p <= ||.((seq1 . b_{1}) - 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 ;

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

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 b

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

assume 0 < p ; :: thesis: ex b

for b

( not b

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 b

( not n <= b

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

then
( m1 + k = m & ||.((seq . m1) - g1).|| < 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 not p <= ||.((seq1 . m) - g1).|| by A3, NAT_1:def 3; :: thesis: verum