:: UNIFORM1 semantic presentation begin theorem Th1: :: UNIFORM1:1 for r being Real st r > 0 holds ex n being Element of NAT st ( n > 0 & 1 / n < r ) proof let r be Real; ::_thesis: ( r > 0 implies ex n being Element of NAT st ( n > 0 & 1 / n < r ) ) assume A1: r > 0 ; ::_thesis: ex n being Element of NAT st ( n > 0 & 1 / n < r ) A2: 1 / r > 0 by A1; consider n being Element of NAT such that A3: 1 / r < n by SEQ_4:3; (1 / r) * r < n * r by A1, A3, XREAL_1:68; then 1 < n * r by A1, XCMPLX_1:87; then 1 / n < r by A3, A2, XREAL_1:83; hence ex n being Element of NAT st ( n > 0 & 1 / n < r ) by A3, A2; ::_thesis: verum end; definition let X, Y be non empty MetrStruct ; let f be Function of X,Y; attrf is uniformly_continuous means :Def1: :: UNIFORM1:def 1 for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for u1, u2 being Element of X st dist (u1,u2) < s holds dist ((f /. u1),(f /. u2)) < r ) ); end; :: deftheorem Def1 defines uniformly_continuous UNIFORM1:def_1_:_ for X, Y being non empty MetrStruct for f being Function of X,Y holds ( f is uniformly_continuous iff for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for u1, u2 being Element of X st dist (u1,u2) < s holds dist ((f /. u1),(f /. u2)) < r ) ) ); theorem Th2: :: UNIFORM1:2 for X being non empty TopSpace for M being non empty MetrSpace for f being Function of X,(TopSpaceMetr M) st f is continuous holds for r being Real for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open proof let X be non empty TopSpace; ::_thesis: for M being non empty MetrSpace for f being Function of X,(TopSpaceMetr M) st f is continuous holds for r being Real for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open let M be non empty MetrSpace; ::_thesis: for f being Function of X,(TopSpaceMetr M) st f is continuous holds for r being Real for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open let f be Function of X,(TopSpaceMetr M); ::_thesis: ( f is continuous implies for r being Real for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open ) assume A1: f is continuous ; ::_thesis: for r being Real for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open thus for r being Real for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open ::_thesis: verum proof let r be Real; ::_thesis: for u being Element of M for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open let u be Element of M; ::_thesis: for P being Subset of (TopSpaceMetr M) st P = Ball (u,r) holds f " P is open let P be Subset of (TopSpaceMetr M); ::_thesis: ( P = Ball (u,r) implies f " P is open ) reconsider P9 = P as Subset of (TopSpaceMetr M) ; assume P = Ball (u,r) ; ::_thesis: f " P is open then ( [#] (TopSpaceMetr M) <> {} & P9 is open ) by TOPMETR:14; hence f " P is open by A1, TOPS_2:43; ::_thesis: verum end; end; theorem Th3: :: UNIFORM1:3 for N, M being non empty MetrSpace for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being real number for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) holds f is continuous proof let N, M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st ( for r being real number for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) holds f is continuous let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( ( for r being real number for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) implies f is continuous ) dom f = the carrier of (TopSpaceMetr N) by FUNCT_2:def_1; then A1: dom f = the carrier of N by TOPMETR:12; now__::_thesis:_(_(_for_r_being_real_number_ for_u_being_Element_of_N for_u1_being_Element_of_M_st_r_>_0_&_u1_=_f_._u_holds_ ex_s_being_real_number_st_ (_s_>_0_&_(_for_w_being_Element_of_N for_w1_being_Element_of_M_st_w1_=_f_._w_&_dist_(u,w)_<_s_holds_ dist_(u1,w1)_<_r_)_)_)_implies_f_is_continuous_) assume A2: for r being real number for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ; ::_thesis: f is continuous for r being real number for u being Element of M for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds f " P is open proof let r be real number ; ::_thesis: for u being Element of M for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds f " P is open let u be Element of M; ::_thesis: for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds f " P is open let P be Subset of (TopSpaceMetr M); ::_thesis: ( r > 0 & P = Ball (u,r) implies f " P is open ) reconsider P9 = P as Subset of (TopSpaceMetr M) ; assume that r > 0 and A3: P = Ball (u,r) ; ::_thesis: f " P is open for p being Point of N st p in f " P holds ex s being real number st ( s > 0 & Ball (p,s) c= f " P ) proof let p be Point of N; ::_thesis: ( p in f " P implies ex s being real number st ( s > 0 & Ball (p,s) c= f " P ) ) assume p in f " P ; ::_thesis: ex s being real number st ( s > 0 & Ball (p,s) c= f " P ) then A4: f . p in Ball (u,r) by A3, FUNCT_1:def_7; then reconsider wf = f . p as Element of M ; P9 is open by A3, TOPMETR:14; then consider r1 being real number such that A5: r1 > 0 and A6: Ball (wf,r1) c= P by A3, A4, TOPMETR:15; reconsider r1 = r1 as Real by XREAL_0:def_1; consider s being real number such that A7: s > 0 and A8: for w being Element of N for w1 being Element of M st w1 = f . w & dist (p,w) < s holds dist (wf,w1) < r1 by A2, A5; reconsider s = s as Real by XREAL_0:def_1; Ball (p,s) c= f " P proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (p,s) or x in f " P ) assume A9: x in Ball (p,s) ; ::_thesis: x in f " P then reconsider wx = x as Element of N ; f . wx in rng f by A1, FUNCT_1:def_3; then reconsider wfx = f . wx as Element of M by TOPMETR:12; dist (p,wx) < s by A9, METRIC_1:11; then dist (wf,wfx) < r1 by A8; then wfx in Ball (wf,r1) by METRIC_1:11; hence x in f " P by A1, A6, FUNCT_1:def_7; ::_thesis: verum end; hence ex s being real number st ( s > 0 & Ball (p,s) c= f " P ) by A7; ::_thesis: verum end; hence f " P is open by TOPMETR:15; ::_thesis: verum end; hence f is continuous by JORDAN2B:16; ::_thesis: verum end; hence ( ( for r being real number for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) implies f is continuous ) ; ::_thesis: verum end; theorem Th4: :: UNIFORM1:4 for N, M being non empty MetrSpace for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds for r being Real for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) proof let N, M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f is continuous holds for r being Real for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let f be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( f is continuous implies for r being Real for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) assume A1: f is continuous ; ::_thesis: for r being Real for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let r be Real; ::_thesis: for u being Element of N for u1 being Element of M st r > 0 & u1 = f . u holds ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u be Element of N; ::_thesis: for u1 being Element of M st r > 0 & u1 = f . u holds ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u1 be Element of M; ::_thesis: ( r > 0 & u1 = f . u implies ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) reconsider P = Ball (u1,r) as Subset of (TopSpaceMetr M) by TOPMETR:12; A2: ( the carrier of N = the carrier of (TopSpaceMetr N) & dom f = the carrier of (TopSpaceMetr N) ) by FUNCT_2:def_1, TOPMETR:12; assume ( r > 0 & u1 = f . u ) ; ::_thesis: ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) then f . u in P by GOBOARD6:1; then A3: u in f " P by A2, FUNCT_1:def_7; f " P is open by A1, Th2; then consider s1 being real number such that A4: s1 > 0 and A5: Ball (u,s1) c= f " P by A3, TOPMETR:15; reconsider s1 = s1 as Real by XREAL_0:def_1; for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds dist (u1,w1) < r proof let w be Element of N; ::_thesis: for w1 being Element of M st w1 = f . w & dist (u,w) < s1 holds dist (u1,w1) < r let w1 be Element of M; ::_thesis: ( w1 = f . w & dist (u,w) < s1 implies dist (u1,w1) < r ) assume that A6: w1 = f . w and A7: dist (u,w) < s1 ; ::_thesis: dist (u1,w1) < r w in Ball (u,s1) by A7, METRIC_1:11; then f . w in P by A5, FUNCT_1:def_7; hence dist (u1,w1) < r by A6, METRIC_1:11; ::_thesis: verum end; hence ex s being Real st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) by A4; ::_thesis: verum end; theorem :: UNIFORM1:5 for N, M being non empty MetrSpace for f being Function of N,M for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds g is continuous proof let N, M be non empty MetrSpace; ::_thesis: for f being Function of N,M for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds g is continuous let f be Function of N,M; ::_thesis: for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st f = g & f is uniformly_continuous holds g is continuous let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( f = g & f is uniformly_continuous implies g is continuous ) assume that A1: f = g and A2: f is uniformly_continuous ; ::_thesis: g is continuous for r being real number for u being Element of N for u1 being Element of M st r > 0 & u1 = g . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r ) ) proof let r be real number ; ::_thesis: for u being Element of N for u1 being Element of M st r > 0 & u1 = g . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u be Element of N; ::_thesis: for u1 being Element of M st r > 0 & u1 = g . u holds ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u1 be Element of M; ::_thesis: ( r > 0 & u1 = g . u implies ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) reconsider r9 = r as Real by XREAL_0:def_1; assume that A3: r > 0 and A4: u1 = g . u ; ::_thesis: ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r ) ) consider s being Real such that A5: 0 < s and A6: for wu1, wu2 being Element of N st dist (wu1,wu2) < s holds dist ((f /. wu1),(f /. wu2)) < r9 by A2, A3, Def1; for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r proof let w be Element of N; ::_thesis: for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r let w1 be Element of M; ::_thesis: ( w1 = g . w & dist (u,w) < s implies dist (u1,w1) < r ) assume that A7: w1 = g . w and A8: dist (u,w) < s ; ::_thesis: dist (u1,w1) < r A9: u1 = f /. u by A1, A4; w1 = f /. w by A1, A7; hence dist (u1,w1) < r by A6, A8, A9; ::_thesis: verum end; hence ex s being real number st ( s > 0 & ( for w being Element of N for w1 being Element of M st w1 = g . w & dist (u,w) < s holds dist (u1,w1) < r ) ) by A5; ::_thesis: verum end; hence g is continuous by Th3; ::_thesis: verum end; theorem Th6: :: UNIFORM1:6 for N being non empty MetrSpace for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds ex r being Real st ( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds ex Ga being Subset of (TopSpaceMetr N) st ( w1 in Ga & w2 in Ga & Ga in G ) ) ) proof let N be non empty MetrSpace; ::_thesis: for G being Subset-Family of (TopSpaceMetr N) st G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact holds ex r being Real st ( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds ex Ga being Subset of (TopSpaceMetr N) st ( w1 in Ga & w2 in Ga & Ga in G ) ) ) let G be Subset-Family of (TopSpaceMetr N); ::_thesis: ( G is Cover of (TopSpaceMetr N) & G is open & TopSpaceMetr N is compact implies ex r being Real st ( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds ex Ga being Subset of (TopSpaceMetr N) st ( w1 in Ga & w2 in Ga & Ga in G ) ) ) ) assume that A1: G is Cover of (TopSpaceMetr N) and A2: G is open and A3: TopSpaceMetr N is compact ; ::_thesis: ex r being Real st ( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds ex Ga being Subset of (TopSpaceMetr N) st ( w1 in Ga & w2 in Ga & Ga in G ) ) ) now__::_thesis:_ex_r_being_Real_st_ (_r_>_0_&_(_for_w1,_w2_being_Element_of_N_st_dist_(w1,w2)_<_r_holds_ ex_Ga_being_Subset_of_(TopSpaceMetr_N)_st_ (_w1_in_Ga_&_w2_in_Ga_&_Ga_in_G_)_)_) set TM = TopSpaceMetr N; defpred S1[ set , set ] means for n being Element of NAT for w1 being Element of N st n = \$1 & w1 = \$2 holds ex w2 being Element of N st ( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds ( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ); A4: TopSpaceMetr N = TopStruct(# the carrier of N,(Family_open_set N) #) by PCOMPS_1:def_5; assume A5: for r being Real holds ( not r > 0 or ex w1, w2 being Element of N st ( dist (w1,w2) < r & ( for Ga being Subset of (TopSpaceMetr N) holds ( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ) ; ::_thesis: contradiction A6: for e being set st e in NAT holds ex u being set st ( u in the carrier of N & S1[e,u] ) proof let e be set ; ::_thesis: ( e in NAT implies ex u being set st ( u in the carrier of N & S1[e,u] ) ) assume e in NAT ; ::_thesis: ex u being set st ( u in the carrier of N & S1[e,u] ) then reconsider m = e as Element of NAT ; set r = 1 / (m + 1); consider w1, w2 being Element of N such that A7: ( dist (w1,w2) < 1 / (m + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds ( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) by A5; for n being Element of NAT for w4 being Element of N st n = e & w4 = w1 holds ex w5 being Element of N st ( dist (w4,w5) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds ( not w4 in Ga or not w5 in Ga or not Ga in G ) ) ) by A7; hence ex u being set st ( u in the carrier of N & S1[e,u] ) ; ::_thesis: verum end; ex f being Function of NAT, the carrier of N st for e being set st e in NAT holds S1[e,f . e] from FUNCT_2:sch_1(A6); then consider f being Function of NAT, the carrier of N such that A8: for e being set st e in NAT holds for n being Element of NAT for w1 being Element of N st n = e & w1 = f . e holds ex w2 being Element of N st ( dist (w1,w2) < 1 / (n + 1) & ( for Ga being Subset of (TopSpaceMetr N) holds ( not w1 in Ga or not w2 in Ga or not Ga in G ) ) ) ; defpred S2[ Subset of (TopSpaceMetr N)] means ex p being Element of NAT st \$1 = { x where x is Point of N : ex n being Element of NAT st ( p <= n & x = f . n ) } ; consider F being Subset-Family of (TopSpaceMetr N) such that A9: for B being Subset of (TopSpaceMetr N) holds ( B in F iff S2[B] ) from SUBSET_1:sch_3(); defpred S3[ set ] means ex n being Element of NAT st ( 0 <= n & \$1 = f . n ); set B0 = { x where x is Point of N : S3[x] } ; A10: { x where x is Point of N : S3[x] } is Subset of N from DOMAIN_1:sch_7(); then A11: { x where x is Point of N : S3[x] } in F by A4, A9; A12: for p being Element of NAT holds { x where x is Point of N : ex n being Element of NAT st ( p <= n & x = f . n ) } <> {} proof let p be Element of NAT ; ::_thesis: { x where x is Point of N : ex n being Element of NAT st ( p <= n & x = f . n ) } <> {} f . p in { x where x is Point of N : ex n being Element of NAT st ( p <= n & x = f . n ) } ; hence { x where x is Point of N : ex n being Element of NAT st ( p <= n & x = f . n ) } <> {} ; ::_thesis: verum end; reconsider B0 = { x where x is Point of N : S3[x] } as Subset of (TopSpaceMetr N) by A4, A10; reconsider F = F as Subset-Family of (TopSpaceMetr N) ; set G1 = clf F; A13: Cl B0 in clf F by A11, PCOMPS_1:def_2; ( clf F <> {} & ( for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds meet Gd <> {} ) ) proof thus clf F <> {} by A13; ::_thesis: for Gd being set st Gd <> {} & Gd c= clf F & Gd is finite holds meet Gd <> {} let H be set ; ::_thesis: ( H <> {} & H c= clf F & H is finite implies meet H <> {} ) assume that A14: H <> {} and A15: H c= clf F and A16: H is finite ; ::_thesis: meet H <> {} reconsider H = H as Subset-Family of (TopSpaceMetr N) by A15, TOPS_2:2; H is c=-linear proof let B, C be set ; :: according to ORDINAL1:def_8 ::_thesis: ( not B in H or not C in H or B,C are_c=-comparable ) assume that A17: B in H and A18: C in H ; ::_thesis: B,C are_c=-comparable reconsider B = B as Subset of (TopSpaceMetr N) by A17; consider V being Subset of (TopSpaceMetr N) such that A19: B = Cl V and A20: V in F by A15, A17, PCOMPS_1:def_2; consider p being Element of NAT such that A21: V = { x where x is Point of N : ex n being Element of NAT st ( p <= n & x = f . n ) } by A9, A20; reconsider C = C as Subset of (TopSpaceMetr N) by A18; consider W being Subset of (TopSpaceMetr N) such that A22: C = Cl W and A23: W in F by A15, A18, PCOMPS_1:def_2; consider q being Element of NAT such that A24: W = { x where x is Point of N : ex n being Element of NAT st ( q <= n & x = f . n ) } by A9, A23; now__::_thesis:_(_(_q_<=_p_&_V_c=_W_)_or_(_p_<=_q_&_W_c=_V_)_) percases ( q <= p or p <= q ) ; caseA25: q <= p ; ::_thesis: V c= W thus V c= W ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in V or y in W ) assume y in V ; ::_thesis: y in W then consider x being Point of N such that A26: y = x and A27: ex n being Element of NAT st ( p <= n & x = f . n ) by A21; consider n being Element of NAT such that A28: p <= n and A29: x = f . n by A27; q <= n by A25, A28, XXREAL_0:2; hence y in W by A24, A26, A29; ::_thesis: verum end; end; caseA30: p <= q ; ::_thesis: W c= V thus W c= V ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in W or y in V ) assume y in W ; ::_thesis: y in V then consider x being Point of N such that A31: y = x and A32: ex n being Element of NAT st ( q <= n & x = f . n ) by A24; consider n being Element of NAT such that A33: q <= n and A34: x = f . n by A32; p <= n by A30, A33, XXREAL_0:2; hence y in V by A21, A31, A34; ::_thesis: verum end; end; end; end; then ( B c= C or C c= B ) by A19, A22, PRE_TOPC:19; hence B,C are_c=-comparable by XBOOLE_0:def_9; ::_thesis: verum end; then consider m being set such that A35: m in H and A36: for C being set st C in H holds m c= C by A14, A16, FINSET_1:11; A37: m c= meet H by A14, A36, SETFAM_1:5; reconsider m = m as Subset of (TopSpaceMetr N) by A35; consider A being Subset of (TopSpaceMetr N) such that A38: m = Cl A and A39: A in F by A15, A35, PCOMPS_1:def_2; A <> {} by A9, A12, A39; then m <> {} by A38, PRE_TOPC:18, XBOOLE_1:3; hence meet H <> {} by A37; ::_thesis: verum end; then ( clf F is closed & clf F is centered ) by FINSET_1:def_3, PCOMPS_1:11; then meet (clf F) <> {} by A3, COMPTS_1:4; then consider c being Point of (TopSpaceMetr N) such that A40: c in meet (clf F) by SUBSET_1:4; reconsider c = c as Point of N by A4; consider Ge being Subset of (TopSpaceMetr N) such that A41: c in Ge and A42: Ge in G by A1, PCOMPS_1:3; reconsider Ge = Ge as Subset of (TopSpaceMetr N) ; Ge is open by A2, A42, TOPS_2:def_1; then consider r being real number such that A43: r > 0 and A44: Ball (c,r) c= Ge by A41, TOPMETR:15; reconsider r = r as Real by XREAL_0:def_1; consider n being Element of NAT such that A45: n > 0 and A46: 1 / n < r / 2 by A43, Th1, XREAL_1:215; reconsider Q1 = Ball (c,(r / 2)) as Subset of (TopSpaceMetr N) by TOPMETR:12; A47: Q1 is open by TOPMETR:14; defpred S4[ set ] means ex n2 being Element of NAT st ( n <= n2 & \$1 = f . n2 ); reconsider B2 = { x where x is Point of (TopSpaceMetr N) : S4[x] } as Subset of (TopSpaceMetr N) from DOMAIN_1:sch_7(); A48: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12; then B2 in F by A9; then Cl B2 in clf F by PCOMPS_1:def_2; then A49: c in Cl B2 by A40, SETFAM_1:def_1; c in Q1 by A43, GOBOARD6:1, XREAL_1:215; then B2 meets Q1 by A49, A47, TOPS_1:12; then consider x being set such that A50: x in B2 and A51: x in Q1 by XBOOLE_0:3; consider y being Point of N such that A52: x = y and A53: ex n2 being Element of NAT st ( n <= n2 & y = f . n2 ) by A48, A50; A54: dist (c,y) < r / 2 by A51, A52, METRIC_1:11; 1 / n >= 1 / (n + 1) by A45, NAT_1:11, XREAL_1:85; then A55: 1 / (n + 1) < r / 2 by A46, XXREAL_0:2; consider n2 being Element of NAT such that A56: n <= n2 and A57: y = f . n2 by A53; consider w2 being Element of N such that A58: dist (y,w2) < 1 / (n2 + 1) and A59: for Ga being Subset of (TopSpaceMetr N) holds ( not y in Ga or not w2 in Ga or not Ga in G ) by A8, A57; n + 1 <= n2 + 1 by A56, XREAL_1:7; then 1 / (n + 1) >= 1 / (n2 + 1) by XREAL_1:118; then dist (y,w2) < 1 / (n + 1) by A58, XXREAL_0:2; then dist (y,w2) < r / 2 by A55, XXREAL_0:2; then A60: (r / 2) + (dist (y,w2)) < (r / 2) + (r / 2) by XREAL_1:6; r / 1 > r / 2 by A43, XREAL_1:76; then dist (c,y) < r by A54, XXREAL_0:2; then A61: y in Ball (c,r) by METRIC_1:11; ( dist (c,w2) <= (dist (c,y)) + (dist (y,w2)) & (dist (c,y)) + (dist (y,w2)) < (r / 2) + (dist (y,w2)) ) by A54, METRIC_1:4, XREAL_1:6; then dist (c,w2) < (r / 2) + (dist (y,w2)) by XXREAL_0:2; then dist (c,w2) < (r / 2) + (r / 2) by A60, XXREAL_0:2; then w2 in Ball (c,r) by METRIC_1:11; hence contradiction by A42, A44, A61, A59; ::_thesis: verum end; hence ex r being Real st ( r > 0 & ( for w1, w2 being Element of N st dist (w1,w2) < r holds ex Ga being Subset of (TopSpaceMetr N) st ( w1 in Ga & w2 in Ga & Ga in G ) ) ) ; ::_thesis: verum end; begin theorem Th7: :: UNIFORM1:7 for N, M being non empty MetrSpace for f being Function of N,M for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds f is uniformly_continuous proof let N, M be non empty MetrSpace; ::_thesis: for f being Function of N,M for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds f is uniformly_continuous let f be Function of N,M; ::_thesis: for g being Function of (TopSpaceMetr N),(TopSpaceMetr M) st g = f & TopSpaceMetr N is compact & g is continuous holds f is uniformly_continuous let g be Function of (TopSpaceMetr N),(TopSpaceMetr M); ::_thesis: ( g = f & TopSpaceMetr N is compact & g is continuous implies f is uniformly_continuous ) assume that A1: g = f and A2: TopSpaceMetr N is compact and A3: g is continuous ; ::_thesis: f is uniformly_continuous for r being Real st 0 < r holds ex s being Real st ( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds dist ((f /. u1),(f /. u2)) < r ) ) proof let r be Real; ::_thesis: ( 0 < r implies ex s being Real st ( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds dist ((f /. u1),(f /. u2)) < r ) ) ) set G = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) } ; A4: the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12; { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) } c= bool the carrier of N proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) } or x in bool the carrier of N ) assume x in { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) } ; ::_thesis: x in bool the carrier of N then ex P being Subset of (TopSpaceMetr N) st ( x = P & ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) ) ; hence x in bool the carrier of N ; ::_thesis: verum end; then reconsider G1 = { P where P is Subset of (TopSpaceMetr N) : ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) } as Subset-Family of (TopSpaceMetr N) by TOPMETR:12; for P3 being Subset of (TopSpaceMetr N) st P3 in G1 holds P3 is open proof let P3 be Subset of (TopSpaceMetr N); ::_thesis: ( P3 in G1 implies P3 is open ) assume P3 in G1 ; ::_thesis: P3 is open then ex P being Subset of (TopSpaceMetr N) st ( P3 = P & ex w being Element of N ex s being Real st ( P = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) ) ; hence P3 is open by TOPMETR:14; ::_thesis: verum end; then A5: G1 is open by TOPS_2:def_1; assume 0 < r ; ::_thesis: ex s being Real st ( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds dist ((f /. u1),(f /. u2)) < r ) ) then A6: 0 < r / 2 by XREAL_1:215; A7: the carrier of N c= union G1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of N or x in union G1 ) assume x in the carrier of N ; ::_thesis: x in union G1 then reconsider w0 = x as Element of N ; g . w0 = f /. w0 by A1; then reconsider w4 = g . w0 as Element of M ; consider s4 being Real such that A8: s4 > 0 and A9: for u5 being Element of N for w5 being Element of M st w5 = g . u5 & dist (w0,u5) < s4 holds dist (w4,w5) < r / 2 by A3, A6, Th4; reconsider P2 = Ball (w0,s4) as Subset of (TopSpaceMetr N) by TOPMETR:12; for w1 being Element of N for w2, w3 being Element of M st w2 = f . w0 & w3 = f . w1 & dist (w0,w1) < s4 holds dist (w2,w3) < r / 2 by A1, A9; then ex w being Element of N ex s being Real st ( P2 = Ball (w,s) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s holds dist (w2,w3) < r / 2 ) ) ; then A10: Ball (w0,s4) in G1 ; x in Ball (w0,s4) by A8, GOBOARD6:1; hence x in union G1 by A10, TARSKI:def_4; ::_thesis: verum end; the carrier of (TopSpaceMetr N) = the carrier of N by TOPMETR:12; then the carrier of N = union G1 by A7, XBOOLE_0:def_10; then G1 is Cover of (TopSpaceMetr N) by A4, SETFAM_1:45; then consider s1 being Real such that A11: s1 > 0 and A12: for w1, w2 being Element of N st dist (w1,w2) < s1 holds ex Ga being Subset of (TopSpaceMetr N) st ( w1 in Ga & w2 in Ga & Ga in G1 ) by A2, A5, Th6; for u1, u2 being Element of N st dist (u1,u2) < s1 holds dist ((f /. u1),(f /. u2)) < r proof let u1, u2 be Element of N; ::_thesis: ( dist (u1,u2) < s1 implies dist ((f /. u1),(f /. u2)) < r ) assume dist (u1,u2) < s1 ; ::_thesis: dist ((f /. u1),(f /. u2)) < r then consider Ga being Subset of (TopSpaceMetr N) such that A13: u1 in Ga and A14: u2 in Ga and A15: Ga in G1 by A12; consider P being Subset of (TopSpaceMetr N) such that A16: Ga = P and A17: ex w being Element of N ex s2 being Real st ( P = Ball (w,s2) & ( for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s2 holds dist (w2,w3) < r / 2 ) ) by A15; consider w being Element of N, s2 being Real such that A18: P = Ball (w,s2) and A19: for w1 being Element of N for w2, w3 being Element of M st w2 = f . w & w3 = f . w1 & dist (w,w1) < s2 holds dist (w2,w3) < r / 2 by A17; dist (w,u2) < s2 by A14, A16, A18, METRIC_1:11; then A20: dist ((f /. w),(f /. u2)) < r / 2 by A19; dist (w,u1) < s2 by A13, A16, A18, METRIC_1:11; then dist ((f /. w),(f /. u1)) < r / 2 by A19; then ( dist ((f /. u1),(f /. u2)) <= (dist ((f /. u1),(f /. w))) + (dist ((f /. w),(f /. u2))) & (dist ((f /. w),(f /. u1))) + (dist ((f /. w),(f /. u2))) < (r / 2) + (r / 2) ) by A20, METRIC_1:4, XREAL_1:8; hence dist ((f /. u1),(f /. u2)) < r by XXREAL_0:2; ::_thesis: verum end; hence ex s being Real st ( 0 < s & ( for u1, u2 being Element of N st dist (u1,u2) < s holds dist ((f /. u1),(f /. u2)) < r ) ) by A11; ::_thesis: verum end; hence f is uniformly_continuous by Def1; ::_thesis: verum end; Lm1: Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7; Lm2: I[01] = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:20, TOPMETR:def_7; Lm3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by Lm1, TOPMETR:12, TOPMETR:20; theorem :: UNIFORM1:8 for n being Element of NAT for g being Function of I[01],(TOP-REAL n) for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds f is uniformly_continuous proof let n be Element of NAT ; ::_thesis: for g being Function of I[01],(TOP-REAL n) for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds f is uniformly_continuous let g be Function of I[01],(TOP-REAL n); ::_thesis: for f being Function of (Closed-Interval-MSpace (0,1)),(Euclid n) st g is continuous & f = g holds f is uniformly_continuous let f be Function of (Closed-Interval-MSpace (0,1)),(Euclid n); ::_thesis: ( g is continuous & f = g implies f is uniformly_continuous ) assume that A1: g is continuous and A2: f = g ; ::_thesis: f is uniformly_continuous A3: 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)) ; h is continuous by A1, A3, PRE_TOPC:33; hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; ::_thesis: verum end; theorem :: UNIFORM1:9 for n being Element of NAT for P being Subset of (TOP-REAL n) for Q being non empty Subset of (Euclid n) for g being Function of I[01],((TOP-REAL n) | P) for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds f is uniformly_continuous proof let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n) for Q being non empty Subset of (Euclid n) for g being Function of I[01],((TOP-REAL n) | P) for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds f is uniformly_continuous let P be Subset of (TOP-REAL n); ::_thesis: for Q being non empty Subset of (Euclid n) for g being Function of I[01],((TOP-REAL n) | P) for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds f is uniformly_continuous let Q be non empty Subset of (Euclid n); ::_thesis: for g being Function of I[01],((TOP-REAL n) | P) for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds f is uniformly_continuous let g be Function of I[01],((TOP-REAL n) | P); ::_thesis: for f being Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q) st P = Q & g is continuous & f = g holds f is uniformly_continuous let f be Function of (Closed-Interval-MSpace (0,1)),((Euclid n) | Q); ::_thesis: ( P = Q & g is continuous & f = g implies f is uniformly_continuous ) assume that A1: P = Q and A2: ( g is continuous & f = g ) ; ::_thesis: f is uniformly_continuous (TOP-REAL n) | P = TopSpaceMetr ((Euclid n) | Q) by A1, EUCLID:63; hence f is uniformly_continuous by A2, Lm1, Th7, TOPMETR:20; ::_thesis: verum end; begin theorem :: UNIFORM1:10 for n being Element of NAT for g being Function of I[01],(TOP-REAL n) holds g is Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67; Lm4: for x being set for f being FinSequence holds ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) proof let x be set ; ::_thesis: for f being FinSequence holds ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) let f be FinSequence; ::_thesis: ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) A1: len (<*x*> ^ f) = (len <*x*>) + (len f) by FINSEQ_1:22 .= (len f) + 1 by FINSEQ_1:39 ; 1 <= len <*x*> by FINSEQ_1:39; then A2: 1 in dom <*x*> by FINSEQ_3:25; then A3: (<*x*> ^ f) . 1 = <*x*> . 1 by FINSEQ_1:def_7 .= x by FINSEQ_1:def_8 ; (f ^ <*x*>) . ((len f) + 1) = <*x*> . 1 by A2, FINSEQ_1:def_7 .= x by FINSEQ_1:def_8 ; hence ( len (f ^ <*x*>) = (len f) + 1 & len (<*x*> ^ f) = (len f) + 1 & (f ^ <*x*>) . ((len f) + 1) = x & (<*x*> ^ f) . 1 = x ) by A1, A3, FINSEQ_2:16; ::_thesis: verum end; Lm5: for x being set for f being FinSequence st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) proof let x be set ; ::_thesis: for f being FinSequence st 1 <= len f holds ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) let f be FinSequence; ::_thesis: ( 1 <= len f implies ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) ) assume A1: 1 <= len f ; ::_thesis: ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) then A2: len f in dom f by FINSEQ_3:25; A3: (<*x*> ^ f) . ((len f) + 1) = (<*x*> ^ f) . ((len <*x*>) + (len f)) by FINSEQ_1:39 .= f . (len f) by A2, FINSEQ_1:def_7 ; 1 in dom f by A1, FINSEQ_3:25; hence ( (f ^ <*x*>) . 1 = f . 1 & (<*x*> ^ f) . ((len f) + 1) = f . (len f) ) by A3, FINSEQ_1:def_7; ::_thesis: verum end; theorem Th11: :: UNIFORM1:11 for r, s being real number holds abs (r - s) = abs (s - r) proof let r, s be real number ; ::_thesis: abs (r - s) = abs (s - r) percases ( r > s or r = s or r < s ) by XXREAL_0:1; suppose r > s ; ::_thesis: abs (r - s) = abs (s - r) then s - r < 0 by XREAL_1:49; then abs (s - r) = - (s - r) by ABSVALUE:def_1 .= r - s ; hence abs (r - s) = abs (s - r) ; ::_thesis: verum end; suppose r = s ; ::_thesis: abs (r - s) = abs (s - r) hence abs (r - s) = abs (s - r) ; ::_thesis: verum end; suppose r < s ; ::_thesis: abs (r - s) = abs (s - r) then r - s < 0 by XREAL_1:49; then abs (r - s) = - (r - s) by ABSVALUE:def_1 .= s - r ; hence abs (r - s) = abs (s - r) ; ::_thesis: verum end; end; end; Lm6: for r, s1, s2 being Real holds ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) ) proof let r, s1, s2 be Real; ::_thesis: ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) ) A1: now__::_thesis:_(_r_in_[.s1,s2.]_implies_(_s1_<=_r_&_r_<=_s2_)_) assume r in [.s1,s2.] ; ::_thesis: ( s1 <= r & r <= s2 ) then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } by RCOMP_1:def_1; then ex r1 being Real st ( r1 = r & s1 <= r1 & r1 <= s2 ) ; hence ( s1 <= r & r <= s2 ) ; ::_thesis: verum end; now__::_thesis:_(_s1_<=_r_&_r_<=_s2_implies_r_in_[.s1,s2.]_) assume ( s1 <= r & r <= s2 ) ; ::_thesis: r in [.s1,s2.] then r in { r1 where r1 is Real : ( s1 <= r1 & r1 <= s2 ) } ; hence r in [.s1,s2.] by RCOMP_1:def_1; ::_thesis: verum end; hence ( r in [.s1,s2.] iff ( s1 <= r & r <= s2 ) ) by A1; ::_thesis: verum end; theorem Th12: :: UNIFORM1:12 for r1, r2, s1, s2 being Real st r1 in [.s1,s2.] & r2 in [.s1,s2.] holds abs (r1 - r2) <= s2 - s1 proof let r1, r2, s1, s2 be Real; ::_thesis: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] implies abs (r1 - r2) <= s2 - s1 ) assume A1: ( r1 in [.s1,s2.] & r2 in [.s1,s2.] ) ; ::_thesis: abs (r1 - r2) <= s2 - s1 then A2: ( r1 <= s2 & s1 <= r2 ) by Lm6; A3: ( s1 <= r1 & r2 <= s2 ) by A1, Lm6; percases ( r1 <= r2 or r1 > r2 ) ; supposeA4: r1 <= r2 ; ::_thesis: abs (r1 - r2) <= s2 - s1 A5: r2 - r1 <= s2 - s1 by A3, XREAL_1:13; r2 - r1 >= 0 by A4, XREAL_1:48; then abs (r2 - r1) <= s2 - s1 by A5, ABSVALUE:def_1; hence abs (r1 - r2) <= s2 - s1 by Th11; ::_thesis: verum end; suppose r1 > r2 ; ::_thesis: abs (r1 - r2) <= s2 - s1 then A6: r1 - r2 >= 0 by XREAL_1:48; r1 - r2 <= s2 - s1 by A2, XREAL_1:13; hence abs (r1 - r2) <= s2 - s1 by A6, ABSVALUE:def_1; ::_thesis: verum end; end; end; definition let IT be FinSequence of REAL ; attrIT is decreasing means :Def2: :: UNIFORM1:def 2 for n, m being Element of NAT st n in dom IT & m in dom IT & n < m holds IT . n > IT . m; end; :: deftheorem Def2 defines decreasing UNIFORM1:def_2_:_ for IT being FinSequence of REAL holds ( IT is decreasing iff for n, m being Element of NAT st n in dom IT & m in dom IT & n < m holds IT . n > IT . m ); Lm7: for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds f /. k < f /. (k + 1) ) holds f is increasing proof let f be FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds f /. k < f /. (k + 1) ) implies f is increasing ) assume A1: for k being Element of NAT st 1 <= k & k < len f holds f /. k < f /. (k + 1) ; ::_thesis: f is increasing now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_i_<_j_holds_ f_._i_<_f_._j let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i < j implies f . i < f . j ) now__::_thesis:_(_i_in_dom_f_&_j_in_dom_f_&_i_<_j_implies_f_._i_<_f_._j_) defpred S1[ Element of NAT ] means ( i + (1 + \$1) <= len f implies f /. i < f /. (i + (1 + \$1)) ); assume that A2: i in dom f and A3: j in dom f and A4: i < j ; ::_thesis: f . i < f . j A5: 1 <= i by A2, FINSEQ_3:25; A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: ( i + (1 + k) <= len f implies f /. i < f /. (i + (1 + k)) ) ; ::_thesis: S1[k + 1] now__::_thesis:_(_i_+_(1_+_(k_+_1))_<=_len_f_implies_f_/._i_<_f_/._(i_+_(1_+_(k_+_1)))_) ( 1 <= i + 1 & i + 1 <= (i + 1) + k ) by NAT_1:11; then A8: 1 <= (i + 1) + k by XXREAL_0:2; A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ; 1 + k < 1 + (k + 1) by NAT_1:13; then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6; assume A11: i + (1 + (k + 1)) <= len f ; ::_thesis: f /. i < f /. (i + (1 + (k + 1))) then i + (1 + k) < len f by A10, XXREAL_0:2; then f /. (i + (1 + k)) < f /. (i + (1 + (k + 1))) by A1, A8, A9; hence f /. i < f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; i + 1 <= j by A4, NAT_1:13; then j -' (i + 1) = j - (i + 1) by XREAL_1:233; then A12: i + (1 + (j -' (i + 1))) = j ; A13: f /. i = f . i by A2, PARTFUN1:def_6; A14: j <= len f by A3, FINSEQ_3:25; then i < len f by A4, XXREAL_0:2; then A15: S1[ 0 ] by A1, A5; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A6); then f /. i < f /. j by A14, A12; hence f . i < f . j by A3, A13, PARTFUN1:def_6; ::_thesis: verum end; hence ( i in dom f & j in dom f & i < j implies f . i < f . j ) ; ::_thesis: verum end; hence f is increasing by SEQM_3:def_1; ::_thesis: verum end; Lm8: for f being FinSequence of REAL st ( for k being Element of NAT st 1 <= k & k < len f holds f /. k > f /. (k + 1) ) holds f is decreasing proof let f be FinSequence of REAL ; ::_thesis: ( ( for k being Element of NAT st 1 <= k & k < len f holds f /. k > f /. (k + 1) ) implies f is decreasing ) assume A1: for k being Element of NAT st 1 <= k & k < len f holds f /. k > f /. (k + 1) ; ::_thesis: f is decreasing now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_dom_f_&_j_in_dom_f_&_i_<_j_holds_ f_._i_>_f_._j let i, j be Element of NAT ; ::_thesis: ( i in dom f & j in dom f & i < j implies f . i > f . j ) now__::_thesis:_(_i_in_dom_f_&_j_in_dom_f_&_i_<_j_implies_f_._i_>_f_._j_) defpred S1[ Element of NAT ] means ( i + (1 + \$1) <= len f implies f /. i > f /. (i + (1 + \$1)) ); assume that A2: i in dom f and A3: j in dom f and A4: i < j ; ::_thesis: f . i > f . j A5: 1 <= i by A2, FINSEQ_3:25; A6: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A7: ( i + (1 + k) <= len f implies f /. i > f /. (i + (1 + k)) ) ; ::_thesis: S1[k + 1] now__::_thesis:_(_i_+_(1_+_(k_+_1))_<=_len_f_implies_f_/._i_>_f_/._(i_+_(1_+_(k_+_1)))_) ( 1 <= i + 1 & i + 1 <= (i + 1) + k ) by NAT_1:11; then A8: 1 <= (i + 1) + k by XXREAL_0:2; A9: i + (1 + (k + 1)) = (i + (1 + k)) + 1 ; 1 + k < 1 + (k + 1) by NAT_1:13; then A10: i + (1 + k) < i + (1 + (k + 1)) by XREAL_1:6; assume A11: i + (1 + (k + 1)) <= len f ; ::_thesis: f /. i > f /. (i + (1 + (k + 1))) then i + (1 + k) < len f by A10, XXREAL_0:2; then f /. (i + (1 + k)) > f /. (i + (1 + (k + 1))) by A1, A8, A9; hence f /. i > f /. (i + (1 + (k + 1))) by A7, A11, A10, XXREAL_0:2; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; i + 1 <= j by A4, NAT_1:13; then j -' (i + 1) = j - (i + 1) by XREAL_1:233; then A12: i + (1 + (j -' (i + 1))) = j ; A13: f /. i = f . i by A2, PARTFUN1:def_6; A14: j <= len f by A3, FINSEQ_3:25; then i < len f by A4, XXREAL_0:2; then A15: S1[ 0 ] by A1, A5; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A6); then f /. i > f /. j by A14, A12; hence f . i > f . j by A3, A13, PARTFUN1:def_6; ::_thesis: verum end; hence ( i in dom f & j in dom f & i < j implies f . i > f . j ) ; ::_thesis: verum end; hence f is decreasing by Def2; ::_thesis: verum end; theorem :: UNIFORM1:13 for n being Element of NAT 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 = 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 ) ) proof 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 = 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 ) ) 1 in { r where r is Real : ( 0 <= r & r <= 1 ) } ; then A1: 1 in [.0,1.] by RCOMP_1:def_1; {1} c= [.0,1.] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {1} or x in [.0,1.] ) assume x in {1} ; ::_thesis: x in [.0,1.] hence x in [.0,1.] by A1, TARSKI:def_1; ::_thesis: verum end; then A2: [.0,1.] \/ {1} = [.0,1.] by XBOOLE_1:12; Closed-Interval-TSpace (0,1) = TopSpaceMetr (Closed-Interval-MSpace (0,1)) by TOPMETR:def_7; then A3: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20 .= [.0,1.] by TOPMETR:10 ; 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 = 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 ) ) 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 = 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 ) ) 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 = 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 ) ) ) assume that A4: e > 0 and A5: g is continuous ; ::_thesis: 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 ) ) A6: e / 2 > 0 by A4, XREAL_1:215; A7: 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 = h as Function of (Closed-Interval-MSpace (0,1)),(Euclid n) by Lm3, EUCLID:67; A8: dom g = the carrier of I[01] by FUNCT_2:def_1; h is continuous by A5, A7, PRE_TOPC:33; then f is uniformly_continuous by Lm1, Th7, TOPMETR:20; then consider s1 being Real such that A9: 0 < s1 and A10: 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 A6, Def1; set s = min (s1,(1 / 2)); defpred S1[ Nat, set ] means \$2 = ((min (s1,(1 / 2))) / 2) * (\$1 - 1); A11: 0 <= min (s1,(1 / 2)) by A9, XXREAL_0:20; then reconsider j = [/(2 / (min (s1,(1 / 2))))\] as Element of NAT by INT_1:53; A12: 2 / (min (s1,(1 / 2))) <= j by INT_1:def_7; A13: min (s1,(1 / 2)) <= s1 by XXREAL_0:17; A14: 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: ( 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 A13, XXREAL_0:2; hence dist ((f /. u1),(f /. u2)) < e / 2 by A10; ::_thesis: verum end; A15: 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 A16: ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - j)) <= ((min (s1,(1 / 2))) / 2) * 1 by A11, XREAL_1:64; A17: for k being Nat st k in Seg j holds ex x being set st S1[k,x] ; consider p being FinSequence such that A18: ( dom p = Seg j & ( for k being Nat st k in Seg j holds S1[k,p . k] ) ) from FINSEQ_1:sch_1(A17); A19: Seg (len p) = Seg j by A18, FINSEQ_1:def_3; rng (p ^ <*1*>) c= REAL proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (p ^ <*1*>) or y in REAL ) A20: len (p ^ <*1*>) = (len p) + (len <*1*>) by FINSEQ_1:22 .= (len p) + 1 by FINSEQ_1:40 ; assume y in rng (p ^ <*1*>) ; ::_thesis: y in REAL then consider x being set such that A21: x in dom (p ^ <*1*>) and A22: y = (p ^ <*1*>) . x by FUNCT_1:def_3; reconsider nx = x as Element of NAT by A21; A23: dom (p ^ <*1*>) = Seg (len (p ^ <*1*>)) by FINSEQ_1:def_3; then A24: nx <= len (p ^ <*1*>) by A21, FINSEQ_1:1; A25: 1 <= nx by A21, A23, FINSEQ_1:1; A26: 1 <= nx by A21, A23, FINSEQ_1:1; now__::_thesis:_(_(_nx_<_(len_p)_+_1_&_y_in_REAL_)_or_(_nx_>=_(len_p)_+_1_&_y_in_REAL_)_) percases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ; case nx < (len p) + 1 ; ::_thesis: y in REAL then A27: nx <= len p by NAT_1:13; then nx in Seg j by A19, A25, FINSEQ_1:1; then A28: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A18; y = p . nx by A22, A26, A27, FINSEQ_1:64; hence y in REAL by A28; ::_thesis: verum end; case nx >= (len p) + 1 ; ::_thesis: y in REAL then nx = (len p) + 1 by A24, A20, XXREAL_0:1; then y = 1 by A22, Lm4; hence y in REAL ; ::_thesis: verum end; end; end; hence y in REAL ; ::_thesis: verum end; then reconsider h1 = p ^ <*1*> as FinSequence of REAL by FINSEQ_1:def_4; A29: len h1 = (len p) + (len <*1*>) by FINSEQ_1:22 .= (len p) + 1 by FINSEQ_1:40 ; A30: len p = j by A18, FINSEQ_1:def_3; A31: min (s1,(1 / 2)) <> 0 by A9, XXREAL_0:15; then 2 / (min (s1,(1 / 2))) >= 2 / (1 / 2) by A11, XREAL_1:118, XXREAL_0:17; then 4 <= j by A12, XXREAL_0:2; then A32: 4 + 1 <= (len p) + 1 by A30, XREAL_1:6; A33: (min (s1,(1 / 2))) / 2 > 0 by A11, A31, XREAL_1:215; A34: 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: 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 ) let r1, r2 be Real; ::_thesis: ( 1 <= i & i < len p & r1 = p . i & r2 = p . (i + 1) implies ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) ) assume that A35: ( 1 <= i & i < len p ) and A36: r1 = p . i and A37: r2 = p . (i + 1) ; ::_thesis: ( r1 < r2 & r2 - r1 = (min (s1,(1 / 2))) / 2 ) ( 1 < i + 1 & i + 1 <= len p ) by A35, NAT_1:13; then i + 1 in Seg j by A19, FINSEQ_1:1; then A38: r2 = ((min (s1,(1 / 2))) / 2) * ((i + 1) - 1) by A18, A37; i < i + 1 by NAT_1:13; then A39: i - 1 < (i + 1) - 1 by XREAL_1:9; A40: i in Seg j by A19, A35, FINSEQ_1:1; then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A18, A36; hence r1 < r2 by A33, A38, A39, XREAL_1:68; ::_thesis: r2 - r1 = (min (s1,(1 / 2))) / 2 r2 - r1 = (((min (s1,(1 / 2))) / 2) * i) - (((min (s1,(1 / 2))) / 2) * (i - 1)) by A18, A36, A40, A38 .= (min (s1,(1 / 2))) / 2 ; hence r2 - r1 = (min (s1,(1 / 2))) / 2 ; ::_thesis: verum end; 0 < min (s1,(1 / 2)) by A9, XXREAL_0:15; then 0 < j by A15, XREAL_1:139; then A41: 0 + 1 <= j by NAT_1:13; then 1 in Seg j by FINSEQ_1:1; then p . 1 = ((min (s1,(1 / 2))) / 2) * (1 - 1) by A18 .= 0 ; then A42: h1 . 1 = 0 by A41, A30, Lm5; 2 * (min (s1,(1 / 2))) <> 0 by A9, XXREAL_0:15; then A43: ( ((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 A44: 1 - (((min (s1,(1 / 2))) / 2) * (j - 1)) = ((min (s1,(1 / 2))) / 2) * (1 + ((2 / (min (s1,(1 / 2)))) - [/(2 / (min (s1,(1 / 2))))\])) ; A45: for r1 being Real st r1 = p . (len p) holds 1 - r1 <= (min (s1,(1 / 2))) / 2 proof let r1 be Real; ::_thesis: ( r1 = p . (len p) implies 1 - r1 <= (min (s1,(1 / 2))) / 2 ) assume A46: r1 = p . (len p) ; ::_thesis: 1 - r1 <= (min (s1,(1 / 2))) / 2 len p in Seg j by A41, A30, FINSEQ_1:1; hence 1 - r1 <= (min (s1,(1 / 2))) / 2 by A16, A18, A30, A44, A46; ::_thesis: verum end; A47: 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: ( 1 <= i & i < len h1 implies (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 ) assume that A48: 1 <= i and A49: i < len h1 ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 A50: i + 1 <= len h1 by A49, NAT_1:13; A51: 1 < i + 1 by A48, NAT_1:13; A52: i <= len p by A29, A49, NAT_1:13; now__::_thesis:_(_(_i_<_len_p_&_(h1_/._(i_+_1))_-_(h1_/._i)_<=_(min_(s1,(1_/_2)))_/_2_)_or_(_i_>=_len_p_&_(h1_/._(i_+_1))_-_(h1_/._i)_<=_(min_(s1,(1_/_2)))_/_2_)_) percases ( i < len p or i >= len p ) ; caseA53: i < len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 then i + 1 <= len p by NAT_1:13; then A54: h1 . (i + 1) = p . (i + 1) by A51, FINSEQ_1:64; A55: h1 . i = p . i by A48, A53, FINSEQ_1:64; ( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A48, A49, A50, A51, FINSEQ_4:15; hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A34, A48, A53, A55, A54; ::_thesis: verum end; case i >= len p ; ::_thesis: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 then A56: i = len p by A52, XXREAL_0:1; A57: h1 /. i = h1 . i by A48, A49, FINSEQ_4:15 .= p . i by A48, A52, FINSEQ_1:64 ; h1 /. (i + 1) = h1 . (i + 1) by A50, A51, FINSEQ_4:15 .= 1 by A56, Lm4 ; hence (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A45, A56, A57; ::_thesis: verum end; end; end; hence (h1 /. (i + 1)) - (h1 /. i) <= (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 A58: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A33, XREAL_1:68; A59: 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: for r1 being Real st 1 <= i & i <= len p & r1 = p . i holds r1 < 1 let r1 be Real; ::_thesis: ( 1 <= i & i <= len p & r1 = p . i implies r1 < 1 ) assume that A60: 1 <= i and A61: i <= len p and A62: r1 = p . i ; ::_thesis: r1 < 1 i - 1 <= j - 1 by A30, A61, XREAL_1:9; then A63: ((min (s1,(1 / 2))) / 2) * (i - 1) <= ((min (s1,(1 / 2))) / 2) * (j - 1) by A11, XREAL_1:64; i in Seg j by A19, A60, A61, FINSEQ_1:1; then r1 = ((min (s1,(1 / 2))) / 2) * (i - 1) by A18, A62; hence r1 < 1 by A58, A43, A63, XXREAL_0:2; ::_thesis: verum end; A64: 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: ( 1 <= i & i < len h1 implies h1 /. i < h1 /. (i + 1) ) assume that A65: 1 <= i and A66: i < len h1 ; ::_thesis: h1 /. i < h1 /. (i + 1) A67: 1 < i + 1 by A65, NAT_1:13; A68: i <= len p by A29, A66, NAT_1:13; A69: i + 1 <= len h1 by A66, NAT_1:13; now__::_thesis:_(_(_i_<_len_p_&_h1_/._i_<_h1_/._(i_+_1)_)_or_(_i_>=_len_p_&_h1_/._i_<_h1_/._(i_+_1)_)_) percases ( i < len p or i >= len p ) ; caseA70: i < len p ; ::_thesis: h1 /. i < h1 /. (i + 1) then i + 1 <= len p by NAT_1:13; then A71: h1 . (i + 1) = p . (i + 1) by A67, FINSEQ_1:64; A72: h1 . i = p . i by A65, A70, FINSEQ_1:64; ( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A65, A66, A69, A67, FINSEQ_4:15; hence h1 /. i < h1 /. (i + 1) by A34, A65, A70, A72, A71; ::_thesis: verum end; case i >= len p ; ::_thesis: h1 /. i < h1 /. (i + 1) then A73: i = len p by A68, XXREAL_0:1; A74: h1 /. i = h1 . i by A65, A66, FINSEQ_4:15 .= p . i by A65, A68, FINSEQ_1:64 ; h1 /. (i + 1) = h1 . (i + 1) by A69, A67, FINSEQ_4:15 .= 1 by A73, Lm4 ; hence h1 /. i < h1 /. (i + 1) by A59, A65, A68, A74; ::_thesis: verum end; end; end; hence h1 /. i < h1 /. (i + 1) ; ::_thesis: verum end; A75: e / 2 < e by A4, XREAL_1:216; A76: 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: 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 let Q be Subset of I[01]; ::_thesis: 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 let W be Subset of (Euclid n); ::_thesis: ( 1 <= i & i < len h1 & Q = [.(h1 /. i),(h1 /. (i + 1)).] & W = g .: Q implies diameter W < e ) assume that A77: ( 1 <= i & i < len h1 ) and A78: Q = [.(h1 /. i),(h1 /. (i + 1)).] and A79: W = g .: Q ; ::_thesis: diameter W < e h1 /. i < h1 /. (i + 1) by A64, A77; then A80: Q <> {} by A78, XXREAL_1:1; A81: 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: ( x in W & y in W implies dist (x,y) <= e / 2 ) assume that A82: x in W and A83: y in W ; ::_thesis: dist (x,y) <= e / 2 consider x3 being set such that A84: x3 in dom g and A85: x3 in Q and A86: x = g . x3 by A79, A82, FUNCT_1:def_6; reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A84, Lm2, TOPMETR:12; reconsider r3 = x3 as Real by A78, A85; A87: (h1 /. (i + 1)) - (h1 /. i) <= (min (s1,(1 / 2))) / 2 by A47, A77; consider y3 being set such that A88: y3 in dom g and A89: y3 in Q and A90: y = g . y3 by A79, A83, FUNCT_1:def_6; reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A88, Lm2, TOPMETR:12; reconsider s3 = y3 as Real by A78, A89; A91: ( f . x3 = f /. x3 & f . y3 = f /. y3 ) ; abs (r3 - s3) <= (h1 /. (i + 1)) - (h1 /. i) by A78, A85, A89, Th12; then abs (r3 - s3) <= (min (s1,(1 / 2))) / 2 by A87, XXREAL_0:2; then A92: dist (x3,y3) <= (min (s1,(1 / 2))) / 2 by HEINE:1; (min (s1,(1 / 2))) / 2 < min (s1,(1 / 2)) by A11, A31, XREAL_1:216; then dist (x3,y3) < min (s1,(1 / 2)) by A92, XXREAL_0:2; hence dist (x,y) <= e / 2 by A14, A86, A90, A91; ::_thesis: verum end; then W is bounded by A6, TBSP_1:def_7; then diameter W <= e / 2 by A8, A79, A80, A81, TBSP_1:def_8; hence diameter W < e by A75, XXREAL_0:2; ::_thesis: verum end; A93: rng p c= [.0,1.] proof let y be set ; :: 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 set such that A94: x in dom p and A95: y = p . x by FUNCT_1:def_3; reconsider nx = x as Element of NAT by A94; A96: p . nx = ((min (s1,(1 / 2))) / 2) * (nx - 1) by A18, A94; then reconsider ry = p . nx as Real ; A97: x in Seg (len p) by A94, FINSEQ_1:def_3; then A98: 1 <= nx by FINSEQ_1:1; then A99: nx - 1 >= 1 - 1 by XREAL_1:9; nx <= len p by A97, FINSEQ_1:1; then ry < 1 by A59, A98; then y in { rs where rs is Real : ( 0 <= rs & rs <= 1 ) } by A11, A95, A96, A99; hence y in [.0,1.] by RCOMP_1:def_1; ::_thesis: verum end; rng <*1*> = {1} by FINSEQ_1:38; then rng h1 = (rng p) \/ {1} by FINSEQ_1:31; then A100: rng h1 c= [.0,1.] \/ {1} by A93, XBOOLE_1:13; h1 . (len h1) = 1 by A29, Lm4; 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 A29, A32, A42, A2, A100, A3, A64, A76, Lm7; ::_thesis: verum end; theorem :: UNIFORM1:14 for n being Element of NAT 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 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 ) ) proof 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 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 ) ) 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 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 ) ) 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 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 ) ) 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 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 ) ) ) 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 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 ) ) 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, Def1; set s = min (s1,(1 / 2)); defpred S1[ 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: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 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; 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 A8, XREAL_1:64; A14: for k being Nat st k in Seg j holds ex x being set 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 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: ( 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 set 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_)_) percases ( nx < (len p) + 1 or nx >= (len p) + 1 ) ; case nx < (len p) + 1 ; ::_thesis: y in REAL then A24: nx <= len p by NAT_1:13; then nx in Seg j by A16, A22, FINSEQ_1:1; then A25: p . nx = 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) by A15; y = p . nx by A19, A23, A24, FINSEQ_1:64; hence y in REAL by A25; ::_thesis: verum end; case nx >= (len p) + 1 ; ::_thesis: y in REAL then nx = (len p) + 1 by A21, A17, XXREAL_0:1; then y = 0 by A19, Lm4; hence y in REAL ; ::_thesis: verum end; end; end; hence y in REAL ; ::_thesis: verum 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: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 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: 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; 0 < min (s1,(1 / 2)) by A6, XXREAL_0:15; 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 proof let r1 be Real; ::_thesis: ( r1 = p . (len p) implies r1 - 0 <= (min (s1,(1 / 2))) / 2 ) assume A42: r1 = p . (len p) ; ::_thesis: r1 - 0 <= (min (s1,(1 / 2))) / 2 len p in Seg j by A37, A27, FINSEQ_1:1; 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: verum 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: ( 1 <= i & i < len h1 implies (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 ) assume that A44: 1 <= i and A45: i < len h1 ; ::_thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 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__::_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_)_) percases ( i < len p or i >= len p ) ; caseA49: i < len p ; ::_thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 then i + 1 <= len p by NAT_1:13; then A50: h1 . (i + 1) = p . (i + 1) by A47, FINSEQ_1:64; A51: h1 . i = p . i by A44, A49, FINSEQ_1:64; ( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A44, A45, A46, A47, FINSEQ_4:15; hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A31, A44, A49, A51, A50; ::_thesis: verum end; case i >= len p ; ::_thesis: (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 then A52: i = len p by A48, XXREAL_0:1; A53: h1 /. i = h1 . i by A44, A45, FINSEQ_4:15 .= p . i by A44, A48, FINSEQ_1:64 ; h1 /. (i + 1) = h1 . (i + 1) by A46, A47, FINSEQ_4:15 .= 0 by A52, Lm4 ; hence (h1 /. i) - (h1 /. (i + 1)) <= (min (s1,(1 / 2))) / 2 by A41, A52, A53; ::_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 A54: ((min (s1,(1 / 2))) / 2) * (j - 1) < ((min (s1,(1 / 2))) / 2) * (2 / (min (s1,(1 / 2)))) by A30, XREAL_1:68; 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: 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 A56: 1 <= i and A57: i <= len p and A58: r1 = p . i ; ::_thesis: 0 < r1 i - 1 <= j - 1 by A27, A57, 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 A54, A39, XXREAL_0:2; then A59: 1 - (((min (s1,(1 / 2))) / 2) * (i - 1)) > 1 - 1 by XREAL_1:10; i in Seg j by A16, A56, A57, FINSEQ_1:1; hence 0 < r1 by A15, A58, A59; ::_thesis: verum 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: ( 1 <= i & i < len h1 implies h1 /. i > h1 /. (i + 1) ) assume that A61: 1 <= i and A62: i < len h1 ; ::_thesis: h1 /. i > h1 /. (i + 1) 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__::_thesis:_(_(_i_<_len_p_&_h1_/._i_>_h1_/._(i_+_1)_)_or_(_i_>=_len_p_&_h1_/._i_>_h1_/._(i_+_1)_)_) percases ( i < len p or i >= len p ) ; caseA66: i < len p ; ::_thesis: h1 /. i > h1 /. (i + 1) then i + 1 <= len p by NAT_1:13; then A67: h1 . (i + 1) = p . (i + 1) by A63, FINSEQ_1:64; A68: h1 . i = p . i by A61, A66, FINSEQ_1:64; ( h1 . i = h1 /. i & h1 . (i + 1) = h1 /. (i + 1) ) by A61, A62, A65, A63, FINSEQ_4:15; hence h1 /. i > h1 /. (i + 1) by A31, A61, A66, A68, A67; ::_thesis: verum end; case i >= len p ; ::_thesis: h1 /. i > h1 /. (i + 1) then A69: i = len p by A64, XXREAL_0:1; A70: h1 /. i = h1 . i by A61, A62, FINSEQ_4:15 .= p . i by A61, A64, FINSEQ_1:64 ; h1 /. (i + 1) = h1 . (i + 1) by A65, A63, FINSEQ_4:15 .= 0 by A69, Lm4 ; hence h1 /. i > h1 /. (i + 1) by A55, A61, A64, A70; ::_thesis: verum end; end; end; hence h1 /. i > h1 /. (i + 1) ; ::_thesis: verum end; A71: e / 2 < e by A3, XREAL_1:216; 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: 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 A73: ( 1 <= i & i < len h1 ) and A74: Q = [.(h1 /. (i + 1)),(h1 /. i).] and A75: W = g .: Q ; ::_thesis: diameter W < e 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: ( x in W & y in W implies dist (x,y) <= e / 2 ) assume that A78: x in W and A79: y in W ; ::_thesis: dist (x,y) <= e / 2 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_6; reconsider x3 = x3 as Element of (Closed-Interval-MSpace (0,1)) by A80, Lm2, TOPMETR:12; 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_6; reconsider y3 = y3 as Element of (Closed-Interval-MSpace (0,1)) by A84, Lm2, TOPMETR:12; 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, Th12; 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:216; 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: verum end; then W is bounded by A5, TBSP_1:def_7; then diameter W <= e / 2 by A1, A75, A76, A77, TBSP_1:def_8; hence diameter W < e by A71, XXREAL_0:2; ::_thesis: verum 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: ( not x in {0} or x in [.0,1.] ) assume x in {0} ; ::_thesis: x in [.0,1.] hence x in [.0,1.] by A89, TARSKI:def_1; ::_thesis: verum 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_7; then A91: the carrier of I[01] = the carrier of (Closed-Interval-MSpace (0,1)) by TOPMETR:12, TOPMETR:20 .= [.0,1.] by TOPMETR:10 ; A92: rng p c= [.0,1.] proof let y be set ; :: 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 set such that A93: x in dom p and A94: y = p . x by FUNCT_1:def_3; 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:1; then nx - 1 >= 1 - 1 by XREAL_1:9; then A98: 1 - (((min (s1,(1 / 2))) / 2) * (nx - 1)) <= 1 - 0 by A8, XREAL_1:6; nx <= len p by A96, FINSEQ_1:1; 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: verum end; rng <*0*> = {0} by FINSEQ_1:38; then rng h1 = (rng p) \/ {0} by FINSEQ_1:31; 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: verum end;