let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL holds
( f is_divergent_to-infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
let f be PartFunc of REAL,REAL; :: thesis: ( f is_divergent_to-infty_in x0 iff ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
f . r1 < g1 ) ) ) ) )
thus ( f is_divergent_to-infty_in x0 implies ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
f . r1 < g1 ) ) ) ) ) :: thesis: ( ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) ) & ( for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
f . r1 < g1 ) ) ) implies f is_divergent_to-infty_in x0 )

proof

assume that
A1: f is_divergent_to-infty_in x0 and
A2: ( ex r1, r2 being Real st
( r1 < x0 & x0 < r2 & ( for g1, g2 being Real holds
( not r1 < g1 or not g1 < x0 or not g1 in dom f or not g2 < r2 or not x0 < g2 or not g2 in dom f ) ) ) or ex g1 being Real st
for g2 being Real st 0 < g2 holds
ex r1 being Real st
( 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f & g1 <= f . r1 ) ) ; :: thesis: contradiction
consider g1 being Real such that
A3: for g2 being Real st 0 < g2 holds
ex r1 being Real st
( 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f & g1 <= f . r1 ) by A1, A2;
defpred S₁[ Element of NAT , Real] means ( 0 < |.(x0 - $2).| & |.(x0 - $2).| < 1 / ($1 + 1) & $2 in dom f & g1 <= f . $2 );
A4: for n being Element of NAT ex r1 being Element of REAL st S₁[n,r1]

proof

let n be Element of NAT ; :: thesis: ex r1 being Element of REAL st S₁[n,r1]
consider r1 being Real such that
A5: S₁[n,r1] by A3, XREAL_1:139;
reconsider r1 = r1 as Element of REAL by XREAL_0:def 1;
take 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: rng s c= (dom f) \ {x0} by A6, Th2;
A8: lim s = x0 by A6, Th2;
s is convergent by A6, Th2;
then f /* s is divergent_to-infty by A1, A8, A7;
then consider n being Nat such that
A9: for k being Nat st n <= k holds
(f /* s) . k < g1 ;
A10: (f /* s) . n < g1 by A9;
A11: n in NAT by ORDINAL1:def 12;
rng s c= dom f by A6, Th2;
then f . (s . n) < g1 by A10, FUNCT_2:108, A11;
hence contradiction by A6, A11; :: thesis: verum

end;

assume that
A12: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) and
A13: for g1 being Real ex g2 being Real st
( 0 < g2 & ( for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
f . r1 < g1 ) ) ; :: thesis: f is_divergent_to-infty_in x0

now :: thesis: for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {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) \ {x0} implies f /* s is divergent_to-infty )
assume that
A14: s is convergent and
A15: lim s = x0 and
A16: rng s c= (dom f) \ {x0} ; :: thesis: f /* s is divergent_to-infty

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

let g1 be Real; :: thesis: ex n being Nat st
for k being Nat st n <= k holds
(f /* s) . k < g1
consider g2 being Real such that
A17: 0 < g2 and
A18: for r1 being Real st 0 < |.(x0 - r1).| & |.(x0 - r1).| < g2 & r1 in dom f holds
f . r1 < g1 by A13;
consider n being Element of NAT such that
A19: for k being Element of NAT st n <= k holds
( 0 < |.(x0 - (s . k)).| & |.(x0 - (s . k)).| < g2 & s . k in dom f ) by A14, A15, A16, A17, Th3;
reconsider n = n as Nat ;
take n = n; :: thesis: for k being Nat st n <= k holds
(f /* s) . k < g1
let k be Nat; :: thesis: ( n <= k implies (f /* s) . k < g1 )
A20: k in NAT by ORDINAL1:def 12;
assume A21: n <= k ; :: thesis: (f /* s) . k < g1
then A22: |.(x0 - (s . k)).| < g2 by A19, A20;
A23: s . k in dom f by A19, A21, A20;
0 < |.(x0 - (s . k)).| by A19, A21, A20;
then f . (s . k) < g1 by A18, A22, A23;
hence (f /* s) . k < g1 by A16, FUNCT_2:108, XBOOLE_1:1, A20; :: thesis: verum

end;

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

end;

hence f is_divergent_to-infty_in x0 by A12; :: thesis: verum