end;

assume AS1: for i being Element of NAT st i in Seg n holds
(Proj (i,n)) * h is_continuous_in x0 ; :: thesis:
1 <= n by NAT_1:14;
then 1 in Seg n by FINSEQ_1:1;
then (Proj (1,n)) * h is_continuous_in x0 by AS1;
then U1: x0 in dom ((Proj (1,n)) * h) by NFCONT_3:8;
U2: dom ((Proj (1,n)) * h) c= dom h by RELAT_1:25;
for r being Real st 0 < r holds
ex s being real number st
( 0 < s & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s holds
||.((h /. x1) - (h /. x0)).|| < r ) )

let r0 be Real; :: thesis:
set r = r0 / 2;
assume AX1: 0 < r0 ; :: thesis:
then AX11: 0 < r0 / 2 by XREAL_1:215;
defpred S₁[ set , real number ] means ex j being Element of NAT st
( $1 = j & 0 < $2 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < $2 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) );
BB1: 0 < (r0 / 2) / n by AX11, XREAL_1:139;
BB2: for j0 being Nat st j0 in Seg n holds
ex x being Element of REAL st S₁[j0,x]

let j0 be Nat; :: thesis:
assume BX0: j0 in Seg n ; :: thesis:
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
U3: (Proj (j,n)) * h is_continuous_in x0 by AS1, BX0;
P20: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
rng h c= the carrier of (REAL-NS n) ;
then P21: dom ((Proj (j,n)) * h) = dom h by P20, RELAT_1:27;
consider sj being real number such that
BX3: ( 0 < sj & ( for x1 being real number st x1 in dom ((Proj (j,n)) * h) & abs (x1 - x0) < sj holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by U3, BB1, NFCONT_3:8;
sj is Real by XREAL_0:def 1;
hence ex x being Element of REAL st S₁[j0,x] by BX3, P21; :: thesis:

end;

consider s0 being FinSequence of REAL such that
BB3: ( dom s0 = Seg n & ( for k being Nat st k in Seg n holds
S₁[k,s0 . k] ) ) from FINSEQ_1:sch 5(BB2);
n in Seg n by FINSEQ_1:3;
then reconsider rs0 = rng s0 as non empty ext-real-membered set by BB3, FUNCT_1:3;
rng s0 is finite by BB3, FINSET_1:8;
then reconsider rs0 = rs0 as non empty ext-real-membered left_end right_end set ;
XA19: min rs0 in rng s0 by XXREAL_2:def 7;
then reconsider s = min rs0 as Real ;
take s ; :: thesis:
consider i1 being set such that
XA20: ( i1 in dom s0 & s = s0 . i1 ) by XA19, FUNCT_1:def 3;
ex j being Element of NAT st
( i1 = j & 0 < s0 . i1 & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . i1 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by BB3, XA20;
hence 0 < s by XA20; :: thesis:
let x1 be real number ; :: thesis:
assume BX3: ( x1 in dom h & abs (x1 - x0) < s ) ; :: thesis:

let j be Element of NAT ; :: thesis:
assume ( 1 <= j & j <= n ) ; :: thesis:
then BX1: j in Seg n by FINSEQ_1:1;
then consider jj being Element of NAT such that
BX2: ( jj = j & 0 < s0 . j & ( for x1 being real number st x1 in dom h & abs (x1 - x0) < s0 . j holds
||.((((Proj (jj,n)) * h) /. x1) - (((Proj (jj,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by BB3;
s0 . j in rng s0 by BX1, BB3, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def 7;
then abs (x1 - x0) < s0 . j by BX3, XXREAL_0:2;
then X100: ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n by BX2, BX3;
C0: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
then C1: ((Proj (j,n)) * h) /. x1 = (Proj (j,n)) /. (h /. x1) by BX3, PARTFUN2:4;
((Proj (j,n)) * h) /. x0 = (Proj (j,n)) /. (h /. x0) by C0, U2, U1, PARTFUN2:4;
hence ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n by X100, C1, PDIFF_8:11; :: thesis:

end;

then ||.((h /. x1) - (h /. x0)).|| <= n * ((r0 / 2) / n) by PDIFF_8:16;
then D1: ||.((h /. x1) - (h /. x0)).|| <= r0 / 2 by XCMPLX_1:87;
r0 / 2 < r0 by AX1, XREAL_1:216;
hence ||.((h /. x1) - (h /. x0)).|| < r0 by D1, XXREAL_0:2; :: thesis:

end;