theorem Th28: :: NDIFF13:27

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 & v is_differentiable_on Z & w = <:u,v:> holds
( w is_differentiable_on Z & ( for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> ) & ( for x being Point of S st x in Z holds
for dx being Point of S holds ((w `| Z) /. x) . dx = [(((u `| Z) /. x) . dx),(((v `| Z) /. x) . dx)] ) )