:: JORDAN2B semantic presentation

begin

                     Lm1:  for n, i being Nat
for p being Element of (TOP-REAL n) ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )
proof
let n, i be Nat; ::_thesis: for p being Element of (TOP-REAL n) ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )
let p be Element of (TOP-REAL n); ::_thesis: ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i )
 p is Element of REAL n by EUCLID:22;
then  p in  {  s where s is Element of REAL * : len s = n  }  ;
then consider s being Element of REAL *  such that
A1: p = s and
 len s = n ;
 s /. i = s /. i ;
hence  ex q being Real ex g being FinSequence of REAL st
( g = p & q = g /. i ) by A1; ::_thesis: verum
end;

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

theorem :: JORDAN2B:1
for i being Element of NAT
for n being Nat ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i
proof
let i be Element of NAT ; ::_thesis: for n being Nat ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i
let n be Nat; ::_thesis: ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i
defpred S1[ set , set ] means  for p being Element of (TOP-REAL n) st $1 = p holds
$2 = p /. i;
A1: for x being set st x in REAL n holds
ex y being set st
( y in REAL & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in REAL n implies ex y being set st
( y in REAL & S1[x,y] ) )
assume  x in REAL n ; ::_thesis: ex y being set st
( y in REAL & S1[x,y] )
then reconsider px = x as Element of (TOP-REAL n) by EUCLID:22;
consider q being Real, g being FinSequence of REAL  such that
A2: g = px and
 q = g /. i by Lm1;
 for p being Element of (TOP-REAL n) st x = p holds
g /. i = p /. i by A2;
hence  ex y being set st
( y in REAL & S1[x,y] ) ; ::_thesis: verum
end;
 ex f being Function of (REAL n),REAL st
for x being set st x in REAL n holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
then consider f being Function of (REAL n),REAL such that
A3: for x being set st x in REAL n holds
for p being Element of (TOP-REAL n) st x = p holds
f . x = p /. i ;
 the carrier of (TOP-REAL n) = REAL n by EUCLID:22;
then reconsider f1 = f as Function of (TOP-REAL n),R^1 by TOPMETR:17;
 for p being Element of (TOP-REAL n) holds f1 . p = p /. i
proof
let p be Element of (TOP-REAL n); ::_thesis: f1 . p = p /. i
 p in the carrier of (TOP-REAL n) ;
then  p in REAL n by EUCLID:22;
hence  f1 . p = p /. i by A3; ::_thesis: verum
end;
hence  ex f being Function of (TOP-REAL n),R^1 st
for p being Element of (TOP-REAL n) holds f . p = p /. i ; ::_thesis: verum
end;

theorem :: JORDAN2B:2
for n, i being Element of NAT st i in Seg n holds
(0. (TOP-REAL n)) /. i = 0
proof
let n, i be Element of NAT ; ::_thesis: ( i in Seg n implies (0. (TOP-REAL n)) /. i = 0 )
assume A1: i in Seg n ; ::_thesis: (0. (TOP-REAL n)) /. i = 0
 len (0* n) = n by CARD_1:def_7;
then A2: i in dom (0* n) by A1, FINSEQ_1:def_3;
(0. (TOP-REAL n)) /. i = (0* n) /. i by EUCLID:70
.= (0* n) . i by A2, PARTFUN1:def_6
.= 0 by A1, FUNCOP_1:7 ;
hence  (0. (TOP-REAL n)) /. i = 0 ; ::_thesis: verum
end;

theorem :: JORDAN2B:3
for n being Element of NAT
for r being real number
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
proof
let n be Element of NAT ; ::_thesis: for r being real number
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
let r be real number ; ::_thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
let p be Point of (TOP-REAL n); ::_thesis: for i being Element of NAT st i in Seg n holds
(r * p) /. i = r * (p /. i)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (r * p) /. i = r * (p /. i) )
reconsider w1 = p as Element of REAL n by EUCLID:22;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w = r * p as Element of REAL n by EUCLID:22;
assume A1: i in Seg n ; ::_thesis: (r * p) /. i = r * (p /. i)
then  i in Seg (len w1) by CARD_1:def_7;
then A2: i in dom w1 by FINSEQ_1:def_3;
 len w = n by CARD_1:def_7;
then A3: i in dom w by A1, FINSEQ_1:def_3;
A4: p /. i = w3 . i by A2, PARTFUN1:def_6;
(r * p) /. i = w . i by A3, PARTFUN1:def_6
.= (r * w3) . i
.= r * (p /. i) by A4, RVSUM_1:45 ;
hence  (r * p) /. i = r * (p /. i) ; ::_thesis: verum
end;

theorem :: JORDAN2B:4
for n being Element of NAT
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(- p) /. i = - (p /. i)
proof
let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(- p) /. i = - (p /. i)
let p be Point of (TOP-REAL n); ::_thesis: for i being Element of NAT st i in Seg n holds
(- p) /. i = - (p /. i)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (- p) /. i = - (p /. i) )
assume A1: i in Seg n ; ::_thesis: (- p) /. i = - (p /. i)
reconsider w1 = p as Element of REAL n by EUCLID:22;
 len w1 = n by CARD_1:def_7;
then A2: i in dom w1 by A1, FINSEQ_1:def_3;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
A3: p /. i = w3 . i by A2, PARTFUN1:def_6;
reconsider w = - p as Element of REAL n by EUCLID:22;
 len w = n by CARD_1:def_7;
then  i in dom w by A1, FINSEQ_1:def_3;
then (- p) /. i = w . i by PARTFUN1:def_6
.= (- w3) . i
.= (- 1) * (p /. i) by A3, RVSUM_1:45
.= - (p /. i) ;
hence  (- p) /. i = - (p /. i) ; ::_thesis: verum
end;

theorem :: JORDAN2B:5
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 + p2) /. i = (p1 /. i) + (p2 /. i)
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 + p2) /. i = (p1 /. i) + (p2 /. i)
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for i being Element of NAT st i in Seg n holds
(p1 + p2) /. i = (p1 /. i) + (p2 /. i)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (p1 + p2) /. i = (p1 /. i) + (p2 /. i) )
reconsider w1 = p1 as Element of REAL n by EUCLID:22;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w5 = p2 as Element of REAL n by EUCLID:22;
reconsider w7 = w5 as Element of n -tuples_on REAL ;
reconsider w = p1 + p2 as Element of REAL n by EUCLID:22;
assume A1: i in Seg n ; ::_thesis: (p1 + p2) /. i = (p1 /. i) + (p2 /. i)
then  i in Seg (len w) by CARD_1:def_7;
then A2: i in dom w by FINSEQ_1:def_3;
 len w5 = n by CARD_1:def_7;
then  i in dom w5 by A1, FINSEQ_1:def_3;
then A3: p2 /. i = w7 . i by PARTFUN1:def_6;
 len w1 = n by CARD_1:def_7;
then  i in dom w1 by A1, FINSEQ_1:def_3;
then A4: p1 /. i = w3 . i by PARTFUN1:def_6;
(p1 + p2) /. i = w . i by A2, PARTFUN1:def_6
.= (w3 + w7) . i
.= (p1 /. i) + (p2 /. i) by A4, A3, RVSUM_1:11 ;
hence  (p1 + p2) /. i = (p1 /. i) + (p2 /. i) ; ::_thesis: verum
end;

theorem Th6: :: JORDAN2B:6
for n being Element of NAT
for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
proof
let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n holds
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for i being Element of NAT st i in Seg n holds
(p1 - p2) /. i = (p1 /. i) - (p2 /. i)
let i be Element of NAT ; ::_thesis: ( i in Seg n implies (p1 - p2) /. i = (p1 /. i) - (p2 /. i) )
reconsider w1 = p1 as Element of REAL n by EUCLID:22;
reconsider w3 = w1 as Element of n -tuples_on REAL ;
reconsider w5 = p2 as Element of REAL n by EUCLID:22;
reconsider w7 = w5 as Element of n -tuples_on REAL ;
reconsider w = p1 - p2 as Element of REAL n by EUCLID:22;
assume A1: i in Seg n ; ::_thesis: (p1 - p2) /. i = (p1 /. i) - (p2 /. i)
then  i in Seg (len w5) by CARD_1:def_7;
then A2: i in dom w5 by FINSEQ_1:def_3;
 len w1 = n by CARD_1:def_7;
then  i in dom w1 by A1, FINSEQ_1:def_3;
then A3: p1 /. i = w3 . i by PARTFUN1:def_6;
 len w = n by CARD_1:def_7;
then A4: i in dom w by A1, FINSEQ_1:def_3;
A5: p2 /. i = w7 . i by A2, PARTFUN1:def_6;
(p1 - p2) /. i = w . i by A4, PARTFUN1:def_6
.= (w3 - w7) . i
.= (p1 /. i) - (p2 /. i) by A3, A5, RVSUM_1:27 ;
hence  (p1 - p2) /. i = (p1 /. i) - (p2 /. i) ; ::_thesis: verum
end;

theorem Th7: :: JORDAN2B:7
for i, n being Element of NAT st i <= n holds
(0* n) | i = 0* i
proof
let i, n be Element of NAT ; ::_thesis: ( i <= n implies (0* n) | i = 0* i )
assume A1: i <= n ; ::_thesis: (0* n) | i = 0* i
then  i <= len (0* n) by CARD_1:def_7;
then A2: len ((0* n) | i) = i by FINSEQ_1:59;
A3: for j being Nat st 1 <= j & j <= i holds
((0* n) | i) . j = (0* i) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= i implies ((0* n) | i) . j = (0* i) . j )
assume that
A4: 1 <= j and
A5: j <= i ; ::_thesis: ((0* n) | i) . j = (0* i) . j
 j <= n by A1, A5, XXREAL_0:2;
then A6: j in Seg n by A4, FINSEQ_1:1;
A7: ((0* n) | i) . j = (n |-> 0) . j by A5, FINSEQ_3:112
.= 0 by A6, FUNCOP_1:7 ;
 j in Seg i by A4, A5, FINSEQ_1:1;
hence  ((0* n) | i) . j = (0* i) . j by A7, FUNCOP_1:7; ::_thesis: verum
end;
 i = len (0* i) by CARD_1:def_7;
hence  (0* n) | i = 0* i by A2, A3, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th8: :: JORDAN2B:8
for n, i being Element of NAT holds (0* n) /^ i = 0* (n -' i)
proof
let n, i be Element of NAT ; ::_thesis: (0* n) /^ i = 0* (n -' i)
A1: len ((0* n) /^ i) = (len (0* n)) -' i by RFINSEQ:29
.= n -' i by CARD_1:def_7 ;
A2: n = len (0* n) by CARD_1:def_7;
A3: for j being Nat st 1 <= j & j <= n -' i holds
((0* n) /^ i) . j = (0* (n -' i)) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= n -' i implies ((0* n) /^ i) . j = (0* (n -' i)) . j )
assume that
A4: 1 <= j and
A5: j <= n -' i ; ::_thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j
now__::_thesis:_not_n_<_i
assume  n < i ; ::_thesis: contradiction
then  n - i < i - i by XREAL_1:9;
hence  contradiction by A4, A5, XREAL_0:def_2; ::_thesis: verum
end;
then  n -' i = n - i by XREAL_1:233;
then A6: j + i <= (n - i) + i by A5, XREAL_1:6;
 1 <= j + i by A4, NAT_1:12;
then A7: j + i in Seg n by A6, FINSEQ_1:1;
A8: j in Seg (n -' i) by A4, A5, FINSEQ_1:1;
then A9: j in dom ((0* n) /^ i) by A1, FINSEQ_1:def_3;
now__::_thesis:_(_(_i_<=_len_(0*_n)_&_((0*_n)_/^_i)_._j_=_(0*_(n_-'_i))_._j_)_or_(_i_>_len_(0*_n)_&_((0*_n)_/^_i)_._j_=_(0*_(n_-'_i))_._j_)_)
percases ( i <= len (0* n) or i > len (0* n) ) ;
case i <= len (0* n) ; ::_thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j
hence ((0* n) /^ i) . j = (n |-> 0) . (j + i) by A9, RFINSEQ:def_1
.= 0 by A7, FUNCOP_1:7
.= (0* (n -' i)) . j by A8, FUNCOP_1:7 ;
::_thesis: verum
end;
caseA10: i > len (0* n) ; ::_thesis: ((0* n) /^ i) . j = (0* (n -' i)) . j
then  i - i > n - i by A2, XREAL_1:9;
then A11: n -' i = 0 by XREAL_0:def_2;
 ((0* n) /^ i) . j = (<*> REAL) . j by A10, RFINSEQ:def_1;
hence  ((0* n) /^ i) . j = (0* (n -' i)) . j by A11; ::_thesis: verum
end;
end;
end;
hence  ((0* n) /^ i) . j = (0* (n -' i)) . j ; ::_thesis: verum
end;
 n -' i = len (0* (n -' i)) by CARD_1:def_7;
hence  (0* n) /^ i = 0* (n -' i) by A1, A3, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th9: :: JORDAN2B:9
for i being Element of NAT holds Sum (0* i) = 0
proof
let i be Element of NAT ; ::_thesis: Sum (0* i) = 0
thus  Sum (0* i) = i * 0 by RVSUM_1:80
.= 0 ; ::_thesis: verum
end;

theorem Th10: :: JORDAN2B:10
for i, n being Element of NAT
for r being Real st i in Seg n holds
Sum ((0* n) +* (i,r)) = r
proof
let i, n be Element of NAT ; ::_thesis: for r being Real st i in Seg n holds
Sum ((0* n) +* (i,r)) = r
let r be Real; ::_thesis: ( i in Seg n implies Sum ((0* n) +* (i,r)) = r )
A1: len (0* n) = n by CARD_1:def_7;
reconsider w = 0* n as FinSequence of REAL ;
assume A2: i in Seg n ; ::_thesis: Sum ((0* n) +* (i,r)) = r
then A3: i <= n by FINSEQ_1:1;
 1 <= i by A2, FINSEQ_1:1;
then  i in dom (0* n) by A3, A1, FINSEQ_3:25;
then  Sum (w +* (i,r)) = Sum (((w | (i -' 1)) ^ <*r*>) ^ (w /^ i)) by FUNCT_7:98
.= (Sum (((0* n) | (i -' 1)) ^ <*r*>)) + (Sum ((0* n) /^ i)) by RVSUM_1:75
.= ((Sum ((0* n) | (i -' 1))) + (Sum <*r*>)) + (Sum ((0* n) /^ i)) by RVSUM_1:75
.= ((Sum ((0* n) | (i -' 1))) + r) + (Sum ((0* n) /^ i)) by FINSOP_1:11
.= ((Sum (0* (i -' 1))) + r) + (Sum ((0* n) /^ i)) by A3, Th7, NAT_D:44
.= (0 + r) + (Sum ((0* n) /^ i)) by Th9
.= (0 + r) + (Sum (0* (n -' i))) by Th8
.= r by Th9 ;
hence  Sum ((0* n) +* (i,r)) = r ; ::_thesis: verum
end;

theorem Th11: :: JORDAN2B:11
for n being Element of NAT
for q being Element of REAL n
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
proof
let n be Element of NAT ; ::_thesis: for q being Element of REAL n
for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let q be Element of REAL n; ::_thesis: for p being Point of (TOP-REAL n)
for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let p be Point of (TOP-REAL n); ::_thesis: for i being Element of NAT st i in Seg n & q = p holds
( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
let i be Element of NAT ; ::_thesis: ( i in Seg n & q = p implies ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 ) )
assume that
A1: i in Seg n and
A2: q = p ; ::_thesis: ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 )
A3: Sum ((0* n) +* (i,((p /. i) ^2))) = (p /. i) ^2 by A1, Th10;
 len (0* n) = n by CARD_1:def_7;
then  len ((0* n) +* (i,((p /. i) ^2))) = n by FUNCT_7:97;
then reconsider w1 = (0* n) +* (i,((p /. i) ^2)) as Element of n -tuples_on REAL by FINSEQ_2:92;
A4: len w1 = n by CARD_1:def_7;
reconsider w2 = sqr q as Element of n -tuples_on REAL ;
A5: Sum (sqr q) >= 0 by RVSUM_1:86;
A6: len q = n by CARD_1:def_7;
A7: for j being Nat st j in Seg n holds
w1 . j <= w2 . j
proof
let j be Nat; ::_thesis: ( j in Seg n implies w1 . j <= w2 . j )
assume A8: j in Seg n ; ::_thesis: w1 . j <= w2 . j
set r1 = w1 . j;
set r2 = w2 . j;
percases ( j = i or j <> i ) ;
supposeA9: j = i ; ::_thesis: w1 . j <= w2 . j
then  j in dom q by A1, A6, FINSEQ_1:def_3;
then A10: q /. j = q . j by PARTFUN1:def_6;
A11: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 i in dom w1 by A1, A4, FINSEQ_1:def_3;
then w1 . j = w1 /. i by A9, PARTFUN1:def_6
.= (q /. i) ^2 by A2, A1, A11, FUNCT_7:36 ;
hence  w1 . j <= w2 . j by A9, A10, VALUED_1:11; ::_thesis: verum
end;
supposeA12: j <> i ; ::_thesis: w1 . j <= w2 . j
A13: dom (0* n) = Seg (len (0* n)) by FINSEQ_1:def_3
.= Seg n by CARD_1:def_7 ;
 dom q = Seg n by A6, FINSEQ_1:def_3;
then  q /. j = q . j by A8, PARTFUN1:def_6;
then A14: w2 . j = (q /. j) ^2 by VALUED_1:11;
 j in dom w1 by A4, A8, FINSEQ_1:def_3;
then w1 . j = w1 /. j by PARTFUN1:def_6
.= (0* n) /. j by A8, A12, A13, FUNCT_7:37
.= (n |-> 0) . j by A8, A13, PARTFUN1:def_6
.= 0 by A8, FUNCOP_1:7 ;
hence  w1 . j <= w2 . j by A14, XREAL_1:63; ::_thesis: verum
end;
end;
end;
then  Sum w1 <= Sum w2 by RVSUM_1:82;
then  ( 0 <= (p /. i) ^2 & (p /. i) ^2 <= (sqrt (Sum (sqr q))) ^2 ) by A5, A3, SQUARE_1:def_2, XREAL_1:63;
then  sqrt ((p /. i) ^2) <= sqrt ((sqrt (Sum (sqr q))) ^2) by SQUARE_1:26;
then  abs (abs (p /. i)) <= sqrt ((sqrt (Sum (sqr q))) ^2) by COMPLEX1:72;
then  ( 0 <= |.q.| & abs (p /. i) <= abs (sqrt (Sum (sqr q))) ) by COMPLEX1:72;
then A15: abs (p /. i) <= sqrt (Sum (sqr q)) by ABSVALUE:def_1;
A16: p /. i <= abs (p /. i) by ABSVALUE:4;
 |.q.| ^2 = Sum (sqr q) by A5, SQUARE_1:def_2;
hence  ( p /. i <= |.q.| & (p /. i) ^2 <= |.q.| ^2 ) by A7, A3, A15, A16, RVSUM_1:82, XXREAL_0:2; ::_thesis: verum
end;

begin

theorem Th12: :: JORDAN2B:12
for n being Element of NAT
for s1 being real number
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 > p /. i  }  & i in Seg n holds
P is open
proof
let n be Element of NAT ; ::_thesis: for s1 being real number
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 > p /. i  }  & i in Seg n holds
P is open
let s1 be real number ; ::_thesis: for P being Subset of (TOP-REAL n)
for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 > p /. i  }  & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); ::_thesis: for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 > p /. i  }  & i in Seg n holds
P is open
let i be Element of NAT ; ::_thesis: ( P =  {  p where p is Point of (TOP-REAL n) : s1 > p /. i  }  & i in Seg n implies P is open )
assume A1: ( P =  {  p where p is Point of (TOP-REAL n) : s1 > p /. i  }  & i in Seg n ) ; ::_thesis: P is open
reconsider s1 = s1 as Real by XREAL_0:def_1;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider PP = P as Subset of (TopSpaceMetr (Euclid n)) ;
 for pe being Point of (Euclid n) st pe in P holds
ex r being real number st
( r > 0 & Ball (pe,r) c= P )
proof
let pe be Point of (Euclid n); ::_thesis: ( pe in P implies ex r being real number st
( r > 0 & Ball (pe,r) c= P ) )
assume  pe in P ; ::_thesis: ex r being real number st
( r > 0 & Ball (pe,r) c= P )
then consider p being Point of (TOP-REAL n) such that
A3: p = pe and
A4: s1 > p /. i by A1;
set r = (s1 - (p /. i)) / 2;
A5: s1 - (p /. i) > 0 by A4, XREAL_1:50;
 Ball (pe,((s1 - (p /. i)) / 2)) c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (pe,((s1 - (p /. i)) / 2)) or x in P )
assume  x in Ball (pe,((s1 - (p /. i)) / 2)) ; ::_thesis: x in P
then  x in  {  q where q is Element of (Euclid n) : dist (pe,q) < (s1 - (p /. i)) / 2  }  by METRIC_1:17;
then consider q being Element of (Euclid n) such that
A6: q = x and
A7: dist (pe,q) < (s1 - (p /. i)) / 2 ;
reconsider ppe = pe, pq = q as Point of (TOP-REAL n) by TOPREAL3:8;
reconsider pen = ppe, pqn = pq as Element of REAL n ;
 (Pitag_dist n) . (q,pe) = dist (q,pe) by METRIC_1:def_1;
then A8: |.(pqn - pen).| < (s1 - (p /. i)) / 2 by A7, EUCLID:def_6;
reconsider q = pq - ppe as Element of REAL n by EUCLID:22;
 (pq - ppe) /. i <= |.q.| by A1, Th11;
then  (pq - ppe) /. i <= |.(pqn - pen).| ;
then  (pq - ppe) /. i < (s1 - (p /. i)) / 2 by A8, XXREAL_0:2;
then  (pq /. i) - (ppe /. i) < (s1 - (p /. i)) / 2 by A1, Th6;
then A9: (p /. i) + ((s1 - (p /. i)) / 2) > pq /. i by A3, XREAL_1:19;
 (p /. i) + ((s1 - (p /. i)) / 2) = s1 - ((s1 - (p /. i)) / 2) ;
then  s1 > (p /. i) + ((s1 - (p /. i)) / 2) by A5, XREAL_1:44, XREAL_1:139;
then  s1 > pq /. i by A9, XXREAL_0:2;
hence  x in P by A1, A6; ::_thesis: verum
end;
hence  ex r being real number st
( r > 0 & Ball (pe,r) c= P ) by A5, XREAL_1:139; ::_thesis: verum
end;
then  PP is open by TOPMETR:15;
hence  P is open by A2, PRE_TOPC:30; ::_thesis: verum
end;

theorem Th13: :: JORDAN2B:13
for n being Element of NAT
for s1 being real number
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 < p /. i  }  & i in Seg n holds
P is open
proof
let n be Element of NAT ; ::_thesis: for s1 being real number
for P being Subset of (TOP-REAL n)
for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 < p /. i  }  & i in Seg n holds
P is open
let s1 be real number ; ::_thesis: for P being Subset of (TOP-REAL n)
for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 < p /. i  }  & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); ::_thesis: for i being Element of NAT st P =  {  p where p is Point of (TOP-REAL n) : s1 < p /. i  }  & i in Seg n holds
P is open
let i be Element of NAT ; ::_thesis: ( P =  {  p where p is Point of (TOP-REAL n) : s1 < p /. i  }  & i in Seg n implies P is open )
assume A1: ( P =  {  p where p is Point of (TOP-REAL n) : s1 < p /. i  }  & i in Seg n ) ; ::_thesis: P is open
reconsider s1 = s1 as Real by XREAL_0:def_1;
A2: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8;
then reconsider PP = P as Subset of (TopSpaceMetr (Euclid n)) ;
 for pe being Point of (Euclid n) st pe in P holds
ex r being real number st
( r > 0 & Ball (pe,r) c= P )
proof
let pe be Point of (Euclid n); ::_thesis: ( pe in P implies ex r being real number st
( r > 0 & Ball (pe,r) c= P ) )
assume  pe in P ; ::_thesis: ex r being real number st
( r > 0 & Ball (pe,r) c= P )
then consider p being Point of (TOP-REAL n) such that
A3: p = pe and
A4: s1 < p /. i by A1;
set r = ((p /. i) - s1) / 2;
A5: (p /. i) - s1 > 0 by A4, XREAL_1:50;
 Ball (pe,(((p /. i) - s1) / 2)) c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Ball (pe,(((p /. i) - s1) / 2)) or x in P )
assume  x in Ball (pe,(((p /. i) - s1) / 2)) ; ::_thesis: x in P
then  x in  {  q where q is Element of (Euclid n) : dist (pe,q) < ((p /. i) - s1) / 2  }  by METRIC_1:17;
then consider q being Element of (Euclid n) such that
A6: q = x and
A7: dist (pe,q) < ((p /. i) - s1) / 2 ;
reconsider ppe = pe, pq = q as Point of (TOP-REAL n) by TOPREAL3:8;
reconsider pen = ppe, pqn = pq as Element of REAL n ;
 (Pitag_dist n) . (pe,q) = dist (pe,q) by METRIC_1:def_1;
then A8: |.(pen - pqn).| < ((p /. i) - s1) / 2 by A7, EUCLID:def_6;
reconsider qq = ppe - pq as Element of REAL n by EUCLID:22;
 (ppe - pq) /. i <= |.qq.| by A1, Th11;
then  (ppe - pq) /. i <= |.(pen - pqn).| ;
then  (ppe - pq) /. i < ((p /. i) - s1) / 2 by A8, XXREAL_0:2;
then  (ppe /. i) - (pq /. i) < ((p /. i) - s1) / 2 by A1, Th6;
then  ((ppe /. i) - (pq /. i)) + (pq /. i) < (((p /. i) - s1) / 2) + (pq /. i) by XREAL_1:6;
then A9: (ppe /. i) - (((p /. i) - s1) / 2) < ((pq /. i) + (((p /. i) - s1) / 2)) - (((p /. i) - s1) / 2) by XREAL_1:9;
 (p /. i) - (((p /. i) - s1) / 2) = s1 + (((p /. i) - s1) / 2) ;
then  s1 < (p /. i) - (((p /. i) - s1) / 2) by A5, XREAL_1:29, XREAL_1:139;
then  s1 < pq /. i by A3, A9, XXREAL_0:2;
hence  x in P by A1, A6; ::_thesis: verum
end;
hence  ex r being real number st
( r > 0 & Ball (pe,r) c= P ) by A5, XREAL_1:139; ::_thesis: verum
end;
then  PP is open by TOPMETR:15;
hence  P is open by A2, PRE_TOPC:30; ::_thesis: verum
end;

theorem Th14: :: JORDAN2B:14
for n being Element of NAT
for P being Subset of (TOP-REAL n)
for a, b being real number
for i being Element of NAT st P =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  & i in Seg n holds
P is open
proof
let n be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL n)
for a, b being real number
for i being Element of NAT st P =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  & i in Seg n holds
P is open
let P be Subset of (TOP-REAL n); ::_thesis: for a, b being real number
for i being Element of NAT st P =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  & i in Seg n holds
P is open
let a, b be real number ; ::_thesis: for i being Element of NAT st P =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  & i in Seg n holds
P is open
let i be Element of NAT ; ::_thesis: ( P =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  & i in Seg n implies P is open )
assume that
A1: P =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  and
A2: i in Seg n ; ::_thesis: P is open
A3: P =  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }
proof
A4:  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  or x in P )
assume A5: x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  ; ::_thesis: x in P
then  x in  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  by XBOOLE_0:def_4;
then A6: ex p2 being Point of (TOP-REAL n) st
( x = p2 & p2 /. i < b ) ;
 x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  by A5, XBOOLE_0:def_4;
then  ex p1 being Point of (TOP-REAL n) st
( x = p1 & a < p1 /. i ) ;
hence  x in P by A1, A6; ::_thesis: verum
end;
 P c=  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  )
assume  x in P ; ::_thesis: x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }
then A7: ex p3 being Point of (TOP-REAL n) st
( p3 = x & a < p3 /. i & p3 /. i < b ) by A1;
then A8: x in  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  ;
 x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  by A7;
hence  x in  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  P =  {  p1 where p1 is Point of (TOP-REAL n) : a < p1 /. i  }  /\  {  p2 where p2 is Point of (TOP-REAL n) : p2 /. i < b  }  by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
  {  p where p is Point of (TOP-REAL n) : p /. i < b  }  c= the carrier of (TOP-REAL n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p where p is Point of (TOP-REAL n) : p /. i < b  }  or x in the carrier of (TOP-REAL n) )
assume  x in  {  p where p is Point of (TOP-REAL n) : p /. i < b  }  ; ::_thesis: x in the carrier of (TOP-REAL n)
then  ex p being Point of (TOP-REAL n) st
( x = p & p /. i < b ) ;
hence  x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
then reconsider P2 =  {  p where p is Point of (TOP-REAL n) : p /. i < b  }  as Subset of (TOP-REAL n) ;
  {  p where p is Point of (TOP-REAL n) : a < p /. i  }  c= the carrier of (TOP-REAL n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p where p is Point of (TOP-REAL n) : a < p /. i  }  or x in the carrier of (TOP-REAL n) )
assume  x in  {  p where p is Point of (TOP-REAL n) : a < p /. i  }  ; ::_thesis: x in the carrier of (TOP-REAL n)
then  ex p being Point of (TOP-REAL n) st
( x = p & a < p /. i ) ;
hence  x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
then reconsider P1 =  {  p where p is Point of (TOP-REAL n) : a < p /. i  }  as Subset of (TOP-REAL n) ;
 ( P1 is open & P2 is open ) by A2, Th12, Th13;
hence  P is open by A3, TOPS_1:11; ::_thesis: verum
end;

theorem Th15: :: JORDAN2B:15
for n being Element of NAT
for a, b being real number
for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
proof
let n be Element of NAT ; ::_thesis: for a, b being real number
for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
let a, b be real number ; ::_thesis: for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
let f be Function of (TOP-REAL n),R^1; ::_thesis: for i being Element of NAT st ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
let i be Element of NAT ; ::_thesis: ( ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) implies f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  )
assume A1: for p being Element of (TOP-REAL n) holds f . p = p /. i ; ::_thesis: f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
thus  f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  ::_thesis: verum
proof
A2: f "  {  s where s is Real : ( a < s & s < b )  }  c=  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f "  {  s where s is Real : ( a < s & s < b )  }  or x in  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  )
assume A3: x in f "  {  s where s is Real : ( a < s & s < b )  }  ; ::_thesis: x in  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }
then reconsider px = x as Element of (TOP-REAL n) ;
 f . x in  {  s where s is Real : ( a < s & s < b )  }  by A3, FUNCT_1:def_7;
then A4: ex s being Real st
( s = f . x & a < s & s < b ) ;
 f . px = px /. i by A1;
hence  x in  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  by A4; ::_thesis: verum
end;
A5: dom f = the carrier of (TOP-REAL n) by FUNCT_2:def_1;
  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  c= f "  {  s where s is Real : ( a < s & s < b )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  or x in f "  {  s where s is Real : ( a < s & s < b )  }  )
assume  x in  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  ; ::_thesis: x in f "  {  s where s is Real : ( a < s & s < b )  }
then consider p being Element of (TOP-REAL n) such that
A6: x = p and
A7: ( a < p /. i & p /. i < b ) ;
 f . x = p /. i by A1, A6;
then  f . x in  {  s where s is Real : ( a < s & s < b )  }  by A7;
hence  x in f "  {  s where s is Real : ( a < s & s < b )  }  by A5, A6, FUNCT_1:def_7; ::_thesis: verum
end;
hence  f "  {  s where s is Real : ( a < s & s < b )  }  =  {  p where p is Element of (TOP-REAL n) : ( a < p /. i & p /. i < b )  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

theorem Th16: :: JORDAN2B:16
for X being non empty TopSpace
for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st ( for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) holds
f is continuous
proof
let X be non empty TopSpace; ::_thesis: for M being non empty MetrSpace
for f being Function of X,(TopSpaceMetr M) st ( for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) holds
f is continuous
let M be non empty MetrSpace; ::_thesis: for f being Function of X,(TopSpaceMetr M) st ( for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) holds
f is continuous
let f be Function of X,(TopSpaceMetr M); ::_thesis: ( ( for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ) implies f is continuous )
assume A1: for r being real number
for u being Element of M
for P being Subset of (TopSpaceMetr M) st r > 0 & P = Ball (u,r) holds
f " P is open ; ::_thesis: f is continuous
A2: for P1 being Subset of (TopSpaceMetr M) st P1 is open holds
f " P1 is open
proof
let P1 be Subset of (TopSpaceMetr M); ::_thesis: ( P1 is open implies f " P1 is open )
assume A3: P1 is open ; ::_thesis: f " P1 is open
 for x being set holds
( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )
proof
let x be set ; ::_thesis: ( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) )
now__::_thesis:_(_x_in_f_"_P1_implies_ex_Q_being_Subset_of_X_st_
(_Q_is_open_&_Q_c=_f_"_P1_&_x_in_Q_)_)
assume A4: x in f " P1 ; ::_thesis: ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q )
then A5: x in dom f by FUNCT_1:def_7;
A6: f . x in P1 by A4, FUNCT_1:def_7;
then reconsider u = f . x as Element of M by TOPMETR:12;
consider r being real number  such that
A7: r > 0 and
A8: Ball (u,r) c= P1 by A3, A6, TOPMETR:15;
reconsider r = r as Real by XREAL_0:def_1;
reconsider PB = Ball (u,r) as Subset of (TopSpaceMetr M) by TOPMETR:12;
A9: f " PB c= f " P1 by A8, RELAT_1:143;
 f . x in Ball (u,r) by A7, TBSP_1:11;
then  x in f " (Ball (u,r)) by A5, FUNCT_1:def_7;
hence  ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) by A1, A7, A9; ::_thesis: verum
end;
hence  ( x in f " P1 iff ex Q being Subset of X st
( Q is open & Q c= f " P1 & x in Q ) ) ; ::_thesis: verum
end;
hence  f " P1 is open by TOPS_1:25; ::_thesis: verum
end;
 [#] (TopSpaceMetr M) <> {} ;
hence  f is continuous by A2, TOPS_2:43; ::_thesis: verum
end;

theorem Th17: :: JORDAN2B:17
for u being Point of RealSpace
for r, u1 being real number st u1 = u holds
Ball (u,r) =  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }
proof
let u be Point of RealSpace; ::_thesis: for r, u1 being real number st u1 = u holds
Ball (u,r) =  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }
let r, u1 be real number ; ::_thesis: ( u1 = u implies Ball (u,r) =  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  )
assume A1: u1 = u ; ::_thesis: Ball (u,r) =  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }
  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  =  {  q where q is Element of RealSpace : dist (u,q) < r  }
proof
A2:  {  q where q is Element of RealSpace : dist (u,q) < r  }  c=  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  q where q is Element of RealSpace : dist (u,q) < r  }  or x in  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  )
assume  x in  {  q where q is Element of RealSpace : dist (u,q) < r  }  ; ::_thesis: x in  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }
then consider q being Element of RealSpace such that
A3: x = q and
A4: dist (u,q) < r ;
reconsider s1 = q as Real by METRIC_1:def_13;
A5: abs (u1 - s1) < r by A1, A4, TOPMETR:11;
then  u1 - s1 < r by SEQ_2:1;
then  (u1 - s1) + s1 < r + s1 by XREAL_1:6;
then A6: u1 - r < (r + s1) - r by XREAL_1:9;
 - r < u1 - s1 by A5, SEQ_2:1;
then  (- r) + s1 < (u1 - s1) + s1 by XREAL_1:6;
then  (s1 - r) + r < u1 + r by XREAL_1:6;
hence  x in  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  by A3, A6; ::_thesis: verum
end;
  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  c=  {  q where q is Element of RealSpace : dist (u,q) < r  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  or x in  {  q where q is Element of RealSpace : dist (u,q) < r  }  )
assume  x in  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  ; ::_thesis: x in  {  q where q is Element of RealSpace : dist (u,q) < r  }
then consider s being Real such that
A7: x = s and
A8: u1 - r < s and
A9: s < u1 + r ;
reconsider q1 = s as Point of RealSpace by METRIC_1:def_13;
 s - r < (u1 + r) - r by A9, XREAL_1:9;
then A10: (s + (- r)) - s < u1 - s by XREAL_1:9;
 (u1 - r) + r < s + r by A8, XREAL_1:6;
then  u1 - s < (s + r) - s by XREAL_1:9;
then  abs (u1 - s) < r by A10, SEQ_2:1;
then  dist (u,q1) < r by A1, TOPMETR:11;
hence  x in  {  q where q is Element of RealSpace : dist (u,q) < r  }  by A7; ::_thesis: verum
end;
hence   {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  =  {  q where q is Element of RealSpace : dist (u,q) < r  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  Ball (u,r) =  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  by METRIC_1:17; ::_thesis: verum
end;

theorem Th18: :: JORDAN2B:18
for n being Element of NAT
for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f is continuous
proof
let n be Element of NAT ; ::_thesis: for f being Function of (TOP-REAL n),R^1
for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f is continuous
let f be Function of (TOP-REAL n),R^1; ::_thesis: for i being Element of NAT st i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) holds
f is continuous
let i be Element of NAT ; ::_thesis: ( i in Seg n & ( for p being Element of (TOP-REAL n) holds f . p = p /. i ) implies f is continuous )
assume that
A1: i in Seg n and
A2: for p being Element of (TOP-REAL n) holds f . p = p /. i ; ::_thesis: f is continuous
reconsider f1 = f as Function of (TOP-REAL n),(TopSpaceMetr RealSpace) by TOPMETR:def_6;
 for r being real number
for u being Element of RealSpace
for P being Subset of (TopSpaceMetr RealSpace) st r > 0 & P = Ball (u,r) holds
f1 " P is open
proof
let r be real number ; ::_thesis: for u being Element of RealSpace
for P being Subset of (TopSpaceMetr RealSpace) st r > 0 & P = Ball (u,r) holds
f1 " P is open
let u be Element of RealSpace; ::_thesis: for P being Subset of (TopSpaceMetr RealSpace) st r > 0 & P = Ball (u,r) holds
f1 " P is open
let P be Subset of (TopSpaceMetr RealSpace); ::_thesis: ( r > 0 & P = Ball (u,r) implies f1 " P is open )
assume that
 r > 0 and
A3: P = Ball (u,r) ; ::_thesis: f1 " P is open
reconsider u1 = u as Real by METRIC_1:def_13;
 Ball (u,r) =  {  s where s is Real : ( u1 - r < s & s < u1 + r )  }  by Th17;
then  f " (Ball (u,r)) =  {  p where p is Element of (TOP-REAL n) : ( u1 - r < p /. i & p /. i < u1 + r )  }  by A2, Th15;
hence  f1 " P is open by A1, A3, Th14; ::_thesis: verum
end;
hence  f is continuous by Th16, TOPMETR:def_6; ::_thesis: verum
end;

begin

theorem :: JORDAN2B:19
for s being Real holds abs <*s*> = <*(abs s)*>
proof
let s be Real; ::_thesis: abs <*s*> = <*(abs s)*>
 rng <*s*> c= dom absreal
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng <*s*> or x in dom absreal )
assume  x in rng <*s*> ; ::_thesis: x in dom absreal
then  x in {s} by FINSEQ_1:38;
then A1: x = s by TARSKI:def_1;
 dom absreal = REAL by FUNCT_2:def_1;
hence  x in dom absreal by A1; ::_thesis: verum
end;
then  dom <*s*> = dom (absreal * <*s*>) by RELAT_1:27;
then  Seg 1 = dom (abs <*s*>) by FINSEQ_1:def_8;
then A2: len (abs <*s*>) = 1 by FINSEQ_1:def_3;
A3: len <*(abs s)*> = 1 by FINSEQ_1:39;
 for j being Nat st 1 <= j & j <= len <*(abs s)*> holds
<*(abs s)*> . j = (abs <*s*>) . j
proof
let j be Nat; ::_thesis: ( 1 <= j & j <= len <*(abs s)*> implies <*(abs s)*> . j = (abs <*s*>) . j )
A4: ( <*s*> . 1 = s & <*s*> is Element of REAL 1 ) by FINSEQ_1:40, FINSEQ_2:98;
assume  ( 1 <= j & j <= len <*(abs s)*> ) ; ::_thesis: <*(abs s)*> . j = (abs <*s*>) . j
then A5: j = 1 by A3, XXREAL_0:1;
then  <*(abs s)*> . j = abs s by FINSEQ_1:40;
hence  <*(abs s)*> . j = (abs <*s*>) . j by A5, A4, VALUED_1:18; ::_thesis: verum
end;
hence  abs <*s*> = <*(abs s)*> by A2, A3, FINSEQ_1:14; ::_thesis: verum
end;

theorem Th20: :: JORDAN2B:20
for p being Element of (TOP-REAL 1) ex r being Real st p = <*r*>
proof
let p be Element of (TOP-REAL 1); ::_thesis: ex r being Real st p = <*r*>
 1 -tuples_on REAL = REAL 1 ;
then reconsider p9 = p as Element of 1 -tuples_on REAL by EUCLID:22;
 ex r being Real st p9 = <*r*> by FINSEQ_2:97;
hence  ex r being Real st p = <*r*> ; ::_thesis: verum
end;

notation
let r be real number ;
synonym |[r]| for <*r*>;
end;

definition
let r be real number ;
:: original: |[
redefine func|[r]| ->  Point of (TOP-REAL 1);
coherence
 |[r]| is Point of (TOP-REAL 1)
proof
reconsider r = r as Real by XREAL_0:def_1;
 <*r*> in REAL 1 by FINSEQ_2:98;
hence  |[r]| is Point of (TOP-REAL 1) by EUCLID:22; ::_thesis: verum
end;
end;

theorem :: JORDAN2B:21
for r being real number
for s being Real holds s * |[r]| = |[(s * r)]| by RVSUM_1:47;

theorem :: JORDAN2B:22
for r1, r2 being real number holds |[(r1 + r2)]| = |[r1]| + |[r2]| by RVSUM_1:13;

theorem :: JORDAN2B:23
for r1, r2 being real number st |[r1]| = |[r2]| holds
r1 = r2 by FINSEQ_1:76;

theorem Th24: :: JORDAN2B:24
for P being Subset of R^1
for b being real number st P =  {  s where s is Real : s < b  }  holds
P is open
proof
let P be Subset of R^1; ::_thesis: for b being real number st P =  {  s where s is Real : s < b  }  holds
P is open
let b be real number ; ::_thesis: ( P =  {  s where s is Real : s < b  }  implies P is open )
assume A1: P =  {  s where s is Real : s < b  }  ; ::_thesis: P is open
 for c being Point of RealSpace st c in P holds
ex r being real number st
( r > 0 & Ball (c,r) c= P )
proof
let c be Point of RealSpace; ::_thesis: ( c in P implies ex r being real number st
( r > 0 & Ball (c,r) c= P ) )
reconsider n = c as Real by METRIC_1:def_13;
reconsider r = b - n as Real ;
assume  c in P ; ::_thesis: ex r being real number st
( r > 0 & Ball (c,r) c= P )
then A2: ex s being Real st
( s = n & s < b ) by A1;
take  r ; ::_thesis: ( r > 0 & Ball (c,r) c= P )
now__::_thesis:_for_x_being_set_st_x_in_Ball_(c,r)_holds_
x_in_P
let x be set ; ::_thesis: ( x in Ball (c,r) implies x in P )
assume A3: x in Ball (c,r) ; ::_thesis: x in P
then reconsider t = x as Real by METRIC_1:def_13;
reconsider u = x as Point of RealSpace by A3;
 Ball (c,r) =  {  q where q is Element of RealSpace : dist (c,q) < r  }  by METRIC_1:17;
then  ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A3;
then  real_dist . (t,n) < r by METRIC_1:def_1, METRIC_1:def_13;
then A4: abs (t - n) < r by METRIC_1:def_12;
 t - n <= abs (t - n) by ABSVALUE:4;
then  t - n < b - n by A4, XXREAL_0:2;
then  t < b by XREAL_1:9;
hence  x in P by A1; ::_thesis: verum
end;
hence  ( r > 0 & Ball (c,r) c= P ) by A2, TARSKI:def_3, XREAL_1:50; ::_thesis: verum
end;
hence  P is open by TOPMETR:15, TOPMETR:def_6; ::_thesis: verum
end;

theorem Th25: :: JORDAN2B:25
for P being Subset of R^1
for a being real number st P =  {  s where s is Real : a < s  }  holds
P is open
proof
let P be Subset of R^1; ::_thesis: for a being real number st P =  {  s where s is Real : a < s  }  holds
P is open
let a be real number ; ::_thesis: ( P =  {  s where s is Real : a < s  }  implies P is open )
assume A1: P =  {  s where s is Real : a < s  }  ; ::_thesis: P is open
 for c being Point of RealSpace st c in P holds
ex r being real number st
( r > 0 & Ball (c,r) c= P )
proof
let c be Point of RealSpace; ::_thesis: ( c in P implies ex r being real number st
( r > 0 & Ball (c,r) c= P ) )
reconsider n = c as Real by METRIC_1:def_13;
reconsider r = n - a as Real ;
assume  c in P ; ::_thesis: ex r being real number st
( r > 0 & Ball (c,r) c= P )
then A2: ex s being Real st
( s = n & a < s ) by A1;
take  r ; ::_thesis: ( r > 0 & Ball (c,r) c= P )
now__::_thesis:_for_x_being_set_st_x_in_Ball_(c,r)_holds_
x_in_P
let x be set ; ::_thesis: ( x in Ball (c,r) implies x in P )
assume A3: x in Ball (c,r) ; ::_thesis: x in P
then reconsider t = x as Real by METRIC_1:def_13;
reconsider u = x as Point of RealSpace by A3;
 Ball (c,r) =  {  q where q is Element of RealSpace : dist (c,q) < r  }  by METRIC_1:17;
then  ex v being Element of RealSpace st
( v = u & dist (c,v) < r ) by A3;
then  real_dist . (n,t) < r by METRIC_1:def_1, METRIC_1:def_13;
then A4: abs (n - t) < r by METRIC_1:def_12;
 n - t <= abs (n - t) by ABSVALUE:4;
then  n - t < n - a by A4, XXREAL_0:2;
then  a < t by XREAL_1:10;
hence  x in P by A1; ::_thesis: verum
end;
hence  ( r > 0 & Ball (c,r) c= P ) by A2, TARSKI:def_3, XREAL_1:50; ::_thesis: verum
end;
hence  P is open by TOPMETR:15, TOPMETR:def_6; ::_thesis: verum
end;

theorem Th26: :: JORDAN2B:26
for P being Subset of R^1
for a, b being real number st P =  {  s where s is Real : ( a < s & s < b )  }  holds
P is open
proof
let P be Subset of R^1; ::_thesis: for a, b being real number st P =  {  s where s is Real : ( a < s & s < b )  }  holds
P is open
let a, b be real number ; ::_thesis: ( P =  {  s where s is Real : ( a < s & s < b )  }  implies P is open )
  {  w1 where w1 is Real : a < w1  }  c= the carrier of R^1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  w1 where w1 is Real : a < w1  }  or x in the carrier of R^1 )
assume  x in  {  w1 where w1 is Real : a < w1  }  ; ::_thesis: x in the carrier of R^1
then  ex r1 being Real st
( x = r1 & a < r1 ) ;
hence  x in the carrier of R^1 by TOPMETR:17; ::_thesis: verum
end;
then reconsider P1 =  {  w1 where w1 is Real : a < w1  }  as Subset of R^1 ;
  {  w2 where w2 is Real : w2 < b  }  c= the carrier of R^1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  w2 where w2 is Real : w2 < b  }  or x in the carrier of R^1 )
assume  x in  {  w2 where w2 is Real : w2 < b  }  ; ::_thesis: x in the carrier of R^1
then  ex r2 being Real st
( x = r2 & r2 < b ) ;
hence  x in the carrier of R^1 by TOPMETR:17; ::_thesis: verum
end;
then reconsider P2 =  {  w2 where w2 is Real : w2 < b  }  as Subset of R^1 ;
assume A1: P =  {  s where s is Real : ( a < s & s < b )  }  ; ::_thesis: P is open
A2: P =  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }
proof
A3:  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }  c= P
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }  or x in P )
assume A4: x in  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }  ; ::_thesis: x in P
then  x in  {  w2 where w2 is Real : w2 < b  }  by XBOOLE_0:def_4;
then A5: ex r2 being Real st
( x = r2 & r2 < b ) ;
 x in  {  w1 where w1 is Real : a < w1  }  by A4, XBOOLE_0:def_4;
then  ex r1 being Real st
( x = r1 & a < r1 ) ;
hence  x in P by A1, A5; ::_thesis: verum
end;
 P c=  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P or x in  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }  )
assume  x in P ; ::_thesis: x in  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }
then A6: ex s being Real st
( s = x & a < s & s < b ) by A1;
then A7: x in  {  w2 where w2 is Real : w2 < b  }  ;
 x in  {  w1 where w1 is Real : a < w1  }  by A6;
hence  x in  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }  by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  P =  {  w1 where w1 is Real : a < w1  }  /\  {  w2 where w2 is Real : w2 < b  }  by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
 ( P1 is open & P2 is open ) by Th24, Th25;
hence  P is open by A2, TOPS_1:11; ::_thesis: verum
end;

theorem Th27: :: JORDAN2B:27
for u being Point of (Euclid 1)
for r, u1 being real number st <*u1*> = u holds
Ball (u,r) =  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }
proof
let u be Point of (Euclid 1); ::_thesis: for r, u1 being real number st <*u1*> = u holds
Ball (u,r) =  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }
let r, u1 be real number ; ::_thesis: ( <*u1*> = u implies Ball (u,r) =  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  )
assume A1: <*u1*> = u ; ::_thesis: Ball (u,r) =  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }
reconsider u1 = u1 as Real by XREAL_0:def_1;
  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  =  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }
proof
A2:  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }  c=  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }  or x in  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  )
assume  x in  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }  ; ::_thesis: x in  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }
then consider q being Element of (Euclid 1) such that
A3: x = q and
A4: dist (u,q) < r ;
reconsider eu = u, eq = q as Element of REAL 1 ;
 q is Tuple of 1, REAL by FINSEQ_2:131;
then consider s1 being Real such that
A5: q = <*s1*> by FINSEQ_2:97;
 <*u1*> - <*s1*> = <*(u1 - s1)*> by RVSUM_1:29;
then  sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2)*> by RVSUM_1:55;
then  Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2 by FINSOP_1:11;
then A6: sqrt (Sum (sqr (<*u1*> - <*s1*>))) = abs (u1 - s1) by COMPLEX1:72;
 (Pitag_dist 1) . (eu,eq) < r by A4, METRIC_1:def_1;
then A7: |.(<*u1*> - <*s1*>).| < r by A1, A5, EUCLID:def_6;
then  u1 - s1 < r by A6, SEQ_2:1;
then  (u1 - s1) + s1 < r + s1 by XREAL_1:6;
then A8: u1 - r < (r + s1) - r by XREAL_1:9;
 - r < u1 - s1 by A7, A6, SEQ_2:1;
then  (- r) + s1 < (u1 - s1) + s1 by XREAL_1:6;
then  (s1 - r) + r < u1 + r by XREAL_1:6;
hence  x in  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  by A3, A5, A8; ::_thesis: verum
end;
  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  c=  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }
proof
reconsider eu1 = <*u1*> as Element of REAL 1 by FINSEQ_2:98;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  or x in  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }  )
assume  x in  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  ; ::_thesis: x in  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }
then consider s being Real such that
A9: x = <*s*> and
A10: u1 - r < s and
A11: s < u1 + r ;
 s - r < (u1 + r) - r by A11, XREAL_1:9;
then A12: (s + (- r)) - s < u1 - s by XREAL_1:9;
reconsider es = <*s*> as Element of REAL 1 by FINSEQ_2:98;
reconsider q1 = <*s*> as Element of (Euclid 1) by FINSEQ_2:98;
 <*u1*> - <*s*> = <*(u1 - s)*> by RVSUM_1:29;
then  sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2)*> by RVSUM_1:55;
then A13: Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2 by FINSOP_1:11;
 (u1 - r) + r < s + r by A10, XREAL_1:6;
then  u1 - s < (s + r) - s by XREAL_1:9;
then  abs (u1 - s) < r by A12, SEQ_2:1;
then  |.(<*u1*> - <*s*>).| < r by A13, COMPLEX1:72;
then  ( the distance of (Euclid 1) . (u,q1) = dist (u,q1) & (Pitag_dist 1) . (eu1,es) < r ) by EUCLID:def_6, METRIC_1:def_1;
hence  x in  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }  by A1, A9; ::_thesis: verum
end;
hence   {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  =  {  q where q is Element of (Euclid 1) : dist (u,q) < r  }  by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  Ball (u,r) =  {  <*s*> where s is Real : ( u1 - r < s & s < u1 + r )  }  by METRIC_1:17; ::_thesis: verum
end;

theorem :: JORDAN2B:28
for f being Function of (TOP-REAL 1),R^1 st ( for p being Element of (TOP-REAL 1) holds f . p = p /. 1 ) holds
f is being_homeomorphism
proof
let f be Function of (TOP-REAL 1),R^1; ::_thesis: ( ( for p being Element of (TOP-REAL 1) holds f . p = p /. 1 ) implies f is being_homeomorphism )
assume A1: for p being Element of (TOP-REAL 1) holds f . p = p /. 1 ; ::_thesis: f is being_homeomorphism
A2: dom f = the carrier of (TOP-REAL 1) by FUNCT_2:def_1;
 REAL c= rng f
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL or x in rng f )
assume  x in REAL ; ::_thesis: x in rng f
then reconsider r = x as Real ;
A3: 1 <= len <*r*> by FINSEQ_1:40;
f . |[r]| = |[r]| /. 1 by A1
.= <*r*> . 1 by A3, FINSEQ_4:15
.= x by FINSEQ_1:40 ;
hence  x in rng f by A2, FUNCT_1:def_3; ::_thesis: verum
end;
then A4: ( [#] (TOP-REAL 1) = the carrier of (TOP-REAL 1) & rng f = [#] R^1 ) by TOPMETR:17, XBOOLE_0:def_10;
A5: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8;
then reconsider ff = f /" as Function of R^1,(TopSpaceMetr (Euclid 1)) ;
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A6: ( x1 in dom f & x2 in dom f ) and
A7: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider p1 = x1, p2 = x2 as Element of (TOP-REAL 1) by A6;
consider r1 being Real such that
A8: p1 = <*r1*> by Th20;
A9: 1 <= len <*r1*> by FINSEQ_1:40;
consider r2 being Real such that
A10: p2 = <*r2*> by Th20;
A11: 1 <= len <*r2*> by FINSEQ_1:40;
A12: f . p2 = p2 /. 1 by A1
.= <*r2*> . 1 by A10, A11, FINSEQ_4:15
.= r2 by FINSEQ_1:40 ;
f . p1 = p1 /. 1 by A1
.= <*r1*> . 1 by A8, A9, FINSEQ_4:15
.= r1 by FINSEQ_1:40 ;
hence  x1 = x2 by A7, A8, A10, A12; ::_thesis: verum
end;
then A13: f is one-to-one by FUNCT_1:def_4;
A14: f /" is continuous
proof
 TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8;
then reconsider g = f /" as Function of R^1,(TopSpaceMetr (Euclid 1)) ;
reconsider g1 = g as Function of the carrier of R^1, the carrier of (TOP-REAL 1) ;
 the carrier of R^1 c= rng f
proof
let z1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not z1 in the carrier of R^1 or z1 in rng f )
assume  z1 in the carrier of R^1 ; ::_thesis: z1 in rng f
then reconsider r1 = z1 as Real by TOPMETR:17;
 <*r1*> in REAL 1 by FINSEQ_2:98;
then reconsider q = <*r1*> as Element of (TOP-REAL 1) by EUCLID:22;
f . q = q /. 1 by A1
.= z1 by FINSEQ_4:16 ;
hence  z1 in rng f by A2, FUNCT_1:def_3; ::_thesis: verum
end;
then A15: rng f = the carrier of R^1 by XBOOLE_0:def_10;
 for r being real number
for u being Element of (Euclid 1)
for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball (u,r) holds
g " P is open
proof
reconsider f1 = f as Function of the carrier of (TOP-REAL 1), the carrier of R^1 ;
let r be real number ; ::_thesis: for u being Element of (Euclid 1)
for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball (u,r) holds
g " P is open
let u be Element of (Euclid 1); ::_thesis: for P being Subset of the carrier of (TopSpaceMetr (Euclid 1)) st r > 0 & P = Ball (u,r) holds
g " P is open
let P be Subset of the carrier of (TopSpaceMetr (Euclid 1)); ::_thesis: ( r > 0 & P = Ball (u,r) implies g " P is open )
assume that
 r > 0 and
A16: P = Ball (u,r) ; ::_thesis: g " P is open
 u is Tuple of 1, REAL by FINSEQ_2:131;
then consider s1 being Real such that
A17: u = <*s1*> by FINSEQ_2:97;
 dom f1 = the carrier of (TOP-REAL 1) by FUNCT_2:def_1;
then A18: dom f1 = REAL 1 by EUCLID:22;
A19: Ball (u,r) =  {  <*s*> where s is Real : ( s1 - r < s & s < s1 + r )  }  by A17, Th27;
A20: f1 .: (Ball (u,r)) =  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }
proof
A21: f1 .: (Ball (u,r)) c=  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in f1 .: (Ball (u,r)) or z in  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  )
assume  z in f1 .: (Ball (u,r)) ; ::_thesis: z in  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }
then consider x1 being set  such that
 x1 in dom f1 and
