let S, T be RealNormSpace; :: thesis: for Z being Subset of S
for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
Z is open
let Z be Subset of S; :: thesis: for n being Nat
for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
Z is open
let n be Nat; :: thesis: for f being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z holds
Z is open
let f be PartFunc of S,T; :: thesis: ( 1 <= n & f is_differentiable_on n,Z implies Z is open )
assume ( 1 <= n & f is_differentiable_on n,Z ) ; :: thesis: Z is open
then f is_differentiable_on 1,Z by Th17;
then ( Z c= dom f & f | Z is_differentiable_on Z ) by Th15;
hence Z is open by NDIFF_1:32; :: thesis: verum