theorem Th43: :: NDIFF13:42

for i being Nat
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 i,Z & v is_differentiable_on i,T holds
v * u is_differentiable_on i,Z