theorem :: NDIFF_4:2

for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n)
for h being PartFunc of REAL,(REAL-NS n)
for x being Real st h = f holds
( f is_differentiable_in x iff h is_differentiable_in x ) ;