A22: x1 in Ball (u,r) and
A23: z = f1 . x1 by FUNCT_1:def_6;
consider s being Real such that
A24: <*s*> = x1 and
A25: ( s1 - r < s & s < s1 + r ) by A19, A22;
 <*s*> in REAL 1 by FINSEQ_2:98;
then reconsider q = <*s*> as Element of (TOP-REAL 1) by EUCLID:22;
A26: len <*s*> = 1 by FINSEQ_1:40;
z = q /. 1 by A1, A23, A24
.= <*s*> . 1 by A26, FINSEQ_4:15
.= s by FINSEQ_1:40 ;
hence  z in  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  by A25; ::_thesis: verum
end;
  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  c= f1 .: (Ball (u,r))
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  or z in f1 .: (Ball (u,r)) )
assume  z in  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  ; ::_thesis: z in f1 .: (Ball (u,r))
then consider r1 being Real such that
A27: z = r1 and
A28: ( s1 - r < r1 & r1 < s1 + r ) ;
 <*r1*> in REAL 1 by FINSEQ_2:98;
then reconsider q = <*r1*> as Element of (TOP-REAL 1) by EUCLID:22;
 Ball (u,r) =  {  <*s*> where s is Real : ( s1 - r < s & s < s1 + r )  }  by A17, Th27;
