let x0 be Real; :: thesis: 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; :: thesis: ( 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) ; :: thesis: ( 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 ) ; :: thesis: ( 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; :: thesis: verum