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:60;
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:9;
Z c= dom (f | Z) by A2, FDIFF_1:9;
then Z c= dom f by A1;
hence f is_differentiable_on Z by A3, FDIFF_1:def 6; :: thesis: verum