let f be PartFunc of REAL,REAL; :: thesis: ( f is divergent_in-infty_to-infty iff ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) ) )
thus ( f is divergent_in-infty_to-infty implies ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) ) ) :: thesis: ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) implies f is divergent_in-infty_to-infty )

proof

deffunc H₁( Nat) -> object = - $1;
assume A1: f is divergent_in-infty_to-infty ; :: thesis: ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ) )
assume ( ex r being Real st
for g being Real holds
( not g < r or not g in dom f ) or ex g being Real st
for r being Real ex r1 being Real st
( r1 < r & r1 in dom f & f . r1 >= g ) ) ; :: thesis: contradiction
then consider g being Real such that
A2: for r being Real ex r1 being Real st
( r1 < r & r1 in dom f & f . r1 >= g ) by A1;
defpred S₁[ Nat, Real] means ( $2 < - $1 & $2 in dom f & g <= f . $2 );
A3: for n being Element of NAT ex r being Element of REAL st S₁[n,r]

proof

let n be Element of NAT ; :: thesis: ex r being Element of REAL st S₁[n,r]
consider r being Real such that
A4: S₁[n,r] by A2;
reconsider r = r as Real ;
S₁[n,r] by A4;
hence ex r being Element of REAL st S₁[n,r] ; :: thesis: verum

end;

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

now :: thesis: for x being object st x in rng s holds
x in dom f

let x be object ; :: thesis: ( x in rng s implies x in dom f )
assume x in rng s ; :: thesis: x in dom f
then ex n being Element of NAT st s . n = x by FUNCT_2:113;
hence x in dom f by A5; :: thesis: verum

end;

then A6: rng s c= dom f ;
consider s1 being Real_Sequence such that
A7: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();

now :: thesis: for n being Nat holds s . n <= s1 . n

let n be Nat; :: thesis: s . n <= s1 . n
A8: n in NAT by ORDINAL1:def 12;
s . n < - n by A5, A8;
hence s . n <= s1 . n by A7; :: thesis: verum

end;

then s is divergent_to-infty by A7, Th21, Th43;
then f /* s is divergent_to-infty by A1, A6;
then consider n being Nat such that
A9: for m being Nat st n <= m holds
(f /* s) . m < g ;
A10: n in NAT by ORDINAL1:def 12;
(f /* s) . n < g by A9;
then f . (s . n) < g by A6, FUNCT_2:108, A10;
hence contradiction by A5, A10; :: thesis: verum

end;

assume that
A11: for r being Real ex g being Real st
( g < r & g in dom f ) and
A12: for g being Real ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g ; :: thesis: f is divergent_in-infty_to-infty

now :: thesis: for s being Real_Sequence st s is divergent_to-infty & rng s c= dom f holds
f /* s is divergent_to-infty

let s be Real_Sequence; :: thesis: ( s is divergent_to-infty & rng s c= dom f implies f /* s is divergent_to-infty )
assume that
A13: s is divergent_to-infty and
A14: rng s c= dom f ; :: thesis: f /* s is divergent_to-infty

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

let g be Real; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(f /* s) . m < g
consider r being Real such that
A15: for r1 being Real st r1 < r & r1 in dom f holds
f . r1 < g by A12;
consider n being Nat such that
A16: for m being Nat st n <= m holds
s . m < r by A13;
take n = n; :: thesis: for m being Nat st n <= m holds
(f /* s) . m < g
let m be Nat; :: thesis: ( n <= m implies (f /* s) . m < g )
A17: s . m in rng s by VALUED_0:28;
A18: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: (f /* s) . m < g
then f . (s . m) < g by A14, A15, A16, A17;
hence (f /* s) . m < g by A14, FUNCT_2:108, A18; :: thesis: verum

end;

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

end;

hence f is divergent_in-infty_to-infty by A11; :: thesis: verum