:: EUCLID_9 semantic presentation

begin


registration
let s be real number ;
let r be non positive real number ;
clusterK510((s - r),(s + r)) ->  empty ;
coherence
 ].(s - r),(s + r).[ is empty
proof
 s + r <= s - r by XREAL_1:6;
hence  ].(s - r),(s + r).[ is empty by XXREAL_1:28; ::_thesis: verum
end;
clusterK508((s - r),(s + r)) ->  empty ;
coherence
 [.(s - r),(s + r).[ is empty
proof
 s + r <= s - r by XREAL_1:6;
hence  [.(s - r),(s + r).[ is empty by XXREAL_1:27; ::_thesis: verum
end;
clusterK509((s - r),(s + r)) ->  empty ;
coherence
 ].(s - r),(s + r).] is empty
proof
 s + r <= s - r by XREAL_1:6;
hence  ].(s - r),(s + r).] is empty by XXREAL_1:26; ::_thesis: verum
end;
end;

registration
let s be real number ;
let r be negative real number ;
clusterK507((s - r),(s + r)) ->  empty ;
coherence
 [.(s - r),(s + r).] is empty
proof
 s + r < s - r by XREAL_1:6;
hence  [.(s - r),(s + r).] is empty by XXREAL_1:29; ::_thesis: verum
end;
end;

registration
let n be Nat;
let f be complex-valued n -element FinSequence;
cluster - f -> n -element ;
coherence
 - f is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
clusterf "  -> n -element ;
coherence
 f " is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
clusterf ^2  -> n -element ;
coherence
 f ^2 is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
cluster|.f.| -> n -element ;
coherence
 abs f is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
let g be complex-valued n -element FinSequence;
clusterf + g -> n -element ;
coherence
 f + g is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
clusterf - g -> n -element ;
coherence
 f - g is n -element ;
clusterf (#) g -> n -element ;
coherence
 f (#) g is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
clusterf /" g -> n -element ;
coherence
 f /" g is n -element ;
end;

registration
let c be complex number ;
let n be Nat;
let f be complex-valued n -element FinSequence;
clusterc + f -> n -element ;
coherence
 c + f is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
clusterf - c -> n -element ;
coherence
 f - c is n -element ;
clusterc (#) f -> n -element ;
coherence
 c (#) f is n -element
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; :: according to CARD_1:def_7 ::_thesis: verum
end;
end;

registration
let f be real-valued Function;
cluster{f} ->  real-functions-membered ;
coherence
 {f} is real-functions-membered
proof
let x be set ; :: according to VALUED_2:def_4 ::_thesis: ( not x in {f} or x is set )
thus  ( not x in {f} or x is set ) by TARSKI:def_1; ::_thesis: verum
end;
let g be real-valued Function;
cluster{f,g} ->  real-functions-membered ;
coherence
 {f,g} is real-functions-membered
proof
let x be set ; :: according to VALUED_2:def_4 ::_thesis: ( not x in {f,g} or x is set )
thus  ( not x in {f,g} or x is set ) by TARSKI:def_2; ::_thesis: verum
end;
end;

registration
let n be Nat;
let x, y be set ;
let f be n -element FinSequence;
clusterf +* (x,y) -> n -element ;
coherence
 f +* (x,y) is n -element
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 ;
:: according to CARD_1:def_7 ::_thesis: verum
end;
end;

theorem Th1: :: EUCLID_9:1
for n being Nat
for f being b1 -element FinSequence st f is empty holds
n = 0
proof
let n be Nat; ::_thesis: for f being n -element FinSequence st f is empty holds
n = 0
let f be n -element FinSequence; ::_thesis: ( f is empty implies n = 0 )
assume  f is empty ; ::_thesis: n = 0
then A1: dom f = Seg 0 ;
 len f = n by CARD_1:def_7;
hence  n = 0 by A1, FINSEQ_1:def_3; ::_thesis: verum
end;

theorem Th2: :: EUCLID_9:2
for n being Nat
for f being real-valued b1 -element FinSequence holds f in REAL n
proof
let n be Nat; ::_thesis: for f being real-valued n -element FinSequence holds f in REAL n
let f be real-valued n -element FinSequence; ::_thesis: f in REAL n
 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  f in REAL n by A1; ::_thesis: verum
end;

theorem Th3: :: EUCLID_9:3
for f, g being complex-valued Function holds abs (f - g) = abs (g - f)
proof
let f, g be complex-valued Function; ::_thesis: abs (f - g) = abs (g - f)
 f - g = - (g - f) by VALUED_2:18;
hence  abs (f - g) = abs (g - f) by EUCLID:5; ::_thesis: verum
end;

definition
let n be Nat;
let f1, f2 be real-valued n -element FinSequence;
func max_diff_index (f1,f2) ->  Nat equals :: EUCLID_9:def 1
 the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))};
coherence
 the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} is Nat ;
commutativity
 for b1 being Nat
for f1, f2 being real-valued n -element FinSequence st b1 = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds
b1 = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))}
proof
let i be Nat; ::_thesis: for f1, f2 being real-valued n -element FinSequence st i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds
i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))}
let f1, f2 be real-valued n -element FinSequence; ::_thesis: ( i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} implies i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} )
 abs (f1 - f2) = abs (f2 - f1) by Th3;
hence  ( i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} implies i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} ) ; ::_thesis: verum
end;
end;

:: deftheorem  defines max_diff_index EUCLID_9:def_1_:_
 for n being Nat
for f1, f2 being real-valued b1 -element FinSequence holds max_diff_index (f1,f2) = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))};

theorem :: EUCLID_9:4
for n being Nat
for f1, f2 being real-valued b1 -element FinSequence st n <> 0 holds
max_diff_index (f1,f2) in dom f1
proof
let n be Nat; ::_thesis: for f1, f2 being real-valued n -element FinSequence st n <> 0 holds
max_diff_index (f1,f2) in dom f1
let f1, f2 be real-valued n -element FinSequence; ::_thesis: ( n <> 0 implies max_diff_index (f1,f2) in dom f1 )
set F = abs (f1 - f2);
assume  n <> 0 ; ::_thesis: max_diff_index (f1,f2) in dom f1
then  not abs (f1 - f2) is empty by Th1;
then  sup (rng (abs (f1 - f2))) in rng (abs (f1 - f2)) by XXREAL_2:def_6;
then A1: (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} <> {} 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: (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} c= dom (abs (f1 - f2)) by RELAT_1:132;
 max_diff_index (f1,f2) in (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} by A1;
hence  max_diff_index (f1,f2) in dom f1 by A4, A2, A3; ::_thesis: verum
end;

theorem Th5: :: EUCLID_9:5
for x being set
for n being Nat
for f1, f2 being real-valued b2 -element FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
proof
let x be set ; ::_thesis: for n being Nat
for f1, f2 being real-valued b1 -element FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
let n be Nat; ::_thesis: for f1, f2 being real-valued n -element FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
let f1, f2 be real-valued n -element FinSequence; ::_thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
set F = abs (f1 - f2);
A1: dom (abs (f1 - f2)) = 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;
percases ( x in dom f1 or not x in dom f1 ) ;
suppose x in dom f1 ; ::_thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
then A3: (abs (f1 - f2)) . x in rng (abs (f1 - f2)) by A2, A1, FUNCT_1:def_3;
then  sup (rng (abs (f1 - f2))) in rng (abs (f1 - f2)) by XXREAL_2:def_6;
then  (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} <> {} by FUNCT_1:72;
then  (abs (f1 - f2)) . (max_diff_index (f1,f2)) in {(sup (rng (abs (f1 - f2))))} by FUNCT_1:def_7;
then  (abs (f1 - f2)) . (max_diff_index (f1,f2)) = sup (rng (abs (f1 - f2))) by TARSKI:def_1;
hence  (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) by A3, XXREAL_2:4; ::_thesis: verum
end;
suppose not x in dom f1 ; ::_thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
then A4: not x in dom (abs (f1 - f2)) by A1, XBOOLE_0:def_4;
 (abs (f1 - f2)) . (max_diff_index (f1,f2)) = abs ((f1 - f2) . (max_diff_index (f1,f2))) by VALUED_1:18;
