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:
let L, R be Function of (REAL m),(REAL n); :: 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;
assume A1: L is LinearOperator of m,n ; :: thesis:
given r0 being Real such that A2: ( 0 < r0 & { y where y is Element of REAL m : |.(y - x0).| < r0 } c= dom f & ( 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:
L is LinearOperator of (REAL-NS m),(REAL-NS n) by A1, Th14;
then reconsider GL = L as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS n))) by LOPBAN_1:def 9;
( REAL m = the carrier of (REAL-NS m) & REAL n = the carrier of (REAL-NS n) ) by REAL_NS1:def 4;
then reconsider GR = R as Function of (REAL-NS m),(REAL-NS n) ;
the carrier of (REAL-NS m) = REAL m by REAL_NS1:def 4;
then A3: dom R = the carrier of (REAL-NS m) by FUNCT_2:def 1;

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider d being Real such that
A4: ( 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 ) ) by A2;
take d = d; :: thesis:
thus d > 0 by A4; :: thesis:
thus for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| ") * ||.(GR /. z).|| < r :: thesis:

end;

then reconsider GR = GR as RestFunc of (REAL-NS m),(REAL-NS n) by NDIFF_1:23;
set N = { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } ;
reconsider N = { y where y is Point of (REAL-NS m) : ||.(y - y0).|| < r0 } as Neighbourhood of y0 by A2, NFCONT_1:3;
A7: N c= dom g by A2, Th23;
A8: for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0))

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

end;