let f be PartFunc of REAL,REAL; :: thesis: for x0, t being Real holds
( f is_right_convergent_in x0 & lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
let x0, t be Real; :: thesis: ( f is_right_convergent_in x0 & lim_right (f,x0) = t iff ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
thus ( f is_right_convergent_in x0 & lim_right (f,x0) = t implies ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) ) ) by LIMFUNC2:def 4, LIMFUNC2:def 8; :: thesis: ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = t ) )
reconsider t = t as Real ;
( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = t ) )

proof

assume that
A1: for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) and
A2: for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ; :: thesis: ( f is_right_convergent_in x0 & lim_right (f,x0) = t )
thus f is_right_convergent_in x0 by A1, A2, LIMFUNC2:def 4; :: thesis: lim_right (f,x0) = t
hence lim_right (f,x0) = t by A2, LIMFUNC2:def 8; :: thesis: verum

end;

hence ( ( for r being Real st x0 < r holds
ex t being Real st
( t < r & x0 < t & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (right_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = t ) ) ; :: thesis: verum