let G be non-trivial RealNormSpace-Sequence; :: thesis:
let S be non trivial RealNormSpace; :: thesis:
let f be PartFunc of (product G),S; :: thesis:
let X be Subset of (product G); :: thesis:
let x be Point of (product G); :: thesis:
assume A1: ( X is open & x in X & ( for i being set st i in dom G holds
( f is_partial_differentiable_on X,i & f `partial| (X,i) is_continuous_on X ) ) ) ; :: thesis:
set m = len G;
CG2: dom G = Seg (len G) by FINSEQ_1:def 3;
reconsider Z0 = 0. (product G) as Element of product (carr G) by LM001;
reconsider x0 = x as Element of product (carr G) by LM001;
reconsider x1 = x as len G -element FinSequence ;
reconsider Z1 = 0. (product G) as len G -element FinSequence ;
consider L being bounded LinearOperator of (product G),S such that
A2: for h being Point of (product G) ex w being FinSequence of S st
( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w ) by Lm8;
A200: for h being Point of (product G) ex w being FinSequence of S st
( dom w = dom G & ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w )

proof

let h be Point of (product G); :: thesis:
consider w being FinSequence of S such that
X1: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w ) by A2;
take w ; :: thesis:
thus dom w = dom G by X1, FINSEQ_1:def 3; :: thesis:
thus ( ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & L . h = Sum w ) by X1, CG2; :: thesis:

end;

consider d0 being Real such that
A3: d0 > 0 and
A4: { y where y is Element of (product G) : ||.(y - x).|| < d0 } c= X by A1, NDIFF_1:3;
set N = { y where y is Element of (product G) : ||.(y - x).|| < d0 } ;
{ y where y is Element of (product G) : ||.(y - x).|| < d0 } c= the carrier of (product G) by A4, XBOOLE_1:1;
then A300: { y where y is Element of (product G) : ||.(y - x).|| < d0 } is Neighbourhood of x by A3, NFCONT_1:def 1;
A301: 1 <= len G by NAT_1:14;
then len G in dom G by CG2;
then f is_partial_differentiable_on X, len G by A1;
then X c= dom f by Def19;
then A5: { y where y is Element of (product G) : ||.(y - x).|| < d0 } c= dom f by A4, XBOOLE_1:1;
deffunc H₁( Element of (product G)) -> Element of the carrier of S = ((f /. (x + $1)) - (f /. x)) - (L . $1);
consider R being Function of the carrier of (product G), the carrier of S such that
A6: for h being Element of the carrier of (product G) holds R . h = H₁(h) from FUNCT_2:sch 4();

now

let r0 be Real; :: thesis:
assume A9: r0 > 0 ; :: thesis:
set r1 = r0 / 2;
set r = (r0 / 2) / (len G);
defpred S₁[ Nat, Element of REAL ] means ex k being Element of NAT st
( $1 = k & 0 < $2 & ( for q being Element of (product G) st q in X & ||.(q - x).|| < $2 holds
||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G) ) );
A10: for k0 being Nat st k0 in Seg (len G) holds
ex d being Element of REAL st S₁[k0,d]

proof

let k0 be Nat; :: thesis:
assume A11: k0 in Seg (len G) ; :: thesis:
reconsider k = k0 as Element of NAT by ORDINAL1:def 12;
f `partial| (X,k) is_continuous_on X by CG2, A11, A1;
then consider d being Real such that
A13: ( 0 < d & ( for q being Point of (product G) st q in X & ||.(q - x).|| < d holds
||.(((f `partial| (X,k)) /. q) - ((f `partial| (X,k)) /. x)).|| < (r0 / 2) / (len G) ) ) by A9, A1, NFCONT_1:19;
take d ; :: thesis:
for q being Point of (product G) st q in X & ||.(q - x).|| < d holds
||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G)

proof

let q be Point of (product G); :: thesis:
assume A14: ( q in X & ||.(q - x).|| < d ) ; :: thesis:
then A15: ||.(((f `partial| (X,k)) /. q) - ((f `partial| (X,k)) /. x)).|| < (r0 / 2) / (len G) by A13;
A16: f is_partial_differentiable_on X,k by A1, A11, CG2;
then (f `partial| (X,k)) /. q = partdiff (f,q,k) by A14, A11, CG2, Def19f;
hence ||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G) by A15, A16, A1, A11, CG2, Def19f; :: thesis:

end;

hence ex k being Element of NAT st
( k0 = k & 0 < d & ( for q being Element of (product G) st q in X & ||.(q - x).|| < d holds
||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G) ) ) by A13; :: thesis:

end;

consider Dseq being FinSequence of REAL such that
A17: ( dom Dseq = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S₁[i,Dseq . i] ) ) from FINSEQ_1:sch 5(A10);
len G in Seg (len G) by A301;
then reconsider rDseq = rng Dseq as non empty ext-real-membered set by A17, FUNCT_1:3;
reconsider rDseq = rDseq as non empty ext-real-membered left_end right_end set ;
A19: min rDseq in rng Dseq by XXREAL_2:def 7;
then reconsider d1 = min rDseq as Real ;
set d = min (d0,d1);
B1: ( min (d0,d1) <= d0 & min (d0,d1) <= d1 ) by XXREAL_0:17;
consider i1 being set such that
A20: ( i1 in dom Dseq & d1 = Dseq . i1 ) by A19, FUNCT_1:def 3;
reconsider i1 = i1 as Nat by A20;
A21: ex k being Element of NAT st
( i1 = k & 0 < Dseq . i1 & ( for q being Element of (product G) st q in X & ||.(q - x).|| < Dseq . i1 holds
||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G) ) ) by A17, A20;

A22: now

let q be Element of (product G); :: thesis:
assume ||.(q - x).|| < min (d0,d1) ; :: thesis:
then ||.(q - x).|| < d0 by B1, XXREAL_0:2;
then q in { y where y is Element of (product G) : ||.(y - x).|| < d0 } ;
hence q in X by A4; :: thesis:

end;

A24: now

let q be Element of (product G); :: thesis:
let i be Element of NAT ; :: thesis:
assume A25: ( ||.(q - x).|| < min (d0,d1) & i in Seg (len G) ) ; :: thesis:
reconsider i0 = i as Nat ;
consider k being Element of NAT such that
A26: ( i0 = k & 0 < Dseq . i0 & ( for q being Element of (product G) st q in X & ||.(q - x).|| < Dseq . i0 holds
||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G) ) ) by A17, A25;
Dseq . i0 in rng Dseq by A17, A25, FUNCT_1:3;
then d1 <= Dseq . i0 by XXREAL_2:def 7;
then min (d0,d1) <= Dseq . i0 by B1, XXREAL_0:2;
then ||.(q - x).|| < Dseq . i0 by A25, XXREAL_0:2;
hence ||.((partdiff (f,q,i)) - (partdiff (f,x,i))).|| < (r0 / 2) / (len G) by A22, A25, A26; :: thesis:

end;

take d = min (d0,d1); :: thesis:
thus 0 < d by A3, A20, A21, XXREAL_0:21; :: thesis:
thus for y being Point of (product G) st y <> 0. (product G) & ||.y.|| < d holds
(||.y.|| ") * ||.(R /. y).|| < r0 :: thesis:

proof

let y be Point of (product G); :: thesis:
assume A28: ( y <> 0. (product G) & ||.y.|| < d ) ; :: thesis:
then A280: 0 <> ||.y.|| by NORMSP_0:def 5;
set z = R /. y;
consider h being FinSequence of (product G), g being FinSequence of S, Z, y0 being Element of product (carr G) such that
A29: ( y0 = y & Z = 0. (product G) & len h = (len G) + 1 & len g = len G & ( for i being Nat st i in dom h holds
h /. i = Z +* (y0 | (Seg (((len G) + 1) -' i))) ) & ( for i being Nat st i in dom g holds
g /. i = (f /. (x + (h /. i))) - (f /. (x + (h /. (i + 1)))) ) & ( for i being Nat
for hi being Point of (product G) st i in dom h & h /. i = hi holds
||.hi.|| <= ||.y.|| ) & (f /. (x + y)) - (f /. x) = Sum g ) by Th28;
consider w being FinSequence of S such that
A31: ( dom w = Seg (len G) & ( for i being Element of NAT st i in Seg (len G) holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . y) ) & L . y = Sum w ) by A2;
A32: ( dom (idseq (len G)) = Seg (len G) & rng (idseq (len G)) = Seg (len G) ) by FUNCT_2:def 1, FUNCT_2:def 3;
then A33: ( dom (Rev (idseq (len G))) = Seg (len G) & rng (Rev (idseq (len G))) = Seg (len G) ) by FINSEQ_5:57;
then reconsider Ri = Rev (idseq (len G)) as Function of (Seg (len G)),(Seg (len G)) by FUNCT_2:1;
( Ri is one-to-one & Ri is onto ) by A33, FUNCT_2:def 3;
then reconsider Ri = Rev (idseq (len G)) as Permutation of (dom w) by A31;
A39: ( len (idseq (len G)) = len G & len w = len G ) by A31, A32, FINSEQ_1:def 3;
dom (w * Ri) = dom Ri by A33, RELAT_1:27;
then A35: dom (w * Ri) = dom (Rev w) by A33, A31, FINSEQ_5:57;
reconsider wRi = w * Ri as FinSequence of S by FINSEQ_2:47;

now

let k be Nat; :: thesis:
assume A36: k in dom (Rev w) ; :: thesis:
then A37: k in dom (Rev (idseq (len G))) by A33, A31, FINSEQ_5:57;
then A38: ( 1 <= k & k <= len G ) by A33, FINSEQ_1:1;
then reconsider mk = (len G) - k as Nat by NAT_1:21;
reconsider zr0 = 0 as Nat ;
0 <= mk ;
then A40: zr0 + 1 <= ((len G) - k) + 1 by XREAL_1:6;
k - 1 >= 1 - 1 by A38, XREAL_1:9;
then (len G) - (k - 1) <= len G by XREAL_1:43;
then A41: mk + 1 in Seg (len G) by A40;
(Rev w) . k = w . (((len (idseq (len G))) - k) + 1) by A39, A36, FINSEQ_5:def 3
.= w . ((idseq (len G)) . (((len (idseq (len G))) - k) + 1)) by A41, A39, FINSEQ_2:49
.= w . ((Rev (idseq (len G))) . k) by A37, FINSEQ_5:def 3 ;
hence (Rev w) . k = wRi . k by A36, A35, FUNCT_1:12; :: thesis:

end;

then A42: Sum (Rev w) = Sum w by A35, FINSEQ_1:13, RLVECT_2:7;
deffunc H₂( Nat) -> Element of the carrier of S = (g /. $1) - ((Rev w) /. $1);
consider gw being FinSequence of S such that
A43: ( len gw = len G & ( for j being Nat st j in dom gw holds
gw . j = H₂(j) ) ) from FINSEQ_2:sch 1();

A44: now

let j be Element of NAT ; :: thesis:
assume j in dom g ; :: thesis:
then j in Seg (len G) by A29, FINSEQ_1:def 3;
then j in dom gw by A43, FINSEQ_1:def 3;
hence gw . j = (g /. j) - ((Rev w) /. j) by A43; :: thesis:

end;

len (Rev w) = len g by A29, A39, FINSEQ_5:def 3;
then Sum gw = (Sum g) - (Sum (Rev w)) by A29, A43, A44, RLVECT_2:5;
then A47: R /. y = Sum gw by A6, A29, A31, A42;
A48: for j being Element of NAT st j in dom gw holds
||.(gw /. j).|| <= ||.y.|| * ((r0 / 2) / (len G))

proof

let j be Element of NAT ; :: thesis:
assume A49: j in dom gw ; :: thesis:
then A50: j in Seg (len G) by A43, FINSEQ_1:def 3;
then A500: j in dom g by A29, FINSEQ_1:def 3;
then A51: g /. j = (f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1)))) by A29;
A52: ( 1 <= j & j <= len G ) by A50, FINSEQ_1:1;
then A54: ( (len G) + 1 <= (len G) + j & j + 1 <= (len G) + 1 ) by XREAL_1:6;
then ( ((len G) + 1) - j <= len G & 1 <= ((len G) + 1) - j ) by XREAL_1:19, XREAL_1:20;
then ( ((len G) + 1) -' j <= len G & 1 <= ((len G) + 1) -' j ) by A52, NAT_D:37;
then A56: ((len G) + 1) -' j in Seg (len G) ;
then f is_partial_differentiable_on X,((len G) + 1) -' j by A1, CG2;
then A55: ( X c= dom f & ( for x being Element of (product G) st x in X holds
f is_partial_differentiable_in x,((len G) + 1) -' j ) ) by XTh34, A1;
w /. (((len G) + 1) -' j) = w . (((len G) + 1) -' j) by A31, A56, PARTFUN1:def 6;
then A57: w /. (((len G) + 1) -' j) = (partdiff (f,x,(((len G) + 1) -' j))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . y) by A56, A31;

A58: now

let j be Element of NAT ; :: thesis:
reconsider hj = h /. j as Element of (product G) ;
assume ( 1 <= j & j <= (len G) + 1 ) ; :: thesis:
then j in dom h by A29, FINSEQ_3:25;
then A59: ||.hj.|| <= ||.y.|| by A29;
(x + (h /. j)) - x = (h /. j) + (x - x) by RLVECT_1:28
.= (h /. j) + (0. (product G)) by RLVECT_1:15 ;
then (x + (h /. j)) - x = h /. j by RLVECT_1:4;
hence ||.((x + (h /. j)) - x).|| < d by A59, A28, XXREAL_0:2; :: thesis:

end;

len G <= (len G) + 1 by NAT_1:11;
then Seg (len G) c= Seg ((len G) + 1) by FINSEQ_1:5;
then ( 1 <= j & j <= (len G) + 1 ) by A50, FINSEQ_1:1;
then A62: ||.((x + (h /. j)) - x).|| < d by A58;
1 <= j + 1 by NAT_1:11;
then A68: ||.((x + (h /. (j + 1))) - x).|| < d by A54, A58;
A75: x + (h /. j) = (reproj ((modetrans (G,(((len G) + 1) -' j))),(x + (h /. (j + 1))))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) by Th46, A29, A52;
Y5: ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + y)) - ((proj (modetrans (G,(((len G) + 1) -' j)))) . (x + (h /. (j + 1)))) = (proj (modetrans (G,(((len G) + 1) -' j)))) . y by Th46X, A29, A52;
for z being Point of (product G) st ||.(z - x).|| < d holds
||.((partdiff (f,z,(((len G) + 1) -' j))) - (partdiff (f,x,(((len G) + 1) -' j)))).|| <= (r0 / 2) / (len G) by A24, A56;
then XXX: ||.(((f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1))))) - ((partdiff (f,x,(((len G) + 1) -' j))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . y))).|| <= ||.((proj (modetrans (G,(((len G) + 1) -' j)))) . y).|| * ((r0 / 2) / (len G)) by A1, A55, A56, CG2, A22, A62, A68, A75, Y5, XTh45;
A89: ((len G) + 1) -' j = ((len G) + 1) - j by A52, NAT_1:12, XREAL_1:233;
j in Seg (len (Rev w)) by A50, A39, FINSEQ_5:def 3;
then A90: j in dom (Rev w) by FINSEQ_1:def 3;
then A901: (Rev w) /. j = (Rev w) . j by PARTFUN1:def 6
.= w . (((len G) - j) + 1) by A39, A90, FINSEQ_5:def 3
.= w /. (((len G) + 1) -' j) by A89, A56, A31, PARTFUN1:def 6 ;
A92: gw /. j = gw . j by A49, PARTFUN1:def 6
.= ((f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1))))) - ((partdiff (f,x,(((len G) + 1) -' j))) . ((proj (modetrans (G,(((len G) + 1) -' j)))) . y)) by A57, A51, A901, A500, A44 ;
||.((proj (modetrans (G,(((len G) + 1) -' j)))) . y).|| * ((r0 / 2) / (len G)) <= ||.y.|| * ((r0 / 2) / (len G)) by A9, XTh50, XREAL_1:64;
hence ||.(gw /. j).|| <= ||.y.|| * ((r0 / 2) / (len G)) by A92, XXX, XXREAL_0:2; :: thesis:

end;

defpred S₂[ set , set ] means $2 = ||.(gw /. $1).||;
A93: for k being Nat st k in Seg (len G) holds
ex x being Element of REAL st S₂[k,x] ;
consider yseq being FinSequence of REAL such that
A94: ( dom yseq = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S₂[i,yseq . i] ) ) from FINSEQ_1:sch 5(A93);
A95: len gw = len yseq by A43, A94, FINSEQ_1:def 3;

A96: now

let i be Element of NAT ; :: thesis:
assume i in dom gw ; :: thesis:
then i in Seg (len G) by A43, FINSEQ_1:def 3;
hence yseq . i = ||.(gw /. i).|| by A94; :: thesis:

end;

reconsider yseq = yseq as Element of REAL (len G) by A95, A43, FINSEQ_2:92;
A97: ||.(Sum gw).|| <= Sum yseq by A96, A95, PDIFF617;
for j being Nat st j in Seg (len G) holds
yseq . j <= ((len G) |-> (||.y.|| * ((r0 / 2) / (len G)))) . j

proof

let j be Nat; :: thesis:
assume A98: j in Seg (len G) ; :: thesis:
then j in dom gw by A43, FINSEQ_1:def 3;
then A100: ||.(gw /. j).|| <= ||.y.|| * ((r0 / 2) / (len G)) by A48;
yseq . j = ||.(gw /. j).|| by A94, A98;
hence yseq . j <= ((len G) |-> (||.y.|| * ((r0 / 2) / (len G)))) . j by A98, A100, FINSEQ_2:57; :: thesis:

end;

then Sum yseq <= Sum ((len G) |-> (||.y.|| * ((r0 / 2) / (len G)))) by RVSUM_1:82;
then Sum yseq <= (len G) * (||.y.|| * ((r0 / 2) / (len G))) by RVSUM_1:80;
then ||.(R /. y).|| <= (len G) * (||.y.|| * ((r0 / 2) / (len G))) by A47, A97, XXREAL_0:2;
then ||.(R /. y).|| * (||.y.|| ") <= (((len G) * ||.y.||) * ((r0 / 2) / (len G))) * (||.y.|| ") by XREAL_1:64;
then ||.(R /. y).|| * (||.y.|| ") <= (len G) * ((((r0 / 2) / (len G)) * ||.y.||) * (||.y.|| ")) ;
then (||.y.|| ") * ||.(R /. y).|| <= (len G) * ((r0 / 2) / (len G)) by A280, XCMPLX_1:203;
then A101: (||.y.|| ") * ||.(R /. y).|| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A9, XREAL_1:216;
hence (||.y.|| ") * ||.(R /. y).|| < r0 by A101, XXREAL_0:2; :: thesis:

end;

then reconsider R = R as REST of (product G),S by NDIFF_1:23;
reconsider L = L as Point of (R_NormSpace_of_BoundedLinearOperators ((product G),S)) by LOPBAN_1:def 9;
AD0: for y being Point of (product G) st y in { y where y is Element of (product G) : ||.(y - x).|| < d0 } holds
(f /. y) - (f /. x) = (L . (y - x)) + (R /. (y - x))

proof

let y be Point of (product G); :: thesis:
assume y in { y where y is Element of (product G) : ||.(y - x).|| < d0 } ; :: thesis:
y - x in the carrier of (product G) ;
then y - x in dom R by PARTFUN1:def 2;
then R /. (y - x) = R . (y - x) by PARTFUN1:def 6;
then R /. (y - x) = ((f /. (x + (y - x))) - (f /. x)) - (L . (y - x)) by A6;
hence (L . (y - x)) + (R /. (y - x)) = ((f /. (x + (y - x))) - (f /. x)) - ((L . (y - x)) - (L . (y - x))) by RLVECT_1:29
.= ((f /. (x + (y - x))) - (f /. x)) - (0. S) by RLVECT_1:5
.= (f /. (x + (y - x))) - (f /. x) by RLVECT_1:13
.= (f /. (y - (x - x))) - (f /. x) by RLVECT_1:29
.= (f /. (y - (0. (product G)))) - (f /. x) by RLVECT_1:5
.= (f /. y) - (f /. x) by RLVECT_1:13 ;
:: thesis:

end;

then f is_differentiable_in x by A5, A300, NDIFF_1:def 6;
then diff (f,x) = L by A300, A5, AD0, NDIFF_1:def 7;
hence ( f is_differentiable_in x & ( for h being Point of (product G) ex w being FinSequence of S st
( dom w = dom G & ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (modetrans (G,i))) . h) ) & (diff (f,x)) . h = Sum w ) ) ) by A200, AD0, A5, A300, NDIFF_1:def 6; :: thesis: