for f being PartFunc of REAL,REAL
for X being Subset of REAL st X is open & X c= dom f holds
( f is_differentiable_on X iff f | X is_differentiable_on X )