hence  (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) by A4, FUNCT_1:def_2; ::_thesis: verum
end;
end;
end;

registration
cluster TopSpaceMetr (Euclid 0) ->  trivial ;
coherence
 TopSpaceMetr (Euclid 0) is trivial by EUCLID:77;
end;

registration
let n be Nat;
cluster Euclid n ->  constituted-FinSeqs ;
coherence
 Euclid n is constituted-FinSeqs
proof
let a be Element of (Euclid n); :: according to MONOID_0:def_2 ::_thesis: a is set
thus  a is set ; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster  ->  REAL -valued for Element of the carrier of (Euclid n);
coherence
 for b1 being Point of (Euclid n) holds b1 is REAL -valued
proof
let a be Element of (Euclid n); ::_thesis: a is REAL -valued
let y be set ; :: according to RELAT_1:def_19,TARSKI:def_3 ::_thesis: ( not y in rng a or y in REAL )
assume  y in rng a ; ::_thesis: y in REAL
hence  y in REAL by XREAL_0:def_1; ::_thesis: verum
end;
end;

registration
let n be Nat;
cluster  -> n -element for Element of the carrier of (Euclid n);
coherence
 for b1 being Point of (Euclid n) holds b1 is n -element ;
end;

theorem Th6: :: EUCLID_9:6
Family_open_set (Euclid 0) = {{},{{}}}
proof
A1: TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) = TopSpaceMetr (Euclid 0) by EUCLID:def_8;
thus  Family_open_set (Euclid 0) = {{},{{}}} by A1, EUCLID:77, YELLOW_9:9; ::_thesis: verum
end;

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


definition
let n be Nat;
let e be Point of (Euclid n);
func @ e ->  Point of (TopSpaceMetr (Euclid n)) equals :: EUCLID_9:def 2
e;
coherence
 e is Point of (TopSpaceMetr (Euclid n)) ;
end;

:: deftheorem  defines @ EUCLID_9:def_2_:_
 for n being Nat
for e being Point of (Euclid n) holds @ e = e;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be non positive real number ;
cluster Ball (e,r) ->  empty ;
coherence
 Ball (e,r) is empty
proof
assume  not Ball (e,r) is empty ; ::_thesis: contradiction
then consider x being Point of (Euclid n) such that
A1: x in Ball (e,r) by SUBSET_1:4;
 dist (x,e) < r by A1, METRIC_1:11;
hence  contradiction by METRIC_1:5; ::_thesis: verum
end;
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be positive real number ;
cluster Ball (e,r) ->  non empty ;
coherence
 not Ball (e,r) is empty by GOBOARD6:1;
end;

theorem Th8: :: EUCLID_9:8
for n, i being Nat
for p1, p2 being Point of (TOP-REAL n) st i in dom p1 holds
((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
proof
let n, i be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st i in dom p1 holds
((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( i in dom p1 implies ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) )
assume A1: i in dom p1 ; ::_thesis: ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
set e = sqr (p1 - p2);
A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_(p1_-_p2))_holds_
0_<=_(sqr_(p1_-_p2))_._i
let i be Nat; ::_thesis: ( i in dom (sqr (p1 - p2)) implies 0 <= (sqr (p1 - p2)) . i )
assume  i in dom (sqr (p1 - p2)) ; ::_thesis: 0 <= (sqr (p1 - p2)) . i
 (sqr (p1 - p2)) . i = ((p1 - p2) . i) ^2 by VALUED_1:11;
hence  0 <= (sqr (p1 - p2)) . i ; ::_thesis: verum
end;
A3: dom (sqr (p1 - p2)) = 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;
(sqr (p1 - p2)) . i = ((p1 - p2) . i) ^2 by VALUED_1:11
.= ((p1 /. i) - (p2 /. i)) ^2 by A6, A7, A1, A5, A4, VALUED_1:13 ;
hence  ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) by A1, A2, A3, A5, A4, MATRPROB:5; ::_thesis: verum
end;

theorem Th9: :: EUCLID_9:9
for n being Nat
for r being real number
for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
proof
let n be Nat; ::_thesis: for r being real number
for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let r be real number ; ::_thesis: for a, o, p being Element of (TOP-REAL n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let a, o, p be Element of (TOP-REAL n); ::_thesis: ( a in Ball (o,r) implies for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) )
A1: n in NAT by ORDINAL1:def_12;
assume A2: a in Ball (o,r) ; ::_thesis: for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
then A3: |.(a - o).| < r by A1, 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 A4: Sum (sqr (a - o)) < r ^2 by A3, SQUARE_1:16;
A5: sqr (a - o) = sqr (o - a) by EUCLID:20;
A6: r > 0 by A2;
let x be set ; ::_thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
A7: dom (a - o) = (dom a) /\ (dom o) by VALUED_1:12;
A8: ( dom a = Seg n & dom o = Seg n ) by FINSEQ_1:89;
percases ( x in dom a or not x in dom a ) ;
supposeA9: x in dom a ; ::_thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
then reconsider x = x as Nat ;
A10: (a - o) . x = (a . x) - (o . x) by A9, A7, A8, VALUED_1:13;
A11: ( a /. x = a . x & o /. x = o . x ) by A9, A8, PARTFUN1:def_6;
now__::_thesis:_not_(o_._x)_-_(a_._x)_>=_r
assume  (o . x) - (a . x) >= r ; ::_thesis: contradiction
then A12: ((o . x) - (a . x)) ^2 >= r ^2 by A6, SQUARE_1:15;
 Sum (sqr (o - a)) >= ((o /. x) - (a /. x)) ^2 by A9, A8, Th8;
hence  contradiction by A4, A12, A5, A11, XXREAL_0:2; ::_thesis: verum
end;
then A13: (o . x) - r < a . x by XREAL_1:11;
now__::_thesis:_not_(a_._x)_-_(o_._x)_>=_r
assume  (a . x) - (o . x) >= r ; ::_thesis: contradiction
then A14: ((a . x) - (o . x)) ^2 >= r ^2 by A6, SQUARE_1:15;
 Sum (sqr (a - o)) >= ((a /. x) - (o /. x)) ^2 by A9, Th8;
hence  contradiction by A4, A14, A11, XXREAL_0:2; ::_thesis: verum
end;
then  a . x < (o . x) + r by XREAL_1:19;
hence  ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A10, A13, RINFSUP1:1; ::_thesis: verum
end;
supposeA15: not x in dom a ; ::_thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
then  not x in dom (abs (a - o)) by A7, A8, VALUED_1:def_11;
then  (abs (a - o)) . x = 0 by FUNCT_1:def_2;
then A16: abs ((a - o) . x) = 0 by VALUED_1:18;
 ( a . x = 0 & o . x = 0 ) by A8, A15, FUNCT_1:def_2;
hence  ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A16, A2; ::_thesis: verum
end;
end;
end;

theorem Th10: :: EUCLID_9:10
for n being Nat
for r being real number
for a, o being Point of (Euclid n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
proof
let n be Nat; ::_thesis: for r being real number
for a, o being Point of (Euclid n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let r be real number ; ::_thesis: for a, o being Point of (Euclid n) st a in Ball (o,r) holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
let a, o be Point of (Euclid n); ::_thesis: ( a in Ball (o,r) implies for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) )
reconsider a1 = a, o1 = o as Point of (TOP-REAL n) by EUCLID:67;
 n in NAT by ORDINAL1:def_12;
then A1: Ball (o,r) = Ball (o1,r) by TOPREAL9:13;
 a - o = a1 - o1 ;
hence  ( a in Ball (o,r) implies for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) ) by A1, Th9; ::_thesis: verum
end;

definition
let f be real-valued Function;
let r be real number ;
func Intervals (f,r) ->  Function means :Def3: :: EUCLID_9:def 3
( dom it = dom f & ( for x being set st x in dom f holds
it . x = ].((f . x) - r),((f . x) + r).[ ) );
existence
 ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) )
