let n be Element of NAT ; :: thesis:
let e be real positive number ; :: thesis:
let g be continuous Function of I[01] ,(TOP-REAL n); :: thesis:
reconsider e = e as positive Real by XREAL_0:def 1;
A1: dom g = the carrier of I[01] by FUNCT_2:def 1;
consider f being Function of (Closed-Interval-MSpace 0 ,1),(Euclid n) such that
A2: f = g by UNIFORM1:11;
A3: f is uniformly_continuous by A2, UNIFORM1:9;
A4: e / 2 < e by XREAL_1:218;
A5: e / 2 > 0 by XREAL_1:217;
then consider s1 being Real such that
A6: 0 < s1 and
A7: for u1, u2 being Element of (Closed-Interval-MSpace 0 ,1) st dist u1,u2 < s1 holds
dist (f /. u1),(f /. u2) < e / 2 by A3, UNIFORM1:def 1;
set s = min s1,(1 / 2);
A8: 0 <= min s1,(1 / 2) by A6, XXREAL_0:20;
A9: min s1,(1 / 2) <> 0 by A6, XXREAL_0:15;
then A10: 0 < min s1,(1 / 2) by A6, XXREAL_0:20;
A11: min s1,(1 / 2) <= s1 by XXREAL_0:17;
A12: for u1, u2 being Element of (Closed-Interval-MSpace 0 ,1) st dist u1,u2 < min s1,(1 / 2) holds
dist (f /. u1),(f /. u2) < e / 2

proof

let u1, u2 be Element of (Closed-Interval-MSpace 0 ,1); :: thesis:
assume dist u1,u2 < min s1,(1 / 2) ; :: thesis:
then dist u1,u2 < s1 by A11, XXREAL_0:2;
hence dist (f /. u1),(f /. u2) < e / 2 by A7; :: thesis:

end;

min s1,(1 / 2) <= 1 / 2 by XXREAL_0:17;
then A13: 2 / (min s1,(1 / 2)) >= 2 / (1 / 2) by A8, A9, XREAL_1:120;
A14: (min s1,(1 / 2)) / 2 > 0 by A8, A9, XREAL_1:217;
2 / (min s1,(1 / 2)) > 0 by A8, A9, XREAL_1:141;
then reconsider j = [/(2 / (min s1,(1 / 2)))\] as Element of NAT by INT_1:80;
A15: 2 / (min s1,(1 / 2)) <= [/(2 / (min s1,(1 / 2)))\] by INT_1:def 5;
A16: 2 / (min s1,(1 / 2)) <= j by INT_1:def 5;
0 < j by A10, A15, XREAL_1:141;
then A17: 0 + 1 <= j by NAT_1:13;
then A18: 1 in Seg j by FINSEQ_1:3;
A19: 4 <= j by A13, A16, XXREAL_0:2;
(2 / (min s1,(1 / 2))) - j <= 0 by A15, XREAL_1:49;
then 1 + ((2 / (min s1,(1 / 2))) - j) <= 1 + 0 by XREAL_1:8;
then A20: ((min s1,(1 / 2)) / 2) * (1 + ((2 / (min s1,(1 / 2))) - j)) <= ((min s1,(1 / 2)) / 2) * 1 by A14, XREAL_1:66;
defpred S₁[ Nat, set ] means $2 = ((min s1,(1 / 2)) / 2) * ($1 - 1);
A22: for k being Nat st k in Seg j holds
ex x being set st S₁[k,x] ;
consider p being FinSequence such that
A23: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A22);
A24: p . 1 = ((min s1,(1 / 2)) / 2) * (1 - 1) by A18, A23
.= 0 ;
A25: Seg (len p) = Seg j by A23, FINSEQ_1:def 3;
A26: len p = j by A23, FINSEQ_1:def 3;
[/(2 / (min s1,(1 / 2)))\] < (2 / (min s1,(1 / 2))) + 1 by INT_1:def 5;
then [/(2 / (min s1,(1 / 2)))\] - 1 < ((2 / (min s1,(1 / 2))) + 1) - 1 by XREAL_1:11;
then A27: ((min s1,(1 / 2)) / 2) * (j - 1) < ((min s1,(1 / 2)) / 2) * (2 / (min s1,(1 / 2))) by A14, XREAL_1:70;
A28: ((min s1,(1 / 2)) / 2) * (2 / (min s1,(1 / 2))) = (2 * (min s1,(1 / 2))) / (2 * (min s1,(1 / 2))) by XCMPLX_1:77;
2 * (min s1,(1 / 2)) <> 0 by A6, XXREAL_0:15;
then A29: (2 * (min s1,(1 / 2))) / (2 * (min s1,(1 / 2))) = 1 by XCMPLX_1:60;
then A30: 1 - (((min s1,(1 / 2)) / 2) * (j - 1)) = ((min s1,(1 / 2)) / 2) * (1 + ((2 / (min s1,(1 / 2))) - [/(2 / (min s1,(1 / 2)))\])) by A28;
A31: for i being Element of NAT
for r1, r2 being Real st 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) holds
( r1 < r2 & r2 - r1 = (min s1,(1 / 2)) / 2 )

proof

let i be Element of NAT ; :: thesis:
let r1, r2 be Real; :: thesis:
assume A32: ( 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) ) ; :: thesis:
then A33: i in Seg j by A25, FINSEQ_1:3;
A34: i < i + 1 by NAT_1:13;
( 1 < i + 1 & i + 1 <= len p ) by A32, NAT_1:13;
then A35: i + 1 in Seg j by A25, FINSEQ_1:3;
A36: r1 = ((min s1,(1 / 2)) / 2) * (i - 1) by A23, A32, A33;
A37: r2 = ((min s1,(1 / 2)) / 2) * ((i + 1) - 1) by A23, A32, A35;
i - 1 < (i + 1) - 1 by A34, XREAL_1:11;
hence r1 < r2 by A14, A36, A37, XREAL_1:70; :: thesis:
r2 - r1 = (((min s1,(1 / 2)) / 2) * i) - (((min s1,(1 / 2)) / 2) * (i - 1)) by A23, A32, A33, A37;
hence r2 - r1 = (min s1,(1 / 2)) / 2 ; :: thesis:

end;

A38: for i being Element of NAT
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
r1 < 1

proof

let i be Element of NAT ; :: thesis:
let r1 be Real; :: thesis:
assume A39: ( 1 <= i & i <= len p & r1 = p . i ) ; :: thesis:
then i in Seg j by A25, FINSEQ_1:3;
then A40: r1 = ((min s1,(1 / 2)) / 2) * (i - 1) by A23, A39;
i - 1 <= j - 1 by A26, A39, XREAL_1:11;
then ((min s1,(1 / 2)) / 2) * (i - 1) <= ((min s1,(1 / 2)) / 2) * (j - 1) by A14, XREAL_1:66;
hence r1 < 1 by A27, A28, A29, A40, XXREAL_0:2; :: thesis:

end;

A41: for r1 being Real st r1 = p . (len p) holds
1 - r1 <= (min s1,(1 / 2)) / 2

proof

let r1 be Real; :: thesis:
assume A42: r1 = p . (len p) ; :: thesis:
len p in Seg j by A17, A26, FINSEQ_1:3;
hence 1 - r1 <= (min s1,(1 / 2)) / 2 by A20, A23, A26, A30, A42; :: thesis:

end;

rng (p ^ <*1*>) c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (p ^ <*1*>) ; :: thesis:
then consider x being set such that
A43: ( x in dom (p ^ <*1*>) & y = (p ^ <*1*>) . x ) by FUNCT_1:def 5;
A44: dom (p ^ <*1*>) = Seg (len (p ^ <*1*>)) by FINSEQ_1:def 3;
reconsider nx = x as Element of NAT by A43;
A45: ( 1 <= nx & nx <= len (p ^ <*1*>) ) by A43, A44, FINSEQ_1:3;
A46: len (p ^ <*1*>) = (len p) + 1 by FINSEQ_2:19;
then A47: ( 1 <= nx & nx <= (len p) + 1 ) by A43, A44, FINSEQ_1:3;

per cases ;

suppose nx < (len p) + 1 ; :: thesis:

then A48: nx <= len p by NAT_1:13;
then nx in Seg j by A25, A47, FINSEQ_1:3;
then A49: p . nx = ((min s1,(1 / 2)) / 2) * (nx - 1) by A23;
y = p . nx by A43, A45, A48, FINSEQ_1:85;
hence y in REAL by A49; :: thesis:

end;

suppose nx >= (len p) + 1 ; :: thesis:

then nx = (len p) + 1 by A45, A46, XXREAL_0:1;
then y = 1 by A43, FINSEQ_1:59;
hence y in REAL ; :: thesis:

end;

then reconsider h1 = p ^ <*1*> as FinSequence of REAL by FINSEQ_1:def 4;
A50: len h1 = (len p) + 1 by FINSEQ_2:19;
A51: 4 + 1 <= (len p) + 1 by A19, A26, XREAL_1:8;
A52: h1 . 1 = 0 by A17, A24, A26, Lm2;
A53: h1 . (len h1) = 1 by A50, FINSEQ_1:59;
A54: rng p c= [.0 ,1.]

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
assume y in rng p ; :: thesis:
then consider x being set such that
A55: ( x in dom p & y = p . x ) by FUNCT_1:def 5;
A56: x in Seg (len p) by A55, FINSEQ_1:def 3;
reconsider nx = x as Element of NAT by A55;
A57: ( 1 <= nx & nx <= len p ) by A56, FINSEQ_1:3;
A58: p . nx = ((min s1,(1 / 2)) / 2) * (nx - 1) by A23, A55;
then reconsider ry = p . nx as Real ;
A59: ry < 1 by A38, A57;
A60: (min s1,(1 / 2)) / 2 >= 0 by A8;
nx - 1 >= 1 - 1 by A57, XREAL_1:11;
then ry >= 0 by A58, A60;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A55, A59;
hence y in [.0 ,1.] by RCOMP_1:def 1; :: thesis:

end;

A61: rng <*1*> = {1} by FINSEQ_1:55;
1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A62: 1 in [.0 ,1.] by RCOMP_1:def 1;
{1} c= [.0 ,1.]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in {1} ; :: thesis:
hence x in [.0 ,1.] by A62, TARSKI:def 1; :: thesis:

end;

then A63: [.0 ,1.] \/ {1} = [.0 ,1.] by XBOOLE_1:12;
rng h1 = (rng p) \/ {1} by A61, FINSEQ_1:44;
then A64: rng h1 c= [.0 ,1.] \/ {1} by A54, XBOOLE_1:13;
Closed-Interval-TSpace 0 ,1 = TopSpaceMetr (Closed-Interval-MSpace 0 ,1) by TOPMETR:def 8;
then A65: the carrier of I[01] = the carrier of (Closed-Interval-MSpace 0 ,1) by TOPMETR:16, TOPMETR:27
.= [.0 ,1.] by TOPMETR:14 ;
A66: for i being Element of NAT st 1 <= i & i < len h1 holds
h1 /. i < h1 /. (i + 1)

proof

let i be Element of NAT ; :: thesis:
assume A67: ( 1 <= i & i < len h1 ) ; :: thesis:
then A68: i <= len p by A50, NAT_1:13;
A69: i + 1 <= len h1 by A67, NAT_1:13;
A70: 1 < i + 1 by A67, NAT_1:13;

per cases ;

suppose A71: i < len p ; :: thesis:

A72: h1 . i = h1 /. i by A67, FINSEQ_4:24;
A73: h1 . i = p . i by A67, A71, FINSEQ_1:85;
A74: i + 1 <= len p by A71, NAT_1:13;
A75: h1 . (i + 1) = h1 /. (i + 1) by A69, A70, FINSEQ_4:24;
h1 . (i + 1) = p . (i + 1) by A70, A74, FINSEQ_1:85;
hence h1 /. i < h1 /. (i + 1) by A31, A67, A71, A72, A73, A75; :: thesis:

end;

suppose i >= len p ; :: thesis:

then A76: i = len p by A68, XXREAL_0:1;
A77: h1 /. (i + 1) = h1 . (i + 1) by A69, A70, FINSEQ_4:24
.= 1 by A76, FINSEQ_1:59 ;
h1 /. i = h1 . i by A67, FINSEQ_4:24
.= p . i by A67, A68, FINSEQ_1:85 ;
hence h1 /. i < h1 /. (i + 1) by A38, A67, A68, A77; :: thesis:

end;

then A78: h1 is increasing by Lm3;
A79: for i being Element of NAT st 1 <= i & i < len h1 holds
(h1 /. (i + 1)) - (h1 /. i) <= (min s1,(1 / 2)) / 2

proof

