theorem Th18: :: NDIFF_4:18

for n being non zero Element of NAT
for Z being open Subset of REAL
for f being PartFunc of REAL,(REAL n)
for r, p being Element of REAL n st Z c= dom f & ( for x being Real st x in Z holds
f /. x = (x * r) + p ) holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) . x = r ) )