let m be non zero Nat; :: thesis:
let f be PartFunc of (REAL m),(REAL 1); :: thesis:
let X be Subset of (REAL m); :: thesis:
let x be Element of REAL m; :: thesis:
assume A1: ( X is open & x in X & ( for i being Nat st 1 <= i & i <= m holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) ) ; :: thesis:
consider L being Lipschitzian LinearOperator of m,1 such that
A2: for h being Element of REAL m ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & L . h = Sum w ) by Lm8;
consider d0 being Real such that
A3: d0 > 0 and
A4: { y where y is Element of REAL m : |.(y - x).| < d0 } c= X by A1, Th31;
set N = { y where y is Element of REAL m : |.(y - x).| < d0 } ;
1 <= m by NAT_1:14;
then f is_partial_differentiable_on X,m by A1;
then X c= dom f ;
then A5: { y where y is Element of REAL m : |.(y - x).| < d0 } c= dom f by A4;
deffunc H₁( Element of REAL m) -> Element of REAL 1 = ((f /. (x + $1)) - (f /. x)) - (L . $1);
consider R being Function of (REAL m),(REAL 1) such that
A6: for h being Element of REAL m holds R . h = H₁(h) from FUNCT_2:sch 4();
consider f0 being PartFunc of (REAL m),REAL such that
A7: f = <>* f0 by Th29;

let r0 be Real; :: thesis:
assume A9: r0 > 0 ; :: thesis:
set r1 = r0 / 2;
set r = (r0 / 2) / m;
defpred S₁[ Nat, Real] means ex k being Nat st
( $1 = k & 0 < $2 & ( for q being Element of REAL m st q in X & |.(q - x).| < $2 holds
|.((partdiff (f,q,k)) - (partdiff (f,x,k))).| < (r0 / 2) / m ) );
A10: for k0 being Nat st k0 in Seg m holds
ex d being Element of REAL st S₁[k0,d]