proof
deffunc H1( set ) ->  Element of K19(REAL) = ].((f . $1) - r),((f . $1) + r).[;
 ex g being Function st
( dom g = dom f & ( for x being set st x in dom f holds
g . x = H1(x) ) ) from FUNCT_1:sch_3();
hence  ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = ].((f . x) - r),((f . x) + r).[ ) holds
b1 = b2
proof
let g, h be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom f holds
g . x = ].((f . x) - r),((f . x) + r).[ ) & dom h = dom f & ( for x being set st x in dom f holds
h . x = ].((f . x) - r),((f . x) + r).[ ) implies g = h )
assume that
A1: dom g = dom f and
A2: for x being set st x in dom f holds
g . x = ].((f . x) - r),((f . x) + r).[ and
A3: dom h = dom f and
A4: for x being set st x in dom f holds
h . x = ].((f . x) - r),((f . x) + r).[ ; ::_thesis: g = h
now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_
g_._x_=_h_._x
let x be set ; ::_thesis: ( x in dom g implies g . x = h . x )
assume A5: x in dom g ; ::_thesis: g . x = h . x
hence g . x = ].((f . x) - r),((f . x) + r).[ by A1, A2
.= h . x by A1, A4, A5 ;
::_thesis: verum
end;
hence  g = h by A1, A3, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Intervals EUCLID_9:def_3_:_
 for f being real-valued Function
for r being real number
for b3 being Function holds
( b3 = Intervals (f,r) iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = ].((f . x) - r),((f . x) + r).[ ) ) );

registration
let r be real number ;
cluster Intervals ({},r) ->  empty ;
coherence
 Intervals ({},r) is empty
proof
 dom (Intervals ({},r)) = dom {} by Def3;
hence  Intervals ({},r) is empty ; ::_thesis: verum
end;
end;

registration
let f be real-valued FinSequence;
let r be real number ;
cluster Intervals (f,r) ->  FinSequence-like ;
coherence
 Intervals (f,r) is FinSequence-like
proof
take  len f ; :: according to FINSEQ_1:def_2 ::_thesis: dom (Intervals (f,r)) = Seg (len f)
 dom (Intervals (f,r)) = dom f by Def3;
hence  dom (Intervals (f,r)) = Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum
end;
end;

definition
let n be Nat;
let e be Point of (Euclid n);
let r be real number ;
func OpenHypercube (e,r) ->  Subset of (TopSpaceMetr (Euclid n)) equals :: EUCLID_9:def 4
 product (Intervals (e,r));
coherence
 product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n))
proof
set T = TopSpaceMetr (Euclid n);
set f = Intervals (e,r);
 product (Intervals (e,r)) c= the carrier of (TopSpaceMetr (Euclid n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Intervals (e,r)) or x in the carrier of (TopSpaceMetr (Euclid n)) )
assume  x in product (Intervals (e,r)) ; ::_thesis: x in the carrier of (TopSpaceMetr (Euclid n))
then consider g being Function such that
A1: x = g and
A2: dom g = dom (Intervals (e,r)) and
A3: for y being set st y in dom (Intervals (e,r)) holds
g . y in (Intervals (e,r)) . y by CARD_3:def_5;
A4: dom (Intervals (e,r)) = dom e by Def3;
 dom e = Seg n by FINSEQ_1:89;
then reconsider x = x as FinSequence by A1, A2, A4, FINSEQ_1:def_2;
 rng x c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng x or b in REAL )
assume  b in rng x ; ::_thesis: b in REAL
then consider a being set  such that
A5: a in dom x and
A6: x . a = b by FUNCT_1:def_3;
A7: g . a in (Intervals (e,r)) . a by A1, A2, A3, A5;
 (Intervals (e,r)) . a = ].((e . a) - r),((e . a) + r).[ by A1, A2, A4, A5, Def3;
hence  b in REAL by A1, A6, A7; ::_thesis: verum
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  x in the carrier of (TopSpaceMetr (Euclid n)) by A8; ::_thesis: verum
end;
hence  product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n)) ; ::_thesis: verum
end;
end;

:: deftheorem  defines OpenHypercube EUCLID_9:def_4_:_
 for n being Nat
for e being Point of (Euclid n)
for r being real number holds OpenHypercube (e,r) = product (Intervals (e,r));

theorem Th11: :: EUCLID_9:11
for n being Nat
for r being real number
for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube (e,r)
proof
let n be Nat; ::_thesis: for r being real number
for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube (e,r)
let r be real number ; ::_thesis: for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube (e,r)
let e be Point of (Euclid n); ::_thesis: ( 0 < r implies e in OpenHypercube (e,r) )
assume A1: 0 < r ; ::_thesis: e in OpenHypercube (e,r)
set f = Intervals (e,r);
A2: dom (Intervals (e,r)) = dom e by Def3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_
e_._x_in_(Intervals_(e,r))_._x
let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies e . x in (Intervals (e,r)) . x )
assume  x in dom (Intervals (e,r)) ; ::_thesis: e . x in (Intervals (e,r)) . x
then A3: (Intervals (e,r)) . 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 (Intervals (e,r)) . x by A3, A4, XXREAL_1:4; ::_thesis: verum
end;
hence  e in OpenHypercube (e,r) by A2, CARD_3:9; ::_thesis: verum
end;

registration
let n be non zero Nat;
let e be Point of (Euclid n);
let r be non positive real number ;
cluster OpenHypercube (e,r) ->  empty ;
coherence
 OpenHypercube (e,r) is empty
proof
assume  not OpenHypercube (e,r) is empty ; ::_thesis: contradiction
then consider x being set  such that
A1: x in OpenHypercube (e,r) by XBOOLE_0:def_1;
reconsider e1 = e as real-valued Function ;
set f = Intervals (e,r);
A2: dom (Intervals (e,r)) = dom e by Def3;
A3: dom e = Seg n by FINSEQ_1:89;
consider N being set  such that
A4: N in Seg n by XBOOLE_0:def_1;
 (Intervals (e,r)) . N = ].((e1 . N) - r),((e1 . N) + r).[ by A4, A3, Def3;
hence  contradiction by A1, A2, A3, A4, CARD_3:9; ::_thesis: verum
end;
end;

theorem Th12: :: EUCLID_9:12
for r being real number
for e being Point of (Euclid 0) holds OpenHypercube (e,r) = {{}} by CARD_3:10;

registration
let e be Point of (Euclid 0);
let r be real number ;
cluster OpenHypercube (e,r) ->  non empty ;
coherence
 not OpenHypercube (e,r) is empty by CARD_3:10;
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be positive real number ;
cluster OpenHypercube (e,r) ->  non empty ;
coherence
 not OpenHypercube (e,r) is empty by Th11;
end;

theorem Th13: :: EUCLID_9:13
for n being Nat
for r, s being real number
for e being Point of (Euclid n) st r <= s holds
OpenHypercube (e,r) c= OpenHypercube (e,s)
proof
let n be Nat; ::_thesis: for r, s being real number
for e being Point of (Euclid n) st r <= s holds
OpenHypercube (e,r) c= OpenHypercube (e,s)
let r, s be real number ; ::_thesis: for e being Point of (Euclid n) st r <= s holds
OpenHypercube (e,r) c= OpenHypercube (e,s)
let e be Point of (Euclid n); ::_thesis: ( r <= s implies OpenHypercube (e,r) c= OpenHypercube (e,s) )
assume A1: r <= s ; ::_thesis: OpenHypercube (e,r) c= OpenHypercube (e,s)
A2: dom (Intervals (e,s)) = dom e by Def3;
A3: dom (Intervals (e,r)) = dom e by Def3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_
(Intervals_(e,r))_._x_c=_(Intervals_(e,s))_._x
let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies (Intervals (e,r)) . x c= (Intervals (e,s)) . x )
assume A4: x in dom (Intervals (e,r)) ; ::_thesis: (Intervals (e,r)) . x c= (Intervals (e,s)) . x
reconsider u = e . x as real number ;
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; ::_thesis: verum
end;
hence  OpenHypercube (e,r) c= OpenHypercube (e,s) by A2, A3, CARD_3:27; ::_thesis: verum
end;

