:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 17 :
for m, n being non zero Nat
for i, j being Nat
for h being PartFunc of (REAL m),(REAL n)
for z being Element of REAL m holds
( h is_partial_differentiable_in z,i,j iff ((proj (j,n)) * h) * (reproj (i,z)) is_differentiable_in (proj (i,m)) . z );