:: Projections in n-Dimensional Euclidean Space to Each Coordinates
::  by Roman Matuszewski and Yatsuka Nakamura
::
:: Received November 3, 1997
:: Copyright (c) 1997-2018 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, REAL_1, SUBSET_1, XBOOLE_0, PRE_TOPC, EUCLID, NAT_1,
      FINSEQ_1, PARTFUN1, RELAT_1, FUNCT_1, TOPMETR, STRUCT_0, SUPINF_2,
      CARD_1, FINSEQ_2, ARYTM_1, ARYTM_3, XXREAL_0, RFINSEQ, CARD_3, FUNCT_4,
      ORDINAL4, COMPLEX1, SQUARE_1, RVSUM_1, RCOMP_1, PCOMPS_1, METRIC_1,
      TARSKI, ORDINAL2, TOPS_2, VALUED_1, MCART_1, FUNCT_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS, XCMPLX_0,
      XREAL_0, COMPLEX1, REAL_1, NAT_1, RVSUM_1, FUNCT_1, PARTFUN1, RELSET_1,
      FINSEQ_1, FUNCT_2, BINOP_1, RFINSEQ, FINSEQ_2, NAT_D, VALUED_0, STRUCT_0,
      TOPS_2, SQUARE_1, FUNCT_7, TOPMETR, PRE_TOPC, METRIC_1, RLVECT_1, EUCLID,
      PSCOMP_1, PCOMPS_1, FINSEQOP, XXREAL_0;
 constructors REAL_1, SQUARE_1, FINSEQOP, FINSEQ_4, FINSOP_1, RFINSEQ, NAT_D,
      FUNCT_7, TOPS_2, TOPMETR, PSCOMP_1, BINOP_2, FUNCSDOM, MONOID_0,
      PCOMPS_1, PRE_POLY;
 registrations XBOOLE_0, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0,
      METRIC_1, PCOMPS_1, EUCLID, TOPMETR, VALUED_0, FINSEQ_1, MONOID_0,
      RELSET_1, FUNCT_2, SQUARE_1, RVSUM_1, PRE_POLY, FUNCT_7, ORDINAL1;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, RELAT_1;
 equalities EUCLID, FINSEQ_2, RVSUM_1, SQUARE_1, STRUCT_0, VALUED_1;
 expansions TARSKI;
 theorems TARSKI, EUCLID, TOPMETR, TOPS_1, METRIC_1, FUNCT_1, RFINSEQ, FUNCT_2,
      RELAT_1, TBSP_1, NAT_1, FINSEQ_3, FINSEQ_1, ABSVALUE, SQUARE_1, FINSEQ_2,
      TOPS_2, RVSUM_1, TOPREAL3, FUNCOP_1, FINSEQ_4, FUNCT_7, SEQ_2, PSCOMP_1,
      XREAL_0, XBOOLE_0, COMPLEX1, XREAL_1, XXREAL_0, FINSOP_1, PARTFUN1,
      NAT_D, VALUED_1, PRE_TOPC, CARD_1;
 schemes FUNCT_2;

begin :: 1. PROJECTIONS

reserve x,x1,x2,y,z,z1 for set;
reserve s1,r,r1,r2 for Real;
reserve s,w1,w2 for Real;
reserve n,i for Element of NAT;
reserve X for non empty TopSpace;
reserve p,p1,p2,p3 for Point of TOP-REAL n;
reserve P for Subset of TOP-REAL n;

Lm1: for n,i being Nat,p being Element of TOP-REAL n ex q
being Real,g being FinSequence of REAL st g=p & q=g/.i
proof
  let n,i be Nat,p be Element of TOP-REAL n;
  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 thesis by A1;
end;

registration let n be Nat;
 cluster -> REAL-valued for Element of TOP-REAL n;
 coherence
  proof let p be Element of TOP-REAL n;
   let y be object;
   assume y in rng p;
   hence y in REAL by XREAL_0:def 1;
  end;
end;

theorem
  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 n be Nat;
  defpred P[object,object] means
   for p being Element of TOP-REAL n st $1=p holds $2= p/.i;
A1: for x being object st x in REAL n ex y being object st y in REAL & P[x,y]
  proof
    let x be object;
    assume x in REAL n;
    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 thesis;
  end;
  ex f being Function of REAL n,REAL st
for x being object st x in REAL n holds P[x,f.x] from FUNCT_2:sch 1(A1);
  then consider f being Function of REAL n,REAL such that
A3: for x being object st x in REAL n
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;
    p in the carrier of TOP-REAL n;
    then p in REAL n by EUCLID:22;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem
  for i st i in Seg n holds (0.TOP-REAL n)/.i=0
proof
  let i;
  assume
A1: i in Seg n;
  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 thesis;
end;

theorem
  for r,p,i st i in Seg n holds (r*p)/.i=r*p/.i
proof
  let 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;
  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 thesis;
end;

theorem
  for p,i st i in Seg n holds (-p)/.i=-p/.i
proof
  let p,i;
  assume
A1: i in Seg n;
  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 thesis;
end;

theorem
  for p1,p2,i st i in Seg n holds (p1+p2)/.i=p1/.i+p2/.i
proof
  let p1,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;
  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 thesis;
end;

theorem Th6:
  for p1,p2,i st i in Seg n holds (p1-p2)/.i=p1/.i-p2/.i
proof
  let p1,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;
  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 thesis;
end;

theorem Th7:
  i<=n implies (0*n) | i=0*i
proof
  assume
A1: i<=n;
  then i<=len (0*n) by CARD_1:def 7;
  then
A2: len ((0*n) | i)=i by FINSEQ_1:59;
A3: for j be Nat st 1<=j & j<=i holds ((0*n) | i).j=(0*i).j
  proof
    let j be Nat;
    assume that
A4: 1<=j and
A5: j<=i;
    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 thesis by A7,FUNCOP_1:7;
  end;
  i=len (0*i) by CARD_1:def 7;
  hence thesis by A2,A3,FINSEQ_1:14;
end;

theorem Th8:
  (0*n)/^i=0*(n-'i)
proof
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 be Nat st 1<=j & j<=n-'i holds ((0*n)/^i).j=(0*(n-'i)).j
  proof
    let j be Nat;
    assume that
A4: 1<=j and
A5: j<=n-'i;
    now
      assume n<i;
      then n-i<i-i by XREAL_1:9;
      hence contradiction by A4,A5,XREAL_0:def 2;
    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
      per cases;
      case
        i<=len (0*n);
        hence ((0*n)/^i).j=(n |-> (0 qua Real)).(j+i) by A9,RFINSEQ:def 1
          .=0 by A7,FUNCOP_1:7
          .= (0*(n-'i)).j by A8,FUNCOP_1:7;
      end;
      case
A10:    i>len (0*n);
        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 thesis by A11;
      end;
    end;
    hence thesis;
  end;
  n-'i=len (0*(n-'i)) by CARD_1:def 7;
  hence thesis by A1,A3,FINSEQ_1:14;
end;

theorem Th9:
  Sum(0*i)=0
proof
  thus Sum(0*i) = i*0 by RVSUM_1:80
    .= 0;
end;

theorem Th10:
  for r being Real st i in Seg n holds Sum((0*n)+*(i,r))=r
proof
  let r be Real;
A1: len(0*n) = n by CARD_1:def 7;
  reconsider w=0*n as FinSequence of REAL;
  assume
A2: i in Seg n;
  then
A3: i<=n by FINSEQ_1:1;
   reconsider r as Element of REAL by XREAL_0:def 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 thesis;
end;

theorem Th11:
  for q being Element of REAL n,p,i st i in Seg n & q=p
   holds p/.i<=|.q.| & (p/.i)^2<=|.q.|^2
proof
  let q be Element of REAL n,p,i;
  assume that
A1: i in Seg n and
A2: q=p;
    reconsider pd = (p/.i)^2 as Element of REAL by XREAL_0:def 1;
A3: Sum( (0*n)+*(i,pd))= pd by A1,Th10;
  len (0*n)=n by CARD_1:def 7;
  then len ((0*n)+*(i,pd))=n by FUNCT_7:97;
  then reconsider
  w1= (0*n)+*(i,pd) 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 be Nat st j in Seg n holds w1.j<=w2.j
  proof
    let j be Nat such that
A8: j in Seg n;
    set r1=w1.j, r2=w2.j;
    per cases;
    suppose
A9:   j=i;
      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 r1=w1/.i by A9,PARTFUN1:def 6
        .=(q/.i)^2 by A2,A1,A11,FUNCT_7:36;
      hence thesis by A9,A10,VALUED_1:11;
    end;
    suppose
A12:  j<>i;
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:  r2=(q/.j)^2 by VALUED_1:11;
      j in dom w1 by A4,A8,FINSEQ_1:def 3;
      then r1=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 thesis by A14,XREAL_1:63;
    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 |.|.p/.i.|.|<=sqrt((sqrt Sum sqr q)^2) by COMPLEX1:72;
  then 0<=|.q.| & |.p/.i.|<= |.sqrt Sum sqr q.| by COMPLEX1:72;
  then
A15: |.p/.i.|<=sqrt Sum sqr q by ABSVALUE:def 1;
A16: p/.i<=|.p/.i.| by ABSVALUE:4;
  |.q.|^2=Sum sqr q by A5,SQUARE_1:def 2;
  hence thesis by A7,A3,A15,A16,RVSUM_1:82,XXREAL_0:2;
end;

begin :: 2. CONTINUITY OF PROJECTIONS

theorem Th12:
  for s1,P,i st P = { p: s1>p/.i } & i in Seg n holds P is open
proof
  let s1,P,i such that
A1: P= { p:s1>p/.i } & i in Seg n;
  reconsider s1 as Real;
A2: the TopStruct 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 ex r be Real st r>0 &
  Ball(pe,r) c= P
  proof
    let pe be Point of Euclid n;
    assume pe in P;
    then consider p 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,r) c= P
    proof
      let x be object;
      assume x in Ball(pe,r);
      then x in {q where q is Element of Euclid n:dist(pe,q)<r} by METRIC_1:17;
      then consider q being Element of Euclid n such that
A6:   q=x and
A7:   dist(pe,q)<r;
      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.|<r 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 <r by A8,XXREAL_0:2;
      then pq/.i-ppe/.i < r 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-r;
      then s1> p/.i+(s1-p/.i)/2 by A5,XREAL_1:44,139;
      then s1>pq/.i by A9,XXREAL_0:2;
      hence thesis by A1,A6;
    end;
    hence thesis by A5,XREAL_1:139;
  end;
  then PP is open by TOPMETR:15;
  hence thesis by A2,PRE_TOPC:30;
end;

theorem Th13:
  for s1,P,i st P = { p: s1<p/.i } & i in Seg n holds P is open
proof
  let s1,P,i such that
A1: P= { p:s1<p/.i } & i in Seg n;
  reconsider s1 as Real;
A2: the TopStruct 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 ex r be Real st r>0 &
  Ball(pe,r) c= P
  proof
    let pe be Point of Euclid n;
    assume pe in P;
    then consider p 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,r) c= P
    proof
      let x be object;
      assume x in Ball(pe,r);
      then x in {q where q is Element of Euclid n:dist(pe,q)<r} by METRIC_1:17;
      then consider q being Element of Euclid n such that
A6:   q=x and
A7:   dist(pe,q)<r;
      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.|<r 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 <r by A8,XXREAL_0:2;
      then ppe/.i-pq/.i < r by A1,Th6;
      then ppe/.i-pq/.i+pq/.i < r+pq/.i by XREAL_1:6;
      then
A9:   ppe/.i-r < pq/.i+r-r by XREAL_1:9;
      p/.i-(p/.i-s1)/2 =s1+r;
      then s1< p/.i-(p/.i-s1)/2 by A5,XREAL_1:29,139;
      then s1<pq/.i by A3,A9,XXREAL_0:2;
      hence thesis by A1,A6;
    end;
    hence thesis by A5,XREAL_1:139;
  end;
  then PP is open by TOPMETR:15;
  hence thesis by A2,PRE_TOPC:30;
end;

theorem Th14:
  for P being Subset of TOP-REAL n,a,b being Real, i 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 P be Subset of TOP-REAL n,a,b be Real,i;
  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;
A3: P = { p1 :a<p1/.i} /\ {p2:p2/.i<b }
  proof
A4: { p1 :a<p1/.i} /\ {p2:p2/.i<b } c= P
    proof
      let x be object;
      assume
A5:   x in { p1 :a<p1/.i} /\ {p2:p2/.i<b };
      then x in {p2:p2/.i<b } by XBOOLE_0:def 4;
      then
A6:   ex p2 st x=p2 & p2/.i<b;
      x in { p1 :a<p1/.i} by A5,XBOOLE_0:def 4;
      then ex p1 st x=p1 & a<p1/.i;
      hence thesis by A1,A6;
    end;
    P c= { p1 :a<p1/.i} /\ {p2:p2/.i<b }
    proof
      let x be object;
      assume x in P;
      then
A7:   ex p3 st p3=x & a<p3/.i & p3/.i<b by A1;
      then
A8:   x in {p2:p2/.i<b };
      x in { p1 :a<p1/.i} by A7;
      hence thesis by A8,XBOOLE_0:def 4;
    end;
    hence thesis by A4,XBOOLE_0:def 10;
  end;
  { p:p/.i<b} c= the carrier of TOP-REAL n
  proof
    let x be object;
    assume x in { p:p/.i<b};
    then ex p st x= p & p/.i<b;
    hence thesis;
  end;
  then reconsider P2={ p:p/.i<b} as Subset of TOP-REAL n;
  { p:a<p/.i} c= the carrier of TOP-REAL n
  proof
    let x be object;
    assume x in { p:a<p/.i};
    then ex p st x= p & a<p/.i;
    hence thesis;
  end;
  then reconsider P1={ p:a<p/.i} as Subset of TOP-REAL n;
  P1 is open & P2 is open by A2,Th12,Th13;
  hence thesis by A3,TOPS_1:11;
end;

theorem Th15:
  for a,b being Real,f being Function of TOP-REAL n,R^1,i
st (for p being Element of TOP-REAL n holds f.p=p/.i) holds f"({s:a<s & s<
  b})={p where p is Element of TOP-REAL n: a<p/.i & p/.i<b}
proof
  let a,b be Real, f be Function of TOP-REAL n,R^1,i;
  assume
A1: for p being Element of TOP-REAL n holds f.p=p/.i;
  thus f"({s:a<s & s<b})={p where p is Element of TOP-REAL n: a<p/.i & p/.i<b}
  proof
A2: f"({s:a<s & s<b}) c= {p where p is Element of TOP-REAL n: a<p/.i & p/.i<b}
    proof
      let x be object;
      assume
A3:   x in f"({s:a<s & s<b});
      then reconsider px=x as Element of (TOP-REAL n);
      f.x in {s:a<s & s<b} by A3,FUNCT_1:def 7;
      then
A4:   ex s st s=f.x & a<s & s<b;
      f.px=px/.i by A1;
      hence thesis by A4;
    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:a<s & s<b})
    proof
      let x be object;
      assume x in {p where p is Element of TOP-REAL n: a<p/.i & p/.i<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:a<s & s<b} by A7;
      hence thesis by A5,A6,FUNCT_1:def 7;
    end;
    hence thesis by A2,XBOOLE_0:def 10;
  end;
