theorem Th69: :: PDIFF_9:69

for m being non zero Element of NAT
for Z being Subset of (REAL m)
for i being Nat
for f being PartFunc of (REAL m),REAL
for x being Element of REAL m st Z is open & Z c= dom f & 1 <= i & i <= m & x in Z & f is_partial_differentiable_in x,i holds
( f | Z is_partial_differentiable_in x,i & partdiff (f,x,i) = partdiff ((f | Z),x,i) )