theorem Th14: :: EUCLID_9:14
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
proof
let n be Nat; ::_thesis: for r being real number
for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
let e1, e be Point of (Euclid n); ::_thesis: ( ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) implies for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) )
assume that
A1: ( n <> 0 or 0 < r ) and
A2: e1 in OpenHypercube (e,r) ; ::_thesis: for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < 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 ; ::_thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
percases ( x in dom e1 or not x in dom e1 ) ;
supposeA5: x in dom e1 ; ::_thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
then A6: (e1 - e) . x = (e1 . x) - (e . x) by A3, A4, VALUED_1:13;
A7: ( e1 . x in REAL & e . x in REAL & r in REAL ) by XREAL_0:def_1;
 dom e = dom (Intervals (e,r)) by Def3;
then A8: 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  ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) by A6, A8, A7, FCONT_3:1; ::_thesis: verum
end;
supposeA9: not x in dom e1 ; ::_thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
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 A10: abs ((e1 - e) . x) = 0 by VALUED_1:18;
 ( e1 . x = 0 & e . x = 0 ) by A3, A9, FUNCT_1:def_2;
hence  ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) by A10, A1, A2; ::_thesis: verum
end;
end;
end;

theorem Th15: :: EUCLID_9:15
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
Sum (sqr (e1 - e)) < n * (r ^2)
proof
let n be Nat; ::_thesis: for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
Sum (sqr (e1 - e)) < n * (r ^2)
let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
Sum (sqr (e1 - e)) < n * (r ^2)
let e1, e be Point of (Euclid n); ::_thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies Sum (sqr (e1 - e)) < n * (r ^2) )
assume that
A1: n <> 0 and
A2: e1 in OpenHypercube (e,r) ; ::_thesis: Sum (sqr (e1 - e)) < n * (r ^2)
set R1 = sqr (e1 - e);
set R2 = n |-> (r ^2);
A3: REAL n = n -tuples_on REAL ;
A4: sqr (e1 - e) in n -tuples_on REAL by Th2;
A5: n |-> (r ^2) in n -tuples_on REAL by A3, Th2;
A6: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_
(sqr_(e1_-_e))_._i_<_(n_|->_(r_^2))_._i
let i be Nat; ::_thesis: ( i in Seg n implies (sqr (e1 - e)) . i < (n |-> (r ^2)) . i )
assume A7: i in Seg n ; ::_thesis: (sqr (e1 - e)) . i < (n |-> (r ^2)) . i
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: (sqr (e1 - e)) . i = ((e1 - e) . i) ^2 by VALUED_1:11;
A11: (n |-> (r ^2)) . i = r ^2 by A7, FINSEQ_2:57;
A12: abs ((e1 . i) - (e . i)) < r by A1, A2, Th14;
 ((e1 - e) . i) ^2 = (abs ((e1 - e) . i)) ^2 by COMPLEX1:75;
hence  (sqr (e1 - e)) . i < (n |-> (r ^2)) . i by A9, A10, A11, A12, SQUARE_1:16; ::_thesis: verum
end;
then A13: for i being Nat st i in Seg n holds
(sqr (e1 - e)) . i <= (n |-> (r ^2)) . i ;
 ex i being Nat st
( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i )
proof
consider i being set  such that
A14: i in Seg n by A1, XBOOLE_0:def_1;
reconsider i = i as Nat by A14;
take  i ; ::_thesis: ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i )
thus  ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i ) by A14, A6; ::_thesis: verum
end;
then  Sum (sqr (e1 - e)) < Sum (n |-> (r ^2)) by A4, A5, A13, RVSUM_1:83;
hence  Sum (sqr (e1 - e)) < n * (r ^2) by RVSUM_1:80; ::_thesis: verum
end;

theorem Th16: :: EUCLID_9:16
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
dist (e1,e) < r * (sqrt n)
proof
let n be Nat; ::_thesis: for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
dist (e1,e) < r * (sqrt n)
let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
dist (e1,e) < r * (sqrt n)
let e1, e be Point of (Euclid n); ::_thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies dist (e1,e) < r * (sqrt n) )
assume that
A1: n <> 0 and
A2: e1 in OpenHypercube (e,r) ; ::_thesis: dist (e1,e) < r * (sqrt n)
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  dist (e1,e) < r * (sqrt n) by A3, A4, SQUARE_1:29; ::_thesis: verum
end;

theorem Th17: :: EUCLID_9:17
for n being Nat
for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
proof
let n be Nat; ::_thesis: for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
let r be real number ; ::_thesis: for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
let e be Point of (Euclid n); ::_thesis: ( n <> 0 implies OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r) )
assume A1: n <> 0 ; ::_thesis: OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OpenHypercube (e,(r / (sqrt n))) or x in Ball (e,r) )
assume A2: x in OpenHypercube (e,(r / (sqrt n))) ; ::_thesis: x in Ball (e,r)
then reconsider x = 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  x in Ball (e,r) by A3, METRIC_1:11; ::_thesis: verum
end;

theorem :: EUCLID_9:18
for n being Nat
for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
proof
let n be Nat; ::_thesis: for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
let r be real number ; ::_thesis: for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
let e be Point of (Euclid n); ::_thesis: ( n <> 0 implies OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) )
assume A1: n <> 0 ; ::_thesis: OpenHypercube (e,r) c= Ball (e,(r * (sqrt n)))
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  OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) by A2, XCMPLX_1:74; ::_thesis: verum
end;

theorem Th19: :: EUCLID_9:19
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st e1 in Ball (e,r) holds
ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
proof
let n be Nat; ::_thesis: for r being real number
for e1, e being Point of (Euclid n) st e1 in Ball (e,r) holds
ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st e1 in Ball (e,r) holds
ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
let e1, e be Point of (Euclid n); ::_thesis: ( e1 in Ball (e,r) implies ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) )
reconsider B = Ball (e,r) as Subset of (TopSpaceMetr (Euclid n)) ;
assume A1: e1 in Ball (e,r) ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
 B is open by TOPMETR:14;
then consider s being real number  such that
A2: s > 0 and
A3: Ball (e1,s) c= B by A1, TOPMETR:15;
A4: s / (sqrt n) is Real by XREAL_0:def_1;
percases ( n <> 0 or n = 0 ) ;
supposeA5: n <> 0 ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
then consider m being Element of NAT  such that
A6: 1 / m < s / (sqrt n) and
A7: m > 0 by A2, A4, FRECHET:36;
reconsider m = m as non zero Element of NAT by A7;
A8: OpenHypercube (e1,(s / (sqrt n))) c= Ball (e1,s) by A5, Th17;
 OpenHypercube (e1,(1 / m)) c= OpenHypercube (e1,(s / (sqrt n))) by A6, Th13;
then  OpenHypercube (e1,(1 / m)) c= Ball (e1,s) by A8, XBOOLE_1:1;
hence  ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) by A3, XBOOLE_1:1; ::_thesis: verum
end;
suppose n = 0 ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r)
then  ( ( OpenHypercube (e1,(1 / 1)) = {} or OpenHypercube (e1,(1 / 1)) = {{}} ) & Ball (e,r) = {{}} ) by A1, EUCLID:77, ZFMISC_1:33;
hence  ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ; ::_thesis: verum
end;
end;
end;

theorem Th20: :: EUCLID_9:20
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
r > (abs (e1 - e)) . (max_diff_index (e1,e))
proof
let n be Nat; ::_thesis: for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
r > (abs (e1 - e)) . (max_diff_index (e1,e))
let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds
r > (abs (e1 - e)) . (max_diff_index (e1,e))
let e1, e be Point of (Euclid n); ::_thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies r > (abs (e1 - e)) . (max_diff_index (e1,e)) )
set d = max_diff_index (e1,e);
 (abs (e1 - e)) . (max_diff_index (e1,e)) = abs ((e1 - e) . (max_diff_index (e1,e))) by VALUED_1:18;
hence  ( n <> 0 & e1 in OpenHypercube (e,r) implies r > (abs (e1 - e)) . (max_diff_index (e1,e)) ) by Th14; ::_thesis: verum
end;

theorem Th21: :: EUCLID_9:21
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
proof
let n be Nat; ::_thesis: for r being real number
for e1, e being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
let e1, e be Point of (Euclid n); ::_thesis: OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r)
set d = max_diff_index (e1,e);
set F = abs (e1 - e);
set s = r - ((abs (e1 - e)) . (max_diff_index (e1,e)));
A1: ( dom e1 = Seg n & dom e = Seg n ) by FINSEQ_1:89;
let y be Point of (TopSpaceMetr (Euclid n)); :: according to LATTICE7:def_1 ::_thesis: ( not y in OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) or y in OpenHypercube (e,r) )
assume A2: y in OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) ; ::_thesis: y in OpenHypercube (e,r)
reconsider y = y as Point of (Euclid n) ;
A3: dom y = dom (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) by A2, CARD_3:9;
A4: dom (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) = dom e1 by Def3;
then A5: dom y = dom (Intervals (e,r)) by A1, A3, Def3;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_
y_._x_in_(Intervals_(e,r))_._x
let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies y . x in (Intervals (e,r)) . x )
assume A6: x in dom (Intervals (e,r)) ; ::_thesis: y . x in (Intervals (e,r)) . x
then A7: (Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[ by A1, A3, A4, A5, Def3;
A8: (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) . x = ].((e1 . x) - (r - ((abs (e1 - e)) . (max_diff_index (e1,e))))),((e1 . x) + (r - ((abs (e1 - e)) . (max_diff_index (e1,e))))).[ by A3, A4, A5, A6, Def3;
 y . x in (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) . x by A2, A3, A5, A6, CARD_3:9;
then A9: abs ((y . x) - (e1 . x)) < r - ((abs (e1 - e)) . (max_diff_index (e1,e))) by A8, RCOMP_1:1;
 dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12;
then  abs ((e1 . x) - (e . x)) = abs ((e1 - e) . x) by A1, A3, A4, A5, A6, VALUED_1:13
.= (abs (e1 - e)) . x by VALUED_1:18 ;
then A10: (abs ((y . x) - (e1 . x))) + (abs ((e1 . x) - (e . x))) < (r - ((abs (e1 - e)) . (max_diff_index (e1,e)))) + ((abs (e1 - e)) . (max_diff_index (e1,e))) by A9, Th5, XREAL_1:8;
 abs ((y . x) - (e . x)) <= (abs ((y . x) - (e1 . x))) + (abs ((e1 . x) - (e . x))) by COMPLEX1:63;
then  abs ((y . x) - (e . x)) < r by A10, XXREAL_0:2;
hence  y . x in (Intervals (e,r)) . x by A7, RCOMP_1:1; ::_thesis: verum
end;
hence  y in OpenHypercube (e,r) by A5, CARD_3:9; ::_thesis: verum
end;

theorem Th22: :: EUCLID_9:22
for n being Nat
for r being real number
for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
proof
let n be Nat; ::_thesis: for r being real number
for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
let r be real number ; ::_thesis: for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r)
let e be Point of (Euclid n); ::_thesis: Ball (e,r) c= OpenHypercube (e,r)
let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in Ball (e,r) or g in OpenHypercube (e,r) )
assume A1: g in Ball (e,r) ; ::_thesis: g in OpenHypercube (e,r)
then reconsider g = 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__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_
g_._x_in_(Intervals_(e,r))_._x
let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies g . x in (Intervals (e,r)) . x )
reconsider u = e . x, v = g . x as Real by XREAL_0:def_1;
assume A4: x in dom (Intervals (e,r)) ; ::_thesis: g . x in (Intervals (e,r)) . x
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) ;
 abs ((g - e) . x) < r by A1, Th10;
hence  g . x in (Intervals (e,r)) . x by A6, A5, A7, FCONT_3:3; ::_thesis: verum
end;
hence  g in OpenHypercube (e,r) by A2, A3, CARD_3:9; ::_thesis: verum
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be real number ;
cluster OpenHypercube (e,r) ->  open ;
coherence
 OpenHypercube (e,r) is open
proof
percases ( n <> 0 or n = 0 ) ;
supposeA1: n <> 0 ; ::_thesis: OpenHypercube (e,r) is open
 for p being Point of (Euclid n) st p in OpenHypercube (e,r) holds
ex s being real number st
( s > 0 & Ball (p,s) c= OpenHypercube (e,r) )
proof
let p be Point of (Euclid n); ::_thesis: ( p in OpenHypercube (e,r) implies ex s being real number st
( s > 0 & Ball (p,s) c= OpenHypercube (e,r) ) )
assume A2: p in OpenHypercube (e,r) ; ::_thesis: ex s being real number st
( s > 0 & Ball (p,s) c= OpenHypercube (e,r) )
set d = (abs (p - e)) . (max_diff_index (p,e));
take s = r - ((abs (p - e)) . (max_diff_index (p,e))); ::_thesis: ( s > 0 & Ball (p,s) c= OpenHypercube (e,r) )
 r - ((abs (p - e)) . (max_diff_index (p,e))) > ((abs (p - e)) . (max_diff_index (p,e))) - ((abs (p - e)) . (max_diff_index (p,e))) by A1, A2, Th20, XREAL_1:8;
hence  s > 0 ; ::_thesis: Ball (p,s) c= OpenHypercube (e,r)
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, XBOOLE_1:1; ::_thesis: verum
end;
hence  OpenHypercube (e,r) is open by TOPMETR:15; ::_thesis: verum
end;
supposeA4: n = 0 ; ::_thesis: OpenHypercube (e,r) is open
then  OpenHypercube (e,r) = {{}} by Th12;
then  OpenHypercube (e,r) in the topology of (TopSpaceMetr (Euclid 0)) by Th6, TARSKI:def_2;
hence  OpenHypercube (e,r) is open by A4, PRE_TOPC:def_2; ::_thesis: verum
end;
end;
end;
end;

theorem :: EUCLID_9:23
for n being Nat
for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
proof
let n be Nat; ::_thesis: for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
let V be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( V is open implies for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V )
assume A1: V is open ; ::_thesis: for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
let e be Point of (Euclid n); ::_thesis: ( e in V implies ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V )
assume  e in V ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V
then consider r being real number  such that
A2: r > 0 and
A3: Ball (e,r) c= V by A1, TOPMETR:15;
consider m being non zero Element of NAT  such that
A4: OpenHypercube (e,(1 / m)) c= Ball (e,r) by A2, Th19, GOBOARD6:1;
take  m ; ::_thesis: OpenHypercube (e,(1 / m)) c= V
thus  OpenHypercube (e,(1 / m)) c= V by A3, A4, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: EUCLID_9:24
for n being Nat
for V being Subset of (TopSpaceMetr (Euclid n)) st ( for e being Point of (Euclid n) st e in V holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= V ) ) holds
V is open
proof
let n be Nat; ::_thesis: for V being Subset of (TopSpaceMetr (Euclid n)) st ( for e being Point of (Euclid n) st e in V holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= V ) ) holds
V is open
let V be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( ( for e being Point of (Euclid n) st e in V holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= V ) ) implies V is open )
assume A1: for e being Point of (Euclid n) st e in V holds
ex r being real number st
( r > 0 & OpenHypercube (e,r) c= V ) ; ::_thesis: V is open
 for e being Point of (Euclid n) st e in V holds
ex r being real number st
( r > 0 & Ball (e,r) c= V )
proof
let e be Point of (Euclid n); ::_thesis: ( e in V implies ex r being real number st
( r > 0 & Ball (e,r) c= V ) )
assume  e in V ; ::_thesis: ex r being real number st
( r > 0 & Ball (e,r) c= V )
then consider r being real number  such that
A2: r > 0 and
A3: OpenHypercube (e,r) c= V by A1;
 Ball (e,r) c= OpenHypercube (e,r) by Th22;