end;

theorem Th16:
  for M being non empty MetrSpace,f being Function of X,
  TopSpaceMetr(M) holds (for r being Real,u being Element
of M,P being Subset of TopSpaceMetr(M) st r>0 & P=Ball(u,r) holds f"P is open)
  implies f is continuous
proof
  let M be non empty MetrSpace,f be Function of X,TopSpaceMetr(M);
  assume
A1: for r being Real, u being Element of M, P being Subset of
  TopSpaceMetr(M) st r>0 & P=Ball(u,r) holds f"P is open;
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);
    assume
A3: P1 is open;
    for x 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;
      now
        assume
A4:     x in f"P1;
        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 be Real such that
A7:     r>0 and
A8:     Ball(u,r) c= P1 by A3,A6,TOPMETR:15;
        reconsider r as Real;
        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;
      end;
      hence thesis;
    end;
    hence thesis by TOPS_1:25;
  end;
  [#]TopSpaceMetr M <> {};
  hence thesis by A2,TOPS_2:43;
end;

theorem Th17:
  for u being Point of RealSpace,r,u1 being Real st u1=u
  holds Ball(u,r)={s:u1-r<s & s<u1+r}
proof
  let u be Point of RealSpace,r,u1 be Real;
  assume
A1: u1=u;
  {s: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:u1-r<s & s<u1+ r}
    proof
      let x be object;
      assume x in {q where q is Element of RealSpace: dist(u,q)<r};
      then consider q being Element of RealSpace such that
A3:   x=q and
A4:   dist(u,q)<r;
      reconsider s1=q as Real;
A5:   |.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 thesis by A3,A6;
    end;
    {s:u1-r<s & s<u1+r} c= {q where q is Element of RealSpace:dist(u,q)<r}
    proof
      let x be object;
      assume x in {s:u1-r<s & s<u1+r};
      then consider s such that
A7:   x=s and
A8:   u1-r<s and
A9:   s<u1+r;
      s in REAL by XREAL_0:def 1;
      then 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 |.u1-s.| < r by A10,SEQ_2:1;
      then dist(u,q1)<r by A1,TOPMETR:11;
      hence thesis by A7;
    end;
    hence thesis by A2,XBOOLE_0:def 10;
  end;
  hence thesis by METRIC_1:17;
end;

theorem Th18:
  for f being Function of TOP-REAL n,R^1,i st i in Seg n & (for p
  being Element of TOP-REAL n holds f.p=p/.i) holds f is continuous
proof
  let f be Function of TOP-REAL n,R^1,i;
  assume that
A1: i in Seg n and
A2: for p being Element of TOP-REAL n holds f.p=p/.i;
  reconsider f1=f as Function of TOP-REAL n,TopSpaceMetr(RealSpace) by
TOPMETR:def 6;
  for r being Real,u being Element of RealSpace,P
being Subset of TopSpaceMetr(RealSpace) st r>0 & P=Ball(u,r) holds f1"P is open
  proof
    let r be Real, u be Element of RealSpace, P be
    Subset of TopSpaceMetr RealSpace;
    assume that
    r>0 and
A3: P=Ball(u,r);
    reconsider u1=u as Real;
    Ball(u,r)={s: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 thesis by A1,A3,Th14;
  end;
  hence thesis by Th16,TOPMETR:def 6;
end;

begin ::3.   1-DIMENSIONAL AND 2-DIMENSIONAL CASES

theorem
  for s being Real holds abs <*s*>=<*|.s.|*>
proof
  let s be Real;
   reconsider s as Element of REAL by XREAL_0:def 1;
  rng <*s*> c= dom absreal
  proof
    let x be object;
    assume x in rng <*s*>;
    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 thesis by A1;
  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 <*|.s.|*>=1 by FINSEQ_1:39;
  for j be Nat st 1<=j & j<=len <*|.s.|*> holds <*|.s.|*>.j=(abs <*s*>) .j
  proof
    let j be Nat;
A4: <*s*>.1=s & <*s*> is Element of REAL 1 by FINSEQ_1:40,FINSEQ_2:98;
    assume 1<=j & j<=len <*|.s.|*>;
    then
A5: j=1 by A3,XXREAL_0:1;
    then <*|.s.|*>.j =|.s.| by FINSEQ_1:40;
    hence thesis by A5,A4,VALUED_1:18;
  end;
  hence thesis by A2,A3,FINSEQ_1:14;
end;

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

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

definition
  let r be Real;
  redefine func |[ r ]| -> Point of TOP-REAL 1;
  coherence
  proof
    reconsider r as Element of REAL by XREAL_0:def 1;
    <*r*> in REAL 1 by FINSEQ_2:98;
    hence thesis by EUCLID:22;
  end;
end;

theorem
  s*|[ r ]|=|[ s*r ]| by RVSUM_1:47;

theorem
  |[ r1+r2 ]|=|[ r1 ]|+|[ r2 ]| by RVSUM_1:13;

theorem
  |[r1]|=|[r2]| implies r1=r2 by FINSEQ_1:76;

theorem Th24:
  for P being Subset of R^1,b being Real st P = { s: s<b }
  holds P is open
proof
  let P be Subset of R^1,b be Real;
  assume
A1: P = { s: s<b };
  for c being Point of RealSpace st c in P ex r being Real st r > 0
  & Ball(c,r) c= P
  proof
    let c be Point of RealSpace;
    reconsider n = c as Element of REAL by METRIC_1:def 13;
    reconsider r = b-n as Element of REAL by XREAL_0:def 1;
    assume c in P;
    then
A2: ex s st s=n & s<b by A1;
    take r;
    now
      let x be object;
      assume
A3:   x in Ball(c,r);
      then reconsider t = x as Element of 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,def 13;
      then
A4:   |. t - n .| < r by METRIC_1:def 12;
      t - n <= |. 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;
    end;
    hence thesis by A2,XREAL_1:50;
  end;
  hence thesis by TOPMETR:15,def 6;
end;

theorem Th25:
  for P being Subset of R^1,a being Real st P = { s: a<s }
  holds P is open
proof
  let P be Subset of R^1,a be Real;
  assume
A1: P = { s: a<s };
  for c being Point of RealSpace st c in P ex r being Real st r > 0
  & Ball(c,r) c= P
  proof
    let c be Point of RealSpace;
    reconsider n = c as Element of REAL by METRIC_1:def 13;
    reconsider r = n-a as Real;
    assume c in P;
    then
A2: ex s st s=n & a<s by A1;
    take r;
    now
      let x be object;
      assume
A3:   x in Ball(c,r);
      then reconsider t = x as Element of 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,def 13;
      then
A4:   |. n - t .| < r by METRIC_1:def 12;
      n - t <= |. 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;
    end;
    hence thesis by A2,XREAL_1:50;
  end;
  hence thesis by TOPMETR:15,def 6;
end;

theorem Th26:
  for P being Subset of R^1,a,b being Real st P = { s: a<s
  & s<b } holds P is open
proof
  let P be Subset of R^1,a,b be Real;
  { w1:a<w1} c= the carrier of R^1
  proof
    let x be object;
    assume x in { w1:a<w1};
    then consider  r1 be Real such that
A1:   x= r1 & a<r1;
     r1 in REAL by XREAL_0:def 1;
    hence thesis by TOPMETR:17,A1;
  end;
  then reconsider P1={w1:a<w1} as Subset of R^1;
  {w2:w2<b} c= the carrier of R^1
  proof
    let x be object;
    assume x in {w2:w2<b};
    then consider r2 be Real such that
A2:   x= r2 & r2<b;
     r2 in REAL by XREAL_0:def 1;
    hence thesis by TOPMETR:17,A2;
  end;
  then reconsider P2={w2:w2<b} as Subset of R^1;
  assume
A3: P = { s: a<s & s<b };
A4: P = { w1: a<w1} /\ {w2: w2<b}
  proof
A5: { w1 :a<w1} /\ {w2:w2<b } c= P
    proof
      let x be object;
      assume
A6:   x in { w1 :a<w1} /\ {w2:w2<b };
      then x in {w2:w2<b } by XBOOLE_0:def 4;
      then
A7:   ex r2 be Real st x=r2 & r2<b;
      x in { w1 :a<w1} by A6,XBOOLE_0:def 4;
      then ex r1 be Real st x=r1 & a<r1;
      hence thesis by A3,A7;
    end;
    P c= {w1: a<w1} /\ {w2: w2<b }
    proof
      let x be object;
      assume x in P;
      then
A8:   ex s st s=x & a<s & s<b by A3;
      then
A9:   x in {w2:w2<b };
      x in { w1 :a<w1} by A8;
      hence thesis by A9,XBOOLE_0:def 4;
    end;
    hence thesis by A5,XBOOLE_0:def 10;
  end;
  P1 is open & P2 is open by Th24,Th25;
  hence thesis by A4,TOPS_1:11;
end;

theorem Th27:
  for u being Point of Euclid 1,r,u1 being Real st <*u1*>=u
  holds Ball(u,r)={<*s*>:u1-r<s & s<u1+r}
proof
  let u be Point of Euclid 1,r,u1 be Real;
  assume
A1: <*u1*>=u;
  reconsider u1 as Element of REAL by XREAL_0:def 1;
  {<*s*>: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*>:u1-r<s & s< u1+r}
    proof
      let x be object;
      assume x in {q where q is Element of Euclid 1: dist(u,q)<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 be Element of REAL such that
A5:   q=<*s1*> by FINSEQ_2:97;
      reconsider us = (u1-s1)^2 as Element of REAL by XREAL_0:def 1;
      <*u1*>-<*s1*> =<*u1-s1*> by RVSUM_1:29;
      then sqr (<*u1*>-<*s1*>)=<*us*> by RVSUM_1:55;
      then Sum sqr (<*u1*>-<*s1*>)=(u1-s1)^2 by FINSOP_1:11;
      then
A6:   sqrt Sum sqr (<*u1*>-<*s1*>)=|.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 thesis by A3,A5,A8;
    end;
    {<*s*>: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 object;
      assume x in {<*s*>:u1-r<s & s<u1+r};
      then consider s 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 ss=s as Element of REAL by XREAL_0:def 1;
      reconsider es=<*ss*> as Element of REAL 1 by FINSEQ_2:98;
      reconsider q1=<*ss*> as Element of Euclid 1 by FINSEQ_2:98;
      reconsider uss = (u1-ss)^2 as Element of REAL by XREAL_0:def 1;
      <*u1*>-<*ss*> =<*u1-ss*> by RVSUM_1:29;
      then sqr (<*u1*>-<*ss*>) =<*uss*> by RVSUM_1:55;
      then
A13:  Sum sqr (<*u1*>-<*ss*>)=(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 |.u1-s.| < r by A12,SEQ_2:1;
      then |.<*u1*>-<*ss*>.| < 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 thesis by A1,A9;
    end;
    hence thesis by A2,XBOOLE_0:def 10;
  end;
  hence thesis by METRIC_1:17;
end;

theorem
  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;
  assume
A1: for p being Element of TOP-REAL 1 holds f.p=p/.1;
A2: dom f=the carrier of TOP-REAL 1 by FUNCT_2:def 1;
  REAL c= rng f
  proof
    let x be object;
    assume x in REAL;
    then reconsider r=x as Element of 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 thesis by A2,FUNCT_1:def 3;
  end;
  then
A4: [#](TOP-REAL 1) = the carrier of TOP-REAL 1 & rng f=[#](R^1) by TOPMETR:17
,XBOOLE_0:def 10;
A5: the TopStruct 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 object st x1 in dom f & x2 in dom f & f.x1 = f.x2
    holds x1 = x2
  proof
    let x1,x2 be object;
    assume that
A6: x1 in dom f & x2 in dom f and
A7: f.x1 = f.x2;
    reconsider p1=x1, p2=x2 as Element of TOP-REAL 1 by A6;
    consider r1 be Real such that
A8: p1=<*r1*> by Th20;
A9: 1<=len <*r1*> by FINSEQ_1:40;
    reconsider r1 as Element of REAL by XREAL_0:def 1;
    consider r2 being Real such that
A10: p2=<*r2*> by Th20;
A11: 1<=len <*r2*> by FINSEQ_1:40;
    reconsider r2 as Element of REAL by XREAL_0:def 1;
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 thesis by A7,A8,A10,A12;
  end;
  then
A13: f is one-to-one by FUNCT_1:def 4;
A14: f/" is continuous
  proof
    the TopStruct 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 object;
      assume z1 in the carrier of R^1;
      then reconsider r1=z1 as Element of 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 thesis by A2,FUNCT_1:def 3;
    end;
    then
A15: rng f= the carrier of R^1 by XBOOLE_0:def 10;
    for r being Real,u being Element of Euclid 1,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,u be Element of Euclid 1,P be Subset
      of the carrier of TopSpaceMetr(Euclid 1);
      assume that
      r>0 and
A16:  P=Ball(u,r);
      u is Tuple of 1,REAL by FINSEQ_2:131;
      then consider s1 be Element of 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*>:s1-r<s & s<s1+r} by A17,Th27;
A20:  f1.:(Ball(u,r))={w1:s1-r<w1 & w1<s1+r}
      proof
A21:    f1.:(Ball(u,r))c={w1:s1-r<w1 & w1<s1+r}
        proof
          let z be object;
          assume z in f1.:(Ball(u,r));
          then consider x1 being object 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 such that
A24:      <*s*>=x1 and
A25:      s1-r<s & s<s1+r by A19,A22;
          reconsider ss=s as Element of REAL by XREAL_0:def 1;
          <*ss*> 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
            .=<*ss*>.1 by A26,FINSEQ_4:15
            .=s by FINSEQ_1:40;
          hence thesis by A25;
        end;
        {w1:s1-r<w1 & w1<s1+r} c= f1.:(Ball(u,r))
        proof
          let z be object;
          assume z in {w1:s1-r<w1 & w1<s1+r};
          then consider r1 be Real such that
A27:      z=r1 and
A28:      s1-r<r1 & r1<s1+r;
          reconsider rr=r1 as Element of REAL by XREAL_0:def 1;
          <*rr*> in REAL 1 by FINSEQ_2:98;
          then reconsider q=<*rr*> as Element of TOP-REAL 1 by EUCLID:22;
          Ball(u,r)={<*s*>: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 thesis by A18,A29,FUNCT_1:def 6;
        end;
        hence thesis by A21,XBOOLE_0:def 10;
      end;
      f1 is onto by A15,FUNCT_2:def 3;
      then g1=(f1 qua Function)" by A13,TOPS_2:def 4;
      then g1"(Ball(u,r))={w1:s1-r<w1 & w1<s1+r} by A13,A20,FUNCT_1:84;
      hence thesis by A16,Th26;
    end;
    then ff is continuous by Th16;
    hence f/" is continuous by A5,PRE_TOPC:33;
  end;
  1 in Seg 1 by FINSEQ_1:1;
  then f is continuous by A1,Th18;
  hence thesis by A2,A4,A13,A14,TOPS_2:def 5;
end;

theorem Th29:
  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;
  reconsider r1=p`1,r2=p`2 as Element of REAL by XREAL_0:def 1;
  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 thesis by A1;
end;

theorem
  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;
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 thesis by A1;
end;