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