theorem :: PDIFF_1:19

for n being non zero Nat
for i being Nat
for g being PartFunc of (REAL n),REAL
for y being Element of REAL n
for g1 being PartFunc of (REAL n),(REAL 1) st g1 = <>* g & g1 is_partial_differentiable_in y,i holds
partdiff (g1,y,i) = <*(partdiff (g,y,i))*>