:: deftheorem defines partdiff PDIFF_1:def 10 :
for m, n 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 partdiff (f,x,i) = diff ((f * (reproj (i,x))),((Proj (i,m)) . x));