:: deftheorem Def7 defines lim_left LIMFUNC2:def 7 :
for f being PartFunc of REAL,REAL
for x0 being Real st f is_left_convergent_in x0 holds
for b₃ being Real holds
( b₃ = lim_left (f,x0) iff for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) holds
( f /* seq is convergent & lim (f /* seq) = b₃ ) );