theorem Th27: :: NDIFF13:26

for S, T, U being RealNormSpace
for x being Point 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_in x & v is_differentiable_in x & w = <:u,v:> holds
( w is_differentiable_in x & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for dx being Point of S holds (diff (w,x)) . dx = [((diff (u,x)) . dx),((diff (v,x)) . dx)] ) )