let n be Element of NAT ; :: thesis:
let e be Real; :: thesis:
let g be Function of I[01] ,(TOP-REAL n); :: thesis:
let p1, p2 be Element of (TOP-REAL n); :: thesis:
A1: dom g = the carrier of I[01] by FUNCT_2:def 1;
A2: TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider h = g as Function of I[01] ,(TopSpaceMetr (Euclid n)) ;
reconsider f = g as Function of (Closed-Interval-MSpace 0 ,1),(Euclid n) by Lm3, EUCLID:71;
assume that
A3: e > 0 and
A4: g is continuous ; :: thesis:
A5: e / 2 > 0 by A3, XREAL_1:217;
h is continuous by A4, A2, PRE_TOPC:63;
then f is uniformly_continuous by Lm1, Th8, TOPMETR:27;
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 A5, Def1;
set s = min s1,(1 / 2);
defpred S₁[ Nat, set ] means $2 = 1 - (((min s1,(1 / 2)) / 2) * ($1 - 1));
A8: 0 <= min s1,(1 / 2) by A6, XXREAL_0:20;
then reconsider j = [/(2 / (min s1,(1 / 2)))\] as Element of NAT by INT_1:80;
A9: 2 / (min s1,(1 / 2)) <= j by INT_1:def 5;
A10: min s1,(1 / 2) <= s1 by XXREAL_0:17;
A11: 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 A10, XXREAL_0:2;
hence dist (f /. u1),(f /. u2) < e / 2 by A7; :: thesis:

end;

A12: 2 / (min s1,(1 / 2)) <= [/(2 / (min s1,(1 / 2)))\] by INT_1:def 5;
then (2 / (min s1,(1 / 2))) - j <= 0 by XREAL_1:49;
then 1 + ((2 / (min s1,(1 / 2))) - j) <= 1 + 0 by XREAL_1:8;
then A13: ((min s1,(1 / 2)) / 2) * (1 + ((2 / (min s1,(1 / 2))) - j)) <= ((min s1,(1 / 2)) / 2) * 1 by A8, XREAL_1:66;
A14: for k being Nat st k in Seg j holds
ex x being set st S₁[k,x] ;
consider p being FinSequence such that
A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A14);
A16: Seg (len p) = Seg j by A15, FINSEQ_1:def 3;
rng (p ^ <*0 *>) c= REAL

proof

let y be set ; :: according to TARSKI:def 3 :: thesis:
A17: len (p ^ <*0 *>) = (len p) + (len <*0 *>) by FINSEQ_1:35
.= (len p) + 1 by FINSEQ_1:57 ;
assume y in rng (p ^ <*0 *>) ; :: thesis:
then consider x being set such that
A18: x in dom (p ^ <*0 *>) and
A19: y = (p ^ <*0 *>) . x by FUNCT_1:def 5;
reconsider nx = x as Element of NAT by A18;
A20: dom (p ^ <*0 *>) = Seg (len (p ^ <*0 *>)) by FINSEQ_1:def 3;
then A21: nx <= len (p ^ <*0 *>) by A18, FINSEQ_1:3;
A22: 1 <= nx by A18, A20, FINSEQ_1:3;
A23: 1 <= nx by A18, A20, FINSEQ_1:3;

now

per cases ;

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

then A24: nx <= len p by NAT_1:13;
then nx in Seg j by A16, A22, FINSEQ_1:3;
then A25: p . nx = 1 - (((min s1,(1 / 2)) / 2) * (nx - 1)) by A15;
y = p . nx by A19, A23, A24, FINSEQ_1:85;
hence y in REAL by A25; :: thesis:

end;

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

then nx = (len p) + 1 by A21, A17, XXREAL_0:1;
then y = 0 by A19, Lm4;
hence y in REAL ; :: thesis:

end;

hence y in REAL ; :: thesis:

end;

then reconsider h1 = p ^ <*0 *> as FinSequence of REAL by FINSEQ_1:def 4;
A26: len h1 = (len p) + (len <*0 *>) by FINSEQ_1:35
.= (len p) + 1 by FINSEQ_1:57 ;
A27: len p = j by A15, FINSEQ_1:def 3;
A28: min s1,(1 / 2) <> 0 by A6, XXREAL_0:15;
then 2 / (min s1,(1 / 2)) >= 2 / (1 / 2) by A8, XREAL_1:120, XXREAL_0:17;
then 4 <= j by A9, XXREAL_0:2;
then A29: 4 + 1 <= (len p) + 1 by A27, XREAL_1:8;
A30: (min s1,(1 / 2)) / 2 > 0 by A8, A28, XREAL_1:217;
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 & r1 - r2 = (min s1,(1 / 2)) / 2 )

proof

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

end;

