theorem Th55: :: NDIFF13:54

for S, E, F being RealNormSpace
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for Z being Subset of S st w = <:u,v:> & u is_differentiable_on Z & v is_differentiable_on Z 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):> ) )