( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider g = f as PartFunc of (REAL m),(REAL n) ;
reconsider y = x as Element of REAL m by REAL_NS1:def 4;
take Jacobian (g,y) ; :: thesis: ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & Jacobian (g,y) = Jacobian (g,y) )
thus ex g being PartFunc of (REAL m),(REAL n) ex y being Element of REAL m st
( g = f & y = x & Jacobian (g,y) = Jacobian (g,y) ) ; :: thesis: verum