hence  ex r being real number st
( r > 0 & Ball (e,r) c= V ) by A2, A3, XBOOLE_1:1; ::_thesis: verum
end;
hence  V is open by TOPMETR:15; ::_thesis: verum
end;

deffunc H1( Nat, Point of (Euclid $1)) ->  set =  {  (OpenHypercube ($2,(1 / m))) where m is non zero Element of NAT : verum  }  ;

definition
let n be Nat;
let e be Point of (Euclid n);
func OpenHypercubes e ->  Subset-Family of (TopSpaceMetr (Euclid n)) equals :: EUCLID_9:def 5
 {  (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum  }  ;
coherence
  {  (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum  }  is Subset-Family of (TopSpaceMetr (Euclid n))
proof
 H1(n,e) c= bool the carrier of (TopSpaceMetr (Euclid n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(n,e) or x in bool the carrier of (TopSpaceMetr (Euclid n)) )
assume  x in H1(n,e) ; ::_thesis: x in bool the carrier of (TopSpaceMetr (Euclid n))
then  ex m being non zero Element of NAT st x = OpenHypercube (e,(1 / m)) ;
hence  x in bool the carrier of (TopSpaceMetr (Euclid n)) by ZFMISC_1:def_1; ::_thesis: verum
end;
hence   {  (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum  }  is Subset-Family of (TopSpaceMetr (Euclid n)) ; ::_thesis: verum
end;
end;

:: deftheorem  defines OpenHypercubes EUCLID_9:def_5_:_
 for n being Nat
for e being Point of (Euclid n) holds OpenHypercubes e =  {  (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum  }  ;

registration
let n be Nat;
let e be Point of (Euclid n);
cluster OpenHypercubes e ->  non empty open @ e -quasi_basis ;
coherence
 ( not OpenHypercubes e is empty & OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )
proof
set T = TopSpaceMetr (Euclid n);
 OpenHypercube (e,(1 / 1)) in OpenHypercubes e ;
hence  not OpenHypercubes e is empty ; ::_thesis: ( OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )
hereby  :: according to TOPS_2:def_1 ::_thesis: OpenHypercubes e is @ e -quasi_basis
let A be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( A in OpenHypercubes e implies A is open )
assume  A in OpenHypercubes e ; ::_thesis: A is open
then  ex m being non zero Element of NAT st A = OpenHypercube (e,(1 / m)) ;
hence  A is open ; ::_thesis: verum
end;
now__::_thesis:_for_Y_being_set_st_Y_in_OpenHypercubes_e_holds_
@_e_in_Y
let Y be set ; ::_thesis: ( Y in OpenHypercubes e implies @ e in Y )
assume  Y in OpenHypercubes e ; ::_thesis: @ e in Y
then  ex m being non zero Element of NAT st Y = OpenHypercube (e,(1 / m)) ;
hence  @ e in Y by Th11; ::_thesis: verum
end;
hence  @ e in Intersect (OpenHypercubes e) by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) holds
( not b1 is open or not @ e in b1 or ex b2 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b2 in OpenHypercubes e & b2 c= b1 ) )
let S be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( not S is open or not @ e in S or ex b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b1 in OpenHypercubes e & b1 c= S ) )
assume that
A1: S is open and
A2: @ e in S ; ::_thesis: ex b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st
( b1 in OpenHypercubes e & b1 c= S )
consider r being real number  such that
A3: r > 0 and
A4: Ball (e,r) c= S by A1, A2, TOPMETR:15;
consider m being 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)); ::_thesis: ( V in OpenHypercubes e & V c= S )
thus  V in OpenHypercubes e ; ::_thesis: V c= S
thus  V c= S by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;
end;

Lm1: now__::_thesis:_TopSpaceMetr_(Euclid_0)_=_product_({}_-->_R^1)
set J = {} --> R^1;
set C = Carrier ({} --> R^1);
set P = product ({} --> R^1);
set T = TopSpaceMetr (Euclid 0);
A1: the carrier of (product ({} --> R^1)) = product (Carrier ({} --> R^1)) by WAYBEL18:def_3;
 { the carrier of (TopSpaceMetr (Euclid 0))} is Basis of (TopSpaceMetr (Euclid 0)) by YELLOW_9:10;
hence  TopSpaceMetr (Euclid 0) = product ({} --> R^1) by A1, CARD_3:10, EUCLID:77, YELLOW_9:10, YELLOW_9:25; ::_thesis: verum
end;

theorem Th25: :: EUCLID_9:25
for n being Nat holds Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1))
proof
let n be Nat; ::_thesis: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1))
set J = (Seg n) --> R^1;
set C = Carrier ((Seg n) --> R^1);
A1: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def_2;
thus  Funcs ((Seg n),REAL) c= product (Carrier ((Seg n) --> R^1)) :: according to XBOOLE_0:def_10 ::_thesis: product (Carrier ((Seg n) --> R^1)) c= Funcs ((Seg n),REAL)
proof
let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in Funcs ((Seg n),REAL) or f in product (Carrier ((Seg n) --> R^1)) )
assume  f in Funcs ((Seg n),REAL) ; ::_thesis: f in product (Carrier ((Seg n) --> R^1))
then reconsider f = f as Function of (Seg n),REAL by FUNCT_2:66;
A2: dom f = Seg n by FUNCT_2:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_(Carrier_((Seg_n)_-->_R^1))_holds_
f_._x_in_(Carrier_((Seg_n)_-->_R^1))_._x
let x be set ; ::_thesis: ( x in dom (Carrier ((Seg n) --> R^1)) implies f . x in (Carrier ((Seg n) --> R^1)) . x )
assume A3: x in dom (Carrier ((Seg n) --> R^1)) ; ::_thesis: f . x in (Carrier ((Seg n) --> R^1)) . x
then A4: ex R being 1-sorted st
( R = ((Seg n) --> R^1) . x & (Carrier ((Seg n) --> R^1)) . x = the carrier of R ) by PRALG_1:def_13;
 f . x in REAL by A3, FUNCT_2:5;
hence  f . x in (Carrier ((Seg n) --> R^1)) . x by A4, A3, FUNCOP_1:7; ::_thesis: verum
end;
hence  f in product (Carrier ((Seg n) --> R^1)) by A2, A1, CARD_3:9; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Carrier ((Seg n) --> R^1)) or x in Funcs ((Seg n),REAL) )
assume  x in product (Carrier ((Seg n) --> R^1)) ; ::_thesis: x in Funcs ((Seg n),REAL)
then consider g being Function such that
A5: x = g and
A6: dom g = dom (Carrier ((Seg n) --> R^1)) and
A7: for y being set st y in dom (Carrier ((Seg n) --> R^1)) holds
g . y in (Carrier ((Seg n) --> R^1)) . y by CARD_3:def_5;
 rng g c= REAL
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in REAL )
assume  z in rng g ; ::_thesis: z in REAL
then consider a being set  such that
A8: a in dom g and
A9: g . a = z by FUNCT_1:def_3;
A10: ex R being 1-sorted st
( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A6, A8, PRALG_1:def_13;
 ((Seg n) --> R^1) . a = R^1 by A6, A8, FUNCOP_1:7;
hence  z in REAL by A6, A7, A8, A9, A10; ::_thesis: verum
end;
hence  x in Funcs ((Seg n),REAL) by A1, A5, A6, FUNCT_2:def_2; ::_thesis: verum
end;

theorem Th26: :: EUCLID_9:26
for n being Nat st n <> 0 holds
for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is quasi_prebasis
proof
let n be Nat; ::_thesis: ( n <> 0 implies for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is quasi_prebasis )
assume A1: n <> 0 ; ::_thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is quasi_prebasis
set E = Euclid n;
set T = TopSpaceMetr (Euclid n);
let PP be Subset-Family of (TopSpaceMetr (Euclid n)); ::_thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is quasi_prebasis )
set J = (Seg n) --> R^1;
set C = Carrier ((Seg n) --> R^1);
set S = Seg n;
reconsider S = Seg n as non empty finite set by A1;
assume A2: PP = product_prebasis ((Seg n) --> R^1) ; ::_thesis: PP is quasi_prebasis
A3: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
A4: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def_2;
A5: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) by Th25;
defpred S1[ set , set ] means  ex e being Point of (Euclid n) st
( e = $1 & $2 = OpenHypercubes e );
A6: for i being Element of (TopSpaceMetr (Euclid n)) ex j being set st S1[i,j]
proof
let i be Element of (TopSpaceMetr (Euclid n)); ::_thesis: ex j being set st S1[i,j]
reconsider j = i as Point of (Euclid n) ;
take  OpenHypercubes j ; ::_thesis: S1[i, OpenHypercubes j]
take  j ; ::_thesis: ( j = i & OpenHypercubes j = OpenHypercubes j )
thus  ( j = i & OpenHypercubes j = OpenHypercubes j ) ; ::_thesis: verum
end;
consider NS being ManySortedSet of (TopSpaceMetr (Euclid n)) such that
A7: for x being Point of (TopSpaceMetr (Euclid n)) holds S1[x,NS . x] from PBOOLE:sch_6(A6);
now__::_thesis:_for_x_being_Point_of_(TopSpaceMetr_(Euclid_n))_holds_NS_._x_is_Basis_of_x
let x be Point of (TopSpaceMetr (Euclid n)); ::_thesis: NS . x is Basis of x
reconsider y = x as Point of (Euclid n) ;
 S1[y,NS . y] by A7;
