let m, n be non empty Element of 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 (REAL-NS m),(REAL-NS 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 (REAL-NS m),(REAL-NS n)
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies diff f,x is LinearOperator of (REAL-NS m),(REAL-NS n) )
assume f is_differentiable_in x ; :: thesis: diff f,x is LinearOperator of (REAL-NS m),(REAL-NS n)
then diff f,x is Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)) by LMBOP1;
hence diff f,x is LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 10; :: thesis: verum