theorem LM00: :: PDIFFEQ1:4

for f being PartFunc of REAL,REAL
for X being Subset of REAL st X is open & X c= dom f & f is_differentiable_on X holds
(f | X) `| X = f `| X