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 that
A1: seq is convergent and
A2: lim seq = x0 and
A3: 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
A4: for k being Element of NAT st n <= k holds
abs ((seq . k) - x0) < r by A1, A2, 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 )
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 n <= k ; :: thesis: ( 0 < abs (x0 - (seq . k)) & abs (x0 - (seq . k)) < r & seq . k in dom f )
then abs ((seq . k) - x0) < r by A4;
then A5: abs (- (x0 - (seq . k))) < r ;

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 A3, XBOOLE_0:def 5;
hence (seq . n) - x0 <> 0 by TARSKI:def 1; :: thesis: verum

end;

then (seq . k) - x0 <> 0 ;
then 0 < abs (- (x0 - (seq . k))) by COMPLEX1:47;
hence 0 < abs (x0 - (seq . k)) by COMPLEX1:52; :: thesis: ( abs (x0 - (seq . k)) < r & seq . k in dom f )
thus abs (x0 - (seq . k)) < r by A5, COMPLEX1:52; :: thesis: seq . k in dom f
seq . k in rng seq by VALUED_0:28;
hence seq . k in dom f by A3, XBOOLE_0:def 5; :: thesis: verum