:: deftheorem defines partdiff PDIFF_1:def 18 :
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 partdiff (h,z,i,j) = diff ((((proj (j,n)) * h) * (reproj (i,z))),((proj (i,m)) . z));