:: deftheorem Def2 defines Jacobian NDIFF11:def 2 :
for m, n being non zero Nat
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m)
for b₅ being Matrix of m,n,F_Real holds
( b₅ = Jacobian (f,x) iff ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & b₅ = Jacobian (g,y) ) );