let G be non-trivial RealNormSpace-Sequence; :: thesis:
let F be non trivial 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;
CG2: dom G = Seg (len G) by FINSEQ_1:def 3;

hereby :: thesis:

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

A3: now

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 A2, CG2;
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;

V1: 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 A2;
then A4: X c= dom f by Def19;
for x being Point of (product G) st x in X holds
f is_differentiable_in x by A1, A2, Th48X;
hence A5: f is_differentiable_on X by A1, A4, NDIFF_1:31; :: thesis:
then A6: 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 A7: ( 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)) ) );

A8: now

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
A9: ( 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 A7, A3;
reconsider s = s as Element of REAL ;
take s = s; :: thesis:
thus S₁[i,s] by A9; :: thesis:

end;

consider S being FinSequence of REAL such that
A10: ( 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(A8);
take s = min S; :: thesis:
A11: len S = len G by A10, FINSEQ_1:def 3;
then min_p S in dom S by RFINSEQ2:def 2;
hence s > 0 by A10; :: thesis:
let y1 be Point of (product G); :: thesis:
assume A12: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis:
reconsider DD = (diff (f,y1)) - (diff (f,y0)) as bounded LinearOperator of (product G),F by LOPBAN_1:def 9;
A13: upper_bound (PreNorms DD) = ||.((diff (f,y1)) - (diff (f,y0))).|| by LOPBAN_1:30;

now

let mt be real number ; :: thesis:
assume mt in PreNorms DD ; :: thesis:
then consider t being VECTOR of (product G) such that
A14: ( mt = ||.(DD . t).|| & ||.t.|| <= 1 ) ;
consider w0 being FinSequence of F such that
A15: ( dom w0 = dom G & ( for i being set st i in dom G holds
w0 . i = (partdiff (f,y0,i)) . ((proj (modetrans (G,i))) . t) ) & (diff (f,y0)) . t = Sum w0 ) by A1, A2, Th48X, A7;
reconsider Sw0 = Sum w0 as Point of F ;
consider w1 being FinSequence of F such that
A16: ( dom w1 = dom G & ( for i being set st i in dom G holds
w1 . i = (partdiff (f,y1,i)) . ((proj (modetrans (G,i))) . t) ) & (diff (f,y1)) . t = Sum w1 ) by A1, A2, Th48X, A12;
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
A17: ( len w2 = len G & ( for i being Nat st i in dom w2 holds
w2 . i = H₁(i) ) ) from FINSEQ_2:sch 1();
A18: ( len w1 = len G & len w0 = len G ) by CG2, A15, A16, FINSEQ_1:def 3;

now

let i be Element of NAT ; :: thesis:
assume i in dom w1 ; :: thesis:
then i in dom w2 by A17, CG2, A16, FINSEQ_1:def 3;
hence w2 . i = H₁(i) by A17; :: thesis:

end;

then Sum w2 = (Sum w1) - (Sum w0) by A17, A18, RLVECT_2:5;
then A21: mt = ||.(Sum w2).|| by A14, A16, A15, LOPBAN_1:40;
deffunc H₂( Nat) -> Element of REAL = ||.(w2 /. $1).||;
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

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

end;

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

now

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

end;

then A270: rng rs c= {rm} by TARSKI:def 3;

now

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

end;

then {rm} c= rng rs by TARSKI:def 3;
then {rm} = rng rs by A270, XBOOLE_0:def 10;
then rs = (len G) |-> (r / (2 * (len G))) by A27, 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

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 A15, A16, A17, 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 A26, A32, FINSEQ_1:def 3;
reconsider p1 = partdiff (f,y1,i), p0 = partdiff (f,y0,i) as bounded LinearOperator of (G . (modetrans (G,i))),F by LOPBAN_1:def 9;
reconsider P1 = p1 . ((proj (modetrans (G,i))) . t) as VECTOR of F ;
reconsider P0 = p0 . ((proj (modetrans (G,i))) . 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 CG2, A15, A16, A32;
then A40: w2 . i = P1 - P0 by A33, A17;
( 1 <= i & i <= len S ) by A11, A32, FINSEQ_1:1;
then A41: ( s <= S . i & f is_partial_differentiable_on X,i ) by CG2, A32, A2, RFINSEQ2:2;
then ||.(y1 - y0).|| < S . i by A12, XXREAL_0:2;
then ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G)) by A10, A32, A12;
then ||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r / (2 * (len G)) by Def19f, A12, A41, CG2, A32;
then A42: ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r / (2 * (len G)) by Def19f, A7, A41, CG2, A32;
reconsider PP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as bounded LinearOperator of (G . (modetrans (G,i))),F by LOPBAN_1:def 9;
A43: upper_bound (PreNorms PP) = ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| by LOPBAN_1:30;
reconsider pt = (proj (modetrans (G,i))) . t as VECTOR of (G . (modetrans (G,i))) ;
A44: PP . pt = P1 - P0 by LOPBAN_1:40;
||.pt.|| <= ||.t.|| by XTh50;
then ||.pt.|| <= 1 by A14, 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 A44, A42, A43, XXREAL_0:2;
hence ys . i <= rs . i by A34, A26, A35, A40; :: thesis:

end;

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

end;

then ( ||.((diff (f,y1)) - (diff (f,y0))).|| <= r / 2 & r / 2 < r ) by A13, A7, 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 A5, A7, NDIFF_1:def 9;
hence ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A5, A12, NDIFF_1:def 9; :: thesis:

end;

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

end;

assume A52: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis:
then A53: ( 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 A540: i in dom G ; :: thesis:
then reconsider i0 = i as Element of NAT ;

now

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

end;

then for x being Point of (product G) st x in X holds
f is_partial_differentiable_in x,i ;
hence A55: f is_partial_differentiable_on X,i by A1, XTh8, A53; :: thesis:
then A56: dom (f `partial| (X,i)) = X by Def19f, A540;
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 A57: ( y0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A58: ( 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 A52, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A58; :: thesis:
let y1 be Point of (product G); :: thesis:
assume A59: ( y1 in X & ||.(y1 - y0).|| < s ) ; :: thesis:
then ||.(((f `| X) /. y1) - ((f `| X) /. y0)).|| < r by A58;
then ||.((diff (f,y1)) - ((f `| X) /. y0)).|| < r by A59, A52, NDIFF_1:def 9;
then A60: ||.((diff (f,y1)) - (diff (f,y0))).|| < r by A57, A52, NDIFF_1:def 9;
( f is_differentiable_in y1 & f is_differentiable_in y0 ) by A52, A1, A59, A57, NDIFF_1:31;
then A61: ( partdiff (f,y1,i) = (diff (f,y1)) * (reproj ((modetrans (G,i)),(0. (product G)))) & partdiff (f,y0,i) = (diff (f,y0)) * (reproj ((modetrans (G,i)),(0. (product G)))) ) by Th21X;
reconsider PP = (partdiff (f,y1,i)) - (partdiff (f,y0,i)) as bounded LinearOperator of (G . (modetrans (G,i))),F by LOPBAN_1:def 9;
reconsider DD = (diff (f,y1)) - (diff (f,y0)) as bounded LinearOperator of (product G),F by LOPBAN_1:def 9;
A62: ( 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;
A64: ( PreNorms PP is bounded_above & PreNorms DD is bounded_above ) by LOPBAN_1:28;

now

let a be set ; :: thesis:
assume a in PreNorms PP ; :: thesis:
then consider t being VECTOR of (G . (modetrans (G,i))) such that
A65: ( a = ||.(PP . t).|| & ||.t.|| <= 1 ) ;
A66: dom (reproj ((modetrans (G,i)),(0. (product G)))) = the carrier of (G . (modetrans (G,i))) by FUNCT_2:def 1;
reconsider tm = (reproj ((modetrans (G,i)),(0. (product G)))) . t as Point of (product G) ;
A67: ||.tm.|| <= 1 by A65, XTh5;
( (partdiff (f,y1,i)) . t = (diff (f,y1)) . tm & (partdiff (f,y0,i)) . t = (diff (f,y0)) . tm ) by A66, A61, 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 A65, A67; :: thesis:

end;

then PreNorms PP c= PreNorms DD by TARSKI:def 3;
then ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| <= ||.((diff (f,y1)) - (diff (f,y0))).|| by A64, A62, SEQ_4:48;
then ||.((partdiff (f,y1,i)) - (partdiff (f,y0,i))).|| < r by A60, XXREAL_0:2;
then ||.((partdiff (f,y1,i)) - ((f `partial| (X,i)) /. y0)).|| < r by Def19f, A57, A55, A540;
hence ||.(((f `partial| (X,i)) /. y1) - ((f `partial| (X,i)) /. y0)).|| < r by Def19f, A59, A55, A540; :: thesis:

end;

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

end;