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
g1 < f . r1 ) ) ) ) )
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
g1 < f . r1 ) ) ) ) )
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
g1 < f . r1 ) ) ) ) ) :: 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
g1 < f . r1 ) ) ) 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 & f . r1 <= g1 ) ) ; :: 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 & f . r1 <= g1 ) by A1, A2;
defpred S₁[ Nat, Real] means ( x0 < $2 & $2 < x0 + (1 / ($1 + 1)) & $2 in dom f & f . $2 <= g1 );

A4: now :: thesis: for n being Element of NAT ex r1 being Element of REAL st S₁[n,r1]

let n be Element of NAT ; :: thesis: ex r1 being Element of 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)) and
A6: x0 < r1 and
A7: r1 in dom f and
A8: f . r1 <= g1 by A3;
reconsider r1 = r1 as Element of REAL by XREAL_0:def 1;
take r1 = r1; :: thesis: S₁[n,r1]
thus S₁[n,r1] by A5, A6, A7, A8; :: thesis: verum

end;

consider s being Real_Sequence such that
A9: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A4);
A10: for n being Nat holds S₁[n,s . n]

proof

let n be Nat; :: thesis: S₁[n,s . n]
n in NAT by ORDINAL1:def 12;
hence S₁[n,s . n] by A9; :: thesis: verum

end;

A11: rng s c= (dom f) /\ (right_open_halfline x0) by A10, Th6;
A12: lim s = x0 by A10, Th6;
s is convergent by A10, Th6;
then f /* s is divergent_to+infty by A1, A12, A11;
then consider n being Nat such that
A13: for k being Nat st n <= k holds
g1 < (f /* s) . k ;
A14: g1 < (f /* s) . n by A13;
A15: n in NAT by ORDINAL1:def 12;
rng s c= dom f by A10, Th6;
then g1 < f . (s . n) by A14, FUNCT_2:108, A15;
hence contradiction by A10; :: thesis: verum

end;

assume that
A16: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom f ) and
A17: 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
g1 < f . r1 ) ) ; :: thesis: f is_right_divergent_to+infty_in x0

now :: thesis: 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

let s be Real_Sequence; :: thesis: ( s is convergent & lim s = x0 & rng s c= (dom f) /\ (right_open_halfline x0) implies f /* s is divergent_to+infty )
assume that
A18: s is convergent and
A19: lim s = x0 and
A20: rng s c= (dom f) /\ (right_open_halfline x0) ; :: thesis: f /* s is divergent_to+infty
A21: (dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;

now :: thesis: for g1 being Real ex n being Nat st
for k being Nat st n <= k holds
g1 < (f /* s) . k

let g1 be Real; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
g1 < (f /* s) . k
consider r being Real such that
A22: x0 < r and
A23: for r1 being Real st r1 < r & x0 < r1 & r1 in dom f holds
g1 < f . r1 by A17;
consider n being Nat such that
A24: for k being Nat st n <= k holds
s . k < r by A18, A19, A22, Th2;
take n = n; :: thesis: for k being Nat st n <= k holds
g1 < (f /* s) . k
let k be Nat; :: thesis: ( n <= k implies g1 < (f /* s) . k )
assume A25: n <= k ; :: thesis: g1 < (f /* s) . k
A26: s . k in rng s by VALUED_0:28;
then s . k in right_open_halfline x0 by A20, XBOOLE_0:def 4;
then s . k in { g2 where g2 is Real : x0 < g2 } by XXREAL_1:230;
then A27: ex g2 being Real st
( g2 = s . k & x0 < g2 ) ;
A28: k in NAT by ORDINAL1:def 12;
s . k in dom f by A20, A26, XBOOLE_0:def 4;
then g1 < f . (s . k) by A23, A24, A25, A27;
hence g1 < (f /* s) . k by A20, A21, FUNCT_2:108, XBOOLE_1:1, A28; :: thesis: verum

end;

hence f /* s is divergent_to+infty ; :: thesis: verum

end;

hence f is_right_divergent_to+infty_in x0 by A16; :: thesis: verum