let seq, seq1 be Real_Sequence; :: thesis: ( seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n implies seq1 is convergent )
assume that
A1: seq is convergent and
A2: ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n ; :: thesis: seq1 is convergent
consider g1 being Real such that
A3: 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;
consider k being Nat such that
A4: for n being Nat st k <= n holds
seq1 . n = seq . n by A2;
take g = g1; :: according to SEQ_2: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) - g).| ) )
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) - g).| ) )
assume 0 < p ; :: thesis: ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= |.((seq1 . b2) - g).| )
then consider n1 being Nat such that
A5: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < p by A3;
A6: now :: thesis: ( n1 <= k implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - g).| < p )
assume A7: n1 <= k ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - g).| < p
take n = k; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - g).| < p )
assume A8: n <= m ; :: thesis: |.((seq1 . m) - g).| < p
then n1 <= m by A7, XXREAL_0:2;
then |.((seq . m) - g1).| < p by A5;
hence |.((seq1 . m) - g).| < p by A4, A8; :: thesis: verum
end;
now :: thesis: ( k <= n1 implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - g).| < p )
assume A9: k <= n1 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq1 . m) - g).| < p
take n = n1; :: thesis: for m being Nat st n <= m holds
|.((seq1 . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq1 . m) - g).| < p )
assume A10: n <= m ; :: thesis: |.((seq1 . m) - g).| < p
then seq1 . m = seq . m by A4, A9, XXREAL_0:2;
hence |.((seq1 . m) - g).| < p by A5, A10; :: thesis: verum
end;
hence ex b1 being set st
for b2 being set holds
( not b1 <= b2 or not p <= |.((seq1 . b2) - g).| ) by A6; :: thesis: verum