:: deftheorem defines is_partial_differentiable_on PDIFF_9:def 5 :
for m being non zero Element of NAT
for Z being set
for i being Nat
for f being PartFunc of (REAL m),REAL holds
( f is_partial_differentiable_on Z,i iff ( Z c= dom f & ( for x being Element of REAL m st x in Z holds
f | Z is_partial_differentiable_in x,i ) ) );