let x0, r be Real; :: thesis: for f being PartFunc of REAL ,REAL st f . x0 <> r & f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f . x0 <> r & f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) )
assume A1: ( f . x0 <> r & f is_differentiable_in x0 ) ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) )
then A2: ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LINEAR ex R being REST st
for r being Real st r in N holds
(f . r) - (f . x0) = (L . (r - x0)) + (R . (r - x0)) ) by FDIFF_1:def 5;
f is_continuous_in x0 by A1, FDIFF_1:32;
hence ex N being Neighbourhood of x0 st
( N c= dom f & ( for g being Real st g in N holds
f . g <> r ) ) by A1, A2, FCONT_3:15; :: thesis: verum