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

proof

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

A4: now

let n be Element of NAT ; :: thesis: ex g2 being Real st S₁[n,g2]
x0 - (1 / (n + 1)) < x0 by Lm3;
then consider g2 being Real such that
A5: x0 - (1 / (n + 1)) < g2 and
A6: g2 < x0 and
A7: g2 in dom f and
A8: g1 <= f . g2 by A3;
take g2 = g2; :: thesis: S₁[n,g2]
thus S₁[n,g2] 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: rng s c= (dom f) /\ (left_open_halfline x0) by A9, Th5;
A11: lim s = x0 by A9, Th5;
s is convergent by A9, Th5;
then f /* s is divergent_to-infty by A1, A11, A10, Def3;
then consider n being Element of NAT such that
A12: for k being Element of NAT st n <= k holds
(f /* s) . k < g1 by LIMFUNC1:def 5;
A13: (f /* s) . n < g1 by A12;
rng s c= dom f by A9, Th5;
then f . (s . n) < g1 by A13, FUNCT_2:108;
hence contradiction by A9; :: thesis: verum

end;

assume that
A14: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) and
A15: for g1 being Real ex r being Real st
( r < x0 & ( for r1 being Real st r < r1 & r1 < x0 & r1 in dom f holds
f . r1 < g1 ) ) ; :: thesis: f is_left_divergent_to-infty_in x0

now

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

now

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

end;

hence f /* s is divergent_to-infty by LIMFUNC1:def 5; :: thesis: verum

end;

hence f is_left_divergent_to-infty_in x0 by A14, Def3; :: thesis: verum