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) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_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) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) & not ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_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) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_open_halfline r) holds
f1 . g <= f2 . g ) ) ) ; :: thesis: lim_in+infty f1 <= lim_in+infty f2

now

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

suppose A3: ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & ( for g being Real st g in (dom f1) /\ (right_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 ( $1 < $2 & $2 in (dom f1) /\ (right_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: ( n + (abs r) < g & g in dom f1 ) by A1, Def6;
take g = g; :: thesis: S₁[n,g]
0 <= abs r by COMPLEX1:132;
then A6: n + 0 <= n + (abs r) by XREAL_1:9;
A7: 0 <= n by NAT_1:2;
r <= abs r by ABSVALUE:11;
then 0 + r <= n + (abs r) by A7, XREAL_1:9;
then r < g by A5, XXREAL_0:2;
then g in { g2 where g2 is Real : r < g2 } ;
then g in right_open_halfline r by XXREAL_1:230;
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);

now

let n be Element of NAT ; :: thesis: (incl NAT ) . n <= s2 . n
n < s2 . n by A8;
hence (incl NAT ) . n <= s2 . n by FUNCT_1:35; :: thesis: verum

end;

then A10: s2 is divergent_to+infty by Lm7, Th47, Th69;
A11: ( lim_in+infty f1 = lim_in+infty f1 & lim_in+infty f2 = lim_in+infty f2 ) ;
A12: 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) /\ (right_open_halfline r) by A8;
hence x in dom f1 by XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

then A15: ( f2 /* s2 is convergent & lim (f2 /* s2) = lim_in+infty f2 ) by A1, A10, A11, Def12;

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 A12, FUNCT_2:185;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A14, FUNCT_2:185; :: thesis: verum

end;

hence lim_in+infty f1 <= lim_in+infty f2 by A13, A15, SEQ_2:32; :: thesis: verum

end;

suppose A16: ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & ( for g being Real st g in (dom f2) /\ (right_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 ( $1 < $2 & $2 in (dom f2) /\ (right_open_halfline r) );

A17: now

let n be Element of NAT ; :: thesis: ex g being Real st S₁[n,g]
consider g being Real such that
A18: ( n + (abs r) < g & g in dom f2 ) by A1, Def6;
take g = g; :: thesis: S₁[n,g]
0 <= abs r by COMPLEX1:132;
then A19: n + 0 <= n + (abs r) by XREAL_1:9;
A20: 0 <= n by NAT_1:2;
r <= abs r by ABSVALUE:11;
then 0 + r <= n + (abs r) by A20, XREAL_1:9;
then r < g by A18, XXREAL_0:2;
then g in { g2 where g2 is Real : r < g2 } ;
then g in right_open_halfline r by XXREAL_1:230;
hence S₁[n,g] by A18, A19, XBOOLE_0:def 4, XXREAL_0:2; :: thesis: verum

end;

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

now

let n be Element of NAT ; :: thesis: (incl NAT ) . n <= s2 . n
n < s2 . n by A21;
hence (incl NAT ) . n <= s2 . n by FUNCT_1:35; :: thesis: verum

end;

then A23: s2 is divergent_to+infty by Lm7, Th47, Th69;
A24: ( lim_in+infty f1 = lim_in+infty f1 & lim_in+infty f2 = lim_in+infty f2 ) ;
A25: 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) /\ (right_open_halfline r) by A21;
hence x in dom f2 by XBOOLE_0:def 4; :: thesis: verum

end;

then A26: ( f2 /* s2 is convergent & lim (f2 /* s2) = lim_in+infty f2 ) by A1, A23, A24, Def12;
A27: 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) /\ (right_open_halfline r) by A21;
hence x in dom f1 by A16, XBOOLE_0:def 4; :: thesis: verum

end;

then A28: ( f1 /* s2 is convergent & lim (f1 /* s2) = lim_in+infty f1 ) by A1, A23, A24, Def12;

now

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

end;

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

end;

end;

end;

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