let m, n be non zero Element of NAT ; :: thesis:
let f be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis:
let X be Subset of (REAL-NS m); :: thesis:
assume A1: X is open ; :: thesis:

hereby :: thesis:

assume A2: ( f is_differentiable_on X & f `| X is_continuous_on X ) ; :: thesis:
then A3: X c= dom f by A1, NDIFF_1:31;
thus for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) :: thesis:

let j be Nat; :: thesis:
assume A4: ( 1 <= j & j <= n ) ; :: thesis:
A5: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
rng f c= the carrier of (REAL-NS n) ;
then A6: X c= dom ((Proj (j,n)) * f) by A3, A5, RELAT_1:27;

now :: thesis:

let x0 be Point of (REAL-NS m); :: thesis:
assume x0 in X ; :: thesis:
then f is_differentiable_in x0 by A2, A1, NDIFF_1:31;
hence (Proj (j,n)) * f is_differentiable_in x0 by A4, PDIFF_6:29; :: thesis:

end;

hence A7: (Proj (j,n)) * f is_differentiable_on X by A6, A1, NDIFF_1:31; :: thesis:
then A8: X c= dom (((Proj (j,n)) * f) `| X) by NDIFF_1:def 9;
A9: for x0 being Point of (REAL-NS m) st x0 in X holds
(((Proj (j,n)) * f) `| X) /. x0 = (Proj (j,n)) * ((f `| X) /. x0)

proof

let x0 be Point of (REAL-NS m); :: thesis:
assume A10: x0 in X ; :: thesis:
then A11: f is_differentiable_in x0 by A2, A1, NDIFF_1:31;
thus (((Proj (j,n)) * f) `| X) /. x0 = diff (((Proj (j,n)) * f),x0) by A7, A10, NDIFF_1:def 9
.= (Proj (j,n)) * (diff (f,x0)) by A11, A4, PDIFF_6:28
.= (Proj (j,n)) * ((f `| X) /. x0) by A2, A10, NDIFF_1:def 9 ; :: thesis:

end;

for x0 being Point of (REAL-NS m)
for r being Real st x0 in X & 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r ) )

proof

let x0 be Point of (REAL-NS m); :: thesis:
let r be Real; :: thesis:
assume A12: ( x0 in X & 0 < r ) ; :: thesis:
then consider s being Real such that
A13: ( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r ) ) by A2, NFCONT_1:19;
take s ; :: thesis:
thus 0 < s by A13; :: thesis:
let x1 be Point of (REAL-NS m); :: thesis:
assume A14: ( x1 in X & ||.(x1 - x0).|| < s ) ; :: thesis:
then A15: ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r by A13;
A16: (((Proj (j,n)) * f) `| X) /. x0 = (Proj (j,n)) * ((f `| X) /. x0) by A9, A12;
reconsider p1 = (Proj (j,n)) * ((f `| X) /. x1) as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by Th7, A4;
reconsider p0 = (Proj (j,n)) * ((f `| X) /. x0) as Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))) by Th7, A4;
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| = ||.(p1 - p0).|| by A9, A14, A16;
then ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| <= ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| by Th14, A4;
hence ||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < r by A15, XXREAL_0:2; :: thesis:

end;

hence ((Proj (j,n)) * f) `| X is_continuous_on X by A8, NFCONT_1:19; :: thesis:

end;

assume A17: for j being Nat st 1 <= j & j <= n holds
( (Proj (j,n)) * f is_differentiable_on X & ((Proj (j,n)) * f) `| X is_continuous_on X ) ; :: thesis:
1 <= n by NAT_1:14;
then (Proj (1,n)) * f is_differentiable_on X by A17;
then A18: X c= dom ((Proj (1,n)) * f) by A1, NDIFF_1:31;
A19: dom (Proj (1,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
rng f c= the carrier of (REAL-NS n) ;
then A20: X c= dom f by A18, A19, RELAT_1:27;

A21: now :: thesis:

let x0 be Point of (REAL-NS m); :: thesis:
assume A22: x0 in X ; :: thesis:

now :: thesis:

let j be Nat; :: thesis:
assume ( 1 <= j & j <= n ) ; :: thesis:
then (Proj (j,n)) * f is_differentiable_on X by A17;
hence (Proj (j,n)) * f is_differentiable_in x0 by A22, A1, NDIFF_1:31; :: thesis:

end;

hence f is_differentiable_in x0 by PDIFF_6:29; :: thesis:

end;

hence A23: f is_differentiable_on X by A1, A20, NDIFF_1:31; :: thesis:
then A24: X c= dom (f `| X) by NDIFF_1:def 9;
A25: for x0 being Point of (REAL-NS m)
for j being Element of NAT st x0 in X & 1 <= j & j <= n holds
(Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0

proof

let x0 be Point of (REAL-NS m); :: thesis:
let j be Element of NAT ; :: thesis:
assume A26: ( x0 in X & 1 <= j & j <= n ) ; :: thesis:
then A27: f is_differentiable_in x0 by A21;
A28: (Proj (j,n)) * f is_differentiable_on X by A17, A26;
thus (Proj (j,n)) * ((f `| X) /. x0) = (Proj (j,n)) * (diff (f,x0)) by A26, A23, NDIFF_1:def 9
.= diff (((Proj (j,n)) * f),x0) by A27, A26, PDIFF_6:28
.= (((Proj (j,n)) * f) `| X) /. x0 by A28, A26, NDIFF_1:def 9 ; :: thesis:

end;

for x0 being Point of (REAL-NS m)
for r0 being Real st x0 in X & 0 < r0 holds
ex s being Real st
( 0 < s & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < s holds
||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 ) )

proof

let x0 be Point of (REAL-NS m); :: thesis:
let r0 be Real; :: thesis:
assume A29: ( x0 in X & 0 < r0 ) ; :: thesis:
set r = r0 / 2;
defpred S₁[ set , set ] means ex j being Element of NAT ex sj being Real st
( $2 = sj & $1 = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) );
A30: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S₁[j0,x]

proof

let j0 be Nat; :: thesis:
assume j0 in Seg n ; :: thesis:
then A31: ( 1 <= j0 & j0 <= n ) by FINSEQ_1:1;
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
((Proj (j,n)) * f) `| X is_continuous_on X by A17, A31;
then consider sj being Real such that
A32: ( 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) ) by A29, NFCONT_1:19;
reconsider sj = sj as Element of REAL by XREAL_0:def 1;
0 < sj by A32;
hence ex x being Element of REAL st S₁[j0,x] by A32; :: thesis:

end;

consider s0 being FinSequence of REAL such that
A33: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,s0 . k] ) ) from FINSEQ_1:sch 5(A30);
A34: rng s0 is finite by A33, FINSET_1:8;
n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by A33, FUNCT_1:3;
reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set by A34;
A35: min rs0 in rng s0 by XXREAL_2:def 7;
reconsider s = min rs0 as Real ;
take s ; :: thesis:
consider i1 being object such that
A36: ( i1 in dom s0 & s = s0 . i1 ) by A35, FUNCT_1:def 3;
ex j being Element of NAT ex sj being Real st
( s0 . i1 = sj & i1 = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (j,n)) * f) `| X) /. x1) - ((((Proj (j,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) ) by A33, A36;
hence 0 < s by A36; :: thesis:
let x1 be Point of (REAL-NS m); :: thesis:
assume A37: ( x1 in X & ||.(x1 - x0).|| < s ) ; :: thesis:

now :: thesis:

let j be Element of NAT ; :: thesis:
let p1, p0 be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS m),(REAL-NS 1))); :: thesis:
assume A38: ( p1 = (Proj (j,n)) * ((f `| X) /. x1) & p0 = (Proj (j,n)) * ((f `| X) /. x0) & 1 <= j & j <= n ) ; :: thesis:
then A39: j in Seg n ;
then consider jj being Element of NAT , sj being Real such that
A40: ( s0 . j = sj & jj = j & 0 < sj & ( for x1 being Point of (REAL-NS m) st x1 in X & ||.(x1 - x0).|| < sj holds
||.(((((Proj (jj,n)) * f) `| X) /. x1) - ((((Proj (jj,n)) * f) `| X) /. x0)).|| < (r0 / 2) / n ) ) by A33;
A41: (Proj (j,n)) * ((f `| X) /. x0) = (((Proj (j,n)) * f) `| X) /. x0 by A25, A29, A38;
A42: (Proj (j,n)) * ((f `| X) /. x1) = (((Proj (j,n)) * f) `| X) /. x1 by A25, A37, A38;
sj in rng s0 by A39, A40, A33, FUNCT_1:3;
then s <= sj by XXREAL_2:def 7;
then ||.(x1 - x0).|| < sj by A37, XXREAL_0:2;
hence ||.(p1 - p0).|| <= (r0 / 2) / n by A40, A37, A38, A41, A42; :: thesis:

end;

then ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| <= n * ((r0 / 2) / n) by Th19;
then A43: ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by A29, XREAL_1:216;
hence ||.(((f `| X) /. x1) - ((f `| X) /. x0)).|| < r0 by A43, XXREAL_0:2; :: thesis:

end;

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