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

proof

assume A1: f is convergent_in-infty ; :: thesis: ( ( for r being Real ex g being Real st
( g < r & g in dom f ) ) & ex g being Real st
for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 )
then consider g2 being Real such that
A2: for seq being Real_Sequence st seq is divergent_to-infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = g2 ) by Def9;
assume ( ex r being Real st
for g being Real holds
( not g < r or not g in dom f ) or for g being Real ex g1 being Real st
( 0 < g1 & ( for r being Real ex r1 being Real st
( r1 < r & r1 in dom f & abs ((f . r1) - g) >= g1 ) ) ) ) ; :: thesis: contradiction
then consider g being Real such that
A3: 0 < g and
A4: for r being Real ex r1 being Real st
( r1 < r & r1 in dom f & abs ((f . r1) - g2) >= g ) by A1, Def9;
defpred S₁[ Element of NAT , real number ] means ( $2 < - $1 & $2 in dom f & abs ((f . $2) - g2) >= g );
A5: for n being Element of NAT ex r being Real st S₁[n,r] by A4;
consider s being Real_Sequence such that
A6: for n being Element of NAT holds S₁[n,s . n] from FUNCT_2:sch 3(A5);

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 A6; :: thesis: verum

end;

then A7: rng s c= dom f by TARSKI:def 3;
deffunc H₁( Element of NAT ) -> Element of REAL = - $1;
consider s1 being Real_Sequence such that
A8: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();

now

let n be Element of NAT ; :: thesis: s . n <= s1 . n
s . n < - n by A6;
hence s . n <= s1 . n by A8; :: thesis: verum

end;

then s is divergent_to-infty by A8, Th48, Th70;
then ( f /* s is convergent & lim (f /* s) = g2 ) by A2, A7;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs (((f /* s) . m) - g2) < g by A3, SEQ_2:def 7;
abs (((f /* s) . n) - g2) < g by A9;
then abs ((f . (s . n)) - g2) < g by A7, FUNCT_2:185;
hence contradiction by A6; :: thesis: verum

end;

assume A10: for r being Real ex g being Real st
( g < r & g in dom f ) ; :: thesis: ( for g being Real ex g1 being Real st
( 0 < g1 & ( for r being Real ex r1 being Real st
( r1 < r & r1 in dom f & not abs ((f . r1) - g) < g1 ) ) ) or f is convergent_in-infty )
given g being Real such that A11: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 ; :: thesis: f is convergent_in-infty

now

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

A14: now

let g1 be real number ; :: thesis: ( 0 < g1 implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* s) . m) - g) < g1 )
assume A15: 0 < g1 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((f /* s) . m) - g) < g1
g1 is Real by XREAL_0:def 1;
then consider r being Real such that
A16: for r1 being Real st r1 < r & r1 in dom f holds
abs ((f . r1) - g) < g1 by A11, A15;
consider n being Element of NAT such that
A17: for m being Element of NAT st n <= m holds
s . m < r by A12, Def5;
take n = n; :: thesis: for m being Element of NAT st n <= m holds
abs (((f /* s) . m) - g) < g1
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((f /* s) . m) - g) < g1 )
A18: s . m in rng s by VALUED_0:28;
assume n <= m ; :: thesis: abs (((f /* s) . m) - g) < g1
then abs ((f . (s . m)) - g) < g1 by A13, A16, A17, A18;
hence abs (((f /* s) . m) - g) < g1 by A13, FUNCT_2:185; :: thesis: verum

end;

hence f /* s is convergent by SEQ_2:def 6; :: thesis: lim (f /* s) = g
hence lim (f /* s) = g by A14, SEQ_2:def 7; :: thesis: verum

end;

hence f is convergent_in-infty by A10, Def9; :: thesis: verum