let x0 be Real; :: thesis: for f1, f2, f being PartFunc of REAL ,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left f1,x0 = lim_left f2,x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) holds
( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 )
let f1, f2, f be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left f1,x0 = lim_left f2,x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ) & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) & ( ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) or ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) implies ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 ) )
assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: lim_left f1,x0 = lim_left f2,x0 and
A4: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom f ) ; :: thesis: ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].(x0 - r),x0.[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) or ( not ( (dom f1) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ ) & not ( (dom f2) /\ ].(x0 - r),x0.[ c= (dom f1) /\ ].(x0 - r),x0.[ & (dom f) /\ ].(x0 - r),x0.[ c= (dom f2) /\ ].(x0 - r),x0.[ ) ) ) or ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 ) )
given r1 being Real such that A5: 0 < r1 and
A6: for g being Real st g in (dom f) /\ ].(x0 - r1),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) and
A7: ( ( (dom f1) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ ) or ( (dom f2) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ ) ) ; :: thesis: ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 )

now

per cases ( ( (dom f1) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ ) or ( (dom f2) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ ) ) by A7;

suppose A8: ( (dom f1) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ ) ; :: thesis: ( f is_left_convergent_in x0 & f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 )

A9: now

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) implies ( f /* seq is convergent & lim (f /* seq) = lim_left f1,x0 ) )
assume that
A10: seq is convergent and
A11: lim seq = x0 and
A12: rng seq c= (dom f) /\ (left_open_halfline x0) ; :: thesis: ( f /* seq is convergent & lim (f /* seq) = lim_left f1,x0 )
x0 - r1 < lim seq by A5, A11, Lm1;
then consider k being Element of NAT such that
A13: for n being Element of NAT st k <= n holds
x0 - r1 < seq . n by A10, Th1;
A14: rng (seq ^\ k) c= rng seq by VALUED_0:21;
(dom f) /\ (left_open_halfline x0) c= left_open_halfline x0 by XBOOLE_1:17;
then rng seq c= left_open_halfline x0 by A12, XBOOLE_1:1;
then A15: rng (seq ^\ k) c= left_open_halfline x0 by A14, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in rng (seq ^\ k) implies x in ].(x0 - r1),x0.[ )
assume A16: x in rng (seq ^\ k) ; :: thesis: x in ].(x0 - r1),x0.[
then consider n being Element of NAT such that
A17: x = (seq ^\ k) . n by FUNCT_2:190;
(seq ^\ k) . n in left_open_halfline x0 by A15, A16, A17;
then (seq ^\ k) . n in { g where g is Real : g < x0 } by XXREAL_1:229;
then A18: ex g being Real st
( g = (seq ^\ k) . n & g < x0 ) ;
x0 - r1 < seq . (n + k) by A13, NAT_1:12;
then x0 - r1 < (seq ^\ k) . n by NAT_1:def 3;
then x in { g1 where g1 is Real : ( x0 - r1 < g1 & g1 < x0 ) } by A17, A18;
hence x in ].(x0 - r1),x0.[ by RCOMP_1:def 2; :: thesis: verum

end;

then A19: rng (seq ^\ k) c= ].(x0 - r1),x0.[ by TARSKI:def 3;
].(x0 - r1),x0.[ c= left_open_halfline x0 by XXREAL_1:263;
then A20: rng (seq ^\ k) c= left_open_halfline x0 by A19, XBOOLE_1:1;
A21: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
then A22: rng seq c= dom f by A12, XBOOLE_1:1;
then rng (seq ^\ k) c= dom f by A14, XBOOLE_1:1;
then A23: rng (seq ^\ k) c= (dom f) /\ ].(x0 - r1),x0.[ by A19, XBOOLE_1:19;
then A24: rng (seq ^\ k) c= (dom f1) /\ ].(x0 - r1),x0.[ by A8, XBOOLE_1:1;
then A25: rng (seq ^\ k) c= (dom f2) /\ ].(x0 - r1),x0.[ by A8, XBOOLE_1:1;
A26: lim (seq ^\ k) = x0 by A10, A11, SEQ_4:33;
A27: (dom f2) /\ ].(x0 - r1),x0.[ c= dom f2 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f2 by A25, XBOOLE_1:1;
then A28: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline x0) by A20, XBOOLE_1:19;
then A29: lim (f2 /* (seq ^\ k)) = lim_left f2,x0 by A2, A10, A26, Def7;
A30: (dom f1) /\ ].(x0 - r1),x0.[ c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A24, XBOOLE_1:1;
then A31: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A20, XBOOLE_1:19;
then A32: lim (f1 /* (seq ^\ k)) = lim_left f1,x0 by A1, A10, A26, Def7;

A33: now

let n be Element of NAT ; :: thesis: ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
A34: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n) by A6, A23;
then A35: (f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n) by A14, A22, FUNCT_2:185, XBOOLE_1:1;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) by A6, A23, A34;
then f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n by A14, A22, FUNCT_2:185, XBOOLE_1:1;
hence ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n ) by A30, A27, A24, A25, A35, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

A36: f2 /* (seq ^\ k) is convergent by A2, A3, A10, A26, A28, Def7;
A37: f1 /* (seq ^\ k) is convergent by A1, A3, A10, A26, A31, Def7;
then f /* (seq ^\ k) is convergent by A3, A32, A36, A29, A33, SEQ_2:33;
then A38: (f /* seq) ^\ k is convergent by A12, A21, VALUED_0:27, XBOOLE_1:1;
hence f /* seq is convergent by SEQ_4:35; :: thesis: lim (f /* seq) = lim_left f1,x0
lim (f /* (seq ^\ k)) = lim_left f1,x0 by A3, A37, A32, A36, A29, A33, SEQ_2:34;
then lim ((f /* seq) ^\ k) = lim_left f1,x0 by A12, A21, VALUED_0:27, XBOOLE_1:1;
hence lim (f /* seq) = lim_left f1,x0 by A38, SEQ_4:36; :: thesis: verum

end;

hence f is_left_convergent_in x0 by A4, Def1; :: thesis: ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 )
hence ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 ) by A9, Def7; :: thesis: verum

end;

suppose A39: ( (dom f2) /\ ].(x0 - r1),x0.[ c= (dom f1) /\ ].(x0 - r1),x0.[ & (dom f) /\ ].(x0 - r1),x0.[ c= (dom f2) /\ ].(x0 - r1),x0.[ ) ; :: thesis: ( f is_left_convergent_in x0 & f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 )

A40: now

let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom f) /\ (left_open_halfline x0) implies ( f /* seq is convergent & lim (f /* seq) = lim_left f1,x0 ) )
assume that
A41: seq is convergent and
A42: lim seq = x0 and
A43: rng seq c= (dom f) /\ (left_open_halfline x0) ; :: thesis: ( f /* seq is convergent & lim (f /* seq) = lim_left f1,x0 )
x0 - r1 < lim seq by A5, A42, Lm1;
then consider k being Element of NAT such that
A44: for n being Element of NAT st k <= n holds
x0 - r1 < seq . n by A41, Th1;
A45: rng (seq ^\ k) c= rng seq by VALUED_0:21;
(dom f) /\ (left_open_halfline x0) c= left_open_halfline x0 by XBOOLE_1:17;
then rng seq c= left_open_halfline x0 by A43, XBOOLE_1:1;
then A46: rng (seq ^\ k) c= left_open_halfline x0 by A45, XBOOLE_1:1;

now

let x be set ; :: thesis: ( x in rng (seq ^\ k) implies x in ].(x0 - r1),x0.[ )
assume A47: x in rng (seq ^\ k) ; :: thesis: x in ].(x0 - r1),x0.[
then consider n being Element of NAT such that
A48: x = (seq ^\ k) . n by FUNCT_2:190;
(seq ^\ k) . n in left_open_halfline x0 by A46, A47, A48;
then (seq ^\ k) . n in { g where g is Real : g < x0 } by XXREAL_1:229;
then A49: ex g being Real st
( g = (seq ^\ k) . n & g < x0 ) ;
x0 - r1 < seq . (n + k) by A44, NAT_1:12;
then x0 - r1 < (seq ^\ k) . n by NAT_1:def 3;
then x in { g1 where g1 is Real : ( x0 - r1 < g1 & g1 < x0 ) } by A48, A49;
hence x in ].(x0 - r1),x0.[ by RCOMP_1:def 2; :: thesis: verum

end;

then A50: rng (seq ^\ k) c= ].(x0 - r1),x0.[ by TARSKI:def 3;
].(x0 - r1),x0.[ c= left_open_halfline x0 by XXREAL_1:263;
then A51: rng (seq ^\ k) c= left_open_halfline x0 by A50, XBOOLE_1:1;
A52: (dom f) /\ (left_open_halfline x0) c= dom f by XBOOLE_1:17;
then A53: rng seq c= dom f by A43, XBOOLE_1:1;
then rng (seq ^\ k) c= dom f by A45, XBOOLE_1:1;
then A54: rng (seq ^\ k) c= (dom f) /\ ].(x0 - r1),x0.[ by A50, XBOOLE_1:19;
then A55: rng (seq ^\ k) c= (dom f2) /\ ].(x0 - r1),x0.[ by A39, XBOOLE_1:1;
then A56: rng (seq ^\ k) c= (dom f1) /\ ].(x0 - r1),x0.[ by A39, XBOOLE_1:1;
A57: lim (seq ^\ k) = x0 by A41, A42, SEQ_4:33;
A58: (dom f2) /\ ].(x0 - r1),x0.[ c= dom f2 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f2 by A55, XBOOLE_1:1;
then A59: rng (seq ^\ k) c= (dom f2) /\ (left_open_halfline x0) by A51, XBOOLE_1:19;
then A60: lim (f2 /* (seq ^\ k)) = lim_left f2,x0 by A2, A41, A57, Def7;
A61: (dom f1) /\ ].(x0 - r1),x0.[ c= dom f1 by XBOOLE_1:17;
then rng (seq ^\ k) c= dom f1 by A56, XBOOLE_1:1;
then A62: rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline x0) by A51, XBOOLE_1:19;
then A63: lim (f1 /* (seq ^\ k)) = lim_left f1,x0 by A1, A41, A57, Def7;

A64: now

let n be Element of NAT ; :: thesis: ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n )
A65: (seq ^\ k) . n in rng (seq ^\ k) by VALUED_0:28;
then f . ((seq ^\ k) . n) <= f2 . ((seq ^\ k) . n) by A6, A54;
then A66: (f /* (seq ^\ k)) . n <= f2 . ((seq ^\ k) . n) by A45, A53, FUNCT_2:185, XBOOLE_1:1;
f1 . ((seq ^\ k) . n) <= f . ((seq ^\ k) . n) by A6, A54, A65;
then f1 . ((seq ^\ k) . n) <= (f /* (seq ^\ k)) . n by A45, A53, FUNCT_2:185, XBOOLE_1:1;
hence ( (f1 /* (seq ^\ k)) . n <= (f /* (seq ^\ k)) . n & (f /* (seq ^\ k)) . n <= (f2 /* (seq ^\ k)) . n ) by A61, A58, A55, A56, A66, FUNCT_2:185, XBOOLE_1:1; :: thesis: verum

end;

A67: f2 /* (seq ^\ k) is convergent by A2, A3, A41, A57, A59, Def7;
A68: f1 /* (seq ^\ k) is convergent by A1, A3, A41, A57, A62, Def7;
then f /* (seq ^\ k) is convergent by A3, A63, A67, A60, A64, SEQ_2:33;
then A69: (f /* seq) ^\ k is convergent by A43, A52, VALUED_0:27, XBOOLE_1:1;
hence f /* seq is convergent by SEQ_4:35; :: thesis: lim (f /* seq) = lim_left f1,x0
lim (f /* (seq ^\ k)) = lim_left f1,x0 by A3, A68, A63, A67, A60, A64, SEQ_2:34;
then lim ((f /* seq) ^\ k) = lim_left f1,x0 by A43, A52, VALUED_0:27, XBOOLE_1:1;
hence lim (f /* seq) = lim_left f1,x0 by A69, SEQ_4:36; :: thesis: verum

end;

hence f is_left_convergent_in x0 by A4, Def1; :: thesis: ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 )
hence ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 ) by A40, Def7; :: thesis: verum

end;

end;

end;

hence ( f is_left_convergent_in x0 & lim_left f,x0 = lim_left f1,x0 ) ; :: thesis: verum