euclid_9.miz

    begin

    reserve x,y for object,

i,n for Nat,

r,s for Real,

f1,f2 for n -element real-valued FinSequence;

    registration

      let s be Real;

      let r be non positive Real;

      cluster ].(s - r), (s + r).[ -> empty;

      coherence by XREAL_1: 6, XXREAL_1: 28;

      cluster [.(s - r), (s + r).[ -> empty;

      coherence by XREAL_1: 6, XXREAL_1: 27;

      cluster ].(s - r), (s + r).] -> empty;

      coherence by XREAL_1: 6, XXREAL_1: 26;

    end

    registration

      let s be Real;

      let r be negative Real;

      cluster [.(s - r), (s + r).] -> empty;

      coherence by XREAL_1: 6, XXREAL_1: 29;

    end

    registration

      let n;

      let f be n -element complex-valued FinSequence;

      cluster ( - f) -> n -element;

      coherence

      proof



         A1: ( dom ( - f)) = ( dom f) by VALUED_1: 8;

        ( len f) = n by CARD_1:def 7;

        hence ( len ( - f)) = n by A1, FINSEQ_3: 29;

      end;

      cluster (f " ) -> n -element;

      coherence

      proof



         A2: ( dom (f " )) = ( dom f) by VALUED_1:def 7;

        ( len f) = n by CARD_1:def 7;

        hence ( len (f " )) = n by A2, FINSEQ_3: 29;

      end;

      cluster (f ^2 ) -> n -element;

      coherence

      proof



         A3: ( dom (f ^2 )) = ( dom f) by VALUED_1: 11;

        ( len f) = n by CARD_1:def 7;

        hence ( len (f ^2 )) = n by A3, FINSEQ_3: 29;

      end;

      cluster ( abs f) -> n -element;

      coherence

      proof



         A4: ( dom ( abs f)) = ( dom f) by VALUED_1:def 11;

        ( len f) = n by CARD_1:def 7;

        hence ( len ( abs f)) = n by A4, FINSEQ_3: 29;

      end;

      let g be n -element complex-valued FinSequence;

      cluster (f + g) -> n -element;

      coherence

      proof



         A5: n in NAT by ORDINAL1:def 12;



         A6: ( dom (f + g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 1;

        ( len f) = n & ( len g) = n by CARD_1:def 7;

        then ( dom f) = ( Seg n) & ( dom g) = ( Seg n) by FINSEQ_1:def 3;

        hence ( len (f + g)) = n by A5, A6, FINSEQ_1:def 3;

      end;

      cluster (f - g) -> n -element;

      coherence ;

      cluster (f (#) g) -> n -element;

      coherence

      proof



         A7: n in NAT by ORDINAL1:def 12;



         A8: ( dom (f (#) g)) = (( dom f) /\ ( dom g)) by VALUED_1:def 4;

        ( len f) = n & ( len g) = n by CARD_1:def 7;

        then ( dom f) = ( Seg n) & ( dom g) = ( Seg n) by FINSEQ_1:def 3;

        hence ( len (f (#) g)) = n by A7, A8, FINSEQ_1:def 3;

      end;

      cluster (f /" g) -> n -element;

      coherence ;

    end

    registration

      let c be Complex, n be Nat, f be n -element complex-valued FinSequence;

      cluster (c + f) -> n -element;

      coherence

      proof



         A1: ( dom (c + f)) = ( dom f) by VALUED_1:def 2;

        ( len f) = n by CARD_1:def 7;

        hence ( len (c + f)) = n by A1, FINSEQ_3: 29;

      end;

      cluster (f - c) -> n -element;

      coherence ;

      cluster (c (#) f) -> n -element;

      coherence

      proof



         A2: ( dom (c (#) f)) = ( dom f) by VALUED_1:def 5;

        ( len f) = n by CARD_1:def 7;

        hence ( len (c (#) f)) = n by A2, FINSEQ_3: 29;

      end;

    end

    registration

      let f be real-valued Function;

      cluster {f} -> real-functions-membered;

      coherence by TARSKI:def 1;

      let g be real-valued Function;

      cluster {f, g} -> real-functions-membered;

      coherence by TARSKI:def 2;

    end

    registration

      let n, x, y;

      let f be n -element FinSequence;

      cluster (f +* (x,y)) -> n -element;

      coherence

      proof

        ( dom (f +* (x,y))) = ( dom f) by FUNCT_7: 30;



        hence ( len (f +* (x,y))) = ( len f) by FINSEQ_3: 29

        .= n by CARD_1:def 7;

      end;

    end

    theorem :: EUCLID_9:1

    for f be n -element FinSequence st f is empty holds n = 0 ;

    theorem :: EUCLID_9:2

    for f be n -element real-valued FinSequence holds f in ( REAL n)

    proof

      let f be n -element real-valued FinSequence;

      ( rng f) c= REAL ;

      then f is FinSequence of REAL by FINSEQ_1:def 4;

      then

       A1: f is Element of ( REAL * ) by FINSEQ_1:def 11;

      ( len f) = n by CARD_1:def 7;

      hence thesis by A1;

    end;

    theorem :: EUCLID_9:3



     Th3: for f,g be complex-valued Function holds ( abs (f - g)) = ( abs (g - f))

    proof

      let f,g be complex-valued Function;

      (f - g) = ( - (g - f)) by VALUED_2: 18;

      hence thesis by EUCLID: 5;

    end;

    definition

      let n, f1, f2;

      :: EUCLID_9:def1

      func max_diff_index (f1,f2) -> Nat equals the Element of (( abs (f1 - f2)) " {( sup ( rng ( abs (f1 - f2))))});

      coherence ;

      commutativity

      proof

        let i, f1, f2;

        ( abs (f1 - f2)) = ( abs (f2 - f1)) by Th3;

        hence thesis;

      end;

    end

    theorem :: EUCLID_9:4

    n <> 0 implies ( max_diff_index (f1,f2)) in ( dom f1)

    proof

      set F = ( abs (f1 - f2));

      assume n <> 0 ;

      then F is non empty;

      then ( sup ( rng F)) in ( rng F) by XXREAL_2:def 6;

      then

       A1: (F " {( sup ( rng F))}) <> {} by FUNCT_1: 72;



       A2: ( dom f1) = ( Seg n) by FINSEQ_1: 89;



       A3: ( dom ( abs (f1 - f2))) = ( Seg n) by FINSEQ_1: 89;



       A4: (F " {( sup ( rng F))}) c= ( dom F) by RELAT_1: 132;

      ( max_diff_index (f1,f2)) in (F " {( sup ( rng F))}) by A1;

      hence thesis by A4, A2, A3;

    end;

    theorem :: EUCLID_9:5



     Th5: (( abs (f1 - f2)) . x) <= (( abs (f1 - f2)) . ( max_diff_index (f1,f2)))

    proof

      set F = ( abs (f1 - f2));



       A1: ( dom F) = ( dom (f1 - f2)) by VALUED_1:def 11

      .= (( dom f1) /\ ( dom f2)) by VALUED_1: 12;

      set m = ( max_diff_index (f1,f2));



       A2: ( dom f1) = ( Seg n) & ( dom f2) = ( Seg n) by FINSEQ_1: 89;

      per cases ;

        suppose x in ( dom f1);

        then

         A3: (F . x) in ( rng F) by A2, A1, FUNCT_1:def 3;

        then ( sup ( rng F)) in ( rng F) by XXREAL_2:def 6;

        then (F " {( sup ( rng F))}) <> {} by FUNCT_1: 72;

        then (F . m) in {( sup ( rng F))} by FUNCT_1:def 7;

        then (F . m) = ( sup ( rng F)) by TARSKI:def 1;

        hence thesis by A3, XXREAL_2: 4;

      end;

        suppose not x in ( dom f1);

        then

         A4: not x in ( dom F) by A1, XBOOLE_0:def 4;

        (F . m) = |.((f1 - f2) . m).| by VALUED_1: 18;

        hence thesis by A4, FUNCT_1:def 2;

      end;

    end;

    registration

      cluster ( TopSpaceMetr ( Euclid 0 )) -> trivial;

      coherence by EUCLID: 77;

    end

    registration

      let n;

      cluster ( Euclid n) -> constituted-FinSeqs;

      coherence ;

    end

    registration

      let n;

      cluster -> REAL -valued for Point of ( Euclid n);

      coherence

      proof

        let a be Element of ( Euclid n);

        let y be object;

        assume y in ( rng a);

        hence y in REAL by XREAL_0:def 1;

      end;

    end

    registration

      let n;

      cluster -> n -element for Point of ( Euclid n);

      coherence ;

    end

    theorem :: EUCLID_9:6



     Th6: ( Family_open_set ( Euclid 0 )) = { {} , { {} }}

    proof



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

      thus thesis by A1, EUCLID: 77, YELLOW_9: 9;

    end;

    theorem :: EUCLID_9:7

    for B be Subset of ( Euclid 0 ) holds B = {} or B = { {} } by EUCLID: 77, ZFMISC_1: 33;

    reserve e,e1 for Point of ( Euclid n);

    definition

      let n, e;

      :: EUCLID_9:def2

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

      coherence ;

    end

    registration

      let n, e;

      let r be non positive Real;

      cluster ( Ball (e,r)) -> empty;

      coherence

      proof

        assume not thesis;

        then

        consider x be Point of ( Euclid n) such that

         A1: x in ( Ball (e,r));

        ( dist (x,e)) < r by A1, METRIC_1: 11;

        hence thesis by METRIC_1: 5;

      end;

    end

    registration

      let n, e;

      let r be positive Real;

      cluster ( Ball (e,r)) -> non empty;

      coherence by GOBOARD6: 1;

    end

    theorem :: EUCLID_9:8



     Th8: for p1,p2 be Point of ( TOP-REAL n) st i in ( dom p1) holds (((p1 /. i) - (p2 /. i)) ^2 ) <= ( Sum ( sqr (p1 - p2)))

    proof

      let p1,p2 be Point of ( TOP-REAL n) such that

       A1: i in ( dom p1);

      set e = ( sqr (p1 - p2));

       A2:

      now

        let i be Nat such that i in ( dom e);

        (e . i) = (((p1 - p2) . i) ^2 ) by VALUED_1: 11;

        hence 0 <= (e . i);

      end;



       A3: ( dom e) = ( dom (p1 - p2)) by VALUED_1: 11;



       A4: ( dom (p1 - p2)) = (( dom p1) /\ ( dom p2)) by VALUED_1: 12;



       A5: ( dom p1) = ( Seg n) by FINSEQ_1: 89

      .= ( dom p2) by FINSEQ_1: 89;



       A6: (p1 . i) = (p1 /. i) by A1, PARTFUN1:def 6;



       A7: (p2 . i) = (p2 /. i) by A1, A5, PARTFUN1:def 6;

      (e . i) = (((p1 - p2) . i) ^2 ) by VALUED_1: 11

      .= (((p1 /. i) - (p2 /. i)) ^2 ) by A6, A7, A1, A5, A4, VALUED_1: 13;

      hence thesis by A1, A2, A3, A5, A4, MATRPROB: 5;

    end;

    theorem :: EUCLID_9:9



     Th9: for a,o,p be Element of ( TOP-REAL n) st a in ( Ball (o,r)) holds for x be object holds |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r

    proof

      let a,o,p be Element of ( TOP-REAL n);

      assume

       A1: a in ( Ball (o,r));

      then

       A2: |.(a - o).| < r by TOPREAL9: 7;

       0 <= ( Sum ( sqr (a - o))) by RVSUM_1: 86;

      then (( sqrt ( Sum ( sqr (a - o)))) ^2 ) = ( Sum ( sqr (a - o))) by SQUARE_1:def 2;

      then

       A3: ( Sum ( sqr (a - o))) < (r ^2 ) by A2, SQUARE_1: 16;



       A4: ( sqr (a - o)) = ( sqr (o - a)) by EUCLID: 20;



       A5: r > 0 by A1;

      let x;



       A6: ( dom (a - o)) = (( dom a) /\ ( dom o)) by VALUED_1: 12;



       A7: ( dom a) = ( Seg n) & ( dom o) = ( Seg n) by FINSEQ_1: 89;

      per cases ;

        suppose

         A8: x in ( dom a);

        then

        reconsider x as Nat;



         A9: ((a - o) . x) = ((a . x) - (o . x)) by A8, A6, A7, VALUED_1: 13;



         A10: (a /. x) = (a . x) & (o /. x) = (o . x) by A8, A7, PARTFUN1:def 6;

        now

          assume ((o . x) - (a . x)) >= r;

          then

           A11: (((o . x) - (a . x)) ^2 ) >= (r ^2 ) by A5, SQUARE_1: 15;

          ( Sum ( sqr (o - a))) >= (((o /. x) - (a /. x)) ^2 ) by A8, A7, Th8;

          hence contradiction by A3, A11, A4, A10, XXREAL_0: 2;

        end;

        then

         A12: ((o . x) - r) < (a . x) by XREAL_1: 11;

        now

          assume ((a . x) - (o . x)) >= r;

          then

           A13: (((a . x) - (o . x)) ^2 ) >= (r ^2 ) by A5, SQUARE_1: 15;

          ( Sum ( sqr (a - o))) >= (((a /. x) - (o /. x)) ^2 ) by A8, Th8;

          hence contradiction by A3, A13, A10, XXREAL_0: 2;

        end;

        then (a . x) < ((o . x) + r) by XREAL_1: 19;

        hence thesis by A9, A12, RINFSUP1: 1;

      end;

        suppose

         A14: not x in ( dom a);

        then not x in ( dom ( abs (a - o))) by A6, A7, VALUED_1:def 11;

        then (( abs (a - o)) . x) = 0 by FUNCT_1:def 2;

        then

         A15: |.((a - o) . x).| = 0 by VALUED_1: 18;

        (a . x) = 0 & (o . x) = 0 by A7, A14, FUNCT_1:def 2;

        hence thesis by A15, A1;

      end;

    end;

    theorem :: EUCLID_9:10



     Th10: for a,o be Point of ( Euclid n) st a in ( Ball (o,r)) holds for x be object holds |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r

    proof

      let a,o be Point of ( Euclid n);

      reconsider a1 = a, o1 = o as Point of ( TOP-REAL n) by EUCLID: 67;



       A1: ( Ball (o,r)) = ( Ball (o1,r)) by TOPREAL9: 13;

      (a - o) = (a1 - o1);

      hence thesis by A1, Th9;

    end;

    definition

      let f be real-valued Function, r be Real;

      :: EUCLID_9:def3

      func Intervals (f,r) -> Function means

      : Def3: ( dom it ) = ( dom f) & for x be object st x in ( dom f) holds (it . x) = ].((f . x) - r), ((f . x) + r).[;

      existence

      proof

        deffunc F( object) = ].((f . $1) - r), ((f . $1) + r).[;

        ex g be Function st ( dom g) = ( dom f) & for x be object st x in ( dom f) holds (g . x) = F(x) from FUNCT_1:sch 3;

        hence thesis;

      end;

      uniqueness

      proof

        let g,h be Function such that

         A1: ( dom g) = ( dom f) and

         A2: for x be object st x in ( dom f) holds (g . x) = ].((f . x) - r), ((f . x) + r).[ and

         A3: ( dom h) = ( dom f) and

         A4: for x be object st x in ( dom f) holds (h . x) = ].((f . x) - r), ((f . x) + r).[;

        now

          let x be object;

          assume

           A5: x in ( dom g);



          hence (g . x) = ].((f . x) - r), ((f . x) + r).[ by A1, A2

          .= (h . x) by A1, A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

    end

    registration

      let r;

      cluster ( Intervals ( {} ,r)) -> empty;

      coherence

      proof

        ( dom ( Intervals ( {} ,r))) = ( dom {} ) by Def3;

        hence thesis;

      end;

    end

    registration

      let f be real-valued FinSequence;

      let r;

      cluster ( Intervals (f,r)) -> FinSequence-like;

      coherence

      proof

        take ( len f);

        ( dom ( Intervals (f,r))) = ( dom f) by Def3;

        hence thesis by FINSEQ_1:def 3;

      end;

    end

    definition

      let n, e, r;

      :: EUCLID_9:def4

      func OpenHypercube (e,r) -> Subset of ( TopSpaceMetr ( Euclid n)) equals ( product ( Intervals (e,r)));

      coherence

      proof

        set T = ( TopSpaceMetr ( Euclid n));

        set f = ( Intervals (e,r));

        ( product f) c= the carrier of T

        proof

          let x be object;

          assume x in ( product f);

          then

          consider g be Function such that

           A1: x = g and

           A2: ( dom g) = ( dom f) and

           A3: for y be object st y in ( dom f) holds (g . y) in (f . y) by CARD_3:def 5;



           A4: ( dom f) = ( dom e) by Def3;

          ( dom e) = ( Seg n) by FINSEQ_1: 89;

          then

          reconsider x as FinSequence by A1, A2, A4, FINSEQ_1:def 2;

          ( rng x) c= REAL

          proof

            let b be object;

            assume b in ( rng x);

            then

            consider a be object such that

             A5: a in ( dom x) and

             A6: (x . a) = b by FUNCT_1:def 3;



             A7: (g . a) in (f . a) by A1, A2, A3, A5;

            (f . a) = ].((e . a) - r), ((e . a) + r).[ by A1, A2, A4, A5, Def3;

            hence thesis by A1, A6, A7;

          end;

          then x is FinSequence of REAL by FINSEQ_1:def 4;

          then

           A8: x in ( REAL * ) by FINSEQ_1:def 11;

          ( len e) = n by CARD_1:def 7;

          then ( len x) = n by A1, A2, A4, FINSEQ_3: 29;

          hence thesis by A8;

        end;

        hence thesis;

      end;

    end

    theorem :: EUCLID_9:11



     Th11: 0 < r implies e in ( OpenHypercube (e,r))

    proof

      assume

       A1: 0 < r;

      set f = ( Intervals (e,r));



       A2: ( dom f) = ( dom e) by Def3;

      now

        let x be object;

        assume x in ( dom f);

        then

         A3: (f . x) = ].((e . x) - r), ((e . x) + r).[ by A2, Def3;



         A4: ((e . x) - r) < ((e . x) - 0 ) by A1, XREAL_1: 10;

        ((e . x) + 0 ) < ((e . x) + r) by A1, XREAL_1: 8;

        hence (e . x) in (f . x) by A3, A4, XXREAL_1: 4;

      end;

      hence thesis by A2, CARD_3: 9;

    end;

    registration

      let n be non zero Nat;

      let e be Point of ( Euclid n);

      let r be non positive Real;

      cluster ( OpenHypercube (e,r)) -> empty;

      coherence

      proof

        assume not thesis;

        then

        consider x be object such that

         A1: x in ( OpenHypercube (e,r));

        reconsider e1 = e as real-valued Function;

        set f = ( Intervals (e,r));



         A2: ( dom f) = ( dom e) by Def3;



         A3: ( dom e) = ( Seg n) by FINSEQ_1: 89;

        consider N be object such that

         A4: N in ( Seg n) by XBOOLE_0:def 1;

        (f . N) = ].((e1 . N) - r), ((e1 . N) + r).[ by A4, A3, Def3;

        hence thesis by A1, A2, A3, A4, CARD_3: 9;

      end;

    end

    theorem :: EUCLID_9:12



     Th12: for e be Point of ( Euclid 0 ) holds ( OpenHypercube (e,r)) = { {} } by CARD_3: 10;

    registration

      let e be Point of ( Euclid 0 );

      let r;

      cluster ( OpenHypercube (e,r)) -> non empty;

      coherence by CARD_3: 10;

    end

    registration

      let n, e;

      let r be positive Real;

      cluster ( OpenHypercube (e,r)) -> non empty;

      coherence by Th11;

    end

    theorem :: EUCLID_9:13



     Th13: r <= s implies ( OpenHypercube (e,r)) c= ( OpenHypercube (e,s))

    proof

      assume

       A1: r <= s;



       A2: ( dom ( Intervals (e,s))) = ( dom e) by Def3;



       A3: ( dom ( Intervals (e,r))) = ( dom e) by Def3;

      now

        let x be object;

        assume

         A4: x in ( dom ( Intervals (e,r)));

        reconsider u = (e . x) as Real;



         A5: (( Intervals (e,r)) . x) = ].(u - r), (u + r).[ & (( Intervals (e,s)) . x) = ].(u - s), (u + s).[ by A4, A3, Def3;

        (u - s) <= (u - r) & (u + r) <= (u + s) by A1, XREAL_1: 6, XREAL_1: 10;

        hence (( Intervals (e,r)) . x) c= (( Intervals (e,s)) . x) by A5, XXREAL_1: 46;

      end;

      hence thesis by A2, A3, CARD_3: 27;

    end;

    theorem :: EUCLID_9:14



     Th14: (n <> 0 or 0 < r) & e1 in ( OpenHypercube (e,r)) implies for x be set holds |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r

    proof

      assume that

       A1: n <> 0 or 0 < r and

       A2: e1 in ( OpenHypercube (e,r));



       A3: ( dom e1) = ( Seg n) & ( dom e) = ( Seg n) by FINSEQ_1: 89;



       A4: ( dom (e1 - e)) = (( dom e1) /\ ( dom e)) by VALUED_1: 12;

      let x be set;

      per cases ;

        suppose

         A5: x in ( dom e1);

        then

         A6: ((e1 - e) . x) = ((e1 . x) - (e . x)) by A3, A4, VALUED_1: 13;

        ( dom e) = ( dom ( Intervals (e,r))) by Def3;

        then

         A7: (e1 . x) in (( Intervals (e,r)) . x) by A5, A3, A2, CARD_3: 9;

        (( Intervals (e,r)) . x) = ].((e . x) - r), ((e . x) + r).[ by A3, A5, Def3;

        hence thesis by A6, A7, FCONT_3: 1;

      end;

        suppose

         A8: not x in ( dom e1);

        then not x in ( dom ( abs (e1 - e))) by A4, A3, VALUED_1:def 11;

        then (( abs (e1 - e)) . x) = 0 by FUNCT_1:def 2;

        then

         A9: |.((e1 - e) . x).| = 0 by VALUED_1: 18;

        (e1 . x) = 0 & (e . x) = 0 by A3, A8, FUNCT_1:def 2;

        hence thesis by A9, A1, A2;

      end;

    end;

    theorem :: EUCLID_9:15



     Th15: n <> 0 & e1 in ( OpenHypercube (e,r)) implies ( Sum ( sqr (e1 - e))) < (n * (r ^2 ))

    proof

      assume that

       A1: n <> 0 and

       A2: e1 in ( OpenHypercube (e,r));

      set R1 = ( sqr (e1 - e));

      set R2 = (n |-> (r ^2 ));

       A6:

      now

        let i;

        assume

         A7: i in ( Seg n);



         A8: ( dom e1) = ( Seg n) & ( dom e) = ( Seg n) by FINSEQ_1: 89;

        ( dom (e1 - e)) = (( dom e1) /\ ( dom e)) by VALUED_1: 12;

        then

         A9: ((e1 - e) . i) = ((e1 . i) - (e . i)) by A7, A8, VALUED_1: 13;



         A10: (R1 . i) = (((e1 - e) . i) ^2 ) by VALUED_1: 11;



         A11: (R2 . i) = (r ^2 ) by A7, FINSEQ_2: 57;



         A12: |.((e1 . i) - (e . i)).| < r by A1, A2, Th14;

        (((e1 - e) . i) ^2 ) = ( |.((e1 - e) . i).| ^2 ) by COMPLEX1: 75;

        hence (R1 . i) < (R2 . i) by A9, A10, A11, A12, SQUARE_1: 16;

      end;

      then

       A13: for i st i in ( Seg n) holds (R1 . i) <= (R2 . i);

      ex i st i in ( Seg n) & (R1 . i) < (R2 . i)

      proof

        consider i be object such that

         A14: i in ( Seg n) by A1, XBOOLE_0:def 1;

        reconsider i as Nat by A14;

        take i;

        thus thesis by A14, A6;

      end;

      then ( Sum R1) < ( Sum R2) by A13, RVSUM_1: 83;

      hence thesis by RVSUM_1: 80;

    end;

    theorem :: EUCLID_9:16



     Th16: n <> 0 & e1 in ( OpenHypercube (e,r)) implies ( dist (e1,e)) < (r * ( sqrt n))

    proof

      assume that

       A1: n <> 0 and

       A2: e1 in ( OpenHypercube (e,r));



       A3: ( dist (e1,e)) = |.(e1 - e).| by EUCLID:def 6;

       0 <= ( Sum ( sqr (e1 - e))) by RVSUM_1: 86;

      then

       A4: ( sqrt ( Sum ( sqr (e1 - e)))) < ( sqrt (n * (r ^2 ))) by A1, A2, Th15, SQUARE_1: 27;

       0 <= r by A1, A2;

      then ( sqrt (r ^2 )) = r by SQUARE_1: 22;

      hence thesis by A3, A4, SQUARE_1: 29;

    end;

    theorem :: EUCLID_9:17



     Th17: n <> 0 implies ( OpenHypercube (e,(r / ( sqrt n)))) c= ( Ball (e,r))

    proof

      assume

       A1: n <> 0 ;

      let x be object;

      assume

       A2: x in ( OpenHypercube (e,(r / ( sqrt n))));

      then

      reconsider x as Point of ( Euclid n);



       A3: ( dist (x,e)) < ((r / ( sqrt n)) * ( sqrt n)) by A1, A2, Th16;

      ((r / ( sqrt n)) * ( sqrt n)) = r by A1, XCMPLX_1: 87;

      hence thesis by A3, METRIC_1: 11;

    end;

    theorem :: EUCLID_9:18

    n <> 0 implies ( OpenHypercube (e,r)) c= ( Ball (e,(r * ( sqrt n))))

    proof

      assume

       A1: n <> 0 ;

      then

       A2: ( OpenHypercube (e,((r * ( sqrt n)) / ( sqrt n)))) c= ( Ball (e,(r * ( sqrt n)))) by Th17;

      ((r / ( sqrt n)) * ( sqrt n)) = r by A1, XCMPLX_1: 87;

      hence thesis by A2, XCMPLX_1: 74;

    end;

    theorem :: EUCLID_9:19



     Th19: e1 in ( Ball (e,r)) implies ex m be non zero Element of NAT st ( OpenHypercube (e1,(1 / m))) c= ( Ball (e,r))

    proof

      reconsider B = ( Ball (e,r)) as Subset of ( TopSpaceMetr ( Euclid n));

      assume

       A1: e1 in ( Ball (e,r));

      B is open by TOPMETR: 14;

      then

      consider s be Real such that

       A2: s > 0 and

       A3: ( Ball (e1,s)) c= B by A1, TOPMETR: 15;

      per cases ;

        suppose

         A4: n <> 0 ;

        then

        consider m be Nat such that

         A5: (1 / m) < (s / ( sqrt n)) and

         A6: m > 0 by A2, FRECHET: 36;

        reconsider m as non zero Element of NAT by A6, ORDINAL1:def 12;



         A7: ( OpenHypercube (e1,(s / ( sqrt n)))) c= ( Ball (e1,s)) by A4, Th17;

        ( OpenHypercube (e1,(1 / m))) c= ( OpenHypercube (e1,(s / ( sqrt n)))) by A5, Th13;

        then ( OpenHypercube (e1,(1 / m))) c= ( Ball (e1,s)) by A7;

        hence thesis by A3, XBOOLE_1: 1;

      end;

        suppose n = 0 ;

        then (( OpenHypercube (e1,(1 / 1))) = {} or ( OpenHypercube (e1,(1 / 1))) = { {} }) & ( Ball (e,r)) = { {} } by A1, EUCLID: 77, ZFMISC_1: 33;

        hence thesis;

      end;

    end;

    theorem :: EUCLID_9:20



     Th20: n <> 0 & e1 in ( OpenHypercube (e,r)) implies r > (( abs (e1 - e)) . ( max_diff_index (e1,e)))

    proof

      set d = ( max_diff_index (e1,e));

      (( abs (e1 - e)) . d) = |.((e1 - e) . d).| by VALUED_1: 18;

      hence thesis by Th14;

    end;

    theorem :: EUCLID_9:21



     Th21: ( OpenHypercube (e1,(r - (( abs (e1 - e)) . ( max_diff_index (e1,e)))))) c= ( OpenHypercube (e,r))

    proof

      set d = ( max_diff_index (e1,e));

      set F = ( abs (e1 - e));

      set s = (r - (F . d));



       A1: ( dom e1) = ( Seg n) & ( dom e) = ( Seg n) by FINSEQ_1: 89;

      let y be Point of ( TopSpaceMetr ( Euclid n));

      assume

       A2: y in ( OpenHypercube (e1,s));

      reconsider y as Point of ( Euclid n);



       A3: ( dom y) = ( dom ( Intervals (e1,s))) by A2, CARD_3: 9;



       A4: ( dom ( Intervals (e1,s))) = ( dom e1) by Def3;

      then

       A5: ( dom y) = ( dom ( Intervals (e,r))) by A1, A3, Def3;

      now

        let x be object;

        assume

         A6: x in ( dom ( Intervals (e,r)));

        then

         A7: (( Intervals (e,r)) . x) = ].((e . x) - r), ((e . x) + r).[ by A1, A3, A4, A5, Def3;



         A8: (( Intervals (e1,s)) . x) = ].((e1 . x) - s), ((e1 . x) + s).[ by A3, A4, A5, A6, Def3;

        (y . x) in (( Intervals (e1,s)) . x) by A2, A3, A5, A6, CARD_3: 9;

        then

         A9: |.((y . x) - (e1 . x)).| < s by A8, RCOMP_1: 1;

        ( dom (e1 - e)) = (( dom e1) /\ ( dom e)) by VALUED_1: 12;



        then |.((e1 . x) - (e . x)).| = |.((e1 - e) . x).| by A1, A3, A4, A5, A6, VALUED_1: 13

        .= (( abs (e1 - e)) . x) by VALUED_1: 18;

        then

         A10: ( |.((y . x) - (e1 . x)).| + |.((e1 . x) - (e . x)).|) < (s + (F . d)) by A9, Th5, XREAL_1: 8;

         |.((y . x) - (e . x)).| <= ( |.((y . x) - (e1 . x)).| + |.((e1 . x) - (e . x)).|) by COMPLEX1: 63;

        then |.((y . x) - (e . x)).| < r by A10, XXREAL_0: 2;

        hence (y . x) in (( Intervals (e,r)) . x) by A7, RCOMP_1: 1;

      end;

      hence thesis by A5, CARD_3: 9;

    end;

    theorem :: EUCLID_9:22



     Th22: ( Ball (e,r)) c= ( OpenHypercube (e,r))

    proof

      let g be object;

      assume

       A1: g in ( Ball (e,r));

      then

      reconsider g as Point of ( Euclid n);



       A2: ( dom ( Intervals (e,r))) = ( dom e) by Def3;



       A3: ( dom g) = ( Seg n) & ( dom e) = ( Seg n) by FINSEQ_1: 89;

      now

        let x be object;

        reconsider u = (e . x), v = (g . x) as Real;

        assume

         A4: x in ( dom ( Intervals (e,r)));

        then

         A5: (( Intervals (e,r)) . x) = ].(u - r), (u + r).[ by A2, Def3;

        ( dom (g - e)) = (( dom g) /\ ( dom e)) by VALUED_1: 12;

        then

         A6: ((g - e) . x) = (v - u) by A2, A3, A4, VALUED_1: 13;



         A7: v = (u + (v - u));

         |.((g - e) . x).| < r by A1, Th10;

        hence (g . x) in (( Intervals (e,r)) . x) by A6, A5, A7, FCONT_3: 3;

      end;

      hence thesis by A2, A3, CARD_3: 9;

    end;

    registration

      let n, e, r;

      cluster ( OpenHypercube (e,r)) -> open;

      coherence

      proof

        per cases ;

          suppose

           A1: n <> 0 ;

          for p be Point of ( Euclid n) st p in ( OpenHypercube (e,r)) holds ex s be Real st s > 0 & ( Ball (p,s)) c= ( OpenHypercube (e,r))

          proof

            let p be Point of ( Euclid n);

            assume

             A2: p in ( OpenHypercube (e,r));

            set d = (( abs (p - e)) . ( max_diff_index (p,e)));

            take s = (r - d);

            (r - d) > (d - d) by A1, A2, Th20, XREAL_1: 8;

            hence s > 0 ;



             A3: ( OpenHypercube (p,s)) c= ( OpenHypercube (e,r)) by Th21;

            ( Ball (p,s)) c= ( OpenHypercube (p,s)) by Th22;

            hence ( Ball (p,s)) c= ( OpenHypercube (e,r)) by A3;

          end;

          hence thesis by TOPMETR: 15;

        end;

          suppose

           A4: n = 0 ;

          then ( OpenHypercube (e,r)) = { {} } by Th12;

          then ( OpenHypercube (e,r)) in the topology of ( TopSpaceMetr ( Euclid 0 )) by Th6, TARSKI:def 2;

          hence thesis by A4, PRE_TOPC:def 2;

        end;

      end;

    end

    theorem :: EUCLID_9:23

    for V be Subset of ( TopSpaceMetr ( Euclid n)) holds V is open implies for e be Point of ( Euclid n) st e in V holds ex m be non zero Element of NAT st ( OpenHypercube (e,(1 / m))) c= V

    proof

      let V be Subset of ( TopSpaceMetr ( Euclid n));

      assume

       A1: V is open;

      let e be Point of ( Euclid n);

      assume e in V;

      then

      consider r be Real such that

       A2: r > 0 and

       A3: ( Ball (e,r)) c= V by A1, TOPMETR: 15;

      consider m be non zero Element of NAT such that

       A4: ( OpenHypercube (e,(1 / m))) c= ( Ball (e,r)) by A2, Th19, GOBOARD6: 1;

      take m;

      thus thesis by A3, A4;

    end;

    theorem :: EUCLID_9:24

    for V be Subset of ( TopSpaceMetr ( Euclid n)) st for e be Point of ( Euclid n) st e in V holds ex r be Real st r > 0 & ( OpenHypercube (e,r)) c= V holds V is open

    proof

      let V be Subset of ( TopSpaceMetr ( Euclid n));

      assume

       A1: for e be Point of ( Euclid n) st e in V holds ex r be Real st r > 0 & ( OpenHypercube (e,r)) c= V;

      for e be Point of ( Euclid n) st e in V holds ex r be Real st r > 0 & ( Ball (e,r)) c= V

      proof

        let e be Point of ( Euclid n);

        assume e in V;

        then

        consider r be Real such that

         A2: r > 0 and

         A3: ( OpenHypercube (e,r)) c= V by A1;

        ( Ball (e,r)) c= ( OpenHypercube (e,r)) by Th22;

        hence thesis by A2, A3, XBOOLE_1: 1;

      end;

      hence thesis by TOPMETR: 15;

    end;

    deffunc K( Nat, Point of ( Euclid $1)) = the set of all ( OpenHypercube ($2,(1 / m))) where m be non zero Element of NAT ;

    definition

      let n, e;

      :: EUCLID_9:def5

      func OpenHypercubes (e) -> Subset-Family of ( TopSpaceMetr ( Euclid n)) equals the set of all ( OpenHypercube (e,(1 / m))) where m be non zero Element of NAT ;

      coherence

      proof

         K(n,e) c= ( bool the carrier of ( TopSpaceMetr ( Euclid n)))

        proof

          let x be object;

          assume x in K(n,e);

          then ex m be non zero Element of NAT st x = ( OpenHypercube (e,(1 / m)));

          hence thesis by ZFMISC_1:def 1;

        end;

        hence thesis;

      end;

    end

    registration

      let n, e;

      cluster ( OpenHypercubes e) -> non empty open( @ e) -quasi_basis;

      coherence

      proof

        set T = ( TopSpaceMetr ( Euclid n));

        ( OpenHypercube (e,(1 / 1))) in ( OpenHypercubes e);

        hence ( OpenHypercubes e) is non empty;

        hereby

          let A be Subset of T;

          assume A in ( OpenHypercubes e);

          then ex m be non zero Element of NAT st A = ( OpenHypercube (e,(1 / m)));

          hence A is open;

        end;

        now

          let Y be set;

          assume Y in ( OpenHypercubes e);

          then ex m be non zero Element of NAT st Y = ( OpenHypercube (e,(1 / m)));

          hence ( @ e) in Y by Th11;

        end;

        hence ( @ e) in ( Intersect ( OpenHypercubes e)) by SETFAM_1: 43;

        let S be Subset of T such that

         A1: S is open and

         A2: ( @ e) in S;

        consider r be Real such that

         A3: r > 0 and

         A4: ( Ball (e,r)) c= S by A1, A2, TOPMETR: 15;

        consider m be non zero Element of NAT such that

         A5: ( OpenHypercube (e,(1 / m))) c= ( Ball (e,r)) by A3, Th19, GOBOARD6: 1;

        take V = ( OpenHypercube (e,(1 / m)));

        thus V in ( OpenHypercubes e);

        thus V c= S by A4, A5;

      end;

    end

     Lm1:

    now

      set J = ( {} --> R^1 );

      set C = ( Carrier J);

      set P = ( product J);

      set T = ( TopSpaceMetr ( Euclid 0 ));



       A1: the carrier of P = ( product C) by WAYBEL18:def 3;



       A2: ( product {} ) = { {} } by CARD_3: 10;



       A3: ( REAL 0 ) = {( 0. ( TOP-REAL 0 ))} by EUCLID: 77;



       A4: {the carrier of T} is Basis of T by YELLOW_9: 10;

      the carrier of T = the carrier of P by A1, A2, A3;

      then P is 1 -element;

      then {the carrier of P} is Basis of P by YELLOW_9: 10;

      hence T = P by A1, A2, A3, A4, YELLOW_9: 25;

    end;

    theorem :: EUCLID_9:25



     Th25: ( Funcs (( Seg n), REAL )) = ( product ( Carrier (( Seg n) --> R^1 )))

    proof

      set J = (( Seg n) --> R^1 );

      set C = ( Carrier J);



       A1: ( dom C) = ( Seg n) by PARTFUN1:def 2;

      thus ( Funcs (( Seg n), REAL )) c= ( product C)

      proof

        let f be object;

        assume f in ( Funcs (( Seg n), REAL ));

        then

        reconsider f as Function of ( Seg n), REAL by FUNCT_2: 66;



         A2: ( dom f) = ( Seg n) by FUNCT_2:def 1;

        now

          let x be object;

          assume

           A3: x in ( dom C);

          then

           A4: ex R be 1-sorted st R = (J . x) & (C . x) = the carrier of R by PRALG_1:def 15;

          (f . x) in REAL by A3, FUNCT_2: 5;

          hence (f . x) in (C . x) by A4, A3, FUNCOP_1: 7;

        end;

        hence thesis by A2, A1, CARD_3: 9;

      end;

      let x be object;

      assume x in ( product C);

      then

      consider g be Function such that

       A5: x = g and

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

       A7: for y be object st y in ( dom C) holds (g . y) in (C . y) by CARD_3:def 5;

      ( rng g) c= REAL

      proof

        let z be object;

        assume z in ( rng g);

        then

        consider a be object such that

         A8: a in ( dom g) and

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



         A10: ex R be 1-sorted st R = (J . a) & (C . a) = the carrier of R by A6, A8, PRALG_1:def 15;

        (J . a) = R^1 by A6, A8, FUNCOP_1: 7;

        hence thesis by A6, A7, A8, A9, A10;

      end;

      hence thesis by A1, A5, A6, FUNCT_2:def 2;

    end;

    theorem :: EUCLID_9:26



     Th26: n <> 0 implies for PP be Subset-Family of ( TopSpaceMetr ( Euclid n)) st PP = ( product_prebasis (( Seg n) --> R^1 )) holds PP is quasi_prebasis

    proof

      assume

       A1: n <> 0 ;

      set E = ( Euclid n);

      set T = ( TopSpaceMetr E);

      let PP be Subset-Family of T;

      set J = (( Seg n) --> R^1 );

      set C = ( Carrier J);

      set S = ( Seg n);

      reconsider S as non empty finite set by A1;

      assume

       A2: PP = ( product_prebasis (( Seg n) --> R^1 ));



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



       A4: ( dom C) = ( Seg n) by PARTFUN1:def 2;



       A5: ( Funcs (( Seg n), REAL )) = ( product C) by Th25;

      defpred P[ set, object] means ex e be Point of E st e = $1 & $2 = ( OpenHypercubes e);



       A6: for i be Element of T holds ex j be object st P[i, j]

      proof

        let i be Element of T;

        reconsider j = i as Point of E;

        take ( OpenHypercubes j), j;

        thus thesis;

      end;

      consider NS be ManySortedSet of T such that

       A7: for x be Point of T holds P[x, (NS . x)] from PBOOLE:sch 6( A6);

      now

        let x be Point of T;

        reconsider y = x as Point of E;

         P[y, (NS . y)] by A7;

        hence (NS . x) is Basis of x;

      end;

      then

      reconsider NS as Neighborhood_System of T by TOPGEN_2:def 3;

      take B = ( Union NS);

      let b be object;

      reconsider bb = b as set by TARSKI: 1;

      assume b in B;

      then

      consider Z be set such that

       A8: b in Z and

       A9: Z in ( rng NS) by TARSKI:def 4;

      consider x be object such that

       A10: x in ( dom NS) and

       A11: (NS . x) = Z by A9, FUNCT_1:def 3;

      reconsider x as Point of E by A10;



       A12: ( dom x) = ( Seg n) by FINSEQ_1: 89;

       P[x, (NS . x)] by A7;

      then

      consider m be non zero Element of NAT such that

       A13: b = ( OpenHypercube (x,(1 / m))) by A8, A11;

      deffunc A( object) = ( product (C +* ($1,( R^1 ].((x . $1) - (1 / m)), ((x . $1) + (1 / m)).[))));

      defpred R[ set] means not contradiction;

      set Y = { A(q) where q be Element of S : R[q] };



       A14: Y is finite from PRE_CIRC:sch 1;

      Y c= ( bool the carrier of T)

      proof

        let s be object;

        assume s in Y;

        then

        consider q be Element of S such that

         A15: s = A(q);

         A(q) c= the carrier of T

        proof

          let z be object;

          set f = (C +* (q,( R^1 ].((x . q) - (1 / m)), ((x . q) + (1 / m)).[)));

          assume z in A(q);

          then

          consider g be Function such that

           A16: z = g and

           A17: ( dom g) = ( dom f) and

           A18: for d be object st d in ( dom f) holds (g . d) in (f . d) by CARD_3:def 5;



           A19: ( dom f) = ( dom C) by FUNCT_7: 30;

          then

          reconsider g as FinSequence by A4, A17, FINSEQ_1:def 2;

          ( rng g) c= REAL

          proof

            let b be object;

            assume b in ( rng g);

            then

            consider a be object such that

             A20: a in ( dom g) and

             A21: (g . a) = b by FUNCT_1:def 3;



             A22: (g . a) in (f . a) by A17, A18, A20;

            per cases ;

              suppose a = q;

              then (f . a) = ( R^1 ].((x . q) - (1 / m)), ((x . q) + (1 / m)).[) by A17, A19, A20, FUNCT_7: 31;

              hence thesis by A21, A22;

            end;

              suppose a <> q;

              then

               A23: (f . a) = (C . a) by FUNCT_7: 32;

              ex R be 1-sorted st R = (J . a) & (C . a) = the carrier of R by A20, A17, A19, PRALG_1:def 15;

              hence thesis by A21, A22, A23, A20, A17, A19, FUNCOP_1: 7;

            end;

          end;

          then g is FinSequence of REAL by FINSEQ_1:def 4;

          then

           A24: g is Element of ( REAL * ) by FINSEQ_1:def 11;

          n in NAT by ORDINAL1:def 12;

          then ( len g) = n by A4, A17, A19, FINSEQ_1:def 3;

          hence thesis by A16, A24;

        end;

        hence thesis by A15, ZFMISC_1:def 1;

      end;

      then

      reconsider Y as Subset-Family of T;



       A25: Y c= PP

      proof

        let z be object;

        assume

         A26: z in Y;

        then

        consider i be Element of S such that

         A27: z = A(i);

        (J . i) = R^1 ;

        hence thesis by A2, A5, A26, A3, A27, WAYBEL18:def 2;

      end;

      consider N be object such that

       A28: N in S by XBOOLE_0:def 1;



       A29: A(N) in Y by A28;

      then

       A30: ( Intersect Y) = ( meet Y) by SETFAM_1:def 9;



       A31: ( dom ( Intervals (x,(1 / m)))) = ( dom x) by Def3;

       A32:

      now

        let i be Element of S;

        set f = (C +* (i,( R^1 ].((x . i) - (1 / m)), ((x . i) + (1 / m)).[)));

        thus ( product ( Intervals (x,(1 / m)))) c= ( product f)

        proof

          let d be object;

          assume d in ( product ( Intervals (x,(1 / m))));

          then

          consider d1 be Function such that

           A33: d = d1 and

           A34: ( dom d1) = ( dom ( Intervals (x,(1 / m)))) and

           A35: for a be object st a in ( dom ( Intervals (x,(1 / m)))) holds (d1 . a) in (( Intervals (x,(1 / m))) . a) by CARD_3:def 5;



           A36: ( dom f) = ( dom C) by FUNCT_7: 30;

          now

            let k be object;

            assume

             A37: k in ( dom f);

            then

             A38: (( Intervals (x,(1 / m))) . k) = ].((x . k) - (1 / m)), ((x . k) + (1 / m)).[ by A36, A12, Def3;



             A39: (d1 . k) in (( Intervals (x,(1 / m))) . k) by A35, A31, A12, A36, A37;

            per cases ;

              suppose k = i;

              hence (d1 . k) in (f . k) by A38, A39, A37, A36, FUNCT_7: 31;

            end;

              suppose k <> i;

              then

               A40: (f . k) = (C . k) by FUNCT_7: 32;



               A41: ex R be 1-sorted st R = (J . k) & (C . k) = the carrier of R by A37, A36, PRALG_1:def 15;

              (d1 . k) in REAL by A38, A39;

              hence (d1 . k) in (f . k) by A40, A41, A37, A36, FUNCOP_1: 7;

            end;

          end;

          hence d in ( product f) by A33, A4, A34, A31, A12, A36, CARD_3: 9;

        end;

      end;

      bb = ( Intersect Y)

      proof

        now

          let M be set;

          assume M in Y;

          then ex i be Element of S st M = A(i);

          hence bb c= M by A13, A32;

        end;

        hence bb c= ( Intersect Y) by A30, A29, SETFAM_1: 5;

        let q be object;

        assume

         A42: q in ( Intersect Y);

        then

        reconsider q as Function;



         A43: ( dom q) = ( Seg n) by A42, FINSEQ_1: 89;

        now

          let a be object such that

           A44: a in ( dom ( Intervals (x,(1 / m))));



           A45: (( Intervals (x,(1 / m))) . a) = ].((x . a) - (1 / m)), ((x . a) + (1 / m)).[ by A44, A31, Def3;

          set f = (C +* (a,( R^1 ].((x . a) - (1 / m)), ((x . a) + (1 / m)).[)));

           A(a) in Y by A44, A31, A12;

          then

           A46: q in A(a) by A42, SETFAM_1: 43;

          then

           A47: ( dom q) = ( dom f) by CARD_3: 9;

          then

           A48: (q . a) in (f . a) by A43, A44, A31, A12, A46, CARD_3: 9;

          ( dom f) = ( dom C) by FUNCT_7: 30;

          hence (q . a) in (( Intervals (x,(1 / m))) . a) by A45, A48, A43, A44, A31, A12, A47, FUNCT_7: 31;

        end;

        hence thesis by A13, A43, A31, A12, CARD_3: 9;

      end;

      hence thesis by A25, A14, CANTOR_1:def 3;

    end;

    theorem :: EUCLID_9:27



     Th27: for PP be Subset-Family of ( TopSpaceMetr ( Euclid n)) st PP = ( product_prebasis (( Seg n) --> R^1 )) holds PP is open

    proof

      let PP be Subset-Family of ( TopSpaceMetr ( Euclid n));

      set J = (( Seg n) --> R^1 );

      set C = ( Carrier J);

      set T = ( TopSpaceMetr ( Euclid n));

      set E = ( Euclid n);

      assume

       A1: PP = ( product_prebasis (( Seg n) --> R^1 ));

      let x be Subset of T;

      assume x in PP;

      then

      consider i be set, R be TopStruct, V be Subset of R such that

       A2: i in ( Seg n) and

       A3: V is open and

       A4: R = (J . i) and

       A5: x = ( product (C +* (i,V))) by A1, WAYBEL18:def 2;



       A6: ( dom C) = ( Seg n) by PARTFUN1:def 2;

       A7:

      now

        let i be set;

        let e,y be Point of E;

        let r be Real;

        assume

         A8: y in ( Ball (e,r));

        set O = ].((e . i) - r), ((e . i) + r).[;

        set G = (C +* (i,O));



         A9: ( dom y) = ( Seg n) by FINSEQ_1: 89;



         A10: ( dom G) = ( dom C) by FUNCT_7: 30;

        now

          let a be object;

          assume

           A11: a in ( dom G);

          per cases ;

            suppose

             A12: a = i;



             A13: (y . i) = ((e . i) + ((y . i) - (e . i)));



             A14: ( dom e) = ( Seg n) by FINSEQ_1: 89;

            ( dom (y - e)) = (( dom y) /\ ( dom e)) by VALUED_1: 12;

            then

             A15: ((y - e) . i) = ((y . i) - (e . i)) by A9, A14, A11, A12, A10, VALUED_1: 13;

             |.((y - e) . i).| < r by A8, Th10;

            then (y . i) in O by A15, A13, FCONT_3: 3;

            hence (y . a) in (G . a) by A12, A10, A11, FUNCT_7: 31;

          end;

            suppose a <> i;

            then

             A16: (G . a) = (C . a) by FUNCT_7: 32;



             A17: ex R be 1-sorted st R = (J . a) & (C . a) = the carrier of R by A11, A10, PRALG_1:def 15;

            (y . a) in REAL by XREAL_0:def 1;

            hence (y . a) in (G . a) by A16, A11, A10, A17, FUNCOP_1: 7;

          end;

        end;

        hence y in ( product G) by A10, A6, A9, CARD_3: 9;

      end;

      set F = (C +* (i,V));



       A18: R = R^1 by A2, A4, FUNCOP_1: 7;

      for e be Element of E st e in x holds ex r be Real st r > 0 & ( Ball (e,r)) c= x

      proof

        let e be Element of E;

        assume

         A19: e in x;



         A20: ( dom F) = ( dom C) by FUNCT_7: 30;

        then

         A21: (e . i) in (F . i) by A2, A6, A19, A5, CARD_3: 9;



         A22: (F . i) = V by A2, A6, FUNCT_7: 31;

        then

        consider r be Real such that

         A23: r > 0 and

         A24: ].((e . i) - r), ((e . i) + r).[ c= V by A3, A18, A21, FRECHET: 8;

        take r;

        thus r > 0 by A23;

        let y be object;

        assume

         A25: y in ( Ball (e,r));

        then

        reconsider y as Point of E;

        set O = ].((e . i) - r), ((e . i) + r).[;

        set G = (C +* (i,O));



         A26: ( dom G) = ( dom C) by FUNCT_7: 30;



         A27: y in ( product G) by A25, A7;

        now

          let a be object;

          assume

           A28: a in ( dom G);

          per cases ;

            suppose a = i;

            hence (G . a) c= (F . a) by A24, A22, A26, A28, FUNCT_7: 31;

          end;

            suppose a <> i;

            then (G . a) = (C . a) & (F . a) = (C . a) by FUNCT_7: 32;

            hence (G . a) c= (F . a);

          end;

        end;

        then ( product G) c= ( product F) by A20, CARD_3: 27, FUNCT_7: 30;

        hence thesis by A27, A5;

      end;

      then x in the topology of T by PCOMPS_1:def 4;

      hence thesis by PRE_TOPC:def 2;

    end;

    theorem :: EUCLID_9:28

    ( TopSpaceMetr ( Euclid n)) = ( product (( Seg n) --> R^1 ))

    proof

      set J = (( Seg n) --> R^1 );

      per cases ;

        suppose

         A1: n = 0 ;

        then J = ( {} --> R^1 );

        hence thesis by A1, Lm1;

      end;

        suppose

         A2: n <> 0 ;



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



         A4: ( Funcs (( Seg n), REAL )) = ( product ( Carrier J)) by Th25;

        then

        reconsider PP = ( product_prebasis J) as Subset-Family of ( TopSpaceMetr ( Euclid n)) by FINSEQ_2: 93;



         A5: PP is open by Th27;

        PP is quasi_prebasis by A2, Th26;

        hence thesis by A4, A3, A5, WAYBEL18:def 3;

      end;

    end;