theorem :: LIMFUNC1:101

for f, f1, f2 being PartFunc of REAL,REAL st f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ex r being Real st
( right_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in right_open_halfline r holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )