let G be RealNormSpace-Sequence; :: thesis:
let S be 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;
A2: dom G = Seg (len G) by FINSEQ_1:def 3;
reconsider Z0 = 0. (product G) as Element of product (carr G) by Th10;
reconsider x0 = x as Element of product (carr G) by Th10;
reconsider x1 = x as len G -element FinSequence ;
reconsider Z1 = 0. (product G) as len G -element FinSequence ;
consider L being Lipschitzian LinearOperator of (product G),S such that
A3: 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 (In (i,(dom G)))) . h) ) & L . h = Sum w ) by Lm5;
A4: 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 (In (i,(dom G)))) . h) ) & L . h = Sum w )

proof

let h be Point of (product G); :: thesis:
consider w being FinSequence of S such that
A5: ( 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 (In (i,(dom G)))) . h) ) & L . h = Sum w ) by A3;
take w ; :: thesis:
thus dom w = dom G by A5, FINSEQ_1:def 3; :: thesis:
thus ( ( for i being set st i in dom G holds
w . i = (partdiff (f,x,i)) . ((proj (In (i,(dom G)))) . h) ) & L . h = Sum w ) by A5, A2; :: thesis:

end;

consider d0 being Real such that
A6: d0 > 0 and
A7: { 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 A7, XBOOLE_1:1;
then A8: { y where y is Element of (product G) : ||.(y - x).|| < d0 } is Neighbourhood of x by A6, NFCONT_1:def 1;
A9: 1 <= len G by NAT_1:14;
then len G in dom G by A2;
then f is_partial_differentiable_on X, len G by A1;
then X c= dom f ;
then A10: { y where y is Element of (product G) : ||.(y - x).|| < d0 } c= dom f by A7;
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
A11: for h being Element of the carrier of (product G) holds R . h = H₁(h) from FUNCT_2:sch 4();

now :: thesis:

let r0 be Real; :: thesis:
assume A12: r0 > 0 ; :: thesis:
set r1 = r0 / 2;
set r = (r0 / 2) / (len G);
defpred S₁[ Nat, 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) ) );
A13: 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 A14: 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 A2, A14, A1;
then consider d being Real such that
A15: ( 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 A12, A1, NFCONT_1:19;
reconsider d = d as Element of REAL by XREAL_0:def 1;
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 A16: ( q in X & ||.(q - x).|| < d ) ; :: thesis:
then A17: ||.(((f `partial| (X,k)) /. q) - ((f `partial| (X,k)) /. x)).|| < (r0 / 2) / (len G) by A15;
A18: f is_partial_differentiable_on X,k by A1, A14, A2;
then (f `partial| (X,k)) /. q = partdiff (f,q,k) by A16, Def9;
hence ||.((partdiff (f,q,k)) - (partdiff (f,x,k))).|| < (r0 / 2) / (len G) by A17, A18, A1, Def9; :: 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 A15; :: thesis:

end;

consider Dseq being FinSequence of REAL such that
A19: ( 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(A13);
len G in Seg (len G) by A9;
then reconsider rDseq = rng Dseq as non empty ext-real-membered set by A19, FUNCT_1:3;
reconsider rDseq = rDseq as non empty ext-real-membered left_end right_end set ;
A20: min rDseq in rng Dseq by XXREAL_2:def 7;
reconsider d1 = min rDseq as Real ;
set d = min (d0,d1);
A21: ( min (d0,d1) <= d0 & min (d0,d1) <= d1 ) by XXREAL_0:17;
consider i1 being object such that
A22: ( i1 in dom Dseq & d1 = Dseq . i1 ) by A20, FUNCT_1:def 3;
reconsider i1 = i1 as Nat by A22;
A23: 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 A19, A22;

A24: now :: thesis:

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

end;

A25: now :: thesis:

let q be Element of (product G); :: thesis:
let i be Element of NAT ; :: thesis:
assume A26: ( ||.(q - x).|| < min (d0,d1) & i in Seg (len G) ) ; :: thesis:
reconsider i0 = i as Nat ;
consider k being Element of NAT such that
A27: ( 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 A19, A26;
Dseq . i0 in rng Dseq by A19, A26, FUNCT_1:3;
then d1 <= Dseq . i0 by XXREAL_2:def 7;
then min (d0,d1) <= Dseq . i0 by A21, XXREAL_0:2;
then ||.(q - x).|| < Dseq . i0 by A26, XXREAL_0:2;
hence ||.((partdiff (f,q,i)) - (partdiff (f,x,i))).|| < (r0 / 2) / (len G) by A24, A26, A27; :: thesis:

end;

take d = min (d0,d1); :: thesis:
thus 0 < d by A6, A22, A23, 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:
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
A30: ( 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 Th45;
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 (In (i,(dom G)))) . y) ) & L . y = Sum w ) by A3;
A32: ( dom (idseq (len G)) = Seg (len G) & rng (idseq (len G)) = Seg (len G) ) ;
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 A32, FINSEQ_5:57;
then reconsider Ri = Rev (idseq (len G)) as Permutation of (dom w) by A31;
A34: ( 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 :: thesis:

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 A39: 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 A40: mk + 1 in Seg (len G) by A39;
(Rev w) . k = w . (((len (idseq (len G))) - k) + 1) by A34, A36, FINSEQ_5:def 3
.= w . ((idseq (len G)) . (((len (idseq (len G))) - k) + 1)) by A40, A34, 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 A41: 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
A42: ( len gw = len G & ( for j being Nat st j in dom gw holds
gw . j = H₂(j) ) ) from FINSEQ_2:sch 1();

A43: now :: thesis:

let j be Nat; :: thesis:
assume j in dom g ; :: thesis:
then j in Seg (len G) by A30, FINSEQ_1:def 3;
then j in dom gw by A42, FINSEQ_1:def 3;
hence gw . j = (g /. j) - ((Rev w) /. j) by A42; :: thesis:

end;

len (Rev w) = len g by A30, A34, FINSEQ_5:def 3;
then Sum gw = (Sum g) - (Sum (Rev w)) by A30, A42, A43, RLVECT_2:5;
then A44: R /. y = Sum gw by A11, A30, A31, A41;
A45: 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 A46: j in dom gw ; :: thesis:
then A47: j in Seg (len G) by A42, FINSEQ_1:def 3;
then A48: j in dom g by A30, FINSEQ_1:def 3;
then A49: g /. j = (f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1)))) by A30;
A50: ( 1 <= j & j <= len G ) by A47, FINSEQ_1:1;
then ( (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 A50, NAT_D:37;
then A52: ((len G) + 1) -' j in Seg (len G) ;
then f is_partial_differentiable_on X,((len G) + 1) -' j by A1, A2;
then A53: ( 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 Th24, A1;
w /. (((len G) + 1) -' j) = w . (((len G) + 1) -' j) by A31, A52, PARTFUN1:def 6;
then A54: w /. (((len G) + 1) -' j) = (partdiff (f,x,(((len G) + 1) -' j))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . y) by A52, A31;

A55: now :: thesis:

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 A56: ||.hj.|| <= ||.y.|| by A30, FINSEQ_3:25;
(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 A56, A28, XXREAL_0:2; :: thesis:

end;

Seg (len G) c= Seg ((len G) + 1) by FINSEQ_1:5, NAT_1:11;
then ( 1 <= j & j <= (len G) + 1 ) by A47, FINSEQ_1:1;
then A57: ||.((x + (h /. j)) - x).|| < d by A55;
1 <= j + 1 by NAT_1:11;
then A58: ||.((x + (h /. (j + 1))) - x).|| < d by A50, A55, XREAL_1:6;
A59: x + (h /. j) = (reproj ((In ((((len G) + 1) -' j),(dom G))),(x + (h /. (j + 1))))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) by Th54, A30, A50;
A60: ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + y)) - ((proj (In ((((len G) + 1) -' j),(dom G)))) . (x + (h /. (j + 1)))) = (proj (In ((((len G) + 1) -' j),(dom G)))) . y by Th55, A30, A50;
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 A25, A52;
then A61: ||.(((f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1))))) - ((partdiff (f,x,(((len G) + 1) -' j))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . y))).|| <= ||.((proj (In ((((len G) + 1) -' j),(dom G)))) . y).|| * ((r0 / 2) / (len G)) by A1, A53, A52, A2, A24, A57, A58, A59, A60, Th53;
A62: ((len G) + 1) -' j = ((len G) + 1) - j by A50, NAT_1:12, XREAL_1:233;
j in Seg (len (Rev w)) by A42, A46, A34, FINSEQ_1:def 3, FINSEQ_5:def 3;
then A63: j in dom (Rev w) by FINSEQ_1:def 3;
then A64: (Rev w) /. j = (Rev w) . j by PARTFUN1:def 6
.= w . (((len G) - j) + 1) by A34, A63, FINSEQ_5:def 3
.= w /. (((len G) + 1) -' j) by A62, A52, A31, PARTFUN1:def 6 ;
A65: gw /. j = gw . j by A46, PARTFUN1:def 6
.= ((f /. (x + (h /. j))) - (f /. (x + (h /. (j + 1))))) - ((partdiff (f,x,(((len G) + 1) -' j))) . ((proj (In ((((len G) + 1) -' j),(dom G)))) . y)) by A54, A49, A64, A48, A43 ;
||.((proj (In ((((len G) + 1) -' j),(dom G)))) . y).|| * ((r0 / 2) / (len G)) <= ||.y.|| * ((r0 / 2) / (len G)) by A12, Th31, XREAL_1:64;
hence ||.(gw /. j).|| <= ||.y.|| * ((r0 / 2) / (len G)) by A65, A61, XXREAL_0:2; :: thesis:

end;

defpred S₂[ set , set ] means $2 = ||.(gw /. $1).||;
A66: 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
A67: ( 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(A66);
A68: len gw = len yseq by A42, A67, FINSEQ_1:def 3;

A69: now :: thesis:

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

end;

reconsider yseq = yseq as Element of REAL (len G) by A68, A42, FINSEQ_2:92;
A70: ||.(Sum gw).|| <= Sum yseq by A69, A68, Th7;
reconsider yr = ||.y.|| * ((r0 / 2) / (len G)) as Element of REAL by XREAL_0:def 1;
for j being Nat st j in Seg (len G) holds
yseq . j <= ((len G) |-> yr) . j

proof

let j be Nat; :: thesis:
assume A71: j in Seg (len G) ; :: thesis:
then j in dom gw by A42, FINSEQ_1:def 3;
then A72: ||.(gw /. j).|| <= ||.y.|| * ((r0 / 2) / (len G)) by A45;
yseq . j = ||.(gw /. j).|| by A67, A71;
hence yseq . j <= ((len G) |-> yr) . j by A71, A72, FINSEQ_2:57; :: thesis:

end;

then Sum yseq <= Sum ((len G) |-> yr) 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 A44, A70, 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 A28, NORMSP_0:def 5, XCMPLX_1:203;
then A73: (||.y.|| ") * ||.(R /. y).|| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A12, XREAL_1:216;
hence (||.y.|| ") * ||.(R /. y).|| < r0 by A73, XXREAL_0:2; :: thesis:

end;

then reconsider R = R as RestFunc 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;
A74: 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 A11;
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 A10, A8, NDIFF_1:def 6;
then diff (f,x) = L by A8, A10, A74, 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 (In (i,(dom G)))) . h) ) & (diff (f,x)) . h = Sum w ) ) ) by A4, A74, A10, A8, NDIFF_1:def 6; :: thesis: