theorem Th21: :: NDIFF_3:21

for F being RealNormSpace
for r, p being Point of F
for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F 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 ) )