:: 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;