theorem Th29: :: NDIFF13:28

for S, T, U being RealNormSpace
for Z being Subset of S
for u being PartFunc of S,T
for v being PartFunc of S,U
for w being PartFunc of S,[:T,U:] st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & w `| Z is_continuous_on Z )