let Z be open Subset of REAL ; :: thesis: for f being PartFunc of REAL ,REAL st f | Z is_differentiable_on Z holds
f is_differentiable_on Z
let f be PartFunc of REAL ,REAL ; :: thesis: ( f | Z is_differentiable_on Z implies f is_differentiable_on Z )
A1: dom (f | Z) c= dom f by RELAT_1:89;
assume A2: f | Z is_differentiable_on Z ; :: thesis: f is_differentiable_on Z
then A3: for x being Real st x in Z holds
f | Z is_differentiable_in x by FDIFF_1:16;
Z c= dom (f | Z) by A2, FDIFF_1:16;
then Z c= dom f by A1, XBOOLE_1:1;
hence f is_differentiable_on Z by A3, FDIFF_1:def 7; :: thesis: verum