let f1, f2, f 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

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

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 Element of NAT such that
A11: for n being Element of NAT st k <= n holds
seq . n < r1 by A9, Def5;
A12: seq ^\ k is divergent_to-infty by A9, Th54;

now

let x be set ; :: 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 by TARSKI:def 3;
A15: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then rng (seq ^\ k) c= dom f by A10, XBOOLE_1:1;
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, XBOOLE_1:1;
then A18: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline r1) by A7, XBOOLE_1:1;
A19: (dom f2) /\ (left_open_halfline r1) c= dom f2 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f2 by A18, XBOOLE_1:1;
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, XBOOLE_1:1;
then A22: ( f1 /* (seq ^\ k) is convergent & lim (f1 /* (seq ^\ k)) = lim_in-infty f1 ) by A1, A3, A12, Def13;

A23: now

let n be Element of NAT ; :: thesis: ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
A24: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n) by A6, A16;
then A25: (f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n) by A10, A15, FUNCT_2:108, XBOOLE_1:1;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) by A6, A16, A24;
then f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n by A10, A15, FUNCT_2:108, 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, A25, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum

end;

A26: f /* (seq ^\ k) = (f /* seq) ^\ k by A10, VALUED_0:27;
then A27: (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, A26, SEQ_2:20;
hence lim (f /* seq) = lim_in-infty f1 by A27, SEQ_4:20, SEQ_4:21; :: thesis: verum

end;

hence f is convergent_in-infty by A4, Def9; :: 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 A28: ( (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 )

A29: now

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
A30: seq is divergent_to-infty and
A31: rng seq c= dom f ; :: thesis: ( f /* seq is convergent & lim (f /* seq) = lim_in-infty f1 )
consider k being Element of NAT such that
A32: for n being Element of NAT st k <= n holds
seq . n < r1 by A30, Def5;
A33: seq ^\ k is divergent_to-infty by A30, Th54;

now

let x be set ; :: 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
A34: x = (seq ^\ k) . n by FUNCT_2:113;
seq . (n + k) < r1 by A32, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then x in { g where g is Real : g < r1 } by A34;
hence x in left_open_halfline r1 by XXREAL_1:229; :: thesis: verum

end;

then A35: rng (seq ^\ k) c= left_open_halfline r1 by TARSKI:def 3;
A36: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then rng (seq ^\ k) c= dom f by A31, XBOOLE_1:1;
then A37: rng (seq ^\ k) c= (dom f) /\ (left_open_halfline r1) by A35, XBOOLE_1:19;
then A38: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline r1) by A28, XBOOLE_1:1;
then A39: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline r1) by A28, XBOOLE_1:1;
A40: (dom f1) /\ (left_open_halfline r1) c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A39, XBOOLE_1:1;
then A41: ( f1 /* (seq ^\ k) is convergent & lim (f1 /* (seq ^\ k)) = lim_in-infty f1 ) by A1, A3, A33, Def13;
A42: (dom f2) /\ (left_open_halfline r1) c= dom f2 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f2 by A38, XBOOLE_1:1;
then A43: ( f2 /* (seq ^\ k) is convergent & lim (f2 /* (seq ^\ k)) = lim_in-infty f1 ) by A2, A3, A33, Def13;

A44: now

let n be Element of NAT ; :: thesis: ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
A45: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n) by A6, A37;
then A46: (f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n) by A31, A36, FUNCT_2:108, XBOOLE_1:1;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) by A6, A37, A45;
then f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n by A31, A36, FUNCT_2:108, XBOOLE_1:1;
hence ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n ) by A38, A42, A39, A40, A46, FUNCT_2:108, XBOOLE_1:1; :: thesis: verum

end;

A47: f /* (seq ^\ k) = (f /* seq) ^\ k by A31, VALUED_0:27;
then A48: (f /* seq) ^\ k is convergent by A43, A41, A44, 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 A43, A41, A44, A47, SEQ_2:20;
hence lim (f /* seq) = lim_in-infty f1 by A48, SEQ_4:20, SEQ_4:21; :: thesis: verum

end;

hence f is convergent_in-infty by A4, Def9; :: 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 A29, Def13; :: thesis: verum

end;

end;

end;

hence ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) ; :: thesis: verum