0 < min s1,(1 / 2) by A6, XXREAL_0:15;
then 0 < j by A12, XREAL_1:141;
then A37: 0 + 1 <= j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:3;
then p . 1 = 1 - (((min s1,(1 / 2)) / 2) * (1 - 1)) by A15
.= 1 ;
then A38: h1 . 1 = 1 by A37, A27, Lm5;
2 * (min s1,(1 / 2)) <> 0 by A6, XXREAL_0:15;
then A39: ( ((min s1,(1 / 2)) / 2) * (2 / (min s1,(1 / 2))) = (2 * (min s1,(1 / 2))) / (2 * (min s1,(1 / 2))) & (2 * (min s1,(1 / 2))) / (2 * (min s1,(1 / 2))) = 1 ) by XCMPLX_1:60, XCMPLX_1:77;
then A40: 1 - (((min s1,(1 / 2)) / 2) * (j - 1)) = ((min s1,(1 / 2)) / 2) * (1 + ((2 / (min s1,(1 / 2))) - [/(2 / (min s1,(1 / 2)))\])) ;
A41: for r1 being Real st r1 = p . (len p) holds
r1 - 0 <= (min s1,(1 / 2)) / 2

proof

let r1 be Real; :: thesis:
assume A42: r1 = p . (len p) ; :: thesis:
len p in Seg j by A37, A27, FINSEQ_1:3;
then r1 = 1 - (((min s1,(1 / 2)) / 2) * ((len p) - 1)) by A15, A42;
hence r1 - 0 <= (min s1,(1 / 2)) / 2 by A13, A15, A40, FINSEQ_1:def 3; :: thesis:

end;

A43: for i being Element of NAT st 1 <= i & i < len h1 holds
(h1 /. i) - (h1 /. (i + 1)) <= (min s1,(1 / 2)) / 2

proof

let i be Element of NAT ; :: thesis:
assume that
A44: 1 <= i and
A45: i < len h1 ; :: thesis:
A46: i + 1 <= len h1 by A45, NAT_1:13;
A47: 1 < i + 1 by A44, NAT_1:13;
A48: i <= len p by A26, A45, NAT_1:13;

now

per cases ;

case A49: i < len p ; :: thesis:

then i + 1 <= len p by NAT_1:13;
then A50: h1 . (i + 1) = p . (i + 1) by A47, FINSEQ_1:85;
A51: h1 . i = p . i by A44, A49, FINSEQ_1:85;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A44, A45, A46, A47, FINSEQ_4:24;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min s1,(1 / 2)) / 2 by A31, A44, A49, A51, A50; :: thesis:

end;

case i >= len p ; :: thesis:

then A52: i = len p by A48, XXREAL_0:1;
A53: h1 /. i = h1 . i by A44, A45, FINSEQ_4:24
.= p . i by A44, A48, FINSEQ_1:85 ;
h1 /. (i + 1) = h1 . (i + 1) by A46, A47, FINSEQ_4:24
.= 0 by A52, Lm4 ;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min s1,(1 / 2)) / 2 by A41, A52, A53; :: thesis:

end;

hence (h1 /. i) - (h1 /. (i + 1)) <= (min s1,(1 / 2)) / 2 ; :: thesis:

end;

