let x0 be Real; :: thesis: for seq being Real_Sequence
for f being PartFunc of REAL ,REAL st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
for r being Real st 0 < r holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )
let seq be Real_Sequence; :: thesis: for f being PartFunc of REAL ,REAL st seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} holds
for r being Real st 0 < r holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )
let f be PartFunc of REAL ,REAL ; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} implies for r being Real st 0 < r holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f ) )
assume A1: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} ) ; :: thesis: for r being Real st 0 < r holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )
let r be Real; :: thesis: ( 0 < r implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f ) )
assume 0 < r ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )
then consider n being Element of NAT such that
A2: for k being Element of NAT st n <= k holds
abs ((seq . k) - x0) < r by A1, SEQ_2:def 7;
take n ; :: thesis: for k being Element of NAT st n <= k holds
( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )

A3: now

let n be Element of NAT ; :: thesis: (seq . n) - x0 <> 0
seq . n in rng seq by VALUED_0:28;
then not seq . n in {x0} by A1, XBOOLE_0:def 5;
hence (seq . n) - x0 <> 0 by TARSKI:def 1; :: thesis: verum

end;

let k be Element of NAT ; :: thesis: ( n <= k implies ( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f ) )
assume A4: n <= k ; :: thesis: ( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )
(seq . k) - x0 <> 0 by A3;
then 0 < abs (- (x0 - (seq . k))) by COMPLEX1:133;
hence 0 < abs (x0 - (seq . k)) by COMPLEX1:138; :: thesis: ( abs (x0 - (seq . k)) < r & seq . k in dom f )
abs ((seq . k) - x0) < r by A2, A4;
then abs (- (x0 - (seq . k))) < r ;
hence abs (x0 - (seq . k)) < r by COMPLEX1:138; :: thesis: seq . k in dom f
seq . k in rng seq by VALUED_0:28;
hence seq . k in dom f by A1, XBOOLE_0:def 5; :: thesis: verum