let f be PartFunc of REAL,REAL; :: thesis: ( f is convergent_in+infty iff ( ( for r being Real ex g being Real st
( r < g & 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 r < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) )
thus ( f is convergent_in+infty implies ( ( for r being Real ex g being Real st
( r < g & 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 r < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ) ) :: thesis: ( ( for r being Real ex g being Real st
( r < g & 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 r < r1 & r1 in dom f holds
|.((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
( r < g & 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 r < r1 & r1 in dom f holds
|.((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 ) ;
assume ( ex r being Real st
for g being Real holds
( not r < g 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
( r < r1 & r1 in dom f & |.((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
( r < r1 & r1 in dom f & |.((f . r1) - g2).| >= g ) by A1;
defpred S₁[ Nat, Real] means ( $1 < $2 & $2 in dom f & |.((f . $2) - g2).| >= g );
A5: 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
A6: S₁[n,r] by A4;
reconsider r = r as Real ;
S₁[n,r] by A6;
hence ex r being Element of REAL st S₁[n,r] ; :: thesis: verum

end;

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

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

end;

then A8: rng s c= dom f ;

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

let n be Nat; :: thesis: s1 . n <= s . n
A9: n in NAT by ORDINAL1:def 12;
then n < s . n by A7;
hence s1 . n <= s . n by FUNCT_1:18, A9; :: thesis: verum

end;

then s is divergent_to+infty by Lm5, Th20, Th42;
then ( f /* s is convergent & lim (f /* s) = g2 ) by A2, A8;
then consider n being Nat such that
A10: for m being Nat st n <= m holds
|.(((f /* s) . m) - g2).| < g by A3, SEQ_2:def 7;
A11: n in NAT by ORDINAL1:def 12;
|.(((f /* s) . n) - g2).| < g by A10;
then |.((f . (s . n)) - g2).| < g by A8, FUNCT_2:108, A11;
hence contradiction by A7, A11; :: thesis: verum

end;

assume A12: for r being Real ex g being Real st
( r < g & 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
( r < r1 & r1 in dom f & not |.((f . r1) - g).| < g1 ) ) ) or f is convergent_in+infty )
given g being Real such that A13: for g1 being Real st 0 < g1 holds
ex r being Real st
for r1 being Real st r < r1 & r1 in dom f holds
|.((f . r1) - g).| < g1 ; :: thesis: f is convergent_in+infty

now :: thesis: for s being Real_Sequence st s is divergent_to+infty & rng s c= dom f holds
( f /* s is convergent & lim (f /* s) = g )

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
A14: s is divergent_to+infty and
A15: rng s c= dom f ; :: thesis: ( f /* s is convergent & lim (f /* s) = g )

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

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

end;

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

end;

hence f is convergent_in+infty by A12; :: thesis: verum