per cases ) /\ (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 A2;

suppose A4: ( (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:

A5: now

let seq be Real_Sequence; :: thesis:
assume A6: ( seq is divergent_to-infty & rng seq c= dom f ) ; :: thesis:
then consider k being Element of NAT such that
A7: for n being Element of NAT st k <= n holds
seq . n < r1 by Def5;
A8: seq ^\ k is divergent_to-infty by A6, Th54;

let x be set ; :: thesis:
assume x in rng (seq ^\ k) ; :: thesis:
then consider n being Element of NAT such that
A9: x = (seq ^\ k) . n by FUNCT_2:190;
seq . (n + k) < r1 by A7, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then x in { g where g is Real : g < r1 } by A9;
hence x in left_open_halfline r1 by XXREAL_1:229; :: thesis:

end;

then A10: rng (seq ^\ k) c= left_open_halfline r1 by TARSKI:def 3;
A11: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then rng (seq ^\ k) c= dom f by A6, XBOOLE_1:1;
then A12: rng (seq ^\ k) c= (dom f) /\ (left_open_halfline r1) by A10, XBOOLE_1:19;
then A13: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline r1) by A4, XBOOLE_1:1;
A14: (dom f1) /\ (left_open_halfline r1) c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A13, XBOOLE_1:1;
then A15: ( f1 /* (seq ^\ k) is convergent & lim (f1 /* (seq ^\ k)) = lim_in-infty f1 ) by A1, A8, Def13;
A16: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline r1) by A4, A13, XBOOLE_1:1;
A17: (dom f2) /\ (left_open_halfline r1) c= dom f2 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f2 by A16, XBOOLE_1:1;
then A18: ( f2 /* (seq ^\ k) is convergent & lim (f2 /* (seq ^\ k)) = lim_in-infty f1 ) by A1, A8, Def13;

A19: now

let n be Element of NAT ; :: thesis:
(seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then ( f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) & f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n) ) by A3, A12;
then ( f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n) ) by A6, A11, FUNCT_2:185, XBOOLE_1:1;
hence ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n ) by A13, A14, A16, A17, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

A20: f /* (seq ^\ k) = (f /* seq) ^\ k by A6, VALUED_0:27;
then (f /* seq) ^\ k is convergent by A15, A18, A19, SEQ_2:33;
hence A21: f /* seq is convergent by SEQ_4:35; :: thesis:
lim ((f /* seq) ^\ k) = lim_in-infty f1 by A15, A18, A19, A20, SEQ_2:34;
hence lim (f /* seq) = lim_in-infty f1 by A21, SEQ_4:33; :: thesis:

end;

hence f is convergent_in-infty by A1, Def9; :: thesis:
hence ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) by A5, Def13; :: thesis:

end;

suppose A22: ( (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:

A23: now

let seq be Real_Sequence; :: thesis:
assume A24: ( seq is divergent_to-infty & rng seq c= dom f ) ; :: thesis:
then consider k being Element of NAT such that
A25: for n being Element of NAT st k <= n holds
seq . n < r1 by Def5;
A26: seq ^\ k is divergent_to-infty by A24, Th54;

let x be set ; :: thesis:
assume x in rng (seq ^\ k) ; :: thesis:
then consider n being Element of NAT such that
A27: x = (seq ^\ k) . n by FUNCT_2:190;
seq . (n + k) < r1 by A25, NAT_1:12;
then (seq ^\ k) . n < r1 by NAT_1:def 3;
then x in { g where g is Real : g < r1 } by A27;
hence x in left_open_halfline r1 by XXREAL_1:229; :: thesis:

end;

then A28: rng (seq ^\ k) c= left_open_halfline r1 by TARSKI:def 3;
A29: rng (seq ^\ k) c= rng seq by VALUED_0:21;
then rng (seq ^\ k) c= dom f by A24, XBOOLE_1:1;
then A30: rng (seq ^\ k) c= (dom f) /\ (left_open_halfline r1) by A28, XBOOLE_1:19;
then A31: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline r1) by A22, XBOOLE_1:1;
A32: (dom f2) /\ (left_open_halfline r1) c= dom f2 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f2 by A31, XBOOLE_1:1;
then A33: ( f2 /* (seq ^\ k) is convergent & lim (f2 /* (seq ^\ k)) = lim_in-infty f1 ) by A1, A26, Def13;
A34: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline r1) by A22, A31, XBOOLE_1:1;
A35: (dom f1) /\ (left_open_halfline r1) c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A34, XBOOLE_1:1;
then A36: ( f1 /* (seq ^\ k) is convergent & lim (f1 /* (seq ^\ k)) = lim_in-infty f1 ) by A1, A26, Def13;

A37: now

let n be Element of NAT ; :: thesis:
(seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then ( f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) & f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n) ) by A3, A30;
then ( f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n) ) by A24, A29, FUNCT_2:185, XBOOLE_1:1;
hence ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n ) by A31, A32, A34, A35, FUNCT_2:185, XBOOLE_1:1; :: thesis:

end;

A38: f /* (seq ^\ k) = (f /* seq) ^\ k by A24, VALUED_0:27;
then (f /* seq) ^\ k is convergent by A33, A36, A37, SEQ_2:33;
hence A39: f /* seq is convergent by SEQ_4:35; :: thesis:
lim ((f /* seq) ^\ k) = lim_in-infty f1 by A33, A36, A37, A38, SEQ_2:34;
hence lim (f /* seq) = lim_in-infty f1 by A39, SEQ_4:33; :: thesis:

end;

hence f is convergent_in-infty by A1, Def9; :: thesis:
hence ( f is convergent_in-infty & lim_in-infty f = lim_in-infty f1 ) by A23, Def13; :: thesis:

end;

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