let k0 be Nat; :: thesis:
assume A11: k0 in Seg m ; :: thesis:
reconsider k = k0 as Nat ;
A12: ( 1 <= k & k <= m ) by A11, FINSEQ_1:1;
then f `partial| (X,k) is_continuous_on X by A1;
then consider d being Real such that
A13: ( 0 < d & ( for q being Element of REAL m st q in X & |.(q - x).| < d holds
|.(((f `partial| (X,k)) /. q) - ((f `partial| (X,k)) /. x)).| < (r0 / 2) / m ) ) by A9, A1, Th38;
reconsider d = d as Element of REAL by XREAL_0:def 1;
take d ; :: thesis:
for q being Element of REAL m st q in X & |.(q - x).| < d holds
|.((partdiff (f,q,k)) - (partdiff (f,x,k))).| < (r0 / 2) / m

proof

end;

hence ex k being Nat st
( k0 = k & 0 < d & ( for q being Element of REAL m st q in X & |.(q - x).| < d holds
|.((partdiff (f,q,k)) - (partdiff (f,x,k))).| < (r0 / 2) / m ) ) by A13; :: thesis:

end;

consider Dseq being FinSequence of REAL such that
A17: ( dom Dseq = Seg m & ( for i being Nat st i in Seg m holds
S₁[i,Dseq . i] ) ) from FINSEQ_1:sch 5(A10);
A18: rng Dseq is finite by A17, FINSET_1:8;
m in Seg m by FINSEQ_1:3;
then reconsider rDseq = rng Dseq as non empty ext-real-membered set by A17, FUNCT_1:3;
reconsider rDseq = rDseq as non empty ext-real-membered left_end right_end set by A18;
A19: min rDseq in rng Dseq by XXREAL_2:def 7;
reconsider d1 = min rDseq as Real ;
set d = min (d0,d1);
consider i1 being object such that
A20: ( i1 in dom Dseq & d1 = Dseq . i1 ) by A19, FUNCT_1:def 3;
reconsider i1 = i1 as Nat by A20;
A21: ex k being Nat st
( i1 = k & 0 < Dseq . i1 & ( for q being Element of REAL m st q in X & |.(q - x).| < Dseq . i1 holds
|.((partdiff (f,q,k)) - (partdiff (f,x,k))).| < (r0 / 2) / m ) ) by A17, A20;

A22: now :: thesis:

let q be Element of REAL m; :: thesis:
assume A23: |.(q - x).| < min (d0,d1) ; :: thesis:
min (d0,d1) <= d0 by XXREAL_0:17;
then |.(q - x).| < d0 by A23, XXREAL_0:2;
then q in { y where y is Element of REAL m : |.(y - x).| < d0 } ;
hence q in X by A4; :: thesis:

end;

A24: now :: thesis:

let q be Element of REAL m; :: thesis:
let i be Nat; :: thesis:
assume A25: ( |.(q - x).| < min (d0,d1) & i in Seg m ) ; :: thesis:
reconsider i0 = i as Nat ;
consider k being Nat such that
A26: ( i0 = k & 0 < Dseq . i0 & ( for q being Element of REAL m st q in X & |.(q - x).| < Dseq . i0 holds
|.((partdiff (f,q,k)) - (partdiff (f,x,k))).| < (r0 / 2) / m ) ) by A17, A25;
Dseq . i0 in rng Dseq by A17, A25, FUNCT_1:3;
then A27: d1 <= Dseq . i0 by XXREAL_2:def 7;
min (d0,d1) <= d1 by XXREAL_0:17;
then min (d0,d1) <= Dseq . i0 by A27, XXREAL_0:2;
then |.(q - x).| < Dseq . i0 by A25, XXREAL_0:2;
hence |.((partdiff (f,q,i)) - (partdiff (f,x,i))).| < (r0 / 2) / m by A22, A25, A26; :: thesis:

end;

take d = min (d0,d1); :: thesis:
thus 0 < d by A3, A20, A21, XXREAL_0:21; :: thesis:
thus for y being Element of REAL m
for z being Element of REAL 1 st y <> 0* m & |.y.| < d & z = R . y holds
(|.y.| ") * |.z.| < r0 :: thesis:

proof

let y be Element of REAL m; :: thesis:
let z be Element of REAL 1; :: thesis:
assume A28: ( y <> 0* m & |.y.| < d & z = R . y ) ; :: thesis:
consider h being FinSequence of REAL m, g being FinSequence of REAL 1 such that
A29: ( len h = m + 1 & len g = m & ( for i being Nat st i in dom h holds
h /. i = (y | ((m + 1) -' i)) ^ (0* (i -' 1)) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Element of REAL m st i in dom h & h /. i = hi holds
|.hi.| <= |.y.| ) & (f /. (x + y)) - (f /. x) = Sum g ) by Th28;
A30: R /. y = (Sum g) - (L . y) by A6, A29;
consider w being FinSequence of REAL 1 such that
A31: ( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . y) * (partdiff (f,x,i)) ) & L . y = Sum w ) by A2;
idseq m is Permutation of (Seg m) by FINSEQ_2:55;
then A32: ( dom (idseq m) = Seg m & rng (idseq m) = Seg m & idseq m is one-to-one ) by FUNCT_2:def 1, FUNCT_2:def 3;
then A33: ( dom (Rev (idseq m)) = Seg m & rng (Rev (idseq m)) = Seg m ) by FINSEQ_5:57;
then reconsider Ri = Rev (idseq m) as Function of (Seg m),(Seg m) by FUNCT_2:1;
( Ri is one-to-one & Ri is onto ) by A33, FUNCT_2:def 3;
then reconsider Ri = Rev (idseq m) as Permutation of (dom w) by A31;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A34: len (idseq m) = mm by A32, FINSEQ_1:def 3
.= len w by A31, FINSEQ_1:def 3 ;
A35: dom (w (*) Ri) = dom Ri by A33, RELAT_1:27
.= dom (Rev w) by A33, A31, FINSEQ_5:57 ;

now :: thesis:

let k be Nat; :: thesis:
assume A36: k in dom (Rev w) ; :: thesis:
then A37: k in dom (Rev (idseq m)) by A33, A31, FINSEQ_5:57;
then A38: ( 1 <= k & k <= m ) by A33, FINSEQ_1:1;
then reconsider mk = m - k as Nat by NAT_1:21;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A39: len (idseq m) = mm by A32, FINSEQ_1:def 3;
0 <= mk ;
then A40: 0 + 1 <= (m - k) + 1 by XREAL_1:6;
k - 1 >= 1 - 1 by A38, XREAL_1:9;
then m - (k - 1) <= m by XREAL_1:43;
then A41: mk + 1 in Seg m by A40;
thus (Rev w) . k = w . (((len (idseq m)) - k) + 1) by A34, A36, FINSEQ_5:def 3
.= w . ((idseq m) . (((len (idseq m)) - k) + 1)) by A41, A39, FINSEQ_2:49
.= w . ((Rev (idseq m)) . k) by A37, FINSEQ_5:def 3
.= (w (*) Ri) . k by A36, A35, FUNCT_1:12 ; :: thesis:

end;

then A42: Sum (Rev w) = Sum w by A35, EUCLID_7:21, FINSEQ_1:13;
deffunc H₂( Nat) -> Element of REAL 1 = (g /. $1) - ((Rev w) /. $1);
consider gw being FinSequence of REAL 1 such that
A43: ( len gw = m & ( for j being Nat st j in dom gw holds
gw . j = H₂(j) ) ) from FINSEQ_2:sch 1();

A44: now :: thesis:

let j be Nat; :: thesis:
assume A45: j in dom gw ; :: thesis:
hence gw /. j = gw . j by PARTFUN1:def 6
.= (g /. j) - ((Rev w) /. j) by A45, A43 ;
:: thesis:

end;

reconsider mm = m as Element of NAT by ORDINAL1:def 12;
A46: len w = mm by A31, FINSEQ_1:def 3;
then len (Rev w) = m by FINSEQ_5:def 3;
then A47: R /. y = Sum gw by A29, A30, A31, A43, A44, A42, Th27;
A48: for j being Nat st j in dom gw holds
ex gwj being Element of REAL 1 st
( gw . j = gwj & |.gwj.| <= |.y.| * ((r0 / 2) / m) )

proof

let j be Nat; :: thesis:
assume A49: j in dom gw ; :: thesis:
then A50: j in Seg m by A43, FINSEQ_1:def 3;
then j in dom g by A29, FINSEQ_1:def 3;
then A51: g /. j = (f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1)))) by A29;
A52: ( 1 <= j & j <= m ) by A50, FINSEQ_1:1;
then ( m + 1 <= m + j & j + 1 <= m + 1 ) by XREAL_1:6;
then ( (m + 1) - j <= m & 1 <= (m + 1) - j ) by XREAL_1:19, XREAL_1:20;
then A53: ( (m + 1) -' j <= m & 1 <= (m + 1) -' j ) by A52, NAT_D:37;
then A54: f is_partial_differentiable_on X,(m + 1) -' j by A1;
then A55: ( X c= dom f & ( for x being Element of REAL m st x in X holds
f is_partial_differentiable_in x,(m + 1) -' j ) ) by A53, Th34, A1;
A56: (m + 1) -' j in Seg m by A53;
then A57: w /. ((m + 1) -' j) = w . ((m + 1) -' j) by A31, PARTFUN1:def 6
.= ((proj (((m + 1) -' j),m)) . y) * (partdiff (f,x,((m + 1) -' j))) by A31, A56 ;

A58: now :: thesis:

let j be Nat; :: thesis:
assume ( 1 <= j & j <= m + 1 ) ; :: thesis:
then j in Seg (m + 1) ;
then A59: j in dom h by A29, FINSEQ_1:def 3;
A60: (x + (h /. j)) - x = h /. j by RVSUM_1:42;
reconsider hj = h /. j as Element of REAL m ;
|.hj.| <= |.y.| by A29, A59;
hence |.((x + (h /. j)) - x).| < d by A60, A28, XXREAL_0:2; :: thesis:

end;

rng f0 c= dom ((proj (1,1)) ") by PDIFF_1:2;
then A61: dom f = dom f0 by A7, RELAT_1:27;
m <= m + 1 by NAT_1:11;
then Seg m c= Seg (m + 1) by FINSEQ_1:5;
then ( 1 <= j & j <= m + 1 ) by A50, FINSEQ_1:1;
then A62: |.((x + (h /. j)) - x).| < d by A58;
then A63: x + (h /. j) in X by A22;
then A64: f /. (x + (h /. j)) = (<>* f0) . (x + (h /. j)) by A55, A7, PARTFUN1:def 6
.= ((proj (1,1)) ") . (f0 . (x + (h /. j))) by A63, A55, A61, FUNCT_1:13
.= <*(f0 . (x + (h /. j)))*> by PDIFF_1:1
.= <*(f0 /. (x + (h /. j)))*> by A63, A55, A61, PARTFUN1:def 6 ;
A65: ( 1 <= j & j <= m ) by A50, FINSEQ_1:1;
A66: 1 <= j + 1 by NAT_1:11;
A67: j + 1 <= m + 1 by A65, XREAL_1:6;
then A68: |.((x + (h /. (j + 1))) - x).| < d by A66, A58;
then A69: x + (h /. (j + 1)) in X by A22;
then A70: f /. (x + (h /. (j + 1))) = (<>* f0) . (x + (h /. (j + 1))) by A55, A7, PARTFUN1:def 6
.= ((proj (1,1)) ") . (f0 . (x + (h /. (j + 1)))) by A69, A55, A61, FUNCT_1:13
.= <*(f0 . (x + (h /. (j + 1))))*> by PDIFF_1:1
.= <*(f0 /. (x + (h /. (j + 1))))*> by A69, A55, A61, PARTFUN1:def 6 ;
f is_partial_differentiable_in x,(m + 1) -' j by A54, A53, Th34, A1;
then A71: partdiff (f,x,((m + 1) -' j)) = <*(partdiff (f0,x,((m + 1) -' j)))*> by A7, PDIFF_1:19;
then A72: ((proj (((m + 1) -' j),m)) . y) * (partdiff (f,x,((m + 1) -' j))) = <*(((proj (((m + 1) -' j),m)) . y) * (partdiff (f0,x,((m + 1) -' j))))*> by RVSUM_1:47;
A73: (f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1)))) = <*((f0 /. (x + (h /. j))) - (f0 /. (x + (h /. (j + 1)))))*> by A64, A70, RVSUM_1:29;
A74: ( X c= dom f0 & ( for x being Element of REAL m st x in X holds
f0 is_partial_differentiable_in x,(m + 1) -' j ) )

proof

thus X c= dom f0 by A54, A61; :: thesis:
let x be Element of REAL m; :: thesis:
assume x in X ; :: thesis:
then f is_partial_differentiable_in x,(m + 1) -' j by A54, A53, Th34, A1;
hence f0 is_partial_differentiable_in x,(m + 1) -' j by A7, PDIFF_1:18; :: thesis:

end;

A75: x + (h /. j) = (reproj (((m + 1) -' j),(x + (h /. (j + 1))))) . ((proj (((m + 1) -' j),m)) . (x + y)) by Th46, A29, A65;
(m + 1) -' (j + 1) = (m + 1) - (j + 1) by A67, XREAL_1:233;
then (m + 1) -' (j + 1) = m - j ;
then A76: (m + 1) -' (j + 1) = m -' j by A65, XREAL_1:233;
A77: (j + 1) -' 1 = (j + 1) - 1 by NAT_1:11, XREAL_1:233;
consider q being Element of REAL m such that
A78: ( |.(q - x).| < d & f0 is_partial_differentiable_in q,(m + 1) -' j & (f0 /. (x + (h /. j))) - (f0 /. (x + (h /. (j + 1)))) = (((proj (((m + 1) -' j),m)) . (x + y)) - ((proj (((m + 1) -' j),m)) . (x + (h /. (j + 1))))) * (partdiff (f0,q,((m + 1) -' j))) ) by A62, A68, A75, A53, A74, A22, A1, Th45;
A79: |.((partdiff (f,q,((m + 1) -' j))) - (partdiff (f,x,((m + 1) -' j)))).| < (r0 / 2) / m by A78, A56, A24;
f is_partial_differentiable_in q,(m + 1) -' j by A78, A7, PDIFF_1:18;
then A80: partdiff (f,q,((m + 1) -' j)) = <*(partdiff (f0,q,((m + 1) -' j)))*> by A7, PDIFF_1:19;
set mij = (m + 1) -' j;
set mj = m -' j;
reconsider hj1 = h /. (j + 1) as Element of REAL m ;
A81: ( len x = m & len y = m & len hj1 = m ) by CARD_1:def 7;
then ( (m + 1) -' j in dom x & (m + 1) -' j in dom y & (m + 1) -' j in dom hj1 ) by A56, FINSEQ_1:def 3;
then ( (m + 1) -' j in (dom x) /\ (dom y) & (m + 1) -' j in (dom x) /\ (dom hj1) ) by XBOOLE_0:def 4;
then A82: ( (m + 1) -' j in dom (x + y) & (m + 1) -' j in dom (x + hj1) ) by VALUED_1:def 1;
j + 1 in Seg (m + 1) by A66, A67;
then j + 1 in dom h by A29, FINSEQ_1:def 3;
then A83: h /. (j + 1) = (y | (m -' j)) ^ (0* j) by A29, A76, A77;
A84: len (y | (m -' j)) = m -' j by A81, FINSEQ_1:59, NAT_D:35;
(m + 1) -' j = (m -' j) + 1 by A65, NAT_D:38;
then (m + 1) -' j > len (y | (m -' j)) by A84, NAT_1:13;
then A85: hj1 . ((m + 1) -' j) = (0* j) . (((m + 1) -' j) - (m -' j)) by A53, A81, A83, A84, FINSEQ_1:24
.= 0 ;
A86: ((proj (((m + 1) -' j),m)) . (x + y)) - ((proj (((m + 1) -' j),m)) . (x + (h /. (j + 1)))) = ((x + y) . ((m + 1) -' j)) - ((proj (((m + 1) -' j),m)) . (x + (h /. (j + 1)))) by PDIFF_1:def 1
.= ((x + y) . ((m + 1) -' j)) - ((x + (h /. (j + 1))) . ((m + 1) -' j)) by PDIFF_1:def 1
.= ((x . ((m + 1) -' j)) + (y . ((m + 1) -' j))) - ((x + (h /. (j + 1))) . ((m + 1) -' j)) by A82, VALUED_1:def 1
.= ((x . ((m + 1) -' j)) + (y . ((m + 1) -' j))) - ((x . ((m + 1) -' j)) + 0) by A85, A82, VALUED_1:def 1
.= (proj (((m + 1) -' j),m)) . y by PDIFF_1:def 1 ;
reconsider gwj = gw /. j as Element of REAL 1 ;
take gwj ; :: thesis:
thus gw . j = gwj by A49, PARTFUN1:def 6; :: thesis:
A87: (m + 1) -' j = (m + 1) - j by A65, NAT_1:12, XREAL_1:233;
j in Seg (len (Rev w)) by A50, A46, FINSEQ_5:def 3;
then A88: j in dom (Rev w) by FINSEQ_1:def 3;
then (Rev w) /. j = (Rev w) . j by PARTFUN1:def 6
.= w . ((m - j) + 1) by A46, A88, FINSEQ_5:def 3
.= w /. ((m + 1) -' j) by A87, A56, A31, PARTFUN1:def 6 ;
then gw /. j = (g /. j) - (w /. ((m + 1) -' j)) by A49, A44
.= <*((((proj (((m + 1) -' j),m)) . y) * (partdiff (f0,q,((m + 1) -' j)))) - (((proj (((m + 1) -' j),m)) . y) * (partdiff (f0,x,((m + 1) -' j)))))*> by A78, A86, A57, A51, A72, A73, RVSUM_1:29
.= <*(((proj (((m + 1) -' j),m)) . y) * ((partdiff (f0,q,((m + 1) -' j))) - (partdiff (f0,x,((m + 1) -' j)))))*>
.= ((proj (((m + 1) -' j),m)) . y) * <*((partdiff (f0,q,((m + 1) -' j))) - (partdiff (f0,x,((m + 1) -' j))))*> by RVSUM_1:47
.= ((proj (((m + 1) -' j),m)) . y) * ((partdiff (f,q,((m + 1) -' j))) - (partdiff (f,x,((m + 1) -' j)))) by A71, A80, RVSUM_1:29 ;
then A89: |.gwj.| = |.((proj (((m + 1) -' j),m)) . y).| * |.((partdiff (f,q,((m + 1) -' j))) - (partdiff (f,x,((m + 1) -' j)))).| by EUCLID:11;
0 <= |.((proj (((m + 1) -' j),m)) . y).| by COMPLEX1:46;
then A90: |.gwj.| <= |.((proj (((m + 1) -' j),m)) . y).| * ((r0 / 2) / m) by A89, A79, XREAL_1:64;
|.(y . ((m + 1) -' j)).| <= |.y.| by A56, REAL_NS1:8;
then |.((proj (((m + 1) -' j),m)) . y).| <= |.y.| by PDIFF_1:def 1;
then |.((proj (((m + 1) -' j),m)) . y).| * ((r0 / 2) / m) <= |.y.| * ((r0 / 2) / m) by A9, XREAL_1:64;
hence |.gwj.| <= |.y.| * ((r0 / 2) / m) by A90, XXREAL_0:2; :: thesis:

end;

defpred S₂[ set , set ] means ex v being Element of REAL 1 st
( v = gw . $1 & $2 = |.v.| );

A91: now :: thesis:

let k be Nat; :: thesis:
assume k in Seg m ; :: thesis:
then k in dom gw by A43, FINSEQ_1:def 3;
then reconsider v = gw . k as Element of REAL 1 by PARTFUN1:4;
|.v.| in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S₂[k,x] ; :: thesis:

end;

consider yseq being FinSequence of REAL such that
A92: ( dom yseq = Seg m & ( for i being Nat st i in Seg m holds
S₂[i,yseq . i] ) ) from FINSEQ_1:sch 5(A91);
A93: len gw = len yseq by A43, A92, FINSEQ_1:def 3;

A94: now :: thesis:

let i be Nat; :: thesis:
assume i in dom gw ; :: thesis:
then i in Seg m by A43, FINSEQ_1:def 3;
hence ex v being Element of REAL 1 st
( v = gw . i & yseq . i = |.v.| ) by A92; :: thesis:

end;

reconsider yseq = yseq as Element of REAL m by A93, A43, FINSEQ_2:92;
A95: |.(Sum gw).| <= Sum yseq by A94, A93, PDIFF_6:17;
reconsider yr = |.y.| * ((r0 / 2) / m) as Element of REAL by XREAL_0:def 1;
for j being Nat st j in Seg m holds
yseq . j <= (m |-> yr) . j

proof

let j be Nat; :: thesis:
assume A96: j in Seg m ; :: thesis:
then A97: j in dom gw by A43, FINSEQ_1:def 3;
then A98: ex v being Element of REAL 1 st
( v = gw . j & yseq . j = |.v.| ) by A94;
ex gwj being Element of REAL 1 st
( gw . j = gwj & |.gwj.| <= |.y.| * ((r0 / 2) / m) ) by A48, A97;
hence yseq . j <= (m |-> yr) . j by A98, A96, FINSEQ_2:57; :: thesis:

end;

then Sum yseq <= Sum (m |-> yr) by RVSUM_1:82;
then Sum yseq <= m * (|.y.| * ((r0 / 2) / m)) by RVSUM_1:80;
then |.z.| <= m * (|.y.| * ((r0 / 2) / m)) by A47, A28, A95, XXREAL_0:2;
then |.z.| * (|.y.| ") <= ((m * |.y.|) * ((r0 / 2) / m)) * (|.y.| ") by XREAL_1:64;
then |.z.| * (|.y.| ") <= m * ((((r0 / 2) / m) * |.y.|) * (|.y.| ")) ;
then (|.y.| ") * |.z.| <= m * ((r0 / 2) / m) by A28, EUCLID:8, XCMPLX_1:203;
then A99: (|.y.| ") * |.z.| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A9, XREAL_1:216;
hence (|.y.| ") * |.z.| < r0 by A99, XXREAL_0:2; :: thesis:

end;

for y being Element of REAL m st |.(y - x).| < d0 holds
(f /. y) - (f /. x) = (L . (y - x)) + (R . (y - x))

proof

let y be Element of REAL m; :: thesis:
assume |.(y - x).| < d0 ; :: thesis:
R . (y - x) = ((f /. (x + (y - x))) - (f /. x)) - (L . (y - x)) by A6;
hence (L . (y - x)) + (R . (y - x)) = ((f /. (x + (y - x))) - (f /. x)) - ((L . (y - x)) - (L . (y - x))) by RVSUM_1:41
.= ((f /. (x + (y - x))) - (f /. x)) - (0* 1) by RVSUM_1:37
.= (f /. (x + (y - x))) - (f /. x) by RVSUM_1:32
.= (f /. ((x + y) - x)) - (f /. x) by RVSUM_1:40
.= (f /. (y + (x - x))) - (f /. x) by RVSUM_1:40
.= (f /. (y + (0* m))) - (f /. x) by RVSUM_1:37
.= (f /. y) - (f /. x) by RVSUM_1:16 ;
:: thesis:

end;

then ( f is_differentiable_in x & diff (f,x) = L ) by A3, A5, A8, PDIFF_6:24;
hence ( f is_differentiable_in x & ( for h being Element of REAL m ex w being FinSequence of REAL 1 st
( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h) * (partdiff (f,x,i)) ) & (diff (f,x)) . h = Sum w ) ) ) by A2; :: thesis: