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 Point of (R_NormSpace_of_BoundedLinearOperators ((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 Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
let x be Element of REAL m; :: thesis: ( f is_differentiable_in x implies diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) )
assume f is_differentiable_in x ; :: thesis: diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n)))
then ex g being PartFunc of (REAL-NS m),(REAL-NS n) ex y being Point of (REAL-NS m) st
( f = g & x = y & diff (f,x) = diff (g,y) ) by PDIFF_1:def 8;
hence diff (f,x) is Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ; :: thesis: verum