uniform1.miz



    begin

    reserve x,y for set;

    reserve s,s1,s2,s4,r,r1,r2 for Real;

    reserve n,m,i,j for Element of NAT ;

    theorem :: UNIFORM1:1

    

     Th1: for r st r > 0 holds ex n be Nat st n > 0 & (1 / n) < r

    proof

      let r such that

       A1: r > 0 ;

      

       A2: (1 / r) > 0 by A1;

      consider n be 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 thesis by A3, A2;

    end;

    definition

      let X,Y be non empty MetrStruct, f be Function of X, Y;

      :: UNIFORM1:def1

      attr f is uniformly_continuous means for r st 0 < r holds ex s st 0 < s & for u1,u2 be Element of X st ( dist (u1,u2)) < s holds ( dist ((f /. u1),(f /. u2))) < r;

    end

    theorem :: UNIFORM1:2

    

     Th2: for X be non empty TopSpace, M be non empty MetrSpace, f be Function of X, ( TopSpaceMetr M) st f is continuous holds for r be Real, u be Element of M, P be Subset of ( TopSpaceMetr M) st P = ( Ball (u,r)) holds (f " P) is open

    proof

      let X be non empty TopSpace, M be non empty MetrSpace, f be Function of X, ( TopSpaceMetr M);

      assume

       A1: f is continuous;

      let r be Real, u be Element of M, P be Subset of ( TopSpaceMetr M);

      reconsider P9 = P as Subset of ( TopSpaceMetr M);

      assume P = ( Ball (u,r));

      then ( [#] ( TopSpaceMetr M)) <> {} & P9 is open by TOPMETR: 14;

      hence thesis by A1, TOPS_2: 43;

    end;

    theorem :: UNIFORM1:3

    

     Th3: for N,M be non empty MetrSpace, f be Function of ( TopSpaceMetr N), ( TopSpaceMetr M) holds (for r be Real, u be Element of N, u1 be Element of M st r > 0 & u1 = (f . u) holds ex s be Real st s > 0 & for w be Element of N, w1 be Element of M st w1 = (f . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r) implies f is continuous

    proof

      let N,M be non empty MetrSpace, f be Function of ( TopSpaceMetr N), ( TopSpaceMetr M);

      ( dom f) = the carrier of ( TopSpaceMetr N) by FUNCT_2:def 1;

      then

       A1: ( dom f) = the carrier of N by TOPMETR: 12;

      now

        assume

         A2: for r be Real, u be Element of N, u1 be Element of M st r > 0 & u1 = (f . u) holds ex s be Real st s > 0 & for w be Element of N, w1 be Element of M st w1 = (f . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r;

        for r be Real, u be Element of M, P be Subset of ( TopSpaceMetr M) st r > 0 & P = ( Ball (u,r)) holds (f " P) is open

        proof

          let r be Real, u be Element of M, P be Subset of ( TopSpaceMetr M);

          reconsider P9 = P as Subset of ( TopSpaceMetr M);

          assume that r > 0 and

           A3: P = ( Ball (u,r));

          for p be Point of N st p in (f " P) holds ex s be Real st s > 0 & ( Ball (p,s)) c= (f " P)

          proof

            let p be Point of N;

            assume p in (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 be Real such that

             A5: r1 > 0 and

             A6: ( Ball (wf,r1)) c= P by A3, A4, TOPMETR: 15;

            reconsider r1 as Real;

            consider s be Real such that

             A7: s > 0 and

             A8: for w be Element of N, w1 be Element of M st w1 = (f . w) & ( dist (p,w)) < s holds ( dist (wf,w1)) < r1 by A2, A5;

            reconsider s as Real;

            ( Ball (p,s)) c= (f " P)

            proof

              let x be object;

              assume

               A9: x in ( Ball (p,s));

              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 thesis by A1, A6, FUNCT_1:def 7;

            end;

            hence thesis by A7;

          end;

          hence thesis by TOPMETR: 15;

        end;

        hence f is continuous by JORDAN2B: 16;

      end;

      hence thesis;

    end;

    theorem :: UNIFORM1:4

    

     Th4: for N,M be non empty MetrSpace, f be Function of ( TopSpaceMetr N), ( TopSpaceMetr M) st f is continuous holds for r be Real, u be Element of N, u1 be Element of M st r > 0 & u1 = (f . u) holds ex s st s > 0 & for w be Element of N, w1 be Element of M st w1 = (f . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r

    proof

      let N,M be non empty MetrSpace, f be Function of ( TopSpaceMetr N), ( TopSpaceMetr M);

      assume

       A1: f is continuous;

      let r be Real, u be Element of N, u1 be Element of M;

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

      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 be Real such that

       A4: s1 > 0 and

       A5: ( Ball (u,s1)) c= (f " P) by A3, TOPMETR: 15;

      reconsider s1 as Real;

      for w be Element of N, w1 be Element of M st w1 = (f . w) & ( dist (u,w)) < s1 holds ( dist (u1,w1)) < r

      proof

        let w be Element of N, w1 be Element of M;

        assume that

         A6: w1 = (f . w) and

         A7: ( dist (u,w)) < s1;

        w in ( Ball (u,s1)) by A7, METRIC_1: 11;

        then (f . w) in P by A5, FUNCT_1:def 7;

        hence thesis by A6, METRIC_1: 11;

      end;

      hence thesis by A4;

    end;

    theorem :: UNIFORM1:5

    for N,M be non empty MetrSpace, f be Function of N, M, g be 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, f be Function of N, M, g be Function of ( TopSpaceMetr N), ( TopSpaceMetr M);

      assume that

       A1: f = g and

       A2: f is uniformly_continuous;

      for r be Real, u be Element of N, u1 be Element of M st r > 0 & u1 = (g . u) holds ex s be Real st s > 0 & for w be Element of N, w1 be Element of M st w1 = (g . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r

      proof

        let r be Real, u be Element of N, u1 be Element of M;

        reconsider r9 = r as Real;

        assume that

         A3: r > 0 and

         A4: u1 = (g . u);

        consider s be Real such that

         A5: 0 < s and

         A6: for wu1,wu2 be Element of N st ( dist (wu1,wu2)) < s holds ( dist ((f /. wu1),(f /. wu2))) < r by A2, A3;

        for w be Element of N, w1 be Element of M st w1 = (g . w) & ( dist (u,w)) < s holds ( dist (u1,w1)) < r

        proof

          let w be Element of N, w1 be Element of M;

          assume that

           A7: w1 = (g . w) and

           A8: ( dist (u,w)) < s;

          

           A9: u1 = (f /. u) by A1, A4;

          w1 = (f /. w) by A1, A7;

          hence thesis by A6, A8, A9;

        end;

        hence thesis by A5;

      end;

      hence thesis by Th3;

    end;

    reserve p for Element of NAT ;

    ::$Notion-Name

    theorem :: UNIFORM1:6

    

     Th6: for N be non empty MetrSpace, G be Subset-Family of ( TopSpaceMetr N) st G is Cover of ( TopSpaceMetr N) & G is open & ( TopSpaceMetr N) is compact holds ex r st r > 0 & for w1,w2 be Element of N st ( dist (w1,w2)) < r holds ex Ga be Subset of ( TopSpaceMetr N) st w1 in Ga & w2 in Ga & Ga in G

    proof

      let N be non empty MetrSpace, G be Subset-Family of ( TopSpaceMetr N);

      assume that

       A1: G is Cover of ( TopSpaceMetr N) and

       A2: G is open and

       A3: ( TopSpaceMetr N) is compact;

      now

        set TM = ( TopSpaceMetr N);

        defpred P[ object, object] means (for n be Element of NAT , w1 be Element of N st n = $1 & w1 = $2 holds ex w2 be Element of N st ( dist (w1,w2)) < (1 / (n + 1)) & for Ga be Subset of ( TopSpaceMetr N) holds not (w1 in Ga & w2 in Ga & Ga in G));

        

         A4: TM = TopStruct (# the carrier of N, ( Family_open_set N) #) by PCOMPS_1:def 5;

        assume

         A5: not ex r st r > 0 & for w1,w2 be Element of N st ( dist (w1,w2)) < r holds ex Ga be Subset of ( TopSpaceMetr N) st w1 in Ga & w2 in Ga & Ga in G;

        

         A6: for e be object st e in NAT holds ex u be object st u in the carrier of N & P[e, u]

        proof

          let e be object;

          assume e in NAT ;

          then

          reconsider m = e as Element of NAT ;

          set r = (1 / (m + 1));

          consider w1,w2 be Element of N such that

           A7: ( dist (w1,w2)) < r & for Ga be Subset of ( TopSpaceMetr N) holds not (w1 in Ga & w2 in Ga & Ga in G) by A5;

          for n be Element of NAT , w4 be Element of N st n = e & w4 = w1 holds ex w5 be Element of N st ( dist (w4,w5)) < (1 / (n + 1)) & for Ga be Subset of ( TopSpaceMetr N) holds not (w4 in Ga & w5 in Ga & Ga in G) by A7;

          hence thesis;

        end;

        ex f be sequence of the carrier of N st for e be object st e in NAT holds P[e, (f . e)] from FUNCT_2:sch 1( A6);

        then

        consider f be sequence of the carrier of N such that

         A8: for e be object st e in NAT holds for n be Element of NAT , w1 be Element of N st n = e & w1 = (f . e) holds ex w2 be Element of N st ( dist (w1,w2)) < (1 / (n + 1)) & for Ga be Subset of ( TopSpaceMetr N) holds not (w1 in Ga & w2 in Ga & Ga in G);

        defpred P[ Subset of ( TopSpaceMetr N)] means ex p st $1 = { x where x be Point of N : ex n st p <= n & x = (f . n) };

        consider F be Subset-Family of ( TopSpaceMetr N) such that

         A9: for B be Subset of ( TopSpaceMetr N) holds B in F iff P[B] from SUBSET_1:sch 3;

        defpred P[ set] means ex n st 0 <= n & $1 = (f . n);

        set B0 = { x where x be Point of N : P[x] };

        

         A10: B0 is Subset of N from DOMAIN_1:sch 7;

        then

         A11: B0 in F by A4, A9;

        

         A12: for p holds { x where x be Point of N : ex n st p <= n & x = (f . n) } <> {}

        proof

          let p be Element of NAT ;

          (f . p) in { x where x be Point of N : ex n st p <= n & x = (f . n) };

          hence thesis;

        end;

        reconsider B0 as Subset of ( TopSpaceMetr N) by A4, A10;

        reconsider F as Subset-Family of ( TopSpaceMetr N);

        set G1 = ( clf F);

        

         A13: ( Cl B0) in G1 by A11, PCOMPS_1:def 2;

        G1 <> {} & for Gd be set st Gd <> {} & Gd c= G1 & Gd is finite holds ( meet Gd) <> {}

        proof

          thus G1 <> {} by A13;

          let H be set such that

           A14: H <> {} and

           A15: H c= G1 and

           A16: H is finite;

          reconsider H as Subset-Family of TM by A15, TOPS_2: 2;

          H is c=-linear

          proof

            let B,C be set;

            assume that

             A17: B in H and

             A18: C in H;

            reconsider B as Subset of TM by A17;

            consider V be Subset of TM such that

             A19: B = ( Cl V) and

             A20: V in F by A15, A17, PCOMPS_1:def 2;

            consider p such that

             A21: V = { x where x be Point of N : ex n st p <= n & x = (f . n) } by A9, A20;

            reconsider C as Subset of TM by A18;

            consider W be Subset of TM such that

             A22: C = ( Cl W) and

             A23: W in F by A15, A18, PCOMPS_1:def 2;

            consider q be Element of NAT such that

             A24: W = { x where x be Point of N : ex n st q <= n & x = (f . n) } by A9, A23;

            now

              per cases ;

                case

                 A25: q <= p;

                thus V c= W

                proof

                  let y be object;

                  assume y in V;

                  then

                  consider x be Point of N such that

                   A26: y = x and

                   A27: ex n st p <= n & x = (f . n) by A21;

                  consider n such that

                   A28: p <= n and

                   A29: x = (f . n) by A27;

                  q <= n by A25, A28, XXREAL_0: 2;

                  hence thesis by A24, A26, A29;

                end;

              end;

                case

                 A30: p <= q;

                thus W c= V

                proof

                  let y be object;

                  assume y in W;

                  then

                  consider x be Point of N such that

                   A31: y = x and

                   A32: ex n st q <= n & x = (f . n) by A24;

                  consider n such that

                   A33: q <= n and

                   A34: x = (f . n) by A32;

                  p <= n by A30, A33, XXREAL_0: 2;

                  hence thesis by A21, A31, A34;

                end;

              end;

            end;

            then B c= C or C c= B by A19, A22, PRE_TOPC: 19;

            hence thesis by XBOOLE_0:def 9;

          end;

          then

          consider m be set such that

           A35: m in H and

           A36: for C be 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 as Subset of TM by A35;

          consider A be Subset of TM 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 thesis by A37;

        end;

        then G1 is closed & G1 is centered by FINSET_1:def 3, PCOMPS_1: 11;

        then ( meet G1) <> {} by A3, COMPTS_1: 4;

        then

        consider c be Point of TM such that

         A40: c in ( meet G1) by SUBSET_1: 4;

        reconsider c as Point of N by A4;

        consider Ge be Subset of TM such that

         A41: c in Ge and

         A42: Ge in G by A1, PCOMPS_1: 3;

        reconsider Ge as Subset of TM;

        Ge is open by A2, A42, TOPS_2:def 1;

        then

        consider r be Real such that

         A43: r > 0 and

         A44: ( Ball (c,r)) c= Ge by A41, TOPMETR: 15;

        reconsider r as Real;

        consider n be 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 Q[ set] means ex n2 be Element of NAT st n <= n2 & $1 = (f . n2);

        reconsider B2 = { x where x be Point of ( TopSpaceMetr N) : Q[x] } as Subset of ( TopSpaceMetr N) from DOMAIN_1:sch 7;

        

         A48: n in NAT by ORDINAL1:def 12;

        

         A49: the carrier of ( TopSpaceMetr N) = the carrier of N by TOPMETR: 12;

        then B2 in F by A9, A48;

        then ( Cl B2) in ( clf F) by PCOMPS_1:def 2;

        then

         A50: 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 A50, A47, TOPS_1: 12;

        then

        consider x be object such that

         A51: x in B2 and

         A52: x in Q1 by XBOOLE_0: 3;

        consider y be Point of N such that

         A53: x = y and

         A54: ex n2 be Element of NAT st n <= n2 & y = (f . n2) by A49, A51;

        

         A55: ( dist (c,y)) < (r / 2) by A52, A53, METRIC_1: 11;

        (1 / n) >= (1 / (n + 1)) by A45, NAT_1: 11, XREAL_1: 85;

        then

         A56: (1 / (n + 1)) < (r / 2) by A46, XXREAL_0: 2;

        consider n2 be Element of NAT such that

         A57: n <= n2 and

         A58: y = (f . n2) by A54;

        consider w2 be Element of N such that

         A59: ( dist (y,w2)) < (1 / (n2 + 1)) and

         A60: for Ga be Subset of ( TopSpaceMetr N) holds not (y in Ga & w2 in Ga & Ga in G) by A8, A58;

        (n + 1) <= (n2 + 1) by A57, XREAL_1: 7;

        then (1 / (n + 1)) >= (1 / (n2 + 1)) by XREAL_1: 118;

        then ( dist (y,w2)) < (1 / (n + 1)) by A59, XXREAL_0: 2;

        then ( dist (y,w2)) < (r / 2) by A56, XXREAL_0: 2;

        then

         A61: ((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 A55, XXREAL_0: 2;

        then

         A62: 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 A55, 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 A61, XXREAL_0: 2;

        then w2 in ( Ball (c,r)) by METRIC_1: 11;

        hence contradiction by A42, A44, A62, A60;

      end;

      hence thesis;

    end;

    begin

    theorem :: UNIFORM1:7

    

     Th7: for N,M be non empty MetrSpace, f be Function of N, M, g be 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, f be Function of N, M, g be Function of ( TopSpaceMetr N), ( TopSpaceMetr M);

      assume that

       A1: g = f and

       A2: ( TopSpaceMetr N) is compact and

       A3: g is continuous;

      for r st 0 < r holds ex s st 0 < s & for u1,u2 be Element of N st ( dist (u1,u2)) < s holds ( dist ((f /. u1),(f /. u2))) < r

      proof

        let r;

        set G = { P where P be Subset of ( TopSpaceMetr N) : ex w be Element of N, s st P = ( Ball (w,s)) & (for w1 be Element of N, w2,w3 be 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;

        G c= ( bool the carrier of N)

        proof

          let x be object;

          assume x in G;

          then ex P be Subset of ( TopSpaceMetr N) st x = P & ex w be Element of N, s st P = ( Ball (w,s)) & for w1 be Element of N, w2,w3 be Element of M st w2 = (f . w) & w3 = (f . w1) & ( dist (w,w1)) < s holds ( dist (w2,w3)) < (r / 2);

          hence thesis;

        end;

        then

        reconsider G1 = G as Subset-Family of ( TopSpaceMetr N) by TOPMETR: 12;

        for P3 be Subset of ( TopSpaceMetr N) holds P3 in G1 implies P3 is open

        proof

          let P3 be Subset of ( TopSpaceMetr N);

          assume P3 in G1;

          then ex P be Subset of ( TopSpaceMetr N) st P3 = P & ex w be Element of N, s st P = ( Ball (w,s)) & for w1 be Element of N, w2,w3 be Element of M st w2 = (f . w) & w3 = (f . w1) & ( dist (w,w1)) < s holds ( dist (w2,w3)) < (r / 2);

          hence thesis by TOPMETR: 14;

        end;

        then

         A5: G1 is open by TOPS_2:def 1;

        assume 0 < r;

        then

         A6: 0 < (r / 2) by XREAL_1: 215;

        

         A7: the carrier of N c= ( union G1)

        proof

          let x be object;

          assume x in the carrier of N;

          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 such that

           A8: s4 > 0 and

           A9: for u5 be Element of N, w5 be 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 be Element of N, w2,w3 be 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 be Element of N, s st P2 = ( Ball (w,s)) & for w1 be Element of N, w2,w3 be 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 thesis by A10, TARSKI:def 4;

        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 such that

         A11: s1 > 0 and

         A12: for w1,w2 be Element of N st ( dist (w1,w2)) < s1 holds ex Ga be Subset of ( TopSpaceMetr N) st w1 in Ga & w2 in Ga & Ga in G1 by A2, A5, Th6;

        for u1,u2 be Element of N st ( dist (u1,u2)) < s1 holds ( dist ((f /. u1),(f /. u2))) < r

        proof

          let u1,u2 be Element of N;

          assume ( dist (u1,u2)) < s1;

          then

          consider Ga be Subset of ( TopSpaceMetr N) such that

           A13: u1 in Ga and

           A14: u2 in Ga and

           A15: Ga in G1 by A12;

          consider P be Subset of ( TopSpaceMetr N) such that

           A16: Ga = P and

           A17: ex w be Element of N, s2 st P = ( Ball (w,s2)) & for w1 be Element of N, w2,w3 be Element of M st w2 = (f . w) & w3 = (f . w1) & ( dist (w,w1)) < s2 holds ( dist (w2,w3)) < (r / 2) by A15;

          consider w be Element of N, s2 such that

           A18: P = ( Ball (w,s2)) and

           A19: for w1 be Element of N, w2,w3 be 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 thesis by XXREAL_0: 2;

        end;

        hence thesis by A11;

      end;

      hence thesis;

    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 g be Function of I[01] , ( TOP-REAL n), f be Function of ( Closed-Interval-MSpace ( 0 ,1)), ( Euclid n) st g is continuous & f = g holds f is uniformly_continuous

    proof

      let g be Function of I[01] , ( TOP-REAL n), f be Function of ( Closed-Interval-MSpace ( 0 ,1)), ( Euclid n) such that

       A1: g is continuous and

       A2: f = g;

      

       A3: the TopStruct 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;

    end;

    theorem :: UNIFORM1:9

    for P be Subset of ( TOP-REAL n), Q be non empty Subset of ( Euclid n), g be Function of I[01] , (( TOP-REAL n) | P), f be 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 P be Subset of ( TOP-REAL n), Q be non empty Subset of ( Euclid n), g be Function of I[01] , (( TOP-REAL n) | P), f be Function of ( Closed-Interval-MSpace ( 0 ,1)), (( Euclid n) | Q);

      assume that

       A1: P = Q and

       A2: g is continuous & f = g;

      (( TOP-REAL n) | P) = ( TopSpaceMetr (( Euclid n) | Q)) by A1, EUCLID: 63;

      hence thesis by A2, Lm1, Th7, TOPMETR: 20;

    end;

    begin

    theorem :: UNIFORM1:10

    for g be 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 be set, f be 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, f be FinSequence;

      

       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 thesis by A1, A3, FINSEQ_2: 16;

    end;

    

     Lm5: for x be set, f be FinSequence st 1 <= ( len f) holds ((f ^ <*x*>) . 1) = (f . 1) & (( <*x*> ^ f) . (( len f) + 1)) = (f . ( len f))

    proof

      let x be set, f be FinSequence;

      assume

       A1: 1 <= ( 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 thesis by A3, FINSEQ_1:def 7;

    end;

    theorem :: UNIFORM1:11

    

     Th11: for r,s be Real holds |.(r - s).| = |.(s - r).|

    proof

      let r,s be Real;

      per cases by XXREAL_0: 1;

        suppose r > s;

        then (s - r) < 0 by XREAL_1: 49;

        

        then |.(s - r).| = ( - (s - r)) by ABSVALUE:def 1

        .= (r - s);

        hence thesis;

      end;

        suppose r = s;

        hence thesis;

      end;

        suppose r < s;

        then (r - s) < 0 by XREAL_1: 49;

        

        then |.(r - s).| = ( - (r - s)) by ABSVALUE:def 1

        .= (s - r);

        hence thesis;

      end;

    end;

    

     Lm6: for r, s1, s2 holds r in [.s1, s2.] iff s1 <= r & r <= s2

    proof

      let r, s1, s2;

       A1:

      now

        assume r in [.s1, s2.];

        then r in { r1 : s1 <= r1 & r1 <= s2 } by RCOMP_1:def 1;

        then ex r1 st r1 = r & s1 <= r1 & r1 <= s2;

        hence s1 <= r & r <= s2;

      end;

      now

        assume s1 <= r & r <= s2;

        then r in { r1 : s1 <= r1 & r1 <= s2 };

        hence r in [.s1, s2.] by RCOMP_1:def 1;

      end;

      hence thesis by A1;

    end;

    theorem :: UNIFORM1:12

    

     Th12: for r1, r2, s1, s2 st r1 in [.s1, s2.] & r2 in [.s1, s2.] holds |.(r1 - r2).| <= (s2 - s1)

    proof

      let r1, r2, s1, s2;

      assume

       A1: r1 in [.s1, s2.] & r2 in [.s1, s2.];

      then

       A2: r1 <= s2 & s1 <= r2 by Lm6;

      

       A3: s1 <= r1 & r2 <= s2 by A1, Lm6;

      per cases ;

        suppose

         A4: r1 <= r2;

        

         A5: (r2 - r1) <= (s2 - s1) by A3, XREAL_1: 13;

        (r2 - r1) >= 0 by A4, XREAL_1: 48;

        then |.(r2 - r1).| <= (s2 - s1) by A5, ABSVALUE:def 1;

        hence thesis by Th11;

      end;

        suppose r1 > r2;

        then

         A6: (r1 - r2) >= 0 by XREAL_1: 48;

        (r1 - r2) <= (s2 - s1) by A2, XREAL_1: 13;

        hence thesis by A6, ABSVALUE:def 1;

      end;

    end;

    definition

      let IT be FinSequence of REAL ;

      :: UNIFORM1:def2

      attr IT is decreasing means for n, m st n in ( dom IT) & m in ( dom IT) & n < m holds (IT . n) > (IT . m);

    end

    

     Lm7: for f be FinSequence of REAL st (for k be Nat st 1 <= k & k < ( len f) holds (f /. k) < (f /. (k + 1))) holds f is increasing

    proof

      let f be FinSequence of REAL ;

      assume

       A1: for k be Nat st 1 <= k & k < ( len f) holds (f /. k) < (f /. (k + 1));

      now

        let i,j be Nat;

        now

          defpred P[ 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;

          

           A5: 1 <= i by A2, FINSEQ_3: 25;

          

           A6: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A7: (i + (1 + k)) <= ( len f) implies (f /. i) < (f /. (i + (1 + k)));

            now

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

              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;

            end;

            hence thesis;

          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: P[ 0 ] by A1, A5;

          for k be Nat holds P[k] from NAT_1:sch 2( A15, A6);

          then (f /. i) < (f /. j) by A14, A12;

          hence (f . i) < (f . j) by A3, A13, PARTFUN1:def 6;

        end;

        hence i in ( dom f) & j in ( dom f) & i < j implies (f . i) < (f . j);

      end;

      hence thesis by SEQM_3:def 1;

    end;

    

     Lm8: for f be FinSequence of REAL st for k be Nat st 1 <= k < ( len f) holds (f /. k) > (f /. (k + 1)) holds f is decreasing

    proof

      let f be FinSequence of REAL ;

      assume

       A1: for k be Nat st 1 <= k & k < ( len f) holds (f /. k) > (f /. (k + 1));

      now

        let i, j;

        now

          defpred P[ 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;

          

           A5: 1 <= i by A2, FINSEQ_3: 25;

          

           A6: for k be Nat st P[k] holds P[(k + 1)]

          proof

            let k be Nat;

            assume

             A7: (i + (1 + k)) <= ( len f) implies (f /. i) > (f /. (i + (1 + k)));

            now

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

              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;

            end;

            hence thesis;

          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: P[ 0 ] by A1, A5;

          for k be Nat holds P[k] from NAT_1:sch 2( A15, A6);

          then (f /. i) > (f /. j) by A14, A12;

          hence (f . i) > (f . j) by A3, A13, PARTFUN1:def 6;

        end;

        hence i in ( dom f) & j in ( dom f) & i < j implies (f . i) > (f . j);

      end;

      hence thesis;

    end;

    theorem :: UNIFORM1:13

    for e be Real, g be Function of I[01] , ( TOP-REAL n), p1,p2 be Element of ( TOP-REAL n) st e > 0 & g is continuous holds ex h be 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 be Nat, Q be Subset of I[01] , W be Subset of ( Euclid n) st 1 <= i & i < ( len h) & Q = [.(h /. i), (h /. (i + 1)).] & W = (g .: Q) holds ( diameter W) < e

    proof

      1 in { r where r be Real : 0 <= r & r <= 1 };

      then

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

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

      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, g be Function of I[01] , ( TOP-REAL n), p1,p2 be Element of ( TOP-REAL n);

      assume that

       A4: e > 0 and

       A5: g is continuous;

      

       A6: (e / 2) > 0 by A4, XREAL_1: 215;

      

       A7: the TopStruct 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 be Real such that

       A9: 0 < s1 and

       A10: for u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1)) st ( dist (u1,u2)) < s1 holds ( dist ((f /. u1),(f /. u2))) < (e / 2) by A6;

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

      defpred P[ Nat, object] means $2 = ((s / 2) * ($1 - 1));

      

       A11: 0 <= s by A9, XXREAL_0: 20;

      then

      reconsider j = [/(2 / s)\] as Element of NAT by INT_1: 53;

      

       A12: (2 / s) <= j by INT_1:def 7;

      

       A13: s <= s1 by XXREAL_0: 17;

      

       A14: for u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1)) st ( dist (u1,u2)) < s holds ( dist ((f /. u1),(f /. u2))) < (e / 2)

      proof

        let u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1));

        assume ( dist (u1,u2)) < s;

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

        hence thesis by A10;

      end;

      

       A15: (2 / s) <= [/(2 / s)\] by INT_1:def 7;

      then ((2 / s) - j) <= 0 by XREAL_1: 47;

      then (1 + ((2 / s) - j)) <= (1 + 0 ) by XREAL_1: 6;

      then

       A16: ((s / 2) * (1 + ((2 / s) - j))) <= ((s / 2) * 1) by A11, XREAL_1: 64;

      

       A17: for k be Nat st k in ( Seg j) holds ex x be object st P[k, x];

      consider p be FinSequence such that

       A18: ( dom p) = ( Seg j) & for k be Nat st k in ( Seg j) holds P[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 object;

        

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

        then

        consider x be object 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;

        per cases ;

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

          then

           A27: nx <= ( len p) by NAT_1: 13;

          then nx in ( Seg j) by A19, A25, FINSEQ_1: 1;

          then

           A28: (p . nx) = ((s / 2) * (nx - 1)) by A18;

          y = (p . nx) by A22, A26, A27, FINSEQ_1: 64;

          hence thesis by A28, XREAL_0:def 1;

        end;

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

          then nx = (( len p) + 1) by A24, A20, XXREAL_0: 1;

          then

           A29: y = 1 by A22, Lm4;

          1 in REAL by XREAL_0:def 1;

          hence thesis by A29;

        end;

      end;

      then

      reconsider h1 = (p ^ <*1*>) as FinSequence of REAL by FINSEQ_1:def 4;

      

       A30: ( len h1) = (( len p) + ( len <*1*>)) by FINSEQ_1: 22

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

      

       A31: ( len p) = j by A18, FINSEQ_1:def 3;

      

       A32: s <> 0 by A9, XXREAL_0: 15;

      then (2 / s) >= (2 / (1 / 2)) by A11, XREAL_1: 118, XXREAL_0: 17;

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

      then

       A33: (4 + 1) <= (( len p) + 1) by A31, XREAL_1: 6;

      

       A34: (s / 2) > 0 by A11, A32, XREAL_1: 215;

      

       A35: for i be Nat, r1, r2 st 1 <= i & i < ( len p) & r1 = (p . i) & r2 = (p . (i + 1)) holds r1 < r2 & (r2 - r1) = (s / 2)

      proof

        let i be Nat, r1, r2;

        assume that

         A36: 1 <= i & i < ( len p) and

         A37: r1 = (p . i) and

         A38: r2 = (p . (i + 1));

        1 < (i + 1) & (i + 1) <= ( len p) by A36, NAT_1: 13;

        then (i + 1) in ( Seg j) by A19, FINSEQ_1: 1;

        then

         A39: r2 = ((s / 2) * ((i + 1) - 1)) by A18, A38;

        i < (i + 1) by NAT_1: 13;

        then

         A40: (i - 1) < ((i + 1) - 1) by XREAL_1: 9;

        

         A41: i in ( Seg j) by A19, A36, FINSEQ_1: 1;

        then r1 = ((s / 2) * (i - 1)) by A18, A37;

        hence r1 < r2 by A34, A39, A40, XREAL_1: 68;

        (r2 - r1) = (((s / 2) * i) - ((s / 2) * (i - 1))) by A18, A37, A41, A39

        .= (s / 2);

        hence thesis;

      end;

       0 < s by A9, XXREAL_0: 15;

      then 0 < j by A15, XREAL_1: 139;

      then

       A42: ( 0 + 1) <= j by NAT_1: 13;

      then 1 in ( Seg j) by FINSEQ_1: 1;

      

      then (p . 1) = ((s / 2) * (1 - 1)) by A18

      .= 0 ;

      then

       A43: (h1 . 1) = 0 by A42, A31, Lm5;

      (2 * s) <> 0 by A9, XXREAL_0: 15;

      then

       A44: ((s / 2) * (2 / s)) = ((2 * s) / (2 * s)) & ((2 * s) / (2 * s)) = 1 by XCMPLX_1: 60, XCMPLX_1: 76;

      then

       A45: (1 - ((s / 2) * (j - 1))) = ((s / 2) * (1 + ((2 / s) - [/(2 / s)\])));

      

       A46: for r1 st r1 = (p . ( len p)) holds (1 - r1) <= (s / 2) by A42, A31, FINSEQ_1: 1, A16, A18, A45;

      

       A47: for i be Nat st 1 <= i & i < ( len h1) holds ((h1 /. (i + 1)) - (h1 /. i)) <= (s / 2)

      proof

        let i be Nat;

        assume that

         A48: 1 <= i and

         A49: i < ( len h1);

        

         A50: (i + 1) <= ( len h1) by A49, NAT_1: 13;

        

         A51: 1 < (i + 1) by A48, NAT_1: 13;

        

         A52: i <= ( len p) by A30, A49, NAT_1: 13;

        now

          per cases ;

            case

             A53: i < ( len p);

            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 thesis by A35, A48, A53, A55, A54;

          end;

            case i >= ( len p);

            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 thesis by A46, A56, A57;

          end;

        end;

        hence thesis;

      end;

       [/(2 / s)\] < ((2 / s) + 1) by INT_1:def 7;

      then ( [/(2 / s)\] - 1) < (((2 / s) + 1) - 1) by XREAL_1: 9;

      then

       A58: ((s / 2) * (j - 1)) < ((s / 2) * (2 / s)) by A34, XREAL_1: 68;

      

       A59: for i be Nat, r1 st 1 <= i & i <= ( len p) & r1 = (p . i) holds r1 < 1

      proof

        let i be Nat, r1;

        assume that

         A60: 1 <= i and

         A61: i <= ( len p) and

         A62: r1 = (p . i);

        (i - 1) <= (j - 1) by A31, A61, XREAL_1: 9;

        then

         A63: ((s / 2) * (i - 1)) <= ((s / 2) * (j - 1)) by A11, XREAL_1: 64;

        i in ( Seg j) by A19, A60, A61, FINSEQ_1: 1;

        then r1 = ((s / 2) * (i - 1)) by A18, A62;

        hence thesis by A58, A44, A63, XXREAL_0: 2;

      end;

      

       A64: for i be Nat st 1 <= i & i < ( len h1) holds (h1 /. i) < (h1 /. (i + 1))

      proof

        let i be Nat;

        assume that

         A65: 1 <= i and

         A66: i < ( len h1);

        

         A67: 1 < (i + 1) by A65, NAT_1: 13;

        

         A68: i <= ( len p) by A30, A66, NAT_1: 13;

        

         A69: (i + 1) <= ( len h1) by A66, NAT_1: 13;

        per cases ;

          suppose

           A70: i < ( len p);

          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 thesis by A35, A65, A70, A72, A71;

        end;

          suppose i >= ( len p);

          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 thesis by A59, A65, A68, A74;

        end;

      end;

      

       A75: (e / 2) < e by A4, XREAL_1: 216;

      

       A76: for i be Nat, Q be Subset of I[01] , W be 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 Nat, Q be Subset of I[01] , W be Subset of ( Euclid n);

        assume that

         A77: 1 <= i & i < ( len h1) and

         A78: Q = [.(h1 /. i), (h1 /. (i + 1)).] and

         A79: W = (g .: Q);

        (h1 /. i) < (h1 /. (i + 1)) by A64, A77;

        then

         A80: Q <> {} by A78, XXREAL_1: 1;

        

         A81: for x,y be 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);

          assume that

           A82: x in W and

           A83: y in W;

          consider x3 be object 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 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)) <= (s / 2) by A47, A77;

          consider y3 be object 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 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);

           |.(r3 - s3).| <= ((h1 /. (i + 1)) - (h1 /. i)) by A78, A85, A89, Th12;

          then |.(r3 - s3).| <= (s / 2) by A87, XXREAL_0: 2;

          then

           A92: ( dist (x3,y3)) <= (s / 2) by HEINE: 1;

          (s / 2) < s by A11, A32, XREAL_1: 216;

          then ( dist (x3,y3)) < s by A92, XXREAL_0: 2;

          hence thesis by A14, A86, A90, A91;

        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 thesis by A75, XXREAL_0: 2;

      end;

      

       A93: ( rng p) c= [. 0 , 1.]

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be object 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) = ((s / 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 be Real : 0 <= rs & rs <= 1 } by A11, A95, A96, A99;

        hence thesis by RCOMP_1:def 1;

      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 A30, Lm4;

      hence thesis by A30, A33, A43, A2, A100, A3, A64, A76, Lm7;

    end;

    theorem :: UNIFORM1:14

    for e be Real, g be Function of I[01] , ( TOP-REAL n), p1,p2 be Element of ( TOP-REAL n) st e > 0 & g is continuous holds ex h be 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 be Nat, Q be Subset of I[01] , W be 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 e be Real, g be Function of I[01] , ( TOP-REAL n), p1,p2 be Element of ( TOP-REAL n);

      

       A1: ( dom g) = the carrier of I[01] by FUNCT_2:def 1;

      

       A2: the TopStruct 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;

      

       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 be Real such that

       A6: 0 < s1 and

       A7: for u1,u2 be 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 P[ Nat, object] means $2 = (1 - ((s / 2) * ($1 - 1)));

      

       A8: 0 <= s by A6, XXREAL_0: 20;

      then

      reconsider j = [/(2 / s)\] as Element of NAT by INT_1: 53;

      

       A9: (2 / s) <= j by INT_1:def 7;

      

       A10: s <= s1 by XXREAL_0: 17;

      

       A11: for u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1)) st ( dist (u1,u2)) < s holds ( dist ((f /. u1),(f /. u2))) < (e / 2)

      proof

        let u1,u2 be Element of ( Closed-Interval-MSpace ( 0 ,1));

        assume ( dist (u1,u2)) < s;

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

        hence thesis by A7;

      end;

      

       A12: (2 / s) <= [/(2 / s)\] by INT_1:def 7;

      then ((2 / s) - j) <= 0 by XREAL_1: 47;

      then (1 + ((2 / s) - j)) <= (1 + 0 ) by XREAL_1: 6;

      then

       A13: ((s / 2) * (1 + ((2 / s) - j))) <= ((s / 2) * 1) by A8, XREAL_1: 64;

      

       A14: for k be Nat st k in ( Seg j) holds ex x be object st P[k, x];

      consider p be FinSequence such that

       A15: ( dom p) = ( Seg j) & for k be Nat st k in ( Seg j) holds P[k, (p . k)] from FINSEQ_1:sch 1( A14);

      

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

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

      proof

        let y be object;

        

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

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

        assume y in ( rng (p ^ <* 0 qua Real*>));

        then

        consider x be object such that

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

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

        reconsider nx = x as Element of NAT by A18;

        

         A20: ( dom (p ^ <* 0 qua Real*>)) = ( Seg ( len (p ^ <* 0 qua Real*>))) by FINSEQ_1:def 3;

        then

         A21: nx <= ( len (p ^ <* 0 qua Real*>)) by A18, FINSEQ_1: 1;

        

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

        

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

        now

          per cases ;

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

            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 - ((s / 2) * (nx - 1))) by A15;

            y = (p . nx) by A19, A23, A24, FINSEQ_1: 64;

            hence thesis by A25, XREAL_0:def 1;

          end;

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

            then nx = (( len p) + 1) by A21, A17, XXREAL_0: 1;

            then y = ( In ( 0 , REAL )) by A19, Lm4;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then

      reconsider h1 = (p ^ <* 0 qua Real*>) as FinSequence of REAL by FINSEQ_1:def 4;

      

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

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

      

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

      

       A28: s <> 0 by A6, XXREAL_0: 15;

      then (2 / s) >= (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: (s / 2) > 0 by A8, A28, XREAL_1: 215;

      

       A31: for i be Nat, r1, r2 st 1 <= i & i < ( len p) & r1 = (p . i) & r2 = (p . (i + 1)) holds r1 > r2 & (r1 - r2) = (s / 2)

      proof

        let i be Nat, r1, r2;

        assume that

         A32: 1 <= i & i < ( len p) and

         A33: r1 = (p . i) and

         A34: r2 = (p . (i + 1));

        i in ( Seg j) by A16, A32, FINSEQ_1: 1;

        then

         A35: r1 = (1 - ((s / 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 - ((s / 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 ((s / 2) * (i - 1)) < ((s / 2) * ((i + 1) - 1)) by A30, XREAL_1: 68;

        hence r1 > r2 by A35, A36, XREAL_1: 15;

        thus thesis by A35, A36;

      end;

       0 < s 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 - ((s / 2) * (1 - 1))) by A15

      .= 1;

      then

       A38: (h1 . 1) = 1 by A37, A27, Lm5;

      (2 * s) <> 0 by A6, XXREAL_0: 15;

      then

       A39: ((s / 2) * (2 / s)) = ((2 * s) / (2 * s)) & ((2 * s) / (2 * s)) = 1 by XCMPLX_1: 60, XCMPLX_1: 76;

      then

       A40: (1 - ((s / 2) * (j - 1))) = ((s / 2) * (1 + ((2 / s) - [/(2 / s)\])));

      

       A41: for r1 st r1 = (p . ( len p)) holds (r1 - 0 ) <= (s / 2) by A37, A27, FINSEQ_1: 1, A15, A13, A40;

      

       A42: for i be Nat st 1 <= i & i < ( len h1) holds ((h1 /. i) - (h1 /. (i + 1))) <= (s / 2)

      proof

        let i be Nat;

        assume that

         A43: 1 <= i and

         A44: i < ( len h1);

        

         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

          per cases ;

            case

             A48: i < ( len p);

            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 thesis by A31, A43, A48, A50, A49;

          end;

            case i >= ( len p);

            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 thesis by A41, A51, A52;

          end;

        end;

        hence thesis;

      end;

       [/(2 / s)\] < ((2 / s) + 1) by INT_1:def 7;

      then ( [/(2 / s)\] - 1) < (((2 / s) + 1) - 1) by XREAL_1: 9;

      then

       A53: ((s / 2) * (j - 1)) < ((s / 2) * (2 / s)) by A30, XREAL_1: 68;

      

       A54: for i be Nat, r1 st 1 <= i & i <= ( len p) & r1 = (p . i) holds 0 < r1

      proof

        let i be Nat, r1;

        assume that

         A55: 1 <= i and

         A56: i <= ( len p) and

         A57: r1 = (p . i);

        (i - 1) <= (j - 1) by A27, A56, XREAL_1: 9;

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

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

        then

         A58: (1 - ((s / 2) * (i - 1))) > (1 - 1) by XREAL_1: 10;

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

        hence thesis by A15, A57, A58;

      end;

      

       A59: for i be Nat st 1 <= i & i < ( len h1) holds (h1 /. i) > (h1 /. (i + 1))

      proof

        let i be Nat;

        assume that

         A60: 1 <= i and

         A61: i < ( len h1);

        

         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

          per cases ;

            case

             A65: i < ( len p);

            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 thesis by A31, A60, A65, A67, A66;

          end;

            case i >= ( len p);

            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 thesis by A54, A60, A63, A69;

          end;

        end;

        hence thesis;

      end;

      

       A70: (e / 2) < e by A3, XREAL_1: 216;

      

       A71: for i be Nat, Q be Subset of I[01] , W be 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 Nat, Q be Subset of I[01] , W be Subset of ( Euclid n);

        assume that

         A72: 1 <= i & i < ( len h1) and

         A73: Q = [.(h1 /. (i + 1)), (h1 /. i).] and

         A74: W = (g .: Q);

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

        then

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

        

         A76: for x,y be 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);

          assume that

           A77: x in W and

           A78: y in W;

          consider x3 be 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 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 be 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 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))) <= (s / 2) by A42, A72;

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

          then

           A87: |.(r3 - s3).| <= (s / 2) by A86, XXREAL_0: 2;

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

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

          hence thesis by A11, A85, A82;

        end;

        then W is bounded by A5, TBSP_1:def 7;

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

        hence thesis by A70, XXREAL_0: 2;

      end;

       0 in { r where r be Real : 0 <= r & r <= 1 };

      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 qua Real, 1.] by TOPMETR: 10;

      

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

      proof

        let y be object;

        assume y in ( rng p);

        then

        consider x be 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 - ((s / 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 - ((s / 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 be Real : 0 <= rs & rs <= 1 } by A93, A94, A97;

        hence thesis by RCOMP_1:def 1;

      end;

      ( rng <* 0 qua Real*>) = { 0 } by FINSEQ_1: 38;

      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 thesis by A26, A29, A38, A89, A98, A90, A59, A71, Lm8;

    end;