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
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) ) )
thus ( f is divergent_in+infty_to+infty implies ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) ) ) :: thesis: ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) implies f is divergent_in+infty_to+infty )

proof

assume A1: f is divergent_in+infty_to+infty ; :: thesis: ( ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ( for g being Real ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 ) )
assume ( ex r being Real st
for g being Real holds
( not r < g or not g in dom f ) or ex g being Real st
for r being Real ex r1 being Real st
( r < r1 & r1 in dom f & g >= f . r1 ) ) ; :: thesis: contradiction
then consider g being Real such that
A2: for r being Real ex r1 being Real st
( r < r1 & r1 in dom f & g >= f . r1 ) by A1, Def7;
defpred S₁[ Element of NAT , real number ] means ( $1 < $2 & $2 in dom f & g >= f . $2 );
A3: for n being Element of NAT ex r being Real st S₁[n,r] by A2;
consider s being Real_Sequence such that
A4: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A3);

now

let x be set ; :: 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:190;
hence x in dom f by A4; :: thesis: verum

end;

then A5: rng s c= dom f by TARSKI:def 3;

now

let n be Element of NAT ; :: thesis: (incl NAT ) . n <= s . n
n < s . n by A4;
hence (incl NAT ) . n <= s . n by FUNCT_1:35; :: thesis: verum

end;

then s is divergent_to+infty by Lm4, Th47, Th69;
then f /* s is divergent_to+infty by A1, A5, Def7;
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
g < (f /* s) . m by Def4;
g < (f /* s) . n by A6;
then g < f . (s . n) by A5, FUNCT_2:185;
hence contradiction by A4; :: thesis: verum

end;

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

now

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
A9: s is divergent_to+infty and
A10: rng s c= dom f ; :: thesis: f /* s is divergent_to+infty

now

let g be Real; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
g < (f /* s) . m
consider r being Real such that
A11: for r1 being Real st r < r1 & r1 in dom f holds
g < f . r1 by A8;
consider n being Element of NAT such that
A12: for m being Element of NAT st n <= m holds
r < s . m by A9, Def4;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
g < (f /* s) . m
let m be Element of NAT ; :: thesis: ( n <= m implies g < (f /* s) . m )
A13: s . m in rng s by VALUED_0:28;
assume n <= m ; :: thesis: g < (f /* s) . m
then g < f . (s . m) by A10, A11, A12, A13;
hence g < (f /* s) . m by A10, FUNCT_2:185; :: thesis: verum

end;

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

end;

hence f is divergent_in+infty_to+infty by A7, Def7; :: thesis: verum