:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 9 :
for n, m being non zero Nat
for i 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 iff f * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x );