then A29: <*r1*> in Ball (u,r) by A28;
z = q /. 1 by A27, FINSEQ_4:16
.= f1 . <*r1*> by A1 ;
hence  z in f1 .: (Ball (u,r)) by A18, A29, FUNCT_1:def_6; ::_thesis: verum
end;
hence  f1 .: (Ball (u,r)) =  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  by A21, XBOOLE_0:def_10; ::_thesis: verum
end;
 f1 is onto by A15, FUNCT_2:def_3;
then  g1 = f1 " by A13, TOPS_2:def_4;
then  g1 " (Ball (u,r)) =  {  w1 where w1 is Real : ( s1 - r < w1 & w1 < s1 + r )  }  by A13, A20, FUNCT_1:84;
hence  g " P is open by A16, Th26; ::_thesis: verum
end;
then  ff is continuous by Th16;
hence  f /" is continuous by A5, PRE_TOPC:33; ::_thesis: verum
end;
 1 in Seg 1 by FINSEQ_1:1;
then  f is continuous by A1, Th18;
hence  f is being_homeomorphism by A2, A4, A13, A14, TOPS_2:def_5; ::_thesis: verum
end;

theorem Th29: :: JORDAN2B:29
for p being Element of (TOP-REAL 2) holds
( p /. 1 = p `1 & p /. 2 = p `2 )
proof
let p be Element of (TOP-REAL 2); ::_thesis: ( p /. 1 = p `1 & p /. 2 = p `2 )
reconsider r1 = p `1 , r2 = p `2 as Real ;
reconsider g = <*r1,r2*> as FinSequence of REAL by FINSEQ_2:13;
A1: p /. 2 = g /. 2 by EUCLID:53
.= p `2 by FINSEQ_4:17 ;
p /. 1 = g /. 1 by EUCLID:53
.= p `1 by FINSEQ_4:17 ;
hence  ( p /. 1 = p `1 & p /. 2 = p `2 ) by A1; ::_thesis: verum
end;

theorem :: JORDAN2B:30
for p being Element of (TOP-REAL 2) holds
( p /. 1 = proj1 . p & p /. 2 = proj2 . p )
proof
let p be Element of (TOP-REAL 2); ::_thesis: ( p /. 1 = proj1 . p & p /. 2 = proj2 . p )
A1: proj2 . p = p `2 by PSCOMP_1:def_6
.= p /. 2 by Th29 ;
proj1 . p = p `1 by PSCOMP_1:def_5
.= p /. 1 by Th29 ;
hence  ( p /. 1 = proj1 . p & p /. 2 = proj2 . p ) by A1; ::_thesis: verum
end;