let m, n be non zero Nat; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of m,n
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x being Element of REAL m st f is_differentiable_in x holds
diff (f,x) is LinearOperator of m,n
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies diff (f,x) is LinearOperator of m,n )
assume f is_differentiable_in x ; :: thesis: diff (f,x) is LinearOperator of m,n
then diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) by Th18;
hence diff (f,x) is LinearOperator of m,n by Th14; :: thesis: verum