hence  NS . x is Basis of x ; ::_thesis: verum
end;
then reconsider NS = NS as Neighborhood_System of TopSpaceMetr (Euclid n) by TOPGEN_2:def_3;
take B = Union NS; :: according to CANTOR_1:def_4 ::_thesis: B c= FinMeetCl PP
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in B or b in FinMeetCl PP )
assume  b in B ; ::_thesis: b in FinMeetCl PP
then consider Z being set  such that
A8: b in Z and
A9: Z in rng NS by TARSKI:def_4;
consider x being set  such that
A10: x in dom NS and
A11: NS . x = Z by A9, FUNCT_1:def_3;
reconsider x = x as Point of (Euclid n) by A10;
A12: dom x = Seg n by FINSEQ_1:89;
 S1[x,NS . x] by A7;
then consider m being non zero Element of NAT  such that
A13: b = OpenHypercube (x,(1 / m)) by A8, A11;
deffunc H2( set ) ->  set = product ((Carrier ((Seg n) --> R^1)) +* ($1,(R^1 ].((x . $1) - (1 / m)),((x . $1) + (1 / m)).[)));
defpred S2[ set ] means verum;
set Y =  {  H2(q) where q is Element of S : S2[q]  }  ;
A14:  {  H2(q) where q is Element of S : S2[q]  }  is finite from PRE_CIRC:sch_1();
  {  H2(q) where q is Element of S : S2[q]  }  c= bool the carrier of (TopSpaceMetr (Euclid n))
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in  {  H2(q) where q is Element of S : S2[q]  }  or s in bool the carrier of (TopSpaceMetr (Euclid n)) )
assume  s in  {  H2(q) where q is Element of S : S2[q]  }  ; ::_thesis: s in bool the carrier of (TopSpaceMetr (Euclid n))
then consider q being Element of S such that
A15: s = H2(q) ;
 H2(q) c= the carrier of (TopSpaceMetr (Euclid n))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in H2(q) or z in the carrier of (TopSpaceMetr (Euclid n)) )
set f = (Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[));
assume  z in H2(q) ; ::_thesis: z in the carrier of (TopSpaceMetr (Euclid n))
then consider g being Function such that
A16: z = g and
A17: dom g = dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) and
A18: for d being set st d in dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) holds
g . d in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . d by CARD_3:def_5;
A19: dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
then reconsider g = g as FinSequence by A4, A17, FINSEQ_1:def_2;
 rng g c= REAL
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng g or b in REAL )
assume  b in rng g ; ::_thesis: b in REAL
then consider a being set  such that
A20: a in dom g and
A21: g . a = b by FUNCT_1:def_3;
A22: g . a in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a by A17, A18, A20;
percases ( a = q or a <> q ) ;
suppose a = q ; ::_thesis: b in REAL
then  ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[ by A17, A19, A20, FUNCT_7:31;
hence  b in REAL by A21, A22; ::_thesis: verum
end;
suppose a <> q ; ::_thesis: b in REAL
then A23: ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = (Carrier ((Seg n) --> R^1)) . a by FUNCT_7:32;
 ex R being 1-sorted st
( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A20, A17, A19, PRALG_1:def_13;
hence  b in REAL by A21, A22, A23, A20, A17, A19, FUNCOP_1:7; ::_thesis: verum
end;
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  z in the carrier of (TopSpaceMetr (Euclid n)) by A16, A24; ::_thesis: verum
end;
hence  s in bool the carrier of (TopSpaceMetr (Euclid n)) by A15, ZFMISC_1:def_1; ::_thesis: verum
end;
then reconsider Y =  {  H2(q) where q is Element of S : S2[q]  }  as Subset-Family of (TopSpaceMetr (Euclid n)) ;
A25: Y c= PP
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Y or z in PP )
assume A26: z in Y ; ::_thesis: z in PP
then consider i being Element of S such that
A27: z = H2(i) ;
 ((Seg n) --> R^1) . i = R^1 by FUNCOP_1:7;
hence  z in PP by A2, A5, A26, A3, A27, WAYBEL18:def_2; ::_thesis: verum
end;
consider N being set  such that
A28: N in S by XBOOLE_0:def_1;
A29: H2(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__::_thesis:_for_i_being_Element_of_S_holds_product_(Intervals_(x,(1_/_m)))_c=_product_((Carrier_((Seg_n)_-->_R^1))_+*_(i,(R^1_].((x_._i)_-_(1_/_m)),((x_._i)_+_(1_/_m)).[)))
let i be Element of S; ::_thesis: product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
set f = (Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[));
thus  product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ::_thesis: verum
proof
let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in product (Intervals (x,(1 / m))) or d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) )
assume  d in product (Intervals (x,(1 / m))) ; ::_thesis: d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)))
then consider d1 being Function such that
A33: d = d1 and
A34: dom d1 = dom (Intervals (x,(1 / m))) and
A35: for a being set st a in dom (Intervals (x,(1 / m))) holds
d1 . a in (Intervals (x,(1 / m))) . a by CARD_3:def_5;
A36: dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
now__::_thesis:_for_k_being_set_st_k_in_dom_((Carrier_((Seg_n)_-->_R^1))_+*_(i,(R^1_].((x_._i)_-_(1_/_m)),((x_._i)_+_(1_/_m)).[)))_holds_
d1_._k_in_((Carrier_((Seg_n)_-->_R^1))_+*_(i,(R^1_].((x_._i)_-_(1_/_m)),((x_._i)_+_(1_/_m)).[)))_._k
let k be set ; ::_thesis: ( k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) implies d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1 )
assume A37: k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ; ::_thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1
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;
percases ( k = i or k <> i ) ;
suppose k = i ; ::_thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1
hence  d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A38, A39, A37, A36, FUNCT_7:31; ::_thesis: verum
end;
suppose k <> i ; ::_thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1
then A40: ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k = (Carrier ((Seg n) --> R^1)) . k by FUNCT_7:32;
A41: ex R being 1-sorted st
( R = ((Seg n) --> R^1) . k & (Carrier ((Seg n) --> R^1)) . k = the carrier of R ) by A37, A36, PRALG_1:def_13;
 d1 . k in REAL by A38, A39;
hence  d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A40, A41, A37, A36, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
hence  d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) by A33, A4, A34, A31, A12, A36, CARD_3:9; ::_thesis: verum
end;
end;
 b = Intersect Y
