let x0 be Real; for f, f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f1,x0) = lim (f2,x0) & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) holds
( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
let f, f1, f2 be PartFunc of REAL,REAL; ( f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f1,x0) = lim (f2,x0) & ex r being Real st
( 0 < r & ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) & ( for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g ) ) ) implies ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) )
assume that
A1:
f1 is_convergent_in x0
and
A2:
f2 is_convergent_in x0
and
A3:
lim (f1,x0) = lim (f2,x0)
; ( for r being Real holds
( not 0 < r or not ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f) or ex g being Real st
( g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ & not ( f1 . g <= f . g & f . g <= f2 . g ) ) ) or ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) ) )
given r being Real such that A4:
0 < r
and
A5:
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= ((dom f1) /\ (dom f2)) /\ (dom f)
and
A6:
for g being Real st g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ holds
( f1 . g <= f . g & f . g <= f2 . g )
; ( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
A7:
(dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
by A5, XBOOLE_1:18, XBOOLE_1:28;
A8:
].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ c= (dom f1) /\ (dom f2)
by A5, XBOOLE_1:18;
then A9:
(dom f1) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
by XBOOLE_1:18, XBOOLE_1:28;
A10:
(dom f2) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) = ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[
by A8, XBOOLE_1:18, XBOOLE_1:28;
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )
by A4, A5, Th5, XBOOLE_1:18;
hence
( f is_convergent_in x0 & lim (f,x0) = lim (f1,x0) )
by A1, A2, A3, A4, A6, A7, A9, A10, Th41; verum