let n, m be non zero Nat; :: thesis: for i being 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 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 RestFunc 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 RestFunc 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 1;
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 :: thesis: for s being object st s in { z where z is Point of (REAL-NS 1) : ||.(z - x0).|| < r0 } holds
s in the carrier of (REAL-NS 1)

let s be object ; :: 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 1;
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 2;
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 2;
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:23;
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 :: thesis: for z being Point of (REAL-NS 1) st z <> 0. (REAL-NS 1) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r

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 6;
then R /. ((reproj (i,(0. (REAL-NS m)))) . z) = R1 . z by A10, FUNCT_1:13;
then R /. ((reproj (i,(0. (REAL-NS m)))) . z) = R1 /. z by A11, PARTFUN1:def 6;
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 RestFunc of (REAL-NS 1),(REAL-NS n) by A8, NDIFF_1:23;
reconsider dfx = diff (f,x) as Lipschitzian LinearOperator of (REAL-NS m),(REAL-NS n) by LOPBAN_1:def 9;
reconsider LD1 = dfx * (reproj (i,(0. (REAL-NS m)))) as Function of (REAL-NS 1),(REAL-NS n) ;

A15: now :: thesis: for x, y being Element of (REAL-NS 1) holds LD1 . (x + y) = (LD1 . x) + (LD1 . y)

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:15;
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 VECTSP_1:def 20;
then LD1 . (x + y) = (LD1 . x) + (dfx . ((reproj (i,(0. (REAL-NS m)))) . y)) by FUNCT_2:15;
hence LD1 . (x + y) = (LD1 . x) + (LD1 . y) by FUNCT_2:15; :: thesis: verum

end;

now :: thesis: for x being Element of (REAL-NS 1)
for a being Real holds LD1 . (a * x) = a * (LD1 . x)

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:15;
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 5;
hence LD1 . (a * x) = a * (LD1 . x) by FUNCT_2:15; :: thesis: verum

end;

then reconsider LD1 = LD1 as LinearOperator of (REAL-NS 1),(REAL-NS n) by A15, LOPBAN_1:def 5, VECTSP_1:def 20;
reconsider LD1 = LD1 as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS n))) by LOPBAN_1:def 9;

now :: thesis: for s being object st s in (reproj (i,x)) .: Nx0 holds
s in dom f

let s be object ; :: 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:65;
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 ;
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 A16, FUNCT_3:3;
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 by XREAL_0:def 1;
x0 = <*((proj (i,m)) . x)*> by PDIFF_1:def 4;
then q = (proj (i,m)) . z by A21, FINSEQ_1:76;
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:35;
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 6;
then (f * (reproj (i,x))) /. y = f . ((reproj (i,x)) . y) by FUNCT_2:15;
then A25: (f * (reproj (i,x))) /. y = f /. ((reproj (i,x)) . y) by A20, A3, PARTFUN1:def 6;
(f * (reproj (i,x))) /. x0 = (f * (reproj (i,x))) . x0 by A23, A17, PARTFUN1:def 6;
then (f * (reproj (i,x))) /. x0 = f . ((reproj (i,x)) . x0) by FUNCT_2:15;
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 6;
R /. ((reproj (i,(0. (REAL-NS m)))) . (y - x0)) = R . ((reproj (i,(0. (REAL-NS m)))) . (y - x0)) by A9, PARTFUN1:def 6;
then R /. ((reproj (i,(0. (REAL-NS m)))) . (y - x0)) = R1 . (y - x0) by A10, FUNCT_1:13;
then A27: R /. ((reproj (i,(0. (REAL-NS m)))) . (y - x0)) = R1 /. (y - x0) by A11, PARTFUN1:def 6;
((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:15; :: 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 ; :: 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, A17, A18, NDIFF_1:def 7; :: thesis: verum