let Z be open Subset of REAL ; :: thesis: for f being differentiable PartFunc of REAL ,REAL st Z c= dom f holds
f is_differentiable_on Z
let f be differentiable PartFunc of REAL ,REAL ; :: 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 Def9;
hence f is_differentiable_on Z by A1, Th34; :: thesis: verum