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 A1: ( f1 is convergent_in-infty & 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 A2: ( ( (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 A2;

suppose 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 ) ) ; :: thesis: lim_in-infty f1 <= lim_in-infty f2

defpred S₁[ Element of NAT , real number ] means ( $2 < - $1 & $2 in (dom f1) /\ (left_open_halfline r) );

A4: now

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

end;

consider s2 being Real_Sequence such that
A8: for n being Element of NAT holds S₁[n,s2 . n] from FUNCT_2:sch 3(A4);
deffunc H₁( Element of NAT ) -> Element of REAL = - $1;
consider s1 being Real_Sequence such that
A9: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();

now

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

end;

then A11: s2 is divergent_to-infty by A9, Th48, Th70;
A12: ( lim_in-infty f1 = lim_in-infty f1 & lim_in-infty f2 = lim_in-infty f2 ) ;
A13: 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 A8;
hence x in dom f1 by XBOOLE_0:def 4; :: thesis: verum

end;

then A14: ( f1 /* s2 is convergent & lim (f1 /* s2) = lim_in-infty f1 ) by A1, A11, A12, Def13;
A15: 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 A8;
hence x in dom f2 by A3, XBOOLE_0:def 4; :: thesis: verum

end;

then A16: ( f2 /* s2 is convergent & lim (f2 /* s2) = lim_in-infty f2 ) by A1, A11, A12, Def13;

now

let n be Element of NAT ; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
f1 . (s2 . n) <= f2 . (s2 . n) by A3, A8;
then (f1 /* s2) . n <= f2 . (s2 . n) by A13, FUNCT_2:185;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A15, FUNCT_2:185; :: thesis: verum

end;

hence lim_in-infty f1 <= lim_in-infty f2 by A14, A16, SEQ_2:32; :: thesis: verum

end;

suppose A17: ( (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

defpred S₁[ Element of NAT , real number ] means ( $2 < - $1 & $2 in (dom f2) /\ (left_open_halfline r) );

A18: now

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

end;

consider s2 being Real_Sequence such that
A22: for n being Element of NAT holds S₁[n,s2 . n] from FUNCT_2:sch 3(A18);
deffunc H₁( Element of NAT ) -> Element of REAL = - $1;
consider s1 being Real_Sequence such that
A23: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();

now

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

end;

then A25: s2 is divergent_to-infty by A23, Th48, Th70;
A26: ( lim_in-infty f1 = lim_in-infty f1 & lim_in-infty f2 = lim_in-infty f2 ) ;
A27: 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 A22;
hence x in dom f2 by XBOOLE_0:def 4; :: thesis: verum

end;

then A28: ( f2 /* s2 is convergent & lim (f2 /* s2) = lim_in-infty f2 ) by A1, A25, A26, Def13;
A29: 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 A22;
hence x in dom f1 by A17, XBOOLE_0:def 4; :: thesis: verum

end;

then A30: ( f1 /* s2 is convergent & lim (f1 /* s2) = lim_in-infty f1 ) by A1, A25, A26, Def13;

now

let n be Element of NAT ; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
f1 . (s2 . n) <= f2 . (s2 . n) by A17, A22;
then (f1 /* s2) . n <= f2 . (s2 . n) by A29, FUNCT_2:185;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A27, FUNCT_2:185; :: thesis: verum

end;

hence lim_in-infty f1 <= lim_in-infty f2 by A28, A30, SEQ_2:32; :: thesis: verum

end;

end;

end;

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