let X be RealNormSpace; :: thesis: for seq, seq1 being sequence of X st seq1 is subsequence of seq & seq is convergent holds

lim seq1 = lim seq

let seq, seq1 be sequence of X; :: thesis: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )

assume that

A1: seq1 is subsequence of seq and

A2: seq is convergent ; :: thesis: lim seq1 = lim seq

consider Nseq being increasing sequence of NAT such that

A3: seq1 = seq * Nseq by A1, VALUED_0:def 17;

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: ( seq1 is subsequence of seq & seq is convergent implies lim seq1 = lim seq )

assume that

A1: seq1 is subsequence of seq and

A2: seq is convergent ; :: thesis: lim seq1 = lim seq

consider Nseq being increasing sequence of NAT such that

A3: seq1 = seq * Nseq by A1, VALUED_0:def 17;

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

ex n being Nat st

for m being Nat st n <= m holds

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

seq1 is convergent
by A1, A2, Th7;ex n being Nat 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 Nat st

for m being Nat st n <= m holds

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

assume 0 < p ; :: thesis: ex n being Nat 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 A2, NORMSP_1:def 7;

take n = n1; :: 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

A7: m in NAT by ORDINAL1:def 12;

m <= Nseq . m by SEQM_3:14;

then A8: n <= Nseq . m by A6, XXREAL_0:2;

seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15, A7;

hence ||.((seq1 . m) - (lim seq)).|| < p by A5, A8; :: thesis: verum

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

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

assume 0 < p ; :: thesis: ex n being Nat 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 A2, NORMSP_1:def 7;

take n = n1; :: 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

A7: m in NAT by ORDINAL1:def 12;

m <= Nseq . m by SEQM_3:14;

then A8: n <= Nseq . m by A6, XXREAL_0:2;

seq1 . m = seq . (Nseq . m) by A3, FUNCT_2:15, A7;

hence ||.((seq1 . m) - (lim seq)).|| < p by A5, A8; :: thesis: verum

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