let n be Element of NAT ; :: thesis: for e being Real
for g being Function of I,()
for p1, p2 being Element of () st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I & h is decreasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )

let e be Real; :: thesis: for g being Function of I,()
for p1, p2 being Element of () st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I & h is decreasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )

let g be Function of I,(); :: thesis: for p1, p2 being Element of () st e > 0 & g is continuous holds
ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I & h is decreasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )

let p1, p2 be Element of (); :: thesis: ( e > 0 & g is continuous implies ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I & h is decreasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) ) )

A1: dom g = the carrier of I by FUNCT_2:def 1;
A2: TopStruct(# the carrier of (), the topology of () #) = TopSpaceMetr () by EUCLID:def 8;
then reconsider h = g as Function of I,() ;
reconsider f = g as Function of (),() by ;
assume that
A3: e > 0 and
A4: g is continuous ; :: thesis: ex h being FinSequence of REAL st
( h . 1 = 1 & h . (len h) = 0 & 5 <= len h & rng h c= the carrier of I & h is decreasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) )

A5: e / 2 > 0 by ;
h is continuous by ;
then f is uniformly_continuous by ;
then consider s1 being Real such that
A6: 0 < s1 and
A7: for u1, u2 being Element of () st dist (u1,u2) < s1 holds
dist ((f /. u1),(f /. u2)) < e / 2 by A5;
set s = min (s1,(1 / 2));
defpred S1[ Nat, object ] means \$2 = 1 - (((min (s1,(1 / 2))) / 2) * (\$1 - 1));
A8: 0 <= min (s1,(1 / 2)) by ;
then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Element of NAT by INT_1:53;
A9: 2 / (min (s1,(1 / 2))) <= j by INT_1:def 7;
A10: min (s1,(1 / 2)) <= s1 by XXREAL_0:17;
A11: for u1, u2 being Element of () st dist (u1,u2) < min (s1,(1 / 2)) holds
dist ((f /. u1),(f /. u2)) < e / 2
proof
let u1, u2 be Element of (); :: thesis: ( dist (u1,u2) < min (s1,(1 / 2)) implies dist ((f /. u1),(f /. u2)) < e / 2 )
assume dist (u1,u2) < min (s1,(1 / 2)) ; :: thesis: dist ((f /. u1),(f /. u2)) < e / 2
then dist (u1,u2) < s1 by ;
hence dist ((f /. u1),(f /. u2)) < e / 2 by A7; :: thesis: verum
end;
A12: 2 / (min (s1,(1 / 2))) <= [/(2 / (min (s1,(1 / 2))))\] by INT_1:def 7;
then (2 / (min (s1,(1 / 2)))) - j <= 0 by XREAL_1:47;
then 1 + ((2 / (min (s1,(1 / 2)))) - j) <= 1 + 0 by XREAL_1:6;
then A13: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by ;
A14: for k being Nat st k in Seg j holds
ex x being object st S1[k,x] ;
consider p being FinSequence such that
A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds
S1[k,p . k] ) ) from A16: Seg (len p) = Seg j by ;
rng () c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng () or y in REAL )
A17: len () = (len p) + () by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
assume y in rng () ; :: thesis:
then consider x being object such that
A18: x in dom () and
A19: y = () . x by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A18;
A20: dom () = Seg (len ()) by FINSEQ_1:def 3;
then A21: nx <= len () by ;
A22: 1 <= nx by ;
A23: 1 <= nx by ;
now :: thesis: ( ( nx < (len p) + 1 & y in REAL ) or ( nx >= (len p) + 1 & y in REAL ) )
per cases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ;
case nx < (len p) + 1 ; :: thesis:
then A24: nx <= len p by NAT_1:13;
then nx in Seg j by ;
then A25: p . nx = 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) by A15;
y = p . nx by ;
hence y in REAL by ; :: thesis: verum
end;
case nx >= (len p) + 1 ; :: thesis:
then nx = (len p) + 1 by ;
then y = In (0,REAL) by ;
hence y in REAL ; :: thesis: verum
end;
end;
end;
hence y in REAL ; :: thesis: verum
end;
then reconsider h1 = p ^ as FinSequence of REAL by FINSEQ_1:def 4;
A26: len h1 = (len p) + () by FINSEQ_1:22
.= (len p) + 1 by FINSEQ_1:40 ;
A27: len p = j by ;
A28: min (s1,(1 / 2)) <> 0 by ;
then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by ;
then 4 <= j by ;
then A29: 4 + 1 <= (len p) + 1 by ;
A30: (min (s1,(1 / 2))) / 2 > 0 by ;
A31: for i being 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 Nat; :: thesis: 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 )

