let G be non-trivial RealNormSpace-Sequence; :: thesis: for S being non trivial 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 ((modetrans (G,i)),(0. (product G)))) )
let S be non trivial 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 ((modetrans (G,i)),(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 ((modetrans (G,i)),(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 ((modetrans (G,i)),(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 ((modetrans (G,i0)),(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 ((modetrans (G,i0)),(0. (product G)))) )
set i = modetrans (G,i0);
consider N being Neighbourhood of x such that
A3: ( N c= dom f & ex R being REST 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 REST of (product G),S such that
A4: 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 A3;
consider r0 being Real such that
A5: ( 0 < r0 & { z where z is Point of (product G) : ||.(z - x).|| < r0 } c= N ) by NFCONT_1:def 1;
set u = f * (reproj ((modetrans (G,i0)),x));
reconsider x0 = (proj (modetrans (G,i0))) . x as Point of (G . (modetrans (G,i0))) ;
set Z = 0. (product G);
set Nx0 = { z where z is Point of (G . (modetrans (G,i0))) : ||.(z - x0).|| < r0 } ;

now

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

end;

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

proof

let xi be Element of (G . (modetrans (G,i0))); :: thesis: ( xi in Nx0 implies (reproj ((modetrans (G,i0)),x)) . xi in N )
assume xi in Nx0 ; :: thesis: (reproj ((modetrans (G,i0)),x)) . xi in N
then A7: ex z being Point of (G . (modetrans (G,i0))) st
( xi = z & ||.(z - x0).|| < r0 ) ;
((reproj ((modetrans (G,i0)),x)) . xi) - x = (reproj ((modetrans (G,i0)),(0. (product G)))) . (xi - x0) by XTh6;
then ||.(((reproj ((modetrans (G,i0)),x)) . xi) - x).|| < r0 by XTh5, A7;
then (reproj ((modetrans (G,i0)),x)) . xi in { z where z is Point of (product G) : ||.(z - x).|| < r0 } ;
hence (reproj ((modetrans (G,i0)),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 (product G) by PARTFUN1:def 2;
reconsider R1 = R * (reproj ((modetrans (G,i0)),(0. (product G)))) as PartFunc of (G . (modetrans (G,i0))),S ;
A10: dom (reproj ((modetrans (G,i0)),(0. (product G)))) = the carrier of (G . (modetrans (G,i0))) by FUNCT_2:def 1;
A11: dom R1 = the carrier of (G . (modetrans (G,i0))) 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 (G . (modetrans (G,i0))) st z <> 0. (G . (modetrans (G,i0))) & ||.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 . (modetrans (G,i0))) st z <> 0. (G . (modetrans (G,i0))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) ) )
assume r > 0 ; :: thesis: ex d being Real st
( d > 0 & ( for z being Point of (G . (modetrans (G,i0))) st z <> 0. (G . (modetrans (G,i0))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )
then consider d being Real such that
A12: ( d > 0 & ( for z being Point of (product G) st z <> 0. (product G) & ||.z.|| < d holds
(||.z.|| ") * ||.(R /. z).|| < r ) ) by A8, NDIFF_1:23;
take d ; :: thesis: ( d > 0 & ( for z being Point of (G . (modetrans (G,i0))) st z <> 0. (G . (modetrans (G,i0))) & ||.z.|| < d holds
(||.z.|| ") * ||.(R1 /. z).|| < r ) )

now

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

end;

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

end;

then reconsider R1 = R1 as REST of (G . (modetrans (G,i0))),S by A8, NDIFF_1:23;
reconsider dfx = diff (f,x) as bounded LinearOperator of (product G),S by LOPBAN_1:def 9;
reconsider LD1 = dfx * (reproj ((modetrans (G,i0)),(0. (product G)))) as Function of (G . (modetrans (G,i0))),S ;

A15: now

let x, y be Element of (G . (modetrans (G,i0))); :: thesis: LD1 . (x + y) = (LD1 . x) + (LD1 . y)
LD1 . (x + y) = dfx . ((reproj ((modetrans (G,i0)),(0. (product G)))) . (x + y)) by FUNCT_2:15;
then LD1 . (x + y) = dfx . (((reproj ((modetrans (G,i0)),(0. (product G)))) . x) + ((reproj ((modetrans (G,i0)),(0. (product G)))) . y)) by XTh9;
then LD1 . (x + y) = (dfx . ((reproj ((modetrans (G,i0)),(0. (product G)))) . x)) + (dfx . ((reproj ((modetrans (G,i0)),(0. (product G)))) . y)) by GRCAT_1:def 8;
then LD1 . (x + y) = (LD1 . x) + (dfx . ((reproj ((modetrans (G,i0)),(0. (product G)))) . y)) by FUNCT_2:15;
hence LD1 . (x + y) = (LD1 . x) + (LD1 . y) by FUNCT_2:15; :: thesis: verum

end;

now

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

now

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

end;

then LD1 is bounded by KKK1, LOPBAN_1:def 8;
then reconsider LD1 = LD1 as Point of (R_NormSpace_of_BoundedLinearOperators ((G . (modetrans (G,i0))),S)) by LOPBAN_1:def 9;

now

let s be set ; :: thesis: ( s in (reproj ((modetrans (G,i0)),x)) .: Nx0 implies s in dom f )
assume s in (reproj ((modetrans (G,i0)),x)) .: Nx0 ; :: thesis: s in dom f
then ex t being Element of (G . (modetrans (G,i0))) st
( t in Nx0 & s = (reproj ((modetrans (G,i0)),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 ((modetrans (G,i0)),x)) .: Nx0 c= dom f by TARSKI:def 3;
dom (reproj ((modetrans (G,i0)),x)) = the carrier of (G . (modetrans (G,i0))) by FUNCT_2:def 1;
then A17: Nx0 c= dom (f * (reproj ((modetrans (G,i0)),x))) by A16, FUNCT_3:3;
A18: for y being Point of (G . (modetrans (G,i0))) st y in Nx0 holds
((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))

proof

let y be Point of (G . (modetrans (G,i0))); :: thesis: ( y in Nx0 implies ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) )
assume A19: y in Nx0 ; :: thesis: ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0))
then A20: (reproj ((modetrans (G,i0)),x)) . y in N by A6;
Z1: (reproj ((modetrans (G,i0)),x)) . x0 = x +* ((modetrans (G,i0)),x0) by Def5;
ZZ: the carrier of (product G) = product (carr G) by LM001;
x . (modetrans (G,i0)) = x0 by Def1, ZZ;
then A22: x = x +* ((modetrans (G,i0)),x0) by FUNCT_7:35;
A24: (reproj ((modetrans (G,i0)),x)) . x0 in N by A6, NFCONT_1:4;
(f * (reproj ((modetrans (G,i0)),x))) /. y = (f * (reproj ((modetrans (G,i0)),x))) . y by A19, A17, PARTFUN1:def 6;
then (f * (reproj ((modetrans (G,i0)),x))) /. y = f . ((reproj ((modetrans (G,i0)),x)) . y) by FUNCT_2:15;
then A25: (f * (reproj ((modetrans (G,i0)),x))) /. y = f /. ((reproj ((modetrans (G,i0)),x)) . y) by A20, A3, PARTFUN1:def 6;
R /. ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0)) = R . ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0)) by A9, PARTFUN1:def 6;
then R /. ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0)) = R1 . (y - x0) by A10, FUNCT_1:13;
then A27: R /. ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0)) = R1 /. (y - x0) by A11, PARTFUN1:def 6;
x0 in Nx0 by NFCONT_1:4;
then (f * (reproj ((modetrans (G,i0)),x))) /. x0 = (f * (reproj ((modetrans (G,i0)),x))) . x0 by A17, PARTFUN1:def 6;
then (f * (reproj ((modetrans (G,i0)),x))) /. x0 = f . ((reproj ((modetrans (G,i0)),x)) . x0) by FUNCT_2:15;
then ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (f /. ((reproj ((modetrans (G,i0)),x)) . y)) - (f /. x) by A25, A22, A24, A3, Z1, PARTFUN1:def 6;
then ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = ((diff (f,x)) . (((reproj ((modetrans (G,i0)),x)) . y) - x)) + (R /. (((reproj ((modetrans (G,i0)),x)) . y) - x)) by A4, A19, A6;
then ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (dfx . ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0))) + (R /. (((reproj ((modetrans (G,i0)),x)) . y) - x)) by XTh6;
then ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (dfx . ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0))) + (R /. ((reproj ((modetrans (G,i0)),(0. (product G)))) . (y - x0))) by XTh6;
hence ((f * (reproj ((modetrans (G,i0)),x))) /. y) - ((f * (reproj ((modetrans (G,i0)),x))) /. x0) = (LD1 . (y - x0)) + (R1 /. (y - x0)) by A27, FUNCT_2:15; :: thesis: verum

end;

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