theorem Th41: :: NDIFF13:40

for S, E, F, G being RealNormSpace
for Z being Subset of S
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:] st w = <:u,v:> & u is_continuous_on Z & v is_continuous_on Z holds
w is_continuous_on Z