let r1, r2 be Real; :: thesis: ( 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) implies ( r1 > r2 & r1 - r2 = (min (s1,(1 / 2))) / 2 ) )
assume that
A32: ( 1 <= i & i < len p ) and
A33: r1 = p . i and
A34: r2 = p . (i + 1) ; :: thesis: ( r1 > r2 & r1 - r2 = (min (s1,(1 / 2))) / 2 )
i in Seg j by ;
then A35: r1 = 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) by ;
( 1 < i + 1 & i + 1 <= len p ) by ;
then i + 1 in Seg j by ;
then A36: r2 = 1 - (((min (s1,(1 / 2))) / 2) * ((i + 1) - 1)) by ;
i < i + 1 by NAT_1:13;
then i - 1 < (i + 1) - 1 by XREAL_1:9;
then ((min (s1,(1 / 2))) / 2) * (i - 1) < ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by ;
hence r1 > r2 by ; :: thesis: r1 - r2 = (min (s1,(1 / 2))) / 2
thus r1 - r2 = (min (s1,(1 / 2))) / 2 by ; :: thesis: verum
end;
0 < min (s1,(1 / 2)) by ;
then 0 < j by ;
then A37: 0 + 1 <= j by NAT_1:13;
then 1 in Seg j by FINSEQ_1:1;
then p . 1 = 1 - (((min (s1,(1 / 2))) / 2) * (1 - 1)) by A15
.= 1 ;
then A38: h1 . 1 = 1 by ;
2 * (min (s1,(1 / 2))) <> 0 by ;
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 ;
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 by ;
A42: for i being Nat st 1 <= i & i < len h1 holds
(h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
proof
let i be Nat; :: thesis: ( 1 <= i & i < len h1 implies (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 )
assume that
A43: 1 <= i and
A44: i < len h1 ; :: thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
A45: i + 1 <= len h1 by ;
A46: 1 < i + 1 by ;
A47: i <= len p by ;
now :: thesis: ( ( i < len p & (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 ) or ( i >= len p & (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 ) )
per cases ( i < len p or i >= len p ) ;
case A48: i < len p ; :: thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
then i + 1 <= len p by NAT_1:13;
then A49: h1 . (i + 1) = p . (i + 1) by ;
A50: h1 . i = p . i by ;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by ;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A31, A43, A48, A50, A49; :: thesis: verum
end;
case i >= len p ; :: thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
then A51: i = len p by ;
A52: h1 /. i = h1 . i by
.= p . i by ;
h1 /. (i + 1) = h1 . (i + 1) by
.= 0 by ;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by ; :: thesis: verum
end;
end;
end;
hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 ; :: thesis: verum
end;
[/(2 / (min (s1,(1 / 2))))\] < (2 / (min (s1,(1 / 2)))) + 1 by INT_1:def 7;
then [/(2 / (min (s1,(1 / 2))))\] - 1 < ((2 / (min (s1,(1 / 2)))) + 1) - 1 by XREAL_1:9;
then A53: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by ;
A54: for i being Nat
for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
0 < r1
proof
let i be Nat; :: thesis: for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds
0 < r1

let r1 be Real; :: thesis: ( 1 <= i & i <= len p & r1 = p . i implies 0 < r1 )
assume that
A55: 1 <= i and
A56: i <= len p and
A57: r1 = p . i ; :: thesis: 0 < r1
i - 1 <= j - 1 by ;
then ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by ;
then ((min (s1,(1 / 2))) / 2) * (i - 1) < 1 by ;
then A58: 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) > 1 - 1 by XREAL_1:10;
i in Seg j by ;
hence 0 < r1 by ; :: thesis: verum
end;
A59: for i being Nat st 1 <= i & i < len h1 holds
h1 /. i > h1 /. (i + 1)
proof
let i be Nat; :: thesis: ( 1 <= i & i < len h1 implies h1 /. i > h1 /. (i + 1) )
assume that
A60: 1 <= i and
A61: i < len h1 ; :: thesis: h1 /. i > h1 /. (i + 1)
A62: 1 < i + 1 by ;
A63: i <= len p by ;
A64: i + 1 <= len h1 by ;
now :: thesis: ( ( i < len p & h1 /. i > h1 /. (i + 1) ) or ( i >= len p & h1 /. i > h1 /. (i + 1) ) )
per cases ( i < len p or i >= len p ) ;
case A65: i < len p ; :: thesis: h1 /. i > h1 /. (i + 1)
then i + 1 <= len p by NAT_1:13;
then A66: h1 . (i + 1) = p . (i + 1) by ;
A67: h1 . i = p . i by ;
( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by ;
hence h1 /. i > h1 /. (i + 1) by A31, A60, A65, A67, A66; :: thesis: verum
end;
case i >= len p ; :: thesis: h1 /. i > h1 /. (i + 1)
then A68: i = len p by ;
A69: h1 /. i = h1 . i by
.= p . i by ;
h1 /. (i + 1) = h1 . (i + 1) by
.= 0 by ;
hence h1 /. i > h1 /. (i + 1) by A54, A60, A63, A69; :: thesis: verum
end;
end;
end;
hence h1 /. i > h1 /. (i + 1) ; :: thesis: verum
end;
A70: e / 2 < e by ;
A71: for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h1 & Q = [.(h1 /. (i + 1)),(h1 /. i).] & W = g .: Q holds
diameter W < e
proof
let i be Nat; :: thesis: for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h1 & Q = [.(h1 /. (i + 1)),(h1 /. i).] & W = g .: Q holds
diameter W < e

let Q be Subset of I; :: thesis: for W being Subset of () st 1 <= i & i < len h1 & Q = [.(h1 /. (i + 1)),(h1 /. i).] & W = g .: Q holds
diameter W < e

let W be Subset of (); :: thesis: ( 1 <= i & i < len h1 & Q = [.(h1 /. (i + 1)),(h1 /. i).] & W = g .: Q implies diameter W < e )
assume that
A72: ( 1 <= i & i < len h1 ) and
A73: Q = [.(h1 /. (i + 1)),(h1 /. i).] and
A74: W = g .: Q ; :: thesis:
h1 /. i > h1 /. (i + 1) by ;
then A75: Q <> {} by ;
A76: for x, y being Point of () st x in W & y in W holds
dist (x,y) <= e / 2
proof
let x, y be Point of (); :: thesis: ( x in W & y in W implies dist (x,y) <= e / 2 )
assume that
A77: x in W and
A78: y in W ; :: thesis: dist (x,y) <= e / 2
consider x3 being object such that
A79: x3 in dom g and
A80: x3 in Q and
A81: x = g . x3 by ;
reconsider x3 = x3 as Element of () by ;
reconsider r3 = x3 as Real by ;
A82: x = f /. x3 by A81;
consider y3 being object such that
A83: y3 in dom g and
A84: y3 in Q and
A85: y = g . y3 by ;
reconsider y3 = y3 as Element of () by ;
reconsider s3 = y3 as Real by ;
A86: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by ;
|.(r3 - s3).| <= (h1 /. i) - (h1 /. (i + 1)) by ;
then A87: |.(r3 - s3).| <= (min (s1,(1 / 2))) / 2 by ;
( dist (x3,y3) = |.(r3 - s3).| & (min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) ) by ;
then ( f . y3 = f /. y3 & dist (x3,y3) < min (s1,(1 / 2)) ) by ;
hence dist (x,y) <= e / 2 by ; :: thesis: verum
end;
then W is bounded by ;
then diameter W <= e / 2 by ;
hence diameter W < e by ; :: thesis: verum
end;
0 in { r where r is Real : ( 0 <= r & r <= 1 ) } ;
then A88: 0 in [.0,1.] by RCOMP_1:def 1;
{0} c= [.0,1.] by ;
then A89: [.0,1.] \/ = [.0,1.] by XBOOLE_1:12;
Closed-Interval-TSpace (0,1) = TopSpaceMetr () by TOPMETR:def 7;
then A90: the carrier of I = the carrier of () by
.= [.0,1.] by TOPMETR:10 ;
A91: rng p c= [.0,1.]
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng p or y in [.0,1.] )
assume y in rng p ; :: thesis: y in [.0,1.]
then consider x being object such that
A92: x in dom p and
A93: y = p . x by FUNCT_1:def 3;
reconsider nx = x as Element of NAT by A92;
A94: p . nx = 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) by ;
then reconsider ry = p . nx as Real ;
A95: x in Seg (len p) by ;
then A96: 1 <= nx by FINSEQ_1:1;
then nx - 1 >= 1 - 1 by XREAL_1:9;
then A97: 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) <= 1 - 0 by ;
nx <= len p by ;
then 0 < ry by ;
then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by ;
hence y in [.0,1.] by RCOMP_1:def 1; :: thesis: verum
end;
rng = by FINSEQ_1:38;
then rng h1 = (rng p) \/ by FINSEQ_1:31;
then A98: rng h1 c= [.0,1.] \/ by ;
h1 . (len h1) = 0 by ;
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 & h is decreasing & ( for i being Nat
for Q being Subset of I
for W being Subset of () st 1 <= i & i < len h & Q = [.(h /. (i + 1)),(h /. i).] & W = g .: Q holds
diameter W < e ) ) by A26, A29, A38, A89, A98, A90, A59, A71, Lm8; :: thesis: verum