[/(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 A54: ((min s1,(1 / 2)) / 2) * (j - 1) < ((min s1,(1 / 2)) / 2) * (2 / (min s1,(1 / 2))) by A30, XREAL_1:70;
A55: for i being Element of NAT
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
0 < r1

proof

let i be Element of NAT ; :: thesis:
let r1 be Real; :: thesis:
assume that
A56: 1 <= i and
A57: i <= len p and
A58: r1 = p . i ; :: thesis:
i - 1 <= j - 1 by A27, A57, XREAL_1:11;
then ((min s1,(1 / 2)) / 2) * (i - 1) <= ((min s1,(1 / 2)) / 2) * (j - 1) by A8, XREAL_1:66;
then ((min s1,(1 / 2)) / 2) * (i - 1) < 1 by A54, A39, XXREAL_0:2;
then A59: 1 - (((min s1,(1 / 2)) / 2) * (i - 1)) > 1 - 1 by XREAL_1:12;
i in Seg j by A16, A56, A57, FINSEQ_1:3;
hence 0 < r1 by A15, A58, A59; :: thesis:

end;

A60: 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 that
A61: 1 <= i and
A62: i < len h1 ; :: thesis:
A63: 1 < i + 1 by A61, NAT_1:13;
A64: i <= len p by A26, A62, NAT_1:13;
A65: i + 1 <= len h1 by A62, NAT_1:13;

now

per cases ;

case A66: i < len p ; :: thesis:

then i + 1 <= len p by NAT_1:13;
then A67: h1 . (i + 1) = p . (i + 1) by A63, FINSEQ_1:85;
A68: h1 . i = p . i by A61, A66, FINSEQ_1:85;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A61, A62, A65, A63, FINSEQ_4:24;
hence h1 /. i > h1 /. (i + 1) by A31, A61, A66, A68, A67; :: thesis:

end;

case i >= len p ; :: thesis:

then A69: i = len p by A64, XXREAL_0:1;
A70: h1 /. i = h1 . i by A61, A62, FINSEQ_4:24
.= p . i by A61, A64, FINSEQ_1:85 ;
h1 /. (i + 1) = h1 . (i + 1) by A65, A63, FINSEQ_4:24
.= 0 by A69, Lm4 ;
hence h1 /. i > h1 /. (i + 1) by A55, A61, A64, A70; :: thesis:

end;

hence h1 /. i > h1 /. (i + 1) ; :: thesis:

end;

A71: e / 2 < e by A3, XREAL_1:218;
A72: 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 + 1)),(h1 /. i).] & 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 that
A73: ( 1 <= i & i < len h1 ) and
A74: Q = [.(h1 /. (i + 1)),(h1 /. i).] and
A75: W = g .: Q ; :: thesis:
h1 /. i > h1 /. (i + 1) by A60, A73;
then A76: Q <> {} by A74, XXREAL_1:1;
A77: 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 that
A78: x in W and
A79: y in W ; :: thesis:
consider x3 being set such that
A80: x3 in dom g and
A81: x3 in Q and
A82: x = g . x3 by A75, A78, FUNCT_1:def 12;
reconsider x3 = x3 as Element of (Closed-Interval-MSpace 0 ,1) by A80, Lm2, TOPMETR:16;
reconsider r3 = x3 as Real by A74, A81;
A83: x = f /. x3 by A82;
consider y3 being set such that
A84: y3 in dom g and
A85: y3 in Q and
A86: y = g . y3 by A75, A79, FUNCT_1:def 12;
reconsider y3 = y3 as Element of (Closed-Interval-MSpace 0 ,1) by A84, Lm2, TOPMETR:16;
reconsider s3 = y3 as Real by A74, A85;
A87: (h1 /. i) - (h1 /. (i + 1)) <= (min s1,(1 / 2)) / 2 by A43, A73;
abs (r3 - s3) <= (h1 /. i) - (h1 /. (i + 1)) by A74, A81, A85, Th14;
then A88: abs (r3 - s3) <= (min s1,(1 / 2)) / 2 by A87, XXREAL_0:2;
( dist x3,y3 = abs (r3 - s3) & (min s1,(1 / 2)) / 2 < min s1,(1 / 2) ) by A8, A28, HEINE:1, XREAL_1:218;
then ( f . y3 = f /. y3 & dist x3,y3 < min s1,(1 / 2) ) by A88, XXREAL_0:2;
hence dist x,y <= e / 2 by A11, A86, A83; :: thesis:

end;

then W is bounded by A5, TBSP_1:def 9;
then diameter W <= e / 2 by A1, A75, A76, A77, TBSP_1:def 10;
hence diameter W < e by A71, XXREAL_0:2; :: thesis:
consider x1 being Element of Q;

end;

0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A89: 0 in [.0 ,1.] by RCOMP_1:def 1;
{0 } c= [.0 ,1.]

proof

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

end;

then A90: [.0 ,1.] \/ {0 } = [.0 ,1.] by XBOOLE_1:12;
Closed-Interval-TSpace 0 ,1 = TopSpaceMetr (Closed-Interval-MSpace 0 ,1) by TOPMETR:def 8;
then A91: the carrier of I[01] = the carrier of (Closed-Interval-MSpace 0 ,1) by TOPMETR:16, TOPMETR:27
.= [.0 ,1.] by TOPMETR:14 ;
A92: 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
A93: x in dom p and
A94: y = p . x by FUNCT_1:def 5;
reconsider nx = x as Element of NAT by A93;
A95: p . nx = 1 - (((min s1,(1 / 2)) / 2) * (nx - 1)) by A15, A93;
then reconsider ry = p . nx as Real ;
A96: x in Seg (len p) by A93, FINSEQ_1:def 3;
then A97: 1 <= nx by FINSEQ_1:3;
then nx - 1 >= 1 - 1 by XREAL_1:11;
then A98: 1 - (((min s1,(1 / 2)) / 2) * (nx - 1)) <= 1 - 0 by A8, XREAL_1:8;
nx <= len p by A96, FINSEQ_1:3;
then 0 < ry by A55, A97;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A94, A95, A98;
hence y in [.0 ,1.] by RCOMP_1:def 1; :: thesis:

end;

rng <*0 *> = {0 } by FINSEQ_1:55;
then rng h1 = (rng p) \/ {0 } by FINSEQ_1:44;
then A99: rng h1 c= [.0 ,1.] \/ {0 } by A92, XBOOLE_1:13;
h1 . (len h1) = 0 by A26, Lm4;
hence ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I[01] & h is decreasing & ( 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 + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) ) by A26, A29, A38, A90, A99, A91, A60, A72, Lm8; :: thesis: