let x0 be Real; :: thesis: for f being PartFunc of REAL ,REAL holds
( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_right_divergent_to-infty_in x0 iff ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
thus ( f is_right_divergent_to-infty_in x0 implies ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) ) ) :: thesis: ( ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) ) & ( for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ) implies f is_right_divergent_to-infty_in x0 )

proof

assume that
A1: f is_right_divergent_to-infty_in x0 and
A2: ( ex r being Real st
( x0 < r & ( for g being Real holds
( not g < r or not x0 < g or not g in dom f ) ) ) or ex g1 being Real st
for r being Real st x0 < r holds
ex r1 being Real st
( r1 < r & x0 < r1 & r1 in dom f & g1 <= f . r1 ) ) ; :: thesis: contradiction
consider g1 being Real such that
A3: for r being Real st x0 < r holds
ex r1 being Real st
( r1 < r & x0 < r1 & r1 in dom f & g1 <= f . r1 ) by A1, A2, Def6;
defpred S₁[ Element of NAT , real number ] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f & g1 <= f . $2 );

A4: now

let n be Element of NAT ; :: thesis: ex r1 being Real st S₁[n,r1]
x0 < x0 + (1 / (n + 1)) by Lm3;
then consider r1 being Real such that
A5: ( r1 < x0 + (1 / (n + 1)) & x0 < r1 & r1 in dom f & g1 <= f . r1 ) by A3;
take r1 = r1; :: thesis: S₁[n,r1]
thus S₁[n,r1] by A5; :: thesis: verum

end;

consider s being Real_Sequence such that
A6: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A4);
A7: ( s is convergent & lim s = x0 & rng s c= dom f & rng s c= (dom f) /\ (right_open_halfline x0) ) by A6, Th6;
then f /* s is divergent_to-infty by A1, Def6;
then consider n being Element of NAT such that
A8: for k being Element of NAT st n <= k holds
(f /* s) . k < g1 by LIMFUNC1:def 5;
(f /* s) . n < g1 by A8;
then f . (s . n) < g1 by A7, FUNCT_2:185;
hence contradiction by A6; :: thesis: verum

end;

assume that
A9: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) and
A10: for g1 being Real ex r being Real st
( x0 < r & ( for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
f . r1 < g1 ) ) ; :: thesis: f is_right_divergent_to-infty_in x0
for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) holds
f /* s is divergent_to-infty by A10, Lm5;
hence f is_right_divergent_to-infty_in x0 by A9, Def6; :: thesis: verum