let m, n be non zero Nat; 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); 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; ( f is_differentiable_in x implies diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n) )
assume
f is_differentiable_in x
; 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 Th10;
hence
diff (f,x) is LinearOperator of (REAL-NS m),(REAL-NS n)
by LOPBAN_1:def 9; verum