let x0 be Real; :: thesis: for f, f1, f2 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) & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )
let f, f1, f2 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) & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) 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) ; :: thesis: ( for r being Real holds
( not 0 < r or not ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) or ex g being Real st
( g in ].(x0 - r),x0.[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) ) or ( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) ) )
given r being Real such that A4: 0 < r and
A5: ].(x0 - r),x0.[ c= ((dom f1) /\ (dom f2)) /\ (dom f) and
A6: for g being Real st g in ].(x0 - r),x0.[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ; :: thesis: ( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) )
((dom f1) /\ (dom f2)) /\ (dom f) c= (dom f1) /\ (dom f2) by XBOOLE_1:17;
then A7: ].(x0 - r),x0.[ c= (dom f1) /\ (dom f2) by A5, XBOOLE_1:1;
A8: ((dom f1) /\ (dom f2)) /\ (dom f) c= dom f by XBOOLE_1:17;
then A9: ].(x0 - r),x0.[ c= dom f by A5, XBOOLE_1:1;
A10: now :: thesis: for r1 being Real st r1 < x0 holds
ex g being Real st
( r1 < g & g < x0 & g in dom f )
let r1 be Real; :: thesis: ( r1 < x0 implies ex g being Real st
( r1 < g & g < x0 & g in dom f ) )
assume A11: r1 < x0 ; :: thesis: ex g being Real st
( r1 < g & g < x0 & g in dom f )
now :: thesis: ex g being Real st
( r1 < g & g < x0 & g in dom f )
per cases ( r1 <= x0 - r or x0 - r <= r1 ) ;
suppose A12: r1 <= x0 - r ; :: thesis: ex g being Real st
( r1 < g & g < x0 & g in dom f )
now :: thesis: ex g being Real st
( r1 < g & g < x0 & g in dom f )
x0 - r < x0 by A4, Lm1;
then consider g being Real such that
A13: x0 - r < g and
A14: g < x0 by XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( r1 < g & g < x0 & g in dom f )
thus ( r1 < g & g < x0 ) by A12, A13, A14, XXREAL_0:2; :: thesis: g in dom f
g in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A13, A14;
then g in ].(x0 - r),x0.[ by RCOMP_1:def 2;
hence g in dom f by A9; :: thesis: verum
end;
hence ex g being Real st
( r1 < g & g < x0 & g in dom f ) ; :: thesis: verum
end;
suppose A15: x0 - r <= r1 ; :: thesis: ex g being Real st
( r1 < g & g < x0 & g in dom f )
now :: thesis: ex g being Real st
( r1 < g & g < x0 & g in dom f )
consider g being Real such that
A16: r1 < g and
A17: g < x0 by A11, XREAL_1:5;
reconsider g = g as Real ;
take g = g; :: thesis: ( r1 < g & g < x0 & g in dom f )
thus ( r1 < g & g < x0 ) by A16, A17; :: thesis: g in dom f
x0 - r < g by A15, A16, XXREAL_0:2;
then g in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) } by A17;
then g in ].(x0 - r),x0.[ by RCOMP_1:def 2;
hence g in dom f by A9; :: thesis: verum
end;
hence ex g being Real st
( r1 < g & g < x0 & g in dom f ) ; :: thesis: verum
end;
end;
end;
hence ex g being Real st
( r1 < g & g < x0 & g in dom f ) ; :: thesis: verum
end;
(dom f1) /\ (dom f2) c= dom f2 by XBOOLE_1:17;
then A18: (dom f2) /\ ].(x0 - r),x0.[ = ].(x0 - r),x0.[ by A7, XBOOLE_1:1, XBOOLE_1:28;
(dom f1) /\ (dom f2) c= dom f1 by XBOOLE_1:17;
then A19: (dom f1) /\ ].(x0 - r),x0.[ = ].(x0 - r),x0.[ by A7, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ ].(x0 - r),x0.[ = ].(x0 - r),x0.[ by A5, A8, XBOOLE_1:1, XBOOLE_1:28;
hence ( f is_left_convergent_in x0 & lim_left (f,x0) = lim_left (f1,x0) ) by A1, A2, A3, A4, A6, A19, A18, A10, Th63; :: thesis: verum