proof
now__::_thesis:_for_M_being_set_st_M_in_Y_holds_
b_c=_M
let M be set ; ::_thesis: ( M in Y implies b c= M )
assume  M in Y ; ::_thesis: b c= M
then  ex i being Element of S st M = H2(i) ;
hence  b c= M by A13, A32; ::_thesis: verum
end;
hence  b c= Intersect Y by A30, A29, SETFAM_1:5; :: according to XBOOLE_0:def_10 ::_thesis: Intersect Y c= b
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Intersect Y or q in b )
assume A42: q in Intersect Y ; ::_thesis: q in b
then reconsider q = q as Function ;
A43: dom q = Seg n by A42, FINSEQ_1:89;
now__::_thesis:_for_a_being_set_st_a_in_dom_(Intervals_(x,(1_/_m)))_holds_
q_._a_in_(Intervals_(x,(1_/_m)))_._a
let a be set ; ::_thesis: ( a in dom (Intervals (x,(1 / m))) implies q . a in (Intervals (x,(1 / m))) . a )
assume A44: a in dom (Intervals (x,(1 / m))) ; ::_thesis: q . a in (Intervals (x,(1 / m))) . a
A45: (Intervals (x,(1 / m))) . a = ].((x . a) - (1 / m)),((x . a) + (1 / m)).[ by A44, A31, Def3;
set f = (Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[));
 H2(a) in Y by A44, A31, A12;
then A46: q in H2(a) by A42, SETFAM_1:43;
then A47: dom q = dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) by CARD_3:9;
then A48: q . a in ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) . a by A43, A44, A31, A12, A46, CARD_3:9;
 dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
hence  q . a in (Intervals (x,(1 / m))) . a by A45, A48, A43, A44, A31, A12, A47, FUNCT_7:31; ::_thesis: verum
end;
hence  q in b by A13, A43, A31, A12, CARD_3:9; ::_thesis: verum
end;
hence  b in FinMeetCl PP by A25, A14, CANTOR_1:def_3; ::_thesis: verum
end;

theorem Th27: :: EUCLID_9:27
for n being Nat
for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is open
proof
let n be Nat; ::_thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds
PP is open
let PP be Subset-Family of (TopSpaceMetr (Euclid n)); ::_thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is open )
set J = (Seg n) --> R^1;
set C = Carrier ((Seg n) --> R^1);
set T = TopSpaceMetr (Euclid n);
set E = Euclid n;
assume A1: PP = product_prebasis ((Seg n) --> R^1) ; ::_thesis: PP is open
let x be Subset of (TopSpaceMetr (Euclid n)); :: according to TOPS_2:def_1 ::_thesis: ( not x in PP or x is open )
assume  x in PP ; ::_thesis: x is open
then consider i being set , R being TopStruct , V being Subset of R such that
A2: i in Seg n and
A3: V is open and
A4: R = ((Seg n) --> R^1) . i and
A5: x = product ((Carrier ((Seg n) --> R^1)) +* (i,V)) by A1, WAYBEL18:def_2;
A6: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def_2;
A7: now__::_thesis:_for_i_being_set_
for_e,_y_being_Point_of_(Euclid_n)
for_r_being_real_number_st_y_in_Ball_(e,r)_holds_
y_in_product_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))
let i be set ; ::_thesis: for e, y being Point of (Euclid n)
for r being real number st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
let e, y be Point of (Euclid n); ::_thesis: for r being real number st y in Ball (e,r) holds
y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
let r be real number ; ::_thesis: ( y in Ball (e,r) implies y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) )
assume A8: y in Ball (e,r) ; ::_thesis: y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[))
set O = ].((e . i) - r),((e . i) + r).[;
set G = (Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[);
A9: dom y = Seg n by FINSEQ_1:89;
A10: dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
now__::_thesis:_for_a_being_set_st_a_in_dom_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_holds_
y_._a_in_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_._a
let a be set ; ::_thesis: ( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 )
assume A11: a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ; ::_thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1
percases ( a = i or a <> i ) ;
supposeA12: a = i ; ::_thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1
A13: ( r is Real & e . i is Real & y . i is Real & (y . i) - (e . i) is Real ) by XREAL_0:def_1;
A14: y . i = (e . i) + ((y . i) - (e . i)) ;
A15: dom e = Seg n by FINSEQ_1:89;
 dom (y - e) = (dom y) /\ (dom e) by VALUED_1:12;
then A16: (y - e) . i = (y . i) - (e . i) by A9, A15, A11, A12, A10, VALUED_1:13;
 abs ((y - e) . i) < r by A8, Th10;
then  y . i in ].((e . i) - r),((e . i) + r).[ by A16, A13, A14, FCONT_3:3;
hence  y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a by A12, A10, A11, FUNCT_7:31; ::_thesis: verum
end;
suppose a <> i ; ::_thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1
then A17: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a by FUNCT_7:32;
A18: ex R being 1-sorted st
( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A11, A10, PRALG_1:def_13;
 y . a in REAL by XREAL_0:def_1;
hence  y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a by A17, A11, A10, A18, FUNCOP_1:7; ::_thesis: verum
end;
end;
end;
hence  y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) by A10, A6, A9, CARD_3:9; ::_thesis: verum
end;
set F = (Carrier ((Seg n) --> R^1)) +* (i,V);
A19: R = R^1 by A2, A4, FUNCOP_1:7;
 for e being Element of (Euclid n) st e in x holds
ex r being Real st
( r > 0 & Ball (e,r) c= x )
proof
let e be Element of (Euclid n); ::_thesis: ( e in x implies ex r being Real st
( r > 0 & Ball (e,r) c= x ) )
assume A20: e in x ; ::_thesis: ex r being Real st
( r > 0 & Ball (e,r) c= x )
A21: dom ((Carrier ((Seg n) --> R^1)) +* (i,V)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
then A22: e . i in ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i by A2, A6, A20, A5, CARD_3:9;
A23: ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i = V by A2, A6, FUNCT_7:31;
then consider r being Real such that
A24: r > 0 and
A25: ].((e . i) - r),((e . i) + r).[ c= V by A3, A19, A22, FRECHET:8;
take  r ; ::_thesis: ( r > 0 & Ball (e,r) c= x )
thus  r > 0 by A24; ::_thesis: Ball (e,r) c= x
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (e,r) or y in x )
assume A26: y in Ball (e,r) ; ::_thesis: y in x
then reconsider y = y as Point of (Euclid n) ;
set O = ].((e . i) - r),((e . i) + r).[;
set G = (Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[);
A27: dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30;
A28: y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) by A26, A7;
now__::_thesis:_for_a_being_set_st_a_in_dom_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_holds_
((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_._a_c=_((Carrier_((Seg_n)_-->_R^1))_+*_(i,V))_._a
let a be set ; ::_thesis: ( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 )
assume A29: a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ; ::_thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1
percases ( a = i or a <> i ) ;
suppose a = i ; ::_thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1
hence  ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a by A25, A23, A27, A29, FUNCT_7:31; ::_thesis: verum
end;
suppose a <> i ; ::_thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1
then  ( ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a & ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a = (Carrier ((Seg n) --> R^1)) . a ) by FUNCT_7:32;
hence  ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a ; ::_thesis: verum
end;
end;
end;
then  product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) c= product ((Carrier ((Seg n) --> R^1)) +* (i,V)) by A21, CARD_3:27, FUNCT_7:30;
hence  y in x by A28, A5; ::_thesis: verum
end;
then  x in the topology of (TopSpaceMetr (Euclid n)) by PCOMPS_1:def_4;
hence  x is open by PRE_TOPC:def_2; ::_thesis: verum
end;

theorem :: EUCLID_9:28
for n being Nat holds TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1)
proof
let n be Nat; ::_thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1)
set J = (Seg n) --> R^1;
percases ( n = 0 or n <> 0 ) ;
supposeA1: n = 0 ; ::_thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1)
then  (Seg n) --> R^1 = {} --> R^1 ;
hence  TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) by A1, Lm1; ::_thesis: verum
end;
supposeA2: n <> 0 ; ::_thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1)
A3: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93;
A4: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) by Th25;
then reconsider PP = product_prebasis ((Seg n) --> R^1) 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  TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) by A4, A3, A5, WAYBEL18:def_3; ::_thesis: verum
end;
end;
end;