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 )
assume A: f | Z is_differentiable_on Z ; :: thesis: f is_differentiable_on Z
A1: Z c= dom (f | Z) by A, FDIFF_1:16;
dom (f | Z) c= dom f by RELAT_1:89;
then A2: Z c= dom f by A1, XBOOLE_1:1;
for x being Real st x in Z holds
f | Z is_differentiable_in x by A, FDIFF_1:16;
hence f is_differentiable_on Z by A2, FDIFF_1:def 7; :: thesis: verum