let m, n be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),(REAL n)
for x0 being Element of REAL m
for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 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)) ) ) holds
( f is_differentiable_in x0 & diff f,x0 = L )
let f be PartFunc of (REAL m),(REAL n); :: thesis: for x0 being Element of REAL m
for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 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)) ) ) holds
( f is_differentiable_in x0 & diff f,x0 = L )
let x0 be Element of REAL m; :: thesis: for L, R being Function of (REAL m),(REAL n) st L is LinearOperator of m,n & ex r0 being Real st
( 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)) ) ) holds
( f is_differentiable_in x0 & diff f,x0 = L )
let L, R be Function of (REAL m),(REAL n); :: thesis: ( L is LinearOperator of m,n & ex r0 being Real st
( 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)) ) ) implies ( f is_differentiable_in x0 & diff f,x0 = L ) )
reconsider g = f as PartFunc of (REAL-NS m),(REAL-NS n) by DPREP010;
reconsider y0 = x0 as Point of (REAL-NS m) by REAL_NS1:def 4;
assume AS1: ( L is LinearOperator of m,n & ex r0 being Real st
( 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: ( f is_differentiable_in x0 & diff f,x0 = L )
then consider r0 being Real such that
AS2: ( 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)) ) ) ;
L is LinearOperator of (REAL-NS m),(REAL-NS n) by AS1, EQLOPBDef56;
then reconsider GL = L as Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS m),(REAL-NS n)) by LOPBAN_1:def 10;
( 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 D0: dom R = the carrier of (REAL-NS m) by FUNCT_2:def 1;

now

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

proof

let z be Point of (REAL-NS m); :: thesis: ( z <> 0. (REAL-NS m) & ||.z.|| < d implies (||.z.|| " ) * ||.(GR /. z).|| < r )
assume P11: ( z <> 0. (REAL-NS m) & ||.z.|| < d ) ; :: thesis: (||.z.|| " ) * ||.(GR /. z).|| < r
reconsider s = z as Element of REAL m by REAL_NS1:def 4;
reconsider w = R . s as Element of REAL n ;
P12: s <> 0* m by P11, REAL_NS1:def 4;
|.s.| < d by P11, REAL_NS1:1;
then (|.s.| " ) * |.w.| < r by P1, P12;
then (||.z.|| " ) * |.w.| < r by REAL_NS1:1;
hence (||.z.|| " ) * ||.(GR /. z).|| < r by REAL_NS1:1; :: thesis: verum

end;

end;

then reconsider GR = GR as REST of (REAL-NS m),(REAL-NS n) by NDIFF_1:26;
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 AS2, NFCONT_1:3;
P4: N c= dom g by AS2, DPREP099;
PP4: for y being Point of (REAL-NS m) st y in N holds
(g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0))

proof

let y be Point of (REAL-NS m); :: thesis: ( y in N implies (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0)) )
assume P41: y in N ; :: thesis: (g /. y) - (g /. y0) = (GL . (y - y0)) + (GR /. (y - y0))
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 P41, DPREP099;
then ex s being Element of REAL m st
( s = x & |.(s - x0).| < r0 ) ;
then P42: (f /. x) - (f /. x0) = (L . (x - x0)) + (R . (x - x0)) by AS2;
P421: y0 in N by NFCONT_1:4;
then ( f /. x = f . x & f /. x0 = f . x0 ) by P41, P4, PARTFUN1:def 8;
then P423: ( f /. x = g /. y & f /. x0 = g /. y0 ) by P41, P421, P4, PARTFUN1:def 8;
x - x0 = y - y0 by REAL_NS1:5;
then ( L . (x - x0) = GL . (y - y0) & R . (x - x0) = GR /. (y - y0) ) by D0, PARTFUN1:def 8;
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 P42, P423, REAL_NS1:5; :: thesis: verum

end;

then XX1: g is_differentiable_in y0 by P4, NDIFF_1:def 6;
hence XX2: f is_differentiable_in x0 by DPREP020; :: thesis: diff f,x0 = L
diff g,y0 = GL by XX1, PP4, P4, NDIFF_1:def 7;
hence diff f,x0 = L by DPREP030, XX2; :: thesis: verum