theorem LM002: :: PDIFFEQ1:2

for f being PartFunc of REAL,REAL
for Z being Subset of REAL
for x0 being Real st Z is open & x0 in Z holds
( ( f is_differentiable_in x0 implies f | Z is_differentiable_in x0 ) & ( f | Z is_differentiable_in x0 implies f is_differentiable_in x0 ) & ( f is_differentiable_in x0 implies diff (f,x0) = diff ((f | Z),x0) ) )