let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T

for Y being Subset of S st f is_differentiable_on Y holds

Y is open

let f be PartFunc of S,T; :: thesis: for Y being Subset of S st f is_differentiable_on Y holds

Y is open

let Y be Subset of S; :: thesis: ( f is_differentiable_on Y implies Y is open )

assume A1: f is_differentiable_on Y ; :: thesis: Y is open

for Y being Subset of S st f is_differentiable_on Y holds

Y is open

let f be PartFunc of S,T; :: thesis: for Y being Subset of S st f is_differentiable_on Y holds

Y is open

let Y be Subset of S; :: thesis: ( f is_differentiable_on Y implies Y is open )

assume A1: f is_differentiable_on Y ; :: thesis: Y is open

now :: thesis: for x0 being Point of S st x0 in Y holds

ex N being Neighbourhood of x0 st N c= Y

hence
Y is open
by Th4; :: thesis: verumex N being Neighbourhood of x0 st N c= Y

let x0 be Point of S; :: thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y )

assume x0 in Y ; :: thesis: ex N being Neighbourhood of x0 st N c= Y

then f | Y is_differentiable_in x0 by A1;

then consider N being Neighbourhood of x0 such that

A2: N c= dom (f | Y) and

ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

((f | Y) /. x) - ((f | Y) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;

take N = N; :: thesis: N c= Y

dom (f | Y) = (dom f) /\ Y by RELAT_1:61;

then dom (f | Y) c= Y by XBOOLE_1:17;

hence N c= Y by A2; :: thesis: verum

end;assume x0 in Y ; :: thesis: ex N being Neighbourhood of x0 st N c= Y

then f | Y is_differentiable_in x0 by A1;

then consider N being Neighbourhood of x0 such that

A2: N c= dom (f | Y) and

ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st

for x being Point of S st x in N holds

((f | Y) /. x) - ((f | Y) /. x0) = (L . (x - x0)) + (R /. (x - x0)) ;

take N = N; :: thesis: N c= Y

dom (f | Y) = (dom f) /\ Y by RELAT_1:61;

then dom (f | Y) c= Y by XBOOLE_1:17;

hence N c= Y by A2; :: thesis: verum