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 that
A1: f . x0 <> r and
A2: 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 ) )
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 A2, FDIFF_1:def 5;
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, FDIFF_1:32; :: thesis: verum