theorem :: LIMFUNC2:64

for x0 being Real
for f, f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f1,x0) = lim_left (f2,x0) & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )