:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 15 :
for m, n being non zero Nat
for i, j being Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) holds
( f is_partial_differentiable_in x,i,j iff ((Proj (j,n)) * f) * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );