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 } ;
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 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 ) ) 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) ;
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;
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)) 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