let G be RealNormSpace-Sequence; :: thesis: for S being RealNormSpace
for f being PartFunc of (product G),S
for x being Point of (product G)
for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let S be RealNormSpace; :: thesis: for f being PartFunc of (product G),S
for x being Point of (product G)
for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let f be PartFunc of (product G),S; :: thesis: for x being Point of (product G)
for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let x be Point of (product G); :: thesis: for i being set st f is_differentiable_in x holds
( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) )
let i0 be set ; :: thesis: ( f is_differentiable_in x implies ( f is_partial_differentiable_in x,i0 & partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G)))) ) )
assume A1: f is_differentiable_in x ; :: thesis: ( f is_partial_differentiable_in x,i0 & partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G)))) )
set i = In (i0,(dom G));
consider N being Neighbourhood of x such that
A2: ( N c= dom f & ex R being RestFunc of (product G),S st
for y being Point of (product G) 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 (product G),S such that
A3: for y being Point of (product G) st y in N holds
(f /. y) - (f /. x) = ((diff (f,x)) . (y - x)) + (R /. (y - x)) by A2;
consider r0 being Real such that
A4: ( 0 < r0 & { z where z is Point of (product G) : ||.(z - x).|| < r0 } c= N ) by NFCONT_1:def 1;
set u = f * (reproj ((In (i0,(dom G))),x));
reconsider x0 = (proj (In (i0,(dom G)))) . x as Point of (G . (In (i0,(dom G)))) ;
set Z = 0. (product G);
set Nx0 = { z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } ;

now :: thesis: for s being object st s in { z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } holds
s in the carrier of (G . (In (i0,(dom G))))

let s be object ; :: thesis: ( s in { z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } implies s in the carrier of (G . (In (i0,(dom G)))) )
assume s in { z where z is Point of (G . (In (i0,(dom G)))) : ||.(z - x0).|| < r0 } ; :: thesis: s in the carrier of (G . (In (i0,(dom G))))
then ex z being Point of (G . (In (i0,(dom G)))) st
( s = z & ||.(z - x0).|| < r0 ) ;
hence s in the carrier of (G . (In (i0,(dom G)))) ; :: thesis: verum

end;

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

proof

let xi be Element of (G . (In (i0,(dom G)))); :: thesis: ( xi in Nx0 implies (reproj ((In (i0,(dom G))),x)) . xi in N )
assume xi in Nx0 ; :: thesis: (reproj ((In (i0,(dom G))),x)) . xi in N
then A6: ex z being Point of (G . (In (i0,(dom G)))) st
( xi = z & ||.(z - x0).|| < r0 ) ;
((reproj ((In (i0,(dom G))),x)) . xi) - x = (reproj ((In (i0,(dom G))),(0. (product G)))) . (xi - x0) by Th22;
then ||.(((reproj ((In (i0,(dom G))),x)) . xi) - x).|| < r0 by Th21, A6;
then (reproj ((In (i0,(dom G))),x)) . xi in { z where z is Point of (product G) : ||.(z - x).|| < r0 } ;
hence (reproj ((In (i0,(dom G))),x)) . xi in N by A4; :: thesis: verum

end;

A7: R is total by NDIFF_1:def 5;
then A8: dom R = the carrier of (product G) by PARTFUN1:def 2;
reconsider R1 = R * (reproj ((In (i0,(dom G))),(0. (product G)))) as PartFunc of (G . (In (i0,(dom G)))),S ;
A9: dom (reproj ((In (i0,(dom G))),(0. (product G)))) = the carrier of (G . (In (i0,(dom G)))) by FUNCT_2:def 1;
A10: dom R1 = the carrier of (G . (In (i0,(dom G)))) by A7, PARTFUN1:def 2;
for r being Real st r > 0 holds
ex d being Real st
( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.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 (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) ) )
assume r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )
then consider d being Real such that
A11: ( d > 0 & ( for z being Point of (product G) st z <> 0. (product G) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A7, NDIFF_1:23;
take d ; :: thesis: ( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )

now :: thesis: for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r

let z be Point of (G . (In (i0,(dom G)))); :: thesis: ( z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d implies (||.z.|| ") * ||.(R1 /. z).|| < r )
assume A12: ( z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d ) ; :: thesis: (||.z.|| ") * ||.(R1 /. z).|| < r
A13: ||.((reproj ((In (i0,(dom G))),(0. (product G)))) . z).|| = ||.z.|| by Th21;
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) = R . ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) by A8, PARTFUN1:def 6;
then R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) = R1 . z by A9, FUNCT_1:13;
then R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . z) = R1 /. z by A10, PARTFUN1:def 6;
hence (||.z.|| ") * ||.(R1 /. z).|| < r by A11, A13, A12, Th38; :: thesis: verum

end;

hence ( d > 0 & ( for z being Point of (G . (In (i0,(dom G)))) st z <> 0. (G . (In (i0,(dom G)))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) ) by A11; :: thesis: verum

end;

then reconsider R1 = R1 as RestFunc of (G . (In (i0,(dom G)))),S by A7, NDIFF_1:23;
reconsider dfx = diff (f,x) as Lipschitzian LinearOperator of (product G),S by LOPBAN_1:def 9;
reconsider LD1 = dfx * (reproj ((In (i0,(dom G))),(0. (product G)))) as Function of (G . (In (i0,(dom G)))),S ;

A14: now :: thesis: for x, y being Element of (G . (In (i0,(dom G)))) holds LD1 . (x + y) = (LD1 . x) + (LD1 . y)

let x, y be Element of (G . (In (i0,(dom G)))); :: thesis: LD1 . (x + y) = (LD1 . x) + (LD1 . y)
LD1 . (x + y) = dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (x + y)) by FUNCT_2:15;
then LD1 . (x + y) = dfx . (((reproj ((In (i0,(dom G))),(0. (product G)))) . x) + ((reproj ((In (i0,(dom G))),(0. (product G)))) . y)) by Th34;
then LD1 . (x + y) = (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . x)) + (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . y)) by VECTSP_1:def 20;
then LD1 . (x + y) = (LD1 . x) + (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . 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 (G . (In (i0,(dom G))))
for a being Real holds LD1 . (a * x) = a * (LD1 . x)

let x be Element of (G . (In (i0,(dom G)))); :: 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 ((In (i0,(dom G))),(0. (product G)))) . (a * x)) by FUNCT_2:15;
then LD1 . (a * x) = dfx . (a * ((reproj ((In (i0,(dom G))),(0. (product G)))) . x)) by Th39;
then LD1 . (a * x) = a * (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . 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 (G . (In (i0,(dom G)))),S by A14, LOPBAN_1:def 5, VECTSP_1:def 20;
consider K0 being Real such that
A15: ( 0 <= K0 & ( for x being VECTOR of (product G) holds ||.(dfx . x).|| <= K0 * ||.x.|| ) ) by LOPBAN_1:def 8;

now :: thesis: for r being VECTOR of (G . (In (i0,(dom G)))) holds ||.(LD1 . r).|| <= K0 * ||.r.||

let r be VECTOR of (G . (In (i0,(dom G)))); :: thesis: ||.(LD1 . r).|| <= K0 * ||.r.||
||.(dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . r)).|| <= K0 * ||.((reproj ((In (i0,(dom G))),(0. (product G)))) . r).|| by A15;
then ||.(dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . r)).|| <= K0 * ||.r.|| by Th21;
hence ||.(LD1 . r).|| <= K0 * ||.r.|| by FUNCT_2:15; :: thesis: verum

