let x0 be Real; :: thesis:
let n be non zero Element of NAT ; :: thesis:
let h be PartFunc of REAL,(REAL-NS n); :: thesis:

end;

assume A5: 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 A5;
then A6: x0 in dom ((Proj (1,n)) * h) ;
A7: dom ((Proj (1,n)) * h) c= dom h by RELAT_1:25;
for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s holds
||.((h /. x1) - (h /. x0)).|| < r ) )

let r0 be Real; :: thesis:
set r = r0 / 2;
assume A8: 0 < r0 ; :: thesis:
then A9: 0 < r0 / 2 by XREAL_1:215;
defpred S₁[ set , Real] means ex j being Element of NAT st
( $1 = j & 0 < $2 & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < $2 holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) );
A10: 0 < (r0 / 2) / n by A9, XREAL_1:139;
A11: 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 A12: j0 in Seg n ; :: thesis:
reconsider j = j0 as Element of NAT by ORDINAL1:def 12;
A13: (Proj (j,n)) * h is_continuous_in x0 by A5, A12;
A14: 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 A15: dom ((Proj (j,n)) * h) = dom h by A14, RELAT_1:27;
consider sj being Real such that
A16: ( 0 < sj & ( for x1 being Real st x1 in dom ((Proj (j,n)) * h) & |.(x1 - x0).| < sj holds
||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A13, A10, NFCONT_3:8;
sj in REAL by XREAL_0:def 1;
hence ex x being Element of REAL st S₁[j0,x] by A16, A15; :: thesis:

end;

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

let j be Element of NAT ; :: thesis:
assume ( 1 <= j & j <= n ) ; :: thesis:
then A21: j in Seg n by FINSEQ_1:1;
then consider jj being Element of NAT such that
A22: ( jj = j & 0 < s0 . j & ( for x1 being Real st x1 in dom h & |.(x1 - x0).| < s0 . j holds
||.((((Proj (jj,n)) * h) /. x1) - (((Proj (jj,n)) * h) /. x0)).|| < (r0 / 2) / n ) ) by A17;
s0 . j in rng s0 by A21, A17, FUNCT_1:3;
then s <= s0 . j by XXREAL_2:def 7;
then |.(x1 - x0).| < s0 . j by A20, XXREAL_0:2;
then A23: ||.((((Proj (j,n)) * h) /. x1) - (((Proj (j,n)) * h) /. x0)).|| < (r0 / 2) / n by A22, A20;
A24: dom (Proj (j,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
then A25: ((Proj (j,n)) * h) /. x1 = (Proj (j,n)) /. (h /. x1) by A20, PARTFUN2:4;
((Proj (j,n)) * h) /. x0 = (Proj (j,n)) /. (h /. x0) by A24, A7, A6, PARTFUN2:4;
hence ||.((Proj (j,n)) . ((h /. x1) - (h /. x0))).|| <= (r0 / 2) / n by A23, A25, PDIFF_8:11; :: thesis:

end;

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

end;