toprealb.miz



    begin

    set P2 = (2 * PI );

    set o = |[ 0 , 0 ]|;

    set R = the carrier of R^1 ;

    

     Lm1: 0 in INT by INT_1:def 1;

    reconsider p0 = ( - 1) as negative Real;

    reconsider p1 = 1 as positive Real;

    set CIT = ( Closed-Interval-TSpace (( - 1),1));

    set cCIT = the carrier of CIT;

    

     Lm2: cCIT = [.( - 1), 1.] by TOPMETR: 18;

    

     Lm3: (1 - 0 ) <= 1;

    

     Lm4: ((3 / 2) - (1 / 2)) <= 1;

    reserve n for Element of NAT ,

i for Integer,

a,b,r for Real,

x for Point of ( TOP-REAL n);

    registration

      cluster ]. 0 , 1.[ -> non empty;

      coherence ;

      cluster [.( - 1), 1.] -> non empty;

      coherence ;

      cluster ].(1 / 2), (3 / 2).[ -> non empty;

      coherence

      proof

         ].(1 / 2), ((1 / 2) + p1).[ is non empty;

        hence thesis;

      end;

    end

    

     Lm5: ( PI / 2) < ( PI / 1) by XREAL_1: 76;

    

     Lm6: (1 * PI ) < ((3 / 2) * PI ) by XREAL_1: 68;

    

     Lm7: ((3 / 2) * PI ) < (2 * PI ) by XREAL_1: 68;

    

     Lm8: for X be non empty TopSpace, Y be non empty SubSpace of X, Z be non empty SubSpace of Y, p be Point of Z holds p is Point of X

    proof

      let X be non empty TopSpace, Y be non empty SubSpace of X, Z be non empty SubSpace of Y, p be Point of Z;

      p is Point of Y by PRE_TOPC: 25;

      hence thesis by PRE_TOPC: 25;

    end;

    

     Lm9: for X be TopSpace, Y be SubSpace of X, Z be SubSpace of Y, A be Subset of Z holds A is Subset of X

    proof

      let X be TopSpace, Y be SubSpace of X, Z be SubSpace of Y, A be Subset of Z;

      the carrier of Z is Subset of Y by TSEP_1: 1;

      then

       A1: A is Subset of Y by XBOOLE_1: 1;

      the carrier of Y is Subset of X by TSEP_1: 1;

      hence thesis by A1, XBOOLE_1: 1;

    end;

    registration

      cluster sin -> continuous;

      coherence ;

      cluster cos -> continuous;

      coherence ;

      cluster arcsin -> continuous;

      coherence by RELAT_1: 69, SIN_COS6: 63, SIN_COS6: 84;

      cluster arccos -> continuous;

      coherence by RELAT_1: 69, SIN_COS6: 86, SIN_COS6: 107;

    end

    theorem :: TOPREALB:1

    

     Th1: ( sin ((a * r) + b)) = (( sin * ( AffineMap (a,b))) . r)

    proof

      

       A1: r in REAL by XREAL_0:def 1;

      

      thus ( sin ((a * r) + b)) = ( sin . ((a * r) + b)) by SIN_COS:def 17

      .= ( sin . (( AffineMap (a,b)) . r)) by FCONT_1:def 4

      .= (( sin * ( AffineMap (a,b))) . r) by A1, FUNCT_2: 15;

    end;

    theorem :: TOPREALB:2

    

     Th2: ( cos ((a * r) + b)) = (( cos * ( AffineMap (a,b))) . r)

    proof

      

       A1: r in REAL by XREAL_0:def 1;

      

      thus ( cos ((a * r) + b)) = ( cos . ((a * r) + b)) by SIN_COS:def 19

      .= ( cos . (( AffineMap (a,b)) . r)) by FCONT_1:def 4

      .= (( cos * ( AffineMap (a,b))) . r) by A1, FUNCT_2: 15;

    end;

    registration

      let a be non zero Real, b be Real;

      cluster ( AffineMap (a,b)) -> onto one-to-one;

      coherence by FCONT_1: 55, FCONT_1: 50;

    end

    definition

      let a,b be Real;

      :: TOPREALB:def1

      func IntIntervals (a,b) -> set equals the set of all ].(a + n), (b + n).[ where n be Element of INT ;

      coherence ;

    end

    theorem :: TOPREALB:3

    for x be set holds x in ( IntIntervals (a,b)) iff ex n be Element of INT st x = ].(a + n), (b + n).[;

    registration

      let a,b be Real;

      cluster ( IntIntervals (a,b)) -> non empty;

      coherence

      proof

         ].(a + 0 ), (b + 0 ).[ in ( IntIntervals (a,b)) by Lm1;

        hence thesis;

      end;

    end

    theorem :: TOPREALB:4

    (b - a) <= 1 implies ( IntIntervals (a,b)) is mutually-disjoint

    proof

      assume

       A1: (b - a) <= 1;

       A2:

      now

        let k be Element of NAT ;

        

         A3: ((a + 1) + 0 ) <= ((a + 1) + k) by XREAL_1: 6;

        ((b - a) + a) <= (1 + a) by A1, XREAL_1: 6;

        hence (a + (k + 1)) >= b by A3, XXREAL_0: 2;

      end;

      let x,y be set;

      assume x in ( IntIntervals (a,b));

      then

      consider nx be Element of INT such that

       A4: x = ].(a + nx), (b + nx).[;

      assume y in ( IntIntervals (a,b));

      then

      consider ny be Element of INT such that

       A5: y = ].(a + ny), (b + ny).[;

      assume

       A6: x <> y;

      assume x meets y;

      then

      consider z be object such that

       A7: z in x and

       A8: z in y by XBOOLE_0: 3;

      reconsider z as Real by A4, A7;

      

       A9: (a + nx) < z by A4, A7, XXREAL_1: 4;

      

       A10: z < (b + ny) by A5, A8, XXREAL_1: 4;

      

       A11: (a + ny) < z by A5, A8, XXREAL_1: 4;

      

       A12: z < (b + nx) by A4, A7, XXREAL_1: 4;

      per cases by XXREAL_0: 1;

        suppose nx = ny;

        hence contradiction by A4, A5, A6;

      end;

        suppose nx < ny;

        then (nx + 1) <= ny by INT_1: 7;

        then

        reconsider k = (ny - (nx + 1)) as Element of NAT by INT_1: 5;

        (((a + nx) + 1) + k) < (b + nx) by A12, A11, XXREAL_0: 2;

        then (((a + nx) + (k + 1)) - nx) < ((b + nx) - nx) by XREAL_1: 14;

        then (a + (k + 1)) < b;

        hence contradiction by A2;

      end;

        suppose nx > ny;

        then (ny + 1) <= nx by INT_1: 7;

        then

        reconsider k = (nx - (ny + 1)) as Element of NAT by INT_1: 5;

        (((a + ny) + 1) + k) < (b + ny) by A9, A10, XXREAL_0: 2;

        then (((a + ny) + (k + 1)) - ny) < ((b + ny) - ny) by XREAL_1: 14;

        then (a + (k + 1)) < b;

        hence contradiction by A2;

      end;

    end;

    definition

      let a,b be Real;

      :: original: IntIntervals

      redefine

      func IntIntervals (a,b) -> Subset-Family of R^1 ;

      coherence

      proof

        ( IntIntervals (a,b)) c= ( bool the carrier of R^1 )

        proof

          let x be object;

          assume x in ( IntIntervals (a,b));

          then ex n be Element of INT st x = ].(a + n), (b + n).[;

          hence thesis by TOPMETR: 17;

        end;

        hence thesis;

      end;

    end

    definition

      let a,b be Real;

      :: original: IntIntervals

      redefine

      func IntIntervals (a,b) -> open Subset-Family of R^1 ;

      coherence

      proof

        ( IntIntervals (a,b)) is open

        proof

          let A be Subset of R^1 ;

          assume A in ( IntIntervals (a,b));

          then ex n be Element of INT st A = ].(a + n), (b + n).[;

          hence thesis by JORDAN6: 35;

        end;

        hence thesis;

      end;

    end

    begin

    definition

      let r be Real;

      :: TOPREALB:def2

      func R^1 (r) -> Point of R^1 equals r;

      coherence by TOPMETR: 17, XREAL_0:def 1;

    end

    definition

      let A be Subset of REAL ;

      :: TOPREALB:def3

      func R^1 (A) -> Subset of R^1 equals A;

      coherence by TOPMETR: 17;

    end

    registration

      let A be non empty Subset of REAL ;

      cluster ( R^1 A) -> non empty;

      coherence ;

    end

    registration

      let A be open Subset of REAL ;

      cluster ( R^1 A) -> open;

      coherence by BORSUK_5: 39;

    end

    registration

      let A be closed Subset of REAL ;

      cluster ( R^1 A) -> closed;

      coherence by JORDAN5A: 23;

    end

    registration

      let A be open Subset of REAL ;

      cluster ( R^1 | ( R^1 A)) -> open;

      coherence by PRE_TOPC: 8;

    end

    registration

      let A be closed Subset of REAL ;

      cluster ( R^1 | ( R^1 A)) -> closed;

      coherence by PRE_TOPC: 8;

    end

    definition

      let f be PartFunc of REAL , REAL ;

      :: TOPREALB:def4

      func R^1 (f) -> Function of ( R^1 | ( R^1 ( dom f))), ( R^1 | ( R^1 ( rng f))) equals f;

      coherence

      proof

        

         A1: the carrier of ( R^1 | ( R^1 ( rng f))) = ( R^1 ( rng f)) by PRE_TOPC: 8;

        the carrier of ( R^1 | ( R^1 ( dom f))) = ( R^1 ( dom f)) by PRE_TOPC: 8;

        hence thesis by A1, FUNCT_2: 2;

      end;

    end

    registration

      let f be PartFunc of REAL , REAL ;

      cluster ( R^1 f) -> onto;

      coherence by PRE_TOPC: 8;

    end

    registration

      let f be one-to-one PartFunc of REAL , REAL ;

      cluster ( R^1 f) -> one-to-one;

      coherence ;

    end

    theorem :: TOPREALB:5

    

     Th5: ( R^1 | ( R^1 ( [#] REAL ))) = R^1

    proof

      ( [#] R^1 ) = ( R^1 ( [#] REAL )) by TOPMETR: 17;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: TOPREALB:6

    

     Th6: for f be PartFunc of REAL , REAL st ( dom f) = REAL holds ( R^1 | ( R^1 ( dom f))) = R^1

    proof

      let f be PartFunc of REAL , REAL ;

      assume ( dom f) = REAL ;

      then ( [#] R^1 ) = ( R^1 ( dom f)) by TOPMETR: 17;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: TOPREALB:7

    

     Th7: for f be Function of REAL , REAL holds f is Function of R^1 , ( R^1 | ( R^1 ( rng f)))

    proof

      let f be Function of REAL , REAL ;

       REAL = ( dom f) by FUNCT_2:def 1;

      then ( R^1 | ( R^1 ( dom f))) = R^1 by Th6;

      then ( R^1 f) is Function of R^1 , ( R^1 | ( R^1 ( rng f)));

      hence thesis;

    end;

    theorem :: TOPREALB:8

    

     Th8: for f be Function of REAL , REAL holds f is Function of R^1 , R^1

    proof

      let f be Function of REAL , REAL ;

      ( dom f) = REAL by FUNCT_2:def 1;

      then

      reconsider B = ( rng f) as non empty Subset of REAL by RELAT_1: 42;

      f is Function of R^1 , ( R^1 | ( R^1 B)) by Th7;

      hence thesis by TOPREALA: 7;

    end;

    

     Lm10: sin is Function of R^1 , R^1

    proof

      

       A1: sin = ( R^1 sin );

      ( R^1 | ( R^1 ( dom sin ))) = R^1 by Th6, SIN_COS: 24;

      hence thesis by A1, COMPTRIG: 28, TOPREALA: 7;

    end;

    

     Lm11: cos is Function of R^1 , R^1

    proof

      

       A1: cos = ( R^1 cos );

      ( R^1 | ( R^1 ( dom cos ))) = R^1 by Th6, SIN_COS: 24;

      hence thesis by A1, COMPTRIG: 29, TOPREALA: 7;

    end;

    registration

      let f be continuous PartFunc of REAL , REAL ;

      cluster ( R^1 f) -> continuous;

      coherence

      proof

        set g = ( R^1 f);

        per cases ;

          suppose ( dom f) is non empty;

          then

          reconsider A = ( dom f), B = ( rng f) as non empty Subset of REAL by RELAT_1: 42;

          reconsider g as Function of ( R^1 | ( R^1 A)), ( R^1 | ( R^1 B));

          reconsider h = g as Function of ( R^1 | ( R^1 A)), R^1 by TOPREALA: 7;

          for x be Point of ( R^1 | ( R^1 A)) holds h is_continuous_at x

          proof

            let x be Point of ( R^1 | ( R^1 A));

            let G be a_neighborhood of (h . x);

            consider Z be Neighbourhood of (f . x) qua Real such that

             A1: Z c= G by TOPREALA: 20;

            reconsider xx = x as Point of R^1 by PRE_TOPC: 25;

            the carrier of ( R^1 | ( R^1 A)) = A by PRE_TOPC: 8;

            then f is_continuous_in x by FCONT_1:def 2;

            then

            consider N be Neighbourhood of x such that

             A2: (f .: N) c= Z by FCONT_1: 5;

            consider g be Real such that

             A3: 0 < g and

             A4: N = ].(x - g), (x + g).[ by RCOMP_1:def 6;

            

             A5: (x + 0 ) < (x + g) by A3, XREAL_1: 6;

            reconsider NN = N as open Subset of R^1 by A4, JORDAN6: 35, TOPMETR: 17;

            reconsider M = (NN /\ ( [#] ( R^1 | ( R^1 A)))) as Subset of ( R^1 | ( R^1 A));

            

             A6: NN = ( Int NN) by TOPS_1: 23;

            (x - g) < (x - 0 ) by A3, XREAL_1: 15;

            then xx in ( Int NN) by A4, A6, A5, XXREAL_1: 4;

            then NN is open a_neighborhood of xx by CONNSP_2:def 1;

            then

            reconsider M as open a_neighborhood of x by TOPREALA: 5;

            take M;

            (h .: M) c= (h .: NN) by RELAT_1: 123, XBOOLE_1: 17;

            then (h .: M) c= Z by A2;

            hence thesis by A1;

          end;

          then h is continuous by TMAP_1: 44;

          hence thesis by PRE_TOPC: 27;

        end;

          suppose ( dom f) is empty;

          hence thesis;

        end;

      end;

    end

    set A = ( R^1 ]. 0 , 1.[);

     Lm12:

    now

      let a be non zero Real, b be Real;

      

       A1: ( rng ( AffineMap (a,b))) = REAL by FCONT_1: 55;

      

       A2: ( [#] R^1 ) = REAL by TOPMETR: 17;

      ( dom ( AffineMap (a,b))) = REAL by FUNCT_2:def 1;

      hence R^1 = ( R^1 | ( R^1 ( dom ( AffineMap (a,b))))) & R^1 = ( R^1 | ( R^1 ( rng ( AffineMap (a,b))))) by A1, A2, TSEP_1: 3;

    end;

    registration

      let a be non zero Real, b be Real;

      cluster ( R^1 ( AffineMap (a,b))) -> open;

      coherence

      proof

        let A be Subset of ( R^1 | ( R^1 ( dom ( AffineMap (a,b)))));

        

         A1: R^1 = ( R^1 | ( R^1 ( dom ( AffineMap (a,b))))) by Lm12;

        

         A2: R^1 = ( R^1 | ( R^1 ( rng ( AffineMap (a,b))))) by Lm12;

        ( R^1 ( AffineMap (a,b))) is being_homeomorphism by A1, A2, JORDAN16: 20;

        hence thesis by A1, A2, TOPGRP_1: 25;

      end;

    end

    begin

    definition

      let S be SubSpace of ( TOP-REAL 2);

      :: TOPREALB:def5

      attr S is being_simple_closed_curve means

      : Def5: the carrier of S is Simple_closed_curve;

    end

    registration

      cluster being_simple_closed_curve -> non empty pathwise_connected compact for SubSpace of ( TOP-REAL 2);

      coherence

      proof

        let S be SubSpace of ( TOP-REAL 2);

        assume

         A1: the carrier of S is Simple_closed_curve;

        then

        reconsider A = the carrier of S as Simple_closed_curve;

        A is non empty;

        hence the carrier of S is non empty;

        thus S is pathwise_connected by A1, TOPALG_3: 10;

        ( [#] S) = A;

        then ( [#] S) is compact by COMPTS_1: 2;

        hence thesis by COMPTS_1: 1;

      end;

    end

    registration

      let r be positive Real, x be Point of ( TOP-REAL 2);

      cluster ( Sphere (x,r)) -> being_simple_closed_curve;

      coherence

      proof

        reconsider a = x as Point of ( Euclid 2) by TOPREAL3: 8;

        

         A1: x = |[(x `1 ), (x `2 )]| by EUCLID: 53;

        ( Sphere (x,r)) = ( Sphere (a,r)) by TOPREAL9: 15

        .= ( circle ((x `1 ),(x `2 ),r)) by A1, TOPREAL9: 49

        .= { w where w be Point of ( TOP-REAL 2) : |.(w - |[(x `1 ), (x `2 )]|).| = r } by JGRAPH_6:def 5;

        hence thesis by JGRAPH_6: 23;

      end;

    end

    definition

      let n be Nat, x be Point of ( TOP-REAL n), r be Real;

      :: TOPREALB:def6

      func Tcircle (x,r) -> SubSpace of ( TOP-REAL n) equals (( TOP-REAL n) | ( Sphere (x,r)));

      coherence ;

    end

    registration

      let n be non zero Nat, x be Point of ( TOP-REAL n), r be non negative Real;

      cluster ( Tcircle (x,r)) -> strict non empty;

      coherence ;

    end

    theorem :: TOPREALB:9

    

     Th9: the carrier of ( Tcircle (x,r)) = ( Sphere (x,r))

    proof

      ( [#] ( Tcircle (x,r))) = ( Sphere (x,r)) by PRE_TOPC:def 5;

      hence thesis;

    end;

    registration

      let n be Nat, x be Point of ( TOP-REAL n), r be zero Real;

      cluster ( Tcircle (x,r)) -> trivial;

      coherence

      proof

        reconsider e = x as Point of ( Euclid n) by TOPREAL3: 8;

        n in NAT by ORDINAL1:def 12;

        

        then the carrier of ( Tcircle (x,r)) = ( Sphere (x,r)) by Th9

        .= ( Sphere (e,r)) by TOPREAL9: 15

        .= {e} by TOPREAL6: 54;

        hence thesis;

      end;

    end

    theorem :: TOPREALB:10

    

     Th10: ( Tcircle (( 0. ( TOP-REAL 2)),r)) is SubSpace of ( Trectangle (( - r),r,( - r),r))

    proof

      set C = ( Tcircle (( 0. ( TOP-REAL 2)),r));

      set T = ( Trectangle (( - r),r,( - r),r));

      the carrier of C c= the carrier of T

      proof

        let x be object;

        

         A1: ( closed_inside_of_rectangle (( - r),r,( - r),r)) = { p where p be Point of ( TOP-REAL 2) : ( - r) <= (p `1 ) & (p `1 ) <= r & ( - r) <= (p `2 ) & (p `2 ) <= r } by JGRAPH_6:def 2;

        assume

         A2: x in the carrier of C;

        reconsider x as Point of ( TOP-REAL 2) by A2, PRE_TOPC: 25;

        the carrier of C = ( Sphere (( 0. ( TOP-REAL 2)),r)) by Th9;

        then

         A3: |.x.| = r by A2, TOPREAL9: 12;

        

         A4: |.(x `2 ).| <= |.x.| by JGRAPH_1: 33;

        then

         A5: ( - r) <= (x `2 ) by A3, ABSVALUE: 5;

        

         A6: |.(x `1 ).| <= |.x.| by JGRAPH_1: 33;

        then

         A7: (x `1 ) <= r by A3, ABSVALUE: 5;

        

         A8: the carrier of ( Trectangle (( - r),r,( - r),r)) = ( closed_inside_of_rectangle (( - r),r,( - r),r)) by PRE_TOPC: 8;

        

         A9: (x `2 ) <= r by A3, A4, ABSVALUE: 5;

        ( - r) <= (x `1 ) by A3, A6, ABSVALUE: 5;

        hence thesis by A1, A8, A7, A5, A9;

      end;

      hence thesis by TSEP_1: 4;

    end;

    registration

      let x be Point of ( TOP-REAL 2), r be positive Real;

      cluster ( Tcircle (x,r)) -> being_simple_closed_curve;

      coherence by Th9;

    end

    registration

      cluster being_simple_closed_curve strict for SubSpace of ( TOP-REAL 2);

      existence

      proof

        set x = the Point of ( TOP-REAL 2), r = the positive Real;

        take ( Tcircle (x,r));

        thus thesis;

      end;

    end

    theorem :: TOPREALB:11

    for S,T be being_simple_closed_curve SubSpace of ( TOP-REAL 2) holds (S,T) are_homeomorphic

    proof

      let S,T be being_simple_closed_curve SubSpace of ( TOP-REAL 2);

      ( the TopStruct of S, the TopStruct of T) are_homeomorphic

      proof

        reconsider A = the carrier of the TopStruct of S as Simple_closed_curve by Def5;

        consider f be Function of (( TOP-REAL 2) | R^2-unit_square ), (( TOP-REAL 2) | A) such that

         A1: f is being_homeomorphism by TOPREAL2:def 1;

        

         A2: (f " ) is being_homeomorphism by A1, TOPS_2: 56;

        

         A3: ( [#] the TopStruct of S) = A;

         the TopStruct of S is strict SubSpace of ( TOP-REAL 2) by TMAP_1: 6;

        then

         A4: the TopStruct of S = (( TOP-REAL 2) | A) by A3, PRE_TOPC:def 5;

        reconsider B = the carrier of the TopStruct of T as Simple_closed_curve by Def5;

        consider g be Function of (( TOP-REAL 2) | R^2-unit_square ), (( TOP-REAL 2) | B) such that

         A5: g is being_homeomorphism by TOPREAL2:def 1;

        

         A6: ( [#] the TopStruct of T) = B;

        

         A7: the TopStruct of T is strict SubSpace of ( TOP-REAL 2) by TMAP_1: 6;

        then

        reconsider h = (g * (f " )) as Function of the TopStruct of S, the TopStruct of T by A4, A6, PRE_TOPC:def 5;

        take h;

         the TopStruct of T = (( TOP-REAL 2) | B) by A7, A6, PRE_TOPC:def 5;

        hence thesis by A5, A4, A2, TOPS_2: 57;

      end;

      hence thesis by TOPREALA: 15;

    end;

    definition

      let n be Nat;

      :: TOPREALB:def7

      func Tunit_circle (n) -> SubSpace of ( TOP-REAL n) equals ( Tcircle (( 0. ( TOP-REAL n)),1));

      coherence ;

    end

    set TUC = ( Tunit_circle 2);

    set cS1 = the carrier of TUC;

    

     Lm13: cS1 = ( Sphere ( |[ 0 , 0 ]|,1)) by Th9, EUCLID: 54;

    registration

      let n be non zero Nat;

      cluster ( Tunit_circle n) -> non empty;

      coherence ;

    end

    theorem :: TOPREALB:12

    

     Th12: for n be non zero Element of NAT , x be Point of ( TOP-REAL n) holds x is Point of ( Tunit_circle n) implies |.x.| = 1

    proof

      reconsider j = 1 as non negative Real;

      let n be non zero Element of NAT , x be Point of ( TOP-REAL n);

      assume x is Point of ( Tunit_circle n);

      then x in the carrier of ( Tcircle (( 0. ( TOP-REAL n)),j));

      then x in ( Sphere (( 0. ( TOP-REAL n)),1)) by Th9;

      hence thesis by TOPREAL9: 12;

    end;

    theorem :: TOPREALB:13

    

     Th13: for x be Point of ( TOP-REAL 2) st x is Point of ( Tunit_circle 2) holds ( - 1) <= (x `1 ) & (x `1 ) <= 1 & ( - 1) <= (x `2 ) & (x `2 ) <= 1

    proof

      let x be Point of ( TOP-REAL 2) such that

       A1: x is Point of ( Tunit_circle 2);

      consider a,b be Element of REAL such that

       A2: x = <*a, b*> by EUCLID: 51;

      

       A3: b = (x `2 ) by A2, EUCLID: 52;

      

       A4: a = (x `1 ) by A2, EUCLID: 52;

      

       A5: (1 ^2 ) = ( |.x.| ^2 ) by A1, Th12

      .= ((a ^2 ) + (b ^2 )) by A4, A3, JGRAPH_3: 1;

       0 <= (a ^2 ) by XREAL_1: 63;

      then ( - (a ^2 )) <= ( - 0 );

      then

       A6: ((b ^2 ) - 1) <= 0 by A5;

       0 <= (b ^2 ) by XREAL_1: 63;

      then ( - (b ^2 )) <= ( - 0 );

      then ((a ^2 ) - 1) <= 0 by A5;

      hence thesis by A4, A3, A6, SQUARE_1: 43;

    end;

    theorem :: TOPREALB:14

    

     Th14: for x be Point of ( TOP-REAL 2) st x is Point of ( Tunit_circle 2) & (x `1 ) = 1 holds (x `2 ) = 0

    proof

      let x be Point of ( TOP-REAL 2) such that

       A1: x is Point of ( Tunit_circle 2) and

       A2: (x `1 ) = 1;

      (1 ^2 ) = ( |.x.| ^2 ) by A1, Th12

      .= (((x `1 ) ^2 ) + ((x `2 ) ^2 )) by JGRAPH_3: 1;

      hence thesis by A2;

    end;

    theorem :: TOPREALB:15

    

     Th15: for x be Point of ( TOP-REAL 2) st x is Point of ( Tunit_circle 2) & (x `1 ) = ( - 1) holds (x `2 ) = 0

    proof

      let x be Point of ( TOP-REAL 2) such that

       A1: x is Point of ( Tunit_circle 2) and

       A2: (x `1 ) = ( - 1);

      (1 ^2 ) = ( |.x.| ^2 ) by A1, Th12

      .= (((x `1 ) ^2 ) + ((x `2 ) ^2 )) by JGRAPH_3: 1;

      hence thesis by A2;

    end;

    theorem :: TOPREALB:16

    for x be Point of ( TOP-REAL 2) st x is Point of ( Tunit_circle 2) & (x `2 ) = 1 holds (x `1 ) = 0

    proof

      let x be Point of ( TOP-REAL 2) such that

       A1: x is Point of ( Tunit_circle 2) and

       A2: (x `2 ) = 1;

      (1 ^2 ) = ( |.x.| ^2 ) by A1, Th12

      .= (((x `1 ) ^2 ) + ((x `2 ) ^2 )) by JGRAPH_3: 1;

      hence thesis by A2;

    end;

    theorem :: TOPREALB:17

    for x be Point of ( TOP-REAL 2) st x is Point of ( Tunit_circle 2) & (x `2 ) = ( - 1) holds (x `1 ) = 0

    proof

      let x be Point of ( TOP-REAL 2) such that

       A1: x is Point of ( Tunit_circle 2) and

       A2: (x `2 ) = ( - 1);

      (1 ^2 ) = ( |.x.| ^2 ) by A1, Th12

      .= (((x `1 ) ^2 ) + ((x `2 ) ^2 )) by JGRAPH_3: 1;

      hence thesis by A2;

    end;

    set TREC = ( Trectangle (p0,p1,p0,p1));

    theorem :: TOPREALB:18

    ( Tunit_circle 2) is SubSpace of ( Trectangle (( - 1),1,( - 1),1)) by Th10;

    theorem :: TOPREALB:19

    

     Th19: for n be non zero Element of NAT , r be positive Real, x be Point of ( TOP-REAL n), f be Function of ( Tunit_circle n), ( Tcircle (x,r)) st for a be Point of ( Tunit_circle n), b be Point of ( TOP-REAL n) st a = b holds (f . a) = ((r * b) + x) holds f is being_homeomorphism

    proof

      let n be non zero Element of NAT , r be positive Real, x be Point of ( TOP-REAL n), f be Function of ( Tunit_circle n), ( Tcircle (x,r)) such that

       A1: for a be Point of ( Tunit_circle n), b be Point of ( TOP-REAL n) st a = b holds (f . a) = ((r * b) + x);

      defpred P[ Point of ( TOP-REAL n), set] means $2 = ((r * $1) + x);

      set U = ( Tunit_circle n), C = ( Tcircle (x,r));

      

       A2: for u be Point of ( TOP-REAL n) holds ex y be Point of ( TOP-REAL n) st P[u, y];

      consider F be Function of ( TOP-REAL n), ( TOP-REAL n) such that

       A3: for x be Point of ( TOP-REAL n) holds P[x, (F . x)] from FUNCT_2:sch 3( A2);

      defpred R[ Point of ( TOP-REAL n), set] means $2 = ((1 / r) * ($1 - x));

      

       A4: for u be Point of ( TOP-REAL n) holds ex y be Point of ( TOP-REAL n) st R[u, y];

      consider G be Function of ( TOP-REAL n), ( TOP-REAL n) such that

       A5: for a be Point of ( TOP-REAL n) holds R[a, (G . a)] from FUNCT_2:sch 3( A4);

      set f2 = (( TOP-REAL n) --> x);

      set f1 = ( id ( TOP-REAL n));

      ( dom G) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1;

      then

       A6: ( dom (G | ( Sphere (x,r)))) = ( Sphere (x,r)) by RELAT_1: 62;

      for p be Point of ( TOP-REAL n) holds (G . p) = (((1 / r) * (f1 . p)) + (( - (1 / r)) * (f2 . p)))

      proof

        let p be Point of ( TOP-REAL n);

        

        thus (((1 / r) * (f1 . p)) + (( - (1 / r)) * (f2 . p))) = (((1 / r) * p) + (( - (1 / r)) * (f2 . p)))

        .= (((1 / r) * p) + (( - (1 / r)) * x))

        .= (((1 / r) * p) - ((1 / r) * x)) by RLVECT_1: 79

        .= ((1 / r) * (p - x)) by RLVECT_1: 34

        .= (G . p) by A5;

      end;

      then

       A7: G is continuous by TOPALG_1: 16;

      thus ( dom f) = ( [#] U) by FUNCT_2:def 1;

      

       A8: ( dom f) = the carrier of U by FUNCT_2:def 1;

      for p be Point of ( TOP-REAL n) holds (F . p) = ((r * (f1 . p)) + (1 * (f2 . p)))

      proof

        let p be Point of ( TOP-REAL n);

        

        thus ((r * (f1 . p)) + (1 * (f2 . p))) = ((r * (f1 . p)) + (f2 . p)) by RLVECT_1:def 8

        .= ((r * p) + (f2 . p))

        .= ((r * p) + x)

        .= (F . p) by A3;

      end;

      then

       A9: F is continuous by TOPALG_1: 16;

      

       A10: the carrier of C = ( Sphere (x,r)) by Th9;

      

       A11: the carrier of U = ( Sphere (( 0. ( TOP-REAL n)),1)) by Th9;

      

       A12: for a be object st a in ( dom f) holds (f . a) = ((F | ( Sphere (( 0. ( TOP-REAL n)),1))) . a)

      proof

        let a be object such that

         A13: a in ( dom f);

        reconsider y = a as Point of ( TOP-REAL n) by A13, PRE_TOPC: 25;

        

        thus (f . a) = ((r * y) + x) by A1, A13

        .= (F . y) by A3

        .= ((F | ( Sphere (( 0. ( TOP-REAL n)),1))) . a) by A11, A13, FUNCT_1: 49;

      end;

      

       A14: ((1 / r) * r) = 1 by XCMPLX_1: 87;

      thus

       A15: ( rng f) = ( [#] C)

      proof

        thus ( rng f) c= ( [#] C);

        let b be object;

        assume

         A16: b in ( [#] C);

        then

        reconsider c = b as Point of ( TOP-REAL n) by PRE_TOPC: 25;

        set a = ((1 / r) * (c - x));

         |.(a - ( 0. ( TOP-REAL n))).| = |.a.| by RLVECT_1: 13

        .= ( |.(1 / r).| * |.(c - x).|) by TOPRNS_1: 7

        .= ((1 / r) * |.(c - x).|) by ABSVALUE:def 1

        .= ((1 / r) * r) by A10, A16, TOPREAL9: 9;

        then

         A17: a in ( Sphere (( 0. ( TOP-REAL n)),1)) by A14;

        

        then (f . a) = ((r * a) + x) by A1, A11

        .= (((r * (1 / r)) * (c - x)) + x) by RLVECT_1:def 7

        .= ((c - x) + x) by A14, RLVECT_1:def 8

        .= b by RLVECT_4: 1;

        hence thesis by A11, A8, A17, FUNCT_1:def 3;

      end;

      thus

       A18: f is one-to-one

      proof

        let a,b be object such that

         A19: a in ( dom f) and

         A20: b in ( dom f) and

         A21: (f . a) = (f . b);

        reconsider a1 = a, b1 = b as Point of ( TOP-REAL n) by A11, A8, A19, A20;

        

         A22: (f . b1) = ((r * b1) + x) by A1, A20;

        (f . a1) = ((r * a1) + x) by A1, A19;

        then (r * a1) = (((r * b1) + x) - x) by A21, A22, RLVECT_4: 1;

        hence thesis by RLVECT_1: 36, RLVECT_4: 1;

      end;

      

       A23: for a be object st a in ( dom (f " )) holds ((f " ) . a) = ((G | ( Sphere (x,r))) . a)

      proof

        reconsider ff = f as Function;

        let a be object such that

         A24: a in ( dom (f " ));

        reconsider y = a as Point of ( TOP-REAL n) by A24, PRE_TOPC: 25;

        set e = ((1 / r) * (y - x));

        

         A25: f is onto by A15;

         |.(e - ( 0. ( TOP-REAL n))).| = |.e.| by RLVECT_1: 13

        .= ( |.(1 / r).| * |.(y - x).|) by TOPRNS_1: 7

        .= ((1 / r) * |.(y - x).|) by ABSVALUE:def 1

        .= ((1 / r) * r) by A10, A24, TOPREAL9: 9;

        then

         A26: ((1 / r) * (y - x)) in ( Sphere (( 0. ( TOP-REAL n)),1)) by A14;

        

        then (f . e) = ((r * e) + x) by A1, A11

        .= (((r * (1 / r)) * (y - x)) + x) by RLVECT_1:def 7

        .= ((y - x) + x) by A14, RLVECT_1:def 8

        .= y by RLVECT_4: 1;

        then ((ff " ) . a) = ((1 / r) * (y - x)) by A11, A8, A18, A26, FUNCT_1: 32;

        

        hence ((f " ) . a) = ((1 / r) * (y - x)) by A25, A18, TOPS_2:def 4

        .= (G . y) by A5

        .= ((G | ( Sphere (x,r))) . a) by A10, A24, FUNCT_1: 49;

      end;

      ( dom F) = the carrier of ( TOP-REAL n) by FUNCT_2:def 1;

      then ( dom (F | ( Sphere (( 0. ( TOP-REAL n)),1)))) = ( Sphere (( 0. ( TOP-REAL n)),1)) by RELAT_1: 62;

      hence f is continuous by A11, A8, A9, A12, BORSUK_4: 44, FUNCT_1: 2;

      ( dom (f " )) = the carrier of C by FUNCT_2:def 1;

      hence thesis by A10, A6, A7, A23, BORSUK_4: 44, FUNCT_1: 2;

    end;

    registration

      cluster ( Tunit_circle 2) -> being_simple_closed_curve;

      coherence ;

    end

    

     Lm14: for n be non zero Element of NAT , r be positive Real, x be Point of ( TOP-REAL n) holds (( Tunit_circle n),( Tcircle (x,r))) are_homeomorphic

    proof

      let n be non zero Element of NAT , r be positive Real, x be Point of ( TOP-REAL n);

      set U = ( Tunit_circle n), C = ( Tcircle (x,r));

      defpred P[ Point of U, set] means ex w be Point of ( TOP-REAL n) st w = $1 & $2 = ((r * w) + x);

      

       A1: the carrier of C = ( Sphere (x,r)) by Th9;

      

       A2: for u be Point of U holds ex y be Point of C st P[u, y]

      proof

        let u be Point of U;

        reconsider v = u as Point of ( TOP-REAL n) by PRE_TOPC: 25;

        set y = ((r * v) + x);

         |.(y - x).| = |.(r * v).| by RLVECT_4: 1

        .= ( |.r.| * |.v.|) by TOPRNS_1: 7

        .= (r * |.v.|) by ABSVALUE:def 1

        .= (r * 1) by Th12;

        then

        reconsider y as Point of C by A1, TOPREAL9: 9;

        take y;

        thus thesis;

      end;

      consider f be Function of U, C such that

       A3: for x be Point of U holds P[x, (f . x)] from FUNCT_2:sch 3( A2);

      take f;

      for a be Point of U, b be Point of ( TOP-REAL n) st a = b holds (f . a) = ((r * b) + x)

      proof

        let a be Point of U, b be Point of ( TOP-REAL n);

         P[a, (f . a)] by A3;

        hence thesis;

      end;

      hence thesis by Th19;

    end;

    theorem :: TOPREALB:20

    for n be non zero Element of NAT , r,s be positive Real, x,y be Point of ( TOP-REAL n) holds (( Tcircle (x,r)),( Tcircle (y,s))) are_homeomorphic

    proof

      let n be non zero Element of NAT , r,s be positive Real, x,y be Point of ( TOP-REAL n);

      

       A1: (( Tunit_circle n),( Tcircle (y,s))) are_homeomorphic by Lm14;

      (( Tcircle (x,r)),( Tunit_circle n)) are_homeomorphic by Lm14;

      hence thesis by A1, BORSUK_3: 3;

    end;

    registration

      let x be Point of ( TOP-REAL 2), r be non negative Real;

      cluster ( Tcircle (x,r)) -> pathwise_connected;

      coherence

      proof

        per cases ;

          suppose r is positive;

          then

          reconsider r as positive Real;

          ( Tcircle (x,r)) is pathwise_connected;

          hence thesis;

        end;

          suppose r is non positive;

          then

          reconsider r as non negative non positive Real;

          ( Tcircle (x,r)) is trivial;

          hence thesis;

        end;

      end;

    end

    definition

      :: TOPREALB:def8

      func c[10] -> Point of ( Tunit_circle 2) equals |[1, 0 ]|;

      coherence

      proof

        

         A1: ( |[1, 0 ]| `2 ) = 0 by EUCLID: 52;

        

         A2: ( |[1, 0 ]| `1 ) = 1 by EUCLID: 52;

         |.( |[(1 + 0 ), ( 0 + 0 )]| - o).| = |.(( |[1, 0 ]| + o) - o).| by EUCLID: 56

        .= |.( |[1, 0 ]| + (o - o)).| by RLVECT_1:def 3

        .= |.( |[1, 0 ]| + ( 0. ( TOP-REAL 2))).| by RLVECT_1: 5

        .= |. |[1, 0 ]|.| by RLVECT_1: 4

        .= ( sqrt ((1 ^2 ) + ( 0 ^2 ))) by A2, A1, JGRAPH_1: 30

        .= 1 by SQUARE_1: 22;

        hence thesis by Lm13, TOPREAL9: 9;

      end;

      :: TOPREALB:def9

      func c[-10] -> Point of ( Tunit_circle 2) equals |[( - 1), 0 ]|;

      coherence

      proof

        

         A3: ( |[( - 1), 0 ]| `2 ) = 0 by EUCLID: 52;

        

         A4: ( |[( - 1), 0 ]| `1 ) = ( - 1) by EUCLID: 52;

         |.( |[(( - 1) + 0 ), ( 0 + 0 )]| - o).| = |.(( |[( - 1), 0 ]| + o) - o).| by EUCLID: 56

        .= |.( |[( - 1), 0 ]| + (o - o)).| by RLVECT_1:def 3

        .= |.( |[( - 1), 0 ]| + ( 0. ( TOP-REAL 2))).| by RLVECT_1: 5

        .= |. |[( - 1), 0 ]|.| by RLVECT_1: 4

        .= ( sqrt ((( - 1) ^2 ) + ( 0 ^2 ))) by A4, A3, JGRAPH_1: 30

        .= ( sqrt ((1 ^2 ) + ( 0 ^2 )))

        .= 1 by SQUARE_1: 22;

        hence thesis by Lm13, TOPREAL9: 9;

      end;

    end

    

     Lm15: c[10] <> c[-10] by SPPOL_2: 1;

    definition

      let p be Point of ( Tunit_circle 2);

      :: TOPREALB:def10

      func Topen_unit_circle (p) -> strict SubSpace of ( Tunit_circle 2) means

      : Def10: the carrier of it = (the carrier of ( Tunit_circle 2) \ {p});

      existence

      proof

        reconsider A = (cS1 \ {p}) as Subset of TUC;

        take (TUC | A);

        thus thesis by PRE_TOPC: 8;

      end;

      uniqueness by TSEP_1: 5;

    end

    registration

      let p be Point of ( Tunit_circle 2);

      cluster ( Topen_unit_circle p) -> non empty;

      coherence

      proof

        set X = ( Topen_unit_circle p);

        

         A1: the carrier of X = (cS1 \ {p}) by Def10;

        per cases ;

          suppose

           A2: p = c[10] ;

          set x = |[ 0 , 1]|;

          reconsider r = p as Point of ( TOP-REAL 2) by PRE_TOPC: 25;

          

           A3: (x `1 ) = 0 by EUCLID: 52;

          

           A4: (x `2 ) = 1 by EUCLID: 52;

           |.( |[( 0 + 0 ), (1 + 0 )]| - o).| = |.((x + o) - o).| by EUCLID: 56

          .= |.(x + (o - o)).| by RLVECT_1:def 3

          .= |.(x + ( 0. ( TOP-REAL 2))).| by RLVECT_1: 5

          .= |.x.| by RLVECT_1: 4

          .= ( sqrt ((1 ^2 ) + ( 0 ^2 ))) by A3, A4, JGRAPH_1: 30

          .= 1 by SQUARE_1: 22;

          then

           A5: x in cS1 by Lm13;

          (r `1 ) = 1 by A2, EUCLID: 52;

          then not x in {p} by A3, TARSKI:def 1;

          hence the carrier of X is non empty by A1, A5, XBOOLE_0:def 5;

        end;

          suppose p <> c[10] ;

          then not c[10] in {p} by TARSKI:def 1;

          hence the carrier of X is non empty by A1, XBOOLE_0:def 5;

        end;

      end;

    end

    theorem :: TOPREALB:21

    

     Th21: for p be Point of ( Tunit_circle 2) holds not p is Point of ( Topen_unit_circle p)

    proof

      let p be Point of ( Tunit_circle 2);

      

       A1: p in {p} by TARSKI:def 1;

      the carrier of ( Topen_unit_circle p) = (the carrier of ( Tunit_circle 2) \ {p}) by Def10;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    theorem :: TOPREALB:22

    

     Th22: for p be Point of ( Tunit_circle 2) holds ( Topen_unit_circle p) = (( Tunit_circle 2) | (( [#] ( Tunit_circle 2)) \ {p}))

    proof

      let p be Point of ( Tunit_circle 2);

      ( [#] ( Topen_unit_circle p)) = (( [#] ( Tunit_circle 2)) \ {p}) by Def10;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: TOPREALB:23

    

     Th23: for p,q be Point of ( Tunit_circle 2) st p <> q holds q is Point of ( Topen_unit_circle p)

    proof

      let p,q be Point of ( Tunit_circle 2) such that

       A1: p <> q;

      the carrier of ( Topen_unit_circle p) = (the carrier of ( Tunit_circle 2) \ {p}) by Def10;

      hence thesis by A1, ZFMISC_1: 56;

    end;

    theorem :: TOPREALB:24

    

     Th24: for p be Point of ( TOP-REAL 2) st p is Point of ( Topen_unit_circle c[10] ) & (p `2 ) = 0 holds p = c[-10]

    proof

      let p be Point of ( TOP-REAL 2) such that

       A1: p is Point of ( Topen_unit_circle c[10] ) and

       A2: (p `2 ) = 0 ;

       A3:

      now

        assume (p `1 ) = 1;

        then p = c[10] by A2, EUCLID: 53;

        hence contradiction by A1, Th21;

      end;

      p is Point of TUC by A1, PRE_TOPC: 25;

      

      then (1 ^2 ) = ( |.p.| ^2 ) by Th12

      .= (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by JGRAPH_3: 1;

      then (p `1 ) = 1 or (p `1 ) = ( - 1) by A2, SQUARE_1: 41;

      hence thesis by A2, A3, EUCLID: 53;

    end;

    theorem :: TOPREALB:25

    

     Th25: for p be Point of ( TOP-REAL 2) st p is Point of ( Topen_unit_circle c[-10] ) & (p `2 ) = 0 holds p = c[10]

    proof

      let p be Point of ( TOP-REAL 2) such that

       A1: p is Point of ( Topen_unit_circle c[-10] ) and

       A2: (p `2 ) = 0 ;

       A3:

      now

        assume (p `1 ) = ( - 1);

        then p = c[-10] by A2, EUCLID: 53;

        hence contradiction by A1, Th21;

      end;

      p is Point of TUC by A1, PRE_TOPC: 25;

      

      then (1 ^2 ) = ( |.p.| ^2 ) by Th12

      .= (((p `1 ) ^2 ) + ((p `2 ) ^2 )) by JGRAPH_3: 1;

      then (p `1 ) = 1 or (p `1 ) = ( - 1) by A2, SQUARE_1: 41;

      hence thesis by A2, A3, EUCLID: 53;

    end;

    set TOUC = ( Topen_unit_circle c[10] );

    set TOUCm = ( Topen_unit_circle c[-10] );

    set X = the carrier of TOUC;

    set Xm = the carrier of TOUCm;

    set Y = the carrier of ( R^1 | ( R^1 ]. 0 , ( 0 + p1).[));

    set Ym = the carrier of ( R^1 | ( R^1 ].(1 / 2), ((1 / 2) + p1).[));

    

     Lm16: X = ( [#] TOUC);

    

     Lm17: Xm = ( [#] TOUCm);

    theorem :: TOPREALB:26

    

     Th26: for p be Point of ( Tunit_circle 2), x be Point of ( TOP-REAL 2) st x is Point of ( Topen_unit_circle p) holds ( - 1) <= (x `1 ) & (x `1 ) <= 1 & ( - 1) <= (x `2 ) & (x `2 ) <= 1

    proof

      let p be Point of ( Tunit_circle 2), x be Point of ( TOP-REAL 2);

      assume x is Point of ( Topen_unit_circle p);

      then

       A1: x in the carrier of ( Topen_unit_circle p);

      the carrier of ( Topen_unit_circle p) is Subset of cS1 by TSEP_1: 1;

      hence thesis by A1, Th13;

    end;

    theorem :: TOPREALB:27

    

     Th27: for x be Point of ( TOP-REAL 2) st x is Point of ( Topen_unit_circle c[10] ) holds ( - 1) <= (x `1 ) & (x `1 ) < 1

    proof

      let x be Point of ( TOP-REAL 2);

      assume

       A1: x is Point of ( Topen_unit_circle c[10] );

       A2:

      now

        

         A3: the carrier of TOUC = (cS1 \ { c[10] }) by Def10;

        then

         A4: not x in { c[10] } by A1, XBOOLE_0:def 5;

        

         A5: x = |[(x `1 ), (x `2 )]| by EUCLID: 53;

        assume

         A6: (x `1 ) = 1;

        x in cS1 by A1, A3, XBOOLE_0:def 5;

        then x = c[10] by A6, A5, Th14;

        hence contradiction by A4, TARSKI:def 1;

      end;

      (x `1 ) <= 1 by A1, Th26;

      hence thesis by A1, A2, Th26, XXREAL_0: 1;

    end;

    theorem :: TOPREALB:28

    

     Th28: for x be Point of ( TOP-REAL 2) st x is Point of ( Topen_unit_circle c[-10] ) holds ( - 1) < (x `1 ) & (x `1 ) <= 1

    proof

      let x be Point of ( TOP-REAL 2);

      assume

       A1: x is Point of ( Topen_unit_circle c[-10] );

       A2:

      now

        

         A3: the carrier of TOUCm = (cS1 \ { c[-10] }) by Def10;

        then

         A4: not x in { c[-10] } by A1, XBOOLE_0:def 5;

        

         A5: x = |[(x `1 ), (x `2 )]| by EUCLID: 53;

        assume

         A6: (x `1 ) = ( - 1);

        x in cS1 by A1, A3, XBOOLE_0:def 5;

        then x = c[-10] by A6, A5, Th15;

        hence contradiction by A4, TARSKI:def 1;

      end;

      ( - 1) <= (x `1 ) by A1, Th26;

      hence thesis by A1, A2, Th26, XXREAL_0: 1;

    end;

    registration

      let p be Point of ( Tunit_circle 2);

      cluster ( Topen_unit_circle p) -> open;

      coherence

      proof

        let A be Subset of TUC;

        assume A = the carrier of ( Topen_unit_circle p);

        

        then

         A1: (A ` ) = (cS1 \ (cS1 \ {p})) by Def10

        .= (cS1 /\ {p}) by XBOOLE_1: 48

        .= {p} by ZFMISC_1: 46;

        TUC is T_2 by TOPMETR: 2;

        then (A ` ) is closed by A1, PCOMPS_1: 7;

        hence thesis by TOPS_1: 4;

      end;

    end

    theorem :: TOPREALB:29

    for p be Point of ( Tunit_circle 2) holds (( Topen_unit_circle p), I(01) ) are_homeomorphic

    proof

      set D = ( Sphere (( 0. ( TOP-REAL 2)),p1));

      let p be Point of ( Tunit_circle 2);

      set P = ( Topen_unit_circle p);

      reconsider p2 = p as Point of ( TOP-REAL 2) by PRE_TOPC: 25;

      (D \ {p}) c= D by XBOOLE_1: 36;

      then

      reconsider A = (D \ {p}) as Subset of ( Tcircle (( 0. ( TOP-REAL 2)),1)) by Th9;

      P = (( Tcircle (( 0. ( TOP-REAL 2)),1)) | A) by Lm13, Th22, EUCLID: 54

      .= (( TOP-REAL 2) | (D \ {p2})) by GOBOARD9: 2;

      hence thesis by Lm13, BORSUK_4: 52, EUCLID: 54;

    end;

    theorem :: TOPREALB:30

    for p,q be Point of ( Tunit_circle 2) holds (( Topen_unit_circle p),( Topen_unit_circle q)) are_homeomorphic

    proof

      set D = ( Sphere (( 0. ( TOP-REAL 2)),p1));

      let p,q be Point of ( Tunit_circle 2);

      set P = ( Topen_unit_circle p);

      set Q = ( Topen_unit_circle q);

      reconsider p2 = p, q2 = q as Point of ( TOP-REAL 2) by PRE_TOPC: 25;

      

       A1: (D \ {q}) c= D by XBOOLE_1: 36;

      (D \ {p}) c= D by XBOOLE_1: 36;

      then

      reconsider A = (D \ {p}), B = (D \ {q}) as Subset of ( Tcircle (( 0. ( TOP-REAL 2)),1)) by A1, Th9;

      

       A2: Q = (( Tcircle (( 0. ( TOP-REAL 2)),1)) | B) by Lm13, Th22, EUCLID: 54

      .= (( TOP-REAL 2) | (D \ {q2})) by GOBOARD9: 2;

      P = (( Tcircle (( 0. ( TOP-REAL 2)),1)) | A) by Lm13, Th22, EUCLID: 54

      .= (( TOP-REAL 2) | (D \ {p2})) by GOBOARD9: 2;

      hence thesis by A2, Lm13, BORSUK_4: 53, EUCLID: 54;

    end;

    begin

    definition

      :: TOPREALB:def11

      func CircleMap -> Function of R^1 , ( Tunit_circle 2) means

      : Def11: for x be Real holds (it . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]|;

      existence

      proof

        defpred P[ Real, set] means $2 = |[( cos ((2 * PI ) * $1)), ( sin ((2 * PI ) * $1))]|;

        

         A1: for x be Element of R^1 holds ex y be Element of cS1 st P[x, y]

        proof

          let x be Element of R^1 ;

          set y = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]|;

           |.(y - o).| = |.y.| by EUCLID: 54, RLVECT_1: 13

          .= ( sqrt (((y `1 ) ^2 ) + ((y `2 ) ^2 ))) by JGRAPH_1: 30

          .= ( sqrt ((( cos ((2 * PI ) * x)) ^2 ) + ((y `2 ) ^2 ))) by EUCLID: 52

          .= ( sqrt ((( cos ((2 * PI ) * x)) ^2 ) + (( sin ((2 * PI ) * x)) ^2 ))) by EUCLID: 52

          .= 1 by SIN_COS: 29, SQUARE_1: 18;

          then y is Element of cS1 by Lm13, TOPREAL9: 9;

          hence thesis;

        end;

        consider f be Function of R, cS1 such that

         A2: for x be Element of R^1 holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let x be Real;

        x is Point of R^1 by TOPMETR: 17, XREAL_0:def 1;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of R^1 , TUC such that

         A3: for x be Real holds (f . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]| and

         A4: for x be Real holds (g . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]|;

        for x be Point of R^1 holds (f . x) = (g . x)

        proof

          let x be Point of R^1 ;

          

          thus (f . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]| by A3

          .= (g . x) by A4;

        end;

        hence f = g;

      end;

    end

    

     Lm18: ( dom CircleMap ) = REAL by FUNCT_2:def 1, TOPMETR: 17;

    theorem :: TOPREALB:31

    

     Th31: ( CircleMap . r) = ( CircleMap . (r + i))

    proof

      defpred P[ Integer] means ( CircleMap . r) = ( CircleMap . (r + $1));

      

       A1: for i holds P[i] implies P[(i - 1)] & P[(i + 1)]

      proof

        let i such that

         A2: P[i];

        

        thus ( CircleMap . (r + (i - 1))) = |[( cos ((2 * PI ) * ((r + i) - 1))), ( sin ((2 * PI ) * ((r + i) - 1)))]| by Def11

        .= |[( cos ((2 * PI ) * (r + i))), ( sin (((2 * PI ) * (r + i)) + ((2 * PI ) * ( - 1))))]| by COMPLEX2: 9

        .= |[( cos ((2 * PI ) * (r + i))), ( sin ((2 * PI ) * (r + i)))]| by COMPLEX2: 8

        .= ( CircleMap . r) by A2, Def11;

        

        thus ( CircleMap . (r + (i + 1))) = |[( cos ((2 * PI ) * ((r + i) + 1))), ( sin ((2 * PI ) * ((r + i) + 1)))]| by Def11

        .= |[( cos ((2 * PI ) * (r + i))), ( sin (((2 * PI ) * (r + i)) + ((2 * PI ) * 1)))]| by COMPLEX2: 9

        .= |[( cos ((2 * PI ) * (r + i))), ( sin ((2 * PI ) * (r + i)))]| by COMPLEX2: 8

        .= ( CircleMap . r) by A2, Def11;

      end;

      

       A3: P[ 0 ];

      for i holds P[i] from INT_1:sch 4( A3, A1);

      hence thesis;

    end;

    theorem :: TOPREALB:32

    

     Th32: ( CircleMap . i) = c[10]

    proof

      

      thus ( CircleMap . i) = |[( cos (((2 * PI ) * i) + 0 )), ( sin ((2 * PI ) * i))]| by Def11

      .= |[( cos 0 ), ( sin (((2 * PI ) * i) + 0 ))]| by COMPLEX2: 9

      .= c[10] by COMPLEX2: 8, SIN_COS: 31;

    end;

    theorem :: TOPREALB:33

    

     Th33: ( CircleMap " { c[10] }) = INT

    proof

      hereby

        let i be object;

        assume

         A1: i in ( CircleMap " { c[10] });

        then

        reconsider x = i as Real;

        ( CircleMap . i) in { c[10] } by A1, FUNCT_2: 38;

        then ( CircleMap . i) = c[10] by TARSKI:def 1;

        then |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]| = |[1, 0 ]| by Def11;

        then ( cos ((2 * PI ) * x)) = 1 by SPPOL_2: 1;

        hence i in INT by SIN_COS6: 44;

      end;

      let i be object;

      assume i in INT ;

      then

      reconsider i as Integer;

      ( CircleMap . i) = c[10] by Th32;

      then

       A2: ( CircleMap . i) in { c[10] } by TARSKI:def 1;

      i in R by TOPMETR: 17, XREAL_0:def 1;

      hence thesis by A2, FUNCT_2: 38;

    end;

    

     Lm19: ( CircleMap . (1 / 2)) = |[( - 1), 0 ]|

    proof

      

      thus ( CircleMap . (1 / 2)) = |[( cos ((2 * PI ) * (1 / 2))), ( sin ((2 * PI ) * (1 / 2)))]| by Def11

      .= |[( - 1), 0 ]| by SIN_COS: 77;

    end;

    theorem :: TOPREALB:34

    

     Th34: ( frac r) = (1 / 2) implies ( CircleMap . r) = |[( - 1), 0 ]|

    proof

      assume

       A1: ( frac r) = (1 / 2);

      

      thus ( CircleMap . r) = ( CircleMap . (r + ( - [\r/]))) by Th31

      .= ( CircleMap . (r - [\r/]))

      .= |[( - 1), 0 ]| by A1, Lm19, INT_1:def 8;

    end;

    theorem :: TOPREALB:35

    ( frac r) = (1 / 4) implies ( CircleMap . r) = |[ 0 , 1]|

    proof

      assume ( frac r) = (1 / 4);

      then

       A1: (r - [\r/]) = (1 / 4) by INT_1:def 8;

      

      thus ( CircleMap . r) = ( CircleMap . (r + ( - [\r/]))) by Th31

      .= |[( cos ((2 * PI ) * (1 / 4))), ( sin ((2 * PI ) * (1 / 4)))]| by A1, Def11

      .= |[ 0 , 1]| by SIN_COS: 77;

    end;

    theorem :: TOPREALB:36

    ( frac r) = (3 / 4) implies ( CircleMap . r) = |[ 0 , ( - 1)]|

    proof

      assume ( frac r) = (3 / 4);

      then

       A1: (r - [\r/]) = (3 / 4) by INT_1:def 8;

      

      thus ( CircleMap . r) = ( CircleMap . (r + ( - [\r/]))) by Th31

      .= |[( cos ((2 * PI ) * (3 / 4))), ( sin ((2 * PI ) * (3 / 4)))]| by A1, Def11

      .= |[ 0 , ( - 1)]| by SIN_COS: 77;

    end;

    

     Lm20: ( CircleMap . r) = |[(( cos * ( AffineMap ((2 * PI ), 0 ))) . r), (( sin * ( AffineMap ((2 * PI ), 0 ))) . r)]|

    proof

      

      thus ( CircleMap . r) = |[( cos (((2 * PI ) * r) + 0 )), ( sin ((2 * PI ) * r))]| by Def11

      .= |[(( cos * ( AffineMap ((2 * PI ), 0 ))) . r), ( sin (((2 * PI ) * r) + 0 ))]| by Th2

      .= |[(( cos * ( AffineMap ((2 * PI ), 0 ))) . r), (( sin * ( AffineMap ((2 * PI ), 0 ))) . r)]| by Th1;

    end;

    theorem :: TOPREALB:37

    for i,j be Integer holds ( CircleMap . r) = |[(( cos * ( AffineMap ((2 * PI ),((2 * PI ) * i)))) . r), (( sin * ( AffineMap ((2 * PI ),((2 * PI ) * j)))) . r)]|

    proof

      let i,j be Integer;

      

      thus ( CircleMap . r) = |[( cos (((2 * PI ) * r) + 0 )), ( sin ((2 * PI ) * r))]| by Def11

      .= |[( cos (((2 * PI ) * r) + ((2 * PI ) * i))), ( sin (((2 * PI ) * r) + 0 ))]| by COMPLEX2: 9

      .= |[( cos (((2 * PI ) * r) + ((2 * PI ) * i))), ( sin (((2 * PI ) * r) + ((2 * PI ) * j)))]| by COMPLEX2: 8

      .= |[(( cos * ( AffineMap ((2 * PI ),((2 * PI ) * i)))) . r), ( sin (((2 * PI ) * r) + ((2 * PI ) * j)))]| by Th2

      .= |[(( cos * ( AffineMap ((2 * PI ),((2 * PI ) * i)))) . r), (( sin * ( AffineMap ((2 * PI ),((2 * PI ) * j)))) . r)]| by Th1;

    end;

    registration

      cluster CircleMap -> continuous;

      coherence

      proof

        reconsider l = ( AffineMap ((2 * PI ), 0 )) as Function of R^1 , R^1 by Th8;

        set sR = ( R^1 sin ), cR = ( R^1 cos );

        

         A1: ( dom ( AffineMap ((2 * PI ), 0 ))) = REAL by FUNCT_2:def 1;

        reconsider sR, cR as Function of R^1 , R^1 by Lm10, Lm11;

        

         A2: ( AffineMap ((2 * PI ), 0 )) = ( R^1 ( AffineMap ((2 * PI ), 0 )));

        reconsider g = CircleMap as Function of R^1 , ( TOP-REAL 2) by TOPREALA: 7;

        

         A3: ( rng ( AffineMap ((2 * PI ), 0 ))) = ( [#] REAL ) by FCONT_1: 55;

        set c = (cR * l);

        set s = (sR * l);

        

         A4: ( R^1 | ( R^1 ( dom cos ))) = R^1 by Th6, SIN_COS: 24;

        

         A5: ( R^1 | ( R^1 ( dom sin ))) = R^1 by Th6, SIN_COS: 24;

        for p be Point of R^1 , V be Subset of ( TOP-REAL 2) st (g . p) in V & V is open holds ex W be Subset of R^1 st p in W & W is open & (g .: W) c= V

        proof

          let p be Point of R^1 , V be Subset of ( TOP-REAL 2) such that

           A6: (g . p) in V and

           A7: V is open;

          reconsider e = (g . p) as Point of ( Euclid 2) by TOPREAL3: 8;

          V = ( Int V) by A7, TOPS_1: 23;

          then

          consider r be Real such that

           A8: r > 0 and

           A9: ( Ball (e,r)) c= V by A6, GOBOARD6: 5;

          set B = ].(((g . p) `2 ) - (r / ( sqrt 2))), (((g . p) `2 ) + (r / ( sqrt 2))).[;

          set A = ].(((g . p) `1 ) - (r / ( sqrt 2))), (((g . p) `1 ) + (r / ( sqrt 2))).[;

          set F = ((1,2) --> (A,B));

          reconsider A, B as Subset of R^1 by TOPMETR: 17;

          

           A10: B is open by JORDAN6: 35;

          

           A11: ( product F) c= ( Ball (e,r)) by TOPREAL6: 41;

          

           A12: cR is continuous by A4, PRE_TOPC: 26;

          

           A13: sR is continuous by A5, PRE_TOPC: 26;

          

           A14: (g . p) = |[(c . p), (s . p)]| by Lm20;

          then ((g . p) `2 ) = (s . p) by EUCLID: 52;

          then (s . p) in B by A8, SQUARE_1: 19, TOPREAL6: 15;

          then

          consider Ws be Subset of R^1 such that

           A15: p in Ws and

           A16: Ws is open and

           A17: (s .: Ws) c= B by A2, A1, A3, A10, A13, Th5, JGRAPH_2: 10;

          

           A18: A is open by JORDAN6: 35;

          ((g . p) `1 ) = (c . p) by A14, EUCLID: 52;

          then (c . p) in A by A8, SQUARE_1: 19, TOPREAL6: 15;

          then

          consider Wc be Subset of R^1 such that

           A19: p in Wc and

           A20: Wc is open and

           A21: (c .: Wc) c= A by A2, A1, A3, A18, A12, Th5, JGRAPH_2: 10;

          set W = (Ws /\ Wc);

          take W;

          thus p in W by A15, A19, XBOOLE_0:def 4;

          thus W is open by A16, A20;

          let y be object;

          assume y in (g .: W);

          then

          consider x be Element of R^1 such that

           A22: x in W and

           A23: y = (g . x) by FUNCT_2: 65;

          x in Ws by A22, XBOOLE_0:def 4;

          then

           A24: (s . x) in (s .: Ws) by FUNCT_2: 35;

          x in Wc by A22, XBOOLE_0:def 4;

          then

           A25: (c . x) in (c .: Wc) by FUNCT_2: 35;

           |[(c . x), (s . x)]| = ((1,2) --> ((c . x),(s . x))) by TOPREALA: 28;

          then |[(c . x), (s . x)]| in ( product F) by A17, A21, A24, A25, HILBERT3: 11;

          then

           A26: |[(c . x), (s . x)]| in ( Ball (e,r)) by A11;

          (g . x) = |[(c . x), (s . x)]| by Lm20;

          hence thesis by A9, A23, A26;

        end;

        then g is continuous by JGRAPH_2: 10;

        hence thesis by PRE_TOPC: 27;

      end;

    end

    

     Lm21: for A be Subset of R^1 holds ( CircleMap | A) is Function of ( R^1 | A), ( Tunit_circle 2)

    proof

      let A be Subset of R^1 ;

      

       A1: ( rng ( CircleMap | A)) c= cS1;

      ( dom ( CircleMap | A)) = A by Lm18, RELAT_1: 62, TOPMETR: 17

      .= the carrier of ( R^1 | A) by PRE_TOPC: 8;

      hence thesis by A1, FUNCT_2: 2;

    end;

    

     Lm22: ( - 1) <= r & r <= 1 implies 0 <= (( arccos r) / (2 * PI )) & (( arccos r) / (2 * PI )) <= (1 / 2)

    proof

      assume that

       A1: ( - 1) <= r and

       A2: r <= 1;

      ( arccos r) <= PI by A1, A2, SIN_COS6: 99;

      then

       A3: (( arccos r) / (2 * PI )) <= ((1 * PI ) / (2 * PI )) by XREAL_1: 72;

       0 <= ( arccos r) by A1, A2, SIN_COS6: 99;

      hence thesis by A3, XCMPLX_1: 91;

    end;

    theorem :: TOPREALB:38

    

     Th38: for A be Subset of R^1 , f be Function of ( R^1 | A), ( Tunit_circle 2) st [. 0 , 1.[ c= A & f = ( CircleMap | A) holds f is onto

    proof

      let A be Subset of R^1 , f be Function of ( R^1 | A), ( Tunit_circle 2) such that

       A1: [. 0 , 1.[ c= A and

       A2: f = ( CircleMap | A);

      

       A3: ( dom f) = A by A2, Lm18, RELAT_1: 62, TOPMETR: 17;

      thus ( rng f) c= cS1;

      let y be object;

      assume

       A4: y in cS1;

      then

      reconsider z = y as Point of ( TOP-REAL 2) by PRE_TOPC: 25;

      set z1 = (z `1 ), z2 = (z `2 );

      

       A5: z1 <= 1 by A4, Th13;

      set x = (( arccos z1) / (2 * PI ));

      

       A6: ( - 1) <= z1 by A4, Th13;

      then

       A7: 0 <= x by A5, Lm22;

      x <= (1 / 2) by A6, A5, Lm22;

      then

       A8: x < 1 by XXREAL_0: 2;

      

       A9: ((z1 ^2 ) + (z2 ^2 )) = ( |.z.| ^2 ) by JGRAPH_1: 29;

      

       A10: |.z.| = 1 by A4, Th12;

      per cases ;

        suppose

         A11: z2 < 0 ;

        now

          assume x = 0 ;

          then ( arccos z1) = 0 ;

          then z1 = 1 by A6, A5, SIN_COS6: 96;

          hence contradiction by A10, A9, A11;

        end;

        then

         A12: (1 - 0 ) > (1 - x) by A7, XREAL_1: 15;

        (1 - x) > (1 - 1) by A8, XREAL_1: 15;

        then

         A13: (1 - x) in [. 0 , 1.[ by A12, XXREAL_1: 3;

        

        then (f . (1 - x)) = ( CircleMap . (( - x) + 1)) by A1, A2, FUNCT_1: 49

        .= ( CircleMap . ( - x)) by Th31

        .= |[( cos ( - ((2 * PI ) * x))), ( sin ((2 * PI ) * ( - x)))]| by Def11

        .= |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * ( - x)))]| by SIN_COS: 31

        .= |[( cos ( arccos z1)), ( sin ( - ((2 * PI ) * x)))]| by XCMPLX_1: 87

        .= |[( cos ( arccos z1)), ( - ( sin ((2 * PI ) * x)))]| by SIN_COS: 31

        .= |[( cos ( arccos z1)), ( - ( sin ( arccos z1)))]| by XCMPLX_1: 87

        .= |[z1, ( - ( sin ( arccos z1)))]| by A6, A5, SIN_COS6: 91

        .= |[z1, ( - ( - z2))]| by A10, A9, A11, SIN_COS6: 103

        .= y by EUCLID: 53;

        hence thesis by A1, A3, A13, FUNCT_1:def 3;

      end;

        suppose

         A14: z2 >= 0 ;

        

         A15: x in [. 0 , 1.[ by A7, A8, XXREAL_1: 3;

        

        then (f . x) = ( CircleMap . x) by A1, A2, FUNCT_1: 49

        .= |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]| by Def11

        .= |[( cos ( arccos z1)), ( sin ((2 * PI ) * x))]| by XCMPLX_1: 87

        .= |[( cos ( arccos z1)), ( sin ( arccos z1))]| by XCMPLX_1: 87

        .= |[z1, ( sin ( arccos z1))]| by A6, A5, SIN_COS6: 91

        .= |[z1, z2]| by A10, A9, A14, SIN_COS6: 102

        .= y by EUCLID: 53;

        hence thesis by A1, A3, A15, FUNCT_1:def 3;

      end;

    end;

    registration

      cluster CircleMap -> onto;

      coherence

      proof

        

         A1: ( R^1 | ( [#] R^1 )) = R^1 by TSEP_1: 3;

        ( CircleMap | REAL ) = CircleMap by Lm18, RELAT_1: 69;

        hence thesis by A1, Th38, TOPMETR: 17;

      end;

    end

    

     Lm23: ( CircleMap | [. 0 , 1.[) is one-to-one

    proof

      

       A1: ( sin | [.( PI / 2), ((3 / 2) * PI ).]) is one-to-one;

      let x1,y1 be object;

      set f = ( CircleMap | [. 0 , 1.[);

      

       A2: [. 0 , ( PI / 2).] c= [.( - ( PI / 2)), ( PI / 2).] by XXREAL_1: 34;

      

       A3: ( dom f) = [. 0 , 1.[ by Lm18, RELAT_1: 62;

      assume

       A4: x1 in ( dom f);

      then

      reconsider x = x1 as Real;

      

       A5: (f . x) = ( CircleMap . x) by A3, A4, FUNCT_1: 49

      .= |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]| by Def11;

      assume

       A6: y1 in ( dom f);

      then

      reconsider y = y1 as Real;

      assume

       A7: (f . x1) = (f . y1);

      

       A8: (f . y) = ( CircleMap . y) by A3, A6, FUNCT_1: 49

      .= |[( cos ((2 * PI ) * y)), ( sin ((2 * PI ) * y))]| by Def11;

      then

       A9: ( cos ((2 * PI ) * x)) = ( cos ((2 * PI ) * y)) by A7, A5, SPPOL_2: 1;

      

       A10: ( cos ((2 * PI ) * y)) = ( cos . ((2 * PI ) * y)) by SIN_COS:def 19;

      

       A11: ( cos ((2 * PI ) * x)) = ( cos . ((2 * PI ) * x)) by SIN_COS:def 19;

      

       A12: ( sin ((2 * PI ) * x)) = ( sin ((2 * PI ) * y)) by A7, A5, A8, SPPOL_2: 1;

      

       A13: ( sin ((2 * PI ) * y)) = ( sin . ((2 * PI ) * y)) by SIN_COS:def 17;

      

       A14: ( sin ((2 * PI ) * x)) = ( sin . ((2 * PI ) * x)) by SIN_COS:def 17;

      per cases by A3, A4, XXREAL_1: 3;

        suppose

         A15: 0 <= x & x <= (1 / 4);

        

         A16: [. 0 , ( PI / 2).] c= [. 0 , PI .] by Lm5, XXREAL_1: 34;

        ((2 * PI ) * x) <= ((2 * PI ) * (1 / 4)) by A15, XREAL_1: 64;

        then

         A17: ((2 * PI ) * x) in [. 0 , (((2 * PI ) * 1) / 4).] by A15, XXREAL_1: 1;

        per cases by A3, A6, XXREAL_1: 3;

          suppose

           A18: 0 <= y & y <= (1 / 4);

          then ((2 * PI ) * y) <= ((2 * PI ) * (1 / 4)) by XREAL_1: 64;

          then

           A19: ((2 * PI ) * y) in [. 0 , (((2 * PI ) * 1) / 4).] by A18, XXREAL_1: 1;

          set g = ( sin | [. 0 , ( PI / 2).]);

          

           A20: ( dom g) = [. 0 , ( PI / 2).] by RELAT_1: 62, SIN_COS: 24;

          (g . ((2 * PI ) * x)) = ( sin . ((2 * PI ) * x)) by A17, FUNCT_1: 49

          .= ( sin . ((2 * PI ) * y)) by A12, A14, SIN_COS:def 17

          .= (g . ((2 * PI ) * y)) by A19, FUNCT_1: 49;

          then ((2 * PI ) * x) = ((2 * PI ) * y) by A17, A19, A20, FUNCT_1:def 4;

          then x = (((2 * PI ) * y) / P2) by XCMPLX_1: 89;

          hence thesis by XCMPLX_1: 89;

        end;

          suppose

           A21: (1 / 4) < y & y < (3 / 4);

          then

           A22: ((2 * PI ) * y) < ((2 * PI ) * (3 / 4)) by XREAL_1: 68;

          ((2 * PI ) * (1 / 4)) < ((2 * PI ) * y) by A21, XREAL_1: 68;

          then ((2 * PI ) * y) in ].( PI / 2), ((3 / 2) * PI ).[ by A22, XXREAL_1: 4;

          hence thesis by A9, A11, A10, A2, A17, COMPTRIG: 12, COMPTRIG: 13;

        end;

          suppose

           A23: (3 / 4) <= y & y < 1;

          then

           A24: ((2 * PI ) * y) < ((2 * PI ) * 1) by XREAL_1: 68;

          

           A25: [.((3 / 2) * PI ), (2 * PI ).[ c= ]. PI , (2 * PI ).[ by Lm6, XXREAL_1: 48;

          ((2 * PI ) * (3 / 4)) <= ((2 * PI ) * y) by A23, XREAL_1: 64;

          then ((2 * PI ) * y) in [.((3 / 2) * PI ), (2 * PI ).[ by A24, XXREAL_1: 3;

          hence thesis by A12, A14, A13, A17, A16, A25, COMPTRIG: 8, COMPTRIG: 9;

        end;

      end;

        suppose

         A26: (1 / 4) < x & x <= (1 / 2);

        then

         A27: ((2 * PI ) * x) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

        ((2 * PI ) * (1 / 4)) < ((2 * PI ) * x) by A26, XREAL_1: 68;

        then

         A28: ((2 * PI ) * x) in ].( PI / 2), ((2 * PI ) * (1 / 2)).] by A27, XXREAL_1: 2;

        

         A29: ].( PI / 2), PI .] c= ].( PI / 2), ((3 / 2) * PI ).[ by Lm6, XXREAL_1: 49;

        

         A30: ].( PI / 2), PI .] c= [. 0 , PI .] by XXREAL_1: 36;

        per cases by A3, A6, XXREAL_1: 3;

          suppose

           A31: 0 <= y & y <= (1 / 4);

          then ((2 * PI ) * y) <= ((2 * PI ) * (1 / 4)) by XREAL_1: 64;

          then ((2 * PI ) * y) in [. 0 , ((2 * PI ) * (1 / 4)).] by A31, XXREAL_1: 1;

          hence thesis by A9, A11, A10, A2, A28, A29, COMPTRIG: 12, COMPTRIG: 13;

        end;

          suppose

           A32: (1 / 4) < y & y <= (1 / 2);

          then

           A33: ((2 * PI ) * y) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

          ((2 * PI ) * (1 / 4)) < ((2 * PI ) * y) by A32, XREAL_1: 68;

          then

           A34: ((2 * PI ) * y) in ].((2 * PI ) * (1 / 4)), ((2 * PI ) * (1 / 2)).] by A33, XXREAL_1: 2;

          set g = ( sin | ].( PI / 2), PI .]);

          

           A35: ( dom g) = ].( PI / 2), PI .] by RELAT_1: 62, SIN_COS: 24;

          

           A36: g is one-to-one by A1, Lm6, SIN_COS6: 2, XXREAL_1: 36;

          (g . ((2 * PI ) * x)) = ( sin . ((2 * PI ) * x)) by A28, FUNCT_1: 49

          .= ( sin . ((2 * PI ) * y)) by A12, A14, SIN_COS:def 17

          .= (g . ((2 * PI ) * y)) by A34, FUNCT_1: 49;

          then ((2 * PI ) * x) = ((2 * PI ) * y) by A28, A34, A36, A35;

          then x = (((2 * PI ) * y) / P2) by XCMPLX_1: 89;

          hence thesis by XCMPLX_1: 89;

        end;

          suppose

           A37: (1 / 2) < y & y < 1;

          then

           A38: ((2 * PI ) * y) < ((2 * PI ) * 1) by XREAL_1: 68;

          ((2 * PI ) * (1 / 2)) < ((2 * PI ) * y) by A37, XREAL_1: 68;

          then ((2 * PI ) * y) in ]. PI , (2 * PI ).[ by A38, XXREAL_1: 4;

          hence thesis by A12, A14, A13, A28, A30, COMPTRIG: 8, COMPTRIG: 9;

        end;

      end;

        suppose

         A39: (1 / 2) < x & x <= (3 / 4);

        then

         A40: ((2 * PI ) * x) <= ((2 * PI ) * (3 / 4)) by XREAL_1: 64;

        ((2 * PI ) * (1 / 2)) < ((2 * PI ) * x) by A39, XREAL_1: 68;

        then

         A41: ((2 * PI ) * x) in ]. PI , ((2 * PI ) * (3 / 4)).] by A40, XXREAL_1: 2;

        

         A42: ]. PI , ((3 / 2) * PI ).] c= [.( PI / 2), ((3 / 2) * PI ).] by Lm5, XXREAL_1: 36;

        

         A43: ]. PI , ((3 / 2) * PI ).] c= ]. PI , (2 * PI ).[ by Lm7, XXREAL_1: 49;

        per cases by A3, A6, XXREAL_1: 3;

          suppose

           A44: 0 <= y & y <= (1 / 2);

          then ((2 * PI ) * y) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

          then ((2 * PI ) * y) in [. 0 , PI .] by A44, XXREAL_1: 1;

          hence thesis by A12, A14, A13, A41, A43, COMPTRIG: 8, COMPTRIG: 9;

        end;

          suppose

           A45: (1 / 2) < y & y <= (3 / 4);

          then

           A46: ((2 * PI ) * y) <= ((2 * PI ) * (3 / 4)) by XREAL_1: 64;

          ((2 * PI ) * (1 / 2)) < ((2 * PI ) * y) by A45, XREAL_1: 68;

          then

           A47: ((2 * PI ) * y) in ]. PI , ((2 * PI ) * (3 / 4)).] by A46, XXREAL_1: 2;

          set g = ( sin | ]. PI , ((3 / 2) * PI ).]);

          

           A48: ( dom g) = ]. PI , ((3 / 2) * PI ).] by RELAT_1: 62, SIN_COS: 24;

          

           A49: g is one-to-one by A1, Lm5, SIN_COS6: 2, XXREAL_1: 36;

          (g . ((2 * PI ) * x)) = ( sin . ((2 * PI ) * x)) by A41, FUNCT_1: 49

          .= ( sin . ((2 * PI ) * y)) by A12, A14, SIN_COS:def 17

          .= (g . ((2 * PI ) * y)) by A47, FUNCT_1: 49;

          then ((2 * PI ) * x) = ((2 * PI ) * y) by A41, A47, A49, A48;

          then x = (((2 * PI ) * y) / P2) by XCMPLX_1: 89;

          hence thesis by XCMPLX_1: 89;

        end;

          suppose

           A50: (3 / 4) < y & y < 1;

          then

           A51: ((2 * PI ) * y) < ((2 * PI ) * 1) by XREAL_1: 68;

          ((2 * PI ) * (3 / 4)) < ((2 * PI ) * y) by A50, XREAL_1: 68;

          then ((2 * PI ) * y) in ].((3 / 2) * PI ), (2 * PI ).[ by A51, XXREAL_1: 4;

          hence thesis by A9, A11, A10, A41, A42, COMPTRIG: 14, COMPTRIG: 15;

        end;

      end;

        suppose

         A52: (3 / 4) < x & x < 1;

        then

         A53: ((2 * PI ) * x) < ((2 * PI ) * 1) by XREAL_1: 68;

        ((2 * PI ) * (3 / 4)) < ((2 * PI ) * x) by A52, XREAL_1: 68;

        then

         A54: ((2 * PI ) * x) in ].((3 / 2) * PI ), (2 * PI ).[ by A53, XXREAL_1: 4;

        

         A55: ].((3 / 2) * PI ), (2 * PI ).[ c= ]. PI , (2 * PI ).[ by Lm6, XXREAL_1: 46;

        per cases by A3, A6, XXREAL_1: 3;

          suppose

           A56: 0 <= y & y <= (1 / 2);

          then ((2 * PI ) * y) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

          then ((2 * PI ) * y) in [. 0 , PI .] by A56, XXREAL_1: 1;

          hence thesis by A12, A14, A13, A54, A55, COMPTRIG: 8, COMPTRIG: 9;

        end;

          suppose

           A57: (1 / 2) < y & y <= (3 / 4);

          then

           A58: ((2 * PI ) * y) <= ((2 * PI ) * (3 / 4)) by XREAL_1: 64;

          

           A59: ]. PI , ((3 / 2) * PI ).] c= [.( PI / 2), ((3 / 2) * PI ).] by Lm5, XXREAL_1: 36;

          ((2 * PI ) * (1 / 2)) < ((2 * PI ) * y) by A57, XREAL_1: 68;

          then ((2 * PI ) * y) in ]. PI , ((3 / 2) * PI ).] by A58, XXREAL_1: 2;

          hence thesis by A9, A11, A10, A54, A59, COMPTRIG: 14, COMPTRIG: 15;

        end;

          suppose

           A60: (3 / 4) < y & y < 1;

          then

           A61: ((2 * PI ) * y) < ((2 * PI ) * 1) by XREAL_1: 68;

          ((2 * PI ) * (3 / 4)) < ((2 * PI ) * y) by A60, XREAL_1: 68;

          then

           A62: ((2 * PI ) * y) in ].((3 / 2) * PI ), (2 * PI ).[ by A61, XXREAL_1: 4;

          set g = ( sin | ].((3 / 2) * PI ), (2 * PI ).[);

          

           A63: ( dom g) = ].((3 / 2) * PI ), (2 * PI ).[ by RELAT_1: 62, SIN_COS: 24;

          (g . ((2 * PI ) * x)) = ( sin . ((2 * PI ) * x)) by A54, FUNCT_1: 49

          .= ( sin . ((2 * PI ) * y)) by A12, A14, SIN_COS:def 17

          .= (g . ((2 * PI ) * y)) by A62, FUNCT_1: 49;

          then ((2 * PI ) * x) = ((2 * PI ) * y) by A54, A62, A63, FUNCT_1:def 4;

          then x = (((2 * PI ) * y) / P2) by XCMPLX_1: 89;

          hence thesis by XCMPLX_1: 89;

        end;

      end;

    end;

    registration

      let r be Real;

      cluster ( CircleMap | [.r, (r + 1).[) -> one-to-one;

      coherence

      proof

        let x,y be object;

        set g = ( CircleMap | [. 0 , 1.[);

        set f = ( CircleMap | [.r, (r + 1).[);

        assume that

         A1: x in ( dom f) and

         A2: y in ( dom f) and

         A3: (f . x) = (f . y);

        

         A4: ( dom f) = [.r, (r + 1).[ by Lm18, RELAT_1: 62;

        reconsider x, y as Real by A1, A2;

        

         A5: ( dom g) = [. 0 , 1.[ by Lm18, RELAT_1: 62;

        

         A6: r <= y by A4, A2, XXREAL_1: 3;

        

         A7: x < (r + 1) by A4, A1, XXREAL_1: 3;

        set x1 = ( frac x);

        

         A8: x1 = (x - [\x/]) by INT_1:def 8;

        

         A9: x1 < 1 by INT_1: 43;

         0 <= x1 by INT_1: 43;

        then

         A10: x1 in [. 0 , 1.[ by A9, XXREAL_1: 3;

        set y1 = ( frac y);

        

         A11: y1 = (y - [\y/]) by INT_1:def 8;

        

         A12: y1 < 1 by INT_1: 43;

         0 <= y1 by INT_1: 43;

        then

         A13: y1 in [. 0 , 1.[ by A12, XXREAL_1: 3;

        

         A14: (f . y) = ( CircleMap . y) by A2, FUNCT_1: 47

        .= ( CircleMap . (y + ( - [\y/]))) by Th31

        .= (g . y1) by A5, A11, A13, FUNCT_1: 47;

        (f . x) = ( CircleMap . x) by A1, FUNCT_1: 47

        .= ( CircleMap . (x + ( - [\x/]))) by Th31

        .= (g . x1) by A5, A8, A10, FUNCT_1: 47;

        then

         A15: x1 = y1 by A5, A3, A10, A13, A14, Lm23;

        

         A16: y < (r + 1) by A4, A2, XXREAL_1: 3;

        r <= x by A4, A1, XXREAL_1: 3;

        hence thesis by A7, A6, A16, A15, INT_1: 72;

      end;

    end

    registration

      let r be Real;

      cluster ( CircleMap | ].r, (r + 1).[) -> one-to-one;

      coherence

      proof

        ( CircleMap | [.r, (r + 1).[) is one-to-one;

        hence thesis by SIN_COS6: 2, XXREAL_1: 45;

      end;

    end

    theorem :: TOPREALB:39

    

     Th39: (b - a) <= 1 implies for d be set st d in ( IntIntervals (a,b)) holds ( CircleMap | d) is one-to-one

    proof

      assume that

       A1: (b - a) <= 1;

      let d be set;

      assume d in ( IntIntervals (a,b));

      then

      consider n be Element of INT such that

       A2: d = ].(a + n), (b + n).[;

      

       A3: ( CircleMap | [.(a + n), ((a + n) + 1).[) is one-to-one;

      ((b - a) + (a + n)) <= (1 + (a + n)) by A1, XREAL_1: 6;

      hence thesis by A2, A3, SIN_COS6: 2, XXREAL_1: 45;

    end;

    theorem :: TOPREALB:40

    

     Th40: for d be set st d in ( IntIntervals (a,b)) holds ( CircleMap .: d) = ( CircleMap .: ( union ( IntIntervals (a,b))))

    proof

      set D = ( IntIntervals (a,b));

      let d be set;

      assume

       A1: d in D;

      hence ( CircleMap .: d) c= ( CircleMap .: ( union D)) by RELAT_1: 123, ZFMISC_1: 74;

      consider i be Element of INT such that

       A2: d = ].(a + i), (b + i).[ by A1;

      let y be object;

      assume y in ( CircleMap .: ( union D));

      then

      consider x be Element of R^1 such that

       A3: x in ( union D) and

       A4: y = ( CircleMap . x) by FUNCT_2: 65;

      consider Z be set such that

       A5: x in Z and

       A6: Z in D by A3, TARSKI:def 4;

      consider n be Element of INT such that

       A7: Z = ].(a + n), (b + n).[ by A6;

      x < (b + n) by A5, A7, XXREAL_1: 4;

      then (x + i) < ((b + n) + i) by XREAL_1: 6;

      then

       A8: ((x + i) - n) < (((b + n) + i) - n) by XREAL_1: 9;

      set k = ((x + i) - n);

      

       A9: ( CircleMap . k) = ( CircleMap . (x + (i - n)))

      .= y by A4, Th31;

      

       A10: k in R by TOPMETR: 17, XREAL_0:def 1;

      (a + n) < x by A5, A7, XXREAL_1: 4;

      then ((a + n) + i) < (x + i) by XREAL_1: 6;

      then (((a + n) + i) - n) < ((x + i) - n) by XREAL_1: 9;

      then k in d by A2, A8, XXREAL_1: 4;

      hence thesis by A10, A9, FUNCT_2: 35;

    end;

    definition

      let r be Point of R^1 ;

      :: TOPREALB:def12

      func CircleMap (r) -> Function of ( R^1 | ( R^1 ].r, (r + 1).[)), ( Topen_unit_circle ( CircleMap . r)) equals ( CircleMap | ].r, (r + 1).[);

      coherence

      proof

        set B = [.r, (r + 1).[;

        set A = ].r, (r + 1).[;

        set X = ( Topen_unit_circle ( CircleMap . r));

        set f = ( CircleMap | A);

        set g = ( CircleMap | B);

        

         A1: A c= B by XXREAL_1: 45;

        

         A2: ( dom f) = A by Lm18, RELAT_1: 62;

        

         A3: the carrier of X = (cS1 \ {( CircleMap . r)}) by Def10;

        

         A4: ( rng f) c= the carrier of X

        proof

          let y be object;

          assume

           A5: y in ( rng f);

          now

            

             A6: ( dom g) = B by Lm18, RELAT_1: 62;

            assume

             A7: y = ( CircleMap . r);

            (r + 0 ) < (r + 1) by XREAL_1: 8;

            then

             A8: r in B by XXREAL_1: 3;

            consider x be object such that

             A9: x in ( dom f) and

             A10: (f . x) = y by A5, FUNCT_1:def 3;

            (g . x) = ( CircleMap . x) by A1, A2, A9, FUNCT_1: 49

            .= ( CircleMap . r) by A2, A7, A9, A10, FUNCT_1: 49

            .= (g . r) by A8, FUNCT_1: 49;

            then x = r by A1, A2, A9, A8, A6, FUNCT_1:def 4;

            hence contradiction by A2, A9, XXREAL_1: 4;

          end;

          then not y in {( CircleMap . r)} by TARSKI:def 1;

          hence thesis by A3, A5, XBOOLE_0:def 5;

        end;

        the carrier of ( R^1 | ( R^1 A)) = A by PRE_TOPC: 8;

        hence thesis by A2, A4, FUNCT_2: 2;

      end;

    end

    

     Lm24: ( rng (( AffineMap (1,( - a))) | ].(r + a), ((r + a) + 1).[)) = ].r, (r + 1).[

    proof

      set F = ( AffineMap (1,( - a)));

      set f = (F | ].(r + a), ((r + a) + 1).[);

      ( dom F) = REAL by FUNCT_2:def 1;

      then

       A1: ( dom f) = ].(r + a), ((r + a) + 1).[ by RELAT_1: 62;

      thus ( rng f) = ].r, (r + 1).[

      proof

        thus ( rng f) c= ].r, (r + 1).[

        proof

          let y be object;

          assume y in ( rng f);

          then

          consider x be object such that

           A2: x in ( dom f) and

           A3: (f . x) = y by FUNCT_1:def 3;

          reconsider x as Real by A2;

          (r + a) < x by A1, A2, XXREAL_1: 4;

          then

           A4: ((r + a) - a) < (x - a) by XREAL_1: 9;

          x < ((r + a) + 1) by A1, A2, XXREAL_1: 4;

          then

           A5: (x - a) < (((r + a) + 1) - a) by XREAL_1: 9;

          y = (F . x) by A2, A3, FUNCT_1: 47

          .= ((1 * x) + ( - a)) by FCONT_1:def 4;

          hence thesis by A4, A5, XXREAL_1: 4;

        end;

        let y be object;

        assume

         A6: y in ].r, (r + 1).[;

        then

        reconsider y as Real;

        y < (r + 1) by A6, XXREAL_1: 4;

        then

         A7: (y + a) < ((r + 1) + a) by XREAL_1: 6;

        r < y by A6, XXREAL_1: 4;

        then (r + a) < (y + a) by XREAL_1: 6;

        then

         A8: (y + a) in ].(r + a), ((r + a) + 1).[ by A7, XXREAL_1: 4;

        

        then (f . (y + a)) = (F . (y + a)) by FUNCT_1: 49

        .= ((1 * (y + a)) + ( - a)) by FCONT_1:def 4

        .= y;

        hence thesis by A1, A8, FUNCT_1:def 3;

      end;

    end;

    theorem :: TOPREALB:41

    

     Th41: ( CircleMap ( R^1 (a + i))) = (( CircleMap ( R^1 a)) * (( AffineMap (1,( - i))) | ].(a + i), ((a + i) + 1).[))

    proof

      set W = ].a, (a + 1).[;

      set Q = ].(a + i), ((a + i) + 1).[;

      set h = ( CircleMap ( R^1 (a + i)));

      set g = ( CircleMap ( R^1 a));

      set F = ( AffineMap (1,( - i)));

      set f = (F | Q);

      

       A1: ( dom h) = Q by Lm18, RELAT_1: 62;

      ( dom F) = REAL by FUNCT_2:def 1;

      then

       A2: ( dom f) = Q by RELAT_1: 62;

      

       A3: for x be object st x in ( dom h) holds (h . x) = ((g * f) . x)

      proof

        let x be object;

        assume

         A4: x in ( dom h);

        then

        reconsider y = x as Real;

        y < ((a + i) + 1) by A1, A4, XXREAL_1: 4;

        then

         A5: (y - i) < (((a + i) + 1) - i) by XREAL_1: 9;

        (a + i) < y by A1, A4, XXREAL_1: 4;

        then ((a + i) - i) < (y - i) by XREAL_1: 9;

        then

         A6: (y - i) in W by A5, XXREAL_1: 4;

        

        thus ((g * f) . x) = (g . (f . x)) by A1, A2, A4, FUNCT_1: 13

        .= (g . (F . x)) by A1, A4, FUNCT_1: 49

        .= (g . ((1 * y) + ( - i))) by FCONT_1:def 4

        .= ( CircleMap . (y + ( - i))) by A6, FUNCT_1: 49

        .= ( CircleMap . y) by Th31

        .= (h . x) by A1, A4, FUNCT_1: 49;

      end;

      

       A7: ( rng f) = ].a, (a + 1).[ by Lm24;

      ( dom g) = W by Lm18, RELAT_1: 62;

      then ( dom (g * f)) = ( dom f) by A7, RELAT_1: 27;

      hence thesis by A2, A3, Lm18, RELAT_1: 62;

    end;

    registration

      let r be Point of R^1 ;

      cluster ( CircleMap r) -> one-to-one onto continuous;

      coherence

      proof

        thus ( CircleMap r) is one-to-one;

        thus ( CircleMap r) is onto

        proof

          set TOUC = ( Topen_unit_circle ( CircleMap . r));

          set A = ].r, (r + 1).[;

          set f = ( CircleMap | A);

          set X = the carrier of TOUC;

          thus ( rng ( CircleMap r)) c= X;

          let y be object;

          

           A1: [\r/] <= r by INT_1:def 6;

          

           A2: ( dom f) = ].r, (r + 1).[ by Lm18, RELAT_1: 62;

          assume

           A3: y in X;

          then

          reconsider z = y as Point of ( TOP-REAL 2) by Lm8;

          set z1 = (z `1 ), z2 = (z `2 );

          

           A4: z1 <= 1 by A3, Th26;

          set x = (( arccos z1) / (2 * PI ));

          

           A5: ( - 1) <= z1 by A3, Th26;

          then

           A6: 0 <= x by A4, Lm22;

          x <= (1 / 2) by A5, A4, Lm22;

          then

           A7: x < 1 by XXREAL_0: 2;

          then

           A8: (x - x) < (1 - x) by XREAL_1: 14;

          

           A9: ((z1 ^2 ) + (z2 ^2 )) = ( |.z.| ^2 ) by JGRAPH_1: 29;

          z is Point of TUC by A3, PRE_TOPC: 25;

          then

           A10: |.z.| = 1 by Th12;

          per cases ;

            suppose

             A11: z2 < 0 ;

            

             A12: ( CircleMap . ( - x)) = |[( cos ( - ((2 * PI ) * x))), ( sin ((2 * PI ) * ( - x)))]| by Def11

            .= |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * ( - x)))]| by SIN_COS: 31

            .= |[( cos ( arccos z1)), ( sin ( - ((2 * PI ) * x)))]| by XCMPLX_1: 87

            .= |[( cos ( arccos z1)), ( - ( sin ((2 * PI ) * x)))]| by SIN_COS: 31

            .= |[( cos ( arccos z1)), ( - ( sin ( arccos z1)))]| by XCMPLX_1: 87

            .= |[z1, ( - ( sin ( arccos z1)))]| by A5, A4, SIN_COS6: 91

            .= |[z1, ( - ( - z2))]| by A10, A9, A11, SIN_COS6: 103

            .= y by EUCLID: 53;

            per cases ;

              suppose

               A13: ((1 - x) + [\r/]) in A;

              

              then (f . ((1 - x) + [\r/])) = ( CircleMap . (( - x) + ( [\r/] + 1))) by FUNCT_1: 49

              .= ( CircleMap . ( - x)) by Th31;

              hence thesis by A2, A12, A13, FUNCT_1:def 3;

            end;

              suppose

               A14: not ((1 - x) + [\r/]) in A;

              now

                assume x = 0 ;

                then ( arccos z1) = 0 ;

                then z1 = 1 by A5, A4, SIN_COS6: 96;

                hence contradiction by A10, A9, A11;

              end;

              then ( [\r/] - x) < (r - 0 ) by A1, A6, XREAL_1: 15;

              then ((( - x) + [\r/]) + 1) < (r + 1) by XREAL_1: 6;

              then

               A15: r >= ((1 - x) + [\r/]) by A14, XXREAL_1: 4;

              (( [\r/] + 1) + 0 ) < (( [\r/] + 1) + (1 - x)) by A8, XREAL_1: 6;

              then

               A16: r < ((2 - x) + [\r/]) by INT_1: 29, XXREAL_0: 2;

              now

                assume ((( - x) + [\r/]) + 1) = r;

                

                then ( CircleMap . r) = ( CircleMap . (( - x) + ( [\r/] + 1)))

                .= ( CircleMap . ( - x)) by Th31;

                hence contradiction by A3, A12, Th21;

              end;

              then ((1 - x) + [\r/]) < r by A15, XXREAL_0: 1;

              then (((1 - x) + [\r/]) + 1) < (r + 1) by XREAL_1: 6;

              then

               A17: ((( - x) + [\r/]) + 2) in A by A16, XXREAL_1: 4;

              

              then (f . (( - x) + ( [\r/] + 2))) = ( CircleMap . (( - x) + ( [\r/] + 2))) by FUNCT_1: 49

              .= ( CircleMap . ( - x)) by Th31;

              hence thesis by A2, A12, A17, FUNCT_1:def 3;

            end;

          end;

            suppose

             A18: z2 >= 0 ;

            

             A19: ( CircleMap . x) = |[( cos ((2 * PI ) * x)), ( sin ((2 * PI ) * x))]| by Def11

            .= |[( cos ( arccos z1)), ( sin ((2 * PI ) * x))]| by XCMPLX_1: 87

            .= |[( cos ( arccos z1)), ( sin ( arccos z1))]| by XCMPLX_1: 87

            .= |[z1, ( sin ( arccos z1))]| by A5, A4, SIN_COS6: 91

            .= |[z1, z2]| by A10, A9, A18, SIN_COS6: 102

            .= y by EUCLID: 53;

            per cases ;

              suppose

               A20: (x + [\r/]) in A;

              

              then (f . (x + [\r/])) = ( CircleMap . (x + [\r/])) by FUNCT_1: 49

              .= ( CircleMap . x) by Th31;

              hence thesis by A2, A19, A20, FUNCT_1:def 3;

            end;

              suppose

               A21: not (x + [\r/]) in A;

              ( 0 + ( [\r/] + 1)) <= (x + ( [\r/] + 1)) by A6, XREAL_1: 6;

              then

               A22: r < ((x + [\r/]) + 1) by INT_1: 29, XXREAL_0: 2;

               A23:

              now

                assume ((x + [\r/]) + 1) = (r + 1);

                then ( CircleMap . r) = ( CircleMap . x) by Th31;

                hence contradiction by A3, A19, Th21;

              end;

              (x + [\r/]) < (1 + r) by A1, A7, XREAL_1: 8;

              then (x + [\r/]) <= r by A21, XXREAL_1: 4;

              then ((x + [\r/]) + 1) <= (r + 1) by XREAL_1: 6;

              then ((x + [\r/]) + 1) < (r + 1) by A23, XXREAL_0: 1;

              then

               A24: ((x + [\r/]) + 1) in A by A22, XXREAL_1: 4;

              

              then (f . ((x + [\r/]) + 1)) = ( CircleMap . (x + ( [\r/] + 1))) by FUNCT_1: 49

              .= ( CircleMap . x) by Th31;

              hence thesis by A2, A19, A24, FUNCT_1:def 3;

            end;

          end;

        end;

        ( Topen_unit_circle ( CircleMap . r)) = (( Tunit_circle 2) | (( [#] ( Tunit_circle 2)) \ {( CircleMap . r)})) by Th22;

        hence thesis by TOPREALA: 8;

      end;

    end

    definition

      :: TOPREALB:def13

      func Circle2IntervalR -> Function of ( Topen_unit_circle c[10] ), ( R^1 | ( R^1 ]. 0 , 1.[)) means

      : Def13: for p be Point of ( Topen_unit_circle c[10] ) holds ex x,y be Real st p = |[x, y]| & (y >= 0 implies (it . p) = (( arccos x) / (2 * PI ))) & (y <= 0 implies (it . p) = (1 - (( arccos x) / (2 * PI ))));

      existence

      proof

        defpred P[ set, set] means ex x,y be Real st $1 = |[x, y]| & (y >= 0 implies $2 = (( arccos x) / P2)) & (y <= 0 implies $2 = (1 - (( arccos x) / P2)));

        reconsider A as non empty Subset of R^1 ;

        

         A1: Y = A by PRE_TOPC: 8;

        

         A2: for x be Element of X holds ex y be Element of Y st P[x, y]

        proof

          let x be Element of X;

          

           A3: X = (cS1 \ { c[10] }) by Def10;

          then

           A4: x in cS1 by XBOOLE_0:def 5;

          

           A5: cS1 is Subset of ( TOP-REAL 2) by TSEP_1: 1;

          then

          consider a,b be Element of REAL such that

           A6: x = <*a, b*> by A4, EUCLID: 51;

          reconsider x1 = x as Point of ( TOP-REAL 2) by A4, A5;

          

           A7: b = (x1 `2 ) by A6, EUCLID: 52;

          set k = ( arccos a);

          

           A8: a = (x1 `1 ) by A6, EUCLID: 52;

          then

           A9: ( - 1) <= a by Th26;

          

           A10: (1 ^2 ) = ( |.x1.| ^2 ) by A4, Th12

          .= ((a ^2 ) + (b ^2 )) by A8, A7, JGRAPH_3: 1;

          

           A11: a <= 1 by A8, Th26;

          then

           A12: 0 <= k by A9, SIN_COS6: 99;

          

           A13: (k / P2) <= (1 / 2) by A9, A11, Lm22;

          

           A14: not x in { c[10] } by A3, XBOOLE_0:def 5;

           A15:

          now

            assume

             A16: k = 0 ;

            then (1 - 1) = ((1 + (b ^2 )) - 1) by A9, A11, A10, SIN_COS6: 96;

            then

             A17: b = 0 ;

            a = 1 by A9, A11, A16, SIN_COS6: 96;

            hence contradiction by A6, A14, A17, TARSKI:def 1;

          end;

          

           A18: k <= PI by A9, A11, SIN_COS6: 99;

          

           A19: 0 <= (k / P2) by A9, A11, Lm22;

          per cases ;

            suppose

             A20: b = 0 ;

            set y = (k / P2);

            y < 1 by A13, XXREAL_0: 2;

            then

            reconsider y as Element of Y by A1, A19, A15, XXREAL_1: 4;

            take y, a, b;

            thus x = |[a, b]| by A6;

            thus b >= 0 implies y = (( arccos a) / P2);

            assume b <= 0 ;

            

             A21: a <> 1 by A6, A14, A20, TARSKI:def 1;

            

            hence y = ((1 * PI ) / P2) by A10, A20, SIN_COS6: 93, SQUARE_1: 41

            .= (1 - (1 / 2)) by XCMPLX_1: 91

            .= (1 - ((1 * PI ) / P2)) by XCMPLX_1: 91

            .= (1 - (( arccos a) / P2)) by A10, A20, A21, SIN_COS6: 93, SQUARE_1: 41;

          end;

            suppose

             A22: b > 0 ;

            set y = (k / P2);

            y < 1 by A13, XXREAL_0: 2;

            then

            reconsider y as Element of Y by A1, A19, A15, XXREAL_1: 4;

            take y, a, b;

            thus thesis by A6, A22;

          end;

            suppose

             A23: b < 0 ;

            set y = (1 - (k / P2));

            

             A24: ((P2 - k) / P2) = ((P2 / P2) - (k / P2)) by XCMPLX_1: 120

            .= y by XCMPLX_1: 60;

            (P2 - k) < (P2 - 0 ) by A12, A15, XREAL_1: 15;

            then y < (P2 / P2) by A24, XREAL_1: 74;

            then

             A25: y < 1 by XCMPLX_1: 60;

            (1 * k) < P2 by A18, XREAL_1: 98;

            then (k - k) < (P2 - k) by XREAL_1: 14;

            then

            reconsider y as Element of Y by A1, A24, A25, XXREAL_1: 4;

            take y, a, b;

            thus thesis by A6, A23;

          end;

        end;

        ex G be Function of TOUC, ( R^1 | ( R^1 ]. 0 , ( 0 + p1).[)) st for p be Point of TOUC holds P[p, (G . p)] from FUNCT_2:sch 3( A2);

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of TOUC, ( R^1 | A) such that

         A26: for p be Point of TOUC holds ex x,y be Real st p = |[x, y]| & (y >= 0 implies (f . p) = (( arccos x) / (2 * PI ))) & (y <= 0 implies (f . p) = (1 - (( arccos x) / (2 * PI )))) and

         A27: for p be Point of TOUC holds ex x,y be Real st p = |[x, y]| & (y >= 0 implies (g . p) = (( arccos x) / (2 * PI ))) & (y <= 0 implies (g . p) = (1 - (( arccos x) / (2 * PI ))));

        now

          let p be Point of TOUC;

          

           A28: ex x2,y2 be Real st p = |[x2, y2]| & (y2 >= 0 implies (g . p) = (( arccos x2) / (2 * PI ))) & (y2 <= 0 implies (g . p) = (1 - (( arccos x2) / (2 * PI )))) by A27;

          ex x1,y1 be Real st p = |[x1, y1]| & (y1 >= 0 implies (f . p) = (( arccos x1) / (2 * PI ))) & (y1 <= 0 implies (f . p) = (1 - (( arccos x1) / (2 * PI )))) by A26;

          hence (f . p) = (g . p) by A28, SPPOL_2: 1;

        end;

        hence thesis;

      end;

    end

    set A1 = ( R^1 ].(1 / 2), ((1 / 2) + p1).[);

    definition

      :: TOPREALB:def14

      func Circle2IntervalL -> Function of ( Topen_unit_circle c[-10] ), ( R^1 | ( R^1 ].(1 / 2), (3 / 2).[)) means

      : Def14: for p be Point of ( Topen_unit_circle c[-10] ) holds ex x,y be Real st p = |[x, y]| & (y >= 0 implies (it . p) = (1 + (( arccos x) / (2 * PI )))) & (y <= 0 implies (it . p) = (1 - (( arccos x) / (2 * PI ))));

      existence

      proof

        defpred P[ set, set] means ex x,y be Real st $1 = |[x, y]| & (y >= 0 implies $2 = (1 + (( arccos x) / P2))) & (y <= 0 implies $2 = (1 - (( arccos x) / P2)));

        reconsider A1 as non empty Subset of R^1 ;

        

         A1: Ym = A1 by PRE_TOPC: 8;

        

         A2: for x be Element of Xm holds ex y be Element of Ym st P[x, y]

        proof

          let x be Element of Xm;

          

           A3: Xm = (cS1 \ { c[-10] }) by Def10;

          then

           A4: x in cS1 by XBOOLE_0:def 5;

          

           A5: not x in { c[-10] } by A3, XBOOLE_0:def 5;

          

           A6: cS1 is Subset of ( TOP-REAL 2) by TSEP_1: 1;

          then

          consider a,b be Element of REAL such that

           A7: x = <*a, b*> by A4, EUCLID: 51;

          reconsider x1 = x as Point of ( TOP-REAL 2) by A4, A6;

          

           A8: b = (x1 `2 ) by A7, EUCLID: 52;

          set k = ( arccos a);

          

           A9: a = (x1 `1 ) by A7, EUCLID: 52;

          then

           A10: ( - 1) <= a by Th26;

          

           A11: a <= 1 by A9, Th26;

          then

           A12: (k / P2) <= (1 / 2) by A10, Lm22;

          

           A13: (1 ^2 ) = ( |.x1.| ^2 ) by A4, Th12

          .= ((a ^2 ) + (b ^2 )) by A9, A8, JGRAPH_3: 1;

           A14:

          now

            assume

             A15: k = PI ;

            

            then (1 - 1) = (((( - 1) ^2 ) + (b ^2 )) - 1) by A10, A11, A13, SIN_COS6: 98

            .= (((1 ^2 ) + (b ^2 )) - 1);

            then

             A16: b = 0 ;

            a = ( - 1) by A10, A11, A15, SIN_COS6: 98;

            hence contradiction by A7, A5, A16, TARSKI:def 1;

          end;

           A17:

          now

            assume (k / P2) = (1 / 2);

            then ((k / P2) * 2) = ((1 / 2) * 2);

            then (k / PI ) = 1 by XCMPLX_1: 92;

            hence contradiction by A14, XCMPLX_1: 58;

          end;

          

           A18: 0 <= (k / P2) by A10, A11, Lm22;

           A19:

          now

            let y be Real;

            assume

             A20: y = (1 + (k / P2));

            then

             A21: y <> (1 + (1 / 2)) by A17;

            (1 + 0 ) <= y by A18, A20, XREAL_1: 6;

            then

             A22: (1 / 2) < y by XXREAL_0: 2;

            y <= (1 + (1 / 2)) by A12, A20, XREAL_1: 6;

            then y < (3 / 2) by A21, XXREAL_0: 1;

            hence y is Element of Ym by A1, A22, XXREAL_1: 4;

          end;

          per cases ;

            suppose

             A23: b = 0 ;

            reconsider y = (1 + (k / P2)) as Element of Ym by A19;

            take y, a, b;

            thus x = |[a, b]| by A7;

            a <> ( - 1) by A7, A5, A23, TARSKI:def 1;

            then a = 1 by A13, A23, SQUARE_1: 41;

            hence thesis by SIN_COS6: 95;

          end;

            suppose

             A24: b > 0 ;

            reconsider y = (1 + (k / P2)) as Element of Ym by A19;

            take y, a, b;

            thus thesis by A7, A24;

          end;

            suppose

             A25: b < 0 ;

            set y = (1 - (k / P2));

            

             A26: y <> (1 / 2) by A17;

            y >= (1 - (1 / 2)) by A12, XREAL_1: 13;

            then

             A27: (1 / 2) < y by A26, XXREAL_0: 1;

            (1 - 0 ) >= y by A18, XREAL_1: 13;

            then y < (3 / 2) by XXREAL_0: 2;

            then

            reconsider y as Element of Ym by A1, A27, XXREAL_1: 4;

            take y, a, b;

            thus thesis by A7, A25;

          end;

        end;

        ex G be Function of TOUCm, ( R^1 | ( R^1 ].(1 / 2), ((1 / 2) + p1).[)) st for p be Point of TOUCm holds P[p, (G . p)] from FUNCT_2:sch 3( A2);

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of TOUCm, ( R^1 | ( R^1 ].(1 / 2), (3 / 2).[)) such that

         A28: for p be Point of TOUCm holds ex x,y be Real st p = |[x, y]| & (y >= 0 implies (f . p) = (1 + (( arccos x) / (2 * PI )))) & (y <= 0 implies (f . p) = (1 - (( arccos x) / (2 * PI )))) and

         A29: for p be Point of TOUCm holds ex x,y be Real st p = |[x, y]| & (y >= 0 implies (g . p) = (1 + (( arccos x) / (2 * PI )))) & (y <= 0 implies (g . p) = (1 - (( arccos x) / (2 * PI ))));

        now

          let p be Point of TOUCm;

          

           A30: ex x2,y2 be Real st p = |[x2, y2]| & (y2 >= 0 implies (g . p) = (1 + (( arccos x2) / (2 * PI )))) & (y2 <= 0 implies (g . p) = (1 - (( arccos x2) / (2 * PI )))) by A29;

          ex x1,y1 be Real st p = |[x1, y1]| & (y1 >= 0 implies (f . p) = (1 + (( arccos x1) / (2 * PI )))) & (y1 <= 0 implies (f . p) = (1 - (( arccos x1) / (2 * PI )))) by A28;

          hence (f . p) = (g . p) by A30, SPPOL_2: 1;

        end;

        hence thesis;

      end;

    end

    set C = Circle2IntervalR ;

    set Cm = Circle2IntervalL ;

    theorem :: TOPREALB:42

    

     Th42: (( CircleMap ( R^1 0 )) " ) = Circle2IntervalR

    proof

      reconsider A as non empty Subset of R^1 ;

      set f = ( CircleMap ( R^1 0 ));

      set Y = the carrier of ( R^1 | A);

      reconsider f as Function of ( R^1 | A), TOUC by Th32;

      reconsider r0 = ( In ( 0 , REAL )) as Point of R^1 by TOPMETR: 17;

      set F = ( AffineMap ((2 * PI ), 0 ));

      

       A1: ( dom ( id Y)) = Y by RELAT_1: 45;

      ( CircleMap . r0) = c[10] by Th32;

      then

       A2: ( rng f) = X by FUNCT_2:def 3;

      

       A3: Y = A by PRE_TOPC: 8;

       A4:

      now

        let a be object;

        assume

         A5: a in ( dom (C * f));

        then

        reconsider b = a as Point of ( R^1 | A);

        reconsider c = b as Element of REAL by XREAL_0:def 1;

        consider x,y be Real such that

         A6: (f . b) = |[x, y]| and

         A7: y >= 0 implies (C . (f . b)) = (( arccos x) / P2) and

         A8: y <= 0 implies (C . (f . b)) = (1 - (( arccos x) / P2)) by Def13;

        

         A9: (f . b) = ( CircleMap . b) by A3, FUNCT_1: 49

        .= |[(( cos * F) . c), (( sin * F) . c)]| by Lm20;

        then y = (( sin * F) . c) by A6, SPPOL_2: 1;

        then

         A10: y = ( sin . (F . c)) by FUNCT_2: 15;

        x = (( cos * F) . c) by A6, A9, SPPOL_2: 1;

        then x = ( cos . (F . c)) by FUNCT_2: 15;

        then

         A11: x = ( cos (F . c)) by SIN_COS:def 19;

        

         A12: c < 1 by A3, XXREAL_1: 4;

        

         A13: (F . c) = (((2 * PI ) * c) + 0 ) by FCONT_1:def 4;

        then

         A14: ((F . c) / ((2 * PI ) * 1)) = (c / 1) by XCMPLX_1: 91;

        

         A15: (F . (1 - c)) = (((2 * PI ) * (1 - c)) + 0 ) by FCONT_1:def 4;

        then

         A16: ((F . (1 - c)) / ((2 * PI ) * 1)) = ((1 - c) / 1) by XCMPLX_1: 91;

         A17:

        now

          per cases ;

            suppose

             A18: y >= 0 ;

            then not (F . c) in ]. PI , (2 * PI ).[ by A10, COMPTRIG: 9;

            then (F . c) <= PI or (F . c) >= (2 * PI ) by XXREAL_1: 4;

            then ((F . c) / P2) <= ((1 * PI ) / P2) or ((F . c) / P2) >= ((2 * PI ) / P2) by XREAL_1: 72;

            then c <= (1 / 2) by A14, A12, XCMPLX_1: 60, XCMPLX_1: 91;

            then

             A19: ((2 * PI ) * c) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

             0 <= c by A3, XXREAL_1: 4;

            

            hence (C . (f . b)) = ((F . c) / P2) by A7, A11, A13, A18, A19, SIN_COS6: 92

            .= b by A13, XCMPLX_1: 89;

          end;

            suppose

             A20: y < 0 ;

            then not (F . c) in [. 0 , PI .] by A10, COMPTRIG: 8;

            then (F . c) < 0 or (F . c) > PI by XXREAL_1: 1;

            then ((F . c) / P2) < ( 0 / P2) or ((F . c) / P2) > ((1 * PI ) / P2) by XREAL_1: 74;

            then c < 0 or c > (1 / 2) by A14, XCMPLX_1: 91;

            then (1 - c) < (1 - (1 / 2)) by A3, XREAL_1: 15, XXREAL_1: 4;

            then

             A21: ((2 * PI ) * (1 - c)) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

            

             A22: (1 - c) > (1 - 1) by A12, XREAL_1: 15;

            ( cos . (F . (1 - c))) = ( cos (( - ((2 * PI ) * c)) + ((2 * PI ) * 1))) by A15, SIN_COS:def 19

            .= ( cos ( - ((2 * PI ) * c))) by COMPLEX2: 9

            .= ( cos ((2 * PI ) * c)) by SIN_COS: 31;

            

            then ( arccos x) = ( arccos ( cos (F . (1 - c)))) by A11, A13, SIN_COS:def 19

            .= (F . (1 - c)) by A15, A22, A21, SIN_COS6: 92;

            hence (C . (f . b)) = b by A8, A16, A20;

          end;

        end;

        

        thus ((C * f) . a) = (C . (f . b)) by A5, FUNCT_1: 12

        .= (( id Y) . a) by A17;

      end;

      ( dom (C * f)) = Y by FUNCT_2:def 1;

      then C = (f qua Function " ) by A2, A1, A4, FUNCT_1: 2, FUNCT_2: 30;

      hence thesis by TOPS_2:def 4;

    end;

    theorem :: TOPREALB:43

    

     Th43: (( CircleMap ( R^1 (1 / 2))) " ) = Circle2IntervalL

    proof

      reconsider A1 as non empty Subset of R^1 ;

      set f = ( CircleMap ( R^1 (1 / 2)));

      set Y = the carrier of ( R^1 | A1);

      reconsider f as Function of ( R^1 | A1), TOUCm by Lm19;

      set G = ( AffineMap ((2 * PI ), 0 ));

      

       A1: ( dom ( id Ym)) = Ym by RELAT_1: 45;

      

       A2: ( rng f) = Xm by Lm19, FUNCT_2:def 3;

      

       A3: Y = A1 by PRE_TOPC: 8;

       A4:

      now

        let a be object;

        assume

         A5: a in ( dom (Cm * f));

        then

        reconsider b = a as Point of ( R^1 | A1);

        reconsider c = b as Real;

        consider x,y be Real such that

         A6: (f . b) = |[x, y]| and

         A7: y >= 0 implies (Cm . (f . b)) = (1 + (( arccos x) / P2)) and

         A8: y <= 0 implies (Cm . (f . b)) = (1 - (( arccos x) / P2)) by Def14;

        

         A9: (f . b) = ( CircleMap . b) by A3, FUNCT_1: 49

        .= |[( cos ((2 * PI ) * c)), ( sin ((2 * PI ) * c))]| by Def11;

        then

         A10: y = ( sin ((2 * PI ) * c)) by A6, SPPOL_2: 1;

        

         A11: (1 / 2) < c by A3, XXREAL_1: 4;

        then ((2 * PI ) * (1 / 2)) < ((2 * PI ) * c) by XREAL_1: 68;

        then

         A12: ( PI + ((2 * PI ) * 0 )) < ((2 * PI ) * c);

        

         A13: c < (3 / 2) by A3, XXREAL_1: 4;

        then (c - 1) < ((3 / 2) - 1) by XREAL_1: 9;

        then

         A14: ((2 * PI ) * (c - 1)) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

        ((2 * PI ) * c) <= ((2 * PI ) * ((1 / 2) + 1)) by A13, XREAL_1: 64;

        then

         A15: ((2 * PI ) * c) <= ( PI + ((2 * PI ) * 1));

        

         A16: (G . (1 - c)) = (((2 * PI ) * (1 - c)) + 0 ) by FCONT_1:def 4;

        then

         A17: ((G . (1 - c)) / ((2 * PI ) * 1)) = ((1 - c) / 1) by XCMPLX_1: 91;

        

         A18: x = ( cos ((2 * PI ) * c)) by A6, A9, SPPOL_2: 1

        .= ( cos (((2 * PI ) * c) + ((2 * PI ) * ( - 1)))) by COMPLEX2: 9

        .= ( cos ((2 * PI ) * (c - 1)));

         A19:

        now

          per cases ;

            suppose

             A20: c >= 1;

            then

             A21: (1 - 1) <= (c - 1) by XREAL_1: 9;

            ((2 * PI ) * c) >= ((2 * PI ) * 1) by A20, XREAL_1: 64;

            

            hence (Cm . (f . b)) = (1 + (((2 * PI ) * (c - 1)) / P2)) by A7, A18, A10, A14, A15, A21, SIN_COS6: 16, SIN_COS6: 92

            .= (1 + (c - 1)) by XCMPLX_1: 89

            .= b;

          end;

            suppose

             A22: c < 1;

            then ((2 * PI ) * c) < ((2 * PI ) * 1) by XREAL_1: 68;

            then

             A23: ((2 * PI ) * c) < ((2 * PI ) + ((2 * PI ) * 0 ));

            (1 - c) < (1 - (1 / 2)) by A11, XREAL_1: 15;

            then

             A24: ((2 * PI ) * (1 - c)) <= ((2 * PI ) * (1 / 2)) by XREAL_1: 64;

            

             A25: (1 - 1) <= (1 - c) by A22, XREAL_1: 15;

            ( arccos x) = ( arccos ( cos ((2 * PI ) * c))) by A6, A9, SPPOL_2: 1

            .= ( arccos ( cos ( - ((2 * PI ) * c)))) by SIN_COS: 31

            .= ( arccos ( cos (((2 * PI ) * ( - c)) + ((2 * PI ) * 1)))) by COMPLEX2: 9

            .= (G . (1 - c)) by A16, A25, A24, SIN_COS6: 92;

            hence (Cm . (f . b)) = b by A8, A10, A17, A12, A23, SIN_COS6: 12;

          end;

        end;

        

        thus ((Cm * f) . a) = (Cm . (f . b)) by A5, FUNCT_1: 12

        .= (( id Ym) . a) by A19;

      end;

      ( dom (Cm * f)) = Ym by FUNCT_2:def 1;

      then Cm = (f qua Function " ) by A2, A1, A4, FUNCT_1: 2, FUNCT_2: 30;

      hence thesis by TOPS_2:def 4;

    end;

    set A = ]. 0 , 1.[;

    set Q = [.( - 1), 1.[;

    set E = ]. 0 , PI .];

    set j = (1 / P2);

    reconsider Q, E as non empty Subset of REAL ;

    

     Lm25: the carrier of ( R^1 | ( R^1 Q)) = ( R^1 Q) by PRE_TOPC: 8;

    

     Lm26: the carrier of ( R^1 | ( R^1 E)) = ( R^1 E) by PRE_TOPC: 8;

    

     Lm27: the carrier of ( R^1 | ( R^1 A)) = ( R^1 A) by PRE_TOPC: 8;

    set Af = (( AffineMap (j, 0 )) | ( R^1 E));

    ( dom ( AffineMap (j, 0 ))) = R by FUNCT_2:def 1, TOPMETR: 17;

    then

     Lm28: ( dom Af) = ( R^1 E) by RELAT_1: 62;

    ( rng Af) c= A

    proof

      let y be object;

      assume y in ( rng Af);

      then

      consider x be object such that

       A1: x in ( dom Af) and

       A2: (Af . x) = y by FUNCT_1:def 3;

      reconsider x as Real by A1;

      

       A3: y = (( AffineMap (j, 0 )) . x) by A1, A2, Lm28, FUNCT_1: 49

      .= ((j * x) + 0 ) by FCONT_1:def 4

      .= (x / P2) by XCMPLX_1: 99;

      then

      reconsider y as Real;

      x <= PI by A1, Lm28, XXREAL_1: 2;

      then y <= ((1 * PI ) / P2) by A3, XREAL_1: 72;

      then y <= (1 / 2) by XCMPLX_1: 91;

      then

       A4: y < 1 by XXREAL_0: 2;

       0 < x by A1, Lm28, XXREAL_1: 2;

      hence thesis by A3, A4, XXREAL_1: 4;

    end;

    then

    reconsider Af as Function of ( R^1 | ( R^1 E)), ( R^1 | ( R^1 A)) by Lm26, Lm27, Lm28, FUNCT_2: 2;

    

     Lm29: ( R^1 ( AffineMap (j, 0 ))) = ( AffineMap (j, 0 ));

    

     Lm30: ( dom ( AffineMap (j, 0 ))) = REAL by FUNCT_2:def 1;

    

     Lm31: ( rng ( AffineMap (j, 0 ))) = REAL by FCONT_1: 55;

    ( R^1 | ( [#] R^1 )) = R^1 by TSEP_1: 3;

    then

    reconsider Af as continuous Function of ( R^1 | ( R^1 E)), ( R^1 | ( R^1 A)) by Lm29, Lm30, Lm31, TOPMETR: 17, TOPREALA: 8;

    set L = (( R^1 ( AffineMap (( - 1),1))) | ( R^1 A));

    

     Lm32: ( dom ( AffineMap (( - 1),1))) = REAL by FUNCT_2:def 1;

    then

     Lm33: ( dom L) = A by RELAT_1: 62;

    ( rng L) c= A

    proof

      let y be object;

      assume y in ( rng L);

      then

      consider x be object such that

       A1: x in ( dom L) and

       A2: (L . x) = y by FUNCT_1:def 3;

      reconsider x as Real by A1;

       0 < x by A1, Lm33, XXREAL_1: 4;

      then

       A3: (1 - x) < (1 - 0 ) by XREAL_1: 15;

      x < 1 by A1, Lm33, XXREAL_1: 4;

      then

       A4: (1 - 1) < (1 - x) by XREAL_1: 15;

      y = (( AffineMap (( - 1),1)) . x) by A1, A2, Lm33, FUNCT_1: 49

      .= ((( - 1) * x) + 1) by FCONT_1:def 4;

      hence thesis by A4, A3, XXREAL_1: 4;

    end;

    then

    reconsider L as Function of ( R^1 | ( R^1 A)), ( R^1 | ( R^1 A)) by Lm27, Lm33, FUNCT_2: 2;

    

     Lm34: ( rng ( AffineMap (( - 1),1))) = REAL by FCONT_1: 55;

    

     Lm35: ( R^1 | ( [#] R^1 )) = R^1 by TSEP_1: 3;

    then

    reconsider L as continuous Function of ( R^1 | ( R^1 A)), ( R^1 | ( R^1 A)) by Lm32, Lm34, TOPMETR: 17, TOPREALA: 8;

    reconsider ac = ( R^1 arccos ) as continuous Function of ( R^1 | ( R^1 [.( - 1), 1.])), ( R^1 | ( R^1 [. 0 , PI .])) by SIN_COS6: 85, SIN_COS6: 86;

    set c = (ac | ( R^1 Q));

    

     Lm36: ( dom c) = Q by RELAT_1: 62, SIN_COS6: 86, XXREAL_1: 35;

    

     Lm37: ( rng c) c= E

    proof

      let y be object;

      assume

       A1: y in ( rng c);

      then

      consider x be object such that

       A2: x in ( dom c) and

       A3: (c . x) = y by FUNCT_1:def 3;

      reconsider x as Real by A2;

      

       A4: ( - 1) <= x by A2, Lm36, XXREAL_1: 3;

      

       A5: x < 1 by A2, Lm36, XXREAL_1: 3;

      

       A6: ( rng c) c= ( rng ac) by RELAT_1: 70;

      then y in [. 0 , PI .] by A1, SIN_COS6: 85;

      then

      reconsider y as Real;

      

       A7: y <= PI by A1, A6, SIN_COS6: 85, XXREAL_1: 1;

      y = ( arccos . x) by A2, A3, Lm36, FUNCT_1: 49

      .= ( arccos x) by SIN_COS6:def 4;

      then

       A8: y <> 0 by A4, A5, SIN_COS6: 96;

       0 <= y by A1, A6, SIN_COS6: 85, XXREAL_1: 1;

      hence thesis by A7, A8, XXREAL_1: 2;

    end;

    then

    reconsider c as Function of ( R^1 | ( R^1 Q)), ( R^1 | ( R^1 E)) by Lm25, Lm26, Lm36, FUNCT_2: 2;

    the carrier of ( R^1 | ( R^1 [.( - 1), 1.])) = [.( - 1), 1.] by PRE_TOPC: 8;

    then

    reconsider QQ = ( R^1 Q) as Subset of ( R^1 | ( R^1 [.( - 1), 1.])) by XXREAL_1: 35;

    the carrier of ( R^1 | ( R^1 [. 0 , PI .])) = [. 0 , PI .] by PRE_TOPC: 8;

    then

    reconsider EE = ( R^1 E) as Subset of ( R^1 | ( R^1 [. 0 , PI .])) by XXREAL_1: 36;

    

     Lm38: (( R^1 | ( R^1 [.( - 1), 1.])) | QQ) = ( R^1 | ( R^1 Q)) by GOBOARD9: 2;

    (( R^1 | ( R^1 [. 0 , PI .])) | EE) = ( R^1 | ( R^1 E)) by GOBOARD9: 2;

    then

     Lm39: c is continuous by Lm38, TOPREALA: 8;

    reconsider p = proj1 as Function of ( TOP-REAL 2), R^1 by TOPMETR: 17;

    

     Lm40: ( dom p) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

    

     Lm41: p is continuous by JORDAN5A: 27;

    

     Lm42: for aX1 be Subset of TOUC st aX1 = { q where q be Point of ( TOP-REAL 2) : q in X & 0 <= (q `2 ) } holds ( Circle2IntervalR | (TOUC | aX1)) is continuous

    proof

      reconsider c1 = c[-10] as Point of ( TOP-REAL 2);

      let aX1 be Subset of TOUC such that

       A1: aX1 = { q where q be Point of ( TOP-REAL 2) : q in X & 0 <= (q `2 ) };

      

       A2: (c1 `2 ) = 0 by EUCLID: 52;

       c[-10] is Point of ( Topen_unit_circle c[10] ) by Lm15, Th23;

      then c[-10] in aX1 by A1, A2;

      then

      reconsider aX1 as non empty Subset of TOUC;

      set X1 = (TOUC | aX1);

      

       A3: cS1 is Subset of ( TOP-REAL 2) by TSEP_1: 1;

      ( [#] X1) is Subset of TUC by Lm9;

      then

      reconsider B = ( [#] X1) as non empty Subset of ( TOP-REAL 2) by A3, XBOOLE_1: 1;

      set f = (p | B);

      

       A4: ( dom f) = B by Lm40, RELAT_1: 62;

      

       A5: aX1 = the carrier of X1 by PRE_TOPC: 8;

      

       A6: ( rng f) c= Q

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A7: x in ( dom f) and

         A8: (f . x) = y by FUNCT_1:def 3;

        consider q be Point of ( TOP-REAL 2) such that

         A9: q = x and

         A10: q in X and 0 <= (q `2 ) by A1, A5, A4, A7;

        

         A11: ( - 1) <= (q `1 ) by A10, Th27;

        

         A12: (q `1 ) < 1 by A10, Th27;

        y = (p . x) by A4, A7, A8, FUNCT_1: 49

        .= (q `1 ) by A9, PSCOMP_1:def 5;

        hence thesis by A11, A12, XXREAL_1: 3;

      end;

      the carrier of (( TOP-REAL 2) | B) = B by PRE_TOPC: 8;

      then

      reconsider f as Function of (( TOP-REAL 2) | B), ( R^1 | ( R^1 Q)) by A4, A6, Lm25, FUNCT_2: 2;

      X1 is SubSpace of TUC by TSEP_1: 7;

      then X1 is SubSpace of ( TOP-REAL 2) by TSEP_1: 7;

      then

       A13: (( TOP-REAL 2) | B) = X1 by PRE_TOPC:def 5;

      

       A14: for a be Point of X1 holds ((C | X1) . a) = ((Af * (c * f)) . a)

      proof

        let a be Point of X1;

        reconsider b = a as Point of TOUC by PRE_TOPC: 25;

        consider x,y be Real such that

         A15: b = |[x, y]| and

         A16: y >= 0 implies (C . b) = (( arccos x) / P2) and y <= 0 implies (C . b) = (1 - (( arccos x) / P2)) by Def13;

        

         A17: ( |[x, y]| `1 ) < 1 by A15, Th27;

        

         A18: ( |[x, y]| `1 ) = x by EUCLID: 52;

        ( - 1) <= ( |[x, y]| `1 ) by A15, Th26;

        then

         A19: x in Q by A18, A17, XXREAL_1: 3;

        then ( arccos . x) = (c . x) by FUNCT_1: 49;

        then

         A20: ( arccos . x) in ( rng c) by A19, Lm36, FUNCT_1:def 3;

        a in aX1 by A5;

        then ex q be Point of ( TOP-REAL 2) st a = q & q in X & 0 <= (q `2 ) by A1;

        

        hence ((C | X1) . a) = (( arccos x) / P2) by A15, A16, EUCLID: 52, FUNCT_1: 49

        .= (( arccos . x) / P2) by SIN_COS6:def 4

        .= (((1 / P2) * ( arccos . x)) + 0 ) by XCMPLX_1: 99

        .= (( AffineMap (j, 0 )) . ( arccos . x)) by FCONT_1:def 4

        .= (Af . ( arccos . x)) by A20, Lm37, FUNCT_1: 49

        .= (Af . (c . x)) by A19, FUNCT_1: 49

        .= (Af . (c . ( |[x, y]| `1 ))) by EUCLID: 52

        .= (Af . (c . (p . a))) by A15, PSCOMP_1:def 5

        .= (Af . (c . (f . a))) by FUNCT_1: 49

        .= (Af . ((c * f) . a)) by A13, FUNCT_2: 15

        .= ((Af * (c * f)) . a) by A13, FUNCT_2: 15;

      end;

      f is continuous by Lm41, TOPREALA: 8;

      hence thesis by A13, A14, Lm39, FUNCT_2: 63;

    end;

    

     Lm43: for aX1 be Subset of TOUC st aX1 = { q where q be Point of ( TOP-REAL 2) : q in X & 0 >= (q `2 ) } holds ( Circle2IntervalR | (TOUC | aX1)) is continuous

    proof

      reconsider c1 = c[-10] as Point of ( TOP-REAL 2);

      let aX1 be Subset of TOUC such that

       A1: aX1 = { q where q be Point of ( TOP-REAL 2) : q in X & 0 >= (q `2 ) };

      

       A2: (c1 `2 ) = 0 by EUCLID: 52;

       c[-10] is Point of ( Topen_unit_circle c[10] ) by Lm15, Th23;

      then c[-10] in aX1 by A1, A2;

      then

      reconsider aX1 as non empty Subset of TOUC;

      set X1 = (TOUC | aX1);

      

       A3: cS1 is Subset of ( TOP-REAL 2) by TSEP_1: 1;

      ( [#] X1) is Subset of TUC by Lm9;

      then

      reconsider B = ( [#] X1) as non empty Subset of ( TOP-REAL 2) by A3, XBOOLE_1: 1;

      set f = (p | B);

      

       A4: ( dom f) = B by Lm40, RELAT_1: 62;

      

       A5: aX1 = the carrier of X1 by PRE_TOPC: 8;

      

       A6: ( rng f) c= Q

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A7: x in ( dom f) and

         A8: (f . x) = y by FUNCT_1:def 3;

        consider q be Point of ( TOP-REAL 2) such that

         A9: q = x and

         A10: q in X and 0 >= (q `2 ) by A1, A5, A4, A7;

        

         A11: ( - 1) <= (q `1 ) by A10, Th27;

        

         A12: (q `1 ) < 1 by A10, Th27;

        y = (p . x) by A4, A7, A8, FUNCT_1: 49

        .= (q `1 ) by A9, PSCOMP_1:def 5;

        hence thesis by A11, A12, XXREAL_1: 3;

      end;

      

       A13: the carrier of (( TOP-REAL 2) | B) = B by PRE_TOPC: 8;

      then

      reconsider f as Function of (( TOP-REAL 2) | B), ( R^1 | ( R^1 Q)) by A4, A6, Lm25, FUNCT_2: 2;

      X1 is SubSpace of TUC by TSEP_1: 7;

      then X1 is SubSpace of ( TOP-REAL 2) by TSEP_1: 7;

      then

       A14: (( TOP-REAL 2) | B) = X1 by PRE_TOPC:def 5;

      

       A15: for a be Point of X1 holds ((C | X1) . a) = ((L * (Af * (c * f))) . a)

      proof

        let a be Point of X1;

        reconsider b = a as Point of TOUC by PRE_TOPC: 25;

        consider x,y be Real such that

         A16: b = |[x, y]| and y >= 0 implies (C . b) = (( arccos x) / P2) and

         A17: y <= 0 implies (C . b) = (1 - (( arccos x) / P2)) by Def13;

        

         A18: ( |[x, y]| `1 ) < 1 by A16, Th27;

        ( dom (Af * (c * f))) = the carrier of (( TOP-REAL 2) | B) by FUNCT_2:def 1;

        then

         A19: ((Af * (c * f)) . a) in ( rng (Af * (c * f))) by A13, FUNCT_1:def 3;

        reconsider r = ((Af * (c * f)) . a) as Real;

        a in aX1 by A5;

        then

         A20: ex q be Point of ( TOP-REAL 2) st a = q & q in X & 0 >= (q `2 ) by A1;

        

         A21: ( |[x, y]| `1 ) = x by EUCLID: 52;

        ( - 1) <= ( |[x, y]| `1 ) by A16, Th26;

        then

         A22: x in Q by A21, A18, XXREAL_1: 3;

        then ( arccos . x) = (c . x) by FUNCT_1: 49;

        then

         A23: ( arccos . x) in ( rng c) by A22, Lm36, FUNCT_1:def 3;

        (( arccos x) / P2) = (( arccos . x) / P2) by SIN_COS6:def 4

        .= ((j * ( arccos . x)) + 0 ) by XCMPLX_1: 99

        .= (( AffineMap (j, 0 )) . ( arccos . x)) by FCONT_1:def 4

        .= (Af . ( arccos . x)) by A23, Lm37, FUNCT_1: 49

        .= (Af . (c . x)) by A22, FUNCT_1: 49

        .= (Af . (c . ( |[x, y]| `1 ))) by EUCLID: 52

        .= (Af . (c . (p . a))) by A16, PSCOMP_1:def 5

        .= (Af . (c . (f . a))) by FUNCT_1: 49

        .= (Af . ((c * f) . a)) by A14, FUNCT_2: 15

        .= ((Af * (c * f)) . a) by A14, FUNCT_2: 15;

        

        hence ((C | X1) . a) = ((( - 1) * r) + 1) by A16, A17, A20, EUCLID: 52, FUNCT_1: 49

        .= (( R^1 ( AffineMap (( - 1),1))) . r) by FCONT_1:def 4

        .= (L . r) by A19, Lm27, FUNCT_1: 49

        .= ((L * (Af * (c * f))) . a) by A14, FUNCT_2: 15;

      end;

      f is continuous by Lm41, TOPREALA: 8;

      hence thesis by A14, A15, Lm39, FUNCT_2: 63;

    end;

    

     Lm44: for p be Point of ( Topen_unit_circle c[10] ) st p = c[-10] holds Circle2IntervalR is_continuous_at p

    proof

      reconsider c1 = c[-10] as Point of ( TOP-REAL 2);

      set aX2 = { q where q be Point of ( TOP-REAL 2) : q in X & 0 >= (q `2 ) };

      set aX1 = { q where q be Point of ( TOP-REAL 2) : q in X & 0 <= (q `2 ) };

      

       A1: aX1 c= X

      proof

        let x be object;

        assume x in aX1;

        then ex q be Point of ( TOP-REAL 2) st x = q & q in X & 0 <= (q `2 );

        hence thesis;

      end;

      

       A2: aX2 c= X

      proof

        let x be object;

        assume x in aX2;

        then ex q be Point of ( TOP-REAL 2) st x = q & q in X & 0 >= (q `2 );

        hence thesis;

      end;

      

       A3: TOUC is SubSpace of TOUC by TSEP_1: 2;

      

       A4: (c1 `2 ) = 0 by EUCLID: 52;

      

       A5: c[-10] is Point of ( Topen_unit_circle c[10] ) by Lm15, Th23;

      then

       A6: c[-10] in aX1 by A4;

      

       A7: c[-10] in aX2 by A4, A5;

      then

      reconsider aX1, aX2 as non empty Subset of TOUC by A1, A2, A6;

      set X1 = (TOUC | aX1);

      let p be Point of ( Topen_unit_circle c[10] ) such that

       A8: p = c[-10] ;

      reconsider x1 = p as Point of X1 by A8, A6, PRE_TOPC: 8;

      set X2 = (TOUC | aX2);

      reconsider x2 = p as Point of X2 by A8, A7, PRE_TOPC: 8;

      

       A9: the carrier of X2 = aX2 by PRE_TOPC: 8;

      X c= (aX1 \/ aX2)

      proof

        let a be object;

        assume

         A10: a in X;

        then

        reconsider a as Point of ( TOP-REAL 2) by Lm8;

         0 >= (a `2 ) or 0 <= (a `2 );

        then a in aX1 or a in aX2 by A10;

        hence thesis by XBOOLE_0:def 3;

      end;

      then

       A11: X = (aX1 \/ aX2);

      (C | X2) is continuous by Lm43;

      then

       A12: (C | X2) is_continuous_at x2;

      (C | X1) is continuous by Lm42;

      then

       A13: (C | X1) is_continuous_at x1;

      the carrier of X1 = aX1 by PRE_TOPC: 8;

      then TOUC = (X1 union X2) by A9, A3, A11, TSEP_1:def 2;

      hence thesis by A13, A12, TMAP_1: 113;

    end;

    reconsider jj = 1 as Element of REAL by XREAL_0:def 1;

    set h1 = ( REAL --> jj);

    reconsider h1 as PartFunc of REAL , REAL ;

    

     Lm45: Circle2IntervalR is continuous

    proof

      set h = (j (#) arccos );

      set K = [.( - 1), 1.];

      set J = [.p0, 0 .[;

      set I = ]. 0 , p1.];

      set Z = ( R^1 | ( R^1 ]. 0 , ( 0 + p1).[));

      for p be Point of TOUC holds C is_continuous_at p

      proof

        ( Tcircle (( 0. ( TOP-REAL 2)),1)) is SubSpace of TREC by Th10;

        then

         A1: TOUC is SubSpace of TREC by TSEP_1: 7;

        let p be Point of TOUC;

        

         A2: K = ( [#] CIT) by TOPMETR: 18;

        reconsider q = p as Point of ( TOP-REAL 2) by Lm8;

        

         A3: the carrier of Z = ]. 0 , ( 0 + p1).[ by PRE_TOPC: 8;

        consider x,y be Real such that

         A4: p = |[x, y]| and

         A5: y >= 0 implies (C . p) = (( arccos x) / P2) and

         A6: y <= 0 implies (C . p) = (1 - (( arccos x) / P2)) by Def13;

        

         A7: y = (q `2 ) by A4, EUCLID: 52;

        

         A8: x = (q `1 ) by A4, EUCLID: 52;

        then

         A9: x <= 1 by Th26;

        ( - 1) <= x by A8, Th26;

        then

         A10: x in K by A9, XXREAL_1: 1;

        then

         A11: ((h | K) . x) = (h . x) by FUNCT_1: 49;

        ( dom h) = ( dom arccos ) by VALUED_1:def 5

        .= K by SIN_COS6: 86;

        then x in ( dom (h | K)) by A10, RELAT_1: 57;

        then

         A12: (h | K) is_continuous_in x by FCONT_1:def 2;

        

         A13: ( dom h) = ( dom arccos ) by VALUED_1:def 5;

        

        then

         A14: (h . x) = (( arccos . x) * j) by A10, SIN_COS6: 86, VALUED_1:def 5

        .= ((1 * ( arccos . x)) / P2) by XCMPLX_1: 74;

        per cases ;

          suppose y = 0 ;

          hence thesis by A7, Lm44, Th24;

        end;

          suppose

           A15: y < 0 ;

          for V be Subset of Z st V is open & (C . p) in V holds ex W be Subset of TOUC st W is open & p in W & (C .: W) c= V

          proof

            set hh = (h1 - h);

            let V be Subset of Z such that

             A16: V is open and

             A17: (C . p) in V;

            reconsider V1 = V as Subset of REAL by A3, XBOOLE_1: 1;

            reconsider V2 = V1 as Subset of R^1 by TOPMETR: 17;

            V2 is open by A16, TSEP_1: 17;

            then

            reconsider V1 as open Subset of REAL by BORSUK_5: 39;

            consider N1 be Neighbourhood of (C . p) such that

             A18: N1 c= V1 by A17, RCOMP_1: 18;

            

             A19: ((hh | K) . x) = (hh . x) by A10, FUNCT_1: 49;

            ( dom hh) = (( dom h1) /\ ( dom h)) by VALUED_1: 12;

            

            then

             A20: ( dom hh) = ( REAL /\ ( dom h))

            .= K by A13, SIN_COS6: 86, XBOOLE_1: 28;

            then

             A21: ( dom (hh | K)) = K by RELAT_1: 62;

            

             A22: (C . p) = (1 - (( arccos . x) / P2)) by A6, A15, SIN_COS6:def 4;

            

             A23: p = ((1,2) --> (x,y)) by A4, TOPREALA: 28;

            x in ( dom (hh | K)) by A10, A20, RELAT_1: 57;

            then

             A24: (hh | K) is_continuous_in x by FCONT_1:def 2;

            (hh . x) = ((h1 . x) - (h . x)) by A10, A20, VALUED_1: 13

            .= (1 - ((1 * ( arccos . x)) / P2)) by A10, A14, FUNCOP_1: 7;

            then

            consider N be Neighbourhood of x such that

             A25: ((hh | K) .: N) c= N1 by A22, A19, A24, FCONT_1: 5;

            set N3 = (N /\ K);

            

             A26: N3 c= K by XBOOLE_1: 17;

            reconsider N3, J as Subset of CIT by Lm2, XBOOLE_1: 17, XXREAL_1: 35;

            set W = (( product ((1,2) --> (N3,J))) /\ X);

            reconsider W as Subset of TOUC by XBOOLE_1: 17;

            take W;

            reconsider KK = ( product ((1,2) --> (N3,J))) as Subset of TREC by TOPREALA: 38;

            reconsider I3 = J as open Subset of CIT by TOPREALA: 26;

            

             A27: ((hh | K) .: N3) c= ((hh | K) .: N) by RELAT_1: 123, XBOOLE_1: 17;

            ( R^1 N) = N;

            then

            reconsider M3 = N3 as open Subset of CIT by A2, TOPS_2: 24;

            KK = ( product ((1,2) --> (M3,I3)));

            then KK is open by TOPREALA: 39;

            hence W is open by A1, Lm16, TOPS_2: 24;

            x in N by RCOMP_1: 16;

            then

             A28: x in N3 by A10, XBOOLE_0:def 4;

            y >= ( - 1) by A7, Th26;

            then y in J by A15, XXREAL_1: 3;

            then p in ( product ((1,2) --> (N3,J))) by A23, A28, HILBERT3: 11;

            hence p in W by XBOOLE_0:def 4;

            let m be object;

            assume m in (C .: W);

            then

            consider c be Element of TOUC such that

             A29: c in W and

             A30: m = (C . c) by FUNCT_2: 65;

            

             A31: c in ( product ((1,2) --> (N3,J))) by A29, XBOOLE_0:def 4;

            then

             A32: (c . 1) in N3 by TOPREALA: 3;

            consider c1,c2 be Real such that

             A33: c = |[c1, c2]| and c2 >= 0 implies (C . c) = (( arccos c1) / P2) and

             A34: c2 <= 0 implies (C . c) = (1 - (( arccos c1) / P2)) by Def13;

            (c . 2) in J by A31, TOPREALA: 3;

            then c2 in J by A33, TOPREALA: 29;

            then

             A35: (1 - ((1 * ( arccos c1)) * j)) = m by A30, A34, XCMPLX_1: 74, XXREAL_1: 3;

            ((hh | K) . (c . 1)) = (hh . (c . 1)) by A26, A32, FUNCT_1: 49

            .= ((h1 . (c . 1)) - (h . (c . 1))) by A20, A26, A32, VALUED_1: 13

            .= (1 - (h . (c . 1))) by A32, FUNCOP_1: 7

            .= (1 - (( arccos . (c . 1)) * j)) by A13, A26, A32, SIN_COS6: 86, VALUED_1:def 5

            .= (1 - (( arccos . c1) * j)) by A33, TOPREALA: 29

            .= (1 - (( arccos c1) * j)) by SIN_COS6:def 4;

            then m in ((hh | K) .: N3) by A26, A32, A21, A35, FUNCT_1:def 6;

            then m in ((hh | K) .: N) by A27;

            then m in N1 by A25;

            hence thesis by A18;

          end;

          hence thesis by TMAP_1: 43;

        end;

          suppose

           A36: y > 0 ;

          for V be Subset of Z st V is open & (C . p) in V holds ex W be Subset of TOUC st W is open & p in W & (C .: W) c= V

          proof

            let V be Subset of Z such that

             A37: V is open and

             A38: (C . p) in V;

            reconsider V1 = V as Subset of REAL by A3, XBOOLE_1: 1;

            reconsider V2 = V1 as Subset of R^1 by TOPMETR: 17;

            V2 is open by A37, TSEP_1: 17;

            then

            reconsider V1 as open Subset of REAL by BORSUK_5: 39;

            consider N1 be Neighbourhood of (C . p) such that

             A39: N1 c= V1 by A38, RCOMP_1: 18;

            (C . p) = (( arccos . x) / P2) by A5, A36, SIN_COS6:def 4;

            then

            consider N be Neighbourhood of x such that

             A40: ((h | K) .: N) c= N1 by A11, A14, A12, FCONT_1: 5;

            set N3 = (N /\ K);

            

             A41: N3 c= K by XBOOLE_1: 17;

            reconsider N3, I as Subset of CIT by Lm2, XBOOLE_1: 17, XXREAL_1: 36;

            set W = (( product ((1,2) --> (N3,I))) /\ X);

            reconsider W as Subset of TOUC by XBOOLE_1: 17;

            take W;

            reconsider KK = ( product ((1,2) --> (N3,I))) as Subset of TREC by TOPREALA: 38;

            reconsider I3 = I as open Subset of CIT by TOPREALA: 25;

            

             A42: ((h | K) .: N3) c= ((h | K) .: N) by RELAT_1: 123, XBOOLE_1: 17;

            ( R^1 N) = N;

            then

            reconsider M3 = N3 as open Subset of CIT by A2, TOPS_2: 24;

            KK = ( product ((1,2) --> (M3,I3)));

            then KK is open by TOPREALA: 39;

            hence W is open by A1, Lm16, TOPS_2: 24;

            x in N by RCOMP_1: 16;

            then

             A43: x in N3 by A10, XBOOLE_0:def 4;

            

             A44: ( dom (h | K)) = K by A13, RELAT_1: 62, SIN_COS6: 86;

            

             A45: p = ((1,2) --> (x,y)) by A4, TOPREALA: 28;

            y <= 1 by A7, Th26;

            then y in I by A36, XXREAL_1: 2;

            then p in ( product ((1,2) --> (N3,I))) by A45, A43, HILBERT3: 11;

            hence p in W by XBOOLE_0:def 4;

            let m be object;

            assume m in (C .: W);

            then

            consider c be Element of TOUC such that

             A46: c in W and

             A47: m = (C . c) by FUNCT_2: 65;

            

             A48: c in ( product ((1,2) --> (N3,I))) by A46, XBOOLE_0:def 4;

            then

             A49: (c . 1) in N3 by TOPREALA: 3;

            consider c1,c2 be Real such that

             A50: c = |[c1, c2]| and

             A51: c2 >= 0 implies (C . c) = (( arccos c1) / P2) and c2 <= 0 implies (C . c) = (1 - (( arccos c1) / P2)) by Def13;

            (c . 2) in I by A48, TOPREALA: 3;

            then c2 in I by A50, TOPREALA: 29;

            then

             A52: ((1 * ( arccos c1)) * j) = m by A47, A51, XCMPLX_1: 74, XXREAL_1: 2;

            ((h | K) . (c . 1)) = (h . (c . 1)) by A41, A49, FUNCT_1: 49

            .= (( arccos . (c . 1)) * j) by A13, A41, A49, SIN_COS6: 86, VALUED_1:def 5

            .= (( arccos . c1) * j) by A50, TOPREALA: 29

            .= (( arccos c1) * j) by SIN_COS6:def 4;

            then m in ((h | K) .: N3) by A41, A49, A44, A52, FUNCT_1:def 6;

            then m in ((h | K) .: N) by A42;

            then m in N1 by A40;

            hence thesis by A39;

          end;

          hence thesis by TMAP_1: 43;

        end;

      end;

      hence thesis by TMAP_1: 44;

    end;

    set A = ].(1 / 2), ((1 / 2) + p1).[;

    set Q = ].( - 1), 1.];

    set E = [. 0 , PI .[;

    reconsider Q, E as non empty Subset of REAL ;

    

     Lm46: the carrier of ( R^1 | ( R^1 Q)) = ( R^1 Q) by PRE_TOPC: 8;

    

     Lm47: the carrier of ( R^1 | ( R^1 E)) = ( R^1 E) by PRE_TOPC: 8;

    

     Lm48: the carrier of ( R^1 | ( R^1 A)) = ( R^1 A) by PRE_TOPC: 8;

    set Af = (( AffineMap (( - j),1)) | ( R^1 E));

    ( dom ( AffineMap (( - j),1))) = R by FUNCT_2:def 1, TOPMETR: 17;

    then

     Lm49: ( dom Af) = ( R^1 E) by RELAT_1: 62;

    ( rng Af) c= A

    proof

      let y be object;

      assume y in ( rng Af);

      then

      consider x be object such that

       A1: x in ( dom Af) and

       A2: (Af . x) = y by FUNCT_1:def 3;

      reconsider x as Real by A1;

      

       A3: y = (( AffineMap (( - j),1)) . x) by A1, A2, Lm49, FUNCT_1: 49

      .= ((( - j) * x) + 1) by FCONT_1:def 4

      .= (( - (j * x)) + 1)

      .= (( - (x / P2)) + 1) by XCMPLX_1: 99;

      then

      reconsider y as Real;

      x < PI by A1, Lm49, XXREAL_1: 3;

      then (x / P2) < ((1 * PI ) / P2) by XREAL_1: 74;

      then (x / P2) < (1 / 2) by XCMPLX_1: 91;

      then ( - (x / P2)) > ( - (1 / 2)) by XREAL_1: 24;

      then

       A4: (( - (x / P2)) + 1) > (( - (1 / 2)) + 1) by XREAL_1: 6;

       0 <= x by A1, Lm49, XXREAL_1: 3;

      then ( 0 + 1) >= (( - (x / P2)) + 1) by XREAL_1: 6;

      then y < (3 / 2) by A3, XXREAL_0: 2;

      hence thesis by A3, A4, XXREAL_1: 4;

    end;

    then

    reconsider Af as Function of ( R^1 | ( R^1 E)), ( R^1 | ( R^1 A)) by Lm47, Lm48, Lm49, FUNCT_2: 2;

    

     Lm50: ( R^1 ( AffineMap (( - j),1))) = ( AffineMap (( - j),1));

    

     Lm51: ( dom ( AffineMap (( - j),1))) = REAL by FUNCT_2:def 1;

    ( rng ( AffineMap (( - j),1))) = REAL by FCONT_1: 55;

    then

    reconsider Af as continuous Function of ( R^1 | ( R^1 E)), ( R^1 | ( R^1 A)) by Lm35, Lm50, Lm51, TOPMETR: 17, TOPREALA: 8;

    set Af1 = (( AffineMap (j,1)) | ( R^1 E));

    ( dom ( AffineMap (j,1))) = R by FUNCT_2:def 1, TOPMETR: 17;

    then

     Lm52: ( dom Af1) = ( R^1 E) by RELAT_1: 62;

    ( rng Af1) c= A

    proof

      let y be object;

      assume y in ( rng Af1);

      then

      consider x be object such that

       A1: x in ( dom Af1) and

       A2: (Af1 . x) = y by FUNCT_1:def 3;

      reconsider x as Real by A1;

      

       A3: y = (( AffineMap (j,1)) . x) by A1, A2, Lm52, FUNCT_1: 49

      .= ((j * x) + 1) by FCONT_1:def 4

      .= ((x / P2) + 1) by XCMPLX_1: 99;

      then

      reconsider y as Real;

      x < PI by A1, Lm52, XXREAL_1: 3;

      then (x / P2) < ((1 * PI ) / P2) by XREAL_1: 74;

      then (x / P2) < (1 / 2) by XCMPLX_1: 91;

      then

       A4: ((x / P2) + 1) < ((1 / 2) + 1) by XREAL_1: 6;

       0 <= x by A1, Lm52, XXREAL_1: 3;

      then ( 0 + 1) <= ((x / P2) + 1) by XREAL_1: 6;

      then (1 / 2) < y by A3, XXREAL_0: 2;

      hence thesis by A3, A4, XXREAL_1: 4;

    end;

    then

    reconsider Af1 as Function of ( R^1 | ( R^1 E)), ( R^1 | ( R^1 A)) by Lm47, Lm48, Lm52, FUNCT_2: 2;

    

     Lm53: ( R^1 ( AffineMap (j,1))) = ( AffineMap (j,1));

    

     Lm54: ( dom ( AffineMap (j,1))) = REAL by FUNCT_2:def 1;

    ( rng ( AffineMap (j,1))) = REAL by FCONT_1: 55;

    then

    reconsider Af1 as continuous Function of ( R^1 | ( R^1 E)), ( R^1 | ( R^1 A)) by Lm35, Lm53, Lm54, TOPMETR: 17, TOPREALA: 8;

    set c = (ac | ( R^1 Q));

    

     Lm55: ( dom c) = Q by RELAT_1: 62, SIN_COS6: 86, XXREAL_1: 36;

    

     Lm56: ( rng c) c= E

    proof

      let y be object;

      assume

       A1: y in ( rng c);

      then

      consider x be object such that

       A2: x in ( dom c) and

       A3: (c . x) = y by FUNCT_1:def 3;

      

       A4: ( rng c) c= ( rng ac) by RELAT_1: 70;

      then y in [. 0 , PI .] by A1, SIN_COS6: 85;

      then

      reconsider y as Real;

      

       A5: 0 <= y by A1, A4, SIN_COS6: 85, XXREAL_1: 1;

      

       A6: y <= PI by A1, A4, SIN_COS6: 85, XXREAL_1: 1;

      reconsider x as Real by A2;

      

       A7: ( - 1) < x by A2, Lm55, XXREAL_1: 2;

      

       A8: x <= 1 by A2, Lm55, XXREAL_1: 2;

      y = ( arccos . x) by A2, A3, Lm55, FUNCT_1: 49

      .= ( arccos x) by SIN_COS6:def 4;

      then y < PI by A6, A7, A8, SIN_COS6: 98, XXREAL_0: 1;

      hence thesis by A5, XXREAL_1: 3;

    end;

    then

    reconsider c as Function of ( R^1 | ( R^1 Q)), ( R^1 | ( R^1 E)) by Lm46, Lm47, Lm55, FUNCT_2: 2;

    the carrier of ( R^1 | ( R^1 [.( - 1), 1.])) = [.( - 1), 1.] by PRE_TOPC: 8;

    then

    reconsider QQ = ( R^1 Q) as Subset of ( R^1 | ( R^1 [.( - 1), 1.])) by XXREAL_1: 36;

    the carrier of ( R^1 | ( R^1 [. 0 , PI .])) = [. 0 , PI .] by PRE_TOPC: 8;

    then

    reconsider EE = ( R^1 E) as Subset of ( R^1 | ( R^1 [. 0 , PI .])) by XXREAL_1: 35;

    

     Lm57: (( R^1 | ( R^1 [.( - 1), 1.])) | QQ) = ( R^1 | ( R^1 Q)) by GOBOARD9: 2;

    (( R^1 | ( R^1 [. 0 , PI .])) | EE) = ( R^1 | ( R^1 E)) by GOBOARD9: 2;

    then

     Lm58: c is continuous by Lm57, TOPREALA: 8;

    

     Lm59: for aX1 be Subset of TOUCm st aX1 = { q where q be Point of ( TOP-REAL 2) : q in Xm & 0 <= (q `2 ) } holds ( Circle2IntervalL | (TOUCm | aX1)) is continuous

    proof

      reconsider c1 = c[10] as Point of ( TOP-REAL 2);

      let aX1 be Subset of TOUCm such that

       A1: aX1 = { q where q be Point of ( TOP-REAL 2) : q in Xm & 0 <= (q `2 ) };

      

       A2: (c1 `2 ) = 0 by EUCLID: 52;

       c[10] is Point of ( Topen_unit_circle c[-10] ) by Lm15, Th23;

      then c[10] in aX1 by A1, A2;

      then

      reconsider aX1 as non empty Subset of TOUCm;

      set X1 = (TOUCm | aX1);

      

       A3: cS1 is Subset of ( TOP-REAL 2) by TSEP_1: 1;

      ( [#] X1) is Subset of TUC by Lm9;

      then

      reconsider B = ( [#] X1) as non empty Subset of ( TOP-REAL 2) by A3, XBOOLE_1: 1;

      set f = (p | B);

      

       A4: ( dom f) = B by Lm40, RELAT_1: 62;

      

       A5: aX1 = the carrier of X1 by PRE_TOPC: 8;

      

       A6: ( rng f) c= Q

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A7: x in ( dom f) and

         A8: (f . x) = y by FUNCT_1:def 3;

        consider q be Point of ( TOP-REAL 2) such that

         A9: q = x and

         A10: q in Xm and 0 <= (q `2 ) by A1, A5, A4, A7;

        

         A11: ( - 1) < (q `1 ) by A10, Th28;

        

         A12: (q `1 ) <= 1 by A10, Th28;

        y = (p . x) by A4, A7, A8, FUNCT_1: 49

        .= (q `1 ) by A9, PSCOMP_1:def 5;

        hence thesis by A11, A12, XXREAL_1: 2;

      end;

      the carrier of (( TOP-REAL 2) | B) = B by PRE_TOPC: 8;

      then

      reconsider f as Function of (( TOP-REAL 2) | B), ( R^1 | ( R^1 Q)) by A4, A6, Lm46, FUNCT_2: 2;

      X1 is SubSpace of TUC by TSEP_1: 7;

      then X1 is SubSpace of ( TOP-REAL 2) by TSEP_1: 7;

      then

       A13: (( TOP-REAL 2) | B) = X1 by PRE_TOPC:def 5;

      

       A14: for a be Point of X1 holds ((Cm | X1) . a) = ((Af1 * (c * f)) . a)

      proof

        let a be Point of X1;

        reconsider b = a as Point of TOUCm by PRE_TOPC: 25;

        consider x,y be Real such that

         A15: b = |[x, y]| and

         A16: y >= 0 implies (Cm . b) = (1 + (( arccos x) / P2)) and y <= 0 implies (Cm . b) = (1 - (( arccos x) / P2)) by Def14;

        

         A17: ( |[x, y]| `1 ) <= 1 by A15, Th28;

        

         A18: ( |[x, y]| `1 ) = x by EUCLID: 52;

        ( - 1) < ( |[x, y]| `1 ) by A15, Th28;

        then

         A19: x in Q by A18, A17, XXREAL_1: 2;

        then ( arccos . x) = (c . x) by FUNCT_1: 49;

        then

         A20: ( arccos . x) in ( rng c) by A19, Lm55, FUNCT_1:def 3;

        a in aX1 by A5;

        then ex q be Point of ( TOP-REAL 2) st a = q & q in Xm & 0 <= (q `2 ) by A1;

        

        hence ((Cm | X1) . a) = (1 + (( arccos x) / P2)) by A15, A16, EUCLID: 52, FUNCT_1: 49

        .= (1 + (( arccos . x) / P2)) by SIN_COS6:def 4

        .= (1 + (j * ( arccos . x))) by XCMPLX_1: 99

        .= (( AffineMap (j,1)) . ( arccos . x)) by FCONT_1:def 4

        .= (Af1 . ( arccos . x)) by A20, Lm56, FUNCT_1: 49

        .= (Af1 . (c . x)) by A19, FUNCT_1: 49

        .= (Af1 . (c . ( |[x, y]| `1 ))) by EUCLID: 52

        .= (Af1 . (c . (p . a))) by A15, PSCOMP_1:def 5

        .= (Af1 . (c . (f . a))) by FUNCT_1: 49

        .= (Af1 . ((c * f) . a)) by A13, FUNCT_2: 15

        .= ((Af1 * (c * f)) . a) by A13, FUNCT_2: 15;

      end;

      f is continuous by Lm41, TOPREALA: 8;

      hence thesis by A13, A14, Lm58, FUNCT_2: 63;

    end;

    

     Lm60: for aX1 be Subset of TOUCm st aX1 = { q where q be Point of ( TOP-REAL 2) : q in Xm & 0 >= (q `2 ) } holds ( Circle2IntervalL | (TOUCm | aX1)) is continuous

    proof

      reconsider c1 = c[10] as Point of ( TOP-REAL 2);

      let aX1 be Subset of TOUCm such that

       A1: aX1 = { q where q be Point of ( TOP-REAL 2) : q in Xm & 0 >= (q `2 ) };

      

       A2: (c1 `2 ) = 0 by EUCLID: 52;

       c[10] is Point of ( Topen_unit_circle c[-10] ) by Lm15, Th23;

      then c[10] in aX1 by A1, A2;

      then

      reconsider aX1 as non empty Subset of TOUCm;

      set X1 = (TOUCm | aX1);

      

       A3: cS1 is Subset of ( TOP-REAL 2) by TSEP_1: 1;

      ( [#] X1) is Subset of TUC by Lm9;

      then

      reconsider B = ( [#] X1) as non empty Subset of ( TOP-REAL 2) by A3, XBOOLE_1: 1;

      set f = (p | B);

      

       A4: ( dom f) = B by Lm40, RELAT_1: 62;

      

       A5: aX1 = the carrier of X1 by PRE_TOPC: 8;

      

       A6: ( rng f) c= Q

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A7: x in ( dom f) and

         A8: (f . x) = y by FUNCT_1:def 3;

        consider q be Point of ( TOP-REAL 2) such that

         A9: q = x and

         A10: q in Xm and 0 >= (q `2 ) by A1, A5, A4, A7;

        

         A11: ( - 1) < (q `1 ) by A10, Th28;

        

         A12: (q `1 ) <= 1 by A10, Th28;

        y = (p . x) by A4, A7, A8, FUNCT_1: 49

        .= (q `1 ) by A9, PSCOMP_1:def 5;

        hence thesis by A11, A12, XXREAL_1: 2;

      end;

      the carrier of (( TOP-REAL 2) | B) = B by PRE_TOPC: 8;

      then

      reconsider f as Function of (( TOP-REAL 2) | B), ( R^1 | ( R^1 Q)) by A4, A6, Lm46, FUNCT_2: 2;

      X1 is SubSpace of TUC by TSEP_1: 7;

      then X1 is SubSpace of ( TOP-REAL 2) by TSEP_1: 7;

      then

       A13: (( TOP-REAL 2) | B) = X1 by PRE_TOPC:def 5;

      

       A14: for a be Point of X1 holds ((Cm | X1) . a) = ((Af * (c * f)) . a)

      proof

        let a be Point of X1;

        reconsider b = a as Point of TOUCm by PRE_TOPC: 25;

        consider x,y be Real such that

         A15: b = |[x, y]| and y >= 0 implies (Cm . b) = (1 + (( arccos x) / P2)) and

         A16: y <= 0 implies (Cm . b) = (1 - (( arccos x) / P2)) by Def14;

        

         A17: ( |[x, y]| `1 ) <= 1 by A15, Th28;

        

         A18: ( |[x, y]| `1 ) = x by EUCLID: 52;

        ( - 1) < ( |[x, y]| `1 ) by A15, Th28;

        then

         A19: x in Q by A18, A17, XXREAL_1: 2;

        then ( arccos . x) = (c . x) by FUNCT_1: 49;

        then

         A20: ( arccos . x) in ( rng c) by A19, Lm55, FUNCT_1:def 3;

        a in aX1 by A5;

        then ex q be Point of ( TOP-REAL 2) st a = q & q in Xm & 0 >= (q `2 ) by A1;

        

        hence ((Cm | X1) . a) = (1 - (( arccos x) / P2)) by A15, A16, EUCLID: 52, FUNCT_1: 49

        .= (1 - (( arccos . x) / P2)) by SIN_COS6:def 4

        .= (1 - (j * ( arccos . x))) by XCMPLX_1: 99

        .= ((( - j) * ( arccos . x)) + 1)

        .= (( AffineMap (( - j),1)) . ( arccos . x)) by FCONT_1:def 4

        .= (Af . ( arccos . x)) by A20, Lm56, FUNCT_1: 49

        .= (Af . (c . x)) by A19, FUNCT_1: 49

        .= (Af . (c . ( |[x, y]| `1 ))) by EUCLID: 52

        .= (Af . (c . (p . a))) by A15, PSCOMP_1:def 5

        .= (Af . (c . (f . a))) by FUNCT_1: 49

        .= (Af . ((c * f) . a)) by A13, FUNCT_2: 15

        .= ((Af * (c * f)) . a) by A13, FUNCT_2: 15;

      end;

      f is continuous by Lm41, TOPREALA: 8;

      hence thesis by A13, A14, Lm58, FUNCT_2: 63;

    end;

    

     Lm61: for p be Point of ( Topen_unit_circle c[-10] ) st p = c[10] holds Circle2IntervalL is_continuous_at p

    proof

      reconsider c1 = c[10] as Point of ( TOP-REAL 2);

      set aX2 = { q where q be Point of ( TOP-REAL 2) : q in Xm & 0 >= (q `2 ) };

      set aX1 = { q where q be Point of ( TOP-REAL 2) : q in Xm & 0 <= (q `2 ) };

      

       A1: aX1 c= Xm

      proof

        let x be object;

        assume x in aX1;

        then ex q be Point of ( TOP-REAL 2) st x = q & q in Xm & 0 <= (q `2 );

        hence thesis;

      end;

      

       A2: aX2 c= Xm

      proof

        let x be object;

        assume x in aX2;

        then ex q be Point of ( TOP-REAL 2) st x = q & q in Xm & 0 >= (q `2 );

        hence thesis;

      end;

      

       A3: TOUCm is SubSpace of TOUCm by TSEP_1: 2;

      

       A4: (c1 `2 ) = 0 by EUCLID: 52;

      

       A5: c[10] is Point of ( Topen_unit_circle c[-10] ) by Lm15, Th23;

      then

       A6: c[10] in aX1 by A4;

      

       A7: c[10] in aX2 by A4, A5;

      then

      reconsider aX1, aX2 as non empty Subset of TOUCm by A1, A2, A6;

      set X1 = (TOUCm | aX1);

      let p be Point of ( Topen_unit_circle c[-10] ) such that

       A8: p = c[10] ;

      reconsider x1 = p as Point of X1 by A8, A6, PRE_TOPC: 8;

      set X2 = (TOUCm | aX2);

      reconsider x2 = p as Point of X2 by A8, A7, PRE_TOPC: 8;

      

       A9: the carrier of X2 = aX2 by PRE_TOPC: 8;

      Xm c= (aX1 \/ aX2)

      proof

        let a be object;

        assume

         A10: a in Xm;

        then

        reconsider a as Point of ( TOP-REAL 2) by Lm8;

         0 >= (a `2 ) or 0 <= (a `2 );

        then a in aX1 or a in aX2 by A10;

        hence thesis by XBOOLE_0:def 3;

      end;

      then

       A11: Xm = (aX1 \/ aX2);

      (Cm | X2) is continuous by Lm60;

      then

       A12: (Cm | X2) is_continuous_at x2;

      (Cm | X1) is continuous by Lm59;

      then

       A13: (Cm | X1) is_continuous_at x1;

      the carrier of X1 = aX1 by PRE_TOPC: 8;

      then TOUCm = (X1 union X2) by A9, A3, A11, TSEP_1:def 2;

      hence thesis by A13, A12, TMAP_1: 113;

    end;

    

     Lm62: Circle2IntervalL is continuous

    proof

      set h = (j (#) arccos );

      set K = [.( - 1), 1.];

      set J = [.p0, 0 .[;

      set I = ]. 0 , p1.];

      set Z = ( R^1 | ( R^1 ].(1 / 2), ((1 / 2) + p1).[));

      for p be Point of TOUCm holds Cm is_continuous_at p

      proof

        ( Tcircle (( 0. ( TOP-REAL 2)),1)) is SubSpace of TREC by Th10;

        then

         A1: TOUCm is SubSpace of TREC by TSEP_1: 7;

        let p be Point of TOUCm;

        

         A2: K = ( [#] CIT) by TOPMETR: 18;

        reconsider q = p as Point of ( TOP-REAL 2) by Lm8;

        

         A3: the carrier of Z = ].(1 / 2), ((1 / 2) + p1).[ by PRE_TOPC: 8;

        consider x,y be Real such that

         A4: p = |[x, y]| and

         A5: y >= 0 implies (Cm . p) = (1 + (( arccos x) / P2)) and

         A6: y <= 0 implies (Cm . p) = (1 - (( arccos x) / P2)) by Def14;

        

         A7: y = (q `2 ) by A4, EUCLID: 52;

        

         A8: x = (q `1 ) by A4, EUCLID: 52;

        then

         A9: x <= 1 by Th26;

        ( - 1) <= x by A8, Th26;

        then

         A10: x in K by A9, XXREAL_1: 1;

        

         A11: ( dom h) = ( dom arccos ) by VALUED_1:def 5;

        

        then

         A12: (h . x) = (( arccos . x) * j) by A10, SIN_COS6: 86, VALUED_1:def 5

        .= ((1 * ( arccos . x)) / P2) by XCMPLX_1: 74;

        per cases ;

          suppose y = 0 ;

          hence thesis by A7, Lm61, Th25;

        end;

          suppose

           A13: y < 0 ;

          for V be Subset of Z st V is open & (Cm . p) in V holds ex W be Subset of TOUCm st W is open & p in W & (Cm .: W) c= V

          proof

            set hh = (h1 - h);

            let V be Subset of Z such that

             A14: V is open and

             A15: (Cm . p) in V;

            reconsider V1 = V as Subset of REAL by A3, XBOOLE_1: 1;

            reconsider V2 = V1 as Subset of R^1 by TOPMETR: 17;

            V2 is open by A14, TSEP_1: 17;

            then

            reconsider V1 as open Subset of REAL by BORSUK_5: 39;

            consider N1 be Neighbourhood of (Cm . p) such that

             A16: N1 c= V1 by A15, RCOMP_1: 18;

            

             A17: ((hh | K) . x) = (hh . x) by A10, FUNCT_1: 49;

            ( dom hh) = (( dom h1) /\ ( dom h)) by VALUED_1: 12;

            

            then

             A18: ( dom hh) = ( REAL /\ ( dom h))

            .= K by A11, SIN_COS6: 86, XBOOLE_1: 28;

            then

             A19: ( dom (hh | K)) = K by RELAT_1: 62;

            

             A20: (Cm . p) = (1 - (( arccos . x) / P2)) by A6, A13, SIN_COS6:def 4;

            

             A21: p = ((1,2) --> (x,y)) by A4, TOPREALA: 28;

            x in ( dom (hh | K)) by A10, A18, RELAT_1: 57;

            then

             A22: (hh | K) is_continuous_in x by FCONT_1:def 2;

            (hh . x) = ((h1 . x) - (h . x)) by A10, A18, VALUED_1: 13

            .= (1 - ((1 * ( arccos . x)) / P2)) by A10, A12, FUNCOP_1: 7;

            then

            consider N be Neighbourhood of x such that

             A23: ((hh | K) .: N) c= N1 by A20, A17, A22, FCONT_1: 5;

            set N3 = (N /\ K);

            

             A24: N3 c= K by XBOOLE_1: 17;

            reconsider N3, J as Subset of CIT by Lm2, XBOOLE_1: 17, XXREAL_1: 35;

            set W = (( product ((1,2) --> (N3,J))) /\ Xm);

            reconsider W as Subset of TOUCm by XBOOLE_1: 17;

            take W;

            reconsider KK = ( product ((1,2) --> (N3,J))) as Subset of TREC by TOPREALA: 38;

            reconsider I3 = J as open Subset of CIT by TOPREALA: 26;

            

             A25: ((hh | K) .: N3) c= ((hh | K) .: N) by RELAT_1: 123, XBOOLE_1: 17;

            ( R^1 N) = N;

            then

            reconsider M3 = N3 as open Subset of CIT by A2, TOPS_2: 24;

            KK = ( product ((1,2) --> (M3,I3)));

            then KK is open by TOPREALA: 39;

            hence W is open by A1, Lm17, TOPS_2: 24;

            x in N by RCOMP_1: 16;

            then

             A26: x in N3 by A10, XBOOLE_0:def 4;

            y >= ( - 1) by A7, Th26;

            then y in J by A13, XXREAL_1: 3;

            then p in ( product ((1,2) --> (N3,J))) by A21, A26, HILBERT3: 11;

            hence p in W by XBOOLE_0:def 4;

            let m be object;

            assume m in (Cm .: W);

            then

            consider c be Element of TOUCm such that

             A27: c in W and

             A28: m = (Cm . c) by FUNCT_2: 65;

            

             A29: c in ( product ((1,2) --> (N3,J))) by A27, XBOOLE_0:def 4;

            then

             A30: (c . 1) in N3 by TOPREALA: 3;

            consider c1,c2 be Real such that

             A31: c = |[c1, c2]| and c2 >= 0 implies (Cm . c) = (1 + (( arccos c1) / P2)) and

             A32: c2 <= 0 implies (Cm . c) = (1 - (( arccos c1) / P2)) by Def14;

            (c . 2) in J by A29, TOPREALA: 3;

            then c2 in J by A31, TOPREALA: 29;

            then

             A33: (1 - ((1 * ( arccos c1)) * j)) = m by A28, A32, XCMPLX_1: 74, XXREAL_1: 3;

            ((hh | K) . (c . 1)) = (hh . (c . 1)) by A24, A30, FUNCT_1: 49

            .= ((h1 . (c . 1)) - (h . (c . 1))) by A18, A24, A30, VALUED_1: 13

            .= (1 - (h . (c . 1))) by A30, FUNCOP_1: 7

            .= (1 - (( arccos . (c . 1)) * j)) by A11, A24, A30, SIN_COS6: 86, VALUED_1:def 5

            .= (1 - (( arccos . c1) * j)) by A31, TOPREALA: 29

            .= (1 - (( arccos c1) * j)) by SIN_COS6:def 4;

            then m in ((hh | K) .: N3) by A24, A30, A19, A33, FUNCT_1:def 6;

            then m in ((hh | K) .: N) by A25;

            then m in N1 by A23;

            hence thesis by A16;

          end;

          hence thesis by TMAP_1: 43;

        end;

          suppose

           A34: y > 0 ;

          for V be Subset of Z st V is open & (Cm . p) in V holds ex W be Subset of TOUCm st W is open & p in W & (Cm .: W) c= V

          proof

            set hh = (h1 + h);

            let V be Subset of Z such that

             A35: V is open and

             A36: (Cm . p) in V;

            reconsider V1 = V as Subset of REAL by A3, XBOOLE_1: 1;

            reconsider V2 = V1 as Subset of R^1 by TOPMETR: 17;

            V2 is open by A35, TSEP_1: 17;

            then

            reconsider V1 as open Subset of REAL by BORSUK_5: 39;

            consider N1 be Neighbourhood of (Cm . p) such that

             A37: N1 c= V1 by A36, RCOMP_1: 18;

            

             A38: ((hh | K) . x) = (hh . x) by A10, FUNCT_1: 49;

            ( dom hh) = (( dom h1) /\ ( dom h)) by VALUED_1:def 1;

            

            then

             A39: ( dom hh) = ( REAL /\ ( dom h))

            .= K by A11, SIN_COS6: 86, XBOOLE_1: 28;

            then

             A40: ( dom (hh | K)) = K by RELAT_1: 62;

            

             A41: (Cm . p) = (1 + (( arccos . x) / P2)) by A5, A34, SIN_COS6:def 4;

            

             A42: p = ((1,2) --> (x,y)) by A4, TOPREALA: 28;

            x in ( dom (hh | K)) by A10, A39, RELAT_1: 57;

            then

             A43: (hh | K) is_continuous_in x by FCONT_1:def 2;

            (hh . x) = ((h1 . x) + (h . x)) by A10, A39, VALUED_1:def 1

            .= (1 + ((1 * ( arccos . x)) / P2)) by A10, A12, FUNCOP_1: 7;

            then

            consider N be Neighbourhood of x such that

             A44: ((hh | K) .: N) c= N1 by A41, A38, A43, FCONT_1: 5;

            set N3 = (N /\ K);

            

             A45: N3 c= K by XBOOLE_1: 17;

            reconsider N3, I as Subset of CIT by Lm2, XBOOLE_1: 17, XXREAL_1: 36;

            set W = (( product ((1,2) --> (N3,I))) /\ Xm);

            reconsider W as Subset of TOUCm by XBOOLE_1: 17;

            take W;

            reconsider KK = ( product ((1,2) --> (N3,I))) as Subset of TREC by TOPREALA: 38;

            reconsider I3 = I as open Subset of CIT by TOPREALA: 25;

            

             A46: ((hh | K) .: N3) c= ((hh | K) .: N) by RELAT_1: 123, XBOOLE_1: 17;

            ( R^1 N) = N;

            then

            reconsider M3 = N3 as open Subset of CIT by A2, TOPS_2: 24;

            KK = ( product ((1,2) --> (M3,I3)));

            then KK is open by TOPREALA: 39;

            hence W is open by A1, Lm17, TOPS_2: 24;

            x in N by RCOMP_1: 16;

            then

             A47: x in N3 by A10, XBOOLE_0:def 4;

            y <= 1 by A7, Th26;

            then y in I by A34, XXREAL_1: 2;

            then p in ( product ((1,2) --> (N3,I))) by A42, A47, HILBERT3: 11;

            hence p in W by XBOOLE_0:def 4;

            let m be object;

            assume m in (Cm .: W);

            then

            consider c be Element of TOUCm such that

             A48: c in W and

             A49: m = (Cm . c) by FUNCT_2: 65;

            

             A50: c in ( product ((1,2) --> (N3,I))) by A48, XBOOLE_0:def 4;

            then

             A51: (c . 1) in N3 by TOPREALA: 3;

            consider c1,c2 be Real such that

             A52: c = |[c1, c2]| and

             A53: c2 >= 0 implies (Cm . c) = (1 + (( arccos c1) / P2)) and c2 <= 0 implies (Cm . c) = (1 - (( arccos c1) / P2)) by Def14;

            (c . 2) in I by A50, TOPREALA: 3;

            then c2 in I by A52, TOPREALA: 29;

            then

             A54: (1 + ((1 * ( arccos c1)) * j)) = m by A49, A53, XCMPLX_1: 74, XXREAL_1: 2;

            ((hh | K) . (c . 1)) = (hh . (c . 1)) by A45, A51, FUNCT_1: 49

            .= ((h1 . (c . 1)) + (h . (c . 1))) by A39, A45, A51, VALUED_1:def 1

            .= (1 + (h . (c . 1))) by A51, FUNCOP_1: 7

            .= (1 + (( arccos . (c . 1)) * j)) by A11, A45, A51, SIN_COS6: 86, VALUED_1:def 5

            .= (1 + (( arccos . c1) * j)) by A52, TOPREALA: 29

            .= (1 + (( arccos c1) * j)) by SIN_COS6:def 4;

            then m in ((hh | K) .: N3) by A45, A51, A40, A54, FUNCT_1:def 6;

            then m in ((hh | K) .: N) by A46;

            then m in N1 by A44;

            hence thesis by A37;

          end;

          hence thesis by TMAP_1: 43;

        end;

      end;

      hence thesis by TMAP_1: 44;

    end;

    registration

      cluster Circle2IntervalR -> one-to-one onto continuous;

      coherence by Lm45, Th42, GRCAT_1: 41;

      cluster Circle2IntervalL -> one-to-one onto continuous;

      coherence by Lm62, Th43, GRCAT_1: 41;

    end

    

     Lm63: ( CircleMap ( R^1 0 )) is open

    proof

      ( CircleMap . ( R^1 0 )) = c[10] by Th32;

      hence thesis by Th42, TOPREALA: 14;

    end;

    

     Lm64: ( CircleMap ( R^1 (1 / 2))) is open by Lm19, Th43, TOPREALA: 14;

    registration

      let i be Integer;

      cluster ( CircleMap ( R^1 i)) -> open;

      coherence

      proof

        set F = ( AffineMap (1,( - i)));

        set f = (F | ].( 0 + i), (( 0 + i) + p1).[);

        

         A1: the carrier of ( R^1 | ( R^1 ]. 0 , 1.[)) = ( R^1 ]. 0 , 1.[) by PRE_TOPC: 8;

        ( dom F) = REAL by FUNCT_2:def 1;

        then

         A2: ( dom f) = ].i, (i + 1).[ by RELAT_1: 62;

        

         A3: ( rng f) = ]. 0 , ( 0 + 1).[ by Lm24;

        the carrier of ( R^1 | ( R^1 ].i, (i + 1).[)) = ( R^1 ].i, (i + 1).[) by PRE_TOPC: 8;

        then

        reconsider f as Function of ( R^1 | ( R^1 ].i, (i + p1).[)), ( R^1 | ( R^1 ]. 0 , ( 0 + p1).[)) by A1, A2, A3, FUNCT_2: 2;

        

         A4: ( CircleMap ( R^1 ( 0 + i))) = (( CircleMap ( R^1 0 )) * f) by Th41;

        

         A5: ( R^1 | ( R^1 ( rng F))) = R^1 by Lm12;

        

         A6: ( CircleMap . ( R^1 i)) = c[10] by Th32

        .= ( CircleMap . ( R^1 0 )) by Th32;

        

         A7: ( R^1 | ( R^1 ( dom F))) = R^1 by Lm12;

        

         A8: ( R^1 F) = F;

        f is onto by A1, A3;

        then f is open by A7, A5, A8, TOPREALA: 10;

        hence thesis by A4, A6, Lm63, TOPREALA: 11;

      end;

      cluster ( CircleMap ( R^1 ((1 / 2) + i))) -> open;

      coherence

      proof

        ((1 / 2) - 1) < 0 ;

        then [\(1 / 2)/] = 0 by INT_1:def 6;

        then

         A9: ((1 / 2) - [\(1 / 2)/]) = (1 / 2);

        ( frac ((1 / 2) + i)) = ( frac (1 / 2)) by INT_1: 66

        .= (1 / 2) by A9, INT_1:def 8;

        then

         A10: ( CircleMap . ( R^1 ((1 / 2) + i))) = ( CircleMap . ( R^1 ((1 / 2) + 0 ))) by Lm19, Th34;

        set F = ( AffineMap (1,( - i)));

        set f = (F | ].((1 / 2) + i), (((1 / 2) + i) + p1).[);

        

         A11: the carrier of ( R^1 | ( R^1 ].(1 / 2), (3 / 2).[)) = ( R^1 ].(1 / 2), (3 / 2).[) by PRE_TOPC: 8;

        ( dom F) = REAL by FUNCT_2:def 1;

        then

         A12: ( dom f) = ].((1 / 2) + i), (((1 / 2) + i) + 1).[ by RELAT_1: 62;

        

         A13: ( rng f) = ].(1 / 2), ((1 / 2) + 1).[ by Lm24;

        the carrier of ( R^1 | ( R^1 ].((1 / 2) + i), (((1 / 2) + i) + 1).[)) = ( R^1 ].((1 / 2) + i), (((1 / 2) + i) + 1).[) by PRE_TOPC: 8;

        then

        reconsider f as Function of ( R^1 | ( R^1 ].((1 / 2) + i), (((1 / 2) + i) + p1).[)), ( R^1 | ( R^1 ].(1 / 2), ((1 / 2) + p1).[)) by A11, A12, A13, FUNCT_2: 2;

        

         A14: ( CircleMap ( R^1 ((1 / 2) + i))) = (( CircleMap ( R^1 (1 / 2))) * f) by Th41;

        

         A15: ( R^1 | ( R^1 ( rng F))) = R^1 by Lm12;

        

         A16: ( R^1 | ( R^1 ( dom F))) = R^1 by Lm12;

        

         A17: ( R^1 F) = F;

        f is onto by A11, A13;

        then f is open by A16, A15, A17, TOPREALA: 10;

        hence thesis by A14, A10, Lm64, TOPREALA: 11;

      end;

    end

    registration

      cluster Circle2IntervalR -> open;

      coherence

      proof

        ( CircleMap . ( R^1 0 )) = c[10] by Th32;

        hence thesis by Th42, TOPREALA: 13;

      end;

      cluster Circle2IntervalL -> open;

      coherence by Lm19, Th43, TOPREALA: 13;

    end

    theorem :: TOPREALB:44

    ( CircleMap ( R^1 (1 / 2))) is being_homeomorphism

    proof

      reconsider r = 0 as Integer;

      ( CircleMap ( R^1 ((1 / 2) + r))) is open;

      hence thesis by TOPREALA: 16;

    end;

    theorem :: TOPREALB:45

    ex F be Subset-Family of ( Tunit_circle 2) st F = {( CircleMap .: ]. 0 , 1.[), ( CircleMap .: ].(1 / 2), (3 / 2).[)} & F is Cover of ( Tunit_circle 2) & F is open & for U be Subset of ( Tunit_circle 2) holds (U = ( CircleMap .: ]. 0 , 1.[) implies ( union ( IntIntervals ( 0 ,1))) = ( CircleMap " U) & for d be Subset of R^1 st d in ( IntIntervals ( 0 ,1)) holds for f be Function of ( R^1 | d), (( Tunit_circle 2) | U) st f = ( CircleMap | d) holds f is being_homeomorphism) & (U = ( CircleMap .: ].(1 / 2), (3 / 2).[) implies ( union ( IntIntervals ((1 / 2),(3 / 2)))) = ( CircleMap " U) & for d be Subset of R^1 st d in ( IntIntervals ((1 / 2),(3 / 2))) holds for f be Function of ( R^1 | d), (( Tunit_circle 2) | U) st f = ( CircleMap | d) holds f is being_homeomorphism)

    proof

      set D2 = ( IntIntervals ((1 / 2),(3 / 2)));

      set D1 = ( IntIntervals ( 0 ,1));

      set F1 = ( CircleMap .: ( union D1));

      set F2 = ( CircleMap .: ( union D2));

      set F = {F1, F2};

      reconsider F as Subset-Family of TUC;

      take F;

       ].((1 / 2) + 0 ), ((3 / 2) + 0 ).[ in D2 by Lm1;

      then

       A1: F2 = ( CircleMap .: ].(1 / 2), (3 / 2).[) by Th40;

      

       A2: ].( 0 + 0 ), (1 + 0 ).[ in D1 by Lm1;

      hence F = {( CircleMap .: ]. 0 , 1.[), ( CircleMap .: ].(1 / 2), (3 / 2).[)} by A1, Th40;

      thus F is Cover of TUC

      proof

        reconsider A = [. 0 , ( 0 + 1).[ as Subset of R^1 by TOPMETR: 17;

        reconsider f = ( CircleMap | A) as Function of ( R^1 | A), TUC by Lm21;

        let a be object;

        

         A3: F2 in F by TARSKI:def 2;

        f is onto by Th38;

        then

         A4: ( rng f) = cS1;

        assume a in the carrier of TUC;

        then

        consider x be object such that

         A5: x in ( dom f) and

         A6: (f . x) = a by A4, FUNCT_1:def 3;

        

         A7: ( dom f) = A by Lm18, RELAT_1: 62;

        then

        reconsider x as Element of REAL by A5;

        

         A8: ( CircleMap . x) = (f . x) by A5, FUNCT_1: 47;

        per cases by A5, A7, XXREAL_1: 3;

          suppose

           A9: x = 0 ;

           0 in A by XXREAL_1: 3;

          

          then

           A10: (f . 0 ) = ( CircleMap . 0 ) by FUNCT_1: 49

          .= c[10] by Th32

          .= ( CircleMap . 1) by Th32;

          1 in ].(1 / 2), (3 / 2).[ by XXREAL_1: 4;

          then a in ( CircleMap .: ].(1 / 2), (3 / 2).[) by A6, A9, A10, Lm18, FUNCT_1:def 6;

          hence a in ( union F) by A1, A3, TARSKI:def 4;

        end;

          suppose

           A11: 0 < x & x < 1;

          

           A12: ].( 0 + 0 ), (1 + 0 ).[ in D1 by Lm1;

          x in ]. 0 , 1.[ by A11, XXREAL_1: 4;

          then x in ( union D1) by A12, TARSKI:def 4;

          then

           A13: a in F1 by A6, A8, Lm18, FUNCT_1:def 6;

          F1 in F by TARSKI:def 2;

          hence a in ( union F) by A13, TARSKI:def 4;

        end;

          suppose x >= 1 & x < 1;

          hence a in ( union F);

        end;

      end;

      

       A14: F1 = ( CircleMap .: ]. 0 , 1.[) by A2, Th40;

      thus F is open

      proof

        reconsider r = 0 as Integer;

         A15:

        now

          let A be Subset of REAL ;

          A c= A;

          hence A is Subset of ( R^1 | ( R^1 A)) by PRE_TOPC: 8;

        end;

        then

        reconsider M = ]. 0 , 1.[ as Subset of ( R^1 | ( R^1 ].r, (r + 1).[));

        reconsider N = ].(1 / 2), (3 / 2).[ as Subset of ( R^1 | ( R^1 ].((1 / 2) + r), (((1 / 2) + r) + 1).[)) by A15;

        let P be Subset of TUC;

         A16:

        now

          let A be open Subset of REAL ;

          reconsider B = A as Subset of ( R^1 | ( R^1 A)) by A15;

          the carrier of ( R^1 | ( R^1 A)) = A by PRE_TOPC: 8;

          then B = (( [#] ( R^1 | ( R^1 A))) /\ ( R^1 A));

          hence A is open Subset of ( R^1 | ( R^1 A)) by TOPS_2: 24;

        end;

        then M is open;

        then

         A17: (( CircleMap ( R^1 r)) .: M) is open by T_0TOPSP:def 2;

        N is open by A16;

        then

         A18: (( CircleMap ( R^1 ((1 / 2) + r))) .: N) is open by T_0TOPSP:def 2;

        ( CircleMap .: ].(1 / 2), (3 / 2).[) = (( CircleMap ( R^1 (1 / 2))) .: ].(1 / 2), (3 / 2).[) by RELAT_1: 129;

        then

         A19: F2 is open by A1, A18, TSEP_1: 17;

        ( CircleMap .: ]. 0 , 1.[) = (( CircleMap ( R^1 0 )) .: ]. 0 , 1.[) by RELAT_1: 129;

        then F1 is open by A14, A17, TSEP_1: 17;

        hence thesis by A19, TARSKI:def 2;

      end;

      let U be Subset of TUC;

      

       A20: c[10] in { c[10] } by TARSKI:def 1;

      thus U = ( CircleMap .: ]. 0 , 1.[) implies ( union ( IntIntervals ( 0 ,1))) = ( CircleMap " U) & for d be Subset of R^1 st d in ( IntIntervals ( 0 ,1)) holds for f be Function of ( R^1 | d), (( Tunit_circle 2) | U) st f = ( CircleMap | d) holds f is being_homeomorphism

      proof

        assume

         A21: U = ( CircleMap .: ]. 0 , 1.[);

        then

        reconsider U1 = U as non empty Subset of TUC by Lm18;

        

         A22: ( [#] (TUC | U)) = U by PRE_TOPC:def 5;

         ].( 0 + 0 ), (1 + 0 ).[ in D1 by Lm1;

        then

         A23: ( CircleMap .: ]. 0 , 1.[) = ( CircleMap .: ( union D1)) by Th40;

        now

          let x1,x2 be Element of R^1 ;

          set k = [\x2/];

          set K = ].( 0 + k), (1 + k).[;

          assume x1 in ( union D1);

          then

          consider Z be set such that

           A24: x1 in Z and

           A25: Z in D1 by TARSKI:def 4;

          consider n be Element of INT such that

           A26: Z = ].( 0 + n), (1 + n).[ by A25;

          x1 < (1 + n) by A24, A26, XXREAL_1: 4;

          then

           A27: (x1 - 1) < ((1 + n) - 1) by XREAL_1: 9;

          then ((x1 - 1) - n) < (n - n) by XREAL_1: 9;

          then (((x1 - n) - 1) + 1) < ( 0 + 1) by XREAL_1: 8;

          then

           A28: ((2 * PI ) * (x1 - n)) < ((2 * PI ) * 1) by XREAL_1: 68;

          

           A29: ( CircleMap . (x2 - k)) = |[( cos ((2 * PI ) * (x2 - k))), ( sin ((2 * PI ) * (x2 - k)))]| by Def11;

          (x2 - 1) < k by INT_1:def 6;

          then ((x2 - 1) - k) < (k - k) by XREAL_1: 9;

          then (((x2 - 1) - k) + 1) < ( 0 + 1) by XREAL_1: 6;

          then

           A30: ((2 * PI ) * (x2 - k)) < ((2 * PI ) * 1) by XREAL_1: 68;

          assume

           A31: ( CircleMap . x1) = ( CircleMap . x2);

          

           A32: n < x1 by A24, A26, XXREAL_1: 4;

          then

           A33: 0 < (x1 - n) by XREAL_1: 50;

          k in INT by INT_1:def 2;

          then

           A34: K in D1;

          

           A35: ( CircleMap . x2) = ( CircleMap . (x2 + ( - k))) by Th31;

           [\x1/] = n by A32, A27, INT_1:def 6;

          then

           A36: not x1 in INT by A32, INT_1: 26;

           A37:

          now

            assume k = x2;

            then ( CircleMap . x1) = c[10] by A31, Th32;

            hence contradiction by A20, A36, Lm18, Th33, FUNCT_1:def 7, TOPMETR: 17;

          end;

          

           A38: ( CircleMap . (x1 - n)) = |[( cos ((2 * PI ) * (x1 - n))), ( sin ((2 * PI ) * (x1 - n)))]| by Def11;

          

           A39: ( CircleMap . x1) = ( CircleMap . (x1 + ( - n))) by Th31;

          then

           A40: ( cos ((2 * PI ) * (x1 - n))) = ( cos ((2 * PI ) * (x2 - k))) by A31, A35, A38, A29, SPPOL_2: 1;

          

           A41: ( sin ((2 * PI ) * (x1 - n))) = ( sin ((2 * PI ) * (x2 - k))) by A31, A39, A35, A38, A29, SPPOL_2: 1;

          k <= x2 by INT_1:def 6;

          then

           A42: k < x2 by A37, XXREAL_0: 1;

          then 0 <= (x2 - k) by XREAL_1: 50;

          then ((2 * PI ) * (x1 - n)) = ((2 * PI ) * (x2 - k)) by A33, A28, A30, A40, A41, COMPLEX2: 11;

          then (x1 - n) = (x2 - k) by XCMPLX_1: 5;

          then

           A43: x2 = ((x1 - n) + k);

          x1 < (1 + n) by A24, A26, XXREAL_1: 4;

          then (x1 - n) < 1 by XREAL_1: 19;

          then x2 < (1 + k) by A43, XREAL_1: 6;

          then x2 in K by A42, XXREAL_1: 4;

          hence x2 in ( union D1) by A34, TARSKI:def 4;

        end;

        hence ( union D1) = ( CircleMap " U) by A21, A23, T_0TOPSP: 1;

        let d be Subset of R^1 ;

        assume

         A44: d in D1;

        then

        consider n be Element of INT such that

         A45: d = ].( 0 + n), (1 + n).[;

        reconsider d1 = d as non empty Subset of R^1 by A45;

        reconsider J = ].n, (n + p1).[ as non empty Subset of R^1 by TOPMETR: 17;

        

         A46: ( CircleMap | d) = (( CircleMap | J) | d1) by A45, RELAT_1: 74;

        let f be Function of ( R^1 | d), (TUC | U);

        reconsider f1 = f as Function of ( R^1 | d1), (TUC | U1);

        assume

         A47: f = ( CircleMap | d);

        then

         A48: f is continuous by TOPREALA: 8;

        d c= J by A45;

        then

        reconsider d2 = d as Subset of ( R^1 | J) by PRE_TOPC: 8;

        

         A49: (( R^1 | J) | d2) = ( R^1 | d) by A45, PRE_TOPC: 7;

        reconsider F = ( CircleMap | J) as Function of ( R^1 | J), TUC by Lm21;

        ( CircleMap ( R^1 n)) is open;

        then

         A50: F is open by TOPREALA: 12;

        

         A51: F1 = ( CircleMap .: d) by A44, Th40;

        

         A52: f1 is onto

        proof

          thus ( rng f1) c= the carrier of (TUC | U1);

          let b be object;

          

           A53: ( dom ( CircleMap | d)) = d by Lm18, RELAT_1: 62, TOPMETR: 17;

          assume b in the carrier of (TUC | U1);

          then

          consider a be Element of R^1 such that

           A54: a in d and

           A55: b = ( CircleMap . a) by A21, A23, A22, A51, FUNCT_2: 65;

          (( CircleMap | d) . a) = ( CircleMap . a) by A54, FUNCT_1: 49;

          hence thesis by A47, A54, A55, A53, FUNCT_1:def 3;

        end;

        f is one-to-one by A44, A47, Lm3, Th39;

        hence thesis by A47, A48, A49, A46, A52, A50, TOPREALA: 10, TOPREALA: 16;

      end;

      assume

       A56: U = ( CircleMap .: ].(1 / 2), (3 / 2).[);

      then

      reconsider U1 = U as non empty Subset of TUC by Lm18;

      now

        let x1,x2 be Element of R^1 ;

        set k = [\x2/];

        

         A57: k <= x2 by INT_1:def 6;

        assume x1 in ( union D2);

        then

        consider Z be set such that

         A58: x1 in Z and

         A59: Z in D2 by TARSKI:def 4;

        consider n be Element of INT such that

         A60: Z = ].((1 / 2) + n), ((3 / 2) + n).[ by A59;

        

         A61: ((1 / 2) + n) < x1 by A58, A60, XXREAL_1: 4;

        ( 0 + n) < ((1 / 2) + n) by XREAL_1: 8;

        then

         A62: n < x1 by A61, XXREAL_0: 2;

        assume

         A63: ( CircleMap . x1) = ( CircleMap . x2);

        

         A64: x1 < ((3 / 2) + n) by A58, A60, XXREAL_1: 4;

        then

         A65: (x1 - n) < (3 / 2) by XREAL_1: 19;

        per cases by XXREAL_0: 1;

          suppose x1 = (1 + n);

          then ( CircleMap . x2) = c[10] by A63, Th32;

          then

          reconsider w = x2 as Element of INT by A20, Lm18, Th33, FUNCT_1:def 7, TOPMETR: 17;

          

           A66: ( 0 + w) < ((1 / 2) + w) by XREAL_1: 8;

          (w - 1) in INT by INT_1:def 2;

          then

           A67: ].((1 / 2) + (w - 1)), ((3 / 2) + (w - 1)).[ in D2;

          (( - (1 / 2)) + w) < ( 0 + w) by XREAL_1: 8;

          then x2 in ].((1 / 2) + (w - 1)), ((3 / 2) + (w - 1)).[ by A66, XXREAL_1: 4;

          hence x2 in ( union D2) by A67, TARSKI:def 4;

        end;

          suppose x1 < (1 + n);

          then (x1 - 1) < ((n + 1) - 1) by XREAL_1: 9;

          then ((x1 - 1) - n) < (n - n) by XREAL_1: 9;

          then (((x1 - n) - 1) + 1) < ( 0 + 1) by XREAL_1: 8;

          then

           A68: ((2 * PI ) * (x1 - n)) < ((2 * PI ) * 1) by XREAL_1: 68;

          set K = ].((1 / 2) + k), ((3 / 2) + k).[;

          k in INT by INT_1:def 2;

          then

           A69: K in D2;

          

           A70: (x2 - x2) <= (x2 - k) by A57, XREAL_1: 13;

          

           A71: 0 < (x1 - n) by A62, XREAL_1: 50;

          

           A72: ( CircleMap . (x2 - k)) = |[( cos ((2 * PI ) * (x2 - k))), ( sin ((2 * PI ) * (x2 - k)))]| by Def11;

          (x2 - 1) < k by INT_1:def 6;

          then ((x2 - 1) - k) < (k - k) by XREAL_1: 9;

          then (((x2 - 1) - k) + 1) < ( 0 + 1) by XREAL_1: 6;

          then

           A73: ((2 * PI ) * (x2 - k)) < ((2 * PI ) * 1) by XREAL_1: 68;

          

           A74: ( CircleMap . x2) = ( CircleMap . (x2 + ( - k))) by Th31;

          (((1 / 2) + n) - n) < (x1 - n) by A61, XREAL_1: 9;

          then

           A75: ((1 / 2) + k) < ((x1 - n) + k) by XREAL_1: 8;

          

           A76: ( CircleMap . (x1 - n)) = |[( cos ((2 * PI ) * (x1 - n))), ( sin ((2 * PI ) * (x1 - n)))]| by Def11;

          

           A77: ( CircleMap . x1) = ( CircleMap . (x1 + ( - n))) by Th31;

          then

           A78: ( sin ((2 * PI ) * (x1 - n))) = ( sin ((2 * PI ) * (x2 - k))) by A63, A74, A76, A72, SPPOL_2: 1;

          ( cos ((2 * PI ) * (x1 - n))) = ( cos ((2 * PI ) * (x2 - k))) by A63, A77, A74, A76, A72, SPPOL_2: 1;

          then ((2 * PI ) * (x1 - n)) = ((2 * PI ) * (x2 - k)) by A78, A71, A68, A70, A73, COMPLEX2: 11;

          then

           A79: (x1 - n) = (x2 - k) by XCMPLX_1: 5;

          then x2 = ((x1 - n) + k);

          then x2 < ((3 / 2) + k) by A65, XREAL_1: 6;

          then x2 in K by A79, A75, XXREAL_1: 4;

          hence x2 in ( union D2) by A69, TARSKI:def 4;

        end;

          suppose x1 > (1 + n);

          then

           A80: ((n + 1) - 1) < (x1 - 1) by XREAL_1: 9;

          then

           A81: (n - n) < ((x1 - 1) - n) by XREAL_1: 9;

          set K = ].((1 / 2) + (k - 1)), ((3 / 2) + (k - 1)).[;

          

           A82: ( - (1 / 2)) < 0 ;

          (n - n) < ((x1 - 1) - n) by A80, XREAL_1: 9;

          then

           A83: (( - (1 / 2)) + k) < (((x1 - 1) - n) + k) by A82, XREAL_1: 8;

          (k - 1) in INT by INT_1:def 2;

          then

           A84: K in D2;

          

           A85: ((x1 - n) - 1) < ((3 / 2) - 1) by A65, XREAL_1: 9;

          

           A86: (x2 - x2) <= (x2 - k) by A57, XREAL_1: 13;

          

           A87: ( CircleMap . (x2 - k)) = |[( cos ((2 * PI ) * (x2 - k))), ( sin ((2 * PI ) * (x2 - k)))]| by Def11;

          (x1 - 1) < (((3 / 2) + n) - 1) by A64, XREAL_1: 9;

          then ((x1 - 1) - n) < (((1 / 2) + n) - n) by XREAL_1: 9;

          then ((x1 - 1) - n) < 1 by XXREAL_0: 2;

          then

           A88: ((2 * PI ) * ((x1 - 1) - n)) < ((2 * PI ) * 1) by XREAL_1: 68;

          

           A89: ( CircleMap . x2) = ( CircleMap . (x2 + ( - k))) by Th31;

          (x2 - 1) < k by INT_1:def 6;

          then ((x2 - 1) - k) < (k - k) by XREAL_1: 9;

          then (((x2 - 1) - k) + 1) < ( 0 + 1) by XREAL_1: 6;

          then

           A90: ((2 * PI ) * (x2 - k)) < ((2 * PI ) * 1) by XREAL_1: 68;

          

           A91: ( CircleMap . ((x1 - 1) - n)) = |[( cos ((2 * PI ) * ((x1 - 1) - n))), ( sin ((2 * PI ) * ((x1 - 1) - n)))]| by Def11;

          

           A92: ( CircleMap . x1) = ( CircleMap . (x1 + (( - 1) - n))) by Th31;

          then

           A93: ( sin ((2 * PI ) * ((x1 - 1) - n))) = ( sin ((2 * PI ) * (x2 - k))) by A63, A89, A91, A87, SPPOL_2: 1;

          ( cos ((2 * PI ) * ((x1 - 1) - n))) = ( cos ((2 * PI ) * (x2 - k))) by A63, A92, A89, A91, A87, SPPOL_2: 1;

          then ((2 * PI ) * ((x1 - 1) - n)) = ((2 * PI ) * (x2 - k)) by A93, A81, A88, A86, A90, COMPLEX2: 11;

          then

           A94: ((x1 - 1) - n) = (x2 - k) by XCMPLX_1: 5;

          then x2 = (((x1 - 1) - n) + k);

          then x2 < ((1 / 2) + k) by A85, XREAL_1: 6;

          then x2 in K by A94, A83, XXREAL_1: 4;

          hence x2 in ( union D2) by A84, TARSKI:def 4;

        end;

      end;

      hence ( union D2) = ( CircleMap " U) by A1, A56, T_0TOPSP: 1;

      let d be Subset of R^1 ;

      assume

       A95: d in D2;

      then

      consider n be Element of INT such that

       A96: d = ].((1 / 2) + n), ((3 / 2) + n).[;

      

       A97: (1 + n) < ((3 / 2) + n) by XREAL_1: 6;

      ((1 / 2) + n) < (1 + n) by XREAL_1: 6;

      then

      reconsider d1 = d as non empty Subset of R^1 by A96, A97, XXREAL_1: 4;

      

       A98: ( [#] (TUC | U)) = U by PRE_TOPC:def 5;

      let f be Function of ( R^1 | d), (TUC | U);

      reconsider f1 = f as Function of ( R^1 | d1), (TUC | U1);

      assume

       A99: f = ( CircleMap | d);

      then

       A100: f is continuous by TOPREALA: 8;

      reconsider J = ].((1 / 2) + n), (((1 / 2) + n) + p1).[ as non empty Subset of R^1 by TOPMETR: 17;

      

       A101: ( CircleMap | d) = (( CircleMap | J) | d1) by A96, RELAT_1: 74;

      d c= J by A96;

      then

      reconsider d2 = d as Subset of ( R^1 | J) by PRE_TOPC: 8;

      

       A102: (( R^1 | J) | d2) = ( R^1 | d) by A96, PRE_TOPC: 7;

      

       A103: F2 = ( CircleMap .: d) by A95, Th40;

      

       A104: f1 is onto

      proof

        thus ( rng f1) c= the carrier of (TUC | U1);

        let b be object;

        

         A105: ( dom ( CircleMap | d)) = d by Lm18, RELAT_1: 62, TOPMETR: 17;

        assume b in the carrier of (TUC | U1);

        then

        consider a be Element of R^1 such that

         A106: a in d and

         A107: b = ( CircleMap . a) by A1, A56, A98, A103, FUNCT_2: 65;

        (( CircleMap | d) . a) = ( CircleMap . a) by A106, FUNCT_1: 49;

        hence thesis by A99, A106, A107, A105, FUNCT_1:def 3;

      end;

      reconsider F = ( CircleMap | J) as Function of ( R^1 | J), TUC by Lm21;

      ( CircleMap ( R^1 ((1 / 2) + n))) is open;

      then

       A108: F is open by TOPREALA: 12;

      f is one-to-one by A95, A99, Lm4, Th39;

      hence thesis by A99, A100, A102, A101, A104, A108, TOPREALA: 10, TOPREALA: 16;

    end;