srings_5.miz



    begin

    reserve n for Nat,

r,s for Real,

x,y for Element of ( REAL n),

p,q for Point of ( TOP-REAL n),

e for Point of ( Euclid n);

    theorem :: SRINGS_5:1

    

     Th1: ( abs (x - y)) = ( abs (y - x))

    proof

      now

        ( dom ( abs (x - y))) = ( Seg n) & ( dom ( abs (y - x))) = ( Seg n) by FINSEQ_2: 124;

        hence ( dom ( abs (x - y))) = ( dom ( abs (y - x)));

        thus for i be object st i in ( dom ( abs (x - y))) holds (( abs (x - y)) . i) = (( abs (y - x)) . i)

        proof

          let i be object;

          assume i in ( dom ( abs (x - y)));

          reconsider fxy = (x - y), fyx = (y - x) as complex-valued Function;

          

           A1: (( abs fxy) . i) = |.((x - y) . i).| & (( abs fyx) . i) = |.((y - x) . i).| by VALUED_1: 18;

          reconsider j = i as set by TARSKI: 1;

          reconsider rx = x, ry = y as Element of (n -tuples_on REAL );

          

           A2: ((rx - ry) . j) = ((rx . j) - (ry . j)) & ( - ((ry - rx) . j)) = ( - ((ry . j) - (rx . j))) by RVSUM_1: 27;

          reconsider c1 = ((x - y) . i), c2 = ((y - x) . i) as ExtReal;

          

           A3: |.c2.| = |.( - c2).| & c1 = ( - c2) by A2, XXREAL_3:def 3, EXTREAL1: 29;

           |.c1.| = |.((x - y) . i) qua Complex.| & |.c2.| = |.((y - x) . i) qua Complex.| by EXTREAL1: 12;

          hence (( abs (x - y)) . i) = (( abs (y - x)) . i) by A1, A3;

        end;

      end;

      hence thesis by FUNCT_1:def 11;

    end;

    theorem :: SRINGS_5:2

    

     Th2: for i be Nat st i in ( Seg n) holds (( abs x) . i) in REAL

    proof

      let i be Nat;

      assume

       A1: i in ( Seg n);

      reconsider f = x as complex-valued Function;

      ( dom |.f.|) = ( dom f) & ( dom f) = ( Seg n) by FINSEQ_2: 124, VALUED_1:def 11;

      then ( rng |.f.|) c= REAL & i in ( dom |.f.|) by A1, VALUED_0:def 3;

      hence thesis by FUNCT_1: 3;

    end;

    theorem :: SRINGS_5:3

    

     Th3: for x,y be Element of REAL , xe,ye be ExtReal st x <= xe & y <= ye holds (x + y) <= (xe + ye)

    proof

      let x,y be Element of REAL , xe,ye be ExtReal;

      assume that

       A1: x <= xe and

       A2: y <= ye;

      reconsider x1 = x, y1 = y as ExtReal;

      (x1 + y1) <= (xe + ye) by A1, A2, XXREAL_3: 36;

      hence (x + y) <= (xe + ye) by XXREAL_3:def 2;

    end;

    theorem :: SRINGS_5:4

    

     Th4: for a,c be Real, b be R_eal st a < b & [.a, b.[ c= [.a, c.[ holds b is Real

    proof

      let a,c be Real, b be R_eal;

      assume that

       A1: a < b and

       A2: [.a, b.[ c= [.a, c.[;

      set K = [.a, b.[;

      

       A3: not c in K by A2, XXREAL_1: 3;

      per cases ;

        suppose

         A4: K is non empty;

        then

        consider x be object such that

         A5: x in K;

        reconsider x as Real by A5;

        assume not b is Real;

        then not b in REAL & a in REAL & a <= b by XREAL_0:def 1, A4, XXREAL_1: 27;

        then

         A6: b = +infty by XXREAL_0: 10;

        a <= x by A5, XXREAL_1: 3;

        then

         A7: [.x, +infty .[ c= [.a, b.[ by A6, XXREAL_1: 38;

        per cases ;

          suppose c < x;

          hence contradiction by A5, A2, XXREAL_1: 3;

        end;

          suppose x <= c;

          hence contradiction by A3, A7, XXREAL_1: 236;

        end;

      end;

        suppose K is empty;

        hence thesis by A1, XXREAL_1: 31;

      end;

    end;

    theorem :: SRINGS_5:5

    

     Th5: for D be non empty set, D1 be non empty Subset of D holds (n -tuples_on D1) c= (n -tuples_on D)

    proof

      let D be non empty set, D1 be non empty Subset of D;

      ((n -tuples_on D) /\ (n -tuples_on D1)) = (n -tuples_on D1) by MARGREL1: 21;

      hence thesis by XBOOLE_1: 17;

    end;

    theorem :: SRINGS_5:6

    

     Th6: for X be non empty set, f be Function st f = (( Seg n) --> X) holds f is non-emptyn -element FinSequence

    proof

      let X be non empty set, f be Function;

      assume

       A1: f = (( Seg n) --> X);

      ( card f) = ( card ( dom f)) by CARD_1: 62;

      then ( card f) = ( card ( Seg n)) by A1, FUNCOP_1: 13;

      then ( card f) = ( card n) by FINSEQ_1: 55;

      hence f is non-emptyn -element FinSequence by A1, CARD_1:def 7;

    end;

    definition

      let n be Nat;

      :: SRINGS_5:def1

      func ProductREAL (n) -> non-emptyn -element FinSequence equals (( Seg n) --> REAL );

      coherence by Th6;

    end

    theorem :: SRINGS_5:7

    ( ProductREAL n) = (( Seg n) --> the carrier of R^1 );

    theorem :: SRINGS_5:8

    

     Th7: ( product (( Seg n) --> REAL )) = ( REAL n)

    proof

      ( REAL n) = ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

      hence thesis by CARD_3: 11;

    end;

    theorem :: SRINGS_5:9

    ( product ( ProductREAL n)) = ( REAL n) by Th7;

    theorem :: SRINGS_5:10

    

     Th8: for X be set holds ( product (( Seg n) --> X)) = (n -tuples_on X)

    proof

      let X be set;

      (n -tuples_on X) = ( Funcs (( Seg n),X)) by FINSEQ_2: 93;

      hence thesis by CARD_3: 11;

    end;

    theorem :: SRINGS_5:11

    

     Th9: for D be non empty set, x be Tuple of n, D holds x in ( Funcs (( Seg n),D))

    proof

      let D be non empty set, x be Tuple of n, D;

      x in (n -tuples_on D) by FINSEQ_2: 131;

      hence thesis by FINSEQ_2: 93;

    end;

    theorem :: SRINGS_5:12

    

     Th10: for O1 be Subset of ( TOP-REAL n), O2 be Subset of ( TopSpaceMetr ( Euclid n)) st O1 = O2 holds O1 is open iff O2 is open

    proof

      let O1 be Subset of ( TOP-REAL n), O2 be Subset of ( TopSpaceMetr ( Euclid n));

      assume

       A1: O1 = O2;

       the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

      hence thesis by A1;

    end;

    theorem :: SRINGS_5:13

    e = p implies the set of all ( OpenHypercube (e,(1 / m))) where m be non zero Element of NAT = the set of all ( OpenHypercube (p,(1 / m))) where m be non zero Element of NAT

    proof

      assume

       A1: e = p;

      

       A2: for m be non zero Element of NAT holds ( OpenHypercube (e,(1 / m))) = ( OpenHypercube (p,(1 / m)))

      proof

        let m be non zero Element of NAT ;

        consider e0 be Point of ( Euclid n) such that

         A3: p = e0 and

         A4: ( OpenHypercube (e0,(1 / m))) = ( OpenHypercube (p,(1 / m))) by TIETZE_2:def 1;

        thus thesis by A1, A3, A4;

      end;

      set XE = the set of all ( OpenHypercube (e,(1 / m))) where m be non zero Element of NAT ;

      set XTR = the set of all ( OpenHypercube (p,(1 / m))) where m be non zero Element of NAT ;

      thus XE c= XTR

      proof

        let x be object;

        assume x in XE;

        then

        consider me be non zero Element of NAT such that

         A6: x = ( OpenHypercube (e,(1 / me)));

        x = ( OpenHypercube (p,(1 / me))) by A6, A2;

        hence thesis;

      end;

      let x be object;

      assume x in XTR;

      then

      consider mtr be non zero Element of NAT such that

       A7: x = ( OpenHypercube (p,(1 / mtr)));

      x = ( OpenHypercube (e,(1 / mtr))) by A7, A2;

      hence thesis;

    end;

    theorem :: SRINGS_5:14

    

     Th11: q in ( OpenHypercube (p,r)) implies p in ( OpenHypercube (q,r))

    proof

      assume

       A1: q in ( OpenHypercube (p,r));

      now

        let i be Nat;

        assume i in ( Seg n);

        then (q . i) in ].((p . i) - r), ((p . i) + r).[ by A1, TIETZE_2: 4;

        then ((p . i) - r) < (q . i) & (q . i) < ((p . i) + r) by XXREAL_1: 4;

        then (((p . i) - r) + r) < ((q . i) + r) & ((q . i) - r) < (((p . i) + r) - r) by XREAL_1: 8;

        hence (p . i) in ].((q . i) - r), ((q . i) + r).[ by XXREAL_1: 4;

      end;

      hence thesis by TIETZE_2: 4;

    end;

    theorem :: SRINGS_5:15

    

     Th12: q in ( OpenHypercube (p,(r / 2))) implies ( OpenHypercube (q,(r / 2))) c= ( OpenHypercube (p,r))

    proof

      assume

       A1: q in ( OpenHypercube (p,(r / 2)));

      let x be object;

      assume

       A2: x in ( OpenHypercube (q,(r / 2)));

      then

      reconsider x1 = x as Point of ( TOP-REAL n);

      now

        let i be Nat;

        assume

         A3: i in ( Seg n);

        then (x1 . i) in ].((q . i) - (r / 2)), ((q . i) + (r / 2)).[ by A2, TIETZE_2: 4;

        then

         A4: ((q . i) - (r / 2)) < (x1 . i) & (x1 . i) < ((q . i) + (r / 2)) by XXREAL_1: 4;

        (q . i) in ].((p . i) - (r / 2)), ((p . i) + (r / 2)).[ by A1, A3, TIETZE_2: 4;

        then ((p . i) - (r / 2)) < (q . i) & (q . i) < ((p . i) + (r / 2)) by XXREAL_1: 4;

        then (((p . i) - (r / 2)) - (r / 2)) < ((q . i) - (r / 2)) & ((q . i) + (r / 2)) < (((p . i) + (r / 2)) + (r / 2)) by XREAL_1: 8;

        then ((p . i) - r) < (x1 . i) & (x1 . i) < ((p . i) + r) by A4, XXREAL_0: 2;

        hence (x1 . i) in ].((p . i) - r), ((p . i) + r).[ by XXREAL_1: 4;

      end;

      hence x in ( OpenHypercube (p,r)) by TIETZE_2: 4;

    end;

    definition

      let x be Element of [: REAL , REAL :];

      :: original: `1

      redefine

      func x `1 -> Element of REAL ;

      coherence

      proof

        ex a,b be object st a in REAL & b in REAL & x = [a, b] by ZFMISC_1:def 2;

        hence thesis;

      end;

      :: original: `2

      redefine

      func x `2 -> Element of REAL ;

      coherence

      proof

        ex a,b be object st a in REAL & b in REAL & x = [a, b] by ZFMISC_1:def 2;

        hence thesis;

      end;

    end

    definition

      let n be Nat, x be Element of [:( REAL n), ( REAL n):];

      :: original: `1

      redefine

      func x `1 -> Element of ( REAL n) ;

      coherence

      proof

        ex a,b be object st a in ( REAL n) & b in ( REAL n) & x = [a, b] by ZFMISC_1:def 2;

        hence thesis;

      end;

      :: original: `2

      redefine

      func x `2 -> Element of ( REAL n) ;

      coherence

      proof

        ex a,b be object st a in ( REAL n) & b in ( REAL n) & x = [a, b] by ZFMISC_1:def 2;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:16

    

     Th13: for f be n -element FinSequence of [: REAL , REAL :] holds ex x be Element of [:( REAL n), ( REAL n):] st for i be Nat st i in ( Seg n) holds ((x `1 ) . i) = ((f /. i) `1 ) & ((x `2 ) . i) = ((f /. i) `2 )

    proof

      let f be n -element FinSequence of [: REAL , REAL :];

      defpred P[ Nat, set] means $2 = ((f /. $1) `1 );

      

       A2: for i be Nat st i in ( Seg n) holds ex d be Element of REAL st P[i, d];

      ex x1 be FinSequence of REAL st ( len x1) = n & for i be Nat st i in ( Seg n) holds P[i, (x1 /. i)] from FINSEQ_4:sch 1( A2);

      then

      consider x1 be FinSequence of REAL such that

       A3: ( len x1) = n and

       A4: for i be Nat st i in ( Seg n) holds (x1 /. i) = ((f /. i) `1 );

      ( dom x1) = ( Seg n) by A3, FINSEQ_1:def 3;

      then

      reconsider x1 as Element of ( REAL n) by REAL_NS1: 6;

      defpred Q[ Nat, set] means $2 = ((f /. $1) `2 );

      

       A5: for i be Nat st i in ( Seg n) holds ex d be Element of REAL st Q[i, d];

      ex x2 be FinSequence of REAL st ( len x2) = n & for i be Nat st i in ( Seg n) holds Q[i, (x2 /. i)] from FINSEQ_4:sch 1( A5);

      then

      consider x2 be FinSequence of REAL such that

       A6: ( len x2) = n and

       A7: for i be Nat st i in ( Seg n) holds (x2 /. i) = ((f /. i) `2 );

      ( dom x2) = ( Seg n) by A6, FINSEQ_1:def 3;

      then

      reconsider x2 as Element of ( REAL n) by REAL_NS1: 6;

      reconsider x = [x1, x2] as Element of [:( REAL n), ( REAL n):] by ZFMISC_1:def 2;

      take x;

      now

        let i be Nat;

        assume

         A8: i in ( Seg n);

        then

         A9: (x1 /. i) = ((f /. i) `1 ) & (x2 /. i) = ((f /. i) `2 ) by A4, A7;

        i in ( dom x1) & i in ( dom x2) by A3, FINSEQ_1:def 3, A8, A6;

        hence ((x `1 ) . i) = ((f /. i) `1 ) & ((x `2 ) . i) = ((f /. i) `2 ) by A9, PARTFUN1:def 6;

      end;

      hence thesis;

    end;

    begin

    definition

      let n;

      :: SRINGS_5:def2

      func RAT n -> FinSequenceSet of RAT equals (n -tuples_on RAT );

      coherence ;

    end

    theorem :: SRINGS_5:17

    

     Th14: ( RAT 0 ) = { 0 }

    proof

      ( RAT 0 ) = {( <*> RAT )} by FINSEQ_2: 94

      .= { {} };

      hence thesis;

    end;

    registration

      cluster ( RAT 0 ) -> trivial;

      coherence by Th14;

    end

    registration

      let n;

      cluster ( RAT n) -> non empty;

      coherence ;

    end

    registration

      let n;

      cluster -> n -element for Element of ( RAT n);

      coherence ;

    end

    registration

      let n;

      cluster ( RAT n) -> countable;

      coherence by CARD_4: 10;

    end

    registration

      let n be positive Nat;

      cluster ( RAT n) -> infinite;

      correctness

      proof

        deffunc F( Element of (n -tuples_on RAT )) = ($1 . 1);

        consider f be Function such that

         A1: ( dom f) = (n -tuples_on RAT ) & for d be Element of (n -tuples_on RAT ) holds (f . d) = F(d) from FUNCT_1:sch 4;

        for y be object holds y in (f .: (n -tuples_on RAT )) iff y in RAT

        proof

          let y be object;

          ( 0 + 1) < (n + 1) by XREAL_1: 6;

          then

           A2: 1 <= n by NAT_1: 13;

          then

           A3: 1 in ( Seg n);

          hereby

            assume y in (f .: (n -tuples_on RAT ));

            then

            consider x be object such that

             A4: x in ( dom f) & x in (n -tuples_on RAT ) & y = (f . x) by FUNCT_1:def 6;

            reconsider x as Element of (n -tuples_on RAT ) by A4;

            

             A5: y = (x . 1) by A1, A4;

            x in ( Funcs (( Seg n), RAT )) by A4, FINSEQ_2: 93;

            then

            consider f1 be Function such that

             A6: x = f1 & ( dom f1) = ( Seg n) & ( rng f1) c= RAT by FUNCT_2:def 2;

            thus y in RAT by A3, A5, A6, FUNCT_1: 3;

          end;

          assume y in RAT ;

          then

           A7: {y} c= RAT by ZFMISC_1: 31;

          set x = (( Seg n) --> y);

          

           A8: ( dom x) = ( Seg n) & ( rng x) c= {y} by FUNCOP_1: 13;

          ( rng x) c= RAT by A7;

          then x in ( Funcs (( Seg n), RAT )) by A8, FUNCT_2:def 2;

          then

          reconsider x as Element of (n -tuples_on RAT ) by FINSEQ_2: 93;

          (f . x) = (x . 1) by A1

          .= y by A2, FINSEQ_1: 1, FUNCOP_1: 7;

          hence y in (f .: (n -tuples_on RAT )) by A1, FUNCT_1:def 6;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let n be positive Nat;

      cluster ( RAT n) -> denumerable;

      coherence ;

    end

    theorem :: SRINGS_5:18

    

     Th15: ( RAT n) is dense Subset of ( TOP-REAL n)

    proof

      ( RAT n) is Subset of ( REAL n) by NUMBERS: 12, Th5;

      then

      reconsider RATN = ( RAT n) as Subset of ( TOP-REAL n) by EUCLID: 22;

      for Q be Subset of ( TOP-REAL n) st Q <> {} & Q is open holds RATN meets Q

      proof

        let Q be Subset of ( TOP-REAL n);

        assume that

         A1: Q <> {} and

         A2: Q is open;

        consider q be object such that

         A3: q in Q by A1, XBOOLE_0:def 1;

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider Q0 = Q as Subset of ( TopSpaceMetr ( Euclid n));

        reconsider q0 = q as Point of ( Euclid n) by A3, EUCLID: 67;

        Q0 is open by A2, Th10;

        then

        consider m be non zero Element of NAT such that

         A6: ( OpenHypercube (q0,(1 / m))) c= Q0 by A3, EUCLID_9: 23;

        set OH = ( OpenHypercube (q0,(1 / m))), f = ( Intervals (q0,(1 / m)));

        

         A7: ( dom f) = ( dom q0) by EUCLID_9:def 3;

        

         A8: for x be object st x in ( dom f) holds ex k be Element of RAT st k in (f . x)

        proof

          let x be object;

          assume

           A9: x in ( dom f);

          reconsider FF = ].((q0 . x) - (1 / m)), ((q0 . x) + (1 / m)).[ as open Subset of R^1 by BORSUK_5: 39;

          

           A10: ((q0 . x) - (1 / m)) < (q0 . x) by XREAL_1: 44;

          (q0 . x) < ((q0 . x) + (1 / m)) by XREAL_1: 29;

          then ((q0 . x) - (1 / m)) < ((q0 . x) + (1 / m)) by A10, XXREAL_0: 2;

          then FF <> {} & FF is open by XXREAL_1: 33;

          then FF meets RAT by TOPGEN_1: 51, TOPS_1: 45;

          then

          consider k be object such that

           A11: k in FF & k in RAT by XBOOLE_0: 3;

          take k;

          thus thesis by A11, A9, A7, EUCLID_9:def 3;

        end;

        q in ( TOP-REAL n) by A3;

        then q in ( REAL n) by EUCLID: 22;

        then

        reconsider q1 = q as FinSequence of REAL by FINSEQ_2: 131;

        

         A12: ( dom q1) = ( Seg n) by A3, FINSEQ_1: 89;

        defpred P[ object, object] means $2 in (f . $1) & $2 is Element of RAT ;

        

         A13: for x be Nat st x in ( Seg n) holds ex y be object st P[x, y]

        proof

          let x be Nat;

          assume x in ( Seg n);

          then

          consider k be Element of RAT such that

           A14: k in (f . x) by A8, A7, A12;

          take k;

          thus thesis by A14;

        end;

        consider p be FinSequence such that

         A15: ( dom p) = ( Seg n) and

         A16: for k be Nat st k in ( Seg n) holds P[k, (p . k)] from FINSEQ_1:sch 1( A13);

        

         A17: p is n -element

        proof

          ( Seg ( len p)) = ( dom p) by FINSEQ_1:def 3;

          hence thesis by A15, FINSEQ_1: 6, CARD_1:def 7;

        end;

        p is Tuple of n, RAT

        proof

          p is FinSequence of RAT

          proof

            ( rng p) c= RAT

            proof

              let x be object;

              assume x in ( rng p);

              then

              consider x0 be object such that

               A18: x0 in ( dom p) and

               A19: x = (p . x0) by FUNCT_1:def 3;

              (p . x0) in (f . x0) & (p . x0) is Element of RAT by A16, A18, A15;

              hence x in RAT by A19;

            end;

            hence thesis by FINSEQ_1:def 4;

          end;

          hence thesis by A17;

        end;

        then

         A20: p in ( RAT n) by FINSEQ_2: 131;

        p in OH

        proof

          p in ( product ( Intervals (q0,(1 / m))))

          proof

            now

              let x be object;

              assume x in ( dom f);

              then x in ( Seg n) by A7, FINSEQ_1: 89;

              hence (p . x) in (f . x) by A16;

            end;

            hence thesis by A15, A7, A12, CARD_3: 9;

          end;

          hence thesis;

        end;

        hence thesis by A6, A20, XBOOLE_0: 3;

      end;

      hence thesis by TOPS_1: 45;

    end;

    registration

      let n;

      cluster ( RAT n) -> countable dense;

      coherence by Th15;

    end

    begin

    registration

      let n be Nat;

      cluster countable for Basis of ( TOP-REAL n);

      existence by TOPGEN_4: 57;

    end

    begin

    registration

      let n, e;

      cluster ( OpenHypercubes e) -> countable;

      coherence

      proof

        set OH = ( OpenHypercubes e);

        deffunc F( Nat) = ( OpenHypercube (e,(1 / $1)));

        defpred P[ Nat] means $1 <> 0 ;

        

         A1: { F(n) where n be Nat : P[n] } is countable from CARD_4:sch 1;

        { F(n) where n be Nat : P[n] } = OH

        proof

          thus { F(n) where n be Nat : P[n] } c= OH

          proof

            let x be object;

            assume x in { F(n) where n be Nat : P[n] };

            then

            consider n0 be Nat such that

             A3: x = F(n0) and

             A4: P[n0];

            n0 is non zero Element of NAT by A4, ORDINAL1:def 12;

            hence x in OH by A3;

          end;

          let x be object;

          assume x in OH;

          then

          consider m0 be non zero Element of NAT such that

           A5: x = ( OpenHypercube (e,(1 / m0)));

          thus thesis by A5;

        end;

        hence thesis by A1;

      end;

    end

    definition

      let n;

      :: SRINGS_5:def3

      func OpenHypercubesRAT (n) -> non empty set equals { ( OpenHypercubes q) where q be Point of ( Euclid n) : q in ( RAT n) };

      coherence

      proof

        consider q be object such that

         A1: q in ( RAT n) by XBOOLE_0:def 1;

        ( RAT n) c= ( REAL n) by NUMBERS: 12, Th5;

        then

        reconsider q1 = q as Point of ( Euclid n) by A1;

        ( OpenHypercubes q1) in { ( OpenHypercubes q) where q be Point of ( Euclid n) : q in ( RAT n) } by A1;

        hence thesis;

      end;

    end

    definition

      let n;

      let q be Element of ( RAT n);

      :: SRINGS_5:def4

      func @ q -> Point of ( Euclid n) equals q;

      coherence

      proof

        ( RAT n) c= ( REAL n) & q in ( RAT n) by NUMBERS: 12, Th5;

        hence thesis;

      end;

    end

    definition

      let n;

      let q be object;

      :: SRINGS_5:def5

      func object2RAT (q,n) -> Element of ( RAT n) equals

      : Def1: q;

      coherence by A1;

    end

    

     Th16: ( OpenHypercubesRAT n) is countable

    proof

      deffunc F2( object) = ( OpenHypercubes ( @ ( object2RAT ($1,n))));

      consider ff be Function such that

       A1: ( dom ff) = ( RAT n) and

       A2: for x be object st x in ( RAT n) holds (ff . x) = F2(x) from FUNCT_1:sch 3;

      

       A3: ( OpenHypercubesRAT n) = ( rng ff)

      proof

        hereby

          let x be object;

          assume x in ( OpenHypercubesRAT n);

          then

          consider q0 be Point of ( Euclid n) such that

           A4: x = ( OpenHypercubes q0) and

           A5: q0 in ( RAT n);

          x = (ff . q0)

          proof

            (ff . q0) = F2(q0) by A5, A2;

            hence thesis by A4, A5, Def1;

          end;

          hence x in ( rng ff) by A5, A1, FUNCT_1:def 3;

        end;

        let x be object;

        assume x in ( rng ff);

        then

        consider q0 be object such that

         A6: q0 in ( dom ff) and

         A7: x = (ff . q0) by FUNCT_1:def 3;

        ( RAT n) c= ( REAL n) & q0 in ( RAT n) by NUMBERS: 12, Th5, A6, A1;

        then

        reconsider q1 = q0 as Point of ( Euclid n);

        (ff . q1) = F2(q0) by A6, A1, A2;

        hence x in ( OpenHypercubesRAT n) by A7;

      end;

      ( card ( rng ff)) c= ( card ( dom ff)) by CARD_2: 61;

      hence thesis by A3, A1, WAYBEL12: 1;

    end;

    registration

      let n;

      cluster ( OpenHypercubesRAT n) -> countable;

      coherence by Th16;

    end

    

     Th17: ( union ( OpenHypercubesRAT n)) is countable

    proof

      for Y be set st Y in ( OpenHypercubesRAT n) holds Y is countable

      proof

        let Y be set such that

         A2: Y in ( OpenHypercubesRAT n);

        consider q0 be Point of ( Euclid n) such that

         A3: Y = ( OpenHypercubes q0) and q0 in ( RAT n) by A2;

        thus thesis by A3;

      end;

      hence thesis by CARD_4: 12;

    end;

    registration

      let n;

      cluster ( union ( OpenHypercubesRAT n)) -> countable;

      coherence by Th17;

    end

    

     Th18: ( union ( OpenHypercubesRAT n)) is Subset-Family of ( TOP-REAL n)

    proof

      ( union ( OpenHypercubesRAT n)) c= ( bool the carrier of ( TOP-REAL n))

      proof

        let x be object;

        assume x in ( union ( OpenHypercubesRAT n));

        then

        consider y be set such that

         A1: x in y and

         A2: y in ( OpenHypercubesRAT n) by TARSKI:def 4;

        consider q0 be Point of ( Euclid n) such that

         A3: y = ( OpenHypercubes q0) and q0 in ( RAT n) by A2;

        x in ( bool ( REAL n)) by A1, A3;

        hence thesis by EUCLID: 22;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:19

    

     Th19: ( union ( OpenHypercubesRAT n)) is open Subset-Family of ( TOP-REAL n)

    proof

      reconsider UO = ( union ( OpenHypercubesRAT n)) as Subset-Family of ( TOP-REAL n) by Th18;

      UO is open

      proof

        let P be Subset of ( TOP-REAL n);

        assume P in UO;

        then

        consider X be set such that

         A1: P in X and

         A2: X in ( OpenHypercubesRAT n) by TARSKI:def 4;

        consider q0 be Point of ( Euclid n) such that

         A3: X = ( OpenHypercubes q0) and q0 in ( RAT n) by A2;

        

         A4: ( OpenHypercubes q0) is open;

         the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

        then

        reconsider P0 = P as Subset of ( TopSpaceMetr ( Euclid n));

        P0 is open by A4, A3, A1;

        hence thesis by Th10;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:20

    

     Th20: for O be non empty open Subset of ( TOP-REAL n) holds ex p be Element of ( RAT n) st p in O

    proof

      let O be non empty open Subset of ( TOP-REAL n);

      ( RAT n) is dense Subset of ( TOP-REAL n) by Th15;

      then O meets ( RAT n) by TOPS_1: 45;

      then

      consider x be object such that

       A1: x in O and

       A2: x in ( RAT n) by XBOOLE_0: 3;

      reconsider x as Element of ( RAT n) by A2;

      take x;

      thus thesis by A1;

    end;

    theorem :: SRINGS_5:21

    

     Th21: for cB be Subset-Family of ( TOP-REAL n) st cB = ( union ( OpenHypercubesRAT n)) holds cB is quasi_basis

    proof

      let F be Subset-Family of ( TOP-REAL n);

      assume

       A1: F = ( union ( OpenHypercubesRAT n));

      F is quasi_basis

      proof

        now

          let x be object;

          assume

           A2: x in the topology of ( TOP-REAL n);

          then

          reconsider x1 = x as Subset of ( TOP-REAL n);

          

           A3: x1 is open by A2;

           the TopStruct of ( TOP-REAL n) = ( TopSpaceMetr ( Euclid n)) by EUCLID:def 8;

          then

          reconsider x2 = x1 as Subset of ( TopSpaceMetr ( Euclid n));

          

           A4: x2 is open by A3, Th10;

          set Y = { t where t be Subset of ( TOP-REAL n) : t in F & t c= x1 };

          

           A5: Y is Subset-Family of ( TOP-REAL n)

          proof

            Y c= ( bool the carrier of ( TOP-REAL n))

            proof

              let t be object;

              assume t in Y;

              then

              consider t0 be Subset of ( TOP-REAL n) such that

               A6: t = t0 and t0 in F and t0 c= x1;

              thus t in ( bool the carrier of ( TOP-REAL n)) by A6;

            end;

            hence thesis;

          end;

          

           A7: Y c= F

          proof

            let t be object;

            assume t in Y;

            then

            consider t0 be Subset of ( TOP-REAL n) such that

             A8: t = t0 and

             A9: t0 in F and t0 c= x1;

            thus t in F by A8, A9;

          end;

          x = ( union Y)

          proof

            reconsider x3 = x as set by TARSKI: 1;

            

             A10: x3 c= ( union Y)

            proof

              let t be object;

              assume

               A11: t in x3;

              then t in x2;

              then

              reconsider t1 = t as Point of ( Euclid n);

              consider m1 be non zero Element of NAT such that

               A12: ( OpenHypercube (t1,(1 / m1))) c= x2 by A4, A11, EUCLID_9: 23;

              reconsider t2 = t1 as Point of ( TOP-REAL n) by EUCLID: 67;

              reconsider Invm1Div2 = ((1 / m1) / 2) as positive Real;

              consider e be Point of ( Euclid n) such that t2 = e and

               A13: ( OpenHypercube (t2,((1 / m1) / 2))) = ( OpenHypercube (e,((1 / m1) / 2))) by TIETZE_2:def 1;

              consider q0 be Element of ( RAT n) such that

               A14: q0 in ( OpenHypercube (t2,Invm1Div2)) by A13, Th20;

              q0 in ( RAT n) & ( RAT n) is Subset of ( REAL n) by NUMBERS: 12, Th5;

              then

              reconsider q1 = q0 as Point of ( TOP-REAL n) by EUCLID: 22;

              reconsider r = (Invm1Div2 * 2) as Real;

              

               A15: ( OpenHypercube (q1,(r / 2))) c= ( OpenHypercube (t2,r)) by A14, Th12;

              reconsider q2 = q1 as Point of ( Euclid n) by EUCLID: 67;

              set OO = ( OpenHypercube (q2,Invm1Div2));

               A16:

              now

                thus ( OpenHypercube (t2,r)) = ( OpenHypercube (t2,(1 / m1)));

                consider ez be Point of ( Euclid n) such that

                 A17: t2 = ez and

                 A18: ( OpenHypercube (t2,(1 / m1))) = ( OpenHypercube (ez,(1 / m1))) by TIETZE_2:def 1;

                thus ( OpenHypercube (t1,(1 / m1))) = ( OpenHypercube (t2,(1 / m1))) by A17, A18;

                thus ( OpenHypercube (t1,(1 / m1))) c= x1 by A12;

              end;

              consider er be Point of ( Euclid n) such that

               A19: q2 = er and

               A20: ( OpenHypercube (q1,Invm1Div2)) = ( OpenHypercube (er,Invm1Div2)) by TIETZE_2:def 1;

              

               A21: Invm1Div2 = (1 / (m1 * 2)) by XCMPLX_1: 78;

              

               A22: OO in ( union ( OpenHypercubesRAT n))

              proof

                consider e be Point of ( Euclid n) such that

                 A23: q2 = e and ( OpenHypercube (q2,Invm1Div2)) = ( OpenHypercube (e,Invm1Div2));

                

                 A24: OO in ( OpenHypercubes e) by A21, A23;

                ( OpenHypercubes e) in ( OpenHypercubesRAT n) by A23;

                hence thesis by A24, TARSKI:def 4;

              end;

              t in OO & OO in F & OO c= x1 by A22, A1, A19, A20, A14, Th11, A15, A16;

              then t in OO & OO in Y;

              hence t in ( union Y) by TARSKI:def 4;

            end;

            ( union Y) c= x1

            proof

              let t be object;

              assume t in ( union Y);

              then

              consider Z be set such that

               A25: t in Z and

               A26: Z in Y by TARSKI:def 4;

              consider t0 be Subset of ( TOP-REAL n) such that

               A27: Z = t0 and t0 in F and

               A28: t0 c= x1 by A26;

              thus t in x1 by A25, A27, A28;

            end;

            then x1 = ( union Y) by A10;

            hence thesis;

          end;

          hence x in ( UniCl F) by A5, A7, CANTOR_1:def 1;

        end;

        then the topology of ( TOP-REAL n) c= ( UniCl F);

        hence thesis by CANTOR_1:def 2;

      end;

      hence thesis;

    end;

    

     Th22: ( union ( OpenHypercubesRAT n)) is non empty

    proof

      assume ( union ( OpenHypercubesRAT n)) is empty;

      then

       A1: ( OpenHypercubesRAT n) = { {} } by SCMYCIEL: 18;

      ( OpenHypercubesRAT n) is non empty;

      then

      consider x be object such that

       A2: x in ( OpenHypercubesRAT n);

      consider q be Point of ( Euclid n) such that

       A3: x = ( OpenHypercubes q) and q in ( RAT n) by A2;

      thus contradiction by A3, A1, A2, TARSKI:def 1;

    end;

    registration

      let n;

      cluster ( union ( OpenHypercubesRAT n)) -> non empty;

      coherence by Th22;

    end

    definition

      let n;

      :: SRINGS_5:def6

      func dense_countable_OpenHypercubes (n) -> countable open Subset-Family of ( TOP-REAL n) equals ( union ( OpenHypercubesRAT n));

      coherence by Th19;

    end

    theorem :: SRINGS_5:22

    ( dense_countable_OpenHypercubes n) = { ( OpenHypercube (q,(1 / m))) where q be Point of ( Euclid n), m be positive Nat : q in ( RAT n) }

    proof

      now

        let x be object;

        hereby

          assume x in ( dense_countable_OpenHypercubes n);

          then

          consider y be set such that

           A1: x in y and

           A2: y in ( OpenHypercubesRAT n) by TARSKI:def 4;

          consider z be Point of ( Euclid n) such that

           A3: y = ( OpenHypercubes z) and

           A4: z in ( RAT n) by A2;

          consider m be non zero Element of NAT such that

           A5: x = ( OpenHypercube (z,(1 / m))) by A1, A3;

          thus x in { ( OpenHypercube (q,(1 / m))) where q be Point of ( Euclid n), m be positive Nat : q in ( RAT n) } by A4, A5;

        end;

        assume x in { ( OpenHypercube (q,(1 / m))) where q be Point of ( Euclid n), m be positive Nat : q in ( RAT n) };

        then

        consider q0 be Point of ( Euclid n), m0 be positive Nat such that

         A6: x = ( OpenHypercube (q0,(1 / m0))) and

         A7: q0 in ( RAT n);

        reconsider p = q0 as Point of ( Euclid n);

        reconsider m1 = m0 as non zero Element of NAT by ORDINAL1:def 12;

        ( OpenHypercube (q0,(1 / m0))) = ( OpenHypercube (q0,(1 / m1)));

        then x in ( OpenHypercubes p) & ( OpenHypercubes p) in ( OpenHypercubesRAT n) by A6, A7;

        hence x in ( dense_countable_OpenHypercubes n) by TARSKI:def 4;

      end;

      hence thesis by TARSKI: 2;

    end;

    registration

      let n be Nat;

      cluster countable for Basis of ( TOP-REAL n);

      existence

      proof

        ( dense_countable_OpenHypercubes n) is Basis of ( TOP-REAL n) & ( dense_countable_OpenHypercubes n) is countable by Th21;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:23

    ( dense_countable_OpenHypercubes n) is countable Basis of ( TOP-REAL n) by Th21;

    theorem :: SRINGS_5:24

    

     Th23: for O be open Subset of ( TOP-REAL n) holds ex Y be Subset of ( dense_countable_OpenHypercubes n) st Y is countable & O = ( union Y)

    proof

      let O be open Subset of ( TOP-REAL n);

      the topology of ( TOP-REAL n) c= ( UniCl ( dense_countable_OpenHypercubes n)) by Th21, CANTOR_1:def 2;

      then O in ( UniCl ( dense_countable_OpenHypercubes n)) by PRE_TOPC:def 2;

      then

      consider Y be Subset-Family of ( TOP-REAL n) such that

       A1: Y c= ( dense_countable_OpenHypercubes n) and

       A2: O = ( union Y) by CANTOR_1:def 1;

      thus thesis by A1, A2;

    end;

    theorem :: SRINGS_5:25

    

     Th24: for O be open non empty Subset of ( TOP-REAL n) holds ex Y be Subset of ( dense_countable_OpenHypercubes n) st Y is non empty & O = ( union Y) & ex g be Function of NAT , Y st for x be object holds x in O iff ex y be object st y in NAT & x in (g . y)

    proof

      let O be open non empty Subset of ( TOP-REAL n);

      consider Y be Subset of ( dense_countable_OpenHypercubes n) such that Y is countable and

       A1: O = ( union Y) by Th23;

      take Y;

      thus Y is non empty by A1, ZFMISC_1: 2;

      thus O = ( union Y) by A1;

      consider g be Function of omega , Y such that

       A2: ( rng g) = Y by A1, ZFMISC_1: 2, CARD_3: 96;

      take g;

      

       A3: ( dom g) = omega by A1, ZFMISC_1: 2, FUNCT_2:def 1;

      O = ( Union g) by A1, A2;

      hence thesis by A3, CARD_5: 2;

    end;

    theorem :: SRINGS_5:26

    

     Th25: for O be open non empty Subset of ( TOP-REAL n) holds ex s be sequence of ( dense_countable_OpenHypercubes n) st for x be object holds x in O iff ex y be object st y in NAT & x in (s . y)

    proof

      let O be open non empty Subset of ( TOP-REAL n);

      consider Y be Subset of ( dense_countable_OpenHypercubes n) such that Y is non empty and

       A1: O = ( union Y) and

       A2: ex g be Function of NAT , Y st for x be object holds x in O iff ex y be object st y in NAT & x in (g . y) by Th24;

      consider g be Function of NAT , Y such that

       A3: for x be object holds x in O iff ex y be object st y in NAT & x in (g . y) by A2;

      reconsider g2 = g as sequence of ( dense_countable_OpenHypercubes n) by A1, ZFMISC_1: 2, FUNCT_2: 7;

      for x be object holds x in O iff ex y be object st y in NAT & x in (g2 . y) by A3;

      hence thesis;

    end;

    theorem :: SRINGS_5:27

    for O be open non empty Subset of ( TOP-REAL n) holds ex s be sequence of ( dense_countable_OpenHypercubes n) st O = ( Union s)

    proof

      let O be open non empty Subset of ( TOP-REAL n);

      consider s be sequence of ( dense_countable_OpenHypercubes n) such that

       A1: for x be object holds x in O iff ex y be object st y in NAT & x in (s . y) by Th25;

      

       A2: ( dom s) = NAT by FUNCT_2:def 1;

      take s;

      now

        let x be object;

        hereby

          assume x in O;

          then

          consider y be object such that

           A3: y in NAT and

           A4: x in (s . y) by A1;

          (s . y) in ( rng s) by A3, A2, FUNCT_1:def 3;

          hence x in ( Union s) by A4, TARSKI:def 4;

        end;

        assume x in ( Union s);

        then

        consider y be set such that

         A5: x in y and

         A6: y in ( rng s) by TARSKI:def 4;

        consider z be object such that

         A7: z in ( dom s) and

         A8: y = (s . z) by A6, FUNCT_1:def 3;

        thus x in O by A1, A5, A7, A8;

      end;

      hence thesis by TARSKI: 2;

    end;

    begin

    definition

      :: SRINGS_5:def7

      func the_set_of_all_left_open_real_bounded_intervals -> Subset-Family of REAL equals the set of all ].a, b.] where a,b be Real;

      coherence

      proof

         the set of all ].a, b.] where a,b be Real c= ( bool REAL )

        proof

          let x be object;

          assume x in the set of all ].a, b.] where a,b be Real;

          then ex a0,b0 be Real st x = ].a0, b0.];

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      cluster the_set_of_all_left_open_real_bounded_intervals -> non empty;

      coherence

      proof

         ]. 0 , 0 .] in the_set_of_all_left_open_real_bounded_intervals ;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:28

     the_set_of_all_left_open_real_bounded_intervals c= { I where I be Subset of REAL : I is left_open_interval }

    proof

      let x be object;

      assume x in the_set_of_all_left_open_real_bounded_intervals ;

      then

      consider a,b be Real such that

       A1: x = ].a, b.];

      reconsider x1 = x as Subset of REAL by A1;

      reconsider a as R_eal by XREAL_0:def 1, NUMBERS: 31;

      x1 = ].a, b.] by A1;

      then x1 is left_open_interval by MEASURE5:def 5;

      hence thesis;

    end;

    theorem :: SRINGS_5:29

    

     Th26: the_set_of_all_left_open_real_bounded_intervals is cap-closed diff-finite-partition-closed with_empty_element with_countable_Cover

    proof

       the_set_of_all_left_open_real_bounded_intervals = { ].a, b.] where a,b be Real : a <= b }

      proof

        hereby

          let x be object;

          assume x in the_set_of_all_left_open_real_bounded_intervals ;

          then

          consider a,b be Real such that

           A1: x = ].a, b.];

          per cases ;

            suppose a <= b;

            hence x in { ].a, b.] where a,b be Real : a <= b } by A1;

          end;

            suppose not a <= b;

            then x = ]. 0 , 0 .] by A1, XXREAL_1: 26;

            hence x in { ].a, b.] where a,b be Real : a <= b };

          end;

        end;

        let x be object;

        assume x in { ].a, b.] where a,b be Real : a <= b };

        then ex a,b be Real st x = ].a, b.] & a <= b;

        hence x in the_set_of_all_left_open_real_bounded_intervals ;

      end;

      hence thesis by SRINGS_2: 9;

    end;

    theorem :: SRINGS_5:30

     the_set_of_all_left_open_real_bounded_intervals is Semiring of REAL by Th26, SRINGS_3: 10;

    begin

    definition

      :: SRINGS_5:def8

      func the_set_of_all_right_open_real_bounded_intervals -> Subset-Family of REAL equals the set of all [.a, b.[ where a,b be Real;

      coherence

      proof

         the set of all [.a, b.[ where a,b be Real c= ( bool REAL )

        proof

          let x be object;

          assume x in the set of all [.a, b.[ where a,b be Real;

          then ex a0,b0 be Real st x = [.a0, b0.[;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    registration

      cluster the_set_of_all_right_open_real_bounded_intervals -> non empty;

      coherence

      proof

         [. 0 , 0 .[ in the_set_of_all_right_open_real_bounded_intervals ;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:31

    

     Th27: the_set_of_all_right_open_real_bounded_intervals c= { I where I be Subset of REAL : I is right_open_interval }

    proof

      let x be object;

      assume x in the_set_of_all_right_open_real_bounded_intervals ;

      then

      consider a,b be Real such that

       A1: x = [.a, b.[;

      reconsider x1 = x as Subset of REAL by A1;

      reconsider b as R_eal by XREAL_0:def 1, NUMBERS: 31;

      x1 = [.a, b.[ by A1;

      then x1 is right_open_interval by MEASURE5:def 4;

      hence thesis;

    end;

    

     Th28: the_set_of_all_right_open_real_bounded_intervals is with_empty_element

    proof

       [. 0 , 0 .[ in the_set_of_all_right_open_real_bounded_intervals & [. 0 , 0 .[ = {} ;

      hence thesis;

    end;

    

     Th29: the_set_of_all_right_open_real_bounded_intervals is cap-closed diff-finite-partition-closed with_empty_element

    proof

      { I where I be Subset of REAL : I is right_open_interval } c= ( bool REAL )

      proof

        let x be object;

        assume x in { I where I be Subset of REAL : I is right_open_interval };

        then

        consider I be Subset of REAL such that

         A1: x = I and I is right_open_interval;

        thus thesis by A1;

      end;

      then

      reconsider S = { I where I be Subset of REAL : I is right_open_interval } as Subset-Family of REAL ;

      

       A2: S is cap-closed by SRINGS_3: 27;

      now

        let A,B be set;

        assume

         A3: A in the_set_of_all_right_open_real_bounded_intervals & B in the_set_of_all_right_open_real_bounded_intervals ;

        then

         A4: A in S & B in S by Th27;

        then

        consider I be Subset of REAL such that

         A5: A = I & I is right_open_interval;

        consider J be Subset of REAL such that

         A6: B = J & J is right_open_interval by A4;

        S is cap-closed & I in S & J in S by A5, A6, SRINGS_3: 27;

        then (I /\ J) in S by FINSUB_1:def 2;

        then

        consider K be Subset of REAL such that

         A7: (I /\ J) = K and

         A8: K is right_open_interval;

        consider a be Real, b be R_eal such that

         A9: K = [.a, b.[ by A8, MEASURE5:def 4;

        per cases ;

          suppose

           A10: K is non empty;

          consider x be object such that

           A11: x in K by A10;

          reconsider x as Real by A11;

          b is Real

          proof

            assume not b is Real;

            then not b in REAL & a in REAL & a <= b by XREAL_0:def 1, A10, A9, XXREAL_1: 27;

            then

             A12: b = +infty by XXREAL_0: 10;

            a <= x by A11, A9, XXREAL_1: 3;

            then

             A13: [.x, +infty .[ c= A & [.x, +infty .[ c= B by A9, A12, XXREAL_1: 38, A5, A6, A7, XBOOLE_1: 18;

            consider xa,xb be Real such that

             A14: A = [.xa, xb.[ by A3;

            

             A15: not xb in A by A14, XXREAL_1: 3;

            per cases ;

              suppose xb < x;

              then

               A16: not x in A by A14, XXREAL_1: 3;

              x < b by A11, A9, XXREAL_1: 3;

              hence contradiction by A16, A13, A12, XXREAL_1: 3;

            end;

              suppose x <= xb;

              hence contradiction by A15, A13, XXREAL_1: 236;

            end;

          end;

          then

          reconsider b as Real;

          K = [.a, b.[ by A9;

          hence (A /\ B) in the_set_of_all_right_open_real_bounded_intervals by A7, A5, A6;

        end;

          suppose K is empty;

          hence (A /\ B) in the_set_of_all_right_open_real_bounded_intervals by A7, A5, A6, Th28, SETFAM_1:def 8;

        end;

      end;

      hence the_set_of_all_right_open_real_bounded_intervals is cap-closed by FINSUB_1:def 2;

      now

        let A,B be Element of the_set_of_all_right_open_real_bounded_intervals ;

        assume

         A17: (A \ B) is non empty;

        

         A18: A in S & B in S by Th27;

        then

        consider I be Subset of REAL such that

         A19: A = I and I is right_open_interval;

        consider J be Subset of REAL such that

         A20: B = J and J is right_open_interval by A18;

        S is semi-diff-closed & S is non empty by SRINGS_3: 27;

        then S is diff-c=-finite-partition-closed by SRINGS_3: 9;

        then S is diff-finite-partition-closed & I is Element of S & J is Element of S & (I \ J) is non empty by A17, A19, A20, A2, Th27;

        then

        consider x be finite Subset of S such that

         A21: x is a_partition of (I \ J) by SRINGS_1:def 2;

        now

          x in ( bool the_set_of_all_right_open_real_bounded_intervals )

          proof

            reconsider x1 = x as set;

            x1 c= the_set_of_all_right_open_real_bounded_intervals

            proof

              let t be object;

              assume

               A22: t in x1;

              then t in S;

              then

              consider K be Subset of REAL such that

               A23: t = K and

               A24: K is right_open_interval;

              per cases ;

                suppose K is empty;

                hence thesis by A23, Th28, SETFAM_1:def 8;

              end;

                suppose

                 A25: K is non empty;

                consider a be Real, b be R_eal such that

                 A26: K = [.a, b.[ by A24, MEASURE5:def 4;

                

                 A27: K c= (A \ B) & (A \ B) c= A by A22, A23, A21, A19, A20, XBOOLE_1: 36;

                A in the_set_of_all_right_open_real_bounded_intervals ;

                then

                consider e,c be Real such that

                 A28: A = [.e, c.[;

                now

                  thus a is Real & c is Real;

                  thus b is R_eal;

                  thus a < b by A25, A26, XXREAL_1: 27;

                  now

                    let x be object;

                    assume

                     A29: x in [.a, b.[;

                    then

                     A30: x in [.e, c.[ by A26, A27, A28;

                    reconsider x1 = x as ExtReal by A29;

                    a <= x1 & x1 < b & e <= x1 & x1 < c by A29, A30, XXREAL_1: 3;

                    hence x in [.a, c.[ by XXREAL_1: 3;

                  end;

                  hence [.a, b.[ c= [.a, c.[;

                end;

                then b is Real by Th4;

                hence thesis by A26, A23;

              end;

            end;

            hence thesis;

          end;

          hence x is finite Subset of the_set_of_all_right_open_real_bounded_intervals ;

          reconsider x1 = x as Subset-Family of (A \ B) by A21, A19, A20;

          thus x is a_partition of (A \ B) by A19, A20, A21;

        end;

        hence ex x be finite Subset of the_set_of_all_right_open_real_bounded_intervals st x is a_partition of (A \ B);

      end;

      hence the_set_of_all_right_open_real_bounded_intervals is diff-finite-partition-closed with_empty_element by SRINGS_1:def 2, Th28;

    end;

    

     Th30: the_set_of_all_right_open_real_bounded_intervals is with_countable_Cover

    proof

      defpred F[ object, object] means $1 is Element of NAT & $2 in the_set_of_all_right_open_real_bounded_intervals & ex x be real number st x = $1 & $2 = [.( - x), x.[;

      

       A1: for x be object st x in NAT holds ex y be object st y in the_set_of_all_right_open_real_bounded_intervals & F[x, y]

      proof

        let x be object;

        assume

         A2: x in NAT ;

        then

        reconsider x as real number;

        set y = [.( - x), x.[;

        y in the_set_of_all_right_open_real_bounded_intervals & F[x, y] by A2;

        hence thesis;

      end;

      consider f be Function such that

       A3: ( dom f) = NAT & ( rng f) c= the_set_of_all_right_open_real_bounded_intervals and

       A4: for x be object st x in NAT holds F[x, (f . x)] from FUNCT_1:sch 6( A1);

      

       A5: ( rng f) is Subset-Family of REAL by A3, XBOOLE_1: 1;

      

       A6: ( rng f) is countable

      proof

        reconsider f as SetSequence of REAL by A3, A5, RELSET_1: 4, FUNCT_2:def 1;

        ( rng f) is countable by TOPGEN_4: 58;

        hence thesis;

      end;

      ( rng f) is Cover of REAL

      proof

        ( Union f) = REAL

        proof

          thus ( Union f) c= REAL

          proof

            let x be object;

            assume x in ( Union f);

            then

            consider t be object such that

             A7: t in ( dom f) & x in (f . t) by CARD_5: 2;

            consider x0 be real number such that

             A8: x0 = t & (f . t) = [.( - x0), x0.[ by A3, A4, A7;

            thus thesis by A7, A8;

          end;

          for x be object st x in REAL holds x in ( Union f)

          proof

            let x be object;

            assume x in REAL ;

            then

            reconsider x as Real;

            consider n be Element of NAT such that

             A9: |.x.| <= n by MESFUNC1: 8;

            x in (f . (n + 1))

            proof

              consider z be real number such that

               A10: z = (n + 1) & (f . (n + 1)) = [.( - z), z.[ by A4;

              

               A11: x < (n + 1)

              proof

                assume

                 A12: not x < (n + 1);

                x <= n by A9, ABSVALUE:def 1;

                then (n + 1) <= n by A12, XXREAL_0: 2;

                hence contradiction by NAT_1: 13;

              end;

              ( - (n + 1)) <= x

              proof

                per cases ;

                  suppose 0 <= x;

                  hence thesis;

                end;

                  suppose x < 0 ;

                  then ( - x) <= n by A9, ABSVALUE:def 1;

                  then ( - n) <= ( - ( - x)) by XREAL_1: 24;

                  then

                   A13: (( - n) - 1) <= (x - 1) by XREAL_1: 13;

                  (x - 1) <= (x - 0 ) by XREAL_1: 13;

                  hence thesis by A13, XXREAL_0: 2;

                end;

              end;

              hence thesis by A10, A11, XXREAL_1: 3;

            end;

            then x in (f . (n + 1)) & (f . (n + 1)) in ( rng f) by A3, FUNCT_1:def 3;

            hence thesis by TARSKI:def 4;

          end;

          hence thesis;

        end;

        hence thesis by A5, SETFAM_1: 45;

      end;

      hence thesis by A3, A6, SRINGS_1:def 4;

    end;

    registration

      cluster the_set_of_all_right_open_real_bounded_intervals -> cap-closed diff-finite-partition-closed with_empty_element with_countable_Cover;

      coherence by Th29, Th30;

    end

    theorem :: SRINGS_5:32

     the_set_of_all_right_open_real_bounded_intervals is Semiring of REAL by SRINGS_3: 10;

    begin

    reserve n for non zero Nat;

    definition

      let n be non zero Nat;

      :: SRINGS_5:def9

      func ProductLeftOpenIntervals (n) -> ClassicalSemiringFamily of ( ProductREAL n) equals (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals );

      coherence

      proof

        reconsider S = (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals ) as n -element FinSequence by Th6;

        for i be Nat st i in ( Seg n) holds (S . i) is with_empty_element semi-diff-closed cap-closed Subset-Family of (( ProductREAL n) . i)

        proof

          let i be Nat;

          assume

           A1: i in ( Seg n);

          then

           A2: (S . i) = the_set_of_all_left_open_real_bounded_intervals & (( ProductREAL n) . i) = REAL by FUNCOP_1: 7;

          reconsider Si = (S . i) as Subset-Family of REAL by A1, FUNCOP_1: 7;

          thus thesis by A2, Th26, SRINGS_3: 10;

        end;

        hence thesis by SRINGS_4:def 6;

      end;

    end

    theorem :: SRINGS_5:33

    ( ProductLeftOpenIntervals n) = (( Seg n) --> the set of all ].a, b.] where a,b be Real);

    theorem :: SRINGS_5:34

    

     Th30: ( MeasurableRectangle ( ProductLeftOpenIntervals n)) is Semiring of ( REAL n)

    proof

      ( MeasurableRectangle ( ProductLeftOpenIntervals n)) is Semiring of ( product ( ProductREAL n)) by SRINGS_4: 40;

      hence thesis by Th7;

    end;

    theorem :: SRINGS_5:35

    for x be object st x in ( MeasurableRectangle ( ProductLeftOpenIntervals n)) holds ex y be Subset of ( REAL n) st x = y & for i be Nat st i in ( Seg n) holds ex a,b be Real st for t be Element of ( REAL n) st t in y holds (t . i) in ].a, b.]

    proof

      let x be object;

      assume

       A1: x in ( MeasurableRectangle ( ProductLeftOpenIntervals n));

      ( MeasurableRectangle ( ProductLeftOpenIntervals n)) is Subset-Family of ( REAL n) by Th30;

      then

      reconsider y = x as Subset of ( REAL n) by A1;

      reconsider x0 = x as set by TARSKI: 1;

      consider g be Function such that

       A2: x = ( product g) and

       A3: g in ( product ( ProductLeftOpenIntervals n)) by A1, SRINGS_4:def 4;

      ( dom ( ProductLeftOpenIntervals n)) = ( Seg n) by FUNCOP_1: 13;

      then

       A4: ( dom g) = ( Seg n) by A3, CARD_3: 9;

      take y;

      thus x = y;

      now

        let i be Nat;

        assume

         A5: i in ( Seg n);

        then i in ( dom ( ProductLeftOpenIntervals n)) by FUNCOP_1: 13;

        then (g . i) in (( ProductLeftOpenIntervals n) . i) by A3, CARD_3: 9;

        then (g . i) in the set of all ].a, b.] where a,b be Real by A5, FUNCOP_1: 7;

        then

        consider a,b be Real such that

         A6: (g . i) = ].a, b.];

        hereby

          take a, b;

          now

            let t be Element of ( REAL n);

            assume t in y;

            then

            consider j0 be Function such that

             A7: t = j0 and ( dom j0) = ( Seg n) and

             A8: for u be object st u in ( Seg n) holds (j0 . u) in (g . u) by A2, CARD_3:def 5, A4;

            thus (t . i) in ].a, b.] by A7, A6, A8, A5;

          end;

          hence ex a,b be Real st for t be Element of ( REAL n) st t in y holds (t . i) in ].a, b.];

        end;

        hence ex a,b be Real st for t be Element of ( REAL n) st t in y holds (t . i) in ].a, b.];

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:36

    

     Th31: for x be object st x in ( MeasurableRectangle ( ProductLeftOpenIntervals n)) holds ex y be Subset of ( REAL n), f be n -element FinSequence of [: REAL , REAL :] st x = y & (for t be Element of ( REAL n) holds t in y iff for i be Nat st i in ( Seg n) holds (t . i) in ].((f /. i) `1 ), ((f /. i) `2 ).])

    proof

      let x be object;

      assume

       A1: x in ( MeasurableRectangle ( ProductLeftOpenIntervals n));

      ( MeasurableRectangle ( ProductLeftOpenIntervals n)) is Subset-Family of ( REAL n) by Th30;

      then

      reconsider y = x as Subset of ( REAL n) by A1;

      take y;

      reconsider x0 = x as set by TARSKI: 1;

      consider g be Function such that

       A2: x = ( product g) and

       A3: g in ( product ( ProductLeftOpenIntervals n)) by A1, SRINGS_4:def 4;

      ( dom ( ProductLeftOpenIntervals n)) = ( Seg n) by FUNCOP_1: 13;

      then

       A4: ( dom g) = ( Seg n) by A3, CARD_3: 9;

       A5:

      now

        let i be Nat;

        assume

         A6: i in ( Seg n);

        then i in ( dom ( ProductLeftOpenIntervals n)) by FUNCOP_1: 13;

        then (g . i) in (( ProductLeftOpenIntervals n) . i) by A3, CARD_3: 9;

        then (g . i) in the_set_of_all_left_open_real_bounded_intervals by A6, FUNCOP_1: 7;

        hence ex a,b be Real st (g . i) = ].a, b.];

      end;

      defpred P[ Nat, set] means ex x be Element of [: REAL , REAL :] st $2 = x & (g . $1) = ].(x `1 ), (x `2 ).];

      

       A7: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then

        consider a,b be Real such that

         A8: (g . i) = ].a, b.] by A5;

        set d = [a, b];

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        d is Element of [: REAL , REAL :] & (g . i) = ].(d `1 ), (d `2 ).] by A8;

        hence thesis;

      end;

      ex f2 be FinSequence of [: REAL , REAL :] st ( len f2) = n & for i be Nat st i in ( Seg n) holds P[i, (f2 /. i)] from FINSEQ_4:sch 1( A7);

      then

      consider f2 be FinSequence of [: REAL , REAL :] such that

       A9: ( len f2) = n and

       A10: for i be Nat st i in ( Seg n) holds ex x be Element of [: REAL , REAL :] st (f2 /. i) = x & (g . i) = ].(x `1 ), (x `2 ).];

      reconsider f2 as n -element FinSequence of [: REAL , REAL :] by A9, CARD_1:def 7;

      take f2;

      thus x = y;

      

       A11: for i be Nat st i in ( Seg n) holds (g . i) = ].((f2 /. i) `1 ), ((f2 /. i) `2 ).]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then

        consider x be Element of [: REAL , REAL :] such that

         A12: (f2 /. i) = x and

         A13: (g . i) = ].(x `1 ), (x `2 ).] by A10;

        thus thesis by A12, A13;

      end;

      

       A14: for t be Element of ( REAL n) st t in y holds for i be Nat st i in ( Seg n) holds (t . i) in ].((f2 /. i) `1 ), ((f2 /. i) `2 ).]

      proof

        let t be Element of ( REAL n);

        assume t in y;

        then

        consider j0 be Function such that

         A15: t = j0 and ( dom j0) = ( Seg n) and

         A16: for y be object st y in ( Seg n) holds (j0 . y) in (g . y) by A2, CARD_3:def 5, A4;

        now

          let i be Nat;

          assume

           A17: i in ( Seg n);

          then (t . i) in (g . i) by A15, A16;

          hence (t . i) in ].((f2 /. i) `1 ), ((f2 /. i) `2 ).] by A17, A11;

        end;

        hence thesis;

      end;

      for t be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (t . i) in ].((f2 /. i) `1 ), ((f2 /. i) `2 ).] holds t in y

      proof

        let t be Element of ( REAL n);

        assume

         A18: for i be Nat st i in ( Seg n) holds (t . i) in ].((f2 /. i) `1 ), ((f2 /. i) `2 ).];

        reconsider j = t as Function;

        t is Element of ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

        then

         A19: ex j0 be Function st j = j0 & ( dom j0) = ( Seg n) & ( rng j0) c= REAL by FUNCT_2:def 2;

        for y be object st y in ( Seg n) holds (j . y) in (g . y)

        proof

          let y be object;

          assume

           A20: y in ( Seg n);

          then

          reconsider y1 = y as Nat;

          (g . y1) = ].((f2 /. y1) `1 ), ((f2 /. y1) `2 ).] by A20, A11;

          hence thesis by A20, A18;

        end;

        hence t in y by A19, A2, CARD_3:def 5, A4;

      end;

      hence thesis by A14;

    end;

    theorem :: SRINGS_5:37

    

     Th32: for x be object st x in ( MeasurableRectangle ( ProductLeftOpenIntervals n)) holds ex y be Subset of ( REAL n), a,b be Element of ( REAL n) st x = y & for s be object holds s in y iff (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])

    proof

      let x be object;

      assume x in ( MeasurableRectangle ( ProductLeftOpenIntervals n));

      then

      consider y be Subset of ( REAL n), f be n -element FinSequence of [: REAL , REAL :] such that

       A1: x = y and

       A2: (for t be Element of ( REAL n) holds t in y iff for i be Nat st i in ( Seg n) holds (t . i) in ].((f /. i) `1 ), ((f /. i) `2 ).]) by Th31;

      consider x1 be Element of [:( REAL n), ( REAL n):] such that

       A3: for i be Nat st i in ( Seg n) holds ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by Th13;

      consider y1,z1 be object such that

       A4: y1 in ( REAL n) and

       A5: z1 in ( REAL n) and

       A6: x1 = [y1, z1] by ZFMISC_1:def 2;

      reconsider y1, z1 as Element of ( REAL n) by A4, A5;

      take y, y1, z1;

      thus x = y by A1;

      thus for s be object holds (s in y) iff (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in ].(y1 . i), (z1 . i).])

      proof

        let s be object;

        hereby

          assume

           A8: s in y;

          then

          reconsider t = s as Element of ( REAL n);

          now

            take t;

            thus s = t;

            hereby

              let i be Nat;

              assume

               A9: i in ( Seg n);

              then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

              hence (t . i) in ].(y1 . i), (z1 . i).] by A6, A8, A9, A2;

            end;

          end;

          hence (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in ].(y1 . i), (z1 . i).]);

        end;

        assume (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in ].(y1 . i), (z1 . i).]);

        then

        consider t be Element of ( REAL n) such that

         A10: s = t and

         A11: for i be Nat st i in ( Seg n) holds (t . i) in ].(y1 . i), (z1 . i).];

        now

          let i be Nat;

          assume

           A12: i in ( Seg n);

          then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

          hence (t . i) in ].((f /. i) `1 ), ((f /. i) `2 ).] by A11, A12, A6;

        end;

        hence s in y by A10, A2;

      end;

    end;

    theorem :: SRINGS_5:38

    for x be set st x in ( MeasurableRectangle ( ProductLeftOpenIntervals n)) holds ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])

    proof

      let x be set;

      assume x in ( MeasurableRectangle ( ProductLeftOpenIntervals n));

      then

      consider y be Subset of ( REAL n), f be n -element FinSequence of [: REAL , REAL :] such that

       A1: x = y and

       A2: (for t be Element of ( REAL n) holds t in y iff for i be Nat st i in ( Seg n) holds (t . i) in ].((f /. i) `1 ), ((f /. i) `2 ).]) by Th31;

      consider x1 be Element of [:( REAL n), ( REAL n):] such that

       A3: for i be Nat st i in ( Seg n) holds ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by Th13;

      consider y1,z1 be object such that

       A4: y1 in ( REAL n) and

       A5: z1 in ( REAL n) and

       A6: x1 = [y1, z1] by ZFMISC_1:def 2;

      reconsider y1, z1 as Element of ( REAL n) by A4, A5;

      take y1, z1;

      for t be Element of ( REAL n) holds t in x iff for i be Nat st i in ( Seg n) holds (t . i) in ].(y1 . i), (z1 . i).]

      proof

         A7:

        now

          let t be Element of ( REAL n);

          assume

           A8: t in x;

          hereby

            let i be Nat;

            assume

             A9: i in ( Seg n);

            then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

            hence (t . i) in ].(y1 . i), (z1 . i).] by A6, A8, A9, A1, A2;

          end;

        end;

        now

          let t be Element of ( REAL n);

          assume

           A10: for i be Nat st i in ( Seg n) holds (t . i) in ].(y1 . i), (z1 . i).];

          now

            let i be Nat;

            assume

             A11: i in ( Seg n);

            then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

            hence (t . i) in ].((f /. i) `1 ), ((f /. i) `2 ).] by A10, A11, A6;

          end;

          hence t in x by A1, A2;

        end;

        hence thesis by A7;

      end;

      hence thesis;

    end;

    begin

    definition

      let n be non zero Nat;

      :: SRINGS_5:def10

      func ProductRightOpenIntervals (n) -> ClassicalSemiringFamily of ( ProductREAL n) equals (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals );

      coherence

      proof

        reconsider S = (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals ) as n -element FinSequence by Th6;

        for i be Nat st i in ( Seg n) holds (S . i) is with_empty_element semi-diff-closed cap-closed Subset-Family of (( ProductREAL n) . i)

        proof

          let i be Nat;

          assume

           A1: i in ( Seg n);

          then

           A2: (S . i) = the_set_of_all_right_open_real_bounded_intervals & (( ProductREAL n) . i) = REAL by FUNCOP_1: 7;

          reconsider Si = (S . i) as Subset-Family of REAL by A1, FUNCOP_1: 7;

          thus thesis by A2, SRINGS_3: 10;

        end;

        hence thesis by SRINGS_4:def 6;

      end;

    end

    reserve n for non zero Nat;

    theorem :: SRINGS_5:39

    ( ProductRightOpenIntervals n) = (( Seg n) --> the set of all [.a, b.[ where a,b be Real);

    theorem :: SRINGS_5:40

    

     Th33: ( MeasurableRectangle ( ProductRightOpenIntervals n)) is Semiring of ( REAL n)

    proof

      ( MeasurableRectangle ( ProductRightOpenIntervals n)) is Semiring of ( product ( ProductREAL n)) by SRINGS_4: 40;

      hence thesis by Th7;

    end;

    theorem :: SRINGS_5:41

    for x be object st x in ( MeasurableRectangle ( ProductRightOpenIntervals n)) holds ex y be Subset of ( REAL n) st x = y & for i be Nat st i in ( Seg n) holds ex a,b be Real st for t be Element of ( REAL n) st t in y holds (t . i) in [.a, b.[

    proof

      let x be object;

      assume

       A1: x in ( MeasurableRectangle ( ProductRightOpenIntervals n));

      ( MeasurableRectangle ( ProductRightOpenIntervals n)) is Subset-Family of ( REAL n) by Th33;

      then

      reconsider y = x as Subset of ( REAL n) by A1;

      reconsider x0 = x as set by TARSKI: 1;

      consider g be Function such that

       A2: x = ( product g) and

       A3: g in ( product ( ProductRightOpenIntervals n)) by A1, SRINGS_4:def 4;

      ( dom ( ProductRightOpenIntervals n)) = ( Seg n) by FUNCOP_1: 13;

      then

       A4: ( dom g) = ( Seg n) by A3, CARD_3: 9;

      take y;

      thus x = y;

      now

        let i be Nat;

        assume

         A5: i in ( Seg n);

        then i in ( dom ( ProductRightOpenIntervals n)) by FUNCOP_1: 13;

        then (g . i) in (( ProductRightOpenIntervals n) . i) by A3, CARD_3: 9;

        then (g . i) in the set of all [.a, b.[ where a,b be Real by A5, FUNCOP_1: 7;

        then

        consider a,b be Real such that

         A6: (g . i) = [.a, b.[;

        hereby

          take a, b;

          now

            let t be Element of ( REAL n);

            assume t in y;

            then

            consider j0 be Function such that

             A7: t = j0 and ( dom j0) = ( Seg n) and

             A8: for u be object st u in ( Seg n) holds (j0 . u) in (g . u) by A2, CARD_3:def 5, A4;

            thus (t . i) in [.a, b.[ by A7, A6, A8, A5;

          end;

          hence ex a,b be Real st for t be Element of ( REAL n) st t in y holds (t . i) in [.a, b.[;

        end;

        hence ex a,b be Real st for t be Element of ( REAL n) st t in y holds (t . i) in [.a, b.[;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:42

    

     Th34: for x be object st x in ( MeasurableRectangle ( ProductRightOpenIntervals n)) holds ex y be Subset of ( REAL n), f be n -element FinSequence of [: REAL , REAL :] st x = y & (for t be Element of ( REAL n) holds t in y iff for i be Nat st i in ( Seg n) holds (t . i) in [.((f /. i) `1 ), ((f /. i) `2 ).[)

    proof

      let x be object;

      assume

       A1: x in ( MeasurableRectangle ( ProductRightOpenIntervals n));

      ( MeasurableRectangle ( ProductRightOpenIntervals n)) is Subset-Family of ( REAL n) by Th33;

      then

      reconsider y = x as Subset of ( REAL n) by A1;

      take y;

      reconsider x0 = x as set by TARSKI: 1;

      consider g be Function such that

       A2: x = ( product g) and

       A3: g in ( product ( ProductRightOpenIntervals n)) by A1, SRINGS_4:def 4;

      ( dom ( ProductRightOpenIntervals n)) = ( Seg n) by FUNCOP_1: 13;

      then

       A4: ( dom g) = ( Seg n) by A3, CARD_3: 9;

       A5:

      now

        let i be Nat;

        assume

         A6: i in ( Seg n);

        then i in ( dom ( ProductRightOpenIntervals n)) by FUNCOP_1: 13;

        then (g . i) in (( ProductRightOpenIntervals n) . i) by A3, CARD_3: 9;

        then (g . i) in the_set_of_all_right_open_real_bounded_intervals by A6, FUNCOP_1: 7;

        hence ex a,b be Real st (g . i) = [.a, b.[;

      end;

      defpred P[ Nat, set] means ex x be Element of [: REAL , REAL :] st $2 = x & (g . $1) = [.(x `1 ), (x `2 ).[;

      

       A7: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then

        consider a,b be Real such that

         A8: (g . i) = [.a, b.[ by A5;

        set d = [a, b];

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        d is Element of [: REAL , REAL :] & (g . i) = [.(d `1 ), (d `2 ).[ by A8;

        hence thesis;

      end;

      ex f2 be FinSequence of [: REAL , REAL :] st ( len f2) = n & for i be Nat st i in ( Seg n) holds P[i, (f2 /. i)] from FINSEQ_4:sch 1( A7);

      then

      consider f2 be FinSequence of [: REAL , REAL :] such that

       A9: ( len f2) = n and

       A10: for i be Nat st i in ( Seg n) holds ex x be Element of [: REAL , REAL :] st (f2 /. i) = x & (g . i) = [.(x `1 ), (x `2 ).[;

      reconsider f2 as n -element FinSequence of [: REAL , REAL :] by A9, CARD_1:def 7;

      take f2;

      thus x = y;

      

       A11: for i be Nat st i in ( Seg n) holds (g . i) = [.((f2 /. i) `1 ), ((f2 /. i) `2 ).[

      proof

        let i be Nat;

        assume i in ( Seg n);

        then

        consider x be Element of [: REAL , REAL :] such that

         A12: (f2 /. i) = x and

         A13: (g . i) = [.(x `1 ), (x `2 ).[ by A10;

        thus thesis by A12, A13;

      end;

      

       A14: for t be Element of ( REAL n) st t in y holds for i be Nat st i in ( Seg n) holds (t . i) in [.((f2 /. i) `1 ), ((f2 /. i) `2 ).[

      proof

        let t be Element of ( REAL n);

        assume t in y;

        then

        consider j0 be Function such that

         A15: t = j0 and ( dom j0) = ( Seg n) and

         A16: for y be object st y in ( Seg n) holds (j0 . y) in (g . y) by A2, CARD_3:def 5, A4;

        let i be Nat;

        assume

         A17: i in ( Seg n);

        then (t . i) in (g . i) by A15, A16;

        hence (t . i) in [.((f2 /. i) `1 ), ((f2 /. i) `2 ).[ by A17, A11;

      end;

      for t be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (t . i) in [.((f2 /. i) `1 ), ((f2 /. i) `2 ).[ holds t in y

      proof

        let t be Element of ( REAL n);

        assume

         A18: for i be Nat st i in ( Seg n) holds (t . i) in [.((f2 /. i) `1 ), ((f2 /. i) `2 ).[;

        reconsider j = t as Function;

        t is Element of ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

        then

         A19: ex j0 be Function st j = j0 & ( dom j0) = ( Seg n) & ( rng j0) c= REAL by FUNCT_2:def 2;

        for y be object st y in ( Seg n) holds (j . y) in (g . y)

        proof

          let y be object;

          assume

           A20: y in ( Seg n);

          then

          reconsider y1 = y as Nat;

          (g . y1) = [.((f2 /. y1) `1 ), ((f2 /. y1) `2 ).[ by A20, A11;

          hence thesis by A20, A18;

        end;

        hence t in y by A19, A2, CARD_3:def 5, A4;

      end;

      hence thesis by A14;

    end;

    theorem :: SRINGS_5:43

    

     Th35: for x be object st x in ( MeasurableRectangle ( ProductRightOpenIntervals n)) holds ex y be Subset of ( REAL n), a,b be Element of ( REAL n) st x = y & for s be object holds s in y iff (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)

    proof

      let x be object;

      assume x in ( MeasurableRectangle ( ProductRightOpenIntervals n));

      then

      consider y be Subset of ( REAL n), f be n -element FinSequence of [: REAL , REAL :] such that

       A1: x = y and

       A2: (for t be Element of ( REAL n) holds t in y iff for i be Nat st i in ( Seg n) holds (t . i) in [.((f /. i) `1 ), ((f /. i) `2 ).[) by Th34;

      consider x1 be Element of [:( REAL n), ( REAL n):] such that

       A3: for i be Nat st i in ( Seg n) holds ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by Th13;

      consider y1,z1 be object such that

       A4: y1 in ( REAL n) and

       A5: z1 in ( REAL n) and

       A6: x1 = [y1, z1] by ZFMISC_1:def 2;

      reconsider y1, z1 as Element of ( REAL n) by A4, A5;

      take y, y1, z1;

      thus x = y by A1;

      thus for s be object holds s in y iff (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in [.(y1 . i), (z1 . i).[)

      proof

        let s be object;

        hereby

          assume

           A8: s in y;

          then

          reconsider t = s as Element of ( REAL n);

          now

            take t;

            thus s = t;

            hereby

              let i be Nat;

              assume

               A9: i in ( Seg n);

              then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

              hence (t . i) in [.(y1 . i), (z1 . i).[ by A6, A8, A9, A2;

            end;

          end;

          hence (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in [.(y1 . i), (z1 . i).[);

        end;

        given t be Element of ( REAL n) such that

         A10: s = t and

         A11: for i be Nat st i in ( Seg n) holds (t . i) in [.(y1 . i), (z1 . i).[;

        now

          let i be Nat;

          assume

           A12: i in ( Seg n);

          then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

          hence (t . i) in [.((f /. i) `1 ), ((f /. i) `2 ).[ by A11, A12, A6;

        end;

        hence s in y by A10, A2;

      end;

    end;

    theorem :: SRINGS_5:44

    for x be set st x in ( MeasurableRectangle ( ProductRightOpenIntervals n)) holds ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)

    proof

      let x be set;

      assume x in ( MeasurableRectangle ( ProductRightOpenIntervals n));

      then

      consider y be Subset of ( REAL n), f be n -element FinSequence of [: REAL , REAL :] such that

       A1: x = y and

       A2: (for t be Element of ( REAL n) holds t in y iff for i be Nat st i in ( Seg n) holds (t . i) in [.((f /. i) `1 ), ((f /. i) `2 ).[) by Th34;

      consider x1 be Element of [:( REAL n), ( REAL n):] such that

       A3: for i be Nat st i in ( Seg n) holds ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by Th13;

      consider y1,z1 be object such that

       A4: y1 in ( REAL n) and

       A5: z1 in ( REAL n) and

       A6: x1 = [y1, z1] by ZFMISC_1:def 2;

      reconsider y1, z1 as Element of ( REAL n) by A4, A5;

      take y1, z1;

      for t be Element of ( REAL n) holds t in x iff for i be Nat st i in ( Seg n) holds (t . i) in [.(y1 . i), (z1 . i).[

      proof

         A7:

        now

          let t be Element of ( REAL n);

          assume

           A8: t in x;

          hereby

            let i be Nat;

            assume

             A9: i in ( Seg n);

            then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

            hence (t . i) in [.(y1 . i), (z1 . i).[ by A6, A8, A9, A1, A2;

          end;

        end;

        now

          let t be Element of ( REAL n);

          assume

           A10: for i be Nat st i in ( Seg n) holds (t . i) in [.(y1 . i), (z1 . i).[;

          now

            let i be Nat;

            assume

             A11: i in ( Seg n);

            then ((x1 `1 ) . i) = ((f /. i) `1 ) & ((x1 `2 ) . i) = ((f /. i) `2 ) by A3;

            hence (t . i) in [.((f /. i) `1 ), ((f /. i) `2 ).[ by A10, A11, A6;

          end;

          hence t in x by A1, A2;

        end;

        hence thesis by A7;

      end;

      hence thesis;

    end;

    begin

    reserve n for Nat,

X for set,

S for Subset-Family of X;

    definition

      let n, X;

      :: SRINGS_5:def11

      func Product (n,X) -> set means

      : Def2: for f be object holds f in it iff ex g be Function st f = ( product g) & g in ( product (( Seg n) --> X));

      existence

      proof

        defpred P[ object] means ex g be Function st $1 = ( product g) & g in ( product (( Seg n) --> X));

        consider Y be set such that

         A1: for x be object holds x in Y iff x in ( bool ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X)))))) & P[x] from XBOOLE_0:sch 1;

        take Y;

        now

          thus for x be object st x in Y holds ex g be Function st x = ( product g) & g in ( product (( Seg n) --> X)) by A1;

          let x be object;

          assume

           A2: ex g be Function st x = ( product g) & g in ( product (( Seg n) --> X));

          given g be Function such that

           A3: x = ( product g) and

           A4: g in ( product (( Seg n) --> X));

          

           A5: ( dom g) = ( dom (( Seg n) --> X)) by A4, CARD_3: 9;

          ( rng g) c= ( Union (( Seg n) --> X))

          proof

            let t be object;

            assume t in ( rng g);

            then

            consider u be object such that

             A6: u in ( dom g) and

             A7: t = (g . u) by FUNCT_1:def 3;

            consider h be Function such that

             A8: g = h and

             A9: ( dom h) = ( dom (( Seg n) --> X)) and

             A10: for v be object st v in ( dom (( Seg n) --> X)) holds (h . v) in ((( Seg n) --> X) . v) by A4, CARD_3:def 5;

            t in ((( Seg n) --> X) . u) & ((( Seg n) --> X) . u) in ( rng (( Seg n) --> X)) by A8, A9, A10, A6, A7, FUNCT_1:def 3;

            hence thesis by TARSKI:def 4;

          end;

          then ( Union g) c= ( union ( Union (( Seg n) --> X))) by ZFMISC_1: 77;

          then ( Funcs (( dom g),( Union g))) c= ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X))))) by A5, FUNCT_5: 56;

          then

           A11: ( bool ( Funcs (( dom g),( Union g)))) c= ( bool ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X)))))) by ZFMISC_1: 67;

          ( product g) c= ( Funcs (( dom g),( Union g))) by FUNCT_6: 1;

          hence x in Y by A2, A1, A3, A11;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let S1,S2 be set such that

         A12: for f be object holds f in S1 iff ex g be Function st f = ( product g) & g in ( product (( Seg n) --> X)) and

         A13: for f be object holds f in S2 iff ex g be Function st f = ( product g) & g in ( product (( Seg n) --> X));

        now

          let x be object;

          x in S1 iff ex g be Function st x = ( product g) & g in ( product (( Seg n) --> X)) by A12;

          hence x in S1 iff x in S2 by A13;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    theorem :: SRINGS_5:45

    

     Th36: ( Product (n,X)) c= ( bool ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X))))))

    proof

      let x be object;

      assume x in ( Product (n,X));

      then

      consider g be Function such that

       A1: x = ( product g) and

       A2: g in ( product (( Seg n) --> X)) by Def2;

      

       A3: ( dom g) = ( dom (( Seg n) --> X)) by A2, CARD_3: 9;

      ( rng g) c= ( Union (( Seg n) --> X))

      proof

        let t be object;

        assume t in ( rng g);

        then

        consider u be object such that

         A4: u in ( dom g) and

         A5: t = (g . u) by FUNCT_1:def 3;

        consider h be Function such that

         A6: g = h and

         A7: ( dom h) = ( dom (( Seg n) --> X)) and

         A8: for v be object st v in ( dom (( Seg n) --> X)) holds (h . v) in ((( Seg n) --> X) . v) by A2, CARD_3:def 5;

        t in ((( Seg n) --> X) . u) & ((( Seg n) --> X) . u) in ( rng (( Seg n) --> X)) by A6, A7, A8, A4, A5, FUNCT_1:def 3;

        hence thesis by TARSKI:def 4;

      end;

      then ( Union g) c= ( union ( Union (( Seg n) --> X))) by ZFMISC_1: 77;

      then ( Funcs (( dom g),( Union g))) c= ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X))))) by A3, FUNCT_5: 56;

      then

       A9: ( bool ( Funcs (( dom g),( Union g)))) c= ( bool ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X)))))) by ZFMISC_1: 67;

      ( product g) c= ( Funcs (( dom g),( Union g))) by FUNCT_6: 1;

      hence thesis by A1, A9;

    end;

    theorem :: SRINGS_5:46

    

     Th37: ( Product (n,S)) is Subset-Family of ( product (( Seg n) --> X))

    proof

      reconsider SPS = ( Product (n,S)) as Subset of ( bool ( Funcs (( dom (( Seg n) --> S)),( union ( Union (( Seg n) --> S)))))) by Th36;

      SPS c= ( bool ( product (( Seg n) --> X)))

      proof

        let x be object;

        assume

         A1: x in SPS;

        reconsider x1 = x as set by TARSKI: 1;

        x1 c= ( product (( Seg n) --> X))

        proof

          let t be object;

          assume

           A2: t in x1;

          consider g be Function such that

           A3: x1 = ( product g) and

           A4: g in ( product (( Seg n) --> S)) by A1, Def2;

          

           A5: ( dom g) = ( dom (( Seg n) --> S)) by A4, CARD_3: 9;

          consider u be Function such that

           A7: t = u and

           A8: ( dom u) = ( dom g) and

           A9: for v be object st v in ( dom g) holds (u . v) in (g . v) by A2, A3, CARD_3:def 5;

          consider w be Function such that

           A10: g = w and ( dom w) = ( dom (( Seg n) --> S)) and

           A12: for y be object st y in ( dom (( Seg n) --> S)) holds (w . y) in ((( Seg n) --> S) . y) by A4, CARD_3:def 5;

          

           A13: ( dom (( Seg n) --> S)) = ( Seg n) & ( dom (( Seg n) --> X)) = ( Seg n) by FUNCOP_1: 13;

          now

            let a be object;

            assume

             A14: a in ( dom (( Seg n) --> X));

            then

            reconsider a1 = a as Nat;

            (u . a) in (g . a) & (g . a) in ((( Seg n) --> S) . a) by A14, A13, A10, A12, A9, A5;

            then

             A15: (u . a) in ( union ((( Seg n) --> S) . a)) & a in ( Seg n) by A14, TARSKI:def 4;

            ( union ((( Seg n) --> S) . a)) c= ((( Seg n) --> X) . a)

            proof

              

               A16: ((( Seg n) --> S) . a) = S & ((( Seg n) --> X) . a) = X by A14, FUNCOP_1: 7;

              ( union S) c= ( union ( bool X)) by ZFMISC_1: 77;

              hence thesis by A16, ZFMISC_1: 81;

            end;

            hence (u . a) in ((( Seg n) --> X) . a) by A15;

          end;

          hence t in ( product (( Seg n) --> X)) by A13, A5, A8, A7, CARD_3:def 5;

        end;

        hence x in ( bool ( product (( Seg n) --> X)));

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:47

    

     Th38: for S be non empty Subset-Family of X holds ( Product (n,S)) = the set of all ( product f) where f be Tuple of n, S

    proof

      let S be non empty Subset-Family of X;

      thus ( Product (n,S)) c= the set of all ( product f) where f be Tuple of n, S

      proof

        let x be object;

        assume x in ( Product (n,S));

        then

        consider g be Function such that

         A1: x = ( product g) and

         A2: g in ( product (( Seg n) --> S)) by Def2;

        g in (n -tuples_on S) by A2, Th8;

        then g is Tuple of n, S by FINSEQ_2: 131;

        hence x in the set of all ( product f) where f be Tuple of n, S by A1;

      end;

      thus the set of all ( product f) where f be Tuple of n, S c= ( Product (n,S))

      proof

        let x be object;

        assume x in the set of all ( product f) where f be Tuple of n, S;

        then

        consider f be Tuple of n, S such that

         A3: x = ( product f);

        f in (n -tuples_on S) by FINSEQ_2: 131;

        then f in ( product (( Seg n) --> S)) by Th8;

        hence thesis by A3, Def2;

      end;

    end;

    theorem :: SRINGS_5:48

    

     Th39: for n be non zero Nat holds ( Product (n,X)) c= ( bool ( Funcs (( Seg n),( union X))))

    proof

      let n be non zero Nat;

      let x be object;

      assume x in ( Product (n,X));

      then

      consider g be Function such that

       A1: x = ( product g) and

       A2: g in ( product (( Seg n) --> X)) by Def2;

      

       A3: ( dom g) = ( dom (( Seg n) --> X)) by A2, CARD_3: 9;

      ( rng g) c= ( Union (( Seg n) --> X))

      proof

        let t be object;

        assume t in ( rng g);

        then

        consider u be object such that

         A4: u in ( dom g) and

         A5: t = (g . u) by FUNCT_1:def 3;

        consider h be Function such that

         A6: g = h and

         A7: ( dom h) = ( dom (( Seg n) --> X)) and

         A8: for v be object st v in ( dom (( Seg n) --> X)) holds (h . v) in ((( Seg n) --> X) . v) by A2, CARD_3:def 5;

        t in ((( Seg n) --> X) . u) & ((( Seg n) --> X) . u) in ( rng (( Seg n) --> X)) by A6, A7, A8, A4, A5, FUNCT_1:def 3;

        hence thesis by TARSKI:def 4;

      end;

      then ( Union g) c= ( union ( Union (( Seg n) --> X))) by ZFMISC_1: 77;

      then ( Funcs (( dom g),( Union g))) c= ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X))))) by A3, FUNCT_5: 56;

      then ( bool ( Funcs (( dom g),( Union g)))) c= ( bool ( Funcs (( dom (( Seg n) --> X)),( union ( Union (( Seg n) --> X)))))) by ZFMISC_1: 67;

      then ( bool ( Funcs (( dom g),( Union g)))) c= ( bool ( Funcs (( Seg n),( union ( Union (( Seg n) --> X)))))) by FUNCOP_1: 13;

      then

       A11: ( bool ( Funcs (( dom g),( Union g)))) c= ( bool ( Funcs (( Seg n),( union X)))) by CARD_3: 7;

      ( product g) c= ( Funcs (( dom g),( Union g))) by FUNCT_6: 1;

      hence thesis by A1, A11;

    end;

    theorem :: SRINGS_5:49

    

     Th40: for n be non zero Nat, X be non empty set, S be non empty Subset-Family of X st S <> { {} } holds ( Product (n,S)) c= ( bool ( Funcs (( Seg n),X)))

    proof

      let n be non zero Nat, X be non empty set, S be non empty Subset-Family of X;

      assume

       A1: S <> { {} };

      

       A2: ( Product (n,S)) c= ( bool ( Funcs (( Seg n),( union S)))) by Th39;

      ( union S) c= ( union ( bool X)) by ZFMISC_1: 77;

      then

       A3: ( union S) is non empty Subset of X by A1, ZFMISC_1: 81, SCMYCIEL: 18;

      (n -tuples_on X) = ( Funcs (( Seg n),X)) & (n -tuples_on ( union S)) = ( Funcs (( Seg n),( union S))) by FINSEQ_2: 93;

      then ( bool ( Funcs (( Seg n),( union S)))) c= ( bool ( Funcs (( Seg n),X))) by A3, Th5, ZFMISC_1: 67;

      hence thesis by A2;

    end;

    theorem :: SRINGS_5:50

    for n be non zero Nat, X be non empty set, S be non empty Subset-Family of X st S <> { {} } holds ( union ( Product (n,S))) c= ( Funcs (( Seg n),X))

    proof

      let n be non zero Nat, X be non empty set, S be non empty Subset-Family of X;

      assume S <> { {} };

      then ( union ( Product (n,S))) c= ( union ( bool ( Funcs (( Seg n),X)))) by ZFMISC_1: 77, Th40;

      hence thesis by ZFMISC_1: 81;

    end;

    registration

      let n be Nat, X be non empty set;

      cluster ( Product (n,X)) -> non empty;

      coherence

      proof

        X is non empty;

        then

        consider x0 be object such that

         A1: x0 in X;

        reconsider x0 as Element of X by A1;

        

         A2: ( product (( Seg n) --> X)) = (n -tuples_on X) by Th8;

        set f = ( product (n |-> x0));

        f in ( Product (n,X)) by A2, Def2;

        hence thesis;

      end;

    end

    

     Lm1: for X be non empty set, S be non empty Subset-Family of X, x be Element of ( Product (n,S)) holds ex s be Tuple of n, S st for t be Element of ( Funcs (( Seg n),X)) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x

    proof

      let X be non empty set, S be non empty Subset-Family of X, x be Element of ( Product (n,S));

      consider g be Function such that

       A1: x = ( product g) and

       A2: g in ( product (( Seg n) --> S)) by Def2;

      g in (n -tuples_on S) by A2, Th8;

      then

      reconsider g as Tuple of n, S by FINSEQ_2: 131;

      take g;

      for t be Element of ( Funcs (( Seg n),X)) holds (for i be Nat st i in ( Seg n) holds (t . i) in (g . i)) iff t in x

      proof

        let t be Element of ( Funcs (( Seg n),X));

        hereby

          assume

           A3: for i be Nat st i in ( Seg n) holds (t . i) in (g . i);

          t in ( Funcs (( Seg n),X));

          then t in (n -tuples_on X) by FINSEQ_2: 93;

          then ( dom t) = ( Seg n) by FINSEQ_1: 89;

          then

           A4: ( dom t) = ( dom g) by FINSEQ_2: 124;

          for i be object st i in ( dom g) holds (t . i) in (g . i)

          proof

            let i be object;

            assume i in ( dom g);

            then i in ( Seg n) by FINSEQ_2: 124;

            hence (t . i) in (g . i) by A3;

          end;

          hence t in x by A1, A4, CARD_3:def 5;

        end;

        assume

         A5: t in x;

        hereby

          let i be Nat;

          assume

           A6: i in ( Seg n);

          consider h be Function such that

           A7: t = h and ( dom h) = ( dom g) and

           A8: for u be object st u in ( dom g) holds (h . u) in (g . u) by A5, A1, CARD_3:def 5;

          i in ( dom g) by A6, FINSEQ_2: 124;

          hence (t . i) in (g . i) by A8, A7;

        end;

      end;

      hence thesis;

    end;

    

     Lm2: for X be non empty set, S be non empty Subset-Family of X, x be Subset of ( Funcs (( Seg n),X)), s be Tuple of n, S st for t be Element of ( Funcs (( Seg n),X)) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) holds x is Element of ( Product (n,S))

    proof

      let X be non empty set, S be non empty Subset-Family of X, x be Subset of ( Funcs (( Seg n),X)), s be Tuple of n, S;

      assume

       A1: for t be Element of ( Funcs (( Seg n),X)) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in (s . i));

      x = ( product s)

      proof

        for u be object holds u in x iff ex g be Function st u = g & ( dom g) = ( dom s) & for v be object st v in ( dom s) holds (g . v) in (s . v)

        proof

          let u be object;

          hereby

            assume

             A2: u in x;

            then

             A3: u in ( Funcs (( Seg n),X));

            reconsider u1 = u as Function by A2;

            now

              u1 in (n -tuples_on X) by A3, FINSEQ_2: 93;

              then ( dom u1) = ( Seg n) by FINSEQ_1: 89;

              hence ( dom u1) = ( dom s) by FINSEQ_2: 124;

              hereby

                let v be object;

                assume v in ( dom s);

                then v in ( Seg n) by FINSEQ_2: 124;

                hence (u1 . v) in (s . v) by A1, A2;

              end;

            end;

            hence ex g be Function st u = g & ( dom g) = ( dom s) & for v be object st v in ( dom s) holds (g . v) in (s . v);

          end;

          given g be Function such that

           A5: u = g and

           A6: ( dom g) = ( dom s) and

           A7: for v be object st v in ( dom s) holds (g . v) in (s . v);

          now

            thus ( dom g) = ( Seg n) by A6, FINSEQ_2: 124;

            thus ( rng g) c= X

            proof

              let t be object;

              assume t in ( rng g);

              then

              consider a be object such that

               A8: a in ( dom g) and

               A9: t = (g . a) by FUNCT_1:def 3;

              (g . a) in (s . a) & (s . a) in ( rng s) & ( rng s) c= S by A6, A8, A7, FUNCT_1: 3;

              then (g . a) in (s . a) & (s . a) in S & ( union S) c= ( union ( bool X)) by ZFMISC_1: 77;

              hence thesis by A9;

            end;

          end;

          then

           A10: g is Element of ( Funcs (( Seg n),X)) by FUNCT_2:def 2;

          for i be Nat st i in ( Seg n) holds (g . i) in (s . i)

          proof

            let i be Nat;

            assume i in ( Seg n);

            then i in ( dom s) by FINSEQ_2: 124;

            hence (g . i) in (s . i) by A7;

          end;

          hence u in x by A1, A5, A10;

        end;

        hence thesis by CARD_3:def 5;

      end;

      then x in the set of all ( product f) where f be Tuple of n, S;

      hence thesis by Th38;

    end;

    theorem :: SRINGS_5:51

    for X be non empty set, S be non empty Subset-Family of X, x be Subset of ( Funcs (( Seg n),X)) holds x is Element of ( Product (n,S)) iff (ex s be Tuple of n, S st for t be Element of ( Funcs (( Seg n),X)) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x) by Lm1, Lm2;

    begin

    definition

      :: SRINGS_5:def12

      func the_set_of_all_closed_real_bounded_intervals -> Subset-Family of REAL equals the set of all [.a, b.] where a,b be Real;

      coherence

      proof

         the set of all [.a, b.] where a,b be Real c= ( bool REAL )

        proof

          let x be object;

          assume x in the set of all [.a, b.] where a,b be Real;

          then ex a0,b0 be Real st x = [.a0, b0.];

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:52

     the_set_of_all_closed_real_bounded_intervals = { I where I be Subset of REAL : I is closed_interval }

    proof

      

       A1: the_set_of_all_closed_real_bounded_intervals c= { I where I be Subset of REAL : I is closed_interval }

      proof

        let x be object;

        assume x in the_set_of_all_closed_real_bounded_intervals ;

        then

        consider a,b be Real such that

         A2: x = [.a, b.];

        reconsider x1 = x as Subset of REAL by A2;

        x1 is closed_interval by A2, MEASURE5:def 3;

        hence thesis;

      end;

      { I where I be Subset of REAL : I is closed_interval } c= the_set_of_all_closed_real_bounded_intervals

      proof

        let x be object;

        assume x in { I where I be Subset of REAL : I is closed_interval };

        then

        consider I0 be Subset of REAL such that

         A3: x = I0 and

         A4: I0 is closed_interval;

        consider a,b be Real such that

         A5: I0 = [.a, b.] by A4, MEASURE5:def 3;

        thus thesis by A3, A5;

      end;

      hence thesis by A1;

    end;

    registration

      cluster the_set_of_all_closed_real_bounded_intervals -> non empty;

      coherence

      proof

         [. 0 , 0 .] in the_set_of_all_closed_real_bounded_intervals ;

        hence thesis;

      end;

    end

    registration

      cluster the_set_of_all_closed_real_bounded_intervals -> cap-closed with_empty_element with_countable_Cover;

      coherence

      proof

        thus the_set_of_all_closed_real_bounded_intervals is cap-closed

        proof

          now

            let x,y be set;

            assume that

             A1: x in the_set_of_all_closed_real_bounded_intervals and

             A2: y in the_set_of_all_closed_real_bounded_intervals ;

            consider a1,b1 be Real such that

             A3: x = [.a1, b1.] by A1;

            consider a2,b2 be Real such that

             A4: y = [.a2, b2.] by A2;

            ( [.a1, b1.] /\ [.a2, b2.]) = [.( max (a1,a2)), ( min (b1,b2)).] by XXREAL_1: 140;

            hence (x /\ y) in the_set_of_all_closed_real_bounded_intervals by A3, A4;

          end;

          hence thesis by FINSUB_1:def 2;

        end;

         [.1, 0 .] = {} by XXREAL_1: 29;

        then {} in the_set_of_all_closed_real_bounded_intervals ;

        hence the_set_of_all_closed_real_bounded_intervals is with_empty_element;

        ex XX be countable Subset of the_set_of_all_closed_real_bounded_intervals st XX is Cover of REAL

        proof

          defpred F[ object, object] means $1 is Element of NAT & $2 in the_set_of_all_closed_real_bounded_intervals & ex x be real number st x = $1 & $2 = [.( - x), x.];

          

           A5: for x be object st x in NAT holds ex y be object st y in the_set_of_all_closed_real_bounded_intervals & F[x, y]

          proof

            let x be object;

            assume

             A6: x in NAT ;

            then

            reconsider x as real number;

            set y = [.( - x), x.];

            y in the_set_of_all_closed_real_bounded_intervals & F[x, y] by A6;

            hence thesis;

          end;

          consider f be Function such that

           A7: ( dom f) = NAT & ( rng f) c= the_set_of_all_closed_real_bounded_intervals and

           A8: for x be object st x in NAT holds F[x, (f . x)] from FUNCT_1:sch 6( A5);

          

           A9: ( rng f) is Subset-Family of REAL by A7, XBOOLE_1: 1;

          

           A10: ( rng f) is countable

          proof

            reconsider f as SetSequence of REAL by A7, A9, RELSET_1: 4, FUNCT_2:def 1;

            ( rng f) is countable by TOPGEN_4: 58;

            hence thesis;

          end;

          ( rng f) is Cover of REAL

          proof

            ( Union f) = REAL

            proof

              thus ( Union f) c= REAL

              proof

                let x be object;

                assume x in ( Union f);

                then

                consider t be object such that

                 A11: t in ( dom f) & x in (f . t) by CARD_5: 2;

                consider x0 be real number such that

                 A12: x0 = t & (f . t) = [.( - x0), x0.] by A7, A8, A11;

                thus thesis by A11, A12;

              end;

              for x be object st x in REAL holds x in ( Union f)

              proof

                let x be object;

                assume x in REAL ;

                then

                reconsider x as Real;

                consider n be Element of NAT such that

                 A13: |.x.| <= n by MESFUNC1: 8;

                consider z be real number such that

                 A14: z = n & (f . n) = [.( - z), z.] by A8;

                ( - n) <= x & x <= n by A13, ABSVALUE: 5;

                then x in (f . n) & (f . n) in ( rng f) by A14, XXREAL_1: 1, A7, FUNCT_1:def 3;

                hence thesis by TARSKI:def 4;

              end;

              hence thesis;

            end;

            hence thesis by A9, SETFAM_1: 45;

          end;

          hence thesis by A7, A10;

        end;

        hence the_set_of_all_closed_real_bounded_intervals is with_countable_Cover by SRINGS_1:def 4;

      end;

    end

    theorem :: SRINGS_5:53

    for n be Nat holds (( Seg n) --> the_set_of_all_closed_real_bounded_intervals ) is n -element FinSequence

    proof

      let n be Nat;

      reconsider f = (( Seg n) --> the_set_of_all_closed_real_bounded_intervals ) as FinSequence;

      ( dom f) is n -element by FUNCOP_1: 13;

      then ( card ( dom f)) = n by CARD_1:def 7;

      then ( card f) = n by CARD_1: 62;

      hence thesis by CARD_1:def 7;

    end;

    begin

    definition

      :: SRINGS_5:def13

      func the_set_of_all_open_real_bounded_intervals -> Subset-Family of REAL equals the set of all ].a, b.[ where a,b be Real;

      coherence

      proof

         the set of all ].a, b.[ where a,b be Real c= ( bool REAL )

        proof

          let x be object;

          assume x in the set of all ].a, b.[ where a,b be Real;

          then ex a0,b0 be Real st x = ].a0, b0.[;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:54

     the_set_of_all_open_real_bounded_intervals c= { I where I be Subset of REAL : I is open_interval }

    proof

      let x be object;

      assume x in the_set_of_all_open_real_bounded_intervals ;

      then

      consider a,b be Real such that

       A2: x = ].a, b.[;

      reconsider x1 = x as Subset of REAL by A2;

      a is Element of ExtREAL & b is Element of ExtREAL by NUMBERS: 31, XREAL_0:def 1;

      then x1 is open_interval by A2, MEASURE5:def 2;

      hence thesis;

    end;

    registration

      cluster the_set_of_all_open_real_bounded_intervals -> non empty;

      coherence

      proof

         ]. 0 , 0 .[ in the_set_of_all_open_real_bounded_intervals ;

        hence thesis;

      end;

    end

    registration

      cluster the_set_of_all_open_real_bounded_intervals -> cap-closed with_empty_element with_countable_Cover;

      coherence

      proof

        thus the_set_of_all_open_real_bounded_intervals is cap-closed

        proof

          now

            let x,y be set;

            assume that

             A1: x in the_set_of_all_open_real_bounded_intervals and

             A2: y in the_set_of_all_open_real_bounded_intervals ;

            consider a1,b1 be Real such that

             A3: x = ].a1, b1.[ by A1;

            consider a2,b2 be Real such that

             A4: y = ].a2, b2.[ by A2;

            ( ].a1, b1.[ /\ ].a2, b2.[) = ].( max (a1,a2)), ( min (b1,b2)).[ by XXREAL_1: 142;

            hence (x /\ y) in the_set_of_all_open_real_bounded_intervals by A3, A4;

          end;

          hence thesis by FINSUB_1:def 2;

        end;

         ].1, 0 .[ = {} by XXREAL_1: 28;

        then {} in the_set_of_all_open_real_bounded_intervals ;

        hence the_set_of_all_open_real_bounded_intervals is with_empty_element;

        ex XX be countable Subset of the_set_of_all_open_real_bounded_intervals st XX is Cover of REAL

        proof

          defpred F[ object, object] means $1 is Element of NAT & $2 in the_set_of_all_open_real_bounded_intervals & ex x be real number st x = $1 & $2 = ].( - x), x.[;

          

           A5: for x be object st x in NAT holds ex y be object st y in the_set_of_all_open_real_bounded_intervals & F[x, y]

          proof

            let x be object;

            assume

             A6: x in NAT ;

            then

            reconsider x as real number;

            set y = ].( - x), x.[;

            y in the_set_of_all_open_real_bounded_intervals & F[x, y] by A6;

            hence thesis;

          end;

          consider f be Function such that

           A7: ( dom f) = NAT & ( rng f) c= the_set_of_all_open_real_bounded_intervals and

           A8: for x be object st x in NAT holds F[x, (f . x)] from FUNCT_1:sch 6( A5);

          

           A9: ( rng f) is Subset-Family of REAL by A7, XBOOLE_1: 1;

          

           A10: ( rng f) is countable

          proof

            reconsider f as SetSequence of REAL by A7, A9, RELSET_1: 4, FUNCT_2:def 1;

            ( rng f) is countable by TOPGEN_4: 58;

            hence thesis;

          end;

          ( rng f) is Cover of REAL

          proof

            ( Union f) = REAL

            proof

              thus ( Union f) c= REAL

              proof

                let x be object;

                assume x in ( Union f);

                then

                consider t be object such that

                 A11: t in ( dom f) & x in (f . t) by CARD_5: 2;

                consider x0 be real number such that

                 A12: x0 = t & (f . t) = ].( - x0), x0.[ by A7, A8, A11;

                thus thesis by A11, A12;

              end;

              for x be object st x in REAL holds x in ( Union f)

              proof

                let x be object;

                assume x in REAL ;

                then

                reconsider x as Real;

                consider n be Element of NAT such that

                 A13: |.x.| <= n by MESFUNC1: 8;

                consider z be real number such that

                 A14: z = (n + 1) & (f . (n + 1)) = ].( - z), z.[ by A8;

                

                 A15: ( - n) <= x & x <= n by A13, ABSVALUE: 5;

                (( - n) - 1) < ( - n) by XREAL_1: 146;

                then ( - (n + 1)) < x & x < (n + 1) by A15, XXREAL_0: 2, XREAL_1: 145;

                then x in (f . (n + 1)) & (f . (n + 1)) in ( rng f) by A14, A7, FUNCT_1:def 3, XXREAL_1: 4;

                hence thesis by TARSKI:def 4;

              end;

              hence thesis;

            end;

            hence thesis by A9, SETFAM_1: 45;

          end;

          hence thesis by A7, A10;

        end;

        hence the_set_of_all_open_real_bounded_intervals is with_countable_Cover by SRINGS_1:def 4;

      end;

    end

    theorem :: SRINGS_5:55

    for n be Nat holds (( Seg n) --> the_set_of_all_open_real_bounded_intervals ) is n -element FinSequence

    proof

      let n be Nat;

      reconsider f = (( Seg n) --> the_set_of_all_open_real_bounded_intervals ) as FinSequence;

      ( dom f) is n -element by FUNCOP_1: 13;

      then ( card ( dom f)) = n by CARD_1:def 7;

      then ( card f) = n by CARD_1: 62;

      hence thesis by CARD_1:def 7;

    end;

    begin

    reserve n for Nat,

S for Subset-Family of REAL ;

    theorem :: SRINGS_5:56

    

     Th41: ( Product (n,S)) is Subset-Family of ( REAL n)

    proof

      ( Product (n,S)) is Subset-Family of ( product (( Seg n) --> REAL )) by Th37;

      hence thesis by Th7;

    end;

    definition

      let n, S;

      :: original: Product

      redefine

      func Product (n,S) -> Subset-Family of ( REAL n) ;

      coherence by Th41;

    end

    theorem :: SRINGS_5:57

    

     Th42: for S be non empty Subset-Family of REAL , x be Subset of ( REAL n) holds x is Element of ( Product (n,S)) iff ex s be Tuple of n, S st for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x

    proof

      let S be non empty Subset-Family of REAL , x be Subset of ( REAL n);

      

       A1: x is Subset of ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

      thus x is Element of ( Product (n,S)) implies (ex s be Tuple of n, S st (for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff (t in x)))

      proof

        assume x is Element of ( Product (n,S));

        then

        consider s be Tuple of n, S such that

         A2: (for t be Element of ( Funcs (( Seg n), REAL )) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff (t in x)) by Lm1;

        take s;

        for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff (t in x)

        proof

          let t be Element of ( REAL n);

          t is Element of ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

          hence thesis by A2;

        end;

        hence thesis;

      end;

      thus (ex s be Tuple of n, S st (for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff (t in x))) implies x is Element of ( Product (n,S))

      proof

        given s be Tuple of n, S such that

         A3: (for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x);

        ex s be Tuple of n, S st for t be Element of ( Funcs (( Seg n), REAL )) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff (t in x)

        proof

          take s;

          let t be Element of ( Funcs (( Seg n), REAL ));

          t is Element of ( REAL n) by FINSEQ_2: 93;

          hence (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff (t in x) by A3;

        end;

        hence thesis by A1, Lm2;

      end;

    end;

    theorem :: SRINGS_5:58

    

     Th43: for n be non zero Nat, s be Tuple of n, the_set_of_all_closed_real_bounded_intervals holds ex a,b be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).]

    proof

      let n be non zero Nat, s be Tuple of n, the_set_of_all_closed_real_bounded_intervals ;

      s in ( Funcs (( Seg n), the_set_of_all_closed_real_bounded_intervals )) by Th9;

      then

      consider f be Function such that

       A1: s = f and

       A2: ( dom f) = ( Seg n) and ( rng f) c= the_set_of_all_closed_real_bounded_intervals by FUNCT_2:def 2;

      defpred P[ object, object] means ex f be Element of [: REAL , REAL :] st f = $2 & (s . $1) = [.(f `1 ), (f `2 ).];

      

       A3: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (s . i) in ( rng s) by A1, A2, FUNCT_1: 3;

        then (s . i) in the set of all [.a, b.] where a,b be Real;

        then

        consider a,b be Real such that

         A4: (s . i) = [.a, b.];

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d = [a, b] as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        (s . i) = [.(d `1 ), (d `2 ).] by A4;

        hence thesis;

      end;

      consider f be FinSequence of [: REAL , REAL :] such that

       A5: ( len f) = n and

       A6: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A3);

      reconsider f as n -element FinSequence of [: REAL , REAL :] by A5, CARD_1:def 7;

      consider z be Element of [:( REAL n), ( REAL n):] such that

       A7: for i be Nat st i in ( Seg n) holds ((z `1 ) . i) = ((f /. i) `1 ) & ((z `2 ) . i) = ((f /. i) `2 ) by Th13;

      reconsider a = (z `1 ), b = (z `2 ) as Element of ( REAL n);

      take a, b;

      let i be Nat;

      assume i in ( Seg n);

      then (a . i) = ((f /. i) `1 ) & (b . i) = ((f /. i) `2 ) & P[i, (f /. i)] by A6, A7;

      hence (s . i) = [.(a . i), (b . i).];

    end;

    theorem :: SRINGS_5:59

    for n be non zero Nat, x be Element of ( Product (n, the_set_of_all_closed_real_bounded_intervals )) holds (ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).])))

    proof

      let n be non zero Nat, x be Element of ( Product (n, the_set_of_all_closed_real_bounded_intervals ));

      consider s be Tuple of n, the_set_of_all_closed_real_bounded_intervals such that

       A1: for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x by Th42;

      consider a,b be Element of ( REAL n) such that

       A2: for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).] by Th43;

      take a, b;

      let t be Element of ( REAL n);

      hereby

        assume

         A3: t in x;

        thus for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).]

        proof

          let i be Nat;

          assume

           A4: i in ( Seg n);

          then (s . i) = [.(a . i), (b . i).] by A2;

          hence (t . i) in [.(a . i), (b . i).] by A1, A3, A4;

        end;

      end;

      assume

       A5: for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).];

      for i be Nat st i in ( Seg n) holds (t . i) in (s . i)

      proof

        let i be Nat;

        assume

         A6: i in ( Seg n);

        then (s . i) = [.(a . i), (b . i).] by A2;

        hence (t . i) in (s . i) by A6, A5;

      end;

      hence t in x by A1;

    end;

    theorem :: SRINGS_5:60

    for n be non zero Nat, x be Subset of ( REAL n), a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).])) holds x is Element of ( Product (n, the_set_of_all_closed_real_bounded_intervals ))

    proof

      let n be non zero Nat, x be Subset of ( REAL n), a,b be Element of ( REAL n);

      assume

       A1: for t be Element of ( REAL n) holds (t in x) iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).]);

      defpred P[ object, object] means ex n be Nat st $1 = n & $2 = [.(a . n), (b . n).];

      

       A2: for i be Nat st i in ( Seg n) holds ex d be Element of the_set_of_all_closed_real_bounded_intervals st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        set d = [.(a . i), (b . i).];

        take d;

        d in the set of all [.a, b.] where a,b be Real;

        hence d is Element of the_set_of_all_closed_real_bounded_intervals ;

        thus P[i, d];

      end;

      ex g be FinSequence of the_set_of_all_closed_real_bounded_intervals st ( len g) = n & for i be Nat st i in ( Seg n) holds P[i, (g /. i)] from FINSEQ_4:sch 1( A2);

      then

      consider g be FinSequence of the_set_of_all_closed_real_bounded_intervals such that

       A3: ( len g) = n and

       A4: for i be Nat st i in ( Seg n) holds P[i, (g /. i)];

      

       A5: for i be Nat st i in ( Seg n) holds (g . i) = [.(a . i), (b . i).]

      proof

        let i be Nat;

        assume

         A6: i in ( Seg n);

        then P[i, (g /. i)] by A4;

        then

        consider m be object such that

         A7: m = i and

         A8: (g /. m) = [.(a . m), (b . m).];

        i in ( dom g) by A6, A3, FINSEQ_1:def 3;

        hence thesis by A7, A8, PARTFUN1:def 6;

      end;

      ex g be Function st x = ( product g) & g in ( product (( Seg n) --> the_set_of_all_closed_real_bounded_intervals ))

      proof

        take g;

        thus x = ( product g)

        proof

          for t be object holds t in x iff ex h be Function st t = h & ( dom h) = ( dom g) & for u be object st u in ( dom g) holds (h . u) in (g . u)

          proof

            let t be object;

            hereby

              assume

               A9: t in x;

              then

              reconsider t1 = t as Element of ( REAL n);

              

               A10: ( dom t1) = ( Seg n) by FINSEQ_1: 89;

              now

                thus ( dom t1) = ( dom g) by A10, A3, FINSEQ_1:def 3;

                thus for u be object st u in ( dom g) holds (t1 . u) in (g . u)

                proof

                  let u be object;

                  assume u in ( dom g);

                  then

                   A11: u in ( Seg n) by A3, FINSEQ_1:def 3;

                  then (t1 . u) in [.(a . u), (b . u).] by A9, A1;

                  hence (t1 . u) in (g . u) by A11, A5;

                end;

              end;

              hence ex h be Function st t = h & ( dom h) = ( dom g) & for u be object st u in ( dom g) holds (h . u) in (g . u);

            end;

            hereby

              given h be Function such that

               A12: t = h and

               A13: ( dom h) = ( dom g) and

               A14: for u be object st u in ( dom g) holds (h . u) in (g . u);

              

               A15: for i be Nat st i in ( Seg n) holds (h . i) in [.(a . i), (b . i).]

              proof

                let i be Nat;

                assume

                 A16: i in ( Seg n);

                then i in ( dom g) by A3, FINSEQ_1:def 3;

                then (h . i) in (g . i) by A14;

                hence (h . i) in [.(a . i), (b . i).] by A16, A5;

              end;

              ( dom h) = ( dom (( Seg n) --> REAL )) & for u be object st u in ( dom (( Seg n) --> REAL )) holds (h . u) in ((( Seg n) --> REAL ) . u)

              proof

                ( dom h) = ( Seg n) by A13, A3, FINSEQ_1:def 3;

                hence ( dom h) = ( dom (( Seg n) --> REAL )) by FUNCOP_1: 13;

                hereby

                  let u be object;

                  assume

                   A17: u in ( dom (( Seg n) --> REAL ));

                  then

                   A18: u in ( Seg n);

                  (h . u) in [.(a . u), (b . u).] & [.(a . u), (b . u).] c= REAL by A17, A15;

                  then (h . u) in REAL & u in ( dom g) by A18, A3, FINSEQ_1:def 3;

                  hence (h . u) in ((( Seg n) --> REAL ) . u) by FUNCOP_1: 7, A17;

                end;

              end;

              then h in ( product (( Seg n) --> REAL )) by CARD_3: 9;

              then

              reconsider h as Element of ( REAL n) by Th7;

              h in x by A15, A1;

              hence t in x by A12;

            end;

          end;

          hence thesis by CARD_3:def 5;

        end;

        thus g in ( product (( Seg n) --> the_set_of_all_closed_real_bounded_intervals ))

        proof

          

           A19: ( dom g) = ( Seg n) & ( dom (( Seg n) --> the_set_of_all_closed_real_bounded_intervals )) = ( Seg n) by A3, FINSEQ_1:def 3, FUNCOP_1: 13;

          for x be object st x in ( dom (( Seg n) --> the_set_of_all_closed_real_bounded_intervals )) holds (g . x) in ((( Seg n) --> the_set_of_all_closed_real_bounded_intervals ) . x)

          proof

            let x be object;

            assume

             A20: x in ( dom (( Seg n) --> the_set_of_all_closed_real_bounded_intervals ));

            then (g . x) = [.(a . x), (b . x).] by A5;

            then (g . x) in the_set_of_all_closed_real_bounded_intervals & ((( Seg n) --> the_set_of_all_closed_real_bounded_intervals ) . x) = the_set_of_all_closed_real_bounded_intervals by A20, FUNCOP_1: 7;

            hence thesis;

          end;

          hence thesis by A19, CARD_3: 9;

        end;

      end;

      hence thesis by Def2;

    end;

    theorem :: SRINGS_5:61

    

     Th44: for n be non zero Nat, x be Subset of ( REAL n), a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])) holds x is Element of ( Product (n, the_set_of_all_left_open_real_bounded_intervals ))

    proof

      let n be non zero Nat, x be Subset of ( REAL n), a,b be Element of ( REAL n);

      assume

       A1: for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).]);

      defpred P[ object, object] means ex n be Nat st $1 = n & $2 = ].(a . n), (b . n).];

      

       A2: for i be Nat st i in ( Seg n) holds ex d be Element of the_set_of_all_left_open_real_bounded_intervals st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        set d = ].(a . i), (b . i).];

        take d;

        d in the set of all ].a, b.] where a,b be Real;

        hence d is Element of the_set_of_all_left_open_real_bounded_intervals ;

        thus P[i, d];

      end;

      ex g be FinSequence of the_set_of_all_left_open_real_bounded_intervals st ( len g) = n & for i be Nat st i in ( Seg n) holds P[i, (g /. i)] from FINSEQ_4:sch 1( A2);

      then

      consider g be FinSequence of the_set_of_all_left_open_real_bounded_intervals such that

       A3: ( len g) = n and

       A4: for i be Nat st i in ( Seg n) holds P[i, (g /. i)];

      

       A5: for i be Nat st i in ( Seg n) holds (g . i) = ].(a . i), (b . i).]

      proof

        let i be Nat;

        assume

         A6: i in ( Seg n);

        then P[i, (g /. i)] by A4;

        then

        consider m be object such that

         A7: m = i and

         A8: (g /. m) = ].(a . m), (b . m).];

        i in ( dom g) by A6, A3, FINSEQ_1:def 3;

        hence thesis by A7, A8, PARTFUN1:def 6;

      end;

      ex g be Function st x = ( product g) & g in ( product (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals ))

      proof

        take g;

        thus x = ( product g)

        proof

          for t be object holds t in x iff ex h be Function st t = h & ( dom h) = ( dom g) & for u be object st u in ( dom g) holds (h . u) in (g . u)

          proof

            let t be object;

            hereby

              assume

               A9: t in x;

              then

              reconsider t1 = t as Element of ( REAL n);

              

               A10: ( dom t1) = ( Seg n) by FINSEQ_1: 89;

              now

                thus ( dom t1) = ( dom g) by A10, A3, FINSEQ_1:def 3;

                thus for u be object st u in ( dom g) holds (t1 . u) in (g . u)

                proof

                  let u be object;

                  assume u in ( dom g);

                  then

                   A11: u in ( Seg n) by A3, FINSEQ_1:def 3;

                  then (t1 . u) in ].(a . u), (b . u).] by A9, A1;

                  hence (t1 . u) in (g . u) by A11, A5;

                end;

              end;

              hence ex h be Function st t = h & ( dom h) = ( dom g) & for u be object st u in ( dom g) holds (h . u) in (g . u);

            end;

            hereby

              given h be Function such that

               A12: t = h and

               A13: ( dom h) = ( dom g) and

               A14: for u be object st u in ( dom g) holds (h . u) in (g . u);

              

               A15: for i be Nat st i in ( Seg n) holds (h . i) in ].(a . i), (b . i).]

              proof

                let i be Nat;

                assume

                 A16: i in ( Seg n);

                then i in ( dom g) by A3, FINSEQ_1:def 3;

                then (h . i) in (g . i) by A14;

                hence (h . i) in ].(a . i), (b . i).] by A16, A5;

              end;

              ( dom h) = ( dom (( Seg n) --> REAL )) & for u be object st u in ( dom (( Seg n) --> REAL )) holds (h . u) in ((( Seg n) --> REAL ) . u)

              proof

                ( dom h) = ( Seg n) by A13, A3, FINSEQ_1:def 3;

                hence ( dom h) = ( dom (( Seg n) --> REAL )) by FUNCOP_1: 13;

                hereby

                  let u be object;

                  assume

                   A17: u in ( dom (( Seg n) --> REAL ));

                  then

                   A18: u in ( Seg n);

                  (h . u) in ].(a . u), (b . u).] & ].(a . u), (b . u).] c= REAL by A17, A15;

                  then (h . u) in REAL & u in ( dom g) by A18, A3, FINSEQ_1:def 3;

                  hence (h . u) in ((( Seg n) --> REAL ) . u) by FUNCOP_1: 7, A17;

                end;

              end;

              then h in ( product (( Seg n) --> REAL )) by CARD_3: 9;

              then

              reconsider h as Element of ( REAL n) by Th7;

              h in x by A15, A1;

              hence t in x by A12;

            end;

          end;

          hence thesis by CARD_3:def 5;

        end;

        thus g in ( product (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals ))

        proof

          

           A19: ( dom g) = ( Seg n) & ( dom (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals )) = ( Seg n) by A3, FINSEQ_1:def 3, FUNCOP_1: 13;

          for x be object st x in ( dom (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals )) holds (g . x) in ((( Seg n) --> the_set_of_all_left_open_real_bounded_intervals ) . x)

          proof

            let x be object;

            assume

             A20: x in ( dom (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals ));

            then (g . x) = ].(a . x), (b . x).] by A5;

            then (g . x) in the_set_of_all_left_open_real_bounded_intervals & ((( Seg n) --> the_set_of_all_left_open_real_bounded_intervals ) . x) = the_set_of_all_left_open_real_bounded_intervals by A20, FUNCOP_1: 7;

            hence thesis;

          end;

          hence thesis by A19, CARD_3: 9;

        end;

      end;

      hence thesis by Def2;

    end;

    theorem :: SRINGS_5:62

    

     Th45: for n be non zero Nat, x be Subset of ( REAL n), a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)) holds x is Element of ( Product (n, the_set_of_all_right_open_real_bounded_intervals ))

    proof

      let n be non zero Nat, x be Subset of ( REAL n), a,b be Element of ( REAL n);

      assume

       A1: for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[);

      defpred P[ object, object] means ex n be Nat st $1 = n & $2 = [.(a . n), (b . n).[;

      

       A2: for i be Nat st i in ( Seg n) holds ex d be Element of the_set_of_all_right_open_real_bounded_intervals st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        set d = [.(a . i), (b . i).[;

        take d;

        d in the set of all [.a, b.[ where a,b be Real;

        hence d is Element of the_set_of_all_right_open_real_bounded_intervals ;

        thus P[i, d];

      end;

      ex g be FinSequence of the_set_of_all_right_open_real_bounded_intervals st ( len g) = n & for i be Nat st i in ( Seg n) holds P[i, (g /. i)] from FINSEQ_4:sch 1( A2);

      then

      consider g be FinSequence of the_set_of_all_right_open_real_bounded_intervals such that

       A3: ( len g) = n and

       A4: for i be Nat st i in ( Seg n) holds P[i, (g /. i)];

      

       A5: for i be Nat st i in ( Seg n) holds (g . i) = [.(a . i), (b . i).[

      proof

        let i be Nat;

        assume

         A6: i in ( Seg n);

        then P[i, (g /. i)] by A4;

        then

        consider m be object such that

         A7: m = i and

         A8: (g /. m) = [.(a . m), (b . m).[;

        i in ( dom g) by A6, A3, FINSEQ_1:def 3;

        hence thesis by A7, A8, PARTFUN1:def 6;

      end;

      ex g be Function st x = ( product g) & g in ( product (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals ))

      proof

        take g;

        thus x = ( product g)

        proof

          for t be object holds t in x iff ex h be Function st t = h & ( dom h) = ( dom g) & for u be object st u in ( dom g) holds (h . u) in (g . u)

          proof

            let t be object;

            hereby

              assume

               A9: t in x;

              then

              reconsider t1 = t as Element of ( REAL n);

              

               A10: ( dom t1) = ( Seg n) by FINSEQ_1: 89;

              now

                thus ( dom t1) = ( dom g) by A10, A3, FINSEQ_1:def 3;

                thus for u be object st u in ( dom g) holds (t1 . u) in (g . u)

                proof

                  let u be object;

                  assume u in ( dom g);

                  then

                   A11: u in ( Seg n) by A3, FINSEQ_1:def 3;

                  then (t1 . u) in [.(a . u), (b . u).[ by A9, A1;

                  hence (t1 . u) in (g . u) by A11, A5;

                end;

              end;

              hence ex h be Function st t = h & ( dom h) = ( dom g) & for u be object st u in ( dom g) holds (h . u) in (g . u);

            end;

            hereby

              given h be Function such that

               A12: t = h and

               A13: ( dom h) = ( dom g) and

               A14: for u be object st u in ( dom g) holds (h . u) in (g . u);

              

               A15: for i be Nat st i in ( Seg n) holds (h . i) in [.(a . i), (b . i).[

              proof

                let i be Nat;

                assume

                 A16: i in ( Seg n);

                then i in ( dom g) by A3, FINSEQ_1:def 3;

                then (h . i) in (g . i) by A14;

                hence (h . i) in [.(a . i), (b . i).[ by A16, A5;

              end;

              ( dom h) = ( dom (( Seg n) --> REAL )) & for u be object st u in ( dom (( Seg n) --> REAL )) holds (h . u) in ((( Seg n) --> REAL ) . u)

              proof

                ( dom h) = ( Seg n) by A13, A3, FINSEQ_1:def 3;

                hence ( dom h) = ( dom (( Seg n) --> REAL )) by FUNCOP_1: 13;

                hereby

                  let u be object;

                  assume

                   A17: u in ( dom (( Seg n) --> REAL ));

                  then

                   A18: u in ( Seg n);

                  (h . u) in [.(a . u), (b . u).[ & [.(a . u), (b . u).[ c= REAL by A17, A15;

                  then (h . u) in REAL & u in ( dom g) by A18, A3, FINSEQ_1:def 3;

                  hence (h . u) in ((( Seg n) --> REAL ) . u) by FUNCOP_1: 7, A17;

                end;

              end;

              then h in ( product (( Seg n) --> REAL )) by CARD_3: 9;

              then

              reconsider h as Element of ( REAL n) by Th7;

              h in x by A15, A1;

              hence t in x by A12;

            end;

          end;

          hence thesis by CARD_3:def 5;

        end;

        thus g in ( product (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals ))

        proof

          

           A19: ( dom g) = ( Seg n) & ( dom (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals )) = ( Seg n) by A3, FINSEQ_1:def 3, FUNCOP_1: 13;

          for x be object st x in ( dom (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals )) holds (g . x) in ((( Seg n) --> the_set_of_all_right_open_real_bounded_intervals ) . x)

          proof

            let x be object;

            assume

             A20: x in ( dom (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals ));

            then (g . x) = [.(a . x), (b . x).[ by A5;

            then (g . x) in the_set_of_all_right_open_real_bounded_intervals & ((( Seg n) --> the_set_of_all_right_open_real_bounded_intervals ) . x) = the_set_of_all_right_open_real_bounded_intervals by A20, FUNCOP_1: 7;

            hence thesis;

          end;

          hence thesis by A19, CARD_3: 9;

        end;

      end;

      hence thesis by Def2;

    end;

    theorem :: SRINGS_5:63

    

     Th46: for n be non zero Nat, s be Tuple of n, the_set_of_all_left_open_real_bounded_intervals holds ex a,b be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).]

    proof

      let n be non zero Nat, s be Tuple of n, the_set_of_all_left_open_real_bounded_intervals ;

      s in ( Funcs (( Seg n), the_set_of_all_left_open_real_bounded_intervals )) by Th9;

      then

      consider f be Function such that

       A1: s = f and

       A2: ( dom f) = ( Seg n) and ( rng f) c= the_set_of_all_left_open_real_bounded_intervals by FUNCT_2:def 2;

      defpred P[ object, object] means ex f be Element of [: REAL , REAL :] st f = $2 & (s . $1) = ].(f `1 ), (f `2 ).];

      

       A3: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (s . i) in ( rng s) by A1, A2, FUNCT_1: 3;

        then (s . i) in the set of all ].a, b.] where a,b be Real;

        then

        consider a,b be Real such that

         A4: (s . i) = ].a, b.];

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d = [a, b] as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        (s . i) = ].(d `1 ), (d `2 ).] by A4;

        hence thesis;

      end;

      consider f be FinSequence of [: REAL , REAL :] such that

       A5: ( len f) = n and

       A6: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A3);

      reconsider f as n -element FinSequence of [: REAL , REAL :] by A5, CARD_1:def 7;

      consider z be Element of [:( REAL n), ( REAL n):] such that

       A7: for i be Nat st i in ( Seg n) holds ((z `1 ) . i) = ((f /. i) `1 ) & ((z `2 ) . i) = ((f /. i) `2 ) by Th13;

      reconsider a = (z `1 ), b = (z `2 ) as Element of ( REAL n);

      take a, b;

      let i be Nat;

      assume i in ( Seg n);

      then (a . i) = ((f /. i) `1 ) & (b . i) = ((f /. i) `2 ) & P[i, (f /. i)] by A6, A7;

      hence (s . i) = ].(a . i), (b . i).];

    end;

    theorem :: SRINGS_5:64

    for n be non zero Nat, x be Element of ( Product (n, the_set_of_all_left_open_real_bounded_intervals )) holds (ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])))

    proof

      let n be non zero Nat, x be Element of ( Product (n, the_set_of_all_left_open_real_bounded_intervals ));

      consider s be Tuple of n, the_set_of_all_left_open_real_bounded_intervals such that

       A1: for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x by Th42;

      consider a,b be Element of ( REAL n) such that

       A2: for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).] by Th46;

      take a, b;

      for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])

      proof

        let t be Element of ( REAL n);

        hereby

          assume

           A3: t in x;

          thus (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])

          proof

            let i be Nat;

            assume

             A4: i in ( Seg n);

            then (s . i) = ].(a . i), (b . i).] by A2;

            hence (t . i) in ].(a . i), (b . i).] by A1, A3, A4;

          end;

        end;

        assume

         A5: for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).];

        for i be Nat st i in ( Seg n) holds (t . i) in (s . i)

        proof

          let i be Nat;

          assume

           A6: i in ( Seg n);

          then (s . i) = ].(a . i), (b . i).] by A2;

          hence (t . i) in (s . i) by A6, A5;

        end;

        hence t in x by A1;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:65

    

     Th47: for n be non zero Nat, s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals holds ex a,b be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).[

    proof

      let n be non zero Nat, s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals ;

      s in ( Funcs (( Seg n), the_set_of_all_right_open_real_bounded_intervals )) by Th9;

      then

      consider f be Function such that

       A1: s = f and

       A2: ( dom f) = ( Seg n) and ( rng f) c= the_set_of_all_right_open_real_bounded_intervals by FUNCT_2:def 2;

      defpred P[ object, object] means ex f be Element of [: REAL , REAL :] st f = $2 & (s . $1) = [.(f `1 ), (f `2 ).[;

      

       A3: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (s . i) in ( rng s) by A1, A2, FUNCT_1: 3;

        then (s . i) in the set of all [.a, b.[ where a,b be Real;

        then

        consider a,b be Real such that

         A4: (s . i) = [.a, b.[;

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d = [a, b] as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        (s . i) = [.(d `1 ), (d `2 ).[ by A4;

        hence thesis;

      end;

      consider f be FinSequence of [: REAL , REAL :] such that

       A5: ( len f) = n and

       A6: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A3);

      reconsider f as n -element FinSequence of [: REAL , REAL :] by A5, CARD_1:def 7;

      consider z be Element of [:( REAL n), ( REAL n):] such that

       A7: for i be Nat st i in ( Seg n) holds ((z `1 ) . i) = ((f /. i) `1 ) & ((z `2 ) . i) = ((f /. i) `2 ) by Th13;

      reconsider a = (z `1 ), b = (z `2 ) as Element of ( REAL n);

      take a, b;

      thus for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).[

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (a . i) = ((f /. i) `1 ) & (b . i) = ((f /. i) `2 ) & P[i, (f /. i)] by A6, A7;

        hence (s . i) = [.(a . i), (b . i).[;

      end;

    end;

    theorem :: SRINGS_5:66

    for n be non zero Nat, x be Element of ( Product (n, the_set_of_all_right_open_real_bounded_intervals )) holds (ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)))

    proof

      let n be non zero Nat, x be Element of ( Product (n, the_set_of_all_right_open_real_bounded_intervals ));

      consider s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals such that

       A1: for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x by Th42;

      consider a,b be Element of ( REAL n) such that

       A2: for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).[ by Th47;

      take a, b;

      for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)

      proof

        let t be Element of ( REAL n);

        hereby

          assume

           A3: t in x;

          thus for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[

          proof

            let i be Nat;

            assume

             A4: i in ( Seg n);

            then (s . i) = [.(a . i), (b . i).[ by A2;

            hence (t . i) in [.(a . i), (b . i).[ by A1, A3, A4;

          end;

        end;

        assume

         A5: (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[);

        for i be Nat st i in ( Seg n) holds (t . i) in (s . i)

        proof

          let i be Nat;

          assume

           A6: i in ( Seg n);

          then (s . i) = [.(a . i), (b . i).[ by A2;

          hence (t . i) in (s . i) by A6, A5;

        end;

        hence t in x by A1;

      end;

      hence thesis;

    end;

    begin

    reserve n for Nat,

a,b,c,d for Element of ( REAL n);

    definition

      let n, a, b;

      :: SRINGS_5:def14

      func ClosedHyperInterval (a,b) -> Subset of ( REAL n) means

      : Def3: for x be object holds x in it iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).]);

      existence

      proof

        defpred P[ object, object] means ex S be Subset of REAL st S = $2 & S = [.(a . $1), (b . $1).];

        

         A1: for i be Nat st i in ( Seg n) holds ex d be Element of ( bool REAL ) st P[i, d];

        consider f be FinSequence of ( bool REAL ) such that

         A2: ( len f) = n and

         A3: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A1);

        

         A4: ( dom f) = ( Seg n) by A2, FINSEQ_1:def 3;

        set s = ( product f);

        s c= ( product (( Seg n) --> REAL ))

        proof

          let t be object;

          assume

           A5: t in s;

          then

          reconsider t1 = t as Function;

          

           A6: ( dom t1) = ( dom f) & for y be object st y in ( dom f) holds (t1 . y) in (f . y) by A5, CARD_3: 9;

          now

            ( dom (( Seg n) --> REAL )) = ( Seg n) by FUNCOP_1: 13;

            hence ( dom t1) = ( dom (( Seg n) --> REAL )) by A6, A2, FINSEQ_1:def 3;

            thus for y be object st y in ( dom (( Seg n) --> REAL )) holds (t1 . y) in ((( Seg n) --> REAL ) . y)

            proof

              let y be object;

              assume

               A7: y in ( dom (( Seg n) --> REAL ));

              then y in ( Seg n);

              then y in ( dom f) by A2, FINSEQ_1:def 3;

              then (t1 . y) in (f . y) & (f . y) in ( bool REAL ) by A5, CARD_3: 9, FINSEQ_2: 11;

              then (t1 . y) in REAL ;

              hence thesis by A7, FUNCOP_1: 7;

            end;

          end;

          hence t in ( product (( Seg n) --> REAL )) by CARD_3: 9;

        end;

        then

        reconsider s as Subset of ( REAL n) by Th7;

        for x be object holds x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).])

        proof

          let x be object;

          thus x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).])

          proof

            hereby

              assume

               A8: x in s;

              then

              reconsider y = x as Element of ( REAL n);

              take y;

              thus x = y;

              thus for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).]

              proof

                let i be Nat;

                assume

                 A9: i in ( Seg n);

                then

                 A10: i in ( dom f) by A2, FINSEQ_1:def 3;

                then

                 A11: (y . i) in (f . i) by A8, CARD_3: 9;

                consider S2 be Subset of REAL such that

                 A12: (f /. i) = S2 and

                 A13: S2 = [.(a . i), (b . i).] by A9, A3;

                thus (y . i) in [.(a . i), (b . i).] by A10, A11, A12, A13, PARTFUN1:def 6;

              end;

            end;

            given y be Element of ( REAL n) such that

             A14: x = y and

             A15: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).];

            now

              thus ( dom y) = ( dom f) by A4, FINSEQ_1: 89;

              thus for z be object st z in ( dom f) holds (y . z) in (f . z)

              proof

                let z be object;

                assume

                 A16: z in ( dom f);

                then

                 A17: z in ( Seg n) by A2, FINSEQ_1:def 3;

                then

                consider S2 be Subset of REAL such that

                 A18: (f /. z) = S2 and

                 A19: S2 = [.(a . z), (b . z).] by A3;

                (f /. z) = (f . z) by A16, PARTFUN1:def 6;

                hence (y . z) in (f . z) by A18, A19, A15, A17;

              end;

            end;

            hence x in s by A14, CARD_3: 9;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let I1,I2 be Subset of ( REAL n) such that

         A20: for x be object holds x in I1 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).]) and

         A21: for x be object holds x in I2 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).]);

        thus I1 c= I2

        proof

          let x be object;

          assume x in I1;

          then

          consider y be Element of ( REAL n) such that

           A22: x = y and

           A23: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).] by A20;

          thus x in I2 by A21, A23, A22;

        end;

        let x be object;

        assume x in I2;

        then

        consider y be Element of ( REAL n) such that

         A24: x = y and

         A25: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).] by A21;

        thus x in I1 by A24, A25, A20;

      end;

    end

    definition

      let n, a, b;

      :: SRINGS_5:def15

      func OpenHyperInterval (a,b) -> Subset of ( REAL n) means

      : Def4: for x be object holds x in it iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[);

      existence

      proof

        defpred P[ object, object] means ex S be Subset of REAL st S = $2 & S = ].(a . $1), (b . $1).[;

        

         A1: for i be Nat st i in ( Seg n) holds ex d be Element of ( bool REAL ) st P[i, d];

        consider f be FinSequence of ( bool REAL ) such that

         A2: ( len f) = n and

         A3: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A1);

        

         A4: ( dom f) = ( Seg n) by A2, FINSEQ_1:def 3;

        set s = ( product f);

        s c= ( product (( Seg n) --> REAL ))

        proof

          let t be object;

          assume

           A5: t in s;

          then

          reconsider t1 = t as Function;

          

           A6: ( dom t1) = ( dom f) & for y be object st y in ( dom f) holds (t1 . y) in (f . y) by A5, CARD_3: 9;

          now

            ( dom (( Seg n) --> REAL )) = ( Seg n) by FUNCOP_1: 13;

            hence ( dom t1) = ( dom (( Seg n) --> REAL )) by A6, A2, FINSEQ_1:def 3;

            thus for y be object st y in ( dom (( Seg n) --> REAL )) holds (t1 . y) in ((( Seg n) --> REAL ) . y)

            proof

              let y be object;

              assume

               A7: y in ( dom (( Seg n) --> REAL ));

              then y in ( Seg n);

              then y in ( dom f) by A2, FINSEQ_1:def 3;

              then (t1 . y) in (f . y) & (f . y) in ( bool REAL ) by A5, CARD_3: 9, FINSEQ_2: 11;

              then (t1 . y) in REAL ;

              hence thesis by A7, FUNCOP_1: 7;

            end;

          end;

          hence t in ( product (( Seg n) --> REAL )) by CARD_3: 9;

        end;

        then

        reconsider s as Subset of ( REAL n) by Th7;

        for x be object holds x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[)

        proof

          let x be object;

          thus x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[)

          proof

            hereby

              assume

               A8: x in s;

              then

              reconsider y = x as Element of ( REAL n);

              take y;

              thus x = y;

              thus for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[

              proof

                let i be Nat;

                assume

                 A9: i in ( Seg n);

                then

                 A10: i in ( dom f) by A2, FINSEQ_1:def 3;

                then

                 A11: (y . i) in (f . i) by A8, CARD_3: 9;

                consider S2 be Subset of REAL such that

                 A12: (f /. i) = S2 and

                 A13: S2 = ].(a . i), (b . i).[ by A9, A3;

                thus (y . i) in ].(a . i), (b . i).[ by A10, A11, A12, A13, PARTFUN1:def 6;

              end;

            end;

            given y be Element of ( REAL n) such that

             A14: x = y and

             A15: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[;

            now

              thus ( dom y) = ( dom f) by A4, FINSEQ_1: 89;

              thus for z be object st z in ( dom f) holds (y . z) in (f . z)

              proof

                let z be object;

                assume

                 A16: z in ( dom f);

                then

                 A17: z in ( Seg n) by A2, FINSEQ_1:def 3;

                then

                consider S2 be Subset of REAL such that

                 A18: (f /. z) = S2 and

                 A19: S2 = ].(a . z), (b . z).[ by A3;

                (f /. z) = (f . z) by A16, PARTFUN1:def 6;

                hence (y . z) in (f . z) by A18, A19, A15, A17;

              end;

            end;

            hence x in s by A14, CARD_3: 9;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let I1,I2 be Subset of ( REAL n) such that

         A20: for x be object holds x in I1 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[) and

         A21: for x be object holds x in I2 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[);

        thus I1 c= I2

        proof

          let x be object;

          assume x in I1;

          then

          consider y be Element of ( REAL n) such that

           A22: x = y and

           A23: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[ by A20;

          thus x in I2 by A21, A23, A22;

        end;

        let x be object;

        assume x in I2;

        then

        consider y be Element of ( REAL n) such that

         A24: x = y and

         A25: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[ by A21;

        thus x in I1 by A24, A25, A20;

      end;

    end

    definition

      let n, a, b;

      :: SRINGS_5:def16

      func LeftOpenHyperInterval (a,b) -> Subset of ( REAL n) means

      : Def5: for x be object holds x in it iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).]);

      existence

      proof

        defpred P[ object, object] means ex S be Subset of REAL st S = $2 & S = ].(a . $1), (b . $1).];

        

         A1: for i be Nat st i in ( Seg n) holds ex d be Element of ( bool REAL ) st P[i, d];

        consider f be FinSequence of ( bool REAL ) such that

         A2: ( len f) = n and

         A3: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A1);

        

         A4: ( dom f) = ( Seg n) by A2, FINSEQ_1:def 3;

        set s = ( product f);

        s c= ( product (( Seg n) --> REAL ))

        proof

          let t be object;

          assume

           A5: t in s;

          then

          reconsider t1 = t as Function;

          

           A6: ( dom t1) = ( dom f) & for y be object st y in ( dom f) holds (t1 . y) in (f . y) by A5, CARD_3: 9;

          now

            ( dom (( Seg n) --> REAL )) = ( Seg n) by FUNCOP_1: 13;

            hence ( dom t1) = ( dom (( Seg n) --> REAL )) by A6, A2, FINSEQ_1:def 3;

            thus for y be object st y in ( dom (( Seg n) --> REAL )) holds (t1 . y) in ((( Seg n) --> REAL ) . y)

            proof

              let y be object;

              assume

               A7: y in ( dom (( Seg n) --> REAL ));

              then y in ( Seg n);

              then y in ( dom f) by A2, FINSEQ_1:def 3;

              then (t1 . y) in (f . y) & (f . y) in ( bool REAL ) by A5, CARD_3: 9, FINSEQ_2: 11;

              then (t1 . y) in REAL ;

              hence thesis by A7, FUNCOP_1: 7;

            end;

          end;

          hence t in ( product (( Seg n) --> REAL )) by CARD_3: 9;

        end;

        then

        reconsider s as Subset of ( REAL n) by Th7;

        for x be object holds x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).])

        proof

          let x be object;

          thus x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).])

          proof

            hereby

              assume

               A8: x in s;

              then

              reconsider y = x as Element of ( REAL n);

              take y;

              thus x = y;

              thus for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).]

              proof

                let i be Nat;

                assume

                 A9: i in ( Seg n);

                then

                 A10: i in ( dom f) by A2, FINSEQ_1:def 3;

                then

                 A11: (y . i) in (f . i) by A8, CARD_3: 9;

                consider S2 be Subset of REAL such that

                 A12: (f /. i) = S2 and

                 A13: S2 = ].(a . i), (b . i).] by A9, A3;

                thus (y . i) in ].(a . i), (b . i).] by A10, A11, A12, A13, PARTFUN1:def 6;

              end;

            end;

            given y be Element of ( REAL n) such that

             A14: x = y and

             A15: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).];

            now

              thus ( dom y) = ( dom f) by A4, FINSEQ_1: 89;

              thus for z be object st z in ( dom f) holds (y . z) in (f . z)

              proof

                let z be object;

                assume

                 A16: z in ( dom f);

                then

                 A17: z in ( Seg n) by A2, FINSEQ_1:def 3;

                then

                consider S2 be Subset of REAL such that

                 A18: (f /. z) = S2 and

                 A19: S2 = ].(a . z), (b . z).] by A3;

                (f /. z) = (f . z) by A16, PARTFUN1:def 6;

                hence (y . z) in (f . z) by A18, A19, A15, A17;

              end;

            end;

            hence x in s by A14, CARD_3: 9;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let I1,I2 be Subset of ( REAL n) such that

         A20: for x be object holds x in I1 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).]) and

         A21: for x be object holds x in I2 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).]);

        thus I1 c= I2

        proof

          let x be object;

          assume x in I1;

          then

          consider y be Element of ( REAL n) such that

           A22: x = y and

           A23: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).] by A20;

          thus x in I2 by A21, A23, A22;

        end;

        let x be object;

        assume x in I2;

        then

        consider y be Element of ( REAL n) such that

         A24: x = y and

         A25: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).] by A21;

        thus x in I1 by A24, A25, A20;

      end;

    end

    definition

      let n, a, b;

      :: SRINGS_5:def17

      func RightOpenHyperInterval (a,b) -> Subset of ( REAL n) means

      : Def6: for x be object holds x in it iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[);

      existence

      proof

        defpred P[ object, object] means ex S be Subset of REAL st S = $2 & S = [.(a . $1), (b . $1).[;

        

         A1: for i be Nat st i in ( Seg n) holds ex d be Element of ( bool REAL ) st P[i, d];

        consider f be FinSequence of ( bool REAL ) such that

         A2: ( len f) = n and

         A3: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A1);

        

         A4: ( dom f) = ( Seg n) by A2, FINSEQ_1:def 3;

        set s = ( product f);

        s c= ( product (( Seg n) --> REAL ))

        proof

          let t be object;

          assume

           A5: t in s;

          then

          reconsider t1 = t as Function;

          

           A6: ( dom t1) = ( dom f) & for y be object st y in ( dom f) holds (t1 . y) in (f . y) by A5, CARD_3: 9;

          now

            ( dom (( Seg n) --> REAL )) = ( Seg n) by FUNCOP_1: 13;

            hence ( dom t1) = ( dom (( Seg n) --> REAL )) by A6, A2, FINSEQ_1:def 3;

            thus for y be object st y in ( dom (( Seg n) --> REAL )) holds (t1 . y) in ((( Seg n) --> REAL ) . y)

            proof

              let y be object;

              assume

               A7: y in ( dom (( Seg n) --> REAL ));

              then y in ( Seg n);

              then y in ( dom f) by A2, FINSEQ_1:def 3;

              then (t1 . y) in (f . y) & (f . y) in ( bool REAL ) by A5, CARD_3: 9, FINSEQ_2: 11;

              then (t1 . y) in REAL ;

              hence thesis by A7, FUNCOP_1: 7;

            end;

          end;

          hence t in ( product (( Seg n) --> REAL )) by CARD_3: 9;

        end;

        then

        reconsider s as Subset of ( REAL n) by Th7;

        for x be object holds x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[)

        proof

          let x be object;

          thus x in s iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[)

          proof

            hereby

              assume

               A8: x in s;

              then

              reconsider y = x as Element of ( REAL n);

              take y;

              thus x = y;

              thus for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[

              proof

                let i be Nat;

                assume

                 A9: i in ( Seg n);

                then

                 A10: i in ( dom f) by A2, FINSEQ_1:def 3;

                then

                 A11: (y . i) in (f . i) by A8, CARD_3: 9;

                consider S2 be Subset of REAL such that

                 A12: (f /. i) = S2 and

                 A13: S2 = [.(a . i), (b . i).[ by A9, A3;

                thus (y . i) in [.(a . i), (b . i).[ by A10, A11, A12, A13, PARTFUN1:def 6;

              end;

            end;

            given y be Element of ( REAL n) such that

             A14: x = y and

             A15: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[;

            now

              thus ( dom y) = ( dom f) by A4, FINSEQ_1: 89;

              thus for z be object st z in ( dom f) holds (y . z) in (f . z)

              proof

                let z be object;

                assume

                 A16: z in ( dom f);

                then

                 A17: z in ( Seg n) by A2, FINSEQ_1:def 3;

                then

                consider S2 be Subset of REAL such that

                 A18: (f /. z) = S2 and

                 A19: S2 = [.(a . z), (b . z).[ by A3;

                (f /. z) = (f . z) by A16, PARTFUN1:def 6;

                hence (y . z) in (f . z) by A18, A19, A15, A17;

              end;

            end;

            hence x in s by A14, CARD_3: 9;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let I1,I2 be Subset of ( REAL n) such that

         A20: for x be object holds x in I1 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[) and

         A21: for x be object holds x in I2 iff ex y be Element of ( REAL n) st x = y & (for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[);

        thus I1 c= I2

        proof

          let x be object;

          assume x in I1;

          then

          consider y be Element of ( REAL n) such that

           A22: x = y and

           A23: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[ by A20;

          thus x in I2 by A21, A23, A22;

        end;

        thus I2 c= I1

        proof

          let x be object;

          assume x in I2;

          then

          consider y be Element of ( REAL n) such that

           A24: x = y and

           A25: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[ by A21;

          thus x in I1 by A24, A25, A20;

        end;

      end;

    end

    theorem :: SRINGS_5:67

    

     Th48: ( ClosedHyperInterval (a,a)) = {a}

    proof

      

       A1: ( ClosedHyperInterval (a,a)) c= {a}

      proof

        let x be object;

        assume x in ( ClosedHyperInterval (a,a));

        then

        consider y be Element of ( REAL n) such that

         A2: x = y and

         A3: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (a . i).] by Def3;

        reconsider y1 = y, a1 = a as Function;

        

         A4: ( dom y) = ( Seg n) & ( dom a1) = ( Seg n) by FINSEQ_2: 124;

        for z be object st z in ( dom y1) holds (y1 . z) = (a1 . z)

        proof

          let z be object;

          assume z in ( dom y1);

          then z in ( Seg n) by FINSEQ_2: 124;

          then (y1 . z) in [.(a . z), (a . z).] by A3;

          then (y1 . z) in {(a . z)} by XXREAL_1: 17;

          hence thesis by TARSKI:def 1;

        end;

        then y1 = a1 by A4, FUNCT_1:def 11;

        hence thesis by A2, TARSKI:def 1;

      end;

       {a} c= ( ClosedHyperInterval (a,a))

      proof

        let x be object;

        assume

         A5: x in {a};

        then

        reconsider x1 = x as Element of ( REAL n) by TARSKI:def 1;

        for i be Nat st i in ( Seg n) holds (x1 . i) in [.(a . i), (a . i).]

        proof

          let i be Nat;

          assume i in ( Seg n);

          (x1 . i) = (a . i) by A5, TARSKI:def 1;

          then (x1 . i) in {(a . i)} by TARSKI:def 1;

          hence thesis by XXREAL_1: 17;

        end;

        hence thesis by Def3;

      end;

      hence thesis by A1;

    end;

    registration

      let n, a;

      cluster ( ClosedHyperInterval (a,a)) -> trivial;

      coherence

      proof

        ( ClosedHyperInterval (a,a)) = {a} by Th48;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:68

    ( OpenHyperInterval (a,b)) c= ( LeftOpenHyperInterval (a,b)) & ( OpenHyperInterval (a,b)) c= ( RightOpenHyperInterval (a,b)) & ( LeftOpenHyperInterval (a,b)) c= ( ClosedHyperInterval (a,b)) & ( RightOpenHyperInterval (a,b)) c= ( ClosedHyperInterval (a,b))

    proof

      thus ( OpenHyperInterval (a,b)) c= ( LeftOpenHyperInterval (a,b))

      proof

        let x be object;

        assume x in ( OpenHyperInterval (a,b));

        then

        consider y be Element of ( REAL n) such that

         A1: x = y and

         A2: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[ by Def4;

        now

          let i be Nat;

          assume i in ( Seg n);

          then (y . i) in ].(a . i), (b . i).[ & ].(a . i), (b . i).[ c= ].(a . i), (b . i).] by A2, XXREAL_1: 21;

          hence (y . i) in ].(a . i), (b . i).];

        end;

        hence thesis by A1, Def5;

      end;

      thus ( OpenHyperInterval (a,b)) c= ( RightOpenHyperInterval (a,b))

      proof

        let x be object;

        assume x in ( OpenHyperInterval (a,b));

        then

        consider y be Element of ( REAL n) such that

         A3: x = y and

         A4: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).[ by Def4;

        now

          let i be Nat;

          assume i in ( Seg n);

          then (y . i) in ].(a . i), (b . i).[ & ].(a . i), (b . i).[ c= [.(a . i), (b . i).[ by A4, XXREAL_1: 22;

          hence (y . i) in [.(a . i), (b . i).[;

        end;

        hence thesis by A3, Def6;

      end;

      thus ( LeftOpenHyperInterval (a,b)) c= ( ClosedHyperInterval (a,b))

      proof

        let x be object;

        assume x in ( LeftOpenHyperInterval (a,b));

        then

        consider y be Element of ( REAL n) such that

         A5: x = y and

         A6: for i be Nat st i in ( Seg n) holds (y . i) in ].(a . i), (b . i).] by Def5;

        now

          let i be Nat;

          assume i in ( Seg n);

          then (y . i) in ].(a . i), (b . i).] & ].(a . i), (b . i).] c= [.(a . i), (b . i).] by A6, XXREAL_1: 23;

          hence (y . i) in [.(a . i), (b . i).];

        end;

        hence thesis by A5, Def3;

      end;

      thus ( RightOpenHyperInterval (a,b)) c= ( ClosedHyperInterval (a,b))

      proof

        let x be object;

        assume x in ( RightOpenHyperInterval (a,b));

        then

        consider y be Element of ( REAL n) such that

         A7: x = y and

         A8: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).[ by Def6;

        now

          let i be Nat;

          assume i in ( Seg n);

          then (y . i) in [.(a . i), (b . i).[ & [.(a . i), (b . i).[ c= [.(a . i), (b . i).] by A8, XXREAL_1: 24;

          hence (y . i) in [.(a . i), (b . i).];

        end;

        hence thesis by A7, Def3;

      end;

    end;

    definition

      let n, a, b;

      :: SRINGS_5:def18

      pred a <= b means for i be Nat st i in ( Seg n) holds (a . i) <= (b . i);

      reflexivity ;

    end

    theorem :: SRINGS_5:69

    a <= b & b <= c implies a <= c

    proof

      assume that

       A1: a <= b and

       A2: b <= c;

      for i be Nat st i in ( Seg n) holds (a . i) <= (c . i)

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (a . i) <= (b . i) & (b . i) <= (c . i) by A1, A2;

        hence thesis by XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:70

    

     Th49: a <= c & d <= b implies ( ClosedHyperInterval (c,d)) c= ( ClosedHyperInterval (a,b))

    proof

      assume that

       A1: a <= c and

       A3: d <= b;

      now

        let t be object;

        assume t in ( ClosedHyperInterval (c,d));

        then

        consider t1 be Element of ( REAL n) such that

         A4: t = t1 and

         A5: for i be Nat st i in ( Seg n) holds (t1 . i) in [.(c . i), (d . i).] by Def3;

        for i be Nat st i in ( Seg n) holds (t1 . i) in [.(a . i), (b . i).]

        proof

          let i be Nat;

          assume

           A6: i in ( Seg n);

          then (a . i) <= (c . i) & (d . i) <= (b . i) by A1, A3;

          then [.(c . i), (d . i).] c= [.(a . i), (b . i).] by XXREAL_1: 34;

          hence thesis by A6, A5;

        end;

        hence t in ( ClosedHyperInterval (a,b)) by A4, Def3;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:71

    a <= b implies ( ClosedHyperInterval (a,b)) is non empty

    proof

      assume a <= b;

      then ( ClosedHyperInterval (a,a)) c= ( ClosedHyperInterval (a,b)) by Th49;

      then {a} c= ( ClosedHyperInterval (a,b)) by Th48;

      hence thesis;

    end;

    definition

      let n, a, b;

      :: SRINGS_5:def19

      pred a < b means for i be Nat st i in ( Seg n) holds (a . i) < (b . i);

    end

    theorem :: SRINGS_5:72

    a < b & b < c implies a < c

    proof

      assume that

       A1: a < b and

       A2: b < c;

      for i be Nat st i in ( Seg n) holds (a . i) < (c . i)

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (a . i) < (b . i) & (b . i) < (c . i) by A1, A2;

        hence thesis by XXREAL_0: 2;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:73

    b < a & n is non zero implies ( ClosedHyperInterval (a,b)) is empty

    proof

      assume that

       A1: b < a and

       A2: n is non zero;

      assume not ( ClosedHyperInterval (a,b)) is empty;

      then

      consider x be object such that

       A3: x in ( ClosedHyperInterval (a,b));

      consider y be Element of ( REAL n) such that x = y and

       A4: for i be Nat st i in ( Seg n) holds (y . i) in [.(a . i), (b . i).] by A3, Def3;

      1 <= n by A2, NAT_1: 14;

      then (b . 1) < (a . 1) & (y . 1) in [.(a . 1), (b . 1).] by A1, A4, FINSEQ_1: 1;

      hence contradiction by XXREAL_1: 29;

    end;

    theorem :: SRINGS_5:74

    

     Th50: (n |-> r) is Element of ( REAL n)

    proof

      

       A1: r is Element of REAL by XREAL_0:def 1;

      set f = (n |-> r);

      reconsider f as Function;

      f in ( Funcs (( Seg n), REAL ))

      proof

        f is Element of (n -tuples_on REAL ) by A1, FINSEQ_2: 112;

        then f in (n -tuples_on REAL );

        hence thesis by FINSEQ_2: 93;

      end;

      hence thesis by FINSEQ_2: 93;

    end;

    definition

      let n, r;

      :: original: |->

      redefine

      func n |-> r -> Element of ( REAL n) ;

      coherence by Th50;

    end

    definition

      let r;

      :: original: <*

      redefine

      func <*r*> -> Element of ( REAL 1) ;

      coherence

      proof

        (1 |-> r) is Element of ( REAL 1);

        hence thesis by FINSEQ_2: 59;

      end;

    end

    theorem :: SRINGS_5:75

    

     Th51: for n be non zero Nat, e be Point of ( Euclid n) holds ex a be Element of ( REAL n) st a = e & ( OpenHypercube (e,r)) = ( OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))))

    proof

      let n be non zero Nat, e be Point of ( Euclid n);

      reconsider a = e as Element of ( REAL n);

      reconsider p = e as Point of ( TOP-REAL n) by EUCLID: 67;

      consider e0 be Point of ( Euclid n) such that

       A1: p = e0 and

       A2: ( OpenHypercube (e0,r)) = ( OpenHypercube (p,r)) by TIETZE_2:def 1;

      take a;

      thus a = e;

      

       A3: ( OpenHypercube (e,r)) c= ( OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))))

      proof

        let x be object;

        assume

         A4: x in ( OpenHypercube (e,r));

        then

        reconsider y = x as Element of ( REAL n);

        for i be Nat st i in ( Seg n) holds (y . i) in ].((a - (n |-> r)) . i), ((a + (n |-> r)) . i).[

        proof

          let i be Nat;

          assume

           A5: i in ( Seg n);

          

           A6: ((a - (n |-> r)) . i) = ((a . i) - ((n |-> r) . i)) by RVSUM_1: 27

          .= ((a . i) - r) by A5, FINSEQ_2: 57;

          ((a + (n |-> r)) . i) = ((a . i) + ((n |-> r) . i)) by RVSUM_1: 11

          .= ((a . i) + r) by A5, FINSEQ_2: 57;

          hence thesis by A5, A6, A1, A2, A4, TIETZE_2: 4;

        end;

        hence thesis by Def4;

      end;

      ( OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r)))) c= ( OpenHypercube (e,r))

      proof

        let x be object;

        assume

         A7: x in ( OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r))));

        then

        reconsider q = x as Element of ( TOP-REAL n) by EUCLID: 22;

        now

          let i be Nat;

          assume

           A8: i in ( Seg n);

          consider y be Element of ( REAL n) such that

           A9: x = y and

           A10: (for i be Nat st i in ( Seg n) holds (y . i) in ].((a - (n |-> r)) . i), ((a + (n |-> r)) . i).[) by A7, Def4;

          

           A11: ((a - (n |-> r)) . i) = ((a . i) - ((n |-> r) . i)) by RVSUM_1: 27

          .= ((a . i) - r) by A8, FINSEQ_2: 57;

          ((a + (n |-> r)) . i) = ((a . i) + ((n |-> r) . i)) by RVSUM_1: 11

          .= ((a . i) + r) by A8, FINSEQ_2: 57;

          hence (q . i) in ].((p . i) - r), ((p . i) + r).[ by A11, A8, A9, A10;

        end;

        hence thesis by A1, A2, TIETZE_2: 4;

      end;

      hence thesis by A3;

    end;

    theorem :: SRINGS_5:76

    

     Th52: for p be Point of ( TOP-REAL n) holds ex a be Element of ( REAL n) st a = p & ( ClosedHypercube (p,b)) = ( ClosedHyperInterval ((a - b),(a + b)))

    proof

      let p be Point of ( TOP-REAL n);

      reconsider a = p as Element of ( REAL n) by EUCLID: 22;

      take a;

      thus a = p;

      

       A1: ( ClosedHypercube (p,b)) c= ( ClosedHyperInterval ((a - b),(a + b)))

      proof

        let x be object;

        assume

         A2: x in ( ClosedHypercube (p,b));

        then

        reconsider y = x as Element of ( REAL n) by EUCLID: 22;

        for i be Nat st i in ( Seg n) holds (y . i) in [.((a - b) . i), ((a + b) . i).]

        proof

          let i be Nat;

          assume

           A3: i in ( Seg n);

          ((a . i) - (b . i)) = ((a - b) . i) & ((a + b) . i) = ((a . i) + (b . i)) by RVSUM_1: 11, RVSUM_1: 27;

          hence thesis by A2, A3, TIETZE_2:def 2;

        end;

        hence thesis by Def3;

      end;

      ( ClosedHyperInterval ((a - b),(a + b))) c= ( ClosedHypercube (p,b))

      proof

        let x be object;

        assume

         A4: x in ( ClosedHyperInterval ((a - b),(a + b)));

        then

        reconsider q = x as Element of ( TOP-REAL n) by EUCLID: 22;

        now

          let i be Nat;

          assume

           A5: i in ( Seg n);

          consider y be Element of ( REAL n) such that

           A6: x = y and

           A7: (for i be Nat st i in ( Seg n) holds (y . i) in [.((a - b) . i), ((a + b) . i).]) by A4, Def3;

          ((a - b) . i) = ((a . i) - (b . i)) & ((a + b) . i) = ((a . i) + (b . i)) by RVSUM_1: 11, RVSUM_1: 27;

          hence (q . i) in [.((p . i) - (b . i)), ((p . i) + (b . i)).] by A5, A6, A7;

        end;

        hence thesis by TIETZE_2:def 2;

      end;

      hence thesis by A1;

    end;

    begin

    theorem :: SRINGS_5:77

    for x be Real holds x in [.r, s.] iff (1 |-> x) in ( ClosedHyperInterval ( <*r*>, <*s*>))

    proof

      set a1 = <*r*>, b1 = <*s*>;

      

       A1: for x be Real st x in [.r, s.] holds (1 |-> x) in ( ClosedHyperInterval (a1,b1))

      proof

        let t be Real;

        assume

         A2: t in [.r, s.];

        reconsider t1 = (1 |-> t) as Element of ( REAL 1);

        ex y be Element of ( REAL 1) st t1 = y & (for i be Nat st i in ( Seg 1) holds (y . i) in [.(a1 . i), (b1 . i).])

        proof

          take t1;

          thus t1 = t1;

          thus for i be Nat st i in ( Seg 1) holds (t1 . i) in [.(a1 . i), (b1 . i).]

          proof

            let i be Nat;

            assume

             A3: i in ( Seg 1);

            then

             A4: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

            now

              (t1 . 1) = ((( Seg 1) --> t) . 1) by FINSEQ_2:def 2;

              hence (t1 . i) = t by A3, A4, FUNCOP_1: 7;

              thus (a1 . i) = r & (b1 . i) = s by A4, FINSEQ_1:def 8;

            end;

            hence thesis by A2;

          end;

        end;

        hence thesis by Def3;

      end;

      for x be Real st (1 |-> x) in ( ClosedHyperInterval (a1,b1)) holds x in [.r, s.]

      proof

        let x be Real;

        assume (1 |-> x) in ( ClosedHyperInterval (a1,b1));

        then

        consider y be Element of ( REAL 1) such that

         A5: (1 |-> x) = y and

         A6: for i be Nat st i in ( Seg 1) holds (y . i) in [.(a1 . i), (b1 . i).] by Def3;

        

         A7: 1 in ( Seg 1);

        y = (( Seg 1) --> x) & 1 in ( Seg 1) by A5, FINSEQ_2:def 2;

        then

         A8: (y . 1) = x by FUNCOP_1: 7;

        (a1 . 1) = r & (b1 . 1) = s by FINSEQ_1:def 8;

        hence thesis by A6, A7, A8;

      end;

      hence thesis by A1;

    end;

    theorem :: SRINGS_5:78

    for x be Real holds x in ].r, s.[ iff (1 |-> x) in ( OpenHyperInterval ( <*r*>, <*s*>))

    proof

      set a1 = <*r*>, b1 = <*s*>;

      

       A1: for x be Real st x in ].r, s.[ holds (1 |-> x) in ( OpenHyperInterval (a1,b1))

      proof

        let t be Real;

        assume

         A2: t in ].r, s.[;

        reconsider t1 = (1 |-> t) as Element of ( REAL 1);

        ex y be Element of ( REAL 1) st t1 = y & (for i be Nat st i in ( Seg 1) holds (y . i) in ].(a1 . i), (b1 . i).[)

        proof

          take t1;

          thus t1 = t1;

          thus for i be Nat st i in ( Seg 1) holds (t1 . i) in ].(a1 . i), (b1 . i).[

          proof

            let i be Nat;

            assume

             A3: i in ( Seg 1);

            then

             A4: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

            now

              (t1 . 1) = ((( Seg 1) --> t) . 1) by FINSEQ_2:def 2;

              hence (t1 . i) = t by A3, A4, FUNCOP_1: 7;

              thus (a1 . i) = r & (b1 . i) = s by A4, FINSEQ_1:def 8;

            end;

            hence thesis by A2;

          end;

        end;

        hence thesis by Def4;

      end;

      for x be Real st (1 |-> x) in ( OpenHyperInterval (a1,b1)) holds x in ].r, s.[

      proof

        let x be Real;

        assume (1 |-> x) in ( OpenHyperInterval (a1,b1));

        then

        consider y be Element of ( REAL 1) such that

         A5: (1 |-> x) = y and

         A6: for i be Nat st i in ( Seg 1) holds (y . i) in ].(a1 . i), (b1 . i).[ by Def4;

        

         A7: 1 in ( Seg 1);

        y = (( Seg 1) --> x) & 1 in ( Seg 1) by A5, FINSEQ_2:def 2;

        then

         A8: (y . 1) = x by FUNCOP_1: 7;

        (a1 . 1) = r & (b1 . 1) = s by FINSEQ_1:def 8;

        hence thesis by A6, A7, A8;

      end;

      hence thesis by A1;

    end;

    theorem :: SRINGS_5:79

    for x be Real holds x in ].r, s.] iff (1 |-> x) in ( LeftOpenHyperInterval ( <*r*>, <*s*>))

    proof

      set a1 = <*r*>, b1 = <*s*>;

      

       A1: for x be Real st x in ].r, s.] holds (1 |-> x) in ( LeftOpenHyperInterval (a1,b1))

      proof

        let t be Real;

        assume

         A2: t in ].r, s.];

        reconsider t1 = (1 |-> t) as Element of ( REAL 1);

        ex y be Element of ( REAL 1) st t1 = y & (for i be Nat st i in ( Seg 1) holds (y . i) in ].(a1 . i), (b1 . i).])

        proof

          take t1;

          thus t1 = t1;

          thus for i be Nat st i in ( Seg 1) holds (t1 . i) in ].(a1 . i), (b1 . i).]

          proof

            let i be Nat;

            assume

             A3: i in ( Seg 1);

            then

             A4: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

            now

              (t1 . 1) = ((( Seg 1) --> t) . 1) by FINSEQ_2:def 2;

              hence (t1 . i) = t by A3, A4, FUNCOP_1: 7;

              thus (a1 . i) = r & (b1 . i) = s by A4, FINSEQ_1:def 8;

            end;

            hence thesis by A2;

          end;

        end;

        hence thesis by Def5;

      end;

      for x be Real st (1 |-> x) in ( LeftOpenHyperInterval (a1,b1)) holds x in ].r, s.]

      proof

        let x be Real;

        assume (1 |-> x) in ( LeftOpenHyperInterval (a1,b1));

        then

        consider y be Element of ( REAL 1) such that

         A5: (1 |-> x) = y and

         A6: for i be Nat st i in ( Seg 1) holds (y . i) in ].(a1 . i), (b1 . i).] by Def5;

        

         A7: 1 in ( Seg 1);

        y = (( Seg 1) --> x) & 1 in ( Seg 1) by A5, FINSEQ_2:def 2;

        then

         A8: (y . 1) = x by FUNCOP_1: 7;

        (a1 . 1) = r & (b1 . 1) = s by FINSEQ_1:def 8;

        hence thesis by A6, A7, A8;

      end;

      hence thesis by A1;

    end;

    theorem :: SRINGS_5:80

    for x be Real holds x in [.r, s.[ iff (1 |-> x) in ( RightOpenHyperInterval ( <*r*>, <*s*>))

    proof

      set a1 = <*r*>, b1 = <*s*>;

      

       A1: for x be Real st x in [.r, s.[ holds (1 |-> x) in ( RightOpenHyperInterval (a1,b1))

      proof

        let t be Real;

        assume

         A2: t in [.r, s.[;

        reconsider t1 = (1 |-> t) as Element of ( REAL 1);

        ex y be Element of ( REAL 1) st t1 = y & (for i be Nat st i in ( Seg 1) holds (y . i) in [.(a1 . i), (b1 . i).[)

        proof

          take t1;

          thus t1 = t1;

          thus for i be Nat st i in ( Seg 1) holds (t1 . i) in [.(a1 . i), (b1 . i).[

          proof

            let i be Nat;

            assume

             A3: i in ( Seg 1);

            then

             A4: i = 1 by FINSEQ_1: 2, TARSKI:def 1;

            now

              (t1 . 1) = ((( Seg 1) --> t) . 1) by FINSEQ_2:def 2;

              hence (t1 . i) = t by A3, A4, FUNCOP_1: 7;

              thus (a1 . i) = r & (b1 . i) = s by A4, FINSEQ_1:def 8;

            end;

            hence thesis by A2;

          end;

        end;

        hence thesis by Def6;

      end;

      for x be Real st (1 |-> x) in ( RightOpenHyperInterval (a1,b1)) holds x in [.r, s.[

      proof

        let x be Real;

        assume (1 |-> x) in ( RightOpenHyperInterval (a1,b1));

        then

        consider y be Element of ( REAL 1) such that

         A5: (1 |-> x) = y and

         A6: for i be Nat st i in ( Seg 1) holds (y . i) in [.(a1 . i), (b1 . i).[ by Def6;

        

         A7: 1 in ( Seg 1);

        y = (( Seg 1) --> x) & 1 in ( Seg 1) by A5, FINSEQ_2:def 2;

        then

         A8: (y . 1) = x by FUNCOP_1: 7;

        (a1 . 1) = r & (b1 . 1) = s by FINSEQ_1:def 8;

        hence thesis by A6, A7, A8;

      end;

      hence thesis by A1;

    end;

    begin

    reserve n for non zero Nat;

    theorem :: SRINGS_5:81

    

     Th53: for s be Tuple of n, the_set_of_all_open_real_bounded_intervals holds ex a,b be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).[

    proof

      let s be Tuple of n, the_set_of_all_open_real_bounded_intervals ;

      s in ( Funcs (( Seg n), the_set_of_all_open_real_bounded_intervals )) by Th9;

      then

      consider f be Function such that

       A1: s = f and

       A2: ( dom f) = ( Seg n) and ( rng f) c= the_set_of_all_open_real_bounded_intervals by FUNCT_2:def 2;

      defpred P[ object, object] means ex f be Element of [: REAL , REAL :] st f = $2 & (s . $1) = ].(f `1 ), (f `2 ).[;

      

       A3: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (s . i) in ( rng s) by A1, A2, FUNCT_1: 3;

        then (s . i) in the set of all ].a, b.[ where a,b be Real;

        then

        consider a,b be Real such that

         A4: (s . i) = ].a, b.[;

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d = [a, b] as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        (s . i) = ].(d `1 ), (d `2 ).[ by A4;

        hence thesis;

      end;

      consider f be FinSequence of [: REAL , REAL :] such that

       A5: ( len f) = n and

       A6: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A3);

      reconsider f as n -element FinSequence of [: REAL , REAL :] by A5, CARD_1:def 7;

      consider z be Element of [:( REAL n), ( REAL n):] such that

       A7: for i be Nat st i in ( Seg n) holds ((z `1 ) . i) = ((f /. i) `1 ) & ((z `2 ) . i) = ((f /. i) `2 ) by Th13;

      reconsider a = (z `1 ), b = (z `2 ) as Element of ( REAL n);

      take a, b;

      thus for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).[

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (a . i) = ((f /. i) `1 ) & (b . i) = ((f /. i) `2 ) & P[i, (f /. i)] by A6, A7;

        hence (s . i) = ].(a . i), (b . i).[;

      end;

    end;

    theorem :: SRINGS_5:82

    for x be Element of ( Product (n, the_set_of_all_open_real_bounded_intervals )) holds (ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).[)))

    proof

      let x be Element of ( Product (n, the_set_of_all_open_real_bounded_intervals ));

      consider s be Tuple of n, the_set_of_all_open_real_bounded_intervals such that

       A1: for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x by Th42;

      consider a,b be Element of ( REAL n) such that

       A2: for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).[ by Th53;

      take a, b;

      for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).[)

      proof

        let t be Element of ( REAL n);

        hereby

          assume

           A3: t in x;

          thus (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).[)

          proof

            let i be Nat;

            assume

             A4: i in ( Seg n);

            then (s . i) = ].(a . i), (b . i).[ by A2;

            hence (t . i) in ].(a . i), (b . i).[ by A1, A3, A4;

          end;

        end;

        assume

         A5: (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).[);

        for i be Nat st i in ( Seg n) holds (t . i) in (s . i)

        proof

          let i be Nat;

          assume

           A6: i in ( Seg n);

          then (s . i) = ].(a . i), (b . i).[ by A2;

          hence (t . i) in (s . i) by A6, A5;

        end;

        hence t in x by A1;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:83

    

     Th54: for s be Tuple of n, the_set_of_all_left_open_real_bounded_intervals holds ex a,b be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).]

    proof

      let s be Tuple of n, the_set_of_all_left_open_real_bounded_intervals ;

      s in ( Funcs (( Seg n), the_set_of_all_left_open_real_bounded_intervals )) by Th9;

      then

      consider f be Function such that

       A1: s = f and

       A2: ( dom f) = ( Seg n) and ( rng f) c= the_set_of_all_left_open_real_bounded_intervals by FUNCT_2:def 2;

      defpred P[ object, object] means ex f be Element of [: REAL , REAL :] st f = $2 & (s . $1) = ].(f `1 ), (f `2 ).];

      

       A3: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (s . i) in ( rng s) by A1, A2, FUNCT_1: 3;

        then (s . i) in the set of all ].a, b.] where a,b be Real;

        then

        consider a,b be Real such that

         A4: (s . i) = ].a, b.];

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d = [a, b] as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        (s . i) = ].(d `1 ), (d `2 ).] by A4;

        hence thesis;

      end;

      consider f be FinSequence of [: REAL , REAL :] such that

       A5: ( len f) = n and

       A6: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A3);

      reconsider f as n -element FinSequence of [: REAL , REAL :] by A5, CARD_1:def 7;

      consider z be Element of [:( REAL n), ( REAL n):] such that

       A7: for i be Nat st i in ( Seg n) holds ((z `1 ) . i) = ((f /. i) `1 ) & ((z `2 ) . i) = ((f /. i) `2 ) by Th13;

      reconsider a = (z `1 ), b = (z `2 ) as Element of ( REAL n);

      take a, b;

      thus for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (a . i) = ((f /. i) `1 ) & (b . i) = ((f /. i) `2 ) & P[i, (f /. i)] by A6, A7;

        hence (s . i) = ].(a . i), (b . i).];

      end;

    end;

    theorem :: SRINGS_5:84

    for x be Element of ( Product (n, the_set_of_all_left_open_real_bounded_intervals )) holds (ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])))

    proof

      let x be Element of ( Product (n, the_set_of_all_left_open_real_bounded_intervals ));

      consider s be Tuple of n, the_set_of_all_left_open_real_bounded_intervals such that

       A1: for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x by Th42;

      consider a,b be Element of ( REAL n) such that

       A2: for i be Nat st i in ( Seg n) holds (s . i) = ].(a . i), (b . i).] by Th54;

      take a, b;

      for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])

      proof

        let t be Element of ( REAL n);

        hereby

          assume

           A3: t in x;

          thus (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).])

          proof

            let i be Nat;

            assume

             A4: i in ( Seg n);

            then (s . i) = ].(a . i), (b . i).] by A2;

            hence (t . i) in ].(a . i), (b . i).] by A1, A3, A4;

          end;

        end;

        assume

         A5: (for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).]);

        for i be Nat st i in ( Seg n) holds (t . i) in (s . i)

        proof

          let i be Nat;

          assume

           A6: i in ( Seg n);

          then (s . i) = ].(a . i), (b . i).] by A2;

          hence (t . i) in (s . i) by A6, A5;

        end;

        hence t in x by A1;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:85

    

     Th55: for s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals holds ex a,b be Element of ( REAL n) st for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).[

    proof

      let s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals ;

      s in ( Funcs (( Seg n), the_set_of_all_right_open_real_bounded_intervals )) by Th9;

      then

      consider f be Function such that

       A1: s = f and

       A2: ( dom f) = ( Seg n) and ( rng f) c= the_set_of_all_right_open_real_bounded_intervals by FUNCT_2:def 2;

      defpred P[ object, object] means ex f be Element of [: REAL , REAL :] st f = $2 & (s . $1) = [.(f `1 ), (f `2 ).[;

      

       A3: for i be Nat st i in ( Seg n) holds ex d be Element of [: REAL , REAL :] st P[i, d]

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (s . i) in ( rng s) by A1, A2, FUNCT_1: 3;

        then (s . i) in the set of all [.a, b.[ where a,b be Real;

        then

        consider a,b be Real such that

         A4: (s . i) = [.a, b.[;

        a in REAL & b in REAL by XREAL_0:def 1;

        then

        reconsider d = [a, b] as Element of [: REAL , REAL :] by ZFMISC_1:def 2;

        take d;

        (s . i) = [.(d `1 ), (d `2 ).[ by A4;

        hence thesis;

      end;

      consider f be FinSequence of [: REAL , REAL :] such that

       A5: ( len f) = n and

       A6: for i be Nat st i in ( Seg n) holds P[i, (f /. i)] from FINSEQ_4:sch 1( A3);

      reconsider f as n -element FinSequence of [: REAL , REAL :] by A5, CARD_1:def 7;

      consider z be Element of [:( REAL n), ( REAL n):] such that

       A7: for i be Nat st i in ( Seg n) holds ((z `1 ) . i) = ((f /. i) `1 ) & ((z `2 ) . i) = ((f /. i) `2 ) by Th13;

      reconsider a = (z `1 ), b = (z `2 ) as Element of ( REAL n);

      take a, b;

      thus for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).[

      proof

        let i be Nat;

        assume i in ( Seg n);

        then (a . i) = ((f /. i) `1 ) & (b . i) = ((f /. i) `2 ) & P[i, (f /. i)] by A6, A7;

        hence (s . i) = [.(a . i), (b . i).[;

      end;

    end;

    theorem :: SRINGS_5:86

    for x be Element of ( Product (n, the_set_of_all_right_open_real_bounded_intervals )) holds (ex a,b be Element of ( REAL n) st for t be Element of ( REAL n) holds (t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)))

    proof

      let x be Element of ( Product (n, the_set_of_all_right_open_real_bounded_intervals ));

      consider s be Tuple of n, the_set_of_all_right_open_real_bounded_intervals such that

       A1: for t be Element of ( REAL n) holds (for i be Nat st i in ( Seg n) holds (t . i) in (s . i)) iff t in x by Th42;

      consider a,b be Element of ( REAL n) such that

       A2: for i be Nat st i in ( Seg n) holds (s . i) = [.(a . i), (b . i).[ by Th55;

      take a, b;

      for t be Element of ( REAL n) holds t in x iff (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)

      proof

        let t be Element of ( REAL n);

        hereby

          assume

           A3: t in x;

          thus (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[)

          proof

            let i be Nat;

            assume

             A4: i in ( Seg n);

            then (s . i) = [.(a . i), (b . i).[ by A2;

            hence (t . i) in [.(a . i), (b . i).[ by A1, A3, A4;

          end;

        end;

        assume

         A5: (for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[);

        for i be Nat st i in ( Seg n) holds (t . i) in (s . i)

        proof

          let i be Nat;

          assume

           A6: i in ( Seg n);

          then (s . i) = [.(a . i), (b . i).[ by A2;

          hence (t . i) in (s . i) by A6, A5;

        end;

        hence t in x by A1;

      end;

      hence thesis;

    end;

    theorem :: SRINGS_5:87

    ( MeasurableRectangle ( ProductLeftOpenIntervals n)) = ( Product (n, the_set_of_all_left_open_real_bounded_intervals ))

    proof

      thus ( MeasurableRectangle ( ProductLeftOpenIntervals n)) c= ( Product (n, the_set_of_all_left_open_real_bounded_intervals ))

      proof

        let x be object;

        assume x in ( MeasurableRectangle ( ProductLeftOpenIntervals n));

        then

        consider y be Subset of ( REAL n), a,b be Element of ( REAL n) such that

         A1: x = y and

         A2: for s be object holds (s in y) iff (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).]) by Th32;

        now

          let t be Element of ( REAL n);

          hereby

            assume

             A3: t in y;

            hereby

              let i be Nat;

              assume

               A4: i in ( Seg n);

              consider t0 be Element of ( REAL n) such that

               A5: t = t0 and

               A6: for i be Nat st i in ( Seg n) holds (t0 . i) in ].(a . i), (b . i).] by A3, A2;

              thus (t . i) in ].(a . i), (b . i).] by A6, A4, A5;

            end;

          end;

          assume for i be Nat st i in ( Seg n) holds (t . i) in ].(a . i), (b . i).];

          hence t in y by A2;

        end;

        then y is Element of ( Product (n, the_set_of_all_left_open_real_bounded_intervals )) by Th44;

        hence thesis by A1;

      end;

      thus ( Product (n, the_set_of_all_left_open_real_bounded_intervals )) c= ( MeasurableRectangle ( ProductLeftOpenIntervals n))

      proof

        let x be object;

        assume x in ( Product (n, the_set_of_all_left_open_real_bounded_intervals ));

        then

        consider g be Function such that

         A7: x = ( product g) and

         A8: g in ( product (( Seg n) --> the_set_of_all_left_open_real_bounded_intervals )) by Def2;

        thus x in ( MeasurableRectangle ( ProductLeftOpenIntervals n)) by A7, A8, SRINGS_4:def 4;

      end;

    end;

    theorem :: SRINGS_5:88

    ( MeasurableRectangle ( ProductRightOpenIntervals n)) = ( Product (n, the_set_of_all_right_open_real_bounded_intervals ))

    proof

      thus ( MeasurableRectangle ( ProductRightOpenIntervals n)) c= ( Product (n, the_set_of_all_right_open_real_bounded_intervals ))

      proof

        let x be object;

        assume x in ( MeasurableRectangle ( ProductRightOpenIntervals n));

        then

        consider y be Subset of ( REAL n), a,b be Element of ( REAL n) such that

         A1: x = y and

         A2: for s be object holds (s in y) iff (ex t be Element of ( REAL n) st s = t & for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[) by Th35;

        now

          let t be Element of ( REAL n);

          hereby

            assume

             A3: t in y;

            hereby

              let i be Nat;

              assume

               A4: i in ( Seg n);

              consider t0 be Element of ( REAL n) such that

               A5: t = t0 and

               A6: for i be Nat st i in ( Seg n) holds (t0 . i) in [.(a . i), (b . i).[ by A3, A2;

              thus (t . i) in [.(a . i), (b . i).[ by A6, A4, A5;

            end;

          end;

          assume for i be Nat st i in ( Seg n) holds (t . i) in [.(a . i), (b . i).[;

          hence t in y by A2;

        end;

        then y is Element of ( Product (n, the_set_of_all_right_open_real_bounded_intervals )) by Th45;

        hence thesis by A1;

      end;

      thus ( Product (n, the_set_of_all_right_open_real_bounded_intervals )) c= ( MeasurableRectangle ( ProductRightOpenIntervals n))

      proof

        let x be object;

        assume x in ( Product (n, the_set_of_all_right_open_real_bounded_intervals ));

        then

        consider g be Function such that

         A7: x = ( product g) and

         A8: g in ( product (( Seg n) --> the_set_of_all_right_open_real_bounded_intervals )) by Def2;

        thus x in ( MeasurableRectangle ( ProductRightOpenIntervals n)) by A7, A8, SRINGS_4:def 4;

      end;

    end;

    begin

    reserve n for non zero Nat,

x,y,z for Element of ( REAL n);

    definition

      let n;

      :: SRINGS_5:def20

      func Infty_dist n -> Function of [:( REAL n), ( REAL n):], REAL means

      : Def7: for x,y be Element of ( REAL n) holds (it . (x,y)) = ( sup ( rng ( abs (x - y))));

      existence

      proof

        deffunc F( Element of ( REAL n), Element of ( REAL n)) = ( In (( sup ( rng ( abs ($1 - $2)))), REAL ));

        consider f be Function of [:( REAL n), ( REAL n):], REAL such that

         A1: for x,y be Element of ( REAL n) holds (f . (x,y)) = F(x,y) from BINOP_1:sch 4;

        take f;

        let x,y be Element of ( REAL n);

        ( dom ( abs (x - y))) is non empty;

        then

        consider a be object such that

         A2: a in ( dom ( abs (x - y)));

        (( abs (x - y)) . a) in ( rng ( abs (x - y))) by A2, FUNCT_1:def 3;

        then ( sup ( rng ( abs (x - y)))) in ( rng ( abs (x - y))) by XXREAL_2:def 6;

        then (f . (x,y)) = ( In (( sup ( rng ( abs (x - y)))), REAL )) & ( sup ( rng ( abs (x - y)))) in REAL by A1;

        hence thesis by SUBSET_1:def 8;

      end;

      uniqueness

      proof

        let d1,d2 be Function of [:( REAL n), ( REAL n):], REAL such that

         A3: for x,y be Element of ( REAL n) holds (d1 . (x,y)) = ( sup ( rng ( abs (x - y)))) and

         A4: for x,y be Element of ( REAL n) holds (d2 . (x,y)) = ( sup ( rng ( abs (x - y))));

        now

          let x,y be set;

          assume that

           A5: x in ( REAL n) and

           A6: y in ( REAL n);

          reconsider x1 = x, y1 = y as Element of ( REAL n) by A5, A6;

          (d1 . (x1,y1)) = ( sup ( rng ( abs (x1 - y1)))) by A3

          .= (d2 . (x1,y1)) by A4;

          hence (d1 . (x,y)) = (d2 . (x,y));

        end;

        hence d1 = d2 by BINOP_1:def 21;

      end;

    end

    theorem :: SRINGS_5:89

    

     Th56: the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg n) is real-membered & the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg n) = ( rng ( abs (x - y)))

    proof

      set SA = the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg n);

      now

        let t be object;

        assume t in SA;

        then ex i be Element of ( Seg n) st t = |.((x . i) - (y . i)).|;

        hence t is real;

      end;

      hence SA is real-membered by MEMBERED:def 3;

      

       A1: SA c= ( rng ( abs (x - y)))

      proof

        let t be object;

        assume t in SA;

        then

        consider i be Element of ( Seg n) such that

         A2: t = |.((x . i) - (y . i)).|;

        

         A3: t = |.((x - y) . i).| & ( dom ( abs (x - y))) = ( Seg n) by A2, RVSUM_1: 27, FINSEQ_2: 124;

        reconsider f = (x - y) as complex-valued Function;

        t = ( |.f.| . i) by A3, VALUED_1: 18;

        hence t in ( rng ( abs (x - y))) by A3, FUNCT_1:def 3;

      end;

      for t be object st t in ( rng ( abs (x - y))) holds t in SA

      proof

        let t be object;

        assume t in ( rng ( abs (x - y)));

        then

        consider i be object such that

         A4: i in ( dom ( abs (x - y))) and

         A5: t = (( abs (x - y)) . i) by FUNCT_1:def 3;

        

         A6: i is Element of ( Seg n) by A4, FINSEQ_2: 124;

        reconsider f = (x - y) as complex-valued Function;

        t = |.((x - y) . i).| & ((x - y) . i) = ((x . i) - (y . i)) by A4, A5, VALUED_1: 18, RVSUM_1: 27;

        hence thesis by A6;

      end;

      then ( rng ( abs (x - y))) c= SA;

      hence thesis by A1;

    end;

    theorem :: SRINGS_5:90

    

     Th57: ex S be ext-real-membered set st S = the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg n) & (( Infty_dist n) . (x,y)) = ( sup S)

    proof

      set S = the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg n);

      

       A1: S is real-membered & S = ( rng ( abs (x - y))) by Th56;

      then

      reconsider S1 = S as ext-real-membered set;

      take S1;

      thus thesis by A1, Def7;

    end;

    theorem :: SRINGS_5:91

    

     Th58: (( Infty_dist n) . (x,y)) = (( abs (x - y)) . ( max_diff_index (x,y)))

    proof

      ( max_diff_index (x,y)) in ( dom x) by EUCLID_9: 4;

      then

       A1: ( max_diff_index (x,y)) in ( Seg n) by FINSEQ_2: 124;

      ( dom ( abs (x - y))) = ( Seg n) by FINSEQ_2: 124;

      then

       A2: (( abs (x - y)) . ( max_diff_index (x,y))) in ( rng ( abs (x - y))) by A1, FUNCT_1:def 3;

      ( sup ( rng ( abs (x - y)))) is UpperBound of ( rng ( abs (x - y))) by XXREAL_2:def 3;

      then (( abs (x - y)) . ( max_diff_index (x,y))) <= ( sup ( rng ( abs (x - y)))) by A2, XXREAL_2:def 1;

      then

       A3: (( abs (x - y)) . ( max_diff_index (x,y))) <= (( Infty_dist n) . (x,y)) by Def7;

      (( Infty_dist n) . (x,y)) <= (( abs (x - y)) . ( max_diff_index (x,y)))

      proof

        now

          let t be ExtReal;

          assume t in ( rng ( abs (x - y)));

          then ex u be object st u in ( dom ( abs (x - y))) & t = (( abs (x - y)) . u) by FUNCT_1:def 3;

          hence t <= (( abs (x - y)) . ( max_diff_index (x,y))) by EUCLID_9: 5;

        end;

        then (( abs (x - y)) . ( max_diff_index (x,y))) is UpperBound of ( rng ( abs (x - y))) by XXREAL_2:def 1;

        then ( sup ( rng ( abs (x - y)))) <= (( abs (x - y)) . ( max_diff_index (x,y))) by XXREAL_2:def 3;

        hence thesis by Def7;

      end;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: SRINGS_5:92

    

     Th59: (( Infty_dist n) . (x,y)) = 0 iff x = y

    proof

      consider S be ext-real-membered set such that

       A1: S = the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg n) and

       A2: (( Infty_dist n) . (x,y)) = ( sup S) by Th57;

      hereby

        assume

         A3: (( Infty_dist n) . (x,y)) = 0 ;

        

         A4: ( dom x) = ( Seg n) & ( dom y) = ( Seg n) by FINSEQ_2: 124;

        now

          let i be object;

          assume

           A5: i in ( dom x);

          then

           A6: i in ( Seg n) by FINSEQ_2: 124;

          set AXY = (( abs (x - y)) . i);

          reconsider f = (x - y) as complex-valued Function;

          

           A7: AXY = |.((x - y) . i).| by VALUED_1: 18;

          then

           A8: 0 <= AXY by COMPLEX1: 46;

          AXY = |.((x . i) - (y . i)).| by A5, A7, RVSUM_1: 27;

          then AXY in S by A1, A6;

          then (( abs (x - y)) . i) = 0 by A8, A3, A2, XXREAL_2: 4;

          then

           A9: ((x - y) . i) = 0 by A7, ABSVALUE: 2;

          reconsider rx = x, ry = y as Element of (n -tuples_on REAL );

          ((rx - ry) . i) = ((rx . i) - (ry . i)) by A5, RVSUM_1: 27;

          hence (x . i) = (y . i) by A9;

        end;

        hence x = y by A4, FUNCT_1:def 11;

      end;

      assume

       A10: x = y;

      S = { 0 }

      proof

        for t be object st t in S holds t in { 0 }

        proof

          let t be object;

          assume t in S;

          then

          consider i be Element of ( Seg n) such that

           A11: t = |.((x . i) - (y . i)).| by A1;

          t = 0 by A11, A10, ABSVALUE: 2;

          hence t in { 0 } by TARSKI:def 1;

        end;

        then

         A12: S c= { 0 };

        for t be object st t in { 0 } holds t in S

        proof

          let t be object;

          assume

           A13: t in { 0 };

          1 <= 1 & 1 <= n by NAT_1: 53;

          then 1 is Element of ( Seg n) by FINSEQ_1: 1;

          then |.((x . 1) - (y . 1)).| in S & |.((x . 1) - (y . 1)).| = 0 by A10, ABSVALUE: 2, A1;

          hence t in S by A13, TARSKI:def 1;

        end;

        then { 0 } c= S;

        hence thesis by A12;

      end;

      hence (( Infty_dist n) . (x,y)) = 0 by A2, XXREAL_2: 11;

    end;

    theorem :: SRINGS_5:93

    

     Th60: (( Infty_dist n) . (x,y)) = (( Infty_dist n) . (y,x))

    proof

      (( Infty_dist n) . (x,y)) = ( sup ( rng ( abs (x - y)))) & (( Infty_dist n) . (y,x)) = ( sup ( rng ( abs (y - x)))) by Def7;

      hence (( Infty_dist n) . (x,y)) = (( Infty_dist n) . (y,x)) by Th1;

    end;

    theorem :: SRINGS_5:94

    

     Th61: (( Infty_dist n) . (x,y)) <= ((( Infty_dist n) . (x,z)) + (( Infty_dist n) . (z,y)))

    proof

      (( Infty_dist n) . (x,y)) in REAL & (( Infty_dist n) . (x,z)) in REAL & (( Infty_dist n) . (z,y)) in REAL ;

      then

      reconsider sxy = ( sup ( rng ( abs (x - y)))), sxz = ( sup ( rng ( abs (x - z)))), szy = ( sup ( rng ( abs (z - y)))) as Real by Def7;

      sxy <= (sxz + szy)

      proof

        for er be ExtReal st er in ( rng ( abs (x - y))) holds er <= (sxz + szy)

        proof

          let er be ExtReal;

          assume er in ( rng ( abs (x - y)));

          then

          consider i be object such that

           A1: i in ( dom ( abs (x - y))) and

           A2: er = (( abs (x - y)) . i) by FUNCT_1:def 3;

          (( abs (x - y)) . i) <= (sxz + szy)

          proof

            

             A3: (( abs (x - y)) . i) <= ((( abs (x - z)) . i) + (( abs (z - y)) . i))

            proof

              reconsider fxy = (x - y), fxz = (x - z), fzy = (z - y) as complex-valued Function;

              

               A4: (( abs fxy) . i) = |.((x - y) . i).| & (( abs fxz) . i) = |.((x - z) . i).| & (( abs fzy) . i) = |.((z - y) . i).| by VALUED_1: 18;

               |.((x - y) . i).| <= ( |.((x - z) . i).| + |.((z - y) . i).|)

              proof

                

                 A5: |.((x - y) . i).| = |.((x . i) - (y . i)).| & |.((x - z) . i).| = |.((x . i) - (z . i)).| & |.((z - y) . i).| = |.((z . i) - (y . i)).| by A1, RVSUM_1: 27;

                 |.(((x . i) - (z . i)) + ((z . i) - (y . i))).| <= ( |.((x . i) - (z . i)).| + |.((z . i) - (y . i)).|) by COMPLEX1: 56;

                hence thesis by A5;

              end;

              hence thesis by A4;

            end;

            ((( abs (x - z)) . i) + (( abs (z - y)) . i)) <= (sxz + szy)

            proof

              

               A6: ( dom ( abs (x - z))) = ( Seg n) & ( dom ( abs (z - y))) = ( Seg n) & ( dom ( abs (x - y))) = ( Seg n) by FINSEQ_2: 124;

              (( abs (x - z)) . i) in ( rng ( abs (x - z))) & (( abs (z - y)) . i) in ( rng ( abs (z - y))) by A6, A1, FUNCT_1:def 3;

              then

               A7: (( abs (x - z)) . i) <= ( sup ( rng ( abs (x - z)))) & (( abs (z - y)) . i) <= ( sup ( rng ( abs (z - y)))) by XXREAL_2: 4;

              (( abs (x - z)) . i) in REAL & (( abs (z - y)) . i) in REAL by A1, A6, Th2;

              then ((( abs (x - z)) . i) + (( abs (z - y)) . i)) <= (( sup ( rng ( abs (x - z)))) + ( sup ( rng ( abs (z - y))))) by Th3, A7;

              hence thesis by XXREAL_3:def 2;

            end;

            hence thesis by A3, XXREAL_0: 2;

          end;

          hence thesis by A2;

        end;

        then (sxz + szy) is UpperBound of ( rng ( abs (x - y))) by XXREAL_2:def 1;

        hence thesis by XXREAL_2:def 3;

      end;

      then sxy <= (sxz + (( Infty_dist n) . (z,y))) by Def7;

      then sxy <= ((( Infty_dist n) . (x,z)) + (( Infty_dist n) . (z,y))) by Def7;

      hence thesis by Def7;

    end;

    theorem :: SRINGS_5:95

    

     Th62: ( Infty_dist n) is_metric_of ( REAL n)

    proof

      for x,y,z be Element of ( REAL n) holds ((( Infty_dist n) . (x,y)) = 0 iff x = y) & ((( Infty_dist n) . (x,y)) = (( Infty_dist n) . (y,x))) & ((( Infty_dist n) . (x,z)) <= ((( Infty_dist n) . (x,y)) + (( Infty_dist n) . (y,z)))) by Th59, Th60, Th61;

      hence thesis by PCOMPS_1:def 6;

    end;

    theorem :: SRINGS_5:96

    

     Th63: (( Pitag_dist 2) . ( |[ 0 , 0 ]|, |[1, 1]|)) = ( sqrt 2)

    proof

      reconsider A = |[ 0 , 0 ]|, B = |[1, 1]| as Element of ( REAL 2) by EUCLID: 22;

      ( |[ 0 , 0 ]| `1 ) = 0 & ( |[ 0 , 0 ]| `2 ) = 0 & ( |[1, 1]| `1 ) = 1 & ( |[1, 1]| `2 ) = 1 by EUCLID: 52;

      then

       A1: ((A - B) . 1) = ( 0 - 1) & ((A - B) . 2) = ( 0 - 1) by RVSUM_1: 27;

      reconsider f = (A - B) as FinSequence of REAL ;

      ( len f) = ( len (A - B)) & ( len (A - B)) = 2 by FINSEQ_2: 132;

      then

       A2: |.(A - B).| = ( sqrt ((( - 1) ^2 ) + (( - 1) ^2 ))) by A1, EUCLID_3: 22;

      (( - 1) ^2 ) = (1 ^2 ) by SQUARE_1: 3

      .= (1 * 1) by SQUARE_1:def 1

      .= 1;

      hence thesis by A2, EUCLID:def 6;

    end;

    theorem :: SRINGS_5:97

    

     Th64: (( Infty_dist 2) . ( |[ 0 , 0 ]|, |[1, 1]|)) = 1

    proof

      2 is non zero Nat & |[ 0 , 0 ]| is Element of ( REAL 2) & |[1, 1]| is Element of ( REAL 2) by EUCLID: 22;

      then

      consider S be ext-real-membered set such that

       A1: S = the set of all |.(( |[ 0 , 0 ]| . i) - ( |[1, 1]| . i)).| where i be Element of ( Seg 2) and

       A2: (( Infty_dist 2) . ( |[ 0 , 0 ]|, |[1, 1]|)) = ( sup S) by Th57;

      S = { |.( 0 - 1).|}

      proof

        for t be object st t in S holds t in { |.( 0 - 1).|}

        proof

          let t be object;

          assume t in S;

          then

          consider i be Element of ( Seg 2) such that

           A3: t = |.(( |[ 0 , 0 ]| . i) - ( |[1, 1]| . i)).| by A1;

          per cases by FINSEQ_1: 2, TARSKI:def 2;

            suppose

             A4: i = 1;

            ( |[ 0 , 0 ]| . 1) = 0 & ( |[1, 1]| . 1) = 1 by FINSEQ_1: 44;

            hence thesis by TARSKI:def 1, A4, A3;

          end;

            suppose

             A5: i = 2;

            ( |[ 0 , 0 ]| . 2) = 0 & ( |[1, 1]| . 2) = 1 by FINSEQ_1: 44;

            hence thesis by TARSKI:def 1, A5, A3;

          end;

        end;

        then

         A6: S c= { |.( 0 - 1).|};

         { |.( 0 - 1).|} c= S

        proof

          

           A7: ( |[ 0 , 0 ]| . 1) = 0 & ( |[1, 1]| . 1) = 1 by FINSEQ_1: 44;

          1 in ( Seg 2);

          then |.(( |[ 0 , 0 ]| . 1) - ( |[1, 1]| . 1)).| in S by A1;

          hence thesis by A7, TARSKI:def 1;

        end;

        hence thesis by A6;

      end;

      then S = { |.( - 1).|} & |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1;

      hence thesis by A2, XXREAL_2: 11;

    end;

    theorem :: SRINGS_5:98

    

     Th65: for x,y be Element of ( REAL 1) holds (( Infty_dist 1) . (x,y)) = |.((x . 1) - (y . 1)).|

    proof

      let x,y be Element of ( REAL 1);

      consider S be ext-real-membered set such that

       A1: S = the set of all |.((x . i) - (y . i)).| where i be Element of ( Seg 1) and

       A2: (( Infty_dist 1) . (x,y)) = ( sup S) by Th57;

      S = { |.((x . 1) - (y . 1)).|}

      proof

        for t be object st t in S holds t in { |.((x . 1) - (y . 1)).|}

        proof

          let t be object;

          assume t in S;

          then

          consider i be Element of ( Seg 1) such that

           A3: t = |.((x . i) - (y . i)).| by A1;

          i = 1 by TARSKI:def 1, FINSEQ_1: 2;

          hence thesis by A3, TARSKI:def 1;

        end;

        then

         A4: S c= { |.((x . 1) - (y . 1)).|};

        for t be object st t in { |.((x . 1) - (y . 1)).|} holds t in S

        proof

          let t be object;

          assume t in { |.((x . 1) - (y . 1)).|};

          then

           A5: t = |.((x . 1) - (y . 1)).| by TARSKI:def 1;

          1 is Element of ( Seg 1) by TARSKI:def 1, FINSEQ_1: 2;

          hence thesis by A5, A1;

        end;

        then { |.((x . 1) - (y . 1)).|} c= S;

        hence thesis by A4;

      end;

      hence thesis by A2, XXREAL_2: 11;

    end;

    theorem :: SRINGS_5:99

    

     Th66: for x,y be Element of ( REAL 1) holds (( Pitag_dist 1) . (x,y)) = |.((x . 1) - (y . 1)).|

    proof

      let x,y be Element of ( REAL 1);

      

       A1: (( Pitag_dist 1) . (x,y)) = |.(x - y).| by EUCLID:def 6;

      reconsider f = (x - y) as Element of ( TOP-REAL 1) by EUCLID: 22;

      consider r be Real such that

       A2: f = <*r*> by JORDAN2B: 20;

      ( sqr (x - y)) = <*(r ^2 )*> by A2, RVSUM_1: 55;

      then ( Sum ( sqr (x - y))) = (r ^2 ) by RVSUM_1: 73;

      then

       A3: ( sqrt ( Sum ( sqr (x - y)))) = |.r.| by COMPLEX1: 72;

      (f . 1) = ((x - y) . 1) = ((x . 1) - (y . 1)) by RVSUM_1: 27;

      hence thesis by A1, A3, A2, FINSEQ_1:def 8;

    end;

    theorem :: SRINGS_5:100

    ( Pitag_dist 1) = ( Infty_dist 1)

    proof

      now

        let x,y be set;

        assume x in ( REAL 1) & y in ( REAL 1);

        then

        reconsider x1 = x, y1 = y as Element of ( REAL 1);

        

        thus (( Pitag_dist 1) . (x,y)) = |.((x1 . 1) - (y1 . 1)).| by Th66

        .= (( Infty_dist 1) . (x,y)) by Th65;

      end;

      hence thesis by BINOP_1:def 21;

    end;

    theorem :: SRINGS_5:101

    ( Pitag_dist 2) <> ( Infty_dist 2)

    proof

      set x = |[ 0 , 0 ]|, y = |[1, 1]|;

      now

        take x, y;

        x is Element of ( REAL 2) & y is Element of ( REAL 2) by EUCLID: 22;

        hence x in ( REAL 2) & y in ( REAL 2);

        thus (( Pitag_dist 2) . (x,y)) <> (( Infty_dist 2) . (x,y)) by Th63, Th64, SQUARE_1: 19;

      end;

      hence thesis;

    end;

    definition

      let n be non zero Nat;

      :: SRINGS_5:def21

      func EMINFTY n -> strict MetrSpace equals MetrStruct (# ( REAL n), ( Infty_dist n) #);

      coherence

      proof

        ( SpaceMetr (( REAL n),( Infty_dist n))) = MetrStruct (# ( REAL n), ( Infty_dist n) #) by Th62, PCOMPS_1:def 7;

        hence thesis;

      end;

    end

    registration

      let n be non zero Nat;

      cluster ( EMINFTY n) -> non empty;

      coherence ;

    end

    definition

      let n be non zero Nat;

      :: SRINGS_5:def22

      func TOP-REAL-INFTY n -> strict RLTopStruct means

      : Def8: the TopStruct of it = ( TopSpaceMetr ( EMINFTY n)) & the RLSStruct of it = ( RealVectSpace ( Seg n));

      existence

      proof

        set V = ( RealVectSpace ( Seg n)), T = ( TopSpaceMetr ( EMINFTY n));

        the topology of T c= ( bool the carrier of V)

        proof

          let t be object;

          assume t in the topology of T;

          then t in ( bool ( REAL n)) & ( REAL n) = ( Funcs (( Seg n), REAL )) by FINSEQ_2: 93;

          hence t in ( bool the carrier of V);

        end;

        then

        reconsider t = the topology of T as Subset-Family of the carrier of V;

        take S = RLTopStruct (# the carrier of V, the ZeroF of V, the addF of V, the Mult of V, t #);

        thus the TopStruct of S = ( TopSpaceMetr ( EMINFTY n)) by FINSEQ_2: 93;

        thus the RLSStruct of S = ( RealVectSpace ( Seg n));

      end;

      uniqueness ;

    end

    theorem :: SRINGS_5:102

     the RLSStruct of ( TOP-REAL n) = the RLSStruct of ( TOP-REAL-INFTY n)

    proof

       the RLSStruct of ( TOP-REAL n) = ( RealVectSpace ( Seg n)) by EUCLID:def 8;

      hence thesis by Def8;

    end;

    registration

      let n be non zero Nat;

      cluster ( TOP-REAL-INFTY n) -> non empty;

      coherence

      proof

         the TopStruct of ( TOP-REAL-INFTY n) = ( TopSpaceMetr ( EMINFTY n)) by Def8;

        hence thesis;

      end;

    end

    theorem :: SRINGS_5:103

    for x be Element of ( REAL 0 ) holds ( Intervals (x,r)) is empty & ( product ( Intervals (x,r))) = { {} } by CARD_3: 10;

    theorem :: SRINGS_5:104

    

     Th67: r <= 0 implies ( product ( Intervals (x,r))) is empty

    proof

      assume

       A1: r <= 0 ;

      assume ( product ( Intervals (x,r))) is non empty;

      then

      consider t be object such that

       A2: t in ( product ( Intervals (x,r)));

      consider g be Function such that g = t and ( dom g) = ( dom ( Intervals (x,r))) and

       A3: for y be object st y in ( dom ( Intervals (x,r))) holds (g . y) in (( Intervals (x,r)) . y) by A2, CARD_3:def 5;

      

       A4: ( dom x) = ( Seg n) by FINSEQ_2: 124;

      then

       A5: ( dom ( Intervals (x,r))) = ( Seg n) by EUCLID_9:def 3;

      

       A6: n = 1 or n > 1 by NAT_1: 53;

      then 1 in ( dom ( Intervals (x,r))) by A5;

      then (g . 1) in (( Intervals (x,r)) . 1) & 1 in ( dom x) by A3, A4, A6;

      then ].((x . 1) - r), ((x . 1) + r).[ is non empty by EUCLID_9:def 3;

      hence contradiction by A1;

    end;

    reserve p for Element of ( EMINFTY n);

    definition

      let n be non zero Nat, p be Element of ( EMINFTY n);

      :: SRINGS_5:def23

      func @ p -> Element of ( REAL n) equals p;

      coherence ;

    end

    theorem :: SRINGS_5:105

    

     Th68: ( Ball (p,r)) = ( product ( Intervals (( @ p),r)))

    proof

      consider x be Element of ( REAL n) such that

       A1: ( @ p) = x;

      per cases ;

        suppose r <= 0 ;

        then ( Ball (p,r)) = {} & ( product ( Intervals (x,r))) = {} by Th67, TBSP_1: 12;

        hence thesis by A1;

      end;

        suppose

         A2: r > 0 ;

        

         A3: { q where q be Element of ( EMINFTY n) : ( dist (p,q)) < r } c= ( product ( Intervals (x,r)))

        proof

          let t be object;

          assume t in { q where q be Element of ( EMINFTY n) : ( dist (p,q)) < r };

          then

          consider q be Element of ( EMINFTY n) such that

           A4: t = q and

           A5: ( dist (p,q)) < r;

          reconsider pr = p, qr = q as Element of ( REAL n);

          consider S be ext-real-membered set such that

           A6: S = the set of all |.((pr . i) - (qr . i)).| where i be Element of ( Seg n) and

           A7: (( Infty_dist n) . (pr,qr)) = ( sup S) by Th57;

          (( Infty_dist n) . (p,q)) in REAL by BINOP_1: 17;

          then

          reconsider s = (( Infty_dist n) . (p,q)) as Real;

          reconsider f = ( Intervals (x,r)) as Function;

          now

            

             A8: ( dom f) = ( dom x) by EUCLID_9:def 3

            .= ( Seg n) by FINSEQ_1: 89;

            hence ( dom qr) = ( dom f) by FINSEQ_1: 89;

            thus for y be object st y in ( dom f) holds (qr . y) in (f . y)

            proof

              let y be object;

              assume

               A9: y in ( dom f);

              then

               A10: y in ( dom x) by A8, FINSEQ_1: 89;

              reconsider y1 = y as Element of ( Seg n) by A9, A8;

               |.((pr . y1) - (qr . y1)).| in S by A6;

              then |.((pr . y1) - (qr . y1)).| <= ( sup S) & ( sup S) < r by A7, A5, XXREAL_2: 4;

              then

               A11: |.((x . y) - (qr . y)).| < r by A1, XXREAL_0: 2;

              ((x . y) - r) < (qr . y) & (qr . y) < ((x . y) + r)

              proof

                per cases ;

                  suppose

                   A12: ((x . y) - (qr . y)) >= 0 ;

                  then ((x . y) - (qr . y)) < r by A11, COMPLEX1: 43;

                  then (((x . y) - (qr . y)) + (qr . y)) < ((qr . y) + r) by XREAL_1: 8;

                  then ((x . y) - r) < (((qr . y) + r) - r) by XREAL_1: 8;

                  hence ((x . y) - r) < (qr . y);

                  ( 0 + (qr . y)) <= (((x . y) - (qr . y)) + (qr . y)) by A12, XREAL_1: 7;

                  hence thesis by A2, XREAL_1: 8;

                end;

                  suppose

                   A13: ((x . y) - (qr . y)) < 0 ;

                  then (((x . y) - (qr . y)) + (qr . y)) < ( 0 + (qr . y)) by XREAL_1: 8;

                  then ((x . y) - r) < ((qr . y) - 0 ) by A2, XREAL_1: 15;

                  hence ((x . y) - r) < (qr . y);

                   |.((x . y) - (qr . y)).| = ( - ((x . y) - (qr . y))) by A13, COMPLEX1: 70

                  .= ((qr . y) - (x . y));

                  then (((qr . y) - (x . y)) + (x . y)) < (r + (x . y)) by A11, XREAL_1: 8;

                  hence (qr . y) < ((x . y) + r);

                end;

              end;

              then (qr . y) in ].((x . y) - r), ((x . y) + r).[ by XXREAL_1: 4;

              hence (qr . y) in (f . y) by A10, EUCLID_9:def 3;

            end;

          end;

          hence thesis by A4, CARD_3: 9;

        end;

        ( product ( Intervals (x,r))) c= { q where q be Element of ( EMINFTY n) : ( dist (p,q)) < r }

        proof

          let t be object;

          assume t in ( product ( Intervals (x,r)));

          then

          consider g be Function such that

           A14: t = g and

           A15: ( dom g) = ( dom ( Intervals (x,r))) and

           A16: for y be object st y in ( dom ( Intervals (x,r))) holds (g . y) in (( Intervals (x,r)) . y) by CARD_3:def 5;

          

           A17: ( dom ( Intervals (x,r))) = ( dom x) by EUCLID_9:def 3

          .= ( Seg n) by FINSEQ_1: 89;

          ( rng g) c= REAL

          proof

            let u be object;

            assume u in ( rng g);

            then

            consider t be object such that

             A18: t in ( dom g) and

             A19: u = (g . t) by FUNCT_1:def 3;

            

             A20: u in (( Intervals (x,r)) . t) by A18, A19, A15, A16;

            t in ( dom x) by A18, A17, A15, FINSEQ_1: 89;

            then u in ].((x . t) - r), ((x . t) + r).[ by A20, EUCLID_9:def 3;

            hence thesis;

          end;

          then g in ( Funcs (( Seg n), REAL )) by A17, A15, FUNCT_2:def 2;

          then

          reconsider g0 = g as Element of ( EMINFTY n) by FINSEQ_2: 93;

          ( dist (p,g0)) < r

          proof

            reconsider p1 = p, g1 = g0 as Element of ( REAL n);

            consider S be ext-real-membered set such that S = the set of all |.((p1 . i) - (g1 . i)).| where i be Element of ( Seg n) and

             A21: (( Infty_dist n) . (p1,g1)) = ( sup S) by Th57;

            ( sup S) < r

            proof

              assume

               A22: r <= ( sup S);

              set md = ( max_diff_index (p1,g1));

              

               A23: r <= (( abs (p1 - g1)) . md) by A22, A21, Th58;

              

               A24: md in ( dom x) by A1, EUCLID_9: 4;

              then md in ( dom ( Intervals (x,r))) by EUCLID_9:def 3;

              then (g1 . md) in (( Intervals (x,r)) . md) by A16;

              then

               A25: (g1 . md) in ].((p1 . md) - r), ((p1 . md) + r).[ by A24, A1, EUCLID_9:def 3;

              

               A26: ((p1 . md) - r) < (g1 . md) & (g1 . md) < ((p1 . md) + r) by A25, XXREAL_1: 4;

              (((p1 . md) - r) + r) < ((g1 . md) + r) by A26, XREAL_1: 8;

              then

               A27: ((p1 . md) - (g1 . md)) < (((g1 . md) + r) - (g1 . md)) by XREAL_1: 14;

              ((g1 . md) - (p1 . md)) < (((p1 . md) + r) - (p1 . md)) by A26, XREAL_1: 14;

              then

               A28: ((p1 . md) - (g1 . md)) < r & ( - ((p1 . md) - (g1 . md))) < r by A27;

              then

               A29: ((p1 - g1) . md) < r & ( - ((p1 - g1) . md)) < r by RVSUM_1: 27;

              set pg = ((p1 - g1) . md);

               |.pg.| < r

              proof

                per cases ;

                  suppose pg < 0 ;

                  then |.pg.| = ( - pg) by COMPLEX1: 70;

                  hence thesis by A28, RVSUM_1: 27;

                end;

                  suppose 0 <= pg;

                  hence thesis by A29, COMPLEX1: 43;

                end;

              end;

              hence contradiction by A23, VALUED_1: 18;

            end;

            hence thesis by A21;

          end;

          hence t in { q where q be Element of ( EMINFTY n) : ( dist (p,q)) < r } by A14;

        end;

        hence ( Ball (p,r)) = ( product ( Intervals (( @ p),r))) by A1, A3, METRIC_1:def 14;

      end;

    end;

    theorem :: SRINGS_5:106

    for e be Point of ( Euclid n) st e = p holds ( Ball (p,r)) = ( OpenHypercube (e,r))

    proof

      let e be Point of ( Euclid n);

      assume

       A1: e = p;

      ( Ball (p,r)) = ( product ( Intervals (( @ p),r))) by Th68;

      hence thesis by A1;

    end;

    registration

      let n be non zero Nat, p be Element of ( EMINFTY n), r be negative Real;

      cluster ( cl_Ball (p,r)) -> empty;

      coherence

      proof

        assume not thesis;

        then

        consider x be object such that

         A1: x in ( cl_Ball (p,r));

        reconsider x as Element of ( EMINFTY n) by A1;

        ( dist (x,p)) <= r by A1, METRIC_1: 12;

        hence contradiction by METRIC_1: 5;

      end;

    end

    theorem :: SRINGS_5:107

    

     Th69: for t be object holds t in ( cl_Ball (p,r)) iff ex f be Function st t = f & ( dom f) = ( Seg n) & for i be Nat st i in ( Seg n) holds (f . i) in [.((( @ p) . i) - r), ((( @ p) . i) + r).]

    proof

      reconsider x = ( @ p) as Element of ( REAL n);

      per cases ;

        suppose

         A1: r < 0 ;

        for t be object st ex f be Function st t = f & ( dom f) = ( Seg n) & for i be Nat st i in ( Seg n) holds (f . i) in [.((x . i) - r), ((x . i) + r).] holds t in ( cl_Ball (p,r))

        proof

          let t be object;

          given f be Function such that t = f and ( dom f) = ( Seg n) and

           A2: for i be Nat st i in ( Seg n) holds (f . i) in [.((x . i) - r), ((x . i) + r).];

          ((x . 1) + r) < (x . 1) & (x . 1) < ((x . 1) - r) by A1, XREAL_1: 30, XREAL_1: 46;

          then ((x . 1) + r) < ((x . 1) - r) by XXREAL_0: 2;

          then

           A3: [.((x . 1) - r), ((x . 1) + r).] is empty by XXREAL_1: 29;

          ( 0 + 1) < (n + 1) by XREAL_1: 6;

          then 1 <= n by NAT_1: 13;

          then 1 in ( Seg n);

          hence thesis by A3, A2;

        end;

        hence thesis by A1;

      end;

        suppose

         A4: 0 <= r;

        

         A5: for t be object st t in ( cl_Ball (p,r)) holds ex f be Function st t = f & ( dom f) = ( Seg n) & for i be Nat st i in ( Seg n) holds (f . i) in [.((x . i) - r), ((x . i) + r).]

        proof

          let t be object;

          assume

           A6: t in ( cl_Ball (p,r));

          reconsider f = t as Function by A6;

          take f;

          thus t = f;

          f is Tuple of n, REAL by A6, FINSEQ_2: 131;

          hence ( dom f) = ( Seg n) by FINSEQ_2: 124;

          hereby

            let i be Nat;

            assume

             A7: i in ( Seg n);

            reconsider fx = t as Element of ( EMINFTY n) by A6;

            

             A8: ( dist (fx,p)) <= r by A6, METRIC_1: 12;

            reconsider rfx = fx, rp = p as Element of ( REAL n);

            consider S be ext-real-membered set such that

             A9: S = the set of all |.((rfx . i) - (rp . i)).| where i be Element of ( Seg n) and

             A10: (( Infty_dist n) . (rfx,rp)) = ( sup S) by Th57;

             |.((rfx . i) - (rp . i)).| in S by A9, A7;

            then |.((rfx . i) - (rp . i)).| <= ( sup S) by XXREAL_2: 4;

            then

             A11: |.((rfx . i) - (rp . i)).| <= r by A10, A8, XXREAL_0: 2;

            set rfp = ((rfx . i) - (rp . i));

            ((x . i) - r) <= (rfx . i) & (rfx . i) <= ((x . i) + r)

            proof

              per cases ;

                suppose

                 A12: 0 <= rfp;

                then ((rfx . i) - (rp . i)) <= r by A11, COMPLEX1: 43;

                then

                 A13: (((rfx . i) - (rp . i)) + (rp . i)) <= (r + (rp . i)) by XREAL_1: 7;

                ( 0 + (rp . i)) <= (((rfx . i) - (rp . i)) + (rp . i)) by A12, XREAL_1: 7;

                then ((rp . i) - r) <= ((rfx . i) - r) & ((rfx . i) - r) <= (rfx . i) by A4, XREAL_1: 13, XREAL_1: 43;

                hence thesis by A13, XXREAL_0: 2;

              end;

                suppose

                 A14: rfp < 0 ;

                then ( - rfp) <= r by A11, COMPLEX1: 70;

                then (((rp . i) - (rfx . i)) + (rfx . i)) <= (r + (rfx . i)) by XREAL_1: 7;

                then ((rp . i) - r) <= ((r + (rfx . i)) - r) by XREAL_1: 13;

                hence ((x . i) - r) <= (rfx . i);

                (((rfx . i) - (rp . i)) + (rp . i)) < ( 0 + (rp . i)) by A14, XREAL_1: 8;

                hence thesis by A4, XREAL_1: 38;

              end;

            end;

            hence (f . i) in [.((x . i) - r), ((x . i) + r).] by XXREAL_1: 1;

          end;

        end;

        for t be object st ex f be Function st t = f & ( dom f) = ( Seg n) & for i be Nat st i in ( Seg n) holds (f . i) in [.((x . i) - r), ((x . i) + r).] holds t in ( cl_Ball (p,r))

        proof

          let t be object;

          assume

           A15: ex f be Function st t = f & ( dom f) = ( Seg n) & for i be Nat st i in ( Seg n) holds (f . i) in [.((x . i) - r), ((x . i) + r).];

          then

          consider f be Function such that

           A16: t = f and

           A17: ( dom f) = ( Seg n) and

           A18: for i be Nat st i in ( Seg n) holds (f . i) in [.((x . i) - r), ((x . i) + r).];

          ( rng f) c= REAL

          proof

            let u be object;

            assume u in ( rng f);

            then

            consider v be object such that

             A19: v in ( dom f) and

             A20: u = (f . v) by FUNCT_1:def 3;

            (f . v) in [.((x . v) - r), ((x . v) + r).] by A19, A17, A18;

            hence u in REAL by A20;

          end;

          then f in ( Funcs (( Seg n), REAL )) by A17, FUNCT_2:def 2;

          then

          reconsider q = f as Element of ( EMINFTY n) by FINSEQ_2: 93;

          ( dist (p,q)) <= r

          proof

            reconsider rp = p, rq = q as Element of ( REAL n);

            consider S be ext-real-membered set such that

             A21: S = the set of all |.((rp . i) - (rq . i)).| where i be Element of ( Seg n) and

             A22: (( Infty_dist n) . (rp,rq)) = ( sup S) by Th57;

            for e be ExtReal st e in S holds e <= r

            proof

              let e be ExtReal;

              assume e in S;

              then

              consider i be Element of ( Seg n) such that

               A23: e = |.((rp . i) - (rq . i)).| by A21;

               |.((rp . i) - (rq . i)).| <= r

              proof

                (rq . i) in [.((rp . i) - r), ((rp . i) + r).] by A16, A15;

                then

                 A24: ((rp . i) - r) <= (rq . i) & (rq . i) <= ((rp . i) + r) by XXREAL_1: 1;

                set rpq = ((rp . i) - (rq . i));

                per cases ;

                  suppose

                   A25: 0 <= rpq;

                  rpq <= r

                  proof

                    (((rp . i) - r) + r) <= ((rq . i) + r) by A24, XREAL_1: 7;

                    then ((rp . i) - (rq . i)) <= (((rq . i) + r) - (rq . i)) by XREAL_1: 13;

                    hence thesis;

                  end;

                  hence thesis by A25, COMPLEX1: 43;

                end;

                  suppose

                   A26: rpq < 0 ;

                  ( - rpq) <= r

                  proof

                    ((rq . i) - (rp . i)) <= (((rp . i) + r) - (rp . i)) by A24, XREAL_1: 13;

                    hence thesis;

                  end;

                  hence thesis by A26, COMPLEX1: 70;

                end;

              end;

              hence e <= r by A23;

            end;

            then r is UpperBound of S by XXREAL_2:def 1;

            hence thesis by A22, XXREAL_2:def 3;

          end;

          hence t in ( cl_Ball (p,r)) by A16, METRIC_1: 12;

        end;

        hence thesis by A5;

      end;

    end;

    theorem :: SRINGS_5:108

    

     Th70: for p be Point of ( TOP-REAL n), q be Element of ( EMINFTY n) st q = p holds ( cl_Ball (q,r)) = ( ClosedHypercube (p,(n |-> r)))

    proof

      let p be Point of ( TOP-REAL n), q be Element of ( EMINFTY n);

      assume

       A1: q = p;

      

       A8: ( cl_Ball (q,r)) c= ( ClosedHypercube (p,(n |-> r)))

      proof

        let x be object;

        assume x in ( cl_Ball (q,r));

        then

        consider f be Function such that

         A2: x = f and

         A3: ( dom f) = ( Seg n) and

         A4: for i be Nat st i in ( Seg n) holds (f . i) in [.((( @ q) . i) - r), ((( @ q) . i) + r).] by Th69;

        reconsider rq = ( @ q) as Element of ( REAL n);

         A5:

        now

          let i be Nat;

          assume i in ( Seg n);

          then (f . i) in [.((rq . i) - r), ((rq . i) + r).] & ((n |-> r) . i) = r by A4, FINSEQ_2: 57;

          hence (f . i) in [.((p . i) - ((n |-> r) . i)), ((p . i) + ((n |-> r) . i)).] by A1;

        end;

        ( rng f) c= REAL

        proof

          let u be object;

          assume u in ( rng f);

          then

          consider v be object such that

           A6: v in ( dom f) and

           A7: u = (f . v) by FUNCT_1:def 3;

          (f . v) in [.((rq . v) - r), ((rq . v) + r).] by A6, A3, A4;

          hence u in REAL by A7;

        end;

        then f in ( Funcs (( Seg n), REAL )) by A3, FUNCT_2:def 2;

        then f in ( REAL n) by FINSEQ_2: 93;

        then

        reconsider fx = f as Element of ( TOP-REAL n) by EUCLID: 22;

        fx in ( ClosedHypercube (p,(n |-> r))) by A5, TIETZE_2:def 2;

        hence thesis by A2;

      end;

      ( ClosedHypercube (p,(n |-> r))) c= ( cl_Ball (q,r))

      proof

        let x be object;

        assume

         A9: x in ( ClosedHypercube (p,(n |-> r)));

        then

        reconsider y = x as Element of ( TOP-REAL n);

        reconsider f = y as Function;

        now

          take f;

          thus y = f;

          y in ( TOP-REAL n);

          then y in ( REAL n) by EUCLID: 22;

          then y is Tuple of n, REAL by FINSEQ_2: 131;

          hence ( dom f) = ( Seg n) by FINSEQ_2: 124;

          hereby

            let i be Nat;

            assume i in ( Seg n);

            then (y . i) in [.((p . i) - ((n |-> r) . i)), ((p . i) + ((n |-> r) . i)).] & ((n |-> r) . i) = r by FINSEQ_2: 57, A9, TIETZE_2:def 2;

            hence (f . i) in [.((( @ q) . i) - r), ((( @ q) . i) + r).] by A1;

          end;

        end;

        hence thesis by Th69;

      end;

      hence thesis by A8;

    end;

    theorem :: SRINGS_5:109

    ( Ball (p,r)) = ( OpenHyperInterval ((( @ p) - (n |-> r)),(( @ p) + (n |-> r))))

    proof

      reconsider e = p as Point of ( Euclid n);

      ex a be Element of ( REAL n) st a = e & ( OpenHypercube (e,r)) = ( OpenHyperInterval ((a - (n |-> r)),(a + (n |-> r)))) by Th51;

      hence thesis by Th68;

    end;

    theorem :: SRINGS_5:110

    ( cl_Ball (p,r)) = ( ClosedHyperInterval ((( @ p) - (n |-> r)),(( @ p) + (n |-> r))))

    proof

      reconsider q = p as Point of ( TOP-REAL n) by EUCLID: 22;

      ex a be Element of ( REAL n) st a = p & ( ClosedHypercube (q,(n |-> r))) = ( ClosedHyperInterval ((a - (n |-> r)),(a + (n |-> r)))) by Th52;

      hence thesis by Th70;

    end;