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 < |.(x0 - (seq . n)).| & |.(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 < |.(x0 - (seq . n)).| & |.(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 < |.(x0 - (seq . n)).| & |.(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 < |.(x0 - (seq . n)).| & |.(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 :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for k being Nat st n <= k holds
|.((seq . k) - x0).| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for k being Nat st n <= k holds
|.((seq . k) - x0).| < r )
assume A3: 0 < r ; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
|.((seq . k) - x0).| < r
consider n being Nat such that
A4: r " < n by SEQ_4:3;
take n = n; :: thesis: for k being Nat st n <= k holds
|.((seq . k) - x0).| < r
let k be Nat; :: thesis: ( n <= k implies |.((seq . k) - x0).| < r )
assume n <= k ; :: thesis: |.((seq . k) - x0).| < r
then n + 1 <= k + 1 by XREAL_1:6;
then A5: 1 / (k + 1) <= 1 / (n + 1) by XREAL_1:118;
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:76;
then 1 / (k + 1) < 1 / (r ") by A5, XXREAL_0:2;
then A6: 1 / (k + 1) < r by XCMPLX_1:216;
k in NAT by ORDINAL1:def 12;
then |.(x0 - (seq . k)).| < 1 / (k + 1) by A1;
then |.(- ((seq . k) - x0)).| < r by A6, XXREAL_0:2;
hence |.((seq . k) - x0).| < r by COMPLEX1:52; :: 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 object ; :: 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:113;
hence x in dom f by A1; :: thesis: verum

end;

let x be object ; :: 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:113;
0 <> |.(x0 - (seq . n)).| by A1;
then (x0 - (seq . n)) + (seq . n) <> 0 + (seq . n) by ABSVALUE:2;
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