let m be non zero Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS m)
for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real )
let f be PartFunc of (REAL-NS m),(REAL-NS m); :: thesis: for x being Point of (REAL-NS m) st f is_differentiable_in x holds
( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real )
let x be Point of (REAL-NS m); :: thesis: ( f is_differentiable_in x implies ( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real ) )
( Det (Jacobian (f,x)) is unital iff not Det (Jacobian (f,x)) is zero ) ;
then A1: ( Det (Jacobian (f,x)) is unital iff Det (Jacobian (f,x)) <> 0. F_Real ) by STRUCT_0:def 12;
assume f is_differentiable_in x ; :: thesis: ( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real )
then ( diff (f,x) is invertible iff Jacobian (f,x) is invertible ) by Th30;
hence ( diff (f,x) is invertible iff Det (Jacobian (f,x)) <> 0. F_Real ) by A1, LAPLACE:34; :: thesis: verum