jordan2b.miz

    begin

    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 be Nat, p be Element of ( TOP-REAL n) holds ex q be Real, g be 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 be Element of ( REAL * ) : ( len s) = n };

      then

      consider s be 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 :: JORDAN2B:1

    for n be Nat holds ex f be Function of ( TOP-REAL n), R^1 st for p be Element of ( TOP-REAL n) holds (f . p) = (p /. i)

    proof

      let n be Nat;

      defpred P[ object, object] means for p be Element of ( TOP-REAL n) st $1 = p holds $2 = (p /. i);



       A1: for x be object st x in ( REAL n) holds ex y be 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 be Real, g be FinSequence of REAL such that

         A2: g = px and q = (g /. i) by Lm1;

        for p be Element of ( TOP-REAL n) st x = p holds (g /. i) = (p /. i) by A2;

        hence thesis;

      end;

      ex f be Function of ( REAL n), REAL st for x be object st x in ( REAL n) holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

      then

      consider f be Function of ( REAL n), REAL such that

       A3: for x be object st x in ( REAL n) holds for p be 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 be 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 :: JORDAN2B:2

    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 :: JORDAN2B:3

    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 :: JORDAN2B:4

    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 :: JORDAN2B:5

    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 :: JORDAN2B:6



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



     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 :: JORDAN2B:8



     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 :: JORDAN2B:9



     Th9: ( Sum ( 0* i)) = 0

    proof



      thus ( Sum ( 0* i)) = (i * 0 ) by RVSUM_1: 80

      .= 0 ;

    end;

    theorem :: JORDAN2B:10



     Th10: for r be 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 :: JORDAN2B:11



     Th11: for q be 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

    theorem :: JORDAN2B:12



     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 be Point of ( Euclid n) st pe in P holds 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 be Element of ( Euclid n) : ( dist (pe,q)) < r } by METRIC_1: 17;

          then

          consider q be 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, XREAL_1: 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 :: JORDAN2B:13



     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 be Point of ( Euclid n) st pe in P holds 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 be Element of ( Euclid n) : ( dist (pe,q)) < r } by METRIC_1: 17;

          then

          consider q be 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, XREAL_1: 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 :: JORDAN2B:14



     Th14: for P be Subset of ( TOP-REAL n), a,b be Real, i st P = { p where p be 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 be 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 :: JORDAN2B:15



     Th15: for a,b be Real, f be Function of ( TOP-REAL n), R^1 , i st (for p be Element of ( TOP-REAL n) holds (f . p) = (p /. i)) holds (f " { s : a < s & s < b }) = { p where p be 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 be Element of ( TOP-REAL n) holds (f . p) = (p /. i);

      thus (f " { s : a < s & s < b }) = { p where p be Element of ( TOP-REAL n) : a < (p /. i) & (p /. i) < b }

      proof



         A2: (f " { s : a < s & s < b }) c= { p where p be 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 be 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 be Element of ( TOP-REAL n) : a < (p /. i) & (p /. i) < b };

          then

          consider p be 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 :: JORDAN2B:16



     Th16: for M be non empty MetrSpace, f be Function of X, ( TopSpaceMetr M) holds (for r be Real, u be Element of M, P be 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 be Real, u be Element of M, P be Subset of ( TopSpaceMetr M) st r > 0 & P = ( Ball (u,r)) holds (f " P) is open;



       A2: for P1 be 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 be 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 be 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 :: JORDAN2B:17



     Th17: for u be Point of RealSpace , r,u1 be 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 be Element of RealSpace : ( dist (u,q)) < r }

      proof



         A2: { q where q be 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 be Element of RealSpace : ( dist (u,q)) < r };

          then

          consider q be 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 be 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 :: JORDAN2B:18



     Th18: for f be Function of ( TOP-REAL n), R^1 , i st i in ( Seg n) & (for p be 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 be 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 be Real, u be Element of RealSpace , P be 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 be 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

    theorem :: JORDAN2B:19

    for s be 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 :: JORDAN2B:20



     Th20: for p be Element of ( TOP-REAL 1) holds ex r be 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;

      :: original: |[

      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 :: JORDAN2B:21

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

    theorem :: JORDAN2B:22

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

    theorem :: JORDAN2B:23

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

    theorem :: JORDAN2B:24



     Th24: for P be Subset of R^1 , b be 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 be Point of RealSpace st c in P holds ex r be 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 be Element of RealSpace : ( dist (c,q)) < r } by METRIC_1: 17;

          then ex v be 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: |.(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, TOPMETR:def 6;

    end;

    theorem :: JORDAN2B:25



     Th25: for P be Subset of R^1 , a be 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 be Point of RealSpace st c in P holds ex r be 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 be Element of RealSpace : ( dist (c,q)) < r } by METRIC_1: 17;

          then ex v be 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: |.(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, TOPMETR:def 6;

    end;

    theorem :: JORDAN2B:26



     Th26: for P be Subset of R^1 , a,b be 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 :: JORDAN2B:27



     Th27: for u be Point of ( Euclid 1), r,u1 be 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 be Element of ( Euclid 1) : ( dist (u,q)) < r }

      proof



         A2: { q where q be 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 be Element of ( Euclid 1) : ( dist (u,q)) < r };

          then

          consider q be 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 be 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 :: JORDAN2B:28

    for f be Function of ( TOP-REAL 1), R^1 st (for p be 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 be 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 be 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 be 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 be Real, u be Element of ( Euclid 1), P be 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 be 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 :: JORDAN2B:29



     Th29: for p be 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 :: JORDAN2B:30

    for p be 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;