theorem :: LIMFUNC2:39

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