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