theorem Th54: :: NDIFF13:53

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 x being Point of S st w = <:u,v:> & u is_differentiable_in x & v is_differentiable_in x holds
( w is_differentiable_in x & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> )