:: deftheorem defines is_partial_differentiable_in PDIFF_1:def 11 :
for n being non zero Nat
for i being Nat
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds
( f is_partial_differentiable_in x,i iff f * (reproj (i,x)) is_differentiable_in (proj (i,n)) . x );