let f be PartFunc of REAL,REAL; :: thesis: for x0 being Real st ( f is_right_convergent_in x0 or f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds
ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) )
let x0 be Real; :: thesis: ( ( f is_right_convergent_in x0 or f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) implies ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) ) )
assume A1: ( f is_right_convergent_in x0 or f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) ; :: thesis: ex seq being Real_Sequence st
( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) )
defpred S1[ Nat, Real] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f );
A2: for n being Element of NAT ex r being Element of REAL st S1[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S1[n,r]
consider r being Real such that
A3: ( r < x0 + (1 / (n + 1)) & x0 < r & r in dom f ) by A1, XREAL_1:29, LIMFUNC2:def 4, LIMFUNC2:def 5, LIMFUNC2:def 6;
thus ex r being Element of REAL st
( x0 < r & r < x0 + (1 / (n + 1)) & r in dom f ) by A3; :: thesis: verum
end;
consider seq being Real_Sequence such that
A4: for n being Element of NAT holds S1[n,seq . n] from FUNCT_2:sch 3(A2);
 take seq ; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) )
for n being Nat holds
( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f )
proof
let n be Nat; :: thesis: ( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f )
n is Element of NAT by ORDINAL1:def 12;
hence ( x0 < seq . n & seq . n < x0 + (1 / (n + 1)) & seq . n in dom f ) by A4; :: thesis: verum
end;
hence ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (right_open_halfline x0) ) by LIMFUNC2:6; :: thesis: verum