let f be PartFunc of REAL,REAL; :: thesis: for g being Real st f is convergent_in-infty holds
( lim_in-infty f = g iff 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
|.((f . r1) - g).| < g1 )
let g be Real; :: thesis: ( f is convergent_in-infty implies ( lim_in-infty f = g iff 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
|.((f . r1) - g).| < g1 ) )
assume A1: f is convergent_in-infty ; :: thesis: ( lim_in-infty f = g iff 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
|.((f . r1) - g).| < g1 )
thus ( lim_in-infty f = g implies 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
|.((f . r1) - g).| < g1 ) :: thesis: ( ( 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
|.((f . r1) - g).| < g1 ) implies lim_in-infty f = g )
proof
deffunc H1( Nat) -> object = - $1;
assume A2: lim_in-infty f = g ; :: thesis: 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
|.((f . r1) - g).| < g1
consider s1 being Real_Sequence such that
A3: for n being Nat holds s1 . n = H1(n) from SEQ_1:sch 1();
 given g1 being Real such that A4: 0 < g1 and
A5: for r being Real ex r1 being Real st
( r1 < r & r1 in dom f & |.((f . r1) - g).| >= g1 ) ; :: thesis: contradiction
defpred S1[ Nat, Real] means ( $2 < - $1 & $2 in dom f & |.((f . $2) - g).| >= g1 );
A6: for n being Element of NAT ex r being Element of REAL st S1[n,r]
proof
let n be Element of NAT ; :: thesis: ex r being Element of REAL st S1[n,r]
consider r being Real such that
A7: S1[n,r] by A5;
reconsider r = r as Real ;
S1[n,r] by A7;
hence ex r being Element of REAL st S1[n,r] ; :: thesis: verum
end;
consider s being Real_Sequence such that
A8: for n being Element of NAT holds S1[n,s . n] from FUNCT_2:sch 3(A6);
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 A8; :: thesis: verum
end;
then A9: rng s c= dom f ;
now :: thesis: for n being Nat holds s . n <= s1 . n
let n be Nat; :: thesis: s . n <= s1 . n
n in NAT by ORDINAL1:def 12;
then s . n < - n by A8;
hence s . n <= s1 . n by A3; :: thesis: verum
end;
then s is divergent_to-infty by A3, Th21, Th43;
then ( f /* s is convergent & lim (f /* s) = g ) by A1, A2, A9, Def13;
then consider n being Nat such that
A10: for m being Nat st n <= m holds
|.(((f /* s) . m) - g).| < g1 by A4, SEQ_2:def 7;
A11: n in NAT by ORDINAL1:def 12;
|.(((f /* s) . n) - g).| < g1 by A10;
then |.((f . (s . n)) - g).| < g1 by A9, FUNCT_2:108, A11;
hence contradiction by A8, A11; :: thesis: verum
end;
assume A12: 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
|.((f . r1) - g).| < g1 ; :: thesis: lim_in-infty f = g
reconsider g = g as Real ;
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
A13: s is divergent_to-infty and
A14: rng s c= dom f ; :: thesis: ( f /* s is convergent & lim (f /* s) = g )
A15: 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 A16: 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
A17: for r1 being Real st r1 < r & r1 in dom f holds
|.((f . r1) - g).| < g1 by A12, A16;
consider n being Nat such that
A18: 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).| < g1
let m be Nat; :: thesis: ( n <= m implies |.(((f /* s) . m) - g).| < g1 )
A19: s . m in rng s by VALUED_0:28;
A20: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: |.(((f /* s) . m) - g).| < g1
then |.((f . (s . m)) - g).| < g1 by A14, A17, A18, A19;
hence |.(((f /* s) . m) - g).| < g1 by A14, FUNCT_2:108, A20; :: thesis: verum
end;
hence f /* s is convergent ; :: thesis: lim (f /* s) = g
hence lim (f /* s) = g by A15, SEQ_2:def 7; :: thesis: verum
end;
hence lim_in-infty f = g by A1, Def13; :: thesis: verum