theorem :: LIMFUNC1:103

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
( left_open_halfline r c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in left_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 )