let n be non zero Nat; :: thesis:
let D be n -element FinSequence; :: thesis:
let g be PartFunc of (CarProduct ((Seg n) --> RNS_Real)),RNS_Real; :: thesis:
let f be PartFunc of (CarProduct ((Seg n) --> REAL)),REAL; :: thesis:
assume that
A1: f = g and
A2: g is_continuous_on CarProduct D and
A3: CarProduct D c= dom g and
A4: for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ; :: thesis:
set S = (Seg n) --> RNS_Real;
for i being Nat st i in Seg n holds
D . i is Subset of REAL by A4;
then A5: CarProduct D is Subset of (CarProduct ((Seg n) --> REAL)) by FINSEQ_1:3, Th11;
ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact )

proof

per cases ;

suppose D is non-empty ; :: thesis:

hence ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact ) by A4, MEASUR15:51; :: thesis:

end;

suppose not D is non-empty ; :: thesis:

then A6: CarProduct D = {} by Th6;
reconsider I = CarProduct D as Subset of (CarProduct ((Seg n) --> RNS_Real)) by A5, MEASUR15:42;
I is compact by A6;
hence ex I being Subset of (CarProduct ((Seg n) --> RNS_Real)) st
( I = CarProduct D & I is compact ) ; :: thesis:

end;

then consider E being Subset of (CarProduct ((Seg n) --> RNS_Real)) such that
A7: ( E = CarProduct D & E is compact ) ;
A8: g is_uniformly_continuous_on E by A2, A7, NFCONT_2:10;
let e be Real; :: thesis:
assume 0 < e ; :: thesis:
then consider r0 being Real such that
A9: ( 0 < r0 & ( for z1, z2 being Point of (CarProduct ((Seg n) --> RNS_Real)) st z1 in E & z2 in E & ||.(z1 - z2).|| < r0 holds
||.((g /. z1) - (g /. z2)).|| < e ) ) by A8;
set r1 = r0 / 2;
set r = (r0 / 2) / n;
A10: 0 < r0 / 2 by A9, XREAL_1:215;
A11: r0 / 2 < r0 by A9, XREAL_1:216;
((((r0 / 2) / n) * ((r0 / 2) / n)) * n) * 1 <= ((((r0 / 2) / n) * ((r0 / 2) / n)) * n) * n by A9, NAT_1:14, XREAL_1:64;
then (((r0 / 2) / n) * ((r0 / 2) / n)) * n <= (((r0 / 2) / n) * n) * (((r0 / 2) / n) * n) ;
then (((r0 / 2) / n) * ((r0 / 2) / n)) * n <= (r0 / 2) * (((r0 / 2) / n) * n) by XCMPLX_1:87;
then (((r0 / 2) / n) * ((r0 / 2) / n)) * n <= (r0 / 2) * (r0 / 2) by XCMPLX_1:87;
then sqrt ((((r0 / 2) / n) * ((r0 / 2) / n)) * n) <= sqrt ((r0 / 2) ^2) by A9, SQUARE_1:26;
then sqrt ((((r0 / 2) / n) * ((r0 / 2) / n)) * n) <= r0 / 2 by A9, SQUARE_1:22;
then A12: sqrt ((((r0 / 2) / n) * ((r0 / 2) / n)) * n) < r0 by A11, XXREAL_0:2;
take (r0 / 2) / n ; :: thesis:
thus 0 < (r0 / 2) / n by A10, XREAL_1:139; :: thesis:
let x, y be n -element FinSequence of REAL ; :: thesis:
assume A13: ( PtCarProduct x in CarProduct D & PtCarProduct y in CarProduct D & ( for i being Nat st i in dom D holds
ex xi, yi being Real st
( xi = x . i & yi = y . i & |.(xi - yi).| < (r0 / 2) / n ) ) ) ; :: thesis:
len D = n by CARD_1:def 7;
then A14: dom D = Seg n by FINSEQ_1:def 3;
reconsider z1 = PtCarProduct x, z2 = PtCarProduct y as Point of (CarProduct ((Seg n) --> RNS_Real)) by A5, A13, MEASUR15:42;
( g /. z1 = g . z1 & g /. z2 = g . z2 ) by A13, A3, PARTFUN1:def 6;
then (g /. z1) - (g /. z2) = (f . (PtCarProduct x)) - (f . (PtCarProduct y)) by A1, DUALSP03:4;
then A15: ||.((g /. z1) - (g /. z2)).|| = |.((f . (PtCarProduct x)) - (f . (PtCarProduct y))).| by EUCLID:def 2;
reconsider m = n - 1 as Nat by NAT_1:14, NAT_1:21;
consider pxy being m + 1 -element FinSequence such that
A16: z1 - z2 = PtCarProduct pxy by MEASUR15:24;
consider nrxy being Element of REAL (m + 1) such that
A18: ( ( for i being non zero Nat st i <= m + 1 holds
ex pxyi being Point of (ElmFin (((Seg n) --> RNS_Real),i)) st
( pxyi = pxy . i & nrxy . i = ||.pxyi.|| ) ) & ||.(z1 - z2).|| = |.nrxy.| ) by A16, MEASUR15:26;
for i being Nat st i in dom nrxy holds
( 0 <= nrxy . i & nrxy . i <= (r0 / 2) / n )

proof

let i be Nat; :: thesis:
assume i in dom nrxy ; :: thesis:
then A19: i in Seg (len nrxy) by FINSEQ_1:def 3;
then A20: i in Seg (m + 1) by CARD_1:def 7;
then A21: ( 1 <= i & i <= m + 1 ) by FINSEQ_1:1;
reconsider i1 = i as non zero Nat by A19, FINSEQ_1:1;
consider pxyi being Point of (ElmFin (((Seg n) --> RNS_Real),i1)) such that
A22: ( pxyi = pxy . i & nrxy . i = ||.pxyi.|| ) by A18, A21;
thus 0 <= nrxy . i by A22; :: thesis:
consider pxi, pyi being Point of (ElmFin (((Seg n) --> RNS_Real),i1)) such that
A23: ( pxi = x . i & pyi = y . i & pxi - pyi = pxy . i ) by A21, A16, MEASUR15:25;
((Seg n) --> RNS_Real) . i = RNS_Real by A20, FUNCOP_1:7;
then A24: ElmFin (((Seg n) --> RNS_Real),i1) = RNS_Real by A21, MEASUR15:def 3;
then A25: pxyi = (x . i) - (y . i) by A22, A23, DUALSP03:4;
ex xi, yi being Real st
( xi = x . i & yi = y . i & |.(xi - yi).| < (r0 / 2) / n ) by A13, A14, A20;
hence nrxy . i <= (r0 / 2) / n by A25, A22, A24, EUCLID:def 2; :: thesis:

end;