theorem DIFF2: :: PDIFFEQ1:6

for f being PartFunc of REAL,REAL
for Z being Subset of REAL st Z c= dom f & Z is open & f is_differentiable_on 2,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z & f `| Z is_differentiable_on Z & (diff (f,Z)) . 2 = (f `| Z) `| Z )