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 < |.(x0 - (seq . k)).| & |.(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 < |.(x0 - (seq . k)).| & |.(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 < |.(x0 - (seq . k)).| & |.(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 < |.(x0 - (seq . k)).| & |.(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 < |.(x0 - (seq . k)).| & |.(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 < |.(x0 - (seq . k)).| & |.(x0 - (seq . k)).| < r & seq . k in dom f )
then consider n being Nat such that
A4: for k being Nat st n <= k holds
|.((seq . k) - x0).| < r by A1, A2, SEQ_2:def 7;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
take n ; :: thesis: for k being Element of NAT st n <= k holds
( 0 < |.(x0 - (seq . k)).| & |.(x0 - (seq . k)).| < r & seq . k in dom f )
let k be Element of NAT ; :: thesis: ( n <= k implies ( 0 < |.(x0 - (seq . k)).| & |.(x0 - (seq . k)).| < r & seq . k in dom f ) )
assume n <= k ; :: thesis: ( 0 < |.(x0 - (seq . k)).| & |.(x0 - (seq . k)).| < r & seq . k in dom f )
then |.((seq . k) - x0).| < r by A4;
then A5: |.(- (x0 - (seq . k))).| < r ;
now :: thesis: for n being Element of NAT holds (seq . n) - x0 <> 0
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 < |.(- (x0 - (seq . k))).| by COMPLEX1:47;
hence 0 < |.(x0 - (seq . k)).| by COMPLEX1:52; :: thesis: ( |.(x0 - (seq . k)).| < r & seq . k in dom f )
thus |.(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