let G be RealNormSpace-Sequence; :: thesis:
let F be RealNormSpace; :: thesis:
let f be PartFunc of (product G),F; :: thesis:
let X be Subset of (product G); :: thesis:
assume A1: X is open ; :: thesis:
set m = len G;
A2: dom G = Seg (len G) by FINSEQ_1:def 3;

hereby :: thesis:

assume A3: 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:

let i be Element of NAT ; :: thesis:
assume ( 1 <= i & i <= len G ) ; :: thesis:
then i in Seg (len G) ;
then f `partial| (X,i) is_continuous_on X by A3, A2;
hence ( X c= dom (f `partial| (X,i)) & ( for y0 being Point of (product G)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) ) ) ) by NFCONT_1:19; :: thesis:

end;

A5: 1 <= len G by NAT_1:14;
then len G in dom G by A2;
then A6: f is_partial_differentiable_on X, len G by A3;
for x being Point of (product G) st x in X holds
f is_differentiable_in x by A1, A3, Th56;
hence A7: f is_differentiable_on X by A1, A6, NDIFF_1:31; :: thesis:
then A8: dom (f `| X) = X by NDIFF_1:def 9;
for y0 being Point of (product G)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) )

proof

let y0 be Point of (product G); :: thesis:
let r be Real; :: thesis:
assume A9: ( y0 in X & 0 < r ) ; :: thesis:
defpred S₁[ Nat, Real] means for i being Element of NAT st i = $1 holds
( 0 < $2 & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < $2 holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G)) ) );

A10: now :: thesis:

let i be Nat; :: thesis:
reconsider j = i as Element of NAT by ORDINAL1:def 12;
assume i in Seg (len G) ; :: thesis:
then ( 1 <= j & j <= len G ) by FINSEQ_1:1;
then consider s being Real such that
A11: ( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,j)) /. y1) - ((f `partial| (X,j)) /. y0)).|| < r / (2 * (len G)) ) ) by A9, A4;
reconsider s = s as Element of REAL by XREAL_0:def 1;
take s = s; :: thesis:
thus S₁[i,s] by A11; :: thesis:

end;

consider S being FinSequence of REAL such that
A12: ( dom S = Seg (len G) & ( for i being Nat st i in Seg (len G) holds
S₁[i,S . i] ) ) from FINSEQ_1:sch 5(A10);
take s = min S; :: thesis:
A13: len S = len G by A12, FINSEQ_1:def 3;
then min_p S in dom S by RFINSEQ2:def 2;
hence s > 0 by A12; :: thesis:
let y1 be Point of (product G); :: thesis:
assume A14: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis:
reconsider DD = (diff (f,y1)) - (diff (f,y0)) as Lipschitzian LinearOperator of (product G),F by LOPBAN_1:def 9;
A15: upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).|| by LOPBAN_1:30;

now :: thesis:

let mt be Real; :: thesis:
assume mt in PreNorms DD ; :: thesis:
then consider t being VECTOR of (product G) such that
A16: ( mt = ||.(DD . t).|| & ||.t.|| <= 1 ) ;
consider w0 being FinSequence of F such that
A17: ( dom w0 = dom G & ( for i being set st i in dom G holds
w0 . i = (partdiff (f,y0,i)) . ((proj (In (i,(dom G)))) . t) ) & (diff (f,y0)) . t = Sum w0 ) by A1, A3, Th56, A9;
reconsider Sw0 = Sum w0 as Point of F ;
consider w1 being FinSequence of F such that
A18: ( dom w1 = dom G & ( for i being set st i in dom G holds
w1 . i = (partdiff (f,y1,i)) . ((proj (In (i,(dom G)))) . t) ) & (diff (f,y1)) . t = Sum w1 ) by A1, A3, Th56, A14;
reconsider Sw1 = Sum w1 as Point of F ;
deffunc H₁( set ) -> Element of the carrier of F = (w1 /. $1) - (w0 /. $1);
consider w2 being FinSequence of F such that
A19: ( len w2 = len G & ( for i being Nat st i in dom w2 holds
w2 . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A20: ( len w1 = len G & len w0 = len G ) by A2, A17, A18, FINSEQ_1:def 3;

now :: thesis:

let i be Nat; :: thesis:
assume i in dom w1 ; :: thesis:
then i in dom w2 by A19, A2, A18, FINSEQ_1:def 3;
hence w2 . i = H₁(i) by A19; :: thesis:

end;

then Sum w2 = (Sum w1) - (Sum w0) by A19, A20, RLVECT_2:5;
then A21: mt = ||.(Sum w2).|| by A16, A18, A17, LOPBAN_1:40;
deffunc H₂( Nat) -> Element of REAL = In (||.(w2 /. $1).||,REAL);
consider ys being FinSequence of REAL such that
A22: ( len ys = len G & ( for j being Nat st j in dom ys holds
ys . j = H₂(j) ) ) from FINSEQ_2:sch 1();

A23: now :: thesis:

let i be Element of NAT ; :: thesis:
assume i in dom w2 ; :: thesis:
then i in Seg (len G) by A19, FINSEQ_1:def 3;
then i in dom ys by A22, FINSEQ_1:def 3;
hence ys . i = H₂(i) by A22
.= ||.(w2 /. i).|| ;
:: thesis:

end;

then A24: ||.(Sum w2).|| <= Sum ys by A19, A22, Th7;
reconsider rm = r / (2 * (len G)) as Element of REAL by XREAL_0:def 1;
deffunc H₃( Nat) -> Element of REAL = rm;
consider rs being FinSequence of REAL such that
A25: ( len rs = len G & ( for j being Nat st j in dom rs holds
rs . j = H₃(j) ) ) from FINSEQ_2:sch 1();
A26: dom rs = Seg (len G) by A25, FINSEQ_1:def 3;

now :: thesis:

let a be object ; :: thesis:
assume a in rng rs ; :: thesis:
then consider b being object such that
A27: ( b in dom rs & a = rs . b ) by FUNCT_1:def 3;
reconsider b = b as Nat by A27;
rs . b = rm by A27, A25;
hence a in {rm} by A27, TARSKI:def 1; :: thesis:

end;

then A28: rng rs c= {rm} ;

now :: thesis:

let a be object ; :: thesis:
assume a in {rm} ; :: thesis:
then A29: a = rm by TARSKI:def 1;
A30: 1 in dom rs by A5, A26;
then a = rs . 1 by A29, A25;
hence a in rng rs by A30, FUNCT_1:3; :: thesis:

end;

then {rm} c= rng rs ;
then rs = (len G) |-> (r / (2 * (len G))) by A26, A28, XBOOLE_0:def 10, FUNCOP_1:9;
then Sum rs = (len G) * (r / (2 * (len G))) by RVSUM_1:80
.= (len G) * ((r / 2) / (len G)) by XCMPLX_1:78 ;
then A31: Sum rs = r / 2 by XCMPLX_1:87;

now :: thesis:

let i be Element of NAT ; :: thesis:
assume i in dom ys ; :: thesis:
then A32: i in Seg (len G) by A22, FINSEQ_1:def 3;
then A33: ( i in dom w2 & i in dom w1 & i in dom w0 ) by A17, A18, A19, FINSEQ_1:def 3;
then A34: ( ys . i = ||.(w2 /. i).|| & w2 /. i = w2 . i ) by A23, PARTFUN1:def 6;
A35: i in dom rs by A25, A32, FINSEQ_1:def 3;
reconsider p1 = partdiff (f,y1,i), p0 = partdiff (f,y0,i) as Lipschitzian LinearOperator of (G . (In (i,(dom G)))),F by LOPBAN_1:def 9;
reconsider P1 = p1 . ((proj (In (i,(dom G)))) . t) as VECTOR of F ;
reconsider P0 = p0 . ((proj (In (i,(dom G)))) . t) as VECTOR of F ;
( w0 /. i = w0 . i & w1 /. i = w1 . i ) by A33, PARTFUN1:def 6;
then ( w0 /. i = P0 & w1 /. i = P1 ) by A2, A17, A18, A32;
then A36: w2 . i = P1 - P0 by A33, A19;
( 1 <= i & i <= len S ) by A13, A32, FINSEQ_1:1;
then A37: ( s <= S . i & f is_partial_differentiable_on X,i ) by A2, A32, A3, RFINSEQ2:2;
then ||.(y1 - y0).|| < S . i by A14, XXREAL_0:2;
then ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G)) by A12, A32, A14;
then ||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G)) by Def9, A14, A37;
then A38: ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r / (2 * (len G)) by Def9, A9, A37;
reconsider PP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as Lipschitzian LinearOperator of (G . (In (i,(dom G)))),F by LOPBAN_1:def 9;
A39: upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| by LOPBAN_1:30;
reconsider pt = (proj (In (i,(dom G)))) . t as VECTOR of (G . (In (i,(dom G)))) ;
A40: PP . pt = P1 - P0 by LOPBAN_1:40;
||.pt.|| <= ||.t.|| by Th31;
then ||.pt.|| <= 1 by A16, XXREAL_0:2;
then ( ||.(PP . pt).|| in PreNorms PP & not PreNorms PP is empty & PreNorms PP is bounded_above ) by LOPBAN_1:27;
then ||.(PP . pt).|| <= upper_bound (PreNorms PP) by SEQ_4:def 1;
then ||.(P1 - P0).|| <= r / (2 * (len G)) by A40, A38, A39, XXREAL_0:2;
hence ys . i <= rs . i by A34, A25, A35, A36; :: thesis:

end;

then Sum ys <= r / 2 by A31, A25, A22, INTEGRA5:3;
hence mt <= r / 2 by A21, A24, XXREAL_0:2; :: thesis:

end;

then ( ||.((diff (f,y1)) - (diff (f,y0))).|| <= r / 2 & r / 2 < r ) by A15, A9, SEQ_4:45, XREAL_1:216;
then ||.((diff (f,y1)) - (diff (f,y0))).|| < r by XXREAL_0:2;
then ||.((diff (f,y1)) - ((f `| X) /. y0)).|| < r by A7, A9, NDIFF_1:def 9;
hence ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A7, A14, NDIFF_1:def 9; :: thesis:

end;

hence f `| X is_continuous_on X by A8, NFCONT_1:19; :: thesis:

end;

assume A41: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis:
then A42: ( X c= dom f & ( for x being Point of (product G) st x in X holds
f is_differentiable_in x ) ) by A1, NDIFF_1:31;
thus 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:

proof

let i be set ; :: thesis:
assume i in dom G ; :: thesis:
then reconsider i0 = i as Element of NAT ;

now :: thesis:

let x be Point of (product G); :: thesis:
assume x in X ; :: thesis:
then f is_differentiable_in x by A41, A1, NDIFF_1:31;
hence ( f is_partial_differentiable_in x,i & partdiff (f,x,i) = (diff (f,x)) * (reproj ((In (i,(dom G))),(0. (product G)))) ) by Th41; :: thesis:

end;

then for x being Point of (product G) st x in X holds
f is_partial_differentiable_in x,i ;
hence A44: f is_partial_differentiable_on X,i by A1, Th32, A42; :: thesis:
then A45: dom (f `partial| (X,i)) = X by Def9;
for y0 being Point of (product G)
for r being Real st y0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r ) )

proof

let y0 be Point of (product G); :: thesis:
let r be Real; :: thesis:
assume A46: ( y0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A47: ( 0 < s & ( for y1 being Point of (product G) st y1 in X & ||.(y1 - y0).|| < s holds
||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r ) ) by A41, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A47; :: thesis:
let y1 be Point of (product G); :: thesis:
assume A48: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis:
then ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A47;
then ||.((diff (f,y1)) - ((f `| X) /. y0)).|| < r by A48, A41, NDIFF_1:def 9;
then A49: ||.((diff (f,y1)) - (diff (f,y0))).|| < r by A46, A41, NDIFF_1:def 9;
( f is_differentiable_in y1 & f is_differentiable_in y0 ) by A41, A1, A48, A46, NDIFF_1:31;
then A50: ( partdiff (f,y1,i) = (diff (f,y1)) * (reproj ((In (i,(dom G))),(0. (product G)))) & partdiff (f,y0,i) = (diff (f,y0)) * (reproj ((In (i,(dom G))),(0. (product G)))) ) by Th41;
reconsider PP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as Lipschitzian LinearOperator of (G . (In (i,(dom G)))),F by LOPBAN_1:def 9;
reconsider DD = (diff (f,y1)) - (diff (f,y0)) as Lipschitzian LinearOperator of (product G),F by LOPBAN_1:def 9;
A51: ( upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| & upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).|| ) by LOPBAN_1:30;
A52: ( PreNorms PP is bounded_above & PreNorms DD is bounded_above ) by LOPBAN_1:28;

now :: thesis:

let a be object ; :: thesis:
assume a in PreNorms PP ; :: thesis:
then consider t being VECTOR of (G . (In (i,(dom G)))) such that
A53: ( a = ||.(PP . t).|| & ||.t.|| <= 1 ) ;
A54: dom (reproj ((In (i,(dom G))),(0. (product G)))) = the carrier of (G . (In (i,(dom G)))) by FUNCT_2:def 1;
reconsider tm = (reproj ((In (i,(dom G))),(0. (product G)))) . t as Point of (product G) ;
A55: ||.tm.|| <= 1 by A53, Th21;
( (partdiff (f,y1,i)) . t = (diff (f,y1)) . tm & (partdiff (f,y0,i)) . t = (diff (f,y0)) . tm ) by A54, A50, FUNCT_1:13;
then ||.(PP . t).|| = ||.(((diff (f,y1)) . tm) - ((diff (f,y0)) . tm)).|| by LOPBAN_1:40;
then ||.(PP . t).|| = ||.(DD . tm).|| by LOPBAN_1:40;
hence a in PreNorms DD by A53, A55; :: thesis:

end;

then PreNorms PP c= PreNorms DD ;
then ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| <= ||.((diff (f,y1)) - (diff (f,y0))).|| by A52, A51, SEQ_4:48;
then ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r by A49, XXREAL_0:2;
then ||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r by Def9, A46, A44;
hence ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by Def9, A48, A44; :: thesis:

end;

hence f `partial| (X,i) is_continuous_on X by A45, NFCONT_1:19; :: thesis:

end;