theorem Th23: :: NDIFF13:22

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 & u `| Z is_continuous_on Z & v is_differentiable_on T & v `| T is_continuous_on T holds
( v * u is_differentiable_on Z & (v * u) `| Z is_continuous_on Z )