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
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & 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
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) holds
( seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} )
let f be PartFunc of REAL,REAL; :: thesis: ( ( for n being Element of NAT holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ) implies ( seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} ) )
assume A1: for n being Element of NAT holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) ; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) \ {x0} )
A2: for n being Nat holds
( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f )
proof
let n be Nat; :: thesis: ( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f )
n in NAT by ORDINAL1:def 12;
hence ( x0 - (1 / (n + 1)) < seq . n & seq . n < x0 & seq . n in dom f ) by A1; :: thesis: verum
end;
hence ( seq is convergent & lim seq = x0 ) by LIMFUNC2:5; :: thesis: rng seq c= (dom f) \ {x0}
rng seq c= (dom f) /\ (left_open_halfline x0) by LIMFUNC2:5, A2;
hence rng seq c= (dom f) \ {x0} by Th1; :: thesis: verum