end;

then LD1 is Lipschitzian by A15;
then reconsider LD1 = LD1 as Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i0,(dom G)))),S)) by LOPBAN_1:def 9;

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

let s be object ; :: thesis: ( s in (reproj ((In (i0,(dom G))),x)) .: Nx0 implies s in dom f )
assume s in (reproj ((In (i0,(dom G))),x)) .: Nx0 ; :: thesis: s in dom f
then ex t being Element of (G . (In (i0,(dom G)))) st
( t in Nx0 & s = (reproj ((In (i0,(dom G))),x)) . t ) by FUNCT_2:65;
hence s in dom f by A2, A5; :: thesis: verum

end;

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

proof

let y be Point of (G . (In (i0,(dom G)))); :: thesis: ( y in Nx0 implies ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) )
assume A19: y in Nx0 ; :: thesis: ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))
then A20: (reproj ((In (i0,(dom G))),x)) . y in N by A5;
A21: (reproj ((In (i0,(dom G))),x)) . x0 = x +* ((In (i0,(dom G))),x0) by Def4;
A22: the carrier of (product G) = product (carr G) by Th10;
x . (In (i0,(dom G))) = x0 by Def3, A22;
then A23: x = x +* ((In (i0,(dom G))),x0) by FUNCT_7:35;
A24: (reproj ((In (i0,(dom G))),x)) . x0 in N by A5, NFCONT_1:4;
(f * (reproj ((In (i0,(dom G))),x))) /. y = (f * (reproj ((In (i0,(dom G))),x))) . y by A19, A17, PARTFUN1:def 6;
then (f * (reproj ((In (i0,(dom G))),x))) /. y = f . ((reproj ((In (i0,(dom G))),x)) . y) by FUNCT_2:15;
then A25: (f * (reproj ((In (i0,(dom G))),x))) /. y = f /. ((reproj ((In (i0,(dom G))),x)) . y) by A20, A2, PARTFUN1:def 6;
R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) = R . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) by A8, PARTFUN1:def 6;
then R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) = R1 . (y - x0) by A9, FUNCT_1:13;
then A26: R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0)) = R1 /. (y - x0) by A10, PARTFUN1:def 6;
x0 in Nx0 by NFCONT_1:4;
then (f * (reproj ((In (i0,(dom G))),x))) /. x0 = (f * (reproj ((In (i0,(dom G))),x))) . x0 by A17, PARTFUN1:def 6;
then (f * (reproj ((In (i0,(dom G))),x))) /. x0 = f . ((reproj ((In (i0,(dom G))),x)) . x0) by FUNCT_2:15;
then ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (f /. ((reproj ((In (i0,(dom G))),x)) . y)) - (f /. x) by A25, A23, A24, A2, A21, PARTFUN1:def 6;
then ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = ((diff (f,x)) . (((reproj ((In (i0,(dom G))),x)) . y) - x)) + (R /. (((reproj ((In (i0,(dom G))),x)) . y) - x)) by A3, A19, A5;
then ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0))) + (R /. (((reproj ((In (i0,(dom G))),x)) . y) - x)) by Th22;
then ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (dfx . ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0))) + (R /. ((reproj ((In (i0,(dom G))),(0. (product G)))) . (y - x0))) by Th22;
hence ((f * (reproj ((In (i0,(dom G))),x))) /. y) - ((f * (reproj ((In (i0,(dom G))),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) by A26, FUNCT_2:15; :: thesis: verum

end;

hence f is_partial_differentiable_in x,i0 by A17, NDIFF_1:def 6; :: thesis: partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G))))
f * (reproj ((In (i0,(dom G))),x)) is_differentiable_in x0 by A17, A18, NDIFF_1:def 6;
hence partdiff (f,x,i0) = (diff (f,x)) * (reproj ((In (i0,(dom G))),(0. (product G)))) by A17, A18, NDIFF_1:def 7; :: thesis: verum