:: deftheorem Def1 defines Jacobian NDIFF11:def 1 :
for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m
for b₅ being Matrix of m,n,F_Real holds
( b₅ = Jacobian (f,x) iff for i, j being Nat st i in Seg m & j in Seg n holds
b₅ * (i,j) = partdiff (f,x,i,j) );