let x0 be Real; :: thesis: 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
let f, f1 be PartFunc of REAL,REAL; :: thesis: ( 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 ) ) implies f is_right_divergent_to+infty_in x0 )
assume A1: f1 is_right_divergent_to+infty_in x0 ; :: thesis: ( for r being Real holds
( not 0 < r or not ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) or ex g being Real st
( g in ].x0,(x0 + r).[ & not f1 . g <= f . g ) ) or f is_right_divergent_to+infty_in x0 )
given r being Real such that A2: 0 < r and
A3: ].x0,(x0 + r).[ c= (dom f) /\ (dom f1) and
A4: for g being Real st g in ].x0,(x0 + r).[ holds
f1 . g <= f . g ; :: thesis: f is_right_divergent_to+infty_in x0
A5: (dom f) /\ (dom f1) c= dom f by XBOOLE_1:17;
then A6: ].x0,(x0 + r).[ = (dom f) /\ ].x0,(x0 + r).[ by A3, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ (dom f1) c= dom f1 by XBOOLE_1:17;
then A7: ].x0,(x0 + r).[ = (dom f1) /\ ].x0,(x0 + r).[ by A3, XBOOLE_1:1, XBOOLE_1:28;
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) by A2, A3, A5, Th4, XBOOLE_1:1;
hence f is_right_divergent_to+infty_in x0 by A1, A2, A4, A6, A7, Th35; :: thesis: verum