theorem :: FDIFF_2:16

for A being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on A holds
( f | A is_differentiable_on A & f `| A = (f | A) `| A )