let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is convergent_in-infty & f2 is convergent_in-infty & ex r being Real st
( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) implies lim_in-infty f1 <= lim_in-infty f2 )
assume that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty ; :: thesis: ( for r being Real holds
( not ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) & not ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) or lim_in-infty f1 <= lim_in-infty f2 )
given r being Real such that A3: ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) ; :: thesis: lim_in-infty f1 <= lim_in-infty f2

now :: thesis: lim_in-infty f1 <= lim_in-infty f2

per cases ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ) by A3;

suppose A4: ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & ( for g being Real st g in (dom f1) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ; :: thesis: lim_in-infty f1 <= lim_in-infty f2

deffunc H₁( Nat) -> object = - $1;
defpred S₁[ Nat, Real] means ( $2 < - $1 & $2 in (dom f1) /\ (left_open_halfline r) );
consider s1 being Real_Sequence such that
A5: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();

A6: now :: thesis: for n being Element of NAT ex g being Element of REAL st S₁[n,g]

let n be Element of NAT ; :: thesis: ex g being Element of REAL st S₁[n,g]
0 <= |.r.| by COMPLEX1:46;
then A7: (- n) - |.r.| <= (- n) - 0 by XREAL_1:13;
consider g being Real such that
A8: g < (- n) - |.r.| and
A9: g in dom f1 by A1;
reconsider g = g as Element of REAL by XREAL_0:def 1;
take g = g; :: thesis: S₁[n,g]
( 0 <= n & - |.r.| <= r ) by ABSVALUE:4;
then (- |.r.|) - n <= r - 0 by XREAL_1:13;
then g < r by A8, XXREAL_0:2;
then g in { g2 where g2 is Real : g2 < r } ;
then g in left_open_halfline r by XXREAL_1:229;
hence S₁[n,g] by A8, A9, A7, XBOOLE_0:def 4, XXREAL_0:2; :: thesis: verum

end;

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

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

let n be Nat; :: thesis: s2 . n <= s1 . n
n in NAT by ORDINAL1:def 12;
then s2 . n < - n by A10;
hence s2 . n <= s1 . n by A5; :: thesis: verum

end;

then A11: s2 is divergent_to-infty by A5, Th21, Th43;
A12: rng s2 c= dom f2

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in rng s2 or x in dom f2 )
assume x in rng s2 ; :: thesis: x in dom f2
then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;
then x in (dom f1) /\ (left_open_halfline r) by A10;
hence x in dom f2 by A4, XBOOLE_0:def 4; :: thesis: verum

end;

then A13: lim (f2 /* s2) = lim_in-infty f2 by A2, A11, Def13;
A14: rng s2 c= dom f1

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in rng s2 or x in dom f1 )
assume x in rng s2 ; :: thesis: x in dom f1
then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;
then x in (dom f1) /\ (left_open_halfline r) by A10;
hence x in dom f1 by XBOOLE_0:def 4; :: thesis: verum

end;

A15: now :: thesis: for n being Nat holds (f1 /* s2) . n <= (f2 /* s2) . n

let n be Nat; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
A16: n in NAT by ORDINAL1:def 12;
f1 . (s2 . n) <= f2 . (s2 . n) by A4, A10, A16;
then (f1 /* s2) . n <= f2 . (s2 . n) by A14, FUNCT_2:108, A16;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A12, FUNCT_2:108, A16; :: thesis: verum

end;

A17: f2 /* s2 is convergent by A2, A11, A12;
A18: f1 /* s2 is convergent by A1, A11, A14;
lim (f1 /* s2) = lim_in-infty f1 by A1, A11, A14, Def13;
hence lim_in-infty f1 <= lim_in-infty f2 by A18, A17, A13, A15, SEQ_2:18; :: thesis: verum

end;

suppose A19: ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & ( for g being Real st g in (dom f2) /\ (left_open_halfline r) holds
f1 . g <= f2 . g ) ) ; :: thesis: lim_in-infty f1 <= lim_in-infty f2

deffunc H₁( Nat) -> object = - $1;
defpred S₁[ Nat, Real] means ( $2 < - $1 & $2 in (dom f2) /\ (left_open_halfline r) );
consider s1 being Real_Sequence such that
A20: for n being Nat holds s1 . n = H₁(n) from SEQ_1:sch 1();

A21: now :: thesis: for n being Element of NAT ex g being Element of REAL st S₁[n,g]

let n be Element of NAT ; :: thesis: ex g being Element of REAL st S₁[n,g]
0 <= |.r.| by COMPLEX1:46;
then A22: (- n) - |.r.| <= (- n) - 0 by XREAL_1:13;
consider g being Real such that
A23: g < (- n) - |.r.| and
A24: g in dom f2 by A2;
reconsider g = g as Element of REAL by XREAL_0:def 1;
take g = g; :: thesis: S₁[n,g]
( 0 <= n & - |.r.| <= r ) by ABSVALUE:4;
then (- |.r.|) - n <= r - 0 by XREAL_1:13;
then g < r by A23, XXREAL_0:2;
then g in { g2 where g2 is Real : g2 < r } ;
then g in left_open_halfline r by XXREAL_1:229;
hence S₁[n,g] by A23, A24, A22, XBOOLE_0:def 4, XXREAL_0:2; :: thesis: verum

end;

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

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

let n be Nat; :: thesis: s2 . n <= s1 . n
n in NAT by ORDINAL1:def 12;
then s2 . n < - n by A25;
hence s2 . n <= s1 . n by A20; :: thesis: verum

end;

then A26: s2 is divergent_to-infty by A20, Th21, Th43;
A27: rng s2 c= dom f1

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in rng s2 or x in dom f1 )
assume x in rng s2 ; :: thesis: x in dom f1
then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;
then x in (dom f2) /\ (left_open_halfline r) by A25;
hence x in dom f1 by A19, XBOOLE_0:def 4; :: thesis: verum

end;

then A28: lim (f1 /* s2) = lim_in-infty f1 by A1, A26, Def13;
A29: rng s2 c= dom f2

proof

let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in rng s2 or x in dom f2 )
assume x in rng s2 ; :: thesis: x in dom f2
then ex n being Element of NAT st x = s2 . n by FUNCT_2:113;
then x in (dom f2) /\ (left_open_halfline r) by A25;
hence x in dom f2 by XBOOLE_0:def 4; :: thesis: verum

end;

A30: now :: thesis: for n being Nat holds (f1 /* s2) . n <= (f2 /* s2) . n

let n be Nat; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
A31: n in NAT by ORDINAL1:def 12;
f1 . (s2 . n) <= f2 . (s2 . n) by A19, A25, A31;
then (f1 /* s2) . n <= f2 . (s2 . n) by A27, FUNCT_2:108, A31;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A29, FUNCT_2:108, A31; :: thesis: verum

end;

A32: f1 /* s2 is convergent by A1, A26, A27;
A33: f2 /* s2 is convergent by A2, A26, A29;
lim (f2 /* s2) = lim_in-infty f2 by A2, A26, A29, Def13;
hence lim_in-infty f1 <= lim_in-infty f2 by A33, A32, A28, A30, SEQ_2:18; :: thesis: verum

end;

end;

end;

hence lim_in-infty f1 <= lim_in-infty f2 ; :: thesis: verum