let m, n be non zero Nat; :: thesis:
let f be PartFunc of (REAL m),(REAL n); :: thesis:
let x0 be Element of REAL m; :: thesis:
reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) by Th1;
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;

hereby :: thesis:

assume f is_differentiable_in x0 ; :: thesis:
then g is_differentiable_in y0 by Th2;
then consider N being Neighbourhood of y0 such that
A1: ( N c= dom g & ex GL being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) ex GR being RestFunc of (REAL-NS m),(REAL-NS n) st
for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) ) by NDIFF_1:def 6;
consider GL being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))), GR being RestFunc of (REAL-NS m),(REAL-NS n) such that
A2: for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A1;
consider r0 being Real such that
A3: ( 0 < r0 & { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } c= N ) by NFCONT_1:def 1;
take r0 = r0; :: thesis:
thus 0 < r0 by A3; :: thesis:
{ y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } c= dom g by A3, A1, XBOOLE_1:1;
hence { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f by Th23; :: thesis:
A4: GR is total by NDIFF_1:def 5;
then A5: dom GR = the carrier of (REAL-NS m) by PARTFUN1:def 2;
A6: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS n) = REAL n ) by REAL_NS1:def 4;
then reconsider L = GL as Function of (REAL m),(REAL n) by LOPBAN_1:def 9;
reconsider R = GR as Function of (REAL m),(REAL n) by A6, A4;
take L = L; :: thesis:
take R = R; :: thesis:
GL is LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
hence L is LinearOperator of m,n by Th14; :: thesis:
thus 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 ) ) :: thesis:

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider d being Real such that
A7: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r ) ) by A4, NDIFF_1:23;
take d ; :: thesis:
thus d > 0 by A7; :: thesis:
let z be Element of REAL m; :: thesis:
let w be Element of REAL n; :: thesis:
assume A8: ( z <> 0* m & |.z.| < d & w = R . z ) ; :: thesis:
reconsider s = z as Element of (REAL-NS m) by REAL_NS1:def 4;
A9: s <> 0. (REAL-NS m) by A8, REAL_NS1:def 4;
||.s.|| < d by A8, REAL_NS1:1;
then (||.s.|| ") * ||.(GR /. s).|| < r by A7, A9;
then (|.z.| ") * ||.(GR /. s).|| < r by REAL_NS1:1;
hence (|.z.| ") * |.w.| < r by A5, A8, PARTFUN1:def 6, REAL_NS1:1; :: thesis:

end;

thus for x being Element of REAL m st |.(x - x0).| < r0 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) :: thesis:

proof

let x be Element of REAL m; :: thesis:
assume |.(x - x0).| < r0 ; :: thesis:
then x in { s where s is Element of REAL m : |.(s - x0).| < r0 } ;
then A10: x in { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } by Th23;
reconsider y = x as Point of (REAL-NS m) by REAL_NS1:def 4;
A11: (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) by A3, A10, A2;
A12: ( y in N & y0 in N ) by A3, A10, NFCONT_1:4;
then ( f /. x = f . x & f /. x0 = f . x0 ) by A1, PARTFUN1:def 6;
then A13: ( f /. x = g /. y & f /. x0 = g /. y0 ) by A12, A1, PARTFUN1:def 6;
x - x0 = y - y0 by REAL_NS1:5;
then ( L . (x - x0) = GL . (y - y0) & R . (x - x0) = GR /. (y - y0) ) by A5, PARTFUN1:def 6;
then (L . (x - x0)) + (R . (x - x0)) = (GL . (y - y0)) + (GR /. (y - y0)) by REAL_NS1:2;
hence (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) by A11, A13, REAL_NS1:5; :: thesis:

end;

assume 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)) ) ) ) ; :: thesis:
hence f is_differentiable_in x0 by Th24; :: thesis: