theorem Th16: :: NDIFF13:15
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_continuous_on Z & v is_continuous_on T holds
v * u is_continuous_on Z