let x0 be Real; :: thesis: for seq being Real_Sequence
for f being PartFunc of REAL ,REAL st ( for n being Element of NAT holds
( 0 < abs (x0 - (seq . n)) & abs (x0 - (seq . n)) < 1 / (n + 1) & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} )
let seq be Real_Sequence; :: thesis: for f being PartFunc of REAL ,REAL st ( for n being Element of NAT holds
( 0 < abs (x0 - (seq . n)) & abs (x0 - (seq . n)) < 1 / (n + 1) & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} )
let f be PartFunc of REAL ,REAL ; :: thesis: ( ( for n being Element of NAT holds
( 0 < abs (x0 - (seq . n)) & abs (x0 - (seq . n)) < 1 / (n + 1) & seq . n in dom f ) ) implies ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} ) )
assume A1: for n being Element of NAT holds
( 0 < abs (x0 - (seq . n)) & abs (x0 - (seq . n)) < 1 / (n + 1) & seq . n in dom f ) ; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} )

A2: now

let r be real number ; :: thesis: ( 0 < r implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((seq . k) - x0) < r )
assume A3: 0 < r ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
abs ((seq . k) - x0) < r
consider n being Element of NAT such that
A4: r " < n by SEQ_4:10;
take n = n; :: thesis: for k being Element of NAT st n <= k holds
abs ((seq . k) - x0) < r
let k be Element of NAT ; :: thesis: ( n <= k implies abs ((seq . k) - x0) < r )
assume n <= k ; :: thesis: abs ((seq . k) - x0) < r
then n + 1 <= k + 1 by XREAL_1:8;
then A5: 1 / (k + 1) <= 1 / (n + 1) by XREAL_1:120;
n <= n + 1 by NAT_1:12;
then r " < n + 1 by A4, XXREAL_0:2;
then 1 / (n + 1) < 1 / (r " ) by A3, XREAL_1:78;
then 1 / (k + 1) < 1 / (r " ) by A5, XXREAL_0:2;
then A6: 1 / (k + 1) < r by XCMPLX_1:218;
abs (x0 - (seq . k)) < 1 / (k + 1) by A1;
then abs (- ((seq . k) - x0)) < r by A6, XXREAL_0:2;
hence abs ((seq . k) - x0) < r by COMPLEX1:138; :: thesis: verum

end;

hence seq is convergent by SEQ_2:def 6; :: thesis: ( lim seq = x0 & rng seq c= dom f & rng seq c= (dom f) \ {x0} )
hence lim seq = x0 by A2, SEQ_2:def 7; :: thesis: ( rng seq c= dom f & rng seq c= (dom f) \ {x0} )
thus A7: rng seq c= dom f :: thesis: rng seq c= (dom f) \ {x0}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng seq or x in dom f )
assume x in rng seq ; :: thesis: x in dom f
then ex n being Element of NAT st seq . n = x by FUNCT_2:190;
hence x in dom f by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng seq or x in (dom f) \ {x0} )
assume A8: x in rng seq ; :: thesis: x in (dom f) \ {x0}
then consider n being Element of NAT such that
A9: seq . n = x by FUNCT_2:190;
0 <> abs (x0 - (seq . n)) by A1;
then (x0 - (seq . n)) + (seq . n) <> 0 + (seq . n) by ABSVALUE:7;
then not x in {x0} by A9, TARSKI:def 1;
hence x in (dom f) \ {x0} by A7, A8, XBOOLE_0:def 5; :: thesis: verum