let n be non empty Element of NAT ; :: thesis: for Z being open Subset of REAL
for f being differentiable PartFunc of REAL,(REAL n) 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,(REAL n) st Z c= dom f holds
f is_differentiable_on Z
let f be differentiable PartFunc of REAL,(REAL n); :: thesis: ( Z c= dom f implies f is_differentiable_on Z )
f is_differentiable_on dom f by Def5;
hence ( Z c= dom f implies f is_differentiable_on Z ) by Th21; :: thesis: verum