:: 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 (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) 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

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

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)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-r0 & 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.|*> 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 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 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=u holds Ball(u,r)={<*s*>:u1-r=u; reconsider u1 as Element of REAL by XREAL_0:def 1; {<*s*>:u1-r:u1-r 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)-<*s1*>.| < r by A1,A5,EUCLID:def 6; then u1-s1 < r by A6,SEQ_2:1; then u1-s1+s1:u1-r as Element of REAL 1 by FINSEQ_2:98; let x be object; assume x in {<*s*>:u1-r and A10: u1-r 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-<*ss*>.| < r by A13,COMPLEX1:72; then (the distance of Euclid 1).(u,q1)=dist(u,q1) & (Pitag_dist 1).(eu1, es) 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=x1 and A25: s1-r 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 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 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 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;