let f be PartFunc of REAL,REAL; for x0, t being Real holds
( f is_left_convergent_in x0 & lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
let x0, t be Real; ( f is_left_convergent_in x0 & lim_left (f,x0) = t iff ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
thus
( f is_left_convergent_in x0 & lim_left (f,x0) = t implies ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) ) )
by LIMFUNC2:def 1, LIMFUNC2:def 7; ( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = t ) )
reconsider t = t as Real ;
( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = t ) )
hence
( ( for r being Real st r < x0 holds
ex t being Real st
( r < t & t < x0 & t in dom f ) ) & ( for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom f) /\ (left_open_halfline x0) holds
( f /* a is convergent & lim (f /* a) = t ) ) implies ( f is_left_convergent_in x0 & lim_left (f,x0) = t ) )
; verum