theorem :: INTEGR26:25

for X being open Subset of REAL
for x0 being Real
for f being PartFunc of REAL,REAL st x0 in X & f is_differentiable_on X holds
diff (f,x0) = diff ((f | X),x0)