let f, f1, f2 be PartFunc of REAL,REAL; :: thesis: ( 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
( g < r & g in dom f ) ) & ex r being Real st
( ( ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) ) or ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) ) ) & ( for g being Real st g in (dom f) /\ (left_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
( g < r & g in dom f ) ; :: thesis: ( for r being Real holds
( ( not ( (dom f1) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) ) & not ( (dom f2) /\ (left_open_halfline r) c= (dom f1) /\ (left_open_halfline r) & (dom f) /\ (left_open_halfline r) c= (dom f2) /\ (left_open_halfline r) ) ) or ex g being Real st
( g in (dom f) /\ (left_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) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) & (dom f) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) ) or ( (dom f2) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) & (dom f) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) ) ) and
A6: for g being Real st g in (dom f) /\ (left_open_halfline r1) holds
( f1 . g <= f . g & f . g <= f2 . g ) ; :: thesis: ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
now :: thesis: ( f is convergent_in-infty & f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
per cases ( ( (dom f1) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) & (dom f) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) ) or ( (dom f2) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) & (dom f) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) ) ) by A5;
suppose A7: ( (dom f1) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) & (dom f) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) ) ; :: thesis: ( f is convergent_in-infty & f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
A8: now :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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
seq . n < r1 by A9;
A12: seq ^\ k is divergent_to-infty by A9, Th27;
now :: thesis: for x being object st x in rng (seq ^\ k) holds
x in left_open_halfline r1
let x be object ; :: thesis: ( x in rng (seq ^\ k) implies x in left_open_halfline r1 )
assume x in rng (seq ^\ k) ; :: thesis: x in left_open_halfline r1
then consider n being Element of NAT such that
A13: x = (seq ^\ k) . n by FUNCT_2:113;
seq . (n + k) < r1 by A11, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then x in { g where g is Real : g < r1 } by A13;
hence x in left_open_halfline r1 by XXREAL_1:229; :: thesis: verum
end;
then A14: rng (seq ^\ k) c= left_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) /\ (left_open_halfline r1) by A14, XBOOLE_1:19;
then A17: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline r1) by A7;
then A18: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline r1) by A7;
A19: (dom f2) /\ (left_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, Def13;
A21: (dom f1) /\ (left_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, Def13;
A23: now :: thesis: 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; :: thesis: ( (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; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
hence f is convergent_in-infty by A4; :: thesis: ( 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, Def13; :: thesis: verum
end;
suppose A29: ( (dom f2) /\ (left_open_halfline r1) c= (dom f1) /\ (left_open_halfline r1) & (dom f) /\ (left_open_halfline r1) c= (dom f2) /\ (left_open_halfline r1) ) ; :: thesis: ( f is convergent_in-infty & f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 )
A30: now :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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
seq . n < r1 by A31;
A34: seq ^\ k is divergent_to-infty by A31, Th27;
now :: thesis: for x being object st x in rng (seq ^\ k) holds
x in left_open_halfline r1
let x be object ; :: thesis: ( x in rng (seq ^\ k) implies x in left_open_halfline r1 )
assume x in rng (seq ^\ k) ; :: thesis: x in left_open_halfline r1
then consider n being Element of NAT such that
A35: x = (seq ^\ k) . n by FUNCT_2:113;
seq . (n + k) < r1 by A33, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then x in { g where g is Real : g < r1 } by A35;
hence x in left_open_halfline r1 by XXREAL_1:229; :: thesis: verum
end;
then A36: rng (seq ^\ k) c= left_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) /\ (left_open_halfline r1) by A36, XBOOLE_1:19;
then A39: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline r1) by A29;
then A40: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline r1) by A29;
A41: (dom f1) /\ (left_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, Def13;
A43: (dom f2) /\ (left_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, Def13;
A45: now :: thesis: 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; :: thesis: ( (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; :: thesis: 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; :: thesis: 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; :: thesis: verum
end;
hence f is convergent_in-infty by A4; :: thesis: ( 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, Def13; :: thesis: verum
end;
end;
end;
hence ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) ; :: thesis: verum