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 that
A1: f1 is convergent_in+infty and
A2: 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 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 ) ) 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 A3;

suppose A4: ( (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) );

A5: now

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

end;

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

now

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

end;

then A10: s2 is divergent_to+infty by Lm4, Th47, Th69;
A11: 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:113;
then x in (dom f1) /\ (right_open_halfline r) by A9;
hence x in dom f2 by A4, XBOOLE_0:def 4; :: thesis: verum

end;

then A12: lim (f2 /* s2) = lim_in+infty f2 by A2, A10, Def12;
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:113;
then x in (dom f1) /\ (right_open_halfline r) by A9;
hence x in dom f1 by XBOOLE_0:def 4; :: thesis: verum

end;

A14: now

let n be Element of NAT ; :: thesis: (f1 /* s2) . n <= (f2 /* s2) . n
f1 . (s2 . n) <= f2 . (s2 . n) by A4, A9;
then (f1 /* s2) . n <= f2 . (s2 . n) by A13, FUNCT_2:108;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A11, FUNCT_2:108; :: thesis: verum

end;

lim_in+infty f2 = lim_in+infty f2 ;
then A15: f2 /* s2 is convergent by A2, A10, A11, Def12;
lim_in+infty f1 = lim_in+infty f1 ;
then A16: f1 /* s2 is convergent by A1, A10, A13, Def12;
lim (f1 /* s2) = lim_in+infty f1 by A1, A10, A13, Def12;
hence lim_in+infty f1 <= lim_in+infty f2 by A16, A15, A12, A14, SEQ_2:18; :: thesis: verum

end;

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

A18: now

let n be Element of NAT ; :: thesis: ex g being Real st S₁[n,g]
0 <= abs r by COMPLEX1:46;
then A19: n + 0 <= n + (abs r) by XREAL_1:7;
consider g being Real such that
A20: n + (abs r) < g and
A21: g in dom f2 by A2, Def6;
take g = g; :: thesis: S₁[n,g]
( 0 <= n & r <= abs r ) by ABSVALUE:4, NAT_1:2;
then 0 + r <= n + (abs r) by XREAL_1:7;
then r < g by A20, 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 A20, A21, A19, 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);

now

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

end;

then A23: s2 is divergent_to+infty by Lm4, Th47, Th69;
A24: 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:113;
then x in (dom f2) /\ (right_open_halfline r) by A22;
hence x in dom f1 by A17, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

A27: 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 A24, FUNCT_2:108;
hence (f1 /* s2) . n <= (f2 /* s2) . n by A26, FUNCT_2:108; :: thesis: verum

end;

lim_in+infty f1 = lim_in+infty f1 ;
then A28: f1 /* s2 is convergent by A1, A23, A24, Def12;
lim_in+infty f2 = lim_in+infty f2 ;
then A29: f2 /* s2 is convergent by A2, A23, A26, Def12;
lim (f2 /* s2) = lim_in+infty f2 by A2, A23, A26, Def12;
hence lim_in+infty f1 <= lim_in+infty f2 by A29, A28, A25, A27, SEQ_2:18; :: thesis: verum

end;

end;

end;

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