let n, m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_differentiable_in x & 1 <= i & i <= m holds
( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) )
let i be Element of NAT ; :: thesis: for f being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f is_differentiable_in x & 1 <= i & i <= m holds
( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) )
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Point of (REAL-NS m) st f is_differentiable_in x & 1 <= i & i <= m holds
( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) )
let x be Point of (REAL-NS m); :: thesis: ( f is_differentiable_in x & 1 <= i & i <= m implies ( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) ) )
assume A1: f is_differentiable_in x ; :: thesis: ( not 1 <= i or not i <= m or ( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) ) )
assume A2: ( 1 <= i & i <= m ) ; :: thesis: ( f is_partial_differentiable_in x,i & partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) )
consider N being Neighbourhood of x such that
A3: ( N c= dom f & ex R being REST of (REAL-NS m),(REAL-NS n) st
for y being Point of (REAL-NS m) st y in N holds
(f /. y) - (f /. x) = ((diff f,x) . (y - x)) + (R /. (y - x)) ) by A1, NDIFF_1:def 7;
consider R being REST of (REAL-NS m),(REAL-NS n) such that
A4: for y being Point of (REAL-NS m) st y in N holds
(f /. y) - (f /. x) = ((diff f,x) . (y - x)) + (R /. (y - x)) by A3;
consider r0 being Real such that
A5: ( 0 < r0 & { z where z is Point of (REAL-NS m) : ||.(z - x).|| < r0 } c= N ) by NFCONT_1:def 3;
set u = f * (reproj i,x);
reconsider x0 = (Proj i,m) . x as Point of (REAL-NS 1) ;
set Z = 0. (REAL-NS m);
set Nx0 = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < r0 } ;

now

let s be set ; :: thesis: ( s in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < r0 } implies s in the carrier of (REAL-NS 1) )
assume s in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < r0 } ; :: thesis: s in the carrier of (REAL-NS 1)
then ex z being Point of (REAL-NS 1) st
( s = z & ||.(z - x0).|| < r0 ) ;
hence s in the carrier of (REAL-NS 1) ; :: thesis: verum

end;

then { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < r0 } is Subset of (REAL-NS 1) by TARSKI:def 3;
then reconsider Nx0 = { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < r0 } as Neighbourhood of x0 by A5, NFCONT_1:def 3;
A6: for xi being Element of (REAL-NS 1) st xi in Nx0 holds
(reproj i,x) . xi in N

proof

let xi be Element of (REAL-NS 1); :: thesis: ( xi in Nx0 implies (reproj i,x) . xi in N )
assume xi in Nx0 ; :: thesis: (reproj i,x) . xi in N
then A7: ex z being Point of (REAL-NS 1) st
( xi = z & ||.(z - x0).|| < r0 ) ;
((reproj i,x) . xi) - x = (reproj i,(0. (REAL-NS m))) . (xi - x0) by A2, Th20;
then ||.(((reproj i,x) . xi) - x).|| < r0 by A2, Th5, A7;
then (reproj i,x) . xi in { z where z is Point of (REAL-NS m) : ||.(z - x).|| < r0 } ;
hence (reproj i,x) . xi in N by A5; :: thesis: verum

end;

A8: R is total by NDIFF_1:def 5;
then A9: dom R = the carrier of (REAL-NS m) by PARTFUN1:def 4;
reconsider R1 = R * (reproj i,(0. (REAL-NS m))) as PartFunc of (REAL-NS 1),(REAL-NS n) ;
A10: dom (reproj i,(0. (REAL-NS m))) = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
A11: dom R1 = the carrier of (REAL-NS 1) by A8, PARTFUN1:def 4;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R1 /. z).|| < r ) )

proof

let r be Real; :: thesis: ( r > 0 implies ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R1 /. z).|| < r ) ) )
assume r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R1 /. z).|| < r ) )
then consider d being Real such that
A12: ( d > 0 & ( for z being Point of (REAL-NS m) st z <> 0. (REAL-NS m) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R /. z).|| < r ) ) by A8, NDIFF_1:26;
take d ; :: thesis: ( d > 0 & ( for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R1 /. z).|| < r ) )

