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

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₁( Element of NAT ) -> Element of REAL = - $1;
defpred S₁[ Element of NAT , real number ] means ( $2 < - $1 & $2 in (dom f1) /\ (left_open_halfline r) );
consider s1 being Real_Sequence such that
A5: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();

A6: now

let n be Element of NAT ; :: thesis: ex g being Real st S₁[n,g]
0 <= abs r by COMPLEX1:132;
then A7: (- n) - (abs r) <= (- n) - 0 by XREAL_1:15;
consider g being Real such that
A8: g < (- n) - (abs r) and
A9: g in dom f1 by A1, Def9;
take g = g; :: thesis: S₁[n,g]
( 0 <= n & - (abs r) <= r ) by ABSVALUE:11, NAT_1:2;
then (- (abs r)) - n <= r - 0 by XREAL_1:15;
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

let n be Element of NAT ; :: thesis: s2 . n <= s1 . n
s2 . n < - n by A10;
hence s2 . n <= s1 . n by A5; :: thesis: verum

end;

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

proof

let x be real number ; :: 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:190;
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 number ; :: 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:190;
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

let n be Element of NAT ; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
f1 . (s2 . n) <= f2 . (s2 . n) by A4, A10;
then (f1 /* s2) . n <= f2 . (s2 . n) by A14, FUNCT_2:185;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A12, FUNCT_2:185; :: thesis: verum

end;

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

end;

suppose A18: ( (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₁( Element of NAT ) -> Element of REAL = - $1;
defpred S₁[ Element of NAT , real number ] means ( $2 < - $1 & $2 in (dom f2) /\ (left_open_halfline r) );
consider s1 being Real_Sequence such that
A19: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();

A20: now

let n be Element of NAT ; :: thesis: ex g being Real st S₁[n,g]
0 <= abs r by COMPLEX1:132;
then A21: (- n) - (abs r) <= (- n) - 0 by XREAL_1:15;
consider g being Real such that
A22: g < (- n) - (abs r) and
A23: g in dom f2 by A2, Def9;
take g = g; :: thesis: S₁[n,g]
( 0 <= n & - (abs r) <= r ) by ABSVALUE:11, NAT_1:2;
then (- (abs r)) - n <= r - 0 by XREAL_1:15;
then g < r by A22, 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 A22, A23, A21, XBOOLE_0:def 4, XXREAL_0:2; :: thesis: verum

end;

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

now

let n be Element of NAT ; :: thesis: s2 . n <= s1 . n
s2 . n < - n by A24;
hence s2 . n <= s1 . n by A19; :: thesis: verum

end;

then A25: s2 is divergent_to-infty by A19, Th48, Th70;
A26: rng s2 c= dom f1

proof

let x be real number ; :: 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:190;
then x in (dom f2) /\ (left_open_halfline r) by A24;
hence x in dom f1 by A18, XBOOLE_0:def 4; :: thesis: verum

end;

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

proof

let x be real number ; :: 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:190;
then x in (dom f2) /\ (left_open_halfline r) by A24;
hence x in dom f2 by XBOOLE_0:def 4; :: thesis: verum

end;

A29: now

let n be Element of NAT ; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
f1 . (s2 . n) <= f2 . (s2 . n) by A18, A24;
then (f1 /* s2) . n <= f2 . (s2 . n) by A26, FUNCT_2:185;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A28, FUNCT_2:185; :: thesis: verum

end;

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

end;

end;

end;

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