theorem Th15: :: PDIFF_1:15

for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL-NS n),(REAL-NS 1)
for g being PartFunc of (REAL n),REAL
for x being Point of (REAL-NS n)
for y being Element of REAL n st f = <>* g & x = y & f is_partial_differentiable_in x,i holds
(partdiff (f,x,i)) . <*1*> = <*(partdiff (g,y,i))*>