let x0 be Real; for f, f1, f2 being PartFunc of REAL,REAL st f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ex r being Real st
( 0 < r & ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
let f, f1, f2 be PartFunc of REAL,REAL; ( f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & lim_right (f1,x0) = lim_right (f2,x0) & ex r being Real st
( 0 < r & ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) implies ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) )
assume that
A1:
f1 is_right_convergent_in x0
and
A2:
f2 is_right_convergent_in x0
and
A3:
lim_right (f1,x0) = lim_right (f2,x0)
; ( for r being Real holds
( not 0 < r or not ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) or ex g being Real st
( g in ].x0,(x0 + r).[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) ) or ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) ) )
given r being Real such that A4:
0 < r
and
A5:
].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f)
and
A6:
for g being Real st g in ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g )
; ( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
((dom f1) /\ (dom f2)) /\ (dom f) c= (dom f1) /\ (dom f2)
by XBOOLE_1:17;
then A7:
].x0,(x0 + r).[ 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,(x0 + r).[ c= dom f
by A5, XBOOLE_1:1;
A10:
now for r1 being Real st x0 < r1 holds
ex g being Real st
( g < r1 & x0 < g & g in dom f )let r1 be
Real;
( x0 < r1 implies ex g being Real st
( g < r1 & x0 < g & g in dom f ) )assume A11:
x0 < r1
;
ex g being Real st
( g < r1 & x0 < g & g in dom f )hence
ex
g being
Real st
(
g < r1 &
x0 < g &
g in dom f )
;
verum end;
(dom f1) /\ (dom f2) c= dom f2
by XBOOLE_1:17;
then A18:
(dom f2) /\ ].x0,(x0 + r).[ = ].x0,(x0 + r).[
by A7, XBOOLE_1:1, XBOOLE_1:28;
(dom f1) /\ (dom f2) c= dom f1
by XBOOLE_1:17;
then A19:
(dom f1) /\ ].x0,(x0 + r).[ = ].x0,(x0 + r).[
by A7, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ ].x0,(x0 + r).[ = ].x0,(x0 + r).[
by A5, A8, XBOOLE_1:1, XBOOLE_1:28;
hence
( f is_right_convergent_in x0 & lim_right (f,x0) = lim_right (f1,x0) )
by A1, A2, A3, A4, A6, A19, A18, A10, Th65; verum