:: deftheorem defines diff PDIFF_7:def 2 :
for n being non zero Nat
for f being PartFunc of (REAL n),REAL
for x being Element of REAL n holds diff (f,x) = (proj (1,1)) * (diff ((<>* f),x));