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 :: thesis: lim_in+infty f1 <= lim_in+infty f2

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₁[ Nat, Real] means ( $1 < $2 & $2 in (dom f1) /\ (right_open_halfline r) );

A5: 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 A6: n + 0 <= n + |.r.| by XREAL_1:7;
consider g being Real such that
A7: n + |.r.| < g and
A8: 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 0 + r <= n + |.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 :: thesis: for n being Nat holds s1 . n <= s2 . n

let n be Nat; :: thesis: s1 . n <= s2 . n
A10: n in NAT by ORDINAL1:def 12;
then n < s2 . n by A9;
hence s1 . n <= s2 . n by FUNCT_1:18, A10; :: thesis: verum

end;

then A11: s2 is divergent_to+infty by Lm5, Th20, Th42;
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) /\ (right_open_halfline r) by A9;
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, Def12;
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) /\ (right_open_halfline r) by A9;
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, A9, 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, Def12;
hence lim_in+infty f1 <= lim_in+infty f2 by A18, A17, A13, A15, SEQ_2:18; :: thesis: verum

end;

suppose A19: ( (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₁[ Nat, Real] means ( $1 < $2 & $2 in (dom f2) /\ (right_open_halfline r) );

A20: 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 A21: n + 0 <= n + |.r.| by XREAL_1:7;
consider g being Real such that
A22: n + |.r.| < g and
A23: 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 0 + r <= n + |.r.| by XREAL_1:7;
then r < g by A22, 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 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 :: thesis: for n being Nat holds s1 . n <= s2 . n

let n be Nat; :: thesis: s1 . n <= s2 . n
A25: n in NAT by ORDINAL1:def 12;
then n < s2 . n by A24;
hence s1 . n <= s2 . n by FUNCT_1:18, A25; :: thesis: verum

end;

then A26: s2 is divergent_to+infty by Lm5, Th20, Th42;
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) /\ (right_open_halfline r) by A24;
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, Def12;
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) /\ (right_open_halfline r) by A24;
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, A24, 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, Def12;
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