now

let z be Point of (REAL-NS 1); :: thesis: ( z <> 0. (REAL-NS 1) & ||.z.|| < d implies (||.z.|| " ) * ||.(R1 /. z).|| < r )
assume A13: ( z <> 0. (REAL-NS 1) & ||.z.|| < d ) ; :: thesis: (||.z.|| " ) * ||.(R1 /. z).|| < r
A14: ||.((reproj i,(0. (REAL-NS m))) . z).|| = ||.z.|| by A2, Th5;
R /. ((reproj i,(0. (REAL-NS m))) . z) = R . ((reproj i,(0. (REAL-NS m))) . z) by A9, PARTFUN1:def 8;
then R /. ((reproj i,(0. (REAL-NS m))) . z) = R1 . z by FUNCT_1:23, A10;
then R /. ((reproj i,(0. (REAL-NS m))) . z) = R1 /. z by A11, PARTFUN1:def 8;
hence (||.z.|| " ) * ||.(R1 /. z).|| < r by A12, A14, A13, Th18, A2; :: thesis: verum

end;

hence ( d > 0 & ( for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| " ) * ||.(R1 /. z).|| < r ) ) by A12; :: thesis: verum

end;

then reconsider R1 = R1 as REST of (REAL-NS 1),(REAL-NS n) by NDIFF_1:26, A8;
reconsider dfx = diff f,x as bounded LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 10;
reconsider LD1 = dfx * (reproj i,(0. (REAL-NS m))) as Function of (REAL-NS 1),(REAL-NS n) ;

A15: now

let x, y be Element of (REAL-NS 1); :: thesis: LD1 . (x + y) = (LD1 . x) + (LD1 . y)
LD1 . (x + y) = dfx . ((reproj i,(0. (REAL-NS m))) . (x + y)) by FUNCT_2:21;
then LD1 . (x + y) = dfx . (((reproj i,(0. (REAL-NS m))) . x) + ((reproj i,(0. (REAL-NS m))) . y)) by Th14, A2;
then LD1 . (x + y) = (dfx . ((reproj i,(0. (REAL-NS m))) . x)) + (dfx . ((reproj i,(0. (REAL-NS m))) . y)) by GRCAT_1:def 13;
then LD1 . (x + y) = (LD1 . x) + (dfx . ((reproj i,(0. (REAL-NS m))) . y)) by FUNCT_2:21;
hence LD1 . (x + y) = (LD1 . x) + (LD1 . y) by FUNCT_2:21; :: thesis: verum

end;

now

let x be Element of (REAL-NS 1); :: thesis: for a being Real holds LD1 . (a * x) = a * (LD1 . x)
let a be Real; :: thesis: LD1 . (a * x) = a * (LD1 . x)
LD1 . (a * x) = dfx . ((reproj i,(0. (REAL-NS m))) . (a * x)) by FUNCT_2:21;
then LD1 . (a * x) = dfx . (a * ((reproj i,(0. (REAL-NS m))) . x)) by Th16, A2;
then LD1 . (a * x) = a * (dfx . ((reproj i,(0. (REAL-NS m))) . x)) by LOPBAN_1:def 6;
hence LD1 . (a * x) = a * (LD1 . x) by FUNCT_2:21; :: thesis: verum

end;

then reconsider LD1 = LD1 as LinearOperator of (REAL-NS 1),(REAL-NS n) by A15, LOPBAN_1:def 6, GRCAT_1:def 13;
reconsider LD1 = LD1 as Point of (R_NormSpace_of_BoundedLinearOperators (REAL-NS 1),(REAL-NS n)) by LOPBAN_1:def 10;

now

let s be set ; :: thesis: ( s in (reproj i,x) .: Nx0 implies s in dom f )
assume s in (reproj i,x) .: Nx0 ; :: thesis: s in dom f
then ex t being Element of (REAL-NS 1) st
( t in Nx0 & s = (reproj i,x) . t ) by FUNCT_2:116;
then s in N by A6;
hence s in dom f by A3; :: thesis: verum

end;

then A16: (reproj i,x) .: Nx0 c= dom f by TARSKI:def 3;
dom (reproj i,x) = the carrier of (REAL-NS 1) by FUNCT_2:def 1;
then A17: Nx0 c= dom (f * (reproj i,x)) by FUNCT_3:3, A16;
A18: for y being Point of (REAL-NS 1) st y in Nx0 holds
((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))

proof

let y be Point of (REAL-NS 1); :: thesis: ( y in Nx0 implies ((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) )
assume A19: y in Nx0 ; :: thesis: ((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))
then A20: (reproj i,x) . y in N by A6;
consider q being Element of REAL , z being Element of REAL m such that
A21: ( x0 = <*q*> & z = x & (reproj i,x) . x0 = (reproj i,z) . q ) by PDIFF_1:def 6;
reconsider zi = z . i as Element of REAL ;
x0 = <*((proj i,m) . x)*> by PDIFF_1:def 4;
then q = (proj i,m) . z by A21, FINSEQ_1:97;
then (reproj i,x) . x0 = (reproj i,z) . (z . i) by A21, PDIFF_1:def 1;
then (reproj i,x) . x0 = Replace z,i,zi by PDIFF_1:def 5;
then A22: (reproj i,x) . x0 = x by A21, FUNCT_7:37;
A23: x0 in Nx0 by NFCONT_1:4;
A24: (reproj i,x) . x0 in N by A6, NFCONT_1:4;
(f * (reproj i,x)) /. y = (f * (reproj i,x)) . y by A19, A17, PARTFUN1:def 8;
then (f * (reproj i,x)) /. y = f . ((reproj i,x) . y) by FUNCT_2:21;
then A25: (f * (reproj i,x)) /. y = f /. ((reproj i,x) . y) by A20, A3, PARTFUN1:def 8;
(f * (reproj i,x)) /. x0 = (f * (reproj i,x)) . x0 by A23, A17, PARTFUN1:def 8;
then (f * (reproj i,x)) /. x0 = f . ((reproj i,x) . x0) by FUNCT_2:21;
then A26: ((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (f /. ((reproj i,x) . y)) - (f /. x) by A25, A22, A24, A3, PARTFUN1:def 8;
R /. ((reproj i,(0. (REAL-NS m))) . (y - x0)) = R . ((reproj i,(0. (REAL-NS m))) . (y - x0)) by A9, PARTFUN1:def 8;
then R /. ((reproj i,(0. (REAL-NS m))) . (y - x0)) = R1 . (y - x0) by FUNCT_1:23, A10;
then A27: R /. ((reproj i,(0. (REAL-NS m))) . (y - x0)) = R1 /. (y - x0) by A11, PARTFUN1:def 8;
((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = ((diff f,x) . (((reproj i,x) . y) - x)) + (R /. (((reproj i,x) . y) - x)) by A26, A4, A19, A6;
then ((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (dfx . ((reproj i,(0. (REAL-NS m))) . (y - x0))) + (R /. (((reproj i,x) . y) - x)) by A2, Th20;
then ((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (dfx . ((reproj i,(0. (REAL-NS m))) . (y - x0))) + (R /. ((reproj i,(0. (REAL-NS m))) . (y - x0))) by A2, Th20;
hence ((f * (reproj i,x)) /. y) - ((f * (reproj i,x)) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) by A27, FUNCT_2:21; :: thesis: verum

end;

then A28: f * (reproj i,x) is_differentiable_in x0 by A17, NDIFF_1:def 6;
hence f is_partial_differentiable_in x,i by PDIFF_1:def 9; :: thesis: partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m)))
thus partdiff f,x,i = (diff f,x) * (reproj i,(0. (REAL-NS m))) by A28, NDIFF_1:def 7, A17, A18; :: thesis: verum