theorem Th65: :: LIMFUNC2:65

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