let i be Element of NAT ; :: thesis:
assume A80: ( 1 <= i & i < len h1 ) ; :: thesis:
then A81: i <= len p by A50, NAT_1:13;
A82: i + 1 <= len h1 by A80, NAT_1:13;
A83: 1 < i + 1 by A80, NAT_1:13;

per cases ;

suppose A84: i < len p ; :: thesis:

A85: h1 . i = h1 /. i by A80, FINSEQ_4:24;
A86: h1 . i = p . i by A80, A84, FINSEQ_1:85;
A87: i + 1 <= len p by A84, NAT_1:13;
A88: h1 . (i + 1) = h1 /. (i + 1) by A82, A83, FINSEQ_4:24;
h1 . (i + 1) = p . (i + 1) by A83, A87, FINSEQ_1:85;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min s1,(1 / 2)) / 2 by A31, A80, A84, A85, A86, A88; :: thesis:

end;

suppose i >= len p ; :: thesis:

then A89: i = len p by A81, XXREAL_0:1;
A90: h1 /. (i + 1) = h1 . (i + 1) by A82, A83, FINSEQ_4:24
.= 1 by A89, FINSEQ_1:59 ;
h1 /. i = h1 . i by A80, FINSEQ_4:24
.= p . i by A80, A81, FINSEQ_1:85 ;
hence (h1 /. (i + 1)) - (h1 /. i) <= (min s1,(1 / 2)) / 2 by A41, A89, A90; :: thesis:

end;

for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q holds
diameter W < e

proof

let i be Element of NAT ; :: thesis:
let Q be Subset of I[01] ; :: thesis:
let W be Subset of (Euclid n); :: thesis:
assume A91: ( 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q ) ; :: thesis:
then h1 /. i < h1 /. (i + 1) by A66;
then A92: Q <> {} by A91, XXREAL_1:1;
consider x1 being Element of Q;
x1 in Q by A92;
then A93: g . x1 in W by A1, A91, FUNCT_1:def 12;
A94: for x, y being Point of (Euclid n) st x in W & y in W holds
dist x,y <= e / 2

proof

let x, y be Point of (Euclid n); :: thesis:
assume A95: ( x in W & y in W ) ; :: thesis:
then consider x3 being set such that
A96: ( x3 in dom g & x3 in Q & x = g . x3 ) by A91, FUNCT_1:def 12;
reconsider x3 = x3 as Element of (Closed-Interval-MSpace 0 ,1) by A96, Lm1, TOPMETR:16;
consider y3 being set such that
A97: ( y3 in dom g & y3 in Q & y = g . y3 ) by A91, A95, FUNCT_1:def 12;
reconsider y3 = y3 as Element of (Closed-Interval-MSpace 0 ,1) by A97, Lm1, TOPMETR:16;
A98: f . x3 = f /. x3 ;
A99: f . y3 = f /. y3 ;
reconsider r3 = x3 as Real by A91, A96;
reconsider s3 = y3 as Real by A91, A97;
A100: abs (r3 - s3) <= (h1 /. (i + 1)) - (h1 /. i) by A91, A96, A97, UNIFORM1:14;
(h1 /. (i + 1)) - (h1 /. i) <= (min s1,(1 / 2)) / 2 by A79, A91;
then abs (r3 - s3) <= (min s1,(1 / 2)) / 2 by A100, XXREAL_0:2;
then A101: dist x3,y3 <= (min s1,(1 / 2)) / 2 by HEINE:1;
(min s1,(1 / 2)) / 2 < min s1,(1 / 2) by A8, A9, XREAL_1:218;
then dist x3,y3 < min s1,(1 / 2) by A101, XXREAL_0:2;
hence dist x,y <= e / 2 by A2, A12, A96, A97, A98, A99; :: thesis:

end;

then W is bounded by A5, TBSP_1:def 9;
then diameter W <= e / 2 by A93, A94, TBSP_1:def 10;
hence diameter W < e by A4, XXREAL_0:2; :: thesis:

end;

hence ex h being FinSequence of REAL st
( h . 1 = 0 & h . (len h) = 1 & 5 <= len h & rng h c= the carrier of I[01] & h is increasing & ( for i being Element of NAT
for Q being Subset of I[01]
for W being Subset of (Euclid n) st 1 <= i & i < len h & Q = [.(h /. i),(h /. (i + 1)).] & W = g .: Q holds
diameter W < e ) ) by A50, A51, A52, A53, A63, A64, A65, A78; :: thesis: