theorem Th23: :: INTEGRA8:23

for f1 being PartFunc of REAL,REAL
for Z being open Subset of REAL st Z c= dom (- f1) & f1 is_differentiable_on Z holds
( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds
((- f1) `| Z) . x = - (diff (f1,x)) ) )