theorem Th57: :: NDIFF13:56

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 & w `| Z = (CTP (S,(diff_SP (0,S,E)),(diff_SP (0,S,F)))) * <:(u `| Z),(v `| Z):> )