let f1, f2 be PartFunc of REAL,REAL; ( 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
; ( 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 ) ) )
; lim_in+infty f1 <= lim_in+infty f2
now lim_in+infty f1 <= lim_in+infty f2per 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 ) )
;
lim_in+infty f1 <= lim_in+infty f2defpred S1[
Nat,
Real]
means ( $1
< $2 & $2
in (dom f1) /\ (right_open_halfline r) );
consider s2 being
Real_Sequence such that A9:
for
n being
Element of
NAT holds
S1[
n,
s2 . n]
from FUNCT_2:sch 3(A5);
then A11:
s2 is
divergent_to+infty
by Lm5, Th20, Th42;
A12:
rng s2 c= dom f2
then A13:
lim (f2 /* s2) = lim_in+infty f2
by A2, A11, Def12;
A14:
rng s2 c= dom f1
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;
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 ) )
;
lim_in+infty f1 <= lim_in+infty f2defpred S1[
Nat,
Real]
means ( $1
< $2 & $2
in (dom f2) /\ (right_open_halfline r) );
consider s2 being
Real_Sequence such that A24:
for
n being
Element of
NAT holds
S1[
n,
s2 . n]
from FUNCT_2:sch 3(A20);
then A26:
s2 is
divergent_to+infty
by Lm5, Th20, Th42;
A27:
rng s2 c= dom f1
then A28:
lim (f1 /* s2) = lim_in+infty f1
by A1, A26, Def12;
A29:
rng s2 c= dom f2
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;
verum end; end; end;
hence
lim_in+infty f1 <= lim_in+infty f2
; verum