theorem Th19: :: NDIFF13:18

for E, F, G being RealNormSpace
for Z being Subset of E
for T being Subset of F
for u being PartFunc of E,F
for v being PartFunc of F,G st u .: Z c= T & u is_differentiable_on Z & v is_differentiable_on T holds
( v * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((v * u) `| Z) /. x = ((v `| T) /. (u /. x)) * ((u `| Z) /. x) ) )