let n be Element of NAT ; :: thesis: for e being Real

for g being Function of I[01],(TOP-REAL n)

for p1, p2 being Element of (TOP-REAL n) 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[01] & h is decreasing & ( for i being 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 ) )

let e be Real; :: thesis: for g being Function of I[01],(TOP-REAL n)

for p1, p2 being Element of (TOP-REAL n) 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[01] & h is decreasing & ( for i being 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 ) )

let g be Function of I[01],(TOP-REAL n); :: thesis: for p1, p2 being Element of (TOP-REAL n) 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[01] & h is decreasing & ( for i being 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 ) )

let p1, p2 be Element of (TOP-REAL n); :: 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[01] & h is decreasing & ( for i being 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 ) ) )

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:67;

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[01] & h is decreasing & ( for i being 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 ) )

A5: e / 2 > 0 by A3, XREAL_1:215;

h is continuous by A4, A2, PRE_TOPC:33;

then f is uniformly_continuous by Lm1, Th7, TOPMETR:20;

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;

set s = min (s1,(1 / 2));

defpred S_{1}[ Nat, object ] 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: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 (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < min (s1,(1 / 2)) holds

dist ((f /. u1),(f /. u2)) < e / 2

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 A8, XREAL_1:64;

A14: for k being Nat st k in Seg j holds

ex x being object st S_{1}[k,x]
;

consider p being FinSequence such that

A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds

S_{1}[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

A26: len h1 = (len p) + (len <*0*>) by FINSEQ_1:22

.= (len p) + 1 by FINSEQ_1:40 ;

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:118, XXREAL_0:17;

then 4 <= j by A9, XXREAL_0:2;

then A29: 4 + 1 <= (len p) + 1 by A27, XREAL_1:6;

A30: (min (s1,(1 / 2))) / 2 > 0 by A8, A28, XREAL_1:215;

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 )

then 0 < j by A12, XREAL_1:139;

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 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:76;

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 A37, A27, FINSEQ_1:1, A15, A13, A40;

A42: for i being Nat st 1 <= i & i < len h1 holds

(h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2

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 A30, XREAL_1:68;

A54: for i being Nat

for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds

0 < r1

h1 /. i > h1 /. (i + 1)

A71: for i being 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

then A88: 0 in [.0,1.] by RCOMP_1:def 1;

{0} c= [.0,1.] by A88, TARSKI:def 1;

then A89: [.0,1.] \/ {0} = [.0,1.] by XBOOLE_1:12;

Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def 7;

then A90: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20

.= [.0,1.] by TOPMETR:10 ;

A91: rng p c= [.0,1.]

then rng h1 = (rng p) \/ {0} by FINSEQ_1:31;

then A98: rng h1 c= [.0,1.] \/ {0} by A91, 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 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, A89, A98, A90, A59, A71, Lm8; :: thesis: verum

for g being Function of I[01],(TOP-REAL n)

for p1, p2 being Element of (TOP-REAL n) 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[01] & h is decreasing & ( for i being 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 ) )

let e be Real; :: thesis: for g being Function of I[01],(TOP-REAL n)

for p1, p2 being Element of (TOP-REAL n) 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[01] & h is decreasing & ( for i being 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 ) )

let g be Function of I[01],(TOP-REAL n); :: thesis: for p1, p2 being Element of (TOP-REAL n) 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[01] & h is decreasing & ( for i being 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 ) )

let p1, p2 be Element of (TOP-REAL n); :: 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[01] & h is decreasing & ( for i being 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 ) ) )

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:67;

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[01] & h is decreasing & ( for i being 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 ) )

A5: e / 2 > 0 by A3, XREAL_1:215;

h is continuous by A4, A2, PRE_TOPC:33;

then f is uniformly_continuous by Lm1, Th7, TOPMETR:20;

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;

set s = min (s1,(1 / 2));

defpred S

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: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 (Closed-Interval-MSpace (0,1)) st dist (u1,u2) < min (s1,(1 / 2)) holds

dist ((f /. u1),(f /. u2)) < e / 2

proof

A12:
2 / (min (s1,(1 / 2))) <= [/(2 / (min (s1,(1 / 2))))\]
by INT_1:def 7;
let u1, u2 be Element of (Closed-Interval-MSpace (0,1)); :: 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 A10, XXREAL_0:2;

hence dist ((f /. u1),(f /. u2)) < e / 2 by A7; :: thesis: verum

end;assume dist (u1,u2) < min (s1,(1 / 2)) ; :: thesis: dist ((f /. u1),(f /. u2)) < e / 2

then dist (u1,u2) < s1 by A10, XXREAL_0:2;

hence dist ((f /. u1),(f /. u2)) < e / 2 by A7; :: thesis: verum

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 A8, XREAL_1:64;

A14: for k being Nat st k in Seg j holds

ex x being object st S

consider p being FinSequence such that

A15: ( dom p = Seg j & ( for k being Nat st k in Seg j holds

S

A16: Seg (len p) = Seg j by A15, FINSEQ_1:def 3;

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

proof

then reconsider h1 = p ^ <*0*> as FinSequence of REAL by FINSEQ_1:def 4;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (p ^ <*0*>) or y in REAL )

A17: len (p ^ <*0*>) = (len p) + (len <*0*>) by FINSEQ_1:22

.= (len p) + 1 by FINSEQ_1:40 ;

assume y in rng (p ^ <*0*>) ; :: thesis: y in REAL

then consider x being object such that

A18: x in dom (p ^ <*0*>) and

A19: y = (p ^ <*0*>) . x by FUNCT_1:def 3;

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:1;

A22: 1 <= nx by A18, A20, FINSEQ_1:1;

A23: 1 <= nx by A18, A20, FINSEQ_1:1;

end;A17: len (p ^ <*0*>) = (len p) + (len <*0*>) by FINSEQ_1:22

.= (len p) + 1 by FINSEQ_1:40 ;

assume y in rng (p ^ <*0*>) ; :: thesis: y in REAL

then consider x being object such that

A18: x in dom (p ^ <*0*>) and

A19: y = (p ^ <*0*>) . x by FUNCT_1:def 3;

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:1;

A22: 1 <= nx by A18, A20, FINSEQ_1:1;

A23: 1 <= nx by A18, A20, FINSEQ_1:1;

now :: thesis: ( ( nx < (len p) + 1 & y in REAL ) or ( nx >= (len p) + 1 & y in REAL ) )end;

hence
y in REAL
; :: thesis: verumper cases
( nx < (len p) + 1 or nx >= (len p) + 1 )
;

end;

A26: len h1 = (len p) + (len <*0*>) by FINSEQ_1:22

.= (len p) + 1 by FINSEQ_1:40 ;

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:118, XXREAL_0:17;

then 4 <= j by A9, XXREAL_0:2;

then A29: 4 + 1 <= (len p) + 1 by A27, XREAL_1:6;

A30: (min (s1,(1 / 2))) / 2 > 0 by A8, A28, XREAL_1:215;

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

0 < min (s1,(1 / 2))
by A6, XXREAL_0:15;
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 A16, A32, FINSEQ_1:1;

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:1;

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:9;

then ((min (s1,(1 / 2))) / 2) * (i - 1) < ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A30, XREAL_1:68;

hence r1 > r2 by A35, A36, XREAL_1:15; :: thesis: r1 - r2 = (min (s1,(1 / 2))) / 2

thus r1 - r2 = (min (s1,(1 / 2))) / 2 by A35, A36; :: thesis: verum

end;( 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 A16, A32, FINSEQ_1:1;

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:1;

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:9;

then ((min (s1,(1 / 2))) / 2) * (i - 1) < ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A30, XREAL_1:68;

hence r1 > r2 by A35, A36, XREAL_1:15; :: thesis: r1 - r2 = (min (s1,(1 / 2))) / 2

thus r1 - r2 = (min (s1,(1 / 2))) / 2 by A35, A36; :: thesis: verum

then 0 < j by A12, XREAL_1:139;

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 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:76;

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 A37, A27, FINSEQ_1:1, A15, A13, A40;

A42: for i being Nat st 1 <= i & i < len h1 holds

(h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2

proof

[/(2 / (min (s1,(1 / 2))))\] < (2 / (min (s1,(1 / 2)))) + 1
by INT_1:def 7;
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 A44, NAT_1:13;

A46: 1 < i + 1 by A43, NAT_1:13;

A47: i <= len p by A26, A44, NAT_1:13;

end;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 A44, NAT_1:13;

A46: 1 < i + 1 by A43, NAT_1:13;

A47: i <= len p by A26, A44, NAT_1:13;

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 ) )end;

hence
(h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2
; :: thesis: verumper cases
( i < len p or i >= len p )
;

end;

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 A46, FINSEQ_1:64;

A50: h1 . i = p . i by A43, A48, FINSEQ_1:64;

( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A43, A44, A45, A46, FINSEQ_4:15;

hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A31, A43, A48, A50, A49; :: thesis: verum

end;then A49: h1 . (i + 1) = p . (i + 1) by A46, FINSEQ_1:64;

A50: h1 . i = p . i by A43, A48, FINSEQ_1:64;

( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A43, A44, A45, A46, FINSEQ_4:15;

hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A31, A43, A48, A50, A49; :: thesis: verum

case
i >= len p
; :: thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2

then A51:
i = len p
by A47, XXREAL_0:1;

A52: h1 /. i = h1 . i by A43, A44, FINSEQ_4:15

.= p . i by A43, A47, FINSEQ_1:64 ;

h1 /. (i + 1) = h1 . (i + 1) by A45, A46, FINSEQ_4:15

.= 0 by A51, Lm4 ;

hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A41, A51, A52; :: thesis: verum

end;A52: h1 /. i = h1 . i by A43, A44, FINSEQ_4:15

.= p . i by A43, A47, FINSEQ_1:64 ;

h1 /. (i + 1) = h1 . (i + 1) by A45, A46, FINSEQ_4:15

.= 0 by A51, Lm4 ;

hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A41, A51, A52; :: thesis: verum

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 A30, XREAL_1:68;

A54: for i being Nat

for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds

0 < r1

proof

A59:
for i being Nat st 1 <= i & i < len h1 holds
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 A27, A56, XREAL_1:9;

then ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A8, XREAL_1:64;

then ((min (s1,(1 / 2))) / 2) * (i - 1) < 1 by A53, A39, XXREAL_0:2;

then A58: 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) > 1 - 1 by XREAL_1:10;

i in Seg j by A16, A55, A56, FINSEQ_1:1;

hence 0 < r1 by A15, A57, A58; :: thesis: verum

end;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 A27, A56, XREAL_1:9;

then ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A8, XREAL_1:64;

then ((min (s1,(1 / 2))) / 2) * (i - 1) < 1 by A53, A39, XXREAL_0:2;

then A58: 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) > 1 - 1 by XREAL_1:10;

i in Seg j by A16, A55, A56, FINSEQ_1:1;

hence 0 < r1 by A15, A57, A58; :: thesis: verum

h1 /. i > h1 /. (i + 1)

proof

A70:
e / 2 < e
by A3, XREAL_1:216;
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 A60, NAT_1:13;

A63: i <= len p by A26, A61, NAT_1:13;

A64: i + 1 <= len h1 by A61, NAT_1:13;

end;assume that

A60: 1 <= i and

A61: i < len h1 ; :: thesis: h1 /. i > h1 /. (i + 1)

A62: 1 < i + 1 by A60, NAT_1:13;

A63: i <= len p by A26, A61, NAT_1:13;

A64: i + 1 <= len h1 by A61, NAT_1:13;

now :: thesis: ( ( i < len p & h1 /. i > h1 /. (i + 1) ) or ( i >= len p & h1 /. i > h1 /. (i + 1) ) )end;

hence
h1 /. i > h1 /. (i + 1)
; :: thesis: verumper cases
( i < len p or i >= len p )
;

end;

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 A62, FINSEQ_1:64;

A67: h1 . i = p . i by A60, A65, FINSEQ_1:64;

( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A60, A61, A64, A62, FINSEQ_4:15;

hence h1 /. i > h1 /. (i + 1) by A31, A60, A65, A67, A66; :: thesis: verum

end;then A66: h1 . (i + 1) = p . (i + 1) by A62, FINSEQ_1:64;

A67: h1 . i = p . i by A60, A65, FINSEQ_1:64;

( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A60, A61, A64, A62, FINSEQ_4:15;

hence h1 /. i > h1 /. (i + 1) by A31, A60, A65, A67, A66; :: thesis: verum

case
i >= len p
; :: thesis: h1 /. i > h1 /. (i + 1)

then A68:
i = len p
by A63, XXREAL_0:1;

A69: h1 /. i = h1 . i by A60, A61, FINSEQ_4:15

.= p . i by A60, A63, FINSEQ_1:64 ;

h1 /. (i + 1) = h1 . (i + 1) by A64, A62, FINSEQ_4:15

.= 0 by A68, Lm4 ;

hence h1 /. i > h1 /. (i + 1) by A54, A60, A63, A69; :: thesis: verum

end;A69: h1 /. i = h1 . i by A60, A61, FINSEQ_4:15

.= p . i by A60, A63, FINSEQ_1:64 ;

h1 /. (i + 1) = h1 . (i + 1) by A64, A62, FINSEQ_4:15

.= 0 by A68, Lm4 ;

hence h1 /. i > h1 /. (i + 1) by A54, A60, A63, A69; :: thesis: verum

A71: for i being 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

0 in { r where r is Real : ( 0 <= r & r <= 1 ) }
;
let i be Nat; :: thesis: 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

let Q be Subset of I[01]; :: thesis: 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

let W be Subset of (Euclid n); :: 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: diameter W < e

h1 /. i > h1 /. (i + 1) by A59, A72;

then A75: Q <> {} by A73, XXREAL_1:1;

A76: for x, y being Point of (Euclid n) st x in W & y in W holds

dist (x,y) <= e / 2

then diameter W <= e / 2 by A1, A74, A75, A76, TBSP_1:def 8;

hence diameter W < e by A70, XXREAL_0:2; :: thesis: verum

end;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

let Q be Subset of I[01]; :: thesis: 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

let W be Subset of (Euclid n); :: 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: diameter W < e

h1 /. i > h1 /. (i + 1) by A59, A72;

then A75: Q <> {} by A73, XXREAL_1:1;

A76: for x, y being Point of (Euclid n) st x in W & y in W holds

dist (x,y) <= e / 2

proof

then
W is bounded
by A5, TBSP_1:def 7;
let x, y be Point of (Euclid n); :: 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 A74, A77, FUNCT_1:def 6;

reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A79, Lm2, TOPMETR:12;

reconsider r3 = x3 as Real by A73, A80;

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 A74, A78, FUNCT_1:def 6;

reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A83, Lm2, TOPMETR:12;

reconsider s3 = y3 as Real by A73, A84;

A86: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A42, A72;

|.(r3 - s3).| <= (h1 /. i) - (h1 /. (i + 1)) by A73, A80, A84, Th12;

then A87: |.(r3 - s3).| <= (min (s1,(1 / 2))) / 2 by A86, XXREAL_0:2;

( dist (x3,y3) = |.(r3 - s3).| & (min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) ) by A8, A28, HEINE:1, XREAL_1:216;

then ( f . y3 = f /. y3 & dist (x3,y3) < min (s1,(1 / 2)) ) by A87, XXREAL_0:2;

hence dist (x,y) <= e / 2 by A11, A85, A82; :: thesis: verum

end;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 A74, A77, FUNCT_1:def 6;

reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A79, Lm2, TOPMETR:12;

reconsider r3 = x3 as Real by A73, A80;

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 A74, A78, FUNCT_1:def 6;

reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A83, Lm2, TOPMETR:12;

reconsider s3 = y3 as Real by A73, A84;

A86: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A42, A72;

|.(r3 - s3).| <= (h1 /. i) - (h1 /. (i + 1)) by A73, A80, A84, Th12;

then A87: |.(r3 - s3).| <= (min (s1,(1 / 2))) / 2 by A86, XXREAL_0:2;

( dist (x3,y3) = |.(r3 - s3).| & (min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) ) by A8, A28, HEINE:1, XREAL_1:216;

then ( f . y3 = f /. y3 & dist (x3,y3) < min (s1,(1 / 2)) ) by A87, XXREAL_0:2;

hence dist (x,y) <= e / 2 by A11, A85, A82; :: thesis: verum

then diameter W <= e / 2 by A1, A74, A75, A76, TBSP_1:def 8;

hence diameter W < e by A70, XXREAL_0:2; :: thesis: verum

then A88: 0 in [.0,1.] by RCOMP_1:def 1;

{0} c= [.0,1.] by A88, TARSKI:def 1;

then A89: [.0,1.] \/ {0} = [.0,1.] by XBOOLE_1:12;

Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def 7;

then A90: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20

.= [.0,1.] by TOPMETR:10 ;

A91: rng p c= [.0,1.]

proof

rng <*0*> = {0}
by FINSEQ_1:38;
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 A15, A92;

then reconsider ry = p . nx as Real ;

A95: x in Seg (len p) by A92, FINSEQ_1:def 3;

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 A8, XREAL_1:6;

nx <= len p by A95, FINSEQ_1:1;

then 0 < ry by A54, A96;

then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A93, A94, A97;

hence y in [.0,1.] by RCOMP_1:def 1; :: thesis: verum

end;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 A15, A92;

then reconsider ry = p . nx as Real ;

A95: x in Seg (len p) by A92, FINSEQ_1:def 3;

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 A8, XREAL_1:6;

nx <= len p by A95, FINSEQ_1:1;

then 0 < ry by A54, A96;

then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A93, A94, A97;

hence y in [.0,1.] by RCOMP_1:def 1; :: thesis: verum

then rng h1 = (rng p) \/ {0} by FINSEQ_1:31;

then A98: rng h1 c= [.0,1.] \/ {0} by A91, 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 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, A89, A98, A90, A59, A71, Lm8; :: thesis: verum