theorem DIFF1: :: PDIFFEQ1:5

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 1,Z holds
( f is_differentiable_on Z & (diff (f,Z)) . 1 = f `| Z )