let f, f1, f2 be PartFunc of REAL,REAL; ( f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1 = lim_in+infty f2 & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) ) or ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (right_open_halfline r) holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) implies ( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 ) )
assume that
A1:
f1 is convergent_in+infty
and
A2:
f2 is convergent_in+infty
and
A3:
lim_in+infty f1 = lim_in+infty f2
and
A4:
for r being Real ex g being Real st
( r < g & g in dom f )
; ( for r being Real holds
( ( not ( (dom f1) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) ) & not ( (dom f2) /\ (right_open_halfline r) c= (dom f1) /\ (right_open_halfline r) & (dom f) /\ (right_open_halfline r) c= (dom f2) /\ (right_open_halfline r) ) ) or ex g being Real st
( g in (dom f) /\ (right_open_halfline r) & not ( f1 . g <= f . g & f . g <= f2 . g ) ) ) or ( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 ) )
given r1 being Real such that A5:
( ( (dom f1) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) & (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) ) or ( (dom f2) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) & (dom f) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) ) )
and
A6:
for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
( f1 . g <= f . g & f . g <= f2 . g )
; ( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )
now ( f is convergent_in+infty & f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )per cases
( ( (dom f1) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) & (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) ) or ( (dom f2) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) & (dom f) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) ) )
by A5;
suppose A7:
(
(dom f1) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) &
(dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) )
;
( f is convergent_in+infty & f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )A8:
now for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = lim_in+infty f1 )let seq be
Real_Sequence;
( seq is divergent_to+infty & rng seq c= dom f implies ( f /* seq is convergent & lim (f /* seq) = lim_in+infty f1 ) )assume that A9:
seq is
divergent_to+infty
and A10:
rng seq c= dom f
;
( f /* seq is convergent & lim (f /* seq) = lim_in+infty f1 )consider k being
Nat such that A11:
for
n being
Nat st
k <= n holds
r1 < seq . n
by A9;
A12:
seq ^\ k is
divergent_to+infty
by A9, Th26;
then A14:
rng (seq ^\ k) c= right_open_halfline r1
;
A15:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
then
rng (seq ^\ k) c= dom f
by A10;
then A16:
rng (seq ^\ k) c= (dom f) /\ (right_open_halfline r1)
by A14, XBOOLE_1:19;
then A17:
rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline r1)
by A7;
then A18:
rng (seq ^\ k) c= (dom f2) /\ (right_open_halfline r1)
by A7;
A19:
(dom f2) /\ (right_open_halfline r1) c= dom f2
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f2
by A18;
then A20:
(
f2 /* (seq ^\ k) is
convergent &
lim (f2 /* (seq ^\ k)) = lim_in+infty f1 )
by A2, A3, A12, Def12;
A21:
(dom f1) /\ (right_open_halfline r1) c= dom f1
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f1
by A17;
then A22:
(
f1 /* (seq ^\ k) is
convergent &
lim (f1 /* (seq ^\ k)) = lim_in+infty f1 )
by A1, A12, Def12;
A23:
now for n being Nat holds
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )let n be
Nat;
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )A24:
n in NAT
by ORDINAL1:def 12;
A25:
(seq ^\ k) . n in rng (seq ^\ k)
by VALUED_0:28;
then
f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n)
by A6, A16;
then A26:
(f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n)
by A10, A15, FUNCT_2:108, XBOOLE_1:1, A24;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n)
by A6, A16, A25;
then
f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n
by A10, A15, FUNCT_2:108, A24, XBOOLE_1:1;
hence
(
(f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n &
(f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
by A17, A21, A18, A19, A26, FUNCT_2:108, XBOOLE_1:1, A24;
verum end; A27:
f /* (seq ^\ k) = (f /* seq) ^\ k
by A10, VALUED_0:27;
then A28:
(f /* seq) ^\ k is
convergent
by A22, A20, A23, SEQ_2:19;
hence
f /* seq is
convergent
by SEQ_4:21;
lim (f /* seq) = lim_in+infty f1
lim ((f /* seq) ^\ k) = lim_in+infty f1
by A22, A20, A23, A27, SEQ_2:20;
hence
lim (f /* seq) = lim_in+infty f1
by A28, SEQ_4:20, SEQ_4:21;
verum end; hence
f is
convergent_in+infty
by A4;
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )hence
(
f is
convergent_in+infty &
lim_in+infty f = lim_in+infty f1 )
by A8, Def12;
verum end; suppose A29:
(
(dom f2) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) &
(dom f) /\ (right_open_halfline r1) c= (dom f2) /\ (right_open_halfline r1) )
;
( f is convergent_in+infty & f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )A30:
now for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
( f /* seq is convergent & lim (f /* seq) = lim_in+infty f1 )let seq be
Real_Sequence;
( seq is divergent_to+infty & rng seq c= dom f implies ( f /* seq is convergent & lim (f /* seq) = lim_in+infty f1 ) )assume that A31:
seq is
divergent_to+infty
and A32:
rng seq c= dom f
;
( f /* seq is convergent & lim (f /* seq) = lim_in+infty f1 )consider k being
Nat such that A33:
for
n being
Nat st
k <= n holds
r1 < seq . n
by A31;
A34:
seq ^\ k is
divergent_to+infty
by A31, Th26;
then A36:
rng (seq ^\ k) c= right_open_halfline r1
;
A37:
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
then
rng (seq ^\ k) c= dom f
by A32;
then A38:
rng (seq ^\ k) c= (dom f) /\ (right_open_halfline r1)
by A36, XBOOLE_1:19;
then A39:
rng (seq ^\ k) c= (dom f2) /\ (right_open_halfline r1)
by A29;
then A40:
rng (seq ^\ k) c= (dom f1) /\ (right_open_halfline r1)
by A29;
A41:
(dom f1) /\ (right_open_halfline r1) c= dom f1
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f1
by A40;
then A42:
(
f1 /* (seq ^\ k) is
convergent &
lim (f1 /* (seq ^\ k)) = lim_in+infty f1 )
by A1, A34, Def12;
A43:
(dom f2) /\ (right_open_halfline r1) c= dom f2
by XBOOLE_1:17;
then
rng (seq ^\ k) c= dom f2
by A39;
then A44:
(
f2 /* (seq ^\ k) is
convergent &
lim (f2 /* (seq ^\ k)) = lim_in+infty f1 )
by A2, A3, A34, Def12;
A45:
now for n being Nat holds
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )let n be
Nat;
( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )A46:
n in NAT
by ORDINAL1:def 12;
A47:
(seq ^\ k) . n in rng (seq ^\ k)
by VALUED_0:28;
then
f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n)
by A6, A38;
then A48:
(f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n)
by A32, A37, FUNCT_2:108, XBOOLE_1:1, A46;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n)
by A6, A38, A47;
then
f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n
by A32, A37, FUNCT_2:108, A46, XBOOLE_1:1;
hence
(
(f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n &
(f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
by A39, A43, A40, A41, A48, FUNCT_2:108, XBOOLE_1:1, A46;
verum end; A49:
f /* (seq ^\ k) = (f /* seq) ^\ k
by A32, VALUED_0:27;
then A50:
(f /* seq) ^\ k is
convergent
by A44, A42, A45, SEQ_2:19;
hence
f /* seq is
convergent
by SEQ_4:21;
lim (f /* seq) = lim_in+infty f1
lim ((f /* seq) ^\ k) = lim_in+infty f1
by A44, A42, A45, A49, SEQ_2:20;
hence
lim (f /* seq) = lim_in+infty f1
by A50, SEQ_4:20, SEQ_4:21;
verum end; hence
f is
convergent_in+infty
by A4;
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )hence
(
f is
convergent_in+infty &
lim_in+infty f = lim_in+infty f1 )
by A30, Def12;
verum end; end; end;
hence
( f is convergent_in+infty & lim_in+infty f = lim_in+infty f1 )
; verum