let m be non zero Nat; :: thesis:
let f be PartFunc of (REAL-NS m),(REAL-NS 1); :: thesis:
let X be Subset of (REAL-NS m); :: thesis:
let x be Point of (REAL-NS 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:
A2: ( the carrier of (REAL-NS m) = REAL m & the carrier of (REAL-NS 1) = REAL 1 ) by REAL_NS1:def 4;
reconsider One0 = <*jj*> as Element of REAL 1 by FINSEQ_2:98;
reconsider One = One0 as Point of (REAL-NS 1) by REAL_NS1:def 4;
reconsider f0 = f as PartFunc of (REAL m),(REAL 1) by A2;
reconsider X0 = X as Subset of (REAL m) by REAL_NS1:def 4;
reconsider x0 = x as Element of REAL m by REAL_NS1:def 4;
A3: X0 is open by A1;

let z be Element of REAL m; :: thesis:
assume A11: z in X0 ; :: thesis:
then f0 is_partial_differentiable_in z,i by A7, A5, A3, Th34;
then consider g being PartFunc of (REAL-NS m),(REAL-NS 1), y being Point of (REAL-NS m) such that
A12: ( f0 = g & z = y & partdiff (f0,z,i) = (partdiff (g,y,i)) . <*1*> ) by PDIFF_1:def 14;
take y ; :: thesis:
thus z = y by A12; :: thesis:
thus (f0 `partial| (X0,i)) /. z = (partdiff (f,y,i)) . One by A12, A11, Def5, A7; :: thesis:

end;

for z0 being Element of REAL m
for r being Real st z0 in X0 & 0 < r holds
ex s being Real st
( 0 < s & ( for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r ) )

let z0 be Element of REAL m; :: thesis:
let r be Real; :: thesis:
assume A13: ( z0 in X0 & 0 < r ) ; :: thesis:
reconsider y0 = z0 as Point of (REAL-NS m) by REAL_NS1:def 4;
consider s being Real such that
A14: ( 0 < s & ( for y1 being Point of (REAL-NS m) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) by A8, A13, NFCONT_1:19;
reconsider s = s as Real ;
take s ; :: thesis:
thus 0 < s by A14; :: thesis:
thus for z1 being Element of REAL m st z1 in X & |.(z1 - z0).| < s holds
|.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r :: thesis:

let z1 be Element of REAL m; :: thesis:
assume A15: ( z1 in X & |.(z1 - z0).| < s ) ; :: thesis:
reconsider y1 = z1 as Point of (REAL-NS m) by REAL_NS1:def 4;
|.(z1 - z0).| = ||.(y1 - y0).|| by REAL_NS1:1, REAL_NS1:5;
then A16: ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by A15, A14;
(f `partial| (X,i)) /. y1 = partdiff (f,y1,i) by A6, A15, PDIFF_1:def 20;
then A17: ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r by A16, A6, A13, PDIFF_1:def 20;
A18: ex y1 being Point of (REAL-NS m) st
( z1 = y1 & (f0 `partial| (X0,i)) /. z1 = (partdiff (f,y1,i)) . One ) by A10, A15;
A19: ex y0 being Point of (REAL-NS m) st
( z0 = y0 & (f0 `partial| (X0,i)) /. z0 = (partdiff (f,y0,i)) . One ) by A10, A13;
reconsider PDP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 9;
((partdiff (f,y1,i)) . One) - ((partdiff (f,y0,i)) . One) = PDP . One by LOPBAN_1:40;
then A20: ||.(((partdiff (f,y1,i)) . One) - ((partdiff (f,y0,i)) . One)).|| <= ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| * ||.One.|| by LOPBAN_1:32;
||.One.|| = |.One0.| by REAL_NS1:1
.= |.1.| by TOPREALC:18
.= 1 by ABSVALUE:def 1 ;
then ||.(((partdiff (f,y1,i)) . One) - ((partdiff (f,y0,i)) . One)).|| < r by A20, A17, XXREAL_0:2;
hence |.(((f0 `partial| (X0,i)) /. z1) - ((f0 `partial| (X0,i)) /. z0)).| < r by A18, A19, REAL_NS1:1, REAL_NS1:5; :: thesis:

end;

end;

then A21: ( f0 is_differentiable_in x0 & ( for h0 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)) . h0) * (partdiff (f0,x0,i)) ) & (diff (f0,x0)) . h0 = Sum w ) ) ) by Th47, A3, A1;
then ex g being PartFunc of (REAL-NS m),(REAL-NS 1) ex y being Point of (REAL-NS m) st
( f0 = g & x0 = y & g is_differentiable_in y ) ;
hence f is_differentiable_in x ; :: thesis:
A22: ex g being PartFunc of (REAL-NS m),(REAL-NS 1) ex y being Point of (REAL-NS m) st
( f0 = g & x0 = y & diff (f0,x0) = diff (g,y) ) by A21, PDIFF_1:def 8;

let h be Point of (REAL-NS m); :: thesis:
reconsider h0 = h as Element of REAL m by REAL_NS1:def 4;
consider w being FinSequence of REAL 1 such that
A23: ( dom w = Seg m & ( for i being Nat st i in Seg m holds
w . i = ((proj (i,m)) . h0) * (partdiff (f0,x0,i)) ) & (diff (f0,x0)) . h0 = Sum w ) by Th47, A3, A1, A4;
take w = w; :: thesis:
thus dom w = Seg m by A23; :: thesis:
thus for i being Nat st i in Seg m holds
w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> :: thesis:

let i be Nat; :: thesis:
assume A24: i in Seg m ; :: thesis:
then A25: ( 1 <= i & i <= m ) by FINSEQ_1:1;
then f0 is_partial_differentiable_on X0,i by A4;
then f0 is_partial_differentiable_in x0,i by A1, A3, A25, Th34;
then A26: ex g being PartFunc of (REAL-NS m),(REAL-NS 1) ex y being Point of (REAL-NS m) st
( f0 = g & x0 = y & partdiff (f0,x0,i) = (partdiff (g,y,i)) . <*1*> ) by PDIFF_1:def 14;
A27: ((proj (i,m)) . h) * One = ((proj (i,m)) . h0) * One0 by REAL_NS1:3
.= <*(((proj (i,m)) . h0) * 1)*> by RVSUM_1:47
.= <*((proj (i,m)) . h)*> ;
reconsider PDP = partdiff (f,x,i) as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS 1) by LOPBAN_1:def 9;
((proj (i,m)) . h0) * (partdiff (f0,x0,i)) = ((proj (i,m)) . h0) * (PDP . One) by A26, REAL_NS1:3
.= (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> by A27, LOPBAN_1:def 5 ;
hence w . i = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> by A24, A23; :: thesis:

end;

thus (diff (f,x)) . h = Sum w by A23, A22; :: thesis:

end;

hence for h being Point of (REAL-NS 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 = (partdiff (f,x,i)) . <*((proj (i,m)) . h)*> ) & (diff (f,x)) . h = Sum w ) ; :: thesis: