let F be non trivial RealNormSpace; :: thesis: for Z being open Subset of REAL
for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds
f is_differentiable_on Z
let Z be open Subset of REAL; :: thesis: for f being differentiable PartFunc of REAL, the carrier of F st Z c= dom f holds
f is_differentiable_on Z
let f be differentiable PartFunc of REAL, the carrier of F; :: thesis: ( Z c= dom f implies f is_differentiable_on Z )
assume A1: Z c= dom f ; :: thesis: f is_differentiable_on Z
f is_differentiable_on dom f by Def7;
hence f is_differentiable_on Z by A1, Th24; :: thesis: verum