theorem :: PDIFF_6:25

for m, n being non zero Nat
for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m holds
( f is_differentiable_in x0 iff ex r0 being Real st
( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ex L, R being Function of (REAL m),(REAL n) st
( L is LinearOperator of m,n & ( for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Element of REAL m
for w being Element of REAL n st z <> 0* m & |.z.| < d & w = R . z holds
(|.z.| ") * |.w.| < r ) ) ) & ( for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) )