topalg_5.miz



    begin

    set o = |[ 0 , 0 ]|;

    set I = the carrier of I[01] ;

    set R = the carrier of R^1 ;

    

     Lm1: 0 in INT by INT_1:def 1;

    

     Lm2: 0 in I by BORSUK_1: 43;

    then

     Lm3: { 0 } c= I by ZFMISC_1: 31;

    

     Lm4: 0 in { 0 } by TARSKI:def 1;

    

     Lm5: the carrier of [: I[01] , I[01] :] = [:I, I:] by BORSUK_1:def 2;

    reconsider j0 = 0 , j1 = 1 as Point of I[01] by BORSUK_1:def 14, BORSUK_1:def 15;

    

     Lm6: ( [#] I[01] ) = I;

    

     Lm7: ( I[01] | ( [#] I[01] )) = I[01] by TSEP_1: 3;

    

     Lm8: (1 - 0 ) <= 1;

    

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

    registration

      cluster INT.Group -> infinite;

      coherence ;

    end

    reserve a,r,s for Real;

    theorem :: TOPALG_5:1

    

     Th1: r <= s implies for p be Point of ( Closed-Interval-MSpace (r,s)) holds ( Ball (p,a)) = [.r, s.] or ( Ball (p,a)) = [.r, (p + a).[ or ( Ball (p,a)) = ].(p - a), s.] or ( Ball (p,a)) = ].(p - a), (p + a).[

    proof

      set M = ( Closed-Interval-MSpace (r,s));

      assume r <= s;

      then

       A1: the carrier of M = [.r, s.] by TOPMETR: 10;

      let p be Point of M;

      set B = ( Ball (p,a));

      reconsider p1 = p as Point of RealSpace by TOPMETR: 8;

      set B1 = ( Ball (p1,a));

      

       A2: B = (B1 /\ the carrier of M) by TOPMETR: 9;

      

       A3: B1 = ].(p1 - a), (p1 + a).[ by FRECHET: 7;

      per cases ;

        suppose that

         A4: (p1 + a) <= s and

         A5: (p1 - a) < r;

        B = [.r, (p1 + a).[

        proof

          thus B c= [.r, (p1 + a).[

          proof

            let b be object;

            assume

             A6: b in B;

            then

            reconsider b as Element of B;

            b in B1 by A2, A6, XBOOLE_0:def 4;

            then

             A7: b < (p1 + a) by A3, XXREAL_1: 4;

            r <= b by A1, A6, XXREAL_1: 1;

            hence thesis by A7, XXREAL_1: 3;

          end;

          let b be object;

          assume

           A8: b in [.r, (p1 + a).[;

          then

          reconsider b as Real;

          

           A9: r <= b by A8, XXREAL_1: 3;

          

           A10: b < (p1 + a) by A8, XXREAL_1: 3;

          then b <= s by A4, XXREAL_0: 2;

          then

           A11: b in [.r, s.] by A9, XXREAL_1: 1;

          (p1 - a) < b by A5, A9, XXREAL_0: 2;

          then b in B1 by A3, A10, XXREAL_1: 4;

          hence thesis by A1, A2, A11, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

        suppose that

         A12: (p1 + a) <= s and

         A13: (p1 - a) >= r;

        B = ].(p1 - a), (p1 + a).[

        proof

          thus B c= ].(p1 - a), (p1 + a).[ by A2, A3, XBOOLE_1: 17;

          let b be object;

          assume

           A14: b in ].(p1 - a), (p1 + a).[;

          then

          reconsider b as Real;

          b < (p1 + a) by A14, XXREAL_1: 4;

          then

           A15: b <= s by A12, XXREAL_0: 2;

          (p1 - a) <= b by A14, XXREAL_1: 4;

          then r <= b by A13, XXREAL_0: 2;

          then b in [.r, s.] by A15, XXREAL_1: 1;

          hence thesis by A1, A2, A3, A14, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

        suppose that

         A16: (p1 + a) > s and

         A17: (p1 - a) < r;

        B = [.r, s.]

        proof

          thus B c= [.r, s.] by A1;

          let b be object;

          assume

           A18: b in [.r, s.];

          then

          reconsider b as Real;

          b <= s by A18, XXREAL_1: 1;

          then

           A19: b < (p1 + a) by A16, XXREAL_0: 2;

          r <= b by A18, XXREAL_1: 1;

          then (p1 - a) < b by A17, XXREAL_0: 2;

          then b in B1 by A3, A19, XXREAL_1: 4;

          hence thesis by A1, A2, A18, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

        suppose that

         A20: (p1 + a) > s and

         A21: (p1 - a) >= r;

        B = ].(p1 - a), s.]

        proof

          thus B c= ].(p1 - a), s.]

          proof

            let b be object;

            assume

             A22: b in B;

            then

            reconsider b as Element of B;

            b in B1 by A2, A22, XBOOLE_0:def 4;

            then

             A23: (p1 - a) < b by A3, XXREAL_1: 4;

            b <= s by A1, A22, XXREAL_1: 1;

            hence thesis by A23, XXREAL_1: 2;

          end;

          let b be object;

          assume

           A24: b in ].(p1 - a), s.];

          then

          reconsider b as Real;

          

           A25: b <= s by A24, XXREAL_1: 2;

          

           A26: (p1 - a) < b by A24, XXREAL_1: 2;

          then r <= b by A21, XXREAL_0: 2;

          then

           A27: b in [.r, s.] by A25, XXREAL_1: 1;

          b < (p1 + a) by A20, A25, XXREAL_0: 2;

          then b in B1 by A3, A26, XXREAL_1: 4;

          hence thesis by A1, A2, A27, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

    end;

    theorem :: TOPALG_5:2

    

     Th2: r <= s implies ex B be Basis of ( Closed-Interval-TSpace (r,s)) st (ex f be ManySortedSet of ( Closed-Interval-TSpace (r,s)) st for y be Point of ( Closed-Interval-MSpace (r,s)) holds (f . y) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } & B = ( Union f)) & for X be Subset of ( Closed-Interval-TSpace (r,s)) st X in B holds X is connected

    proof

      set L = ( Closed-Interval-TSpace (r,s)), M = ( Closed-Interval-MSpace (r,s));

      assume

       A1: r <= s;

      defpred P[ object, object] means ex x be Point of L, y be Point of M, B be Basis of x st $1 = x & x = y & $2 = B & B = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 };

      

       A2: L = ( TopSpaceMetr M) by TOPMETR:def 7;

      

       A3: for i be object st i in the carrier of L holds ex j be object st P[i, j]

      proof

        let i be object;

        assume i in the carrier of L;

        then

        reconsider i as Point of L;

        reconsider m = i as Point of M by A2, TOPMETR: 12;

        reconsider j = i as Element of ( TopSpaceMetr M) by A2;

        set B = ( Balls j);

        

         A4: ex y be Point of M st y = j & B = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by FRECHET:def 1;

        reconsider B1 = B as Basis of i by A2;

        take B, i, m, B1;

        thus thesis by A4;

      end;

      consider f be ManySortedSet of the carrier of L such that

       A5: for i be object st i in the carrier of L holds P[i, (f . i)] from PBOOLE:sch 3( A3);

      for x be Element of L holds (f . x) is Basis of x

      proof

        let x be Element of L;

         P[x, (f . x)] by A5;

        hence thesis;

      end;

      then

      reconsider B = ( Union f) as Basis of L by TOPGEN_2: 2;

      take B;

      hereby

        take f;

        let x be Point of M;

        the carrier of M = [.r, s.] by A1, TOPMETR: 10

        .= the carrier of L by A1, TOPMETR: 18;

        then P[x, (f . x)] by A5;

        hence (f . x) = { ( Ball (x,(1 / n))) where n be Nat : n <> 0 } & B = ( Union f);

      end;

      let X be Subset of L;

      assume X in B;

      then X in ( union ( rng f)) by CARD_3:def 4;

      then

      consider Z be set such that

       A6: X in Z and

       A7: Z in ( rng f) by TARSKI:def 4;

      consider x be object such that

       A8: x in ( dom f) and

       A9: (f . x) = Z by A7, FUNCT_1:def 3;

      consider x1 be Point of L, y be Point of M, B1 be Basis of x1 such that x = x1 and x1 = y and

       A10: (f . x) = B1 & B1 = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } by A5, A8;

      consider n be Nat such that

       A11: X = ( Ball (y,(1 / n))) and n <> 0 by A6, A9, A10;

      reconsider X1 = X as Subset of R^1 by PRE_TOPC: 11;

      ( Ball (y,(1 / n))) = [.r, s.] or ( Ball (y,(1 / n))) = [.r, (y + (1 / n)).[ or ( Ball (y,(1 / n))) = ].(y - (1 / n)), s.] or ( Ball (y,(1 / n))) = ].(y - (1 / n)), (y + (1 / n)).[ by A1, Th1;

      then X1 is connected by A11;

      hence thesis by CONNSP_1: 23;

    end;

    theorem :: TOPALG_5:3

    

     Th3: for T be TopStruct, A be Subset of T, t be Point of T st t in A holds ( Component_of (t,A)) c= A

    proof

      let T be TopStruct, A be Subset of T, t be Point of T;

      assume

       A1: t in A;

      then ( Down (t,A)) = t by CONNSP_3:def 3;

      then

       A2: ( Component_of (t,A)) = ( Component_of ( Down (t,A))) by A1, CONNSP_3:def 7;

      the carrier of (T | A) = A by PRE_TOPC: 8;

      hence thesis by A2;

    end;

    registration

      let T be TopSpace, A be open Subset of T;

      cluster (T | A) -> open;

      coherence by PRE_TOPC: 8;

    end

    theorem :: TOPALG_5:4

    

     Th4: for T be TopSpace, S be SubSpace of T, A be Subset of T, B be Subset of S st A = B holds (T | A) = (S | B)

    proof

      let T be TopSpace, S be SubSpace of T, A be Subset of T, B be Subset of S;

      assume A = B;

      then (S | B) is SubSpace of T & ( [#] (S | B)) = A by PRE_TOPC:def 5, TSEP_1: 7;

      hence thesis by PRE_TOPC:def 5;

    end;

    theorem :: TOPALG_5:5

    

     Th5: for S,T be TopSpace, A,B be Subset of T, C,D be Subset of S st the TopStruct of S = the TopStruct of T & A = C & B = D & (A,B) are_separated holds (C,D) are_separated by TOPS_3: 80;

    theorem :: TOPALG_5:6

    for S,T be TopSpace st the TopStruct of S = the TopStruct of T & S is connected holds T is connected

    proof

      let S,T be TopSpace such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: S is connected;

      let A,B be Subset of T such that

       A3: ( [#] T) = (A \/ B) and

       A4: (A,B) are_separated ;

      reconsider A1 = A, B1 = B as Subset of S by A1;

      ( [#] S) = the carrier of S & (A1,B1) are_separated by A1, A4, Th5;

      then A1 = ( {} S) or B1 = ( {} S) by A1, A2, A3;

      hence thesis;

    end;

    theorem :: TOPALG_5:7

    

     Th7: for S,T be TopSpace, A be Subset of S, B be Subset of T st the TopStruct of S = the TopStruct of T & A = B & A is connected holds B is connected

    proof

      let S,T be TopSpace, A be Subset of S, B be Subset of T such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: A = B & A is connected;

      now

        let P,Q be Subset of T such that

         A3: B = (P \/ Q) and

         A4: (P,Q) are_separated ;

        reconsider P1 = P, Q1 = Q as Subset of S by A1;

        (P1,Q1) are_separated by A1, A4, Th5;

        then P1 = ( {} S) or Q1 = ( {} S) by A2, A3, CONNSP_1: 15;

        hence P = ( {} T) or Q = ( {} T);

      end;

      hence thesis by CONNSP_1: 15;

    end;

    theorem :: TOPALG_5:8

    

     Th8: for S,T be non empty TopSpace, s be Point of S, t be Point of T, A be a_neighborhood of s st the TopStruct of S = the TopStruct of T & s = t holds A is a_neighborhood of t

    proof

      let S,T be non empty TopSpace, s be Point of S, t be Point of T, A be a_neighborhood of s such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: s = t;

      reconsider B = A as Subset of T by A1;

      

       A3: s in ( Int A) by CONNSP_2:def 1;

      ( Int A) = ( Int B) by A1, TOPS_3: 77;

      hence thesis by A2, A3, CONNSP_2:def 1;

    end;

    theorem :: TOPALG_5:9

    for S,T be non empty TopSpace, A be Subset of S, B be Subset of T, N be a_neighborhood of A st the TopStruct of S = the TopStruct of T & A = B holds N is a_neighborhood of B

    proof

      let S,T be non empty TopSpace, A be Subset of S, B be Subset of T, N be a_neighborhood of A such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: A = B;

      reconsider M = N as Subset of T by A1;

      

       A3: A c= ( Int N) by CONNSP_2:def 2;

      ( Int M) = ( Int N) by A1, TOPS_3: 77;

      hence thesis by A2, A3, CONNSP_2:def 2;

    end;

    theorem :: TOPALG_5:10

    

     Th10: for S,T be non empty TopSpace, A,B be Subset of T, f be Function of S, T st f is being_homeomorphism & A is_a_component_of B holds (f " A) is_a_component_of (f " B)

    proof

      let S,T be non empty TopSpace, A,B be Subset of T, f be Function of S, T such that

       A1: f is being_homeomorphism;

      

       A2: ( rng f) = ( [#] T) by A1

      .= the carrier of T;

      set Y = (f " A);

      given X be Subset of (T | B) such that

       A3: X = A and

       A4: X is a_component;

      

       A5: the carrier of (T | B) = B by PRE_TOPC: 8;

      then (f " X) c= (f " B) by RELAT_1: 143;

      then

      reconsider Y as Subset of (S | (f " B)) by A3, PRE_TOPC: 8;

      take Y;

      thus Y = (f " A);

      X is connected by A4;

      then A is connected by A3, CONNSP_1: 23;

      then (f " A) is connected by A1, TOPS_2: 62;

      hence Y is connected by CONNSP_1: 23;

      let Z be Subset of (S | (f " B)) such that

       A6: Z is connected and

       A7: Y c= Z;

      

       A8: (f .: Y) c= (f .: Z) by A7, RELAT_1: 123;

      

       A9: f is one-to-one by A1;

      

       A10: f is continuous by A1;

      the carrier of (S | (f " B)) = (f " B) by PRE_TOPC: 8;

      then (f .: Z) c= (f .: (f " B)) by RELAT_1: 123;

      then

      reconsider R = (f .: Z) as Subset of (T | B) by A5, A2, FUNCT_1: 77;

      reconsider Z1 = Z as Subset of S by PRE_TOPC: 11;

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

      then

       A11: Z1 c= ( dom f);

      Z1 is connected by A6, CONNSP_1: 23;

      then (f .: Z1) is connected by A10, TOPS_2: 61;

      then

       A12: R is connected by CONNSP_1: 23;

      X = (f .: Y) by A3, A2, FUNCT_1: 77;

      then X = R by A4, A12, A8;

      hence thesis by A3, A9, A11, FUNCT_1: 94;

    end;

    begin

    theorem :: TOPALG_5:11

    

     Th11: for T be non empty TopSpace, S be non empty SubSpace of T, A be non empty Subset of T, B be non empty Subset of S st A = B & A is locally_connected holds B is locally_connected by Th4;

    theorem :: TOPALG_5:12

    

     Th12: for S,T be non empty TopSpace st the TopStruct of S = the TopStruct of T & S is locally_connected holds T is locally_connected

    proof

      let S,T be non empty TopSpace such that

       A1: the TopStruct of S = the TopStruct of T and

       A2: S is locally_connected;

      let t be Point of T;

      reconsider s = t as Point of S by A1;

      let U be Subset of T;

      reconsider U1 = U as Subset of S by A1;

      assume U is a_neighborhood of t;

      then

       A3: U1 is a_neighborhood of s by A1, Th8;

      S is_locally_connected_in s by A2;

      then

      consider V1 be Subset of S such that

       A4: V1 is a_neighborhood of s and

       A5: V1 is connected and

       A6: V1 c= U1 by A3;

      reconsider V = V1 as Subset of T by A1;

      take V;

      thus V is a_neighborhood of t by A1, A4, Th8;

      thus V is connected by A1, A5, Th7;

      thus thesis by A6;

    end;

    theorem :: TOPALG_5:13

    

     Th13: for T be non empty TopSpace holds T is locally_connected iff ( [#] T) is locally_connected

    proof

      let T be non empty TopSpace;

      T is SubSpace of T by TSEP_1: 2;

      then

       A1: the TopStruct of T = the TopStruct of (T | ( [#] T)) by PRE_TOPC: 8, TSEP_1: 5;

      hence T is locally_connected implies ( [#] T) is locally_connected by Th12;

      assume ( [#] T) is locally_connected;

      then (T | ( [#] T)) is locally_connected;

      hence thesis by A1, Th12;

    end;

    

     Lm10: for T be non empty TopSpace, S be non empty open SubSpace of T st T is locally_connected holds the TopStruct of S is locally_connected

    proof

      let T be non empty TopSpace;

      let S be non empty open SubSpace of T;

      reconsider A = ( [#] S) as non empty Subset of T by TSEP_1: 1;

      

       A1: A is open by TSEP_1:def 1;

      assume T is locally_connected;

      then ( [#] S) is locally_connected by A1, Th11, CONNSP_2: 17;

      then S is locally_connected by Th13;

      then the TopStruct of S is locally_connected by Th12;

      then ( [#] the TopStruct of S) is locally_connected by Th13;

      then ( the TopStruct of S | ( [#] the TopStruct of S)) is locally_connected;

      hence thesis by TSEP_1: 3;

    end;

    theorem :: TOPALG_5:14

    

     Th14: for T be non empty TopSpace, S be non empty open SubSpace of T st T is locally_connected holds S is locally_connected

    proof

      let T be non empty TopSpace;

      let S be non empty open SubSpace of T;

      assume T is locally_connected;

      then the TopStruct of S is locally_connected by Lm10;

      hence thesis by Th12;

    end;

    theorem :: TOPALG_5:15

    for S,T be non empty TopSpace st (S,T) are_homeomorphic & S is locally_connected holds T is locally_connected

    proof

      let S,T be non empty TopSpace;

      given f be Function of S, T such that

       A1: f is being_homeomorphism;

      assume

       A2: S is locally_connected;

      now

        let A be non empty Subset of T, B be Subset of T;

        assume A is open & B is_a_component_of A;

        then

         A3: (f " A) is open & (f " B) is_a_component_of (f " A) by A1, Th10, TOPGRP_1: 26;

        ( rng f) = ( [#] T) by A1;

        then (f " A) is non empty by RELAT_1: 139;

        then (f " B) is open by A2, A3, CONNSP_2: 18;

        hence B is open by A1, TOPGRP_1: 26;

      end;

      hence thesis by CONNSP_2: 18;

    end;

    theorem :: TOPALG_5:16

    

     Th16: for T be non empty TopSpace st ex B be Basis of T st for X be Subset of T st X in B holds X is connected holds T is locally_connected

    proof

      let T be non empty TopSpace;

      given B be Basis of T such that

       A1: for X be Subset of T st X in B holds X is connected;

      let x be Point of T;

      let U be Subset of T such that

       A2: x in ( Int U);

      ( Int U) in the topology of T & the topology of T c= ( UniCl B) by CANTOR_1:def 2, PRE_TOPC:def 2;

      then

      consider Y be Subset-Family of T such that

       A3: Y c= B and

       A4: ( Int U) = ( union Y) by CANTOR_1:def 1;

      consider V be set such that

       A5: x in V and

       A6: V in Y by A2, A4, TARSKI:def 4;

      reconsider V as Subset of T by A6;

      take V;

      B c= the topology of T & V in B by A3, A6, TOPS_2: 64;

      then V is open by PRE_TOPC:def 2;

      hence x in ( Int V) by A5, TOPS_1: 23;

      thus V is connected by A1, A3, A6;

      

       A7: ( Int U) c= U by TOPS_1: 16;

      V c= ( union Y) by A6, ZFMISC_1: 74;

      hence thesis by A4, A7;

    end;

    theorem :: TOPALG_5:17

    

     Th17: r <= s implies ( Closed-Interval-TSpace (r,s)) is locally_connected

    proof

      assume r <= s;

      then ex B be Basis of ( Closed-Interval-TSpace (r,s)) st (ex f be ManySortedSet of ( Closed-Interval-TSpace (r,s)) st for y be Point of ( Closed-Interval-MSpace (r,s)) holds (f . y) = { ( Ball (y,(1 / n))) where n be Nat : n <> 0 } & B = ( Union f)) & for X be Subset of ( Closed-Interval-TSpace (r,s)) st X in B holds X is connected by Th2;

      hence thesis by Th16;

    end;

    registration

      cluster I[01] -> locally_connected;

      coherence by Th17, TOPMETR: 20;

    end

    registration

      let A be non empty open Subset of I[01] ;

      cluster ( I[01] | A) -> locally_connected;

      coherence by Th14;

    end

    begin

    definition

      let r be Real;

      :: TOPALG_5:def1

      func ExtendInt (r) -> Function of I[01] , R^1 means

      : Def1: for x be Point of I[01] holds (it . x) = (r * x);

      existence

      proof

        defpred P[ Real, set] means $2 = (r * $1);

        

         A1: for x be Element of I[01] holds ex y be Element of R st P[x, y]

        proof

          let x be Element of I[01] ;

          take (r * x);

          thus thesis by TOPMETR: 17, XREAL_0:def 1;

        end;

        ex f be Function of I, R st for x be Element of I[01] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of I[01] , R^1 such that

         A2: for x be Point of I[01] holds (f . x) = (r * x) and

         A3: for x be Point of I[01] holds (g . x) = (r * x);

        for x be Point of I[01] holds (f . x) = (g . x)

        proof

          let x be Point of I[01] ;

          

          thus (f . x) = (r * x) by A2

          .= (g . x) by A3;

        end;

        hence f = g;

      end;

    end

    registration

      let r be Real;

      cluster ( ExtendInt r) -> continuous;

      coherence

      proof

        reconsider f1 = ( id I[01] ) as Function of I[01] , R^1 by BORSUK_1: 40, FUNCT_2: 7, TOPMETR: 17;

        f1 is continuous by PRE_TOPC: 26;

        then

        consider g be Function of I[01] , R^1 such that

         A1: for p be Point of I[01] , r1 be Real st (f1 . p) = r1 holds (g . p) = (r * r1) and

         A2: g is continuous by JGRAPH_2: 23;

        for x be Point of I[01] holds (g . x) = (( ExtendInt r) . x)

        proof

          let x be Point of I[01] ;

          

          thus (g . x) = (r * (f1 . x)) by A1

          .= (r * x)

          .= (( ExtendInt r) . x) by Def1;

        end;

        hence thesis by A2, FUNCT_2: 63;

      end;

    end

    definition

      let r be Real;

      :: original: ExtendInt

      redefine

      func ExtendInt (r) -> Path of ( R^1 0 ), ( R^1 r) ;

      coherence

      proof

        thus ( ExtendInt r) is continuous;

        

        thus (( ExtendInt r) . 0 ) = (r * 0 ) by Def1, BORSUK_1:def 14

        .= ( R^1 0 ) by TOPREALB:def 2;

        

        thus (( ExtendInt r) . 1) = (r * 1) by Def1, BORSUK_1:def 15

        .= ( R^1 r) by TOPREALB:def 2;

      end;

    end

    definition

      let S,T,Y be non empty TopSpace, H be Function of [:S, T:], Y, t be Point of T;

      :: TOPALG_5:def2

      func Prj1 (t,H) -> Function of S, Y means

      : Def2: for s be Point of S holds (it . s) = (H . (s,t));

      existence

      proof

        deffunc F( Point of S) = (H . [$1, t]);

        consider f be Function of the carrier of S, the carrier of Y such that

         A1: for x be Element of S holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Point of S;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be Function of S, Y such that

         A2: for s be Point of S holds (f . s) = (H . (s,t)) and

         A3: for s be Point of S holds (g . s) = (H . (s,t));

        now

          let s be Point of S;

          

          thus (f . s) = (H . (s,t)) by A2

          .= (g . s) by A3;

        end;

        hence thesis;

      end;

    end

    definition

      let S,T,Y be non empty TopSpace, H be Function of [:S, T:], Y, s be Point of S;

      :: TOPALG_5:def3

      func Prj2 (s,H) -> Function of T, Y means

      : Def3: for t be Point of T holds (it . t) = (H . (s,t));

      existence

      proof

        deffunc F( Point of T) = (H . [s, $1]);

        consider f be Function of the carrier of T, the carrier of Y such that

         A1: for x be Element of T holds (f . x) = F(x) from FUNCT_2:sch 4;

        take f;

        let x be Point of T;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be Function of T, Y such that

         A2: for t be Point of T holds (f . t) = (H . (s,t)) and

         A3: for t be Point of T holds (g . t) = (H . (s,t));

        now

          let t be Point of T;

          

          thus (f . t) = (H . (s,t)) by A2

          .= (g . t) by A3;

        end;

        hence thesis;

      end;

    end

    registration

      let S,T,Y be non empty TopSpace, H be continuous Function of [:S, T:], Y, t be Point of T;

      cluster ( Prj1 (t,H)) -> continuous;

      coherence

      proof

        for p be Point of S, V be Subset of Y st (( Prj1 (t,H)) . p) in V & V is open holds ex W be Subset of S st p in W & W is open & (( Prj1 (t,H)) .: W) c= V

        proof

          let p be Point of S, V be Subset of Y such that

           A1: (( Prj1 (t,H)) . p) in V & V is open;

          (( Prj1 (t,H)) . p) = (H . (p,t)) by Def2;

          then

          consider W be Subset of [:S, T:] such that

           A2: [p, t] in W and

           A3: W is open and

           A4: (H .: W) c= V by A1, JGRAPH_2: 10;

          consider A be Subset-Family of [:S, T:] such that

           A5: W = ( union A) and

           A6: for e be set st e in A holds ex X1 be Subset of S, Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open by A3, BORSUK_1: 5;

          consider e be set such that

           A7: [p, t] in e and

           A8: e in A by A2, A5, TARSKI:def 4;

          consider X1 be Subset of S, Y1 be Subset of T such that

           A9: e = [:X1, Y1:] and

           A10: X1 is open and Y1 is open by A6, A8;

          take X1;

          thus p in X1 by A7, A9, ZFMISC_1: 87;

          thus X1 is open by A10;

          let x be object;

          assume x in (( Prj1 (t,H)) .: X1);

          then

          consider c be Point of S such that

           A11: c in X1 and

           A12: x = (( Prj1 (t,H)) . c) by FUNCT_2: 65;

          t in Y1 by A7, A9, ZFMISC_1: 87;

          then [c, t] in [:X1, Y1:] by A11, ZFMISC_1: 87;

          then [c, t] in W by A5, A8, A9, TARSKI:def 4;

          then

           A13: (H . [c, t]) in (H .: W) by FUNCT_2: 35;

          (( Prj1 (t,H)) . c) = (H . (c,t)) by Def2

          .= (H . [c, t]);

          hence thesis by A4, A12, A13;

        end;

        hence thesis by JGRAPH_2: 10;

      end;

    end

    registration

      let S,T,Y be non empty TopSpace, H be continuous Function of [:S, T:], Y, s be Point of S;

      cluster ( Prj2 (s,H)) -> continuous;

      coherence

      proof

        for p be Point of T, V be Subset of Y st (( Prj2 (s,H)) . p) in V & V is open holds ex W be Subset of T st p in W & W is open & (( Prj2 (s,H)) .: W) c= V

        proof

          let p be Point of T, V be Subset of Y such that

           A1: (( Prj2 (s,H)) . p) in V & V is open;

          (( Prj2 (s,H)) . p) = (H . (s,p)) by Def3;

          then

          consider W be Subset of [:S, T:] such that

           A2: [s, p] in W and

           A3: W is open and

           A4: (H .: W) c= V by A1, JGRAPH_2: 10;

          consider A be Subset-Family of [:S, T:] such that

           A5: W = ( union A) and

           A6: for e be set st e in A holds ex X1 be Subset of S, Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open by A3, BORSUK_1: 5;

          consider e be set such that

           A7: [s, p] in e and

           A8: e in A by A2, A5, TARSKI:def 4;

          consider X1 be Subset of S, Y1 be Subset of T such that

           A9: e = [:X1, Y1:] and X1 is open and

           A10: Y1 is open by A6, A8;

          take Y1;

          thus p in Y1 by A7, A9, ZFMISC_1: 87;

          thus Y1 is open by A10;

          let x be object;

          assume x in (( Prj2 (s,H)) .: Y1);

          then

          consider c be Point of T such that

           A11: c in Y1 and

           A12: x = (( Prj2 (s,H)) . c) by FUNCT_2: 65;

          s in X1 by A7, A9, ZFMISC_1: 87;

          then [s, c] in [:X1, Y1:] by A11, ZFMISC_1: 87;

          then [s, c] in W by A5, A8, A9, TARSKI:def 4;

          then

           A13: (H . [s, c]) in (H .: W) by FUNCT_2: 35;

          (( Prj2 (s,H)) . c) = (H . (s,c)) by Def3

          .= (H . [s, c]);

          hence thesis by A4, A12, A13;

        end;

        hence thesis by JGRAPH_2: 10;

      end;

    end

    theorem :: TOPALG_5:18

    for T be non empty TopSpace, a,b be Point of T, P,Q be Path of a, b, H be Homotopy of P, Q, t be Point of I[01] st H is continuous holds ( Prj1 (t,H)) is continuous;

    theorem :: TOPALG_5:19

    for T be non empty TopSpace, a,b be Point of T, P,Q be Path of a, b, H be Homotopy of P, Q, s be Point of I[01] st H is continuous holds ( Prj2 (s,H)) is continuous;

    set TUC = ( Tunit_circle 2);

    set cS1 = the carrier of TUC;

     Lm11:

    now

      TUC = ( Tcircle (( 0. ( TOP-REAL 2)),1)) by TOPREALB:def 7;

      hence cS1 = ( Sphere ( |[ 0 , 0 ]|,1)) by EUCLID: 54, TOPREALB: 9;

    end;

    

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

    definition

      let r be Real;

      :: TOPALG_5:def4

      func cLoop (r) -> Function of I[01] , ( Tunit_circle 2) means

      : Def4: for x be Point of I[01] holds (it . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x))]|;

      existence

      proof

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

        

         A1: for x be Element of I[01] holds ex y be Element of cS1 st P[x, y]

        proof

          let x be Element of I[01] ;

          set y = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * 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 ) * r) * x)) ^2 ) + ((y `2 ) ^2 ))) by EUCLID: 52

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

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

          then

          reconsider y as Element of cS1 by Lm11, TOPREAL9: 9;

          take y;

          thus thesis;

        end;

        ex f be Function of I, cS1 st for x be Element of I[01] holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of I[01] , TUC such that

         A2: for x be Point of I[01] holds (f . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x))]| and

         A3: for x be Point of I[01] holds (g . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x))]|;

        for x be Point of I[01] holds (f . x) = (g . x)

        proof

          let x be Point of I[01] ;

          

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

          .= (g . x) by A3;

        end;

        hence f = g;

      end;

    end

    theorem :: TOPALG_5:20

    

     Th20: ( cLoop r) = ( CircleMap * ( ExtendInt r))

    proof

      for x be Point of I[01] holds (( cLoop r) . x) = (( CircleMap * ( ExtendInt r)) . x)

      proof

        let x be Point of I[01] ;

        

         A1: (( ExtendInt r) . x) = (r * x) by Def1;

        

        thus (( cLoop r) . x) = |[( cos (((2 * PI ) * r) * x)), ( sin (((2 * PI ) * r) * x))]| by Def4

        .= |[( cos ((2 * PI ) * (( ExtendInt r) . x))), ( sin ((2 * PI ) * (( ExtendInt r) . x)))]| by A1

        .= ( CircleMap . (( ExtendInt r) . x)) by TOPREALB:def 11

        .= (( CircleMap * ( ExtendInt r)) . x) by FUNCT_2: 15;

      end;

      hence thesis;

    end;

    definition

      let n be Integer;

      :: original: cLoop

      redefine

      func cLoop (n) -> Loop of c[10] ;

      coherence

      proof

        set f = ( cLoop n);

        f = ( CircleMap * ( ExtendInt n)) by Th20;

        hence f is continuous;

        

        thus (f . 0 ) = |[( cos (((2 * PI ) * n) * j0)), ( sin (((2 * PI ) * n) * j0))]| by Def4

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

        

        thus (f . 1) = |[( cos (((2 * PI ) * n) * j1)), ( sin (((2 * PI ) * n) * j1))]| by Def4

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

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

      end;

    end

    begin

    

     Lm13: ex F be Subset-Family of ( Tunit_circle 2) st F is Cover of ( Tunit_circle 2) & F is open & for U be Subset of ( Tunit_circle 2) st U in F holds ex D be mutually-disjoint open Subset-Family of R^1 st ( union D) = ( CircleMap " U) & for d be Subset of R^1 st d in D holds for f be Function of ( R^1 | d), (( Tunit_circle 2) | U) st f = ( CircleMap | d) holds f is being_homeomorphism

    proof

      consider F be Subset-Family of ( Tunit_circle 2) such that

       A1: F = {( CircleMap .: ]. 0 , 1.[), ( CircleMap .: ].(1 / 2), (3 / 2).[)} and

       A2: F is Cover of ( Tunit_circle 2) & F is open and

       A3: 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) by TOPREALB: 45;

      take F;

      thus F is Cover of ( Tunit_circle 2) & F is open by A2;

      let U be Subset of ( Tunit_circle 2);

      assume

       A4: U in F;

      per cases by A1, A4, TARSKI:def 2;

        suppose

         A5: U = ( CircleMap .: ]. 0 , 1.[);

        reconsider D = ( IntIntervals ( 0 ,1)) as mutually-disjoint open Subset-Family of R^1 by Lm8, TOPREALB: 4;

        take D;

        thus thesis by A3, A5;

      end;

        suppose

         A6: U = ( CircleMap .: ].(1 / 2), (3 / 2).[);

        reconsider D = ( IntIntervals ((1 / 2),(3 / 2))) as mutually-disjoint open Subset-Family of R^1 by Lm9, TOPREALB: 4;

        take D;

        thus thesis by A3, A6;

      end;

    end;

    

     Lm14: ( [#] ( Sspace 0[01] )) = { 0 } by TEX_2:def 2;

    

     Lm15: for F be Subset-Family of ( Closed-Interval-TSpace (r,s)), C be IntervalCover of F, G be IntervalCoverPts of C holds F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s implies G is non empty

    proof

      let F be Subset-Family of ( Closed-Interval-TSpace (r,s)), C be IntervalCover of F, G be IntervalCoverPts of C;

      assume F is Cover of ( Closed-Interval-TSpace (r,s)) & F is open connected & r <= s;

      then ( len G) = (( len C) + 1) by RCOMP_3:def 3;

      hence thesis by CARD_1: 27;

    end;

    theorem :: TOPALG_5:21

    

     Th21: for UL be Subset-Family of ( Tunit_circle 2) st UL is Cover of ( Tunit_circle 2) & UL is open holds for Y be non empty TopSpace, F be continuous Function of [:Y, I[01] :], ( Tunit_circle 2), y be Point of Y holds ex T be non empty FinSequence of REAL st (T . 1) = 0 & (T . ( len T)) = 1 & T is increasing & ex N be open Subset of Y st y in N & for i be Nat st i in ( dom T) & (i + 1) in ( dom T) holds ex Ui be non empty Subset of ( Tunit_circle 2) st Ui in UL & (F .: [:N, [.(T . i), (T . (i + 1)).]:]) c= Ui

    proof

      set L = ( Closed-Interval-TSpace ( 0 ,1));

      let UL be Subset-Family of TUC such that

       A1: UL is Cover of TUC and

       A2: UL is open;

      let Y be non empty TopSpace, F be continuous Function of [:Y, I[01] :], TUC, y be Point of Y;

      

       A3: ( [#] TUC) = ( union UL) by A1, SETFAM_1: 45;

      

       A4: for i be Point of I[01] holds ex U be non empty open Subset of TUC st (F . [y, i]) in U & U in UL

      proof

        let i be Point of I[01] ;

        consider U be set such that

         A5: (F . [y, i]) in U & U in UL by A3, TARSKI:def 4;

        reconsider U as non empty open Subset of TUC by A2, A5;

        take U;

        thus thesis by A5;

      end;

      then ex U be non empty open Subset of TUC st (F . [y, 0[01] ]) in U & U in UL;

      then

      reconsider UL1 = UL as non empty set;

      set C = the carrier of Y;

      defpred I0[ set, set] means ex V be open Subset of TUC st V in UL1 & (F . [y, $1]) in V & $2 = V;

      

       A6: for i be Element of I holds ex z be Element of UL1 st I0[i, z]

      proof

        let i be Element of I;

        ex U be non empty open Subset of TUC st (F . [y, i]) in U & U in UL by A4;

        hence thesis;

      end;

      consider I0 be Function of I, UL1 such that

       A7: for i be Element of I holds I0[i, (I0 . i)] from FUNCT_2:sch 3( A6);

      defpred I1[ object, object] means ex M be open Subset of Y, O be open connected Subset of I[01] st y in M & $1 in O & (F .: [:M, O:]) c= (I0 . $1) & $2 = [:M, O:];

      

       A8: for i be Element of I holds ex z be Subset of [:C, I:] st I1[i, z]

      proof

        let i be Element of I;

        consider V be open Subset of TUC such that V in UL1 and

         A9: (F . [y, i]) in V and

         A10: (I0 . i) = V by A7;

        consider W be Subset of [:Y, I[01] :] such that

         A11: [y, i] in W and

         A12: W is open and

         A13: (F .: W) c= V by A9, JGRAPH_2: 10;

        consider Q be Subset-Family of [:Y, I[01] :] such that

         A14: W = ( union Q) and

         A15: for e be set st e in Q holds ex A be Subset of Y, B be Subset of I[01] st e = [:A, B:] & A is open & B is open by A12, BORSUK_1: 5;

        consider Z be set such that

         A16: [y, i] in Z and

         A17: Z in Q by A11, A14, TARSKI:def 4;

        consider A be Subset of Y, B be Subset of I[01] such that

         A18: Z = [:A, B:] and

         A19: A is open and

         A20: B is open by A15, A17;

        reconsider A as open Subset of Y by A19;

        

         A21: i in B by A16, A18, ZFMISC_1: 87;

        reconsider B as non empty open Subset of I[01] by A16, A18, A20;

        reconsider i1 = i as Point of ( I[01] | B) by A21, PRE_TOPC: 8;

        ( Component_of i1) is a_component by CONNSP_1: 40;

        then

         A22: ( Component_of i1) is open by CONNSP_2: 15;

        ( Component_of (i,B)) = ( Component_of i1) by A21, CONNSP_3:def 7;

        then

        reconsider D = ( Component_of (i,B)) as open connected Subset of I[01] by A21, A22, CONNSP_3: 33, TSEP_1: 17;

        reconsider z = [:A, D:] as Subset of [:C, I:] by BORSUK_1:def 2;

        take z, A, D;

        thus y in A by A16, A18, ZFMISC_1: 87;

        thus i in D by A21, CONNSP_3: 26;

        D c= B by A21, Th3;

        then

         A23: z c= [:A, B:] by ZFMISC_1: 95;

         [:A, B:] c= W by A14, A17, A18, ZFMISC_1: 74;

        then z c= W by A23;

        then (F .: z) c= (F .: W) by RELAT_1: 123;

        hence (F .: [:A, D:]) c= (I0 . i) by A10, A13;

        thus thesis;

      end;

      consider I1 be Function of I, ( bool [:C, I:]) such that

       A24: for i be Element of I holds I1[i, (I1 . i)] from FUNCT_2:sch 3( A8);

      reconsider C1 = ( rng I1) as Subset-Family of [:Y, I[01] :] by BORSUK_1:def 2;

      

       A25: C1 is open

      proof

        let P be Subset of [:Y, I[01] :];

        assume P in C1;

        then

        consider i be object such that

         A26: i in ( dom I1) and

         A27: (I1 . i) = P by FUNCT_1:def 3;

         I1[i, (I1 . i)] by A24, A26;

        hence thesis by A27, BORSUK_1: 6;

      end;

      

       A28: ( dom I1) = I by FUNCT_2:def 1;

       [: {y}, ( [#] I[01] ):] c= ( union C1)

      proof

        let a be object;

        assume a in [: {y}, ( [#] I[01] ):];

        then

        consider a1,a2 be object such that

         A29: a1 in {y} and

         A30: a2 in ( [#] I[01] ) and

         A31: a = [a1, a2] by ZFMISC_1:def 2;

        

         A32: a1 = y by A29, TARSKI:def 1;

        reconsider a2 as Point of I[01] by A30;

        consider M be open Subset of Y, O be open connected Subset of I[01] such that

         A33: y in M & a2 in O and (F .: [:M, O:]) c= (I0 . a2) and

         A34: (I1 . a2) = [:M, O:] by A24;

         [y, a2] in [:M, O:] & [:M, O:] in C1 by A28, A33, A34, FUNCT_1:def 3, ZFMISC_1: 87;

        hence thesis by A31, A32, TARSKI:def 4;

      end;

      then

       A35: C1 is Cover of [: {y}, ( [#] I[01] ):] by SETFAM_1:def 11;

       [: {y}, ( [#] I[01] ):] is compact by BORSUK_3: 23;

      then

      consider G be Subset-Family of [:Y, I[01] :] such that

       A36: G c= C1 and

       A37: G is Cover of [: {y}, ( [#] I[01] ):] and

       A38: G is finite by A35, A25;

      set NN = { M where M be open Subset of Y : y in M & ex O be open Subset of I[01] st [:M, O:] in G };

      NN c= ( bool C)

      proof

        let a be object;

        assume a in NN;

        then ex M be open Subset of Y st a = M & y in M & ex O be open Subset of I[01] st [:M, O:] in G;

        hence thesis;

      end;

      then

      reconsider NN as Subset-Family of Y;

      consider p be Function such that

       A39: ( rng p) = G and

       A40: ( dom p) in omega by A38, FINSET_1:def 1;

      defpred F[ object, object] means ex M be open Subset of Y, O be non empty open Subset of I[01] st y in M & (p . $1) = [:M, O:] & $2 = M;

      

       A41: for x be object st x in ( dom p) holds ex y be object st y in NN & F[x, y]

      proof

        let x be object;

        assume x in ( dom p);

        then

         A42: (p . x) in ( rng p) by FUNCT_1:def 3;

        then

        consider i be object such that

         A43: i in ( dom I1) and

         A44: (I1 . i) = (p . x) by A36, A39, FUNCT_1:def 3;

        consider M be open Subset of Y, O be open connected Subset of I[01] such that

         A45: y in M & i in O and (F .: [:M, O:]) c= (I0 . i) and

         A46: (I1 . i) = [:M, O:] by A24, A43;

        take M;

        thus thesis by A39, A42, A44, A45, A46;

      end;

      consider p1 be Function of ( dom p), NN such that

       A47: for x be object st x in ( dom p) holds F[x, (p1 . x)] from FUNCT_2:sch 1( A41);

      set ICOV = { O where O be open connected Subset of I[01] : ex M be open Subset of Y st [:M, O:] in G };

      

       A48: [: {y}, ( [#] I[01] ):] c= ( union G) by A37, SETFAM_1:def 11;

      

       A49: y in {y} by TARSKI:def 1;

      then [y, 0[01] ] in [: {y}, ( [#] I[01] ):] by ZFMISC_1:def 2;

      then

      consider Z be set such that [y, 0[01] ] in Z and

       A50: Z in G by A48, TARSKI:def 4;

      consider i be object such that

       A51: i in ( dom I1) and

       A52: (I1 . i) = Z by A36, A50, FUNCT_1:def 3;

      consider M be open Subset of Y, O be open connected Subset of I[01] such that

       A53: y in M and i in O and (F .: [:M, O:]) c= (I0 . i) and

       A54: (I1 . i) = [:M, O:] by A24, A51;

      

       A55: M in NN by A50, A52, A53, A54;

      then

       A56: ( dom p1) = ( dom p) by FUNCT_2:def 1;

      ( rng p1) = NN

      proof

        thus ( rng p1) c= NN;

        let a be object;

        assume a in NN;

        then

        consider M be open Subset of Y such that

         A57: a = M and y in M and

         A58: ex O be open Subset of I[01] st [:M, O:] in G;

        consider O be open Subset of I[01] such that

         A59: [:M, O:] in G by A58;

        consider b be object such that

         A60: b in ( dom p) and

         A61: (p . b) = [:M, O:] by A39, A59, FUNCT_1:def 3;

        consider M1 be open Subset of Y, O1 be non empty open Subset of I[01] such that

         A62: y in M1 & (p . b) = [:M1, O1:] and

         A63: (p1 . b) = M1 by A47, A60;

        M1 = M by A61, A62, ZFMISC_1: 110;

        hence thesis by A56, A57, A60, A63, FUNCT_1:def 3;

      end;

      then

       A64: NN is finite by A40, A56, FINSET_1:def 1;

      NN is open

      proof

        let a be Subset of Y;

        assume a in NN;

        then ex M be open Subset of Y st a = M & y in M & ex O be open Subset of I[01] st [:M, O:] in G;

        hence thesis;

      end;

      then

      reconsider N = ( meet NN) as open Subset of Y by A64, TOPS_2: 20;

      ICOV c= ( bool I)

      proof

        let a be object;

        assume a in ICOV;

        then ex O be open connected Subset of I[01] st a = O & ex M be open Subset of Y st [:M, O:] in G;

        hence thesis;

      end;

      then

      reconsider ICOV as Subset-Family of L by TOPMETR: 20;

      ( [#] L) c= ( union ICOV)

      proof

        let a be object;

        assume a in ( [#] L);

        then

        reconsider a as Point of I[01] by TOPMETR: 20;

         [y, a] in [: {y}, ( [#] I[01] ):] by A49, ZFMISC_1:def 2;

        then

        consider Z be set such that

         A65: [y, a] in Z and

         A66: Z in G by A48, TARSKI:def 4;

        consider i be object such that

         A67: i in ( dom I1) and

         A68: (I1 . i) = Z by A36, A66, FUNCT_1:def 3;

        consider M be open Subset of Y, O be open connected Subset of I[01] such that y in M and i in O and (F .: [:M, O:]) c= (I0 . i) and

         A69: (I1 . i) = [:M, O:] by A24, A67;

        a in O & O in ICOV by A65, A66, A68, A69, ZFMISC_1: 87;

        hence thesis by TARSKI:def 4;

      end;

      then

       A70: ICOV is Cover of L by SETFAM_1:def 11;

      set NCOV = the IntervalCover of ICOV;

      set T = the IntervalCoverPts of NCOV;

      

       A71: ICOV is connected

      proof

        let X be Subset of L;

        assume X in ICOV;

        then ex O be open connected Subset of I[01] st X = O & ex M be open Subset of Y st [:M, O:] in G;

        hence thesis by TOPMETR: 20;

      end;

      

       A72: ICOV is open

      proof

        let a be Subset of L;

        assume a in ICOV;

        then ex O be open connected Subset of I[01] st a = O & ex M be open Subset of Y st [:M, O:] in G;

        hence thesis by TOPMETR: 20;

      end;

      then

      reconsider T as non empty FinSequence of REAL by A70, A71, Lm15;

      take T;

      thus (T . 1) = 0 & (T . ( len T)) = 1 by A70, A72, A71, RCOMP_3:def 3;

      thus T is increasing by A70, A72, A71, RCOMP_3: 65;

      take N;

      now

        let Z be set;

        assume Z in NN;

        then ex M be open Subset of Y st Z = M & y in M & ex O be open Subset of I[01] st [:M, O:] in G;

        hence y in Z;

      end;

      hence y in N by A55, SETFAM_1:def 1;

      let i be Nat;

      assume that

       A73: i in ( dom T) and

       A74: (i + 1) in ( dom T);

      

       A75: 1 <= i by A73, FINSEQ_3: 25;

      

       A76: (i + 1) <= ( len T) by A74, FINSEQ_3: 25;

      ( len T) = (( len NCOV) + 1) by A70, A72, A71, RCOMP_3:def 3;

      then i <= ( len NCOV) by A76, XREAL_1: 6;

      then i in ( dom NCOV) by A75, FINSEQ_3: 25;

      then

       A77: (NCOV . i) in ( rng NCOV) by FUNCT_1:def 3;

      ( rng NCOV) c= ICOV by A70, A72, A71, RCOMP_3:def 2;

      then (NCOV . i) in ICOV by A77;

      then

      consider O be open connected Subset of I[01] such that

       A78: (NCOV . i) = O and

       A79: ex M be open Subset of Y st [:M, O:] in G;

      consider M be open Subset of Y such that

       A80: [:M, O:] in G by A79;

      i < ( len T) by A76, NAT_1: 13;

      then

       A81: [.(T . i), (T . (i + 1)).] c= O by A70, A72, A71, A75, A78, RCOMP_3: 66;

      consider j be object such that

       A82: j in ( dom I1) and

       A83: (I1 . j) = [:M, O:] by A36, A80, FUNCT_1:def 3;

      consider V be open Subset of TUC such that

       A84: V in UL1 and

       A85: (F . [y, j]) in V and

       A86: (I0 . j) = V by A7, A82;

      reconsider V as non empty open Subset of TUC by A85;

      take V;

      thus V in UL by A84;

      consider M1 be open Subset of Y, O1 be open connected Subset of I[01] such that

       A87: y in M1 and

       A88: j in O1 and

       A89: (F .: [:M1, O1:]) c= (I0 . j) and

       A90: (I1 . j) = [:M1, O1:] by A24, A82;

      M = M1 by A83, A87, A88, A90, ZFMISC_1: 110;

      then M in NN by A80, A87;

      then N c= M by SETFAM_1: 3;

      then [:N, [.(T . i), (T . (i + 1)).]:] c= [:M1, O1:] by A83, A90, A81, ZFMISC_1: 96;

      then (F .: [:N, [.(T . i), (T . (i + 1)).]:]) c= (F .: [:M1, O1:]) by RELAT_1: 123;

      hence thesis by A89, A86;

    end;

    theorem :: TOPALG_5:22

    

     Th22: for Y be non empty TopSpace, F be Function of [:Y, I[01] :], ( Tunit_circle 2), Ft be Function of [:Y, ( Sspace 0[01] ):], R^1 st F is continuous & Ft is continuous & (F | [:the carrier of Y, { 0 }:]) = ( CircleMap * Ft) holds ex G be Function of [:Y, I[01] :], R^1 st G is continuous & F = ( CircleMap * G) & (G | [:the carrier of Y, { 0 }:]) = Ft & for H be Function of [:Y, I[01] :], R^1 st H is continuous & F = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = Ft holds G = H

    proof

      consider UL be Subset-Family of TUC such that

       A1: UL is Cover of TUC & UL is open and

       A2: for U be Subset of TUC st U in UL holds ex D be mutually-disjoint open Subset-Family of R^1 st ( union D) = ( CircleMap " U) & for d be Subset of R^1 st d in D holds for f be Function of ( R^1 | d), (TUC | U) st f = ( CircleMap | d) holds f is being_homeomorphism by Lm13;

      let Y be non empty TopSpace, F be Function of [:Y, I[01] :], TUC, Ft be Function of [:Y, ( Sspace 0[01] ):], R^1 such that

       A3: F is continuous and

       A4: Ft is continuous and

       A5: (F | [:the carrier of Y, { 0 }:]) = ( CircleMap * Ft);

      defpred A[ set, set] means ex y be Point of Y, t be Point of I[01] , N be non empty open Subset of Y, Fn be Function of [:(Y | N), I[01] :], R^1 st $1 = [y, t] & $2 = (Fn . $1) & y in N & Fn is continuous & (F | [:N, I:]) = ( CircleMap * Fn) & (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) & for H be Function of [:(Y | N), I[01] :], R^1 st H is continuous & (F | [:N, I:]) = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) holds Fn = H;

      

       A6: ( dom F) = the carrier of [:Y, I[01] :] by FUNCT_2:def 1

      .= [:the carrier of Y, I:] by BORSUK_1:def 2;

      

       A7: the carrier of [:Y, ( Sspace 0[01] ):] = [:the carrier of Y, the carrier of ( Sspace 0[01] ):] by BORSUK_1:def 2;

      then

       A8: ( dom Ft) = [:the carrier of Y, { 0 }:] by Lm14, FUNCT_2:def 1;

      

       A9: for x be Point of [:Y, I[01] :] holds ex z be Point of R^1 st A[x, z]

      proof

        let x be Point of [:Y, I[01] :];

        consider y be Point of Y, t be Point of I[01] such that

         A10: x = [y, t] by BORSUK_1: 10;

        consider TT be non empty FinSequence of REAL such that

         A11: (TT . 1) = 0 and

         A12: (TT . ( len TT)) = 1 and

         A13: TT is increasing and

         A14: ex N be open Subset of Y st y in N & for i be Nat st i in ( dom TT) & (i + 1) in ( dom TT) holds ex Ui be non empty Subset of ( Tunit_circle 2) st Ui in UL & (F .: [:N, [.(TT . i), (TT . (i + 1)).]:]) c= Ui by A3, A1, Th21;

        consider N be open Subset of Y such that

         A15: y in N and

         A16: for i be Nat st i in ( dom TT) & (i + 1) in ( dom TT) holds ex Ui be non empty Subset of ( Tunit_circle 2) st Ui in UL & (F .: [:N, [.(TT . i), (TT . (i + 1)).]:]) c= Ui by A14;

        reconsider N as non empty open Subset of Y by A15;

        defpred N[ Nat] means $1 in ( dom TT) implies ex N2 be non empty open Subset of Y, S be non empty Subset of I[01] , Fn be Function of [:(Y | N2), ( I[01] | S):], R^1 st S = [. 0 , (TT . $1).] & y in N2 & N2 c= N & Fn is continuous & (F | [:N2, S:]) = ( CircleMap * Fn) & (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]);

        

         A17: ( len TT) in ( dom TT) by FINSEQ_5: 6;

        

         A18: 1 in ( dom TT) by FINSEQ_5: 6;

         A19:

        now

          let i be Element of NAT such that

           A20: i in ( dom TT);

          1 <= i by A20, FINSEQ_3: 25;

          then 1 = i or 1 < i by XXREAL_0: 1;

          hence

           A21: 0 <= (TT . i) by A11, A13, A18, A20, SEQM_3:def 1;

          assume

           A22: (i + 1) in ( dom TT);

          

           A23: (i + 0 ) < (i + 1) by XREAL_1: 8;

          hence

           A24: (TT . i) < (TT . (i + 1)) by A13, A20, A22, SEQM_3:def 1;

          (i + 1) <= ( len TT) by A22, FINSEQ_3: 25;

          then (i + 1) = ( len TT) or (i + 1) < ( len TT) by XXREAL_0: 1;

          hence (TT . (i + 1)) <= 1 by A12, A13, A17, A22, SEQM_3:def 1;

          hence (TT . i) < 1 by A24, XXREAL_0: 2;

          thus 0 < (TT . (i + 1)) by A13, A20, A21, A22, A23, SEQM_3:def 1;

        end;

         A25:

        now

          let i be Nat such that

           A26: 0 <= (TT . i) and

           A27: (TT . (i + 1)) <= 1;

          thus [.(TT . i), (TT . (i + 1)).] c= I

          proof

            let a be object;

            assume

             A28: a in [.(TT . i), (TT . (i + 1)).];

            then

            reconsider a as Real;

            a <= (TT . (i + 1)) by A28, XXREAL_1: 1;

            then

             A29: a <= 1 by A27, XXREAL_0: 2;

             0 <= a by A26, A28, XXREAL_1: 1;

            hence thesis by A29, BORSUK_1: 43;

          end;

        end;

        

         A30: for i be Nat st N[i] holds N[(i + 1)]

        proof

          let i be Nat;

          assume that

           A31: N[i] and

           A32: (i + 1) in ( dom TT);

          per cases by A32, TOPREALA: 2;

            suppose

             A33: i = 0 ;

            take N2 = N;

            set Fn = (Ft | [:N2, { 0 }:]);

            set S = [. 0 , (TT . (i + 1)).];

            

             A34: S = { 0 } by A11, A33, XXREAL_1: 17;

            reconsider S as non empty Subset of I[01] by A11, A33, Lm3, XXREAL_1: 17;

            

             A35: ( dom Fn) = [:N2, S:] by A8, A34, RELAT_1: 62, ZFMISC_1: 96;

            reconsider K0 = [:N2, S:] as non empty Subset of [:Y, ( Sspace 0[01] ):] by A7, A34, Lm14, ZFMISC_1: 96;

            

             A36: the carrier of [:(Y | N2), ( I[01] | S):] = [:the carrier of (Y | N2), the carrier of ( I[01] | S):] & ( rng Fn) c= R by BORSUK_1:def 2;

            the carrier of (Y | N2) = N2 & the carrier of ( I[01] | S) = S by PRE_TOPC: 8;

            then

            reconsider Fn as Function of [:(Y | N2), ( I[01] | S):], R^1 by A35, A36, FUNCT_2: 2;

            

             A37: ( dom (F | [:N2, S:])) = [:N2, S:] by A6, RELAT_1: 62, ZFMISC_1: 96;

            reconsider S1 = S as non empty Subset of ( Sspace 0[01] ) by A11, A33, Lm14, XXREAL_1: 17;

            take S, Fn;

            thus S = [. 0 , (TT . (i + 1)).];

            thus y in N2 by A15;

            thus N2 c= N;

            ( I[01] | S) = ( Sspace 0[01] ) by A34, TOPALG_3: 5

            .= (( Sspace 0[01] ) | S1) by A34, Lm14, TSEP_1: 3;

            then [:(Y | N2), ( I[01] | S):] = ( [:Y, ( Sspace 0[01] ):] | K0) by BORSUK_3: 22;

            hence Fn is continuous by A4, A34, TOPMETR: 7;

            ( rng Fn) c= ( dom CircleMap ) by Lm12, TOPMETR: 17;

            then

             A38: ( dom ( CircleMap * Fn)) = ( dom Fn) by RELAT_1: 27;

            

             A39: [:N2, S:] c= ( dom Ft) by A8, A34, ZFMISC_1: 96;

            for x be object st x in ( dom (F | [:N2, S:])) holds ((F | [:N2, S:]) . x) = (( CircleMap * Fn) . x)

            proof

              let x be object such that

               A40: x in ( dom (F | [:N2, S:]));

              

              thus ((F | [:N2, S:]) . x) = (F . x) by A37, A40, FUNCT_1: 49

              .= (( CircleMap * Ft) . x) by A5, A7, A35, A37, A40, Lm14, FUNCT_1: 49

              .= ( CircleMap . (Ft . x)) by A39, A37, A40, FUNCT_1: 13

              .= ( CircleMap . (Fn . x)) by A34, A37, A40, FUNCT_1: 49

              .= (( CircleMap * Fn) . x) by A35, A37, A40, FUNCT_1: 13;

            end;

            hence (F | [:N2, S:]) = ( CircleMap * Fn) by A35, A37, A38;

            

             A41: ( dom (Fn | [:the carrier of Y, { 0 }:])) = ( [:N2, S:] /\ [:the carrier of Y, { 0 }:]) by A35, RELAT_1: 61;

            

             A42: for x be object st x in ( dom (Fn | [:the carrier of Y, { 0 }:])) holds ((Fn | [:the carrier of Y, { 0 }:]) . x) = ((Ft | [:N2, I:]) . x)

            proof

              

               A43: [:N2, { 0 }:] c= [:N2, I:] by Lm3, ZFMISC_1: 95;

              let x be object such that

               A44: x in ( dom (Fn | [:the carrier of Y, { 0 }:]));

              

               A45: x in [:N2, { 0 }:] by A34, A41, A44, XBOOLE_0:def 4;

              x in [:the carrier of Y, { 0 }:] by A41, A44, XBOOLE_0:def 4;

              

              hence ((Fn | [:the carrier of Y, { 0 }:]) . x) = (Fn . x) by FUNCT_1: 49

              .= (Ft . x) by A45, FUNCT_1: 49

              .= ((Ft | [:N2, I:]) . x) by A45, A43, FUNCT_1: 49;

            end;

            ( dom (Ft | [:N2, I:])) = ( [:the carrier of Y, { 0 }:] /\ [:N2, I:]) by A8, RELAT_1: 61

            .= [:N2, S:] by A34, ZFMISC_1: 101;

            hence thesis by A34, A41, A42, ZFMISC_1: 101;

          end;

            suppose

             A46: i in ( dom TT);

            set SS = [.(TT . i), (TT . (i + 1)).];

            consider Ui be non empty Subset of TUC such that

             A47: Ui in UL and

             A48: (F .: [:N, SS:]) c= Ui by A16, A32, A46;

            consider D be mutually-disjoint open Subset-Family of R^1 such that

             A49: ( union D) = ( CircleMap " Ui) and

             A50: for d be Subset of R^1 st d in D holds for f be Function of ( R^1 | d), (TUC | Ui) st f = ( CircleMap | d) holds f is being_homeomorphism by A2, A47;

            

             A51: the carrier of (TUC | Ui) = Ui by PRE_TOPC: 8;

            

             A52: (TT . i) < (TT . (i + 1)) by A19, A32, A46;

            then (TT . i) in SS by XXREAL_1: 1;

            then

             A53: [y, (TT . i)] in [:N, SS:] by A15, ZFMISC_1: 87;

            consider N2 be open Subset of Y, S be non empty Subset of I[01] , Fn be Function of [:(Y | N2), ( I[01] | S):], R^1 such that

             A54: S = [. 0 , (TT . i).] and

             A55: y in N2 and

             A56: N2 c= N and

             A57: Fn is continuous and

             A58: (F | [:N2, S:]) = ( CircleMap * Fn) and

             A59: (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]) by A31, A46;

            reconsider N2 as non empty open Subset of Y by A55;

            

             A60: the carrier of [:(Y | N2), ( I[01] | S):] = [:the carrier of (Y | N2), the carrier of ( I[01] | S):] by BORSUK_1:def 2;

            N2 c= N2;

            then

            reconsider N7 = N2 as non empty Subset of (Y | N2) by PRE_TOPC: 8;

            

             A61: ( dom Fn) = the carrier of [:(Y | N2), ( I[01] | S):] by FUNCT_2:def 1;

            

             A62: 0 <= (TT . i) by A19, A46;

            then

             A63: (TT . i) in S by A54, XXREAL_1: 1;

            then

            reconsider Ti = {(TT . i)} as non empty Subset of I[01] by ZFMISC_1: 31;

            

             A64: the carrier of ( I[01] | S) = S by PRE_TOPC: 8;

            then

            reconsider Ti2 = Ti as non empty Subset of ( I[01] | S) by A63, ZFMISC_1: 31;

            set FnT = (Fn | [:N2, Ti:]);

            

             A65: the carrier of [:(Y | N2), ( I[01] | Ti):] = [:the carrier of (Y | N2), the carrier of ( I[01] | Ti):] & ( rng FnT) c= REAL by BORSUK_1:def 2, TOPMETR: 17;

            

             A66: [:N2, SS:] c= [:N, SS:] by A56, ZFMISC_1: 96;

            

             A67: the carrier of (Y | N2) = N2 by PRE_TOPC: 8;

             {(TT . i)} c= S by A63, ZFMISC_1: 31;

            then

             A68: ( dom FnT) = [:N2, {(TT . i)}:] by A64, A60, A67, A61, RELAT_1: 62, ZFMISC_1: 96;

            

             A69: [:((Y | N2) | N7), (( I[01] | S) | Ti2):] = ( [:(Y | N2), ( I[01] | S):] | [:N7, Ti2:]) by BORSUK_3: 22;

            

             A70: the carrier of ( I[01] | Ti) = Ti by PRE_TOPC: 8;

            then

            reconsider FnT as Function of [:(Y | N2), ( I[01] | Ti):], R^1 by A67, A68, A65, FUNCT_2: 2;

            ((Y | N2) | N7) = (Y | N2) & (( I[01] | S) | Ti2) = ( I[01] | Ti) by GOBOARD9: 2;

            then

             A71: FnT is continuous by A57, A69, TOPMETR: 7;

            

             A72: (Fn . [y, (TT . i)]) in REAL by XREAL_0:def 1;

             [y, (TT . i)] in ( dom F) by A6, A63, ZFMISC_1: 87;

            then

             A73: (F . [y, (TT . i)]) in (F .: [:N, SS:]) by A53, FUNCT_2: 35;

            

             A74: [y, (TT . i)] in [:N2, S:] by A55, A63, ZFMISC_1: 87;

            

            then (F . [y, (TT . i)]) = (( CircleMap * Fn) . [y, (TT . i)]) by A58, FUNCT_1: 49

            .= ( CircleMap . (Fn . [y, (TT . i)])) by A64, A60, A67, A74, FUNCT_2: 15;

            then (Fn . [y, (TT . i)]) in ( CircleMap " Ui) by A48, A73, FUNCT_2: 38, TOPMETR: 17, A72;

            then

            consider Uit be set such that

             A75: (Fn . [y, (TT . i)]) in Uit and

             A76: Uit in D by A49, TARSKI:def 4;

            reconsider Uit as non empty Subset of R^1 by A75, A76;

            ( [#] R^1 ) <> {} & Uit is open by A76, TOPS_2:def 1;

            then (FnT " Uit) is open by A71, TOPS_2: 43;

            then

            consider SF be Subset-Family of [:(Y | N2), ( I[01] | Ti):] such that

             A77: (FnT " Uit) = ( union SF) and

             A78: for e be set st e in SF holds ex X1 be Subset of (Y | N2), Y1 be Subset of ( I[01] | Ti) st e = [:X1, Y1:] & X1 is open & Y1 is open by BORSUK_1: 5;

            

             A79: (TT . i) in {(TT . i)} by TARSKI:def 1;

            then

             A80: [y, (TT . i)] in [:N2, {(TT . i)}:] by A55, ZFMISC_1:def 2;

            then (FnT . [y, (TT . i)]) in Uit by A75, FUNCT_1: 49;

            then [y, (TT . i)] in (FnT " Uit) by A80, A68, FUNCT_1:def 7;

            then

            consider N5 be set such that

             A81: [y, (TT . i)] in N5 and

             A82: N5 in SF by A77, TARSKI:def 4;

            set f = ( CircleMap | Uit);

            

             A83: ( dom f) = Uit by Lm12, RELAT_1: 62, TOPMETR: 17;

            

             A84: ( rng f) c= Ui

            proof

              let b be object;

              assume b in ( rng f);

              then

              consider a be object such that

               A85: a in ( dom f) and

               A86: (f . a) = b by FUNCT_1:def 3;

              a in ( union D) by A76, A83, A85, TARSKI:def 4;

              then ( CircleMap . a) in Ui by A49, FUNCT_2: 38;

              hence thesis by A83, A85, A86, FUNCT_1: 49;

            end;

            consider X1 be Subset of (Y | N2), Y1 be Subset of ( I[01] | Ti) such that

             A87: N5 = [:X1, Y1:] and

             A88: X1 is open and Y1 is open by A78, A82;

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

            then

            reconsider f as Function of ( R^1 | Uit), (TUC | Ui) by A51, A83, A84, FUNCT_2: 2;

            consider NY be Subset of Y such that

             A89: NY is open and

             A90: (NY /\ ( [#] (Y | N2))) = X1 by A88, TOPS_2: 24;

            consider y1,y2 be object such that

             A91: y1 in X1 and

             A92: y2 in Y1 and

             A93: [y, (TT . i)] = [y1, y2] by A81, A87, ZFMISC_1:def 2;

            set N1 = (NY /\ N2);

            y = y1 by A93, XTUPLE_0: 1;

            then

             A94: y in NY by A90, A91, XBOOLE_0:def 4;

            then

            reconsider N1 as non empty open Subset of Y by A55, A89, XBOOLE_0:def 4;

            

             A95: N1 c= N2 by XBOOLE_1: 17;

            then [:N1, SS:] c= [:N2, SS:] by ZFMISC_1: 96;

            then [:N1, SS:] c= [:N, SS:] by A66;

            then

             A96: (F .: [:N1, SS:]) c= (F .: [:N, SS:]) by RELAT_1: 123;

            (TT . (i + 1)) <= 1 by A19, A32, A46;

            then

            reconsider SS as non empty Subset of I[01] by A25, A62, A52, XXREAL_1: 1;

            

             A97: ( dom (F | [:N1, SS:])) = [:N1, SS:] by A6, RELAT_1: 62, ZFMISC_1: 96;

            set Fni1 = ((f " ) * (F | [:N1, SS:]));

            (f " ) is being_homeomorphism by A50, A76, TOPS_2: 56;

            then

             A98: ( dom (f " )) = ( [#] (TUC | Ui));

            

             A99: ( rng (F | [:N1, SS:])) c= ( dom (f " ))

            proof

              let b be object;

              assume b in ( rng (F | [:N1, SS:]));

              then

              consider a be object such that

               A100: a in ( dom (F | [:N1, SS:])) and

               A101: ((F | [:N1, SS:]) . a) = b by FUNCT_1:def 3;

              b = (F . a) by A97, A100, A101, FUNCT_1: 49;

              then b in (F .: [:N1, SS:]) by A97, A100, FUNCT_2: 35;

              then b in (F .: [:N, SS:]) by A96;

              then b in Ui by A48;

              hence thesis by A98, PRE_TOPC: 8;

            end;

            then

             A102: ( dom Fni1) = ( dom (F | [:N1, SS:])) by RELAT_1: 27;

            set Fn2 = (Fn | [:N1, S:]);

            

             A103: the carrier of (Y | N1) = N1 by PRE_TOPC: 8;

            then

             A104: [:N1, S:] = the carrier of [:(Y | N1), ( I[01] | S):] by A64, BORSUK_1:def 2;

            then

             A105: ( dom Fn2) = the carrier of [:(Y | N1), ( I[01] | S):] by A64, A60, A67, A61, A95, RELAT_1: 62, ZFMISC_1: 96;

            reconsider ff = f as Function;

            

             A106: f is being_homeomorphism by A50, A76;

            then

             A107: f is one-to-one;

            

             A108: ( rng Fn2) c= R;

            the carrier of ( R^1 | Uit) is Subset of R^1 by TSEP_1: 1;

            then

             A109: ( rng Fni1) c= R by XBOOLE_1: 1;

            

             A110: the carrier of ( I[01] | SS) = SS by PRE_TOPC: 8;

            then

             A111: [:N1, SS:] = the carrier of [:(Y | N1), ( I[01] | SS):] by A103, BORSUK_1:def 2;

            then

            reconsider Fni1 as Function of [:(Y | N1), ( I[01] | SS):], R^1 by A97, A102, A109, FUNCT_2: 2;

            set Fn1 = (Fn2 +* Fni1);

            reconsider Fn2 as Function of [:(Y | N1), ( I[01] | S):], R^1 by A105, A108, FUNCT_2: 2;

            

             A112: ( rng Fn1) c= (( rng (Fn | [:N1, S:])) \/ ( rng Fni1)) by FUNCT_4: 17;

            ( dom (Fn | [:N1, S:])) = [:N1, S:] by A64, A60, A67, A61, A95, RELAT_1: 62, ZFMISC_1: 96;

            then

             A113: ( dom Fn1) = ( [:N1, S:] \/ [:N1, SS:]) by A97, A102, FUNCT_4:def 1;

            

             A114: ( rng f) = ( [#] (TUC | Ui)) by A106;

            then f is onto;

            then

             A115: (f " ) = (ff " ) by A107, TOPS_2:def 4;

            

             A116: Y1 = Ti

            proof

              thus Y1 c= Ti by A70;

              let a be object;

              assume a in Ti;

              then a = (TT . i) by TARSKI:def 1;

              hence thesis by A92, A93, XTUPLE_0: 1;

            end;

            

             A117: (Fn .: [:N1, {(TT . i)}:]) c= Uit

            proof

              let b be object;

              assume b in (Fn .: [:N1, {(TT . i)}:]);

              then

              consider a be Point of [:(Y | N2), ( I[01] | S):] such that

               A118: a in [:N1, {(TT . i)}:] and

               A119: (Fn . a) = b by FUNCT_2: 65;

              a in N5 by A87, A90, A116, A118, PRE_TOPC:def 5;

              then

               A120: a in ( union SF) by A82, TARSKI:def 4;

              then a in ( dom FnT) by A77, FUNCT_1:def 7;

              then (Fn . a) = (FnT . a) by FUNCT_1: 47;

              hence thesis by A77, A119, A120, FUNCT_1:def 7;

            end;

            

             A121: for p be set st p in (( [#] [:(Y | N1), ( I[01] | S):]) /\ ( [#] [:(Y | N1), ( I[01] | SS):])) holds (Fn2 . p) = (Fni1 . p)

            proof

              

               A122: the carrier of (Y | N2) = N2 by PRE_TOPC: 8;

              let p be set such that

               A123: p in (( [#] [:(Y | N1), ( I[01] | S):]) /\ ( [#] [:(Y | N1), ( I[01] | SS):]));

              

               A124: p in (( [#] [:(Y | N1), ( I[01] | SS):]) /\ ( [#] [:(Y | N1), ( I[01] | S):])) by A123;

              then

               A125: (Fn . p) = (Fn2 . p) by A104, FUNCT_1: 49;

              ( [:N1, S:] /\ [:N1, SS:]) = [:N1, (S /\ SS):] by ZFMISC_1: 99;

              then

               A126: p in [:N1, {(TT . i)}:] by A54, A62, A52, A111, A104, A123, XXREAL_1: 418;

              then

              consider p1 be Element of N1, p2 be Element of {(TT . i)} such that

               A127: p = [p1, p2] by DOMAIN_1: 1;

              

               A128: p1 in N1;

              (S /\ SS) = {(TT . i)} by A54, A62, A52, XXREAL_1: 418;

              then p2 in S by XBOOLE_0:def 4;

              then

               A129: p in [:N2, S:] by A95, A127, A128, ZFMISC_1:def 2;

              then

               A130: (Fn . p) in (Fn .: [:N1, {(TT . i)}:]) by A64, A60, A67, A126, FUNCT_2: 35;

              ((F | [:N1, SS:]) . p) = (F . p) by A111, A123, FUNCT_1: 49

              .= ((F | [:N2, S:]) . p) by A129, FUNCT_1: 49

              .= ( CircleMap . (Fn . p)) by A58, A64, A60, A61, A122, A129, FUNCT_1: 13

              .= (( CircleMap | Uit) . (Fn . p)) by A117, A130, FUNCT_1: 49

              .= (ff . (Fn2 . p)) by A104, A124, FUNCT_1: 49;

              

              hence (Fn2 . p) = ((ff " ) . ((F | [:N1, SS:]) . p)) by A117, A83, A107, A125, A130, FUNCT_1: 32

              .= (Fni1 . p) by A115, A97, A111, A123, FUNCT_1: 13;

            end;

            

             A131: [:N1, S:] c= [:N2, S:] by A95, ZFMISC_1: 96;

            then

            reconsider K0 = [:N1, S:] as Subset of [:(Y | N2), ( I[01] | S):] by A64, A60, PRE_TOPC: 8;

            

             A132: [:N1, SS:] c= ( dom F) by A6, ZFMISC_1: 96;

            reconsider gF = (F | [:N1, SS:]) as Function of [:(Y | N1), ( I[01] | SS):], TUC by A97, A99, A111, FUNCT_2: 2;

            reconsider fF = (F | [:N1, SS:]) as Function of [:(Y | N1), ( I[01] | SS):], (TUC | Ui) by A98, A97, A99, A111, FUNCT_2: 2;

             [:(Y | N1), ( I[01] | SS):] = ( [:Y, I[01] :] | [:N1, SS:]) by BORSUK_3: 22;

            then gF is continuous by A3, TOPMETR: 7;

            then

             A133: fF is continuous by TOPMETR: 6;

            (f " ) is continuous by A106;

            then ((f " ) * fF) is continuous by A133;

            then

             A134: Fni1 is continuous by PRE_TOPC: 26;

            reconsider aN1 = N1 as non empty Subset of (Y | N2) by A95, PRE_TOPC: 8;

            S c= S;

            then

            reconsider aS = S as non empty Subset of ( I[01] | S) by PRE_TOPC: 8;

            ( [:(Y | N2), ( I[01] | S):] | K0) = [:((Y | N2) | aN1), (( I[01] | S) | aS):] by BORSUK_3: 22

            .= [:(Y | N1), (( I[01] | S) | aS):] by GOBOARD9: 2

            .= [:(Y | N1), ( I[01] | S):] by GOBOARD9: 2;

            then

             A135: Fn2 is continuous by A57, TOPMETR: 7;

            take N1;

            take S1 = (S \/ SS);

            

             A136: ( [:N1, S:] \/ [:N1, SS:]) = [:N1, S1:] by ZFMISC_1: 97;

            

             A137: the carrier of ( I[01] | S1) = S1 by PRE_TOPC: 8;

            then [:N1, S1:] = the carrier of [:(Y | N1), ( I[01] | S1):] by A103, BORSUK_1:def 2;

            then

            reconsider Fn1 as Function of [:(Y | N1), ( I[01] | S1):], R^1 by A136, A113, A112, FUNCT_2: 2, XBOOLE_1: 1;

            take Fn1;

            thus

             A138: S1 = [. 0 , (TT . (i + 1)).] by A54, A62, A52, XXREAL_1: 165;

             0 <= (TT . (i + 1)) by A19, A32;

            then 0 in S1 by A138, XXREAL_1: 1;

            then

             A139: { 0 } c= S1 by ZFMISC_1: 31;

            

             A140: ( dom (Fn1 | [:the carrier of Y, { 0 }:])) = (( dom Fn1) /\ [:the carrier of Y, { 0 }:]) by RELAT_1: 61;

            

            then

             A141: ( dom (Fn1 | [:the carrier of Y, { 0 }:])) = [:(N1 /\ the carrier of Y), (S1 /\ { 0 }):] by A136, A113, ZFMISC_1: 100

            .= [:N1, (S1 /\ { 0 }):] by XBOOLE_1: 28

            .= [:N1, { 0 }:] by A139, XBOOLE_1: 28;

            

             A142: for a be object st a in ( dom (Fn1 | [:the carrier of Y, { 0 }:])) holds ((Fn1 | [:the carrier of Y, { 0 }:]) . a) = ((Ft | [:N1, I:]) . a)

            proof

              let a be object;

              

               A143: [:N1, I:] c= [:N2, I:] by A95, ZFMISC_1: 96;

              assume

               A144: a in ( dom (Fn1 | [:the carrier of Y, { 0 }:]));

              then

               A145: a in [:the carrier of Y, { 0 }:] by A140, XBOOLE_0:def 4;

              then

              consider a1,a2 be object such that a1 in the carrier of Y and

               A146: a2 in { 0 } and

               A147: a = [a1, a2] by ZFMISC_1:def 2;

              

               A148: a2 = 0 by A146, TARSKI:def 1;

               0 in S by A54, A62, XXREAL_1: 1;

              then { 0 } c= S by ZFMISC_1: 31;

              then

               A149: [:N1, { 0 }:] c= [:N1, S:] by ZFMISC_1: 96;

              then

               A150: a in [:N1, S:] by A141, A144;

              

               A151: [:N1, S:] c= [:N1, I:] by ZFMISC_1: 96;

              then

               A152: a in [:N1, I:] by A150;

              per cases ;

                suppose

                 A153: not a in ( dom Fni1);

                

                thus ((Fn1 | [:the carrier of Y, { 0 }:]) . a) = (Fn1 . a) by A145, FUNCT_1: 49

                .= ((Fn | [:N1, S:]) . a) by A153, FUNCT_4: 11

                .= (Fn . a) by A141, A144, A149, FUNCT_1: 49

                .= ((Ft | [:N2, I:]) . a) by A59, A145, FUNCT_1: 49

                .= (Ft . a) by A152, A143, FUNCT_1: 49

                .= ((Ft | [:N1, I:]) . a) by A150, A151, FUNCT_1: 49;

              end;

                suppose

                 A154: a in ( dom Fni1);

                set e = ((Ft | [:N1, I:]) . a);

                a in [:N1, SS:] by A6, A102, A154, RELAT_1: 62, ZFMISC_1: 96;

                then

                consider b1,b2 be object such that

                 A155: b1 in N1 and

                 A156: b2 in SS and

                 A157: a = [b1, b2] by ZFMISC_1:def 2;

                a2 = b2 by A147, A157, XTUPLE_0: 1;

                then

                 A158: a2 = (TT . i) by A62, A148, A156, XXREAL_1: 1;

                a1 = b1 by A147, A157, XTUPLE_0: 1;

                then

                 A159: [a1, (TT . i)] in [:N1, S:] & [a1, (TT . i)] in [:N1, {(TT . i)}:] by A63, A79, A155, ZFMISC_1: 87;

                e = (Ft . a) by A150, A151, FUNCT_1: 49

                .= ((Ft | [:N2, I:]) . a) by A152, A143, FUNCT_1: 49

                .= (Fn . a) by A59, A145, FUNCT_1: 49;

                then

                 A160: e in (Fn .: [:N1, {(TT . i)}:]) by A64, A60, A67, A61, A131, A147, A158, A159, FUNCT_1:def 6;

                

                then

                 A161: (ff . e) = ( CircleMap . e) by A117, FUNCT_1: 49

                .= ( CircleMap . (Ft . a)) by A150, A151, FUNCT_1: 49

                .= (( CircleMap * Ft) . a) by A8, A145, FUNCT_1: 13

                .= (F . a) by A5, A145, FUNCT_1: 49;

                

                thus ((Fn1 | [:the carrier of Y, { 0 }:]) . a) = (Fn1 . a) by A145, FUNCT_1: 49

                .= (Fni1 . a) by A154, FUNCT_4: 13

                .= ((ff " ) . ((F | [:N1, SS:]) . a)) by A115, A102, A154, FUNCT_1: 13

                .= ((ff " ) . (F . a)) by A97, A102, A154, FUNCT_1: 49

                .= ((Ft | [:N1, I:]) . a) by A117, A83, A107, A160, A161, FUNCT_1: 32;

              end;

            end;

            

             A162: ( rng Fn1) c= ( dom CircleMap ) by Lm12, TOPMETR: 17;

            then

             A163: ( dom ( CircleMap * Fn1)) = ( dom Fn1) by RELAT_1: 27;

            

             A164: for a be object st a in ( dom ( CircleMap * Fn1)) holds (( CircleMap * Fn1) . a) = (F . a)

            proof

              let a be object such that

               A165: a in ( dom ( CircleMap * Fn1));

              per cases ;

                suppose

                 A166: a in ( dom Fni1);

                

                 A167: [:N1, SS:] c= [:the carrier of Y, I:] by ZFMISC_1: 96;

                

                 A168: a in [:N1, SS:] by A6, A102, A166, RELAT_1: 62, ZFMISC_1: 96;

                then (F . a) in (F .: [:N1, SS:]) by A6, A167, FUNCT_1:def 6;

                then

                 A169: (F . a) in (F .: [:N, SS:]) by A96;

                then a in (F " ( dom (ff " ))) by A6, A48, A51, A98, A115, A168, A167, FUNCT_1:def 7;

                then

                 A170: a in ( dom ((ff " ) * F)) by RELAT_1: 147;

                

                thus (( CircleMap * Fn1) . a) = ( CircleMap . (Fn1 . a)) by A165, FUNCT_2: 15

                .= ( CircleMap . (Fni1 . a)) by A166, FUNCT_4: 13

                .= ( CircleMap . ((f " ) . ((F | [:N1, SS:]) . a))) by A102, A166, FUNCT_1: 13

                .= ( CircleMap . ((f " ) . (F . a))) by A97, A102, A166, FUNCT_1: 49

                .= ( CircleMap . (((ff " ) * F) . a)) by A132, A115, A97, A102, A166, FUNCT_1: 13

                .= (( CircleMap * ((ff " ) * F)) . a) by A170, FUNCT_1: 13

                .= ((( CircleMap * (ff " )) * F) . a) by RELAT_1: 36

                .= (( CircleMap * (ff " )) . (F . a)) by A132, A97, A102, A166, FUNCT_1: 13

                .= (F . a) by A48, A51, A114, A107, A169, TOPALG_3: 2;

              end;

                suppose

                 A171: not a in ( dom Fni1);

                then

                 A172: a in [:N1, S:] by A97, A102, A113, A163, A165, XBOOLE_0:def 3;

                

                thus (( CircleMap * Fn1) . a) = ( CircleMap . (Fn1 . a)) by A165, FUNCT_2: 15

                .= ( CircleMap . ((Fn | [:N1, S:]) . a)) by A171, FUNCT_4: 11

                .= ( CircleMap . (Fn . a)) by A172, FUNCT_1: 49

                .= (( CircleMap * Fn) . a) by A64, A60, A67, A131, A172, FUNCT_2: 15

                .= (F . a) by A58, A131, A172, FUNCT_1: 49;

              end;

            end;

            

             A173: S c= S1 by XBOOLE_1: 7;

            then

             A174: ( [#] ( I[01] | S1)) = the carrier of ( I[01] | S1) & ( I[01] | S) is SubSpace of ( I[01] | S1) by A64, A137, TSEP_1: 4;

            

             A175: SS c= S1 by XBOOLE_1: 7;

            then

            reconsider F1 = ( [#] ( I[01] | S)), F2 = ( [#] ( I[01] | SS)) as Subset of ( I[01] | S1) by A137, A173, PRE_TOPC: 8;

            reconsider hS = F1, hSS = F2 as Subset of I[01] by PRE_TOPC: 8;

            hS is closed by A54, BORSUK_4: 23, PRE_TOPC: 8;

            then

             A176: F1 is closed by TSEP_1: 8;

            thus y in N1 by A55, A94, XBOOLE_0:def 4;

            thus N1 c= N by A56, A95;

            hSS is closed by BORSUK_4: 23, PRE_TOPC: 8;

            then

             A177: F2 is closed by TSEP_1: 8;

            ( I[01] | SS) is SubSpace of ( I[01] | S1) by A110, A137, A175, TSEP_1: 4;

            then ex h be Function of [:(Y | N1), ( I[01] | S1):], R^1 st h = (Fn2 +* Fni1) & h is continuous by A64, A110, A137, A174, A176, A177, A135, A134, A121, TOPALG_3: 19;

            hence Fn1 is continuous;

            ( dom Fn1) = (( dom F) /\ [:N1, S1:]) by A6, A136, A113, XBOOLE_1: 28, ZFMISC_1: 96;

            hence (F | [:N1, S1:]) = ( CircleMap * Fn1) by A162, A164, FUNCT_1: 46, RELAT_1: 27;

            ( dom (Ft | [:N1, I:])) = (( dom Ft) /\ [:N1, I:]) by RELAT_1: 61

            .= [:(the carrier of Y /\ N1), ( { 0 } /\ I):] by A8, ZFMISC_1: 100

            .= [:N1, ( { 0 } /\ I):] by XBOOLE_1: 28

            .= [:N1, { 0 }:] by Lm3, XBOOLE_1: 28;

            hence thesis by A141, A142;

          end;

        end;

        

         A178: N[ 0 ] by FINSEQ_3: 24;

        for i be Nat holds N[i] from NAT_1:sch 2( A178, A30);

        then

        consider N2 be non empty open Subset of Y, S be non empty Subset of I[01] , Fn1 be Function of [:(Y | N2), ( I[01] | S):], R^1 such that

         A179: S = [. 0 , (TT . ( len TT)).] and

         A180: y in N2 and

         A181: N2 c= N and

         A182: Fn1 is continuous and

         A183: (F | [:N2, S:]) = ( CircleMap * Fn1) and

         A184: (Fn1 | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]) by A17;

        (Fn1 . x) in REAL by XREAL_0:def 1;

        then

        reconsider z = (Fn1 . x) as Point of R^1 by TOPMETR: 17;

        

         A185: ( I[01] | S) = I[01] by A12, A179, Lm6, BORSUK_1: 40, TSEP_1: 3;

        then

        reconsider Fn1 as Function of [:(Y | N2), I[01] :], R^1 ;

        take z, y, t, N2;

        take Fn1;

        thus x = [y, t] & z = (Fn1 . x) & y in N2 & Fn1 is continuous & (F | [:N2, I:]) = ( CircleMap * Fn1) & (Fn1 | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]) by A10, A12, A179, A180, A182, A183, A184, A185, BORSUK_1: 40;

        let H be Function of [:(Y | N2), I[01] :], R^1 such that

         A186: H is continuous and

         A187: (F | [:N2, I:]) = ( CircleMap * H) and

         A188: (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]);

        defpred M[ Nat] means $1 in ( dom TT) implies ex Z be non empty Subset of I[01] st Z = [. 0 , (TT . $1).] & (Fn1 | [:N2, Z:]) = (H | [:N2, Z:]);

        

         A189: ( dom Fn1) = the carrier of [:(Y | N2), I[01] :] by FUNCT_2:def 1;

        

         A190: the carrier of [:(Y | N2), I[01] :] = [:the carrier of (Y | N2), I:] & the carrier of (Y | N2) = N2 by BORSUK_1:def 2, PRE_TOPC: 8;

        

         A191: ( dom H) = the carrier of [:(Y | N2), I[01] :] by FUNCT_2:def 1;

        

         A192: for i be Nat st M[i] holds M[(i + 1)]

        proof

          let i be Nat such that

           A193: M[i] and

           A194: (i + 1) in ( dom TT);

          per cases by A194, TOPREALA: 2;

            suppose

             A195: i = 0 ;

            set Z = [. 0 , (TT . (i + 1)).];

            

             A196: Z = { 0 } by A11, A195, XXREAL_1: 17;

            reconsider Z as non empty Subset of I[01] by A11, A195, Lm3, XXREAL_1: 17;

            

             A197: [:N2, Z:] c= [:N2, I:] by ZFMISC_1: 95;

            then

             A198: ( dom (Fn1 | [:N2, Z:])) = [:N2, Z:] by A190, A189, RELAT_1: 62;

            

             A199: for x be object st x in ( dom (Fn1 | [:N2, Z:])) holds ((Fn1 | [:N2, Z:]) . x) = ((H | [:N2, Z:]) . x)

            proof

              let x be object;

              

               A200: [:N2, Z:] c= [:the carrier of Y, Z:] by ZFMISC_1: 95;

              assume

               A201: x in ( dom (Fn1 | [:N2, Z:]));

              

              hence ((Fn1 | [:N2, Z:]) . x) = (Fn1 . x) by A198, FUNCT_1: 49

              .= ((Fn1 | [:the carrier of Y, { 0 }:]) . x) by A196, A198, A201, A200, FUNCT_1: 49

              .= (H . x) by A184, A188, A196, A198, A201, A200, FUNCT_1: 49

              .= ((H | [:N2, Z:]) . x) by A198, A201, FUNCT_1: 49;

            end;

            take Z;

            thus Z = [. 0 , (TT . (i + 1)).];

            ( dom (H | [:N2, Z:])) = [:N2, Z:] by A191, A190, A197, RELAT_1: 62;

            hence thesis by A189, A199, RELAT_1: 62;

          end;

            suppose

             A202: i in ( dom TT);

            set ZZ = [.(TT . i), (TT . (i + 1)).];

            

             A203: 0 <= (TT . i) by A19, A202;

            

             A204: (TT . (i + 1)) <= 1 by A19, A194, A202;

            then

            reconsider ZZ as Subset of I[01] by A25, A203;

            consider Z be non empty Subset of I[01] such that

             A205: Z = [. 0 , (TT . i).] and

             A206: (Fn1 | [:N2, Z:]) = (H | [:N2, Z:]) by A193, A202;

            take Z1 = (Z \/ ZZ);

            

             A207: (TT . i) < (TT . (i + 1)) by A19, A194, A202;

            hence Z1 = [. 0 , (TT . (i + 1)).] by A205, A203, XXREAL_1: 165;

            

             A208: [:N2, Z1:] c= [:N2, I:] by ZFMISC_1: 95;

            then

             A209: ( dom (Fn1 | [:N2, Z1:])) = [:N2, Z1:] by A190, A189, RELAT_1: 62;

            

             A210: for x be object st x in ( dom (Fn1 | [:N2, Z1:])) holds ((Fn1 | [:N2, Z1:]) . x) = ((H | [:N2, Z1:]) . x)

            proof

               0 <= (TT . (i + 1)) by A19, A194;

              then

               A211: (TT . (i + 1)) is Point of I[01] by A204, BORSUK_1: 43;

               0 <= (TT . i) & (TT . i) <= 1 by A19, A194, A202;

              then (TT . i) is Point of I[01] by BORSUK_1: 43;

              then

               A212: ZZ is connected by A207, A211, BORSUK_4: 24;

              consider Ui be non empty Subset of TUC such that

               A213: Ui in UL and

               A214: (F .: [:N, ZZ:]) c= Ui by A16, A194, A202;

              consider D be mutually-disjoint open Subset-Family of R^1 such that

               A215: ( union D) = ( CircleMap " Ui) and

               A216: for d be Subset of R^1 st d in D holds for f be Function of ( R^1 | d), (TUC | Ui) st f = ( CircleMap | d) holds f is being_homeomorphism by A2, A213;

              let x be object such that

               A217: x in ( dom (Fn1 | [:N2, Z1:]));

              consider x1,x2 be object such that

               A218: x1 in N2 and

               A219: x2 in Z1 and

               A220: x = [x1, x2] by A209, A217, ZFMISC_1:def 2;

              

               A221: (TT . i) in ZZ by A207, XXREAL_1: 1;

              then [x1, (TT . i)] in [:N, ZZ:] by A181, A218, ZFMISC_1: 87;

              then

               A222: (F . [x1, (TT . i)]) in (F .: [:N, ZZ:]) by FUNCT_2: 35;

              reconsider xy = {x1} as non empty Subset of Y by A218, ZFMISC_1: 31;

              

               A223: xy c= N2 by A218, ZFMISC_1: 31;

              then

              reconsider xZZ = [:xy, ZZ:] as Subset of [:(Y | N2), I[01] :] by A190, ZFMISC_1: 96;

              

               A224: ( dom (H | [:xy, ZZ:])) = [:xy, ZZ:] by A191, A190, A223, RELAT_1: 62, ZFMISC_1: 96;

              

               A225: D is Cover of (Fn1 .: xZZ)

              proof

                let b be object;

                

                 A226: [:N, ZZ:] c= [:the carrier of Y, I:] by ZFMISC_1: 96;

                assume b in (Fn1 .: xZZ);

                then

                consider a be Point of [:(Y | N2), I[01] :] such that

                 A227: a in xZZ and

                 A228: (Fn1 . a) = b by FUNCT_2: 65;

                xy c= N by A181, A218, ZFMISC_1: 31;

                then [:xy, ZZ:] c= [:N, ZZ:] by ZFMISC_1: 95;

                then a in [:N, ZZ:] by A227;

                then

                 A229: (F . a) in (F .: [:N, ZZ:]) by A6, A226, FUNCT_1:def 6;

                ( CircleMap . (Fn1 . a)) = (( CircleMap * Fn1) . a) by FUNCT_2: 15

                .= (F . a) by A12, A179, A183, A190, BORSUK_1: 40, FUNCT_1: 49;

                hence b in ( union D) by A214, A215, A228, A229, Lm12, FUNCT_1:def 7, TOPMETR: 17;

              end;

              

               A230: D is Cover of (H .: xZZ)

              proof

                let b be object;

                

                 A231: [:N, ZZ:] c= [:the carrier of Y, I:] by ZFMISC_1: 96;

                assume b in (H .: xZZ);

                then

                consider a be Point of [:(Y | N2), I[01] :] such that

                 A232: a in xZZ and

                 A233: (H . a) = b by FUNCT_2: 65;

                

                 A234: ( CircleMap . (H . a)) = (( CircleMap * H) . a) by FUNCT_2: 15

                .= (F . a) by A187, A190, FUNCT_1: 49;

                xy c= N by A181, A218, ZFMISC_1: 31;

                then [:xy, ZZ:] c= [:N, ZZ:] by ZFMISC_1: 95;

                then a in [:N, ZZ:] by A232;

                then (F . a) in (F .: [:N, ZZ:]) by A6, A231, FUNCT_1:def 6;

                hence b in ( union D) by A214, A215, A233, A234, Lm12, FUNCT_1:def 7, TOPMETR: 17;

              end;

              

               A235: (H . [x1, (TT . i)]) in REAL by XREAL_0:def 1;

              (TT . i) in Z by A205, A203, XXREAL_1: 1;

              then

               A236: [x1, (TT . i)] in [:N2, Z:] by A218, ZFMISC_1: 87;

              

              then

               A237: (Fn1 . [x1, (TT . i)]) = ((Fn1 | [:N2, Z:]) . [x1, (TT . i)]) by FUNCT_1: 49

              .= (H . [x1, (TT . i)]) by A206, A236, FUNCT_1: 49;

              

               A238: [:N2, Z:] c= [:N2, I:] by ZFMISC_1: 95;

              

              then (F . [x1, (TT . i)]) = (( CircleMap * H) . [x1, (TT . i)]) by A187, A236, FUNCT_1: 49

              .= ( CircleMap . (H . [x1, (TT . i)])) by A191, A190, A236, A238, FUNCT_1: 13;

              then (H . [x1, (TT . i)]) in ( CircleMap " Ui) by A214, A222, FUNCT_2: 38, A235, TOPMETR: 17;

              then

              consider Uith be set such that

               A239: (H . [x1, (TT . i)]) in Uith and

               A240: Uith in D by A215, TARSKI:def 4;

              

               A241: (Fn1 . [x1, (TT . i)]) in REAL by XREAL_0:def 1;

              (F . [x1, (TT . i)]) = (( CircleMap * Fn1) . [x1, (TT . i)]) by A12, A179, A183, A236, A238, BORSUK_1: 40, FUNCT_1: 49

              .= ( CircleMap . (Fn1 . [x1, (TT . i)])) by A190, A189, A236, A238, FUNCT_1: 13;

              then (Fn1 . [x1, (TT . i)]) in ( CircleMap " Ui) by A214, A222, FUNCT_2: 38, A241, TOPMETR: 17;

              then

              consider Uit be set such that

               A242: (Fn1 . [x1, (TT . i)]) in Uit and

               A243: Uit in D by A215, TARSKI:def 4;

               I[01] is SubSpace of I[01] by TSEP_1: 2;

              then

               A244: [:(Y | N2), I[01] :] is SubSpace of [:Y, I[01] :] by BORSUK_3: 21;

              xy is connected by A218;

              then [:xy, ZZ:] is connected by A212, TOPALG_3: 16;

              then

               A245: xZZ is connected by A244, CONNSP_1: 23;

              reconsider Uith as non empty Subset of R^1 by A239, A240;

              

               A246: x1 in xy by TARSKI:def 1;

              then

               A247: [x1, (TT . i)] in xZZ by A221, ZFMISC_1: 87;

              then (H . [x1, (TT . i)]) in (H .: xZZ) by FUNCT_2: 35;

              then Uith meets (H .: xZZ) by A239, XBOOLE_0: 3;

              then

               A248: (H .: xZZ) c= Uith by A186, A245, A240, A230, TOPALG_3: 12, TOPS_2: 61;

              reconsider Uit as non empty Subset of R^1 by A242, A243;

              set f = ( CircleMap | Uit);

              

               A249: ( dom f) = Uit by Lm12, RELAT_1: 62, TOPMETR: 17;

              

               A250: ( rng f) c= Ui

              proof

                let b be object;

                assume b in ( rng f);

                then

                consider a be object such that

                 A251: a in ( dom f) and

                 A252: (f . a) = b by FUNCT_1:def 3;

                a in ( union D) by A243, A249, A251, TARSKI:def 4;

                then ( CircleMap . a) in Ui by A215, FUNCT_2: 38;

                hence thesis by A249, A251, A252, FUNCT_1: 49;

              end;

              the carrier of (TUC | Ui) = Ui & the carrier of ( R^1 | Uit) = Uit by PRE_TOPC: 8;

              then

              reconsider f as Function of ( R^1 | Uit), (TUC | Ui) by A249, A250, FUNCT_2: 2;

              

               A253: ( dom (Fn1 | [:xy, ZZ:])) = [:xy, ZZ:] by A190, A189, A223, RELAT_1: 62, ZFMISC_1: 96;

              (H . [x1, (TT . i)]) in (H .: xZZ) by A191, A247, FUNCT_1:def 6;

              then Uit meets Uith by A242, A248, A237, XBOOLE_0: 3;

              then

               A254: Uit = Uith by A243, A240, TAXONOM2:def 5;

              

               A255: ( rng (H | [:xy, ZZ:])) c= ( dom f)

              proof

                let b be object;

                assume b in ( rng (H | [:xy, ZZ:]));

                then

                consider a be object such that

                 A256: a in ( dom (H | [:xy, ZZ:])) and

                 A257: ((H | [:xy, ZZ:]) . a) = b by FUNCT_1:def 3;

                (H . a) = b by A224, A256, A257, FUNCT_1: 49;

                then b in (H .: xZZ) by A191, A224, A256, FUNCT_1:def 6;

                hence thesis by A248, A254, A249;

              end;

              (Fn1 . [x1, (TT . i)]) in (Fn1 .: xZZ) by A247, FUNCT_2: 35;

              then Uit meets (Fn1 .: xZZ) by A242, XBOOLE_0: 3;

              then

               A258: (Fn1 .: xZZ) c= Uit by A182, A185, A243, A245, A225, TOPALG_3: 12, TOPS_2: 61;

              

               A259: ( rng (Fn1 | [:xy, ZZ:])) c= ( dom f)

              proof

                let b be object;

                assume b in ( rng (Fn1 | [:xy, ZZ:]));

                then

                consider a be object such that

                 A260: a in ( dom (Fn1 | [:xy, ZZ:])) and

                 A261: ((Fn1 | [:xy, ZZ:]) . a) = b by FUNCT_1:def 3;

                (Fn1 . a) = b by A253, A260, A261, FUNCT_1: 49;

                then b in (Fn1 .: xZZ) by A189, A253, A260, FUNCT_1:def 6;

                hence thesis by A258, A249;

              end;

              then

               A262: ( dom (f * (Fn1 | [:xy, ZZ:]))) = ( dom (Fn1 | [:xy, ZZ:])) by RELAT_1: 27;

              

               A263: for x be object st x in ( dom (f * (Fn1 | [:xy, ZZ:]))) holds ((f * (Fn1 | [:xy, ZZ:])) . x) = ((f * (H | [:xy, ZZ:])) . x)

              proof

                let x be object such that

                 A264: x in ( dom (f * (Fn1 | [:xy, ZZ:])));

                

                 A265: (Fn1 . x) in (Fn1 .: [:xy, ZZ:]) by A189, A253, A262, A264, FUNCT_1:def 6;

                

                 A266: (H . x) in (H .: [:xy, ZZ:]) by A191, A253, A262, A264, FUNCT_1:def 6;

                

                thus ((f * (Fn1 | [:xy, ZZ:])) . x) = (((f * Fn1) | [:xy, ZZ:]) . x) by RELAT_1: 83

                .= ((f * Fn1) . x) by A253, A262, A264, FUNCT_1: 49

                .= (f . (Fn1 . x)) by A189, A264, FUNCT_1: 13

                .= ( CircleMap . (Fn1 . x)) by A258, A265, FUNCT_1: 49

                .= (( CircleMap * Fn1) . x) by A189, A264, FUNCT_1: 13

                .= ( CircleMap . (H . x)) by A12, A179, A183, A187, A191, A264, BORSUK_1: 40, FUNCT_1: 13

                .= (f . (H . x)) by A248, A254, A266, FUNCT_1: 49

                .= ((f * H) . x) by A191, A264, FUNCT_1: 13

                .= (((f * H) | [:xy, ZZ:]) . x) by A253, A262, A264, FUNCT_1: 49

                .= ((f * (H | [:xy, ZZ:])) . x) by RELAT_1: 83;

              end;

              f is being_homeomorphism by A216, A243;

              then

               A267: f is one-to-one;

              ( dom (f * (H | [:xy, ZZ:]))) = ( dom (H | [:xy, ZZ:])) by A255, RELAT_1: 27;

              then

               A268: (f * (Fn1 | [:xy, ZZ:])) = (f * (H | [:xy, ZZ:])) by A253, A224, A259, A263, RELAT_1: 27;

              per cases ;

                suppose x2 in ZZ;

                then

                 A269: x in [:xy, ZZ:] by A220, A246, ZFMISC_1: 87;

                

                thus ((Fn1 | [:N2, Z1:]) . x) = (Fn1 . x) by A209, A217, FUNCT_1: 49

                .= ((Fn1 | [:xy, ZZ:]) . x) by A269, FUNCT_1: 49

                .= ((H | [:xy, ZZ:]) . x) by A267, A253, A224, A259, A255, A268, FUNCT_1: 27

                .= (H . x) by A269, FUNCT_1: 49

                .= ((H | [:N2, Z1:]) . x) by A209, A217, FUNCT_1: 49;

              end;

                suppose not x2 in ZZ;

                then x2 in Z by A219, XBOOLE_0:def 3;

                then

                 A270: x in [:N2, Z:] by A218, A220, ZFMISC_1: 87;

                

                thus ((Fn1 | [:N2, Z1:]) . x) = (Fn1 . x) by A209, A217, FUNCT_1: 49

                .= ((Fn1 | [:N2, Z:]) . x) by A270, FUNCT_1: 49

                .= (H . x) by A206, A270, FUNCT_1: 49

                .= ((H | [:N2, Z1:]) . x) by A209, A217, FUNCT_1: 49;

              end;

            end;

            ( dom (H | [:N2, Z1:])) = [:N2, Z1:] by A191, A190, A208, RELAT_1: 62;

            hence thesis by A189, A210, RELAT_1: 62;

          end;

        end;

        

         A271: M[ 0 ] by FINSEQ_3: 24;

        for i be Nat holds M[i] from NAT_1:sch 2( A271, A192);

        then

        consider Z be non empty Subset of I[01] such that

         A272: Z = [. 0 , (TT . ( len TT)).] and

         A273: (Fn1 | [:N2, Z:]) = (H | [:N2, Z:]) by A17;

        

        thus Fn1 = (Fn1 | [:N2, Z:]) by A12, A190, A189, A272, BORSUK_1: 40, RELAT_1: 69

        .= H by A12, A191, A190, A272, A273, BORSUK_1: 40, RELAT_1: 69;

      end;

      consider G be Function of [:Y, I[01] :], R^1 such that

       A274: for x be Point of [:Y, I[01] :] holds A[x, (G . x)] from FUNCT_2:sch 3( A9);

      take G;

       A275:

      now

        let N be Subset of Y, F be Function of [:(Y | N), I[01] :], R^1 ;

        

        thus ( dom F) = the carrier of [:(Y | N), I[01] :] by FUNCT_2:def 1

        .= [:the carrier of (Y | N), I:] by BORSUK_1:def 2

        .= [:N, I:] by PRE_TOPC: 8;

      end;

      

       A276: for p be Point of [:Y, I[01] :], y be Point of Y, t be Point of I[01] , N1,N2 be non empty open Subset of Y, Fn1 be Function of [:(Y | N1), I[01] :], R^1 , Fn2 be Function of [:(Y | N2), I[01] :], R^1 st p = [y, t] & y in N1 & y in N2 & Fn2 is continuous & Fn1 is continuous & (F | [:N2, I:]) = ( CircleMap * Fn2) & (Fn2 | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]) & (F | [:N1, I:]) = ( CircleMap * Fn1) & (Fn1 | [:the carrier of Y, { 0 }:]) = (Ft | [:N1, I:]) holds (Fn1 | [: {y}, I:]) = (Fn2 | [: {y}, I:])

      proof

        let p be Point of [:Y, I[01] :], y be Point of Y, t be Point of I[01] , N1,N2 be non empty open Subset of Y, Fn1 be Function of [:(Y | N1), I[01] :], R^1 , Fn2 be Function of [:(Y | N2), I[01] :], R^1 such that p = [y, t] and

         A277: y in N1 and

         A278: y in N2 and

         A279: Fn2 is continuous and

         A280: Fn1 is continuous and

         A281: (F | [:N2, I:]) = ( CircleMap * Fn2) and

         A282: (Fn2 | [:the carrier of Y, { 0 }:]) = (Ft | [:N2, I:]) and

         A283: (F | [:N1, I:]) = ( CircleMap * Fn1) and

         A284: (Fn1 | [:the carrier of Y, { 0 }:]) = (Ft | [:N1, I:]);

        

         A285: {y} c= N1 by A277, ZFMISC_1: 31;

        consider TT be non empty FinSequence of REAL such that

         A286: (TT . 1) = 0 and

         A287: (TT . ( len TT)) = 1 and

         A288: TT is increasing and

         A289: ex N be open Subset of Y st y in N & for i be Nat st i in ( dom TT) & (i + 1) in ( dom TT) holds ex Ui be non empty Subset of ( Tunit_circle 2) st Ui in UL & (F .: [:N, [.(TT . i), (TT . (i + 1)).]:]) c= Ui by A3, A1, Th21;

        consider N be open Subset of Y such that

         A290: y in N and

         A291: for i be Nat st i in ( dom TT) & (i + 1) in ( dom TT) holds ex Ui be non empty Subset of ( Tunit_circle 2) st Ui in UL & (F .: [:N, [.(TT . i), (TT . (i + 1)).]:]) c= Ui by A289;

        reconsider N as non empty open Subset of Y by A290;

        defpred M[ Nat] means $1 in ( dom TT) implies ex Z be non empty Subset of I[01] st Z = [. 0 , (TT . $1).] & (Fn1 | [: {y}, Z:]) = (Fn2 | [: {y}, Z:]);

        

         A292: ( len TT) in ( dom TT) by FINSEQ_5: 6;

        

         A293: ( dom Fn2) = the carrier of [:(Y | N2), I[01] :] by FUNCT_2:def 1;

        

         A294: ( dom Fn2) = [:N2, I:] by A275;

        

         A295: {y} c= N2 by A278, ZFMISC_1: 31;

        

         A296: the carrier of [:(Y | N1), I[01] :] = [:the carrier of (Y | N1), I:] & the carrier of (Y | N1) = N1 by BORSUK_1:def 2, PRE_TOPC: 8;

        

         A297: the carrier of [:(Y | N2), I[01] :] = [:the carrier of (Y | N2), I:] & the carrier of (Y | N2) = N2 by BORSUK_1:def 2, PRE_TOPC: 8;

        

         A298: ( dom Fn1) = [:N1, I:] by A275;

        

         A299: ( dom Fn1) = the carrier of [:(Y | N1), I[01] :] by FUNCT_2:def 1;

        

         A300: 1 in ( dom TT) by FINSEQ_5: 6;

        

         A301: for i be Nat st M[i] holds M[(i + 1)]

        proof

          let i be Nat such that

           A302: M[i] and

           A303: (i + 1) in ( dom TT);

          per cases by A303, TOPREALA: 2;

            suppose

             A304: i = 0 ;

            set Z = [. 0 , (TT . (i + 1)).];

            

             A305: Z = { 0 } by A286, A304, XXREAL_1: 17;

            reconsider Z as non empty Subset of I[01] by A286, A304, Lm3, XXREAL_1: 17;

            

             A306: [: {y}, Z:] c= [:N2, I:] by A295, ZFMISC_1: 96;

            

             A307: ( dom (Fn1 | [: {y}, Z:])) = [: {y}, Z:] by A285, A298, RELAT_1: 62, ZFMISC_1: 96;

            

             A308: [: {y}, Z:] c= [:N1, I:] by A285, ZFMISC_1: 96;

            

             A309: for x be object st x in ( dom (Fn1 | [: {y}, Z:])) holds ((Fn1 | [: {y}, Z:]) . x) = ((Fn2 | [: {y}, Z:]) . x)

            proof

              let x be object;

              

               A310: [: {y}, Z:] c= [:the carrier of Y, Z:] by ZFMISC_1: 95;

              assume

               A311: x in ( dom (Fn1 | [: {y}, Z:]));

              

              hence ((Fn1 | [: {y}, Z:]) . x) = (Fn1 . x) by A307, FUNCT_1: 49

              .= ((Fn1 | [:the carrier of Y, { 0 }:]) . x) by A305, A307, A311, A310, FUNCT_1: 49

              .= (Ft . x) by A284, A308, A307, A311, FUNCT_1: 49

              .= ((Ft | [:N2, I:]) . x) by A307, A306, A311, FUNCT_1: 49

              .= (Fn2 . x) by A282, A305, A307, A311, A310, FUNCT_1: 49

              .= ((Fn2 | [: {y}, Z:]) . x) by A307, A311, FUNCT_1: 49;

            end;

            take Z;

            thus Z = [. 0 , (TT . (i + 1)).];

            ( dom (Fn2 | [: {y}, Z:])) = [: {y}, Z:] by A295, A294, RELAT_1: 62, ZFMISC_1: 96;

            hence thesis by A307, A309;

          end;

            suppose

             A312: i in ( dom TT);

             A313:

            now

              let i be Element of NAT such that

               A314: i in ( dom TT);

              1 <= i by A314, FINSEQ_3: 25;

              then 1 = i or 1 < i by XXREAL_0: 1;

              hence

               A315: 0 <= (TT . i) by A286, A288, A300, A314, SEQM_3:def 1;

              assume

               A316: (i + 1) in ( dom TT);

              

               A317: (i + 0 ) < (i + 1) by XREAL_1: 8;

              hence

               A318: (TT . i) < (TT . (i + 1)) by A288, A314, A316, SEQM_3:def 1;

              (i + 1) <= ( len TT) by A316, FINSEQ_3: 25;

              then (i + 1) = ( len TT) or (i + 1) < ( len TT) by XXREAL_0: 1;

              hence (TT . (i + 1)) <= 1 by A287, A288, A292, A316, SEQM_3:def 1;

              hence (TT . i) < 1 by A318, XXREAL_0: 2;

              thus 0 < (TT . (i + 1)) by A288, A314, A315, A316, A317, SEQM_3:def 1;

            end;

            then

             A319: 0 <= (TT . i) by A312;

            

             A320: (TT . (i + 1)) <= 1 by A303, A312, A313;

            set ZZ = [.(TT . i), (TT . (i + 1)).];

            consider Z be non empty Subset of I[01] such that

             A321: Z = [. 0 , (TT . i).] and

             A322: (Fn1 | [: {y}, Z:]) = (Fn2 | [: {y}, Z:]) by A302, A312;

            now

              let i be Nat such that

               A323: 0 <= (TT . i) and

               A324: (TT . (i + 1)) <= 1;

              thus [.(TT . i), (TT . (i + 1)).] c= I

              proof

                let a be object;

                assume

                 A325: a in [.(TT . i), (TT . (i + 1)).];

                then

                reconsider a as Real;

                a <= (TT . (i + 1)) by A325, XXREAL_1: 1;

                then

                 A326: a <= 1 by A324, XXREAL_0: 2;

                 0 <= a by A323, A325, XXREAL_1: 1;

                hence thesis by A326, BORSUK_1: 43;

              end;

            end;

            then

            reconsider ZZ as Subset of I[01] by A319, A320;

            take Z1 = (Z \/ ZZ);

            

             A327: (TT . i) < (TT . (i + 1)) by A303, A312, A313;

            hence Z1 = [. 0 , (TT . (i + 1)).] by A321, A319, XXREAL_1: 165;

            

             A328: ( dom (Fn1 | [: {y}, Z1:])) = [: {y}, Z1:] by A285, A298, RELAT_1: 62, ZFMISC_1: 96;

            

             A329: for x be object st x in ( dom (Fn1 | [: {y}, Z1:])) holds ((Fn1 | [: {y}, Z1:]) . x) = ((Fn2 | [: {y}, Z1:]) . x)

            proof

               0 <= (TT . (i + 1)) by A303, A313;

              then

               A330: (TT . (i + 1)) is Point of I[01] by A320, BORSUK_1: 43;

               0 <= (TT . i) & (TT . i) <= 1 by A303, A312, A313;

              then (TT . i) is Point of I[01] by BORSUK_1: 43;

              then

               A331: ZZ is connected by A327, A330, BORSUK_4: 24;

              

               A332: (TT . i) in ZZ by A327, XXREAL_1: 1;

              consider Ui be non empty Subset of TUC such that

               A333: Ui in UL and

               A334: (F .: [:N, ZZ:]) c= Ui by A291, A303, A312;

              consider D be mutually-disjoint open Subset-Family of R^1 such that

               A335: ( union D) = ( CircleMap " Ui) and

               A336: for d be Subset of R^1 st d in D holds for f be Function of ( R^1 | d), (TUC | Ui) st f = ( CircleMap | d) holds f is being_homeomorphism by A2, A333;

              let x be object such that

               A337: x in ( dom (Fn1 | [: {y}, Z1:]));

              consider x1,x2 be object such that

               A338: x1 in {y} and

               A339: x2 in Z1 and

               A340: x = [x1, x2] by A328, A337, ZFMISC_1:def 2;

              reconsider xy = {x1} as non empty Subset of Y by A338, ZFMISC_1: 31;

              

               A341: xy c= N2 by A295, A338, ZFMISC_1: 31;

              then

               A342: [:xy, ZZ:] c= [:N2, I:] by ZFMISC_1: 96;

              

               A343: x1 = y by A338, TARSKI:def 1;

              then [x1, (TT . i)] in [:N, ZZ:] by A290, A332, ZFMISC_1: 87;

              then

               A344: (F . [x1, (TT . i)]) in (F .: [:N, ZZ:]) by FUNCT_2: 35;

              

               A345: xy c= N1 by A285, A338, ZFMISC_1: 31;

              then

              reconsider xZZ = [:xy, ZZ:] as Subset of [:(Y | N1), I[01] :] by A296, ZFMISC_1: 96;

              xy is connected by A338;

              then

               A346: [:xy, ZZ:] is connected by A331, TOPALG_3: 16;

              

               A347: xy c= N by A290, A343, ZFMISC_1: 31;

              

               A348: D is Cover of (Fn1 .: xZZ)

              proof

                let b be object;

                

                 A349: [:N, ZZ:] c= [:the carrier of Y, I:] by ZFMISC_1: 96;

                assume b in (Fn1 .: xZZ);

                then

                consider a be Point of [:(Y | N1), I[01] :] such that

                 A350: a in xZZ and

                 A351: (Fn1 . a) = b by FUNCT_2: 65;

                

                 A352: ( CircleMap . (Fn1 . a)) = (( CircleMap * Fn1) . a) by FUNCT_2: 15

                .= (F . a) by A283, A296, FUNCT_1: 49;

                 [:xy, ZZ:] c= [:N, ZZ:] by A347, ZFMISC_1: 95;

                then a in [:N, ZZ:] by A350;

                then (F . a) in (F .: [:N, ZZ:]) by A6, A349, FUNCT_1:def 6;

                hence b in ( union D) by A334, A335, A351, A352, Lm12, FUNCT_1:def 7, TOPMETR: 17;

              end;

              

               A353: I[01] is SubSpace of I[01] by TSEP_1: 2;

              then [:(Y | N1), I[01] :] is SubSpace of [:Y, I[01] :] by BORSUK_3: 21;

              then

               A354: xZZ is connected by A346, CONNSP_1: 23;

              reconsider XZZ = [:xy, ZZ:] as Subset of [:(Y | N2), I[01] :] by A297, A341, ZFMISC_1: 96;

               [:(Y | N2), I[01] :] is SubSpace of [:Y, I[01] :] by A353, BORSUK_3: 21;

              then

               A355: XZZ is connected by A346, CONNSP_1: 23;

              

               A356: D is Cover of (Fn2 .: xZZ)

              proof

                let b be object;

                

                 A357: [:N, ZZ:] c= [:the carrier of Y, I:] by ZFMISC_1: 96;

                assume b in (Fn2 .: xZZ);

                then

                consider a be Point of [:(Y | N2), I[01] :] such that

                 A358: a in xZZ and

                 A359: (Fn2 . a) = b by FUNCT_2: 65;

                

                 A360: ( CircleMap . (Fn2 . a)) = (( CircleMap * Fn2) . a) by FUNCT_2: 15

                .= (F . a) by A281, A297, FUNCT_1: 49;

                 [:xy, ZZ:] c= [:N, ZZ:] by A347, ZFMISC_1: 95;

                then a in [:N, ZZ:] by A358;

                then (F . a) in (F .: [:N, ZZ:]) by A6, A357, FUNCT_1:def 6;

                hence b in ( union D) by A334, A335, A359, A360, Lm12, FUNCT_1:def 7, TOPMETR: 17;

              end;

              

               A361: (TT . i) in Z by A321, A319, XXREAL_1: 1;

              then

               A362: [x1, (TT . i)] in [: {y}, Z:] by A338, ZFMISC_1: 87;

              

               A363: (Fn1 . [x1, (TT . i)]) in REAL by XREAL_0:def 1;

              

               A364: [: {y}, Z:] c= [:N1, I:] by A285, ZFMISC_1: 96;

              

              then (F . [x1, (TT . i)]) = (( CircleMap * Fn1) . [x1, (TT . i)]) by A283, A362, FUNCT_1: 49

              .= ( CircleMap . (Fn1 . [x1, (TT . i)])) by A298, A362, A364, FUNCT_1: 13;

              then (Fn1 . [x1, (TT . i)]) in ( CircleMap " Ui) by A334, A344, FUNCT_2: 38, A363, TOPMETR: 17;

              then

              consider Uit be set such that

               A365: (Fn1 . [x1, (TT . i)]) in Uit and

               A366: Uit in D by A335, TARSKI:def 4;

              reconsider Uit as non empty Subset of R^1 by A365, A366;

              set f = ( CircleMap | Uit);

              

               A367: ( dom f) = Uit by Lm12, RELAT_1: 62, TOPMETR: 17;

              

               A368: ( rng f) c= Ui

              proof

                let b be object;

                assume b in ( rng f);

                then

                consider a be object such that

                 A369: a in ( dom f) and

                 A370: (f . a) = b by FUNCT_1:def 3;

                a in ( union D) by A366, A367, A369, TARSKI:def 4;

                then ( CircleMap . a) in Ui by A335, FUNCT_2: 38;

                hence thesis by A367, A369, A370, FUNCT_1: 49;

              end;

              the carrier of (TUC | Ui) = Ui & the carrier of ( R^1 | Uit) = Uit by PRE_TOPC: 8;

              then

              reconsider f as Function of ( R^1 | Uit), (TUC | Ui) by A367, A368, FUNCT_2: 2;

              

               A371: [:N2, Z:] c= [:N2, I:] by ZFMISC_1: 95;

              

               A372: (Fn2 . [x1, (TT . i)]) in REAL by XREAL_0:def 1;

              

               A373: [x1, (TT . i)] in [:N2, Z:] by A295, A338, A361, ZFMISC_1: 87;

              

              then (F . [x1, (TT . i)]) = (( CircleMap * Fn2) . [x1, (TT . i)]) by A281, A371, FUNCT_1: 49

              .= ( CircleMap . (Fn2 . [x1, (TT . i)])) by A293, A297, A373, A371, FUNCT_1: 13;

              then (Fn2 . [x1, (TT . i)]) in ( CircleMap " Ui) by A334, A344, FUNCT_2: 38, A372, TOPMETR: 17;

              then

              consider Uith be set such that

               A374: (Fn2 . [x1, (TT . i)]) in Uith and

               A375: Uith in D by A335, TARSKI:def 4;

              reconsider Uith as non empty Subset of R^1 by A374, A375;

              

               A376: ( dom (Fn1 | [:xy, ZZ:])) = [:xy, ZZ:] by A296, A299, A345, RELAT_1: 62, ZFMISC_1: 96;

              

               A377: x1 in xy by TARSKI:def 1;

              then

               A378: [x1, (TT . i)] in xZZ by A332, ZFMISC_1: 87;

              then (Fn1 . [x1, (TT . i)]) in (Fn1 .: xZZ) by FUNCT_2: 35;

              then Uit meets (Fn1 .: xZZ) by A365, XBOOLE_0: 3;

              then

               A379: (Fn1 .: xZZ) c= Uit by A280, A366, A354, A348, TOPALG_3: 12, TOPS_2: 61;

              

               A380: ( rng (Fn1 | [:xy, ZZ:])) c= ( dom f)

              proof

                let b be object;

                assume b in ( rng (Fn1 | [:xy, ZZ:]));

                then

                consider a be object such that

                 A381: a in ( dom (Fn1 | [:xy, ZZ:])) and

                 A382: ((Fn1 | [:xy, ZZ:]) . a) = b by FUNCT_1:def 3;

                (Fn1 . a) = b by A376, A381, A382, FUNCT_1: 49;

                then b in (Fn1 .: xZZ) by A299, A376, A381, FUNCT_1:def 6;

                hence thesis by A379, A367;

              end;

              then

               A383: ( dom (f * (Fn1 | [:xy, ZZ:]))) = ( dom (Fn1 | [:xy, ZZ:])) by RELAT_1: 27;

               [x1, (TT . i)] in [:xy, ZZ:] by A338, A343, A332, ZFMISC_1: 87;

              then [x1, (TT . i)] in ( dom Fn2) by A294, A342;

              then

               A384: (Fn2 . [x1, (TT . i)]) in (Fn2 .: xZZ) by A378, FUNCT_2: 35;

              then Uith meets (Fn2 .: xZZ) by A374, XBOOLE_0: 3;

              then

               A385: (Fn2 .: xZZ) c= Uith by A279, A375, A355, A356, TOPALG_3: 12, TOPS_2: 61;

              (Fn1 . [x1, (TT . i)]) = ((Fn1 | [: {y}, Z:]) . [x1, (TT . i)]) by A362, FUNCT_1: 49

              .= (Fn2 . [x1, (TT . i)]) by A322, A362, FUNCT_1: 49;

              then Uit meets Uith by A365, A384, A385, XBOOLE_0: 3;

              then

               A386: Uit = Uith by A366, A375, TAXONOM2:def 5;

              

               A387: for x be object st x in ( dom (f * (Fn1 | [:xy, ZZ:]))) holds ((f * (Fn1 | [:xy, ZZ:])) . x) = ((f * (Fn2 | [:xy, ZZ:])) . x)

              proof

                

                 A388: ( dom (Fn1 | [:xy, ZZ:])) c= ( dom Fn1) by RELAT_1: 60;

                let x be object such that

                 A389: x in ( dom (f * (Fn1 | [:xy, ZZ:])));

                

                 A390: (Fn1 . x) in (Fn1 .: [:xy, ZZ:]) by A299, A376, A383, A389, FUNCT_1:def 6;

                

                 A391: (Fn2 . x) in (Fn2 .: [:xy, ZZ:]) by A294, A342, A376, A383, A389, FUNCT_1:def 6;

                ( dom (Fn1 | [:xy, ZZ:])) = (( dom Fn1) /\ [:xy, ZZ:]) by RELAT_1: 61;

                then

                 A392: x in [:xy, ZZ:] by A383, A389, XBOOLE_0:def 4;

                

                thus ((f * (Fn1 | [:xy, ZZ:])) . x) = (((f * Fn1) | [:xy, ZZ:]) . x) by RELAT_1: 83

                .= ((f * Fn1) . x) by A376, A383, A389, FUNCT_1: 49

                .= (f . (Fn1 . x)) by A299, A389, FUNCT_1: 13

                .= ( CircleMap . (Fn1 . x)) by A379, A390, FUNCT_1: 49

                .= (( CircleMap * Fn1) . x) by A299, A389, FUNCT_1: 13

                .= (F . x) by A283, A298, A383, A389, A388, FUNCT_1: 49

                .= (( CircleMap * Fn2) . x) by A281, A342, A392, FUNCT_1: 49

                .= ( CircleMap . (Fn2 . x)) by A294, A342, A392, FUNCT_1: 13

                .= (f . (Fn2 . x)) by A385, A386, A391, FUNCT_1: 49

                .= ((f * Fn2) . x) by A294, A342, A392, FUNCT_1: 13

                .= (((f * Fn2) | [:xy, ZZ:]) . x) by A376, A383, A389, FUNCT_1: 49

                .= ((f * (Fn2 | [:xy, ZZ:])) . x) by RELAT_1: 83;

              end;

              

               A393: ( dom (Fn2 | [:xy, ZZ:])) = [:xy, ZZ:] by A293, A297, A341, RELAT_1: 62, ZFMISC_1: 96;

              

               A394: ( rng (Fn2 | [:xy, ZZ:])) c= ( dom f)

              proof

                let b be object;

                assume b in ( rng (Fn2 | [:xy, ZZ:]));

                then

                consider a be object such that

                 A395: a in ( dom (Fn2 | [:xy, ZZ:])) and

                 A396: ((Fn2 | [:xy, ZZ:]) . a) = b by FUNCT_1:def 3;

                (Fn2 . a) = b by A393, A395, A396, FUNCT_1: 49;

                then b in (Fn2 .: xZZ) by A293, A393, A395, FUNCT_1:def 6;

                hence thesis by A385, A386, A367;

              end;

              then ( dom (f * (Fn2 | [:xy, ZZ:]))) = ( dom (Fn2 | [:xy, ZZ:])) by RELAT_1: 27;

              then

               A397: (f * (Fn1 | [:xy, ZZ:])) = (f * (Fn2 | [:xy, ZZ:])) by A376, A393, A380, A387, RELAT_1: 27;

              f is being_homeomorphism by A336, A366;

              then

               A398: f is one-to-one;

              per cases ;

                suppose x2 in ZZ;

                then

                 A399: x in [:xy, ZZ:] by A340, A377, ZFMISC_1: 87;

                

                thus ((Fn1 | [: {y}, Z1:]) . x) = (Fn1 . x) by A328, A337, FUNCT_1: 49

                .= ((Fn1 | [:xy, ZZ:]) . x) by A399, FUNCT_1: 49

                .= ((Fn2 | [:xy, ZZ:]) . x) by A398, A376, A393, A380, A394, A397, FUNCT_1: 27

                .= (Fn2 . x) by A399, FUNCT_1: 49

                .= ((Fn2 | [: {y}, Z1:]) . x) by A328, A337, FUNCT_1: 49;

              end;

                suppose not x2 in ZZ;

                then x2 in Z by A339, XBOOLE_0:def 3;

                then

                 A400: x in [: {y}, Z:] by A338, A340, ZFMISC_1: 87;

                

                thus ((Fn1 | [: {y}, Z1:]) . x) = (Fn1 . x) by A328, A337, FUNCT_1: 49

                .= ((Fn1 | [: {y}, Z:]) . x) by A400, FUNCT_1: 49

                .= (Fn2 . x) by A322, A400, FUNCT_1: 49

                .= ((Fn2 | [: {y}, Z1:]) . x) by A328, A337, FUNCT_1: 49;

              end;

            end;

            ( dom (Fn2 | [: {y}, Z1:])) = [: {y}, Z1:] by A295, A293, A297, RELAT_1: 62, ZFMISC_1: 96;

            hence thesis by A328, A329;

          end;

        end;

        

         A401: M[ 0 ] by FINSEQ_3: 24;

        for i be Nat holds M[i] from NAT_1:sch 2( A401, A301);

        then ex Z be non empty Subset of I[01] st Z = [. 0 , (TT . ( len TT)).] & (Fn1 | [: {y}, Z:]) = (Fn2 | [: {y}, Z:]) by A292;

        hence thesis by A287, BORSUK_1: 40;

      end;

      for p be Point of [:Y, I[01] :], V be Subset of R^1 st (G . p) in V & V is open holds ex W be Subset of [:Y, I[01] :] st p in W & W is open & (G .: W) c= V

      proof

        let p be Point of [:Y, I[01] :], V be Subset of R^1 such that

         A402: (G . p) in V & V is open;

        consider y be Point of Y, t be Point of I[01] , N be non empty open Subset of Y, Fn be Function of [:(Y | N), I[01] :], R^1 such that

         A403: p = [y, t] and

         A404: (G . p) = (Fn . p) and

         A405: y in N and

         A406: Fn is continuous and

         A407: (F | [:N, I:]) = ( CircleMap * Fn) & (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) and for H be Function of [:(Y | N), I[01] :], R^1 st H is continuous & (F | [:N, I:]) = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) holds Fn = H by A274;

        

         A408: the carrier of [:(Y | N), I[01] :] = [:the carrier of (Y | N), I:] by BORSUK_1:def 2

        .= [:N, I:] by PRE_TOPC: 8;

        then p in the carrier of [:(Y | N), I[01] :] by A403, A405, ZFMISC_1: 87;

        then

        consider W be Subset of [:(Y | N), I[01] :] such that

         A409: p in W and

         A410: W is open and

         A411: (Fn .: W) c= V by A402, A404, A406, JGRAPH_2: 10;

        

         A412: ( dom Fn) = [:N, I:] by A408, FUNCT_2:def 1;

        

         A413: ( [#] (Y | N)) = N by PRE_TOPC:def 5;

        then

         A414: ( [#] [:(Y | N), I[01] :]) = [:N, ( [#] I[01] ):] by BORSUK_3: 1;

         [:(Y | N), I[01] :] = ( [:Y, I[01] :] | [:N, ( [#] I[01] ):]) by Lm7, BORSUK_3: 22;

        then

        consider C be Subset of [:Y, I[01] :] such that

         A415: C is open and

         A416: (C /\ ( [#] [:(Y | N), I[01] :])) = W by A410, TOPS_2: 24;

        take WW = (C /\ [:N, ( [#] I[01] ):]);

        thus p in WW by A409, A416, A413, BORSUK_3: 1;

         [:N, ( [#] I[01] ):] is open by BORSUK_1: 6;

        hence WW is open by A415;

        let y be object;

        assume y in (G .: WW);

        then

        consider x be Point of [:Y, I[01] :] such that

         A417: x in WW and

         A418: y = (G . x) by FUNCT_2: 65;

        consider y0 be Point of Y, t0 be Point of I[01] , N0 be non empty open Subset of Y, Fn0 be Function of [:(Y | N0), I[01] :], R^1 such that

         A419: x = [y0, t0] and

         A420: (G . x) = (Fn0 . x) and

         A421: y0 in N0 & Fn0 is continuous & (F | [:N0, I:]) = ( CircleMap * Fn0) & (Fn0 | [:the carrier of Y, { 0 }:]) = (Ft | [:N0, I:]) and for H be Function of [:(Y | N0), I[01] :], R^1 st H is continuous & (F | [:N0, I:]) = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N0, I:]) holds Fn0 = H by A274;

        x in [:N, ( [#] I[01] ):] by A417, XBOOLE_0:def 4;

        then

         A422: y0 in N by A419, ZFMISC_1: 87;

        

         A423: x in [: {y0}, I:] by A419, ZFMISC_1: 105;

        

        then (Fn . x) = ((Fn | [: {y0}, I:]) . x) by FUNCT_1: 49

        .= ((Fn0 | [: {y0}, I:]) . x) by A276, A406, A407, A419, A421, A422

        .= (Fn0 . x) by A423, FUNCT_1: 49;

        then y in (Fn .: W) by A412, A416, A414, A417, A418, A420, FUNCT_1:def 6;

        hence thesis by A411;

      end;

      hence G is continuous by JGRAPH_2: 10;

      for x be Point of [:Y, I[01] :] holds (F . x) = (( CircleMap * G) . x)

      proof

        let x be Point of [:Y, I[01] :];

        consider y be Point of Y, t be Point of I[01] , N be non empty open Subset of Y, Fn be Function of [:(Y | N), I[01] :], R^1 such that

         A424: x = [y, t] and

         A425: (G . x) = (Fn . x) and

         A426: y in N and Fn is continuous and

         A427: (F | [:N, I:]) = ( CircleMap * Fn) and (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) and for H be Function of [:(Y | N), I[01] :], R^1 st H is continuous & (F | [:N, I:]) = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) holds Fn = H by A274;

        

         A428: the carrier of [:(Y | N), I[01] :] = [:the carrier of (Y | N), I:] by BORSUK_1:def 2

        .= [:N, I:] by PRE_TOPC: 8;

        then

         A429: x in the carrier of [:(Y | N), I[01] :] by A424, A426, ZFMISC_1: 87;

        

        thus (( CircleMap * G) . x) = ( CircleMap . (G . x)) by FUNCT_2: 15

        .= (( CircleMap * Fn) . x) by A425, A429, FUNCT_2: 15

        .= (F . x) by A427, A428, A429, FUNCT_1: 49;

      end;

      hence F = ( CircleMap * G);

      

       A430: [:the carrier of Y, { 0 }:] c= [:the carrier of Y, I:] by Lm3, ZFMISC_1: 95;

      

       A431: the carrier of [:Y, I[01] :] = [:the carrier of Y, I:] by BORSUK_1:def 2;

      then

       A432: ( dom G) = [:the carrier of Y, I:] by FUNCT_2:def 1;

      

       A433: for x be object st x in ( dom Ft) holds (Ft . x) = (G . x)

      proof

        let x be object;

        assume

         A434: x in ( dom Ft);

        then x in ( dom G) by A8, A432, A430;

        then

        consider y be Point of Y, t be Point of I[01] , N be non empty open Subset of Y, Fn be Function of [:(Y | N), I[01] :], R^1 such that

         A435: x = [y, t] and

         A436: (G . x) = (Fn . x) and

         A437: y in N and Fn is continuous and (F | [:N, I:]) = ( CircleMap * Fn) and

         A438: (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) and for H be Function of [:(Y | N), I[01] :], R^1 st H is continuous & (F | [:N, I:]) = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) holds Fn = H by A274;

        x in [:N, I:] by A435, A437, ZFMISC_1: 87;

        

        hence (Ft . x) = ((Ft | [:N, I:]) . x) by FUNCT_1: 49

        .= (G . x) by A7, A434, A436, A438, Lm14, FUNCT_1: 49;

      end;

      ( dom Ft) = (( dom G) /\ [:the carrier of Y, { 0 }:]) by A8, A432, A430, XBOOLE_1: 28;

      hence (G | [:the carrier of Y, { 0 }:]) = Ft by A433, FUNCT_1: 46;

      let H be Function of [:Y, I[01] :], R^1 such that

       A439: H is continuous & F = ( CircleMap * H) and

       A440: (H | [:the carrier of Y, { 0 }:]) = Ft;

      for x be Point of [:Y, I[01] :] holds (G . x) = (H . x)

      proof

        let x be Point of [:Y, I[01] :];

        consider y be Point of Y, t be Point of I[01] , N be non empty open Subset of Y, Fn be Function of [:(Y | N), I[01] :], R^1 such that

         A441: x = [y, t] and

         A442: (G . x) = (Fn . x) and

         A443: y in N and Fn is continuous and (F | [:N, I:]) = ( CircleMap * Fn) and (Fn | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) and

         A444: for H be Function of [:(Y | N), I[01] :], R^1 st H is continuous & (F | [:N, I:]) = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = (Ft | [:N, I:]) holds Fn = H by A274;

        

         A445: the carrier of [:(Y | N), I[01] :] = [:the carrier of (Y | N), I:] by BORSUK_1:def 2

        .= [:N, I:] by PRE_TOPC: 8;

        then

         A446: x in the carrier of [:(Y | N), I[01] :] by A441, A443, ZFMISC_1: 87;

        ( dom H) = the carrier of [:Y, I[01] :] by FUNCT_2:def 1;

        then [:N, I:] c= ( dom H) by A431, ZFMISC_1: 95;

        then

         A447: ( dom (H | [:N, I:])) = [:N, I:] by RELAT_1: 62;

        ( rng (H | [:N, I:])) c= R;

        then

        reconsider H1 = (H | [:N, I:]) as Function of [:(Y | N), I[01] :], R^1 by A445, A447, FUNCT_2: 2;

        

         A448: ((H | [:N, I:]) | [:the carrier of Y, { 0 }:]) = (H | ( [:the carrier of Y, { 0 }:] /\ [:N, I:])) by RELAT_1: 71

        .= (Ft | [:N, I:]) by A440, RELAT_1: 71;

        H1 is continuous & (F | [:N, I:]) = ( CircleMap * (H | [:N, I:])) by A439, RELAT_1: 83, TOPALG_3: 17;

        

        hence (G . x) = ((H | [:N, I:]) . x) by A442, A444, A448

        .= (H . x) by A445, A446, FUNCT_1: 49;

      end;

      hence thesis;

    end;

    theorem :: TOPALG_5:23

    

     Th23: for x0,y0 be Point of ( Tunit_circle 2), xt be Point of R^1 , f be Path of x0, y0 st xt in ( CircleMap " {x0}) holds ex ft be Function of I[01] , R^1 st (ft . 0 ) = xt & f = ( CircleMap * ft) & ft is continuous & for f1 be Function of I[01] , R^1 st f1 is continuous & f = ( CircleMap * f1) & (f1 . 0 ) = xt holds ft = f1

    proof

      set Y = ( 1TopSp {1});

      let x0,y0 be Point of TUC;

      let xt be Point of R^1 ;

      let f be Path of x0, y0;

      deffunc F( set, Element of I) = (f . $2);

      consider F be Function of [:the carrier of Y, I:], cS1 such that

       A1: for y be Element of Y, i be Element of I holds (F . (y,i)) = F(y,i) from BINOP_1:sch 4;

      reconsider j = 1 as Point of Y by TARSKI:def 1;

      

       A2: [j, j0] in [:the carrier of Y, { 0 }:] by Lm4, ZFMISC_1: 87;

      

       A3: the carrier of [:Y, I[01] :] = [:the carrier of Y, I:] by BORSUK_1:def 2;

      then

      reconsider F as Function of [:Y, I[01] :], TUC;

      set Ft = ( [:Y, ( Sspace 0[01] ):] --> xt);

      

       A4: the carrier of [:Y, ( Sspace 0[01] ):] = [:the carrier of Y, the carrier of ( Sspace 0[01] ):] by BORSUK_1:def 2;

      then

       A5: for y be Element of Y, i be Element of { 0 } holds (Ft . [y, i]) = xt by Lm14, FUNCOP_1: 7;

      

       A6: ( [#] Y) = the carrier of Y;

      for p be Point of [:Y, I[01] :], V be Subset of TUC st (F . p) in V & V is open holds ex W be Subset of [:Y, I[01] :] st p in W & W is open & (F .: W) c= V

      proof

        let p be Point of [:Y, I[01] :], V be Subset of TUC such that

         A7: (F . p) in V & V is open;

        consider p1 be Point of Y, p2 be Point of I[01] such that

         A8: p = [p1, p2] by BORSUK_1: 10;

        (F . (p1,p2)) = (f . p2) by A1;

        then

        consider S be Subset of I[01] such that

         A9: p2 in S and

         A10: S is open and

         A11: (f .: S) c= V by A7, A8, JGRAPH_2: 10;

        set W = [: {1}, S:];

        W c= [:the carrier of Y, I:] by ZFMISC_1: 95;

        then

        reconsider W as Subset of [:Y, I[01] :] by BORSUK_1:def 2;

        take W;

        thus p in W by A8, A9, ZFMISC_1: 87;

        thus W is open by A6, A10, BORSUK_1: 6;

        let y be object;

        assume y in (F .: W);

        then

        consider x be object such that

         A12: x in the carrier of [:Y, I[01] :] and

         A13: x in W and

         A14: y = (F . x) by FUNCT_2: 64;

        consider x1 be Point of Y, x2 be Point of I[01] such that

         A15: x = [x1, x2] by A12, BORSUK_1: 10;

        x2 in S by A13, A15, ZFMISC_1: 87;

        then

         A16: (f . x2) in (f .: S) by FUNCT_2: 35;

        y = (F . (x1,x2)) by A14, A15

        .= (f . x2) by A1;

        hence thesis by A11, A16;

      end;

      then

       A17: F is continuous by JGRAPH_2: 10;

      assume xt in ( CircleMap " {x0});

      then

       A18: ( CircleMap . xt) in {x0} by FUNCT_2: 38;

      

       A19: for x be object st x in ( dom ( CircleMap * Ft)) holds ((F | [:the carrier of Y, { 0 }:]) . x) = (( CircleMap * Ft) . x)

      proof

        let x be object such that

         A20: x in ( dom ( CircleMap * Ft));

        consider x1,x2 be object such that

         A21: x1 in the carrier of Y and

         A22: x2 in { 0 } and

         A23: x = [x1, x2] by A4, A20, Lm14, ZFMISC_1:def 2;

        

         A24: x2 = 0 by A22, TARSKI:def 1;

        

        thus ((F | [:the carrier of Y, { 0 }:]) . x) = (F . (x1,x2)) by A4, A20, A23, Lm14, FUNCT_1: 49

        .= (f . x2) by A1, A21, A24, Lm2

        .= x0 by A24, BORSUK_2:def 4

        .= ( CircleMap . xt) by A18, TARSKI:def 1

        .= ( CircleMap . (Ft . x)) by A5, A21, A22, A23

        .= (( CircleMap * Ft) . x) by A20, FUNCT_1: 12;

      end;

      

       A25: ( dom ( CircleMap * Ft)) = [:the carrier of Y, { 0 }:] by A4, Lm14, FUNCT_2:def 1;

      

       A26: ( dom F) = the carrier of [:Y, I[01] :] by FUNCT_2:def 1;

      then

       A27: [:the carrier of Y, { 0 }:] c= ( dom F) by A3, Lm3, ZFMISC_1: 95;

      then ( dom (F | [:the carrier of Y, { 0 }:])) = [:the carrier of Y, { 0 }:] by RELAT_1: 62;

      then

      consider G be Function of [:Y, I[01] :], R^1 such that

       A28: G is continuous and

       A29: F = ( CircleMap * G) and

       A30: (G | [:the carrier of Y, { 0 }:]) = Ft and

       A31: for H be Function of [:Y, I[01] :], R^1 st H is continuous & F = ( CircleMap * H) & (H | [:the carrier of Y, { 0 }:]) = Ft holds G = H by A17, A25, A19, Th22, FUNCT_1: 2;

      take ft = ( Prj2 (j,G));

      

      thus (ft . 0 ) = (G . (j,j0)) by Def3

      .= (Ft . [j, j0]) by A30, A2, FUNCT_1: 49

      .= xt by A5, Lm4;

      for i be Point of I[01] holds (f . i) = (( CircleMap * ft) . i)

      proof

        let i be Point of I[01] ;

        

         A32: the carrier of [:Y, I[01] :] = [:the carrier of Y, the carrier of I[01] :] by BORSUK_1:def 2;

        

        thus (( CircleMap * ft) . i) = ( CircleMap . (ft . i)) by FUNCT_2: 15

        .= ( CircleMap . (G . (j,i))) by Def3

        .= (( CircleMap * G) . (j,i)) by A32, BINOP_1: 18

        .= (f . i) by A1, A29;

      end;

      hence f = ( CircleMap * ft);

      thus ft is continuous by A28;

      let f1 be Function of I[01] , R^1 ;

      deffunc H( set, Element of I) = (f1 . $2);

      consider H be Function of [:the carrier of Y, I:], R such that

       A33: for y be Element of Y, i be Element of I holds (H . (y,i)) = H(y,i) from BINOP_1:sch 4;

      reconsider H as Function of [:Y, I[01] :], R^1 by A3;

      assume that

       A34: f1 is continuous and

       A35: f = ( CircleMap * f1) and

       A36: (f1 . 0 ) = xt;

      for p be Point of [:Y, I[01] :], V be Subset of R^1 st (H . p) in V & V is open holds ex W be Subset of [:Y, I[01] :] st p in W & W is open & (H .: W) c= V

      proof

        let p be Point of [:Y, I[01] :], V be Subset of R^1 such that

         A37: (H . p) in V & V is open;

        consider p1 be Point of Y, p2 be Point of I[01] such that

         A38: p = [p1, p2] by BORSUK_1: 10;

        (H . p) = (H . (p1,p2)) by A38

        .= (f1 . p2) by A33;

        then

        consider W be Subset of I[01] such that

         A39: p2 in W and

         A40: W is open and

         A41: (f1 .: W) c= V by A34, A37, JGRAPH_2: 10;

        take W1 = [:( [#] Y), W:];

        thus p in W1 by A38, A39, ZFMISC_1: 87;

        thus W1 is open by A40, BORSUK_1: 6;

        let y be object;

        assume y in (H .: W1);

        then

        consider c be Element of [:Y, I[01] :] such that

         A42: c in W1 and

         A43: y = (H . c) by FUNCT_2: 65;

        consider c1,c2 be object such that

         A44: c1 in ( [#] Y) and

         A45: c2 in W and

         A46: c = [c1, c2] by A42, ZFMISC_1:def 2;

        

         A47: (f1 . c2) in (f1 .: W) by A45, FUNCT_2: 35;

        (H . c) = (H . (c1,c2)) by A46

        .= (f1 . c2) by A33, A44, A45;

        hence thesis by A41, A43, A47;

      end;

      then

       A48: H is continuous by JGRAPH_2: 10;

      for x be Point of [:Y, I[01] :] holds (F . x) = (( CircleMap * H) . x)

      proof

        let x be Point of [:Y, I[01] :];

        consider x1 be Point of Y, x2 be Point of I[01] such that

         A49: x = [x1, x2] by BORSUK_1: 10;

        

        thus (( CircleMap * H) . x) = ( CircleMap . (H . (x1,x2))) by A49, FUNCT_2: 15

        .= ( CircleMap . (f1 . x2)) by A33

        .= (( CircleMap * f1) . x2) by FUNCT_2: 15

        .= (F . (x1,x2)) by A1, A35

        .= (F . x) by A49;

      end;

      then

       A50: F = ( CircleMap * H);

      for i be Point of I[01] holds (ft . i) = (f1 . i)

      proof

        let i be Point of I[01] ;

        

         A51: ( dom H) = the carrier of [:Y, I[01] :] by FUNCT_2:def 1;

        then

         A52: ( dom (H | [:the carrier of Y, { 0 }:])) = [:the carrier of Y, { 0 }:] by A26, A27, RELAT_1: 62;

        

         A53: for x be object st x in ( dom (H | [:the carrier of Y, { 0 }:])) holds ((H | [:the carrier of Y, { 0 }:]) . x) = (Ft . x)

        proof

          let x be object;

          assume

           A54: x in ( dom (H | [:the carrier of Y, { 0 }:]));

          then

          consider x1,x2 be object such that

           A55: x1 in the carrier of Y and

           A56: x2 in { 0 } and

           A57: x = [x1, x2] by A52, ZFMISC_1:def 2;

          

           A58: x2 = j0 by A56, TARSKI:def 1;

          

          thus ((H | [:the carrier of Y, { 0 }:]) . x) = (H . (x1,x2)) by A54, A57, FUNCT_1: 47

          .= (f1 . x2) by A33, A55, A58

          .= (Ft . x) by A5, A36, A55, A56, A57, A58;

        end;

        ( dom Ft) = [:the carrier of Y, { 0 }:] by A4, Lm14, FUNCT_2:def 1;

        then

         A59: (H | [:the carrier of Y, { 0 }:]) = Ft by A26, A27, A51, A53, RELAT_1: 62;

        

        thus (ft . i) = (G . (j,i)) by Def3

        .= (H . (j,i)) by A31, A50, A48, A59

        .= (f1 . i) by A33;

      end;

      hence thesis;

    end;

    theorem :: TOPALG_5:24

    

     Th24: for x0,y0 be Point of ( Tunit_circle 2), P,Q be Path of x0, y0, F be Homotopy of P, Q, xt be Point of R^1 st (P,Q) are_homotopic & xt in ( CircleMap " {x0}) holds ex yt be Point of R^1 , Pt,Qt be Path of xt, yt, Ft be Homotopy of Pt, Qt st (Pt,Qt) are_homotopic & F = ( CircleMap * Ft) & yt in ( CircleMap " {y0}) & for F1 be Homotopy of Pt, Qt st F = ( CircleMap * F1) holds Ft = F1

    proof

      let x0,y0 be Point of TUC;

      let P,Q be Path of x0, y0;

      let F be Homotopy of P, Q;

      let xt be Point of R^1 ;

      set cP1 = the constant Loop of x0;

      set g1 = ( I[01] --> xt);

      set cP2 = the constant Loop of y0;

      assume

       A1: (P,Q) are_homotopic ;

      then

       A2: F is continuous by BORSUK_6:def 11;

      assume

       A3: xt in ( CircleMap " {x0});

      then

      consider ft be Function of I[01] , R^1 such that

       A4: (ft . 0 ) = xt and

       A5: P = ( CircleMap * ft) and

       A6: ft is continuous and for f1 be Function of I[01] , R^1 st f1 is continuous & P = ( CircleMap * f1) & (f1 . 0 ) = xt holds ft = f1 by Th23;

      defpred P[ set, set, set] means $3 = (ft . $1);

      

       A7: for x be Element of I holds for y be Element of { 0 } holds ex z be Element of REAL st P[x, y, z]

      proof

        let x be Element of I;

        (ft . x) in REAL by XREAL_0:def 1;

        hence thesis;

      end;

      consider Ft be Function of [:I, { 0 }:], REAL such that

       A8: for y be Element of I, i be Element of { 0 } holds P[y, i, (Ft . (y,i))] from BINOP_1:sch 3( A7);

      ( CircleMap . xt) in {x0} by A3, FUNCT_2: 38;

      then

       A9: ( CircleMap . xt) = x0 by TARSKI:def 1;

      

       A10: for x be Point of I[01] holds (cP1 . x) = (( CircleMap * g1) . x)

      proof

        let x be Point of I[01] ;

        

        thus (cP1 . x) = x0 by TOPALG_3: 21

        .= ( CircleMap . (g1 . x)) by A9, TOPALG_3: 4

        .= (( CircleMap * g1) . x) by FUNCT_2: 15;

      end;

      consider ft1 be Function of I[01] , R^1 such that (ft1 . 0 ) = xt and cP1 = ( CircleMap * ft1) and ft1 is continuous and

       A11: for f1 be Function of I[01] , R^1 st f1 is continuous & cP1 = ( CircleMap * f1) & (f1 . 0 ) = xt holds ft1 = f1 by A3, Th23;

      (g1 . j0) = xt by TOPALG_3: 4;

      then

       A12: ft1 = g1 by A11, A10, FUNCT_2: 63;

      

       A13: ( rng Ft) c= REAL ;

      

       A14: ( dom Ft) = [:I, { 0 }:] by FUNCT_2:def 1;

      

       A15: the carrier of [: I[01] , ( Sspace 0[01] ):] = [:I, the carrier of ( Sspace 0[01] ):] by BORSUK_1:def 2;

      then

      reconsider Ft as Function of [: I[01] , ( Sspace 0[01] ):], R^1 by Lm14, TOPMETR: 17;

      

       A16: for x be object st x in ( dom ( CircleMap * Ft)) holds ((F | [:I, { 0 }:]) . x) = (( CircleMap * Ft) . x)

      proof

        let x be object such that

         A17: x in ( dom ( CircleMap * Ft));

        consider x1,x2 be object such that

         A18: x1 in I and

         A19: x2 in { 0 } and

         A20: x = [x1, x2] by A15, A17, Lm14, ZFMISC_1:def 2;

        x2 = 0 by A19, TARSKI:def 1;

        

        hence ((F | [:I, { 0 }:]) . x) = (F . (x1, 0 )) by A15, A17, A20, Lm14, FUNCT_1: 49

        .= (( CircleMap * ft) . x1) by A1, A5, A18, BORSUK_6:def 11

        .= ( CircleMap . (ft . x1)) by A18, FUNCT_2: 15

        .= ( CircleMap . (Ft . (x1,x2))) by A8, A18, A19

        .= (( CircleMap * Ft) . x) by A17, A20, FUNCT_1: 12;

      end;

      for p be Point of [: I[01] , ( Sspace 0[01] ):], V be Subset of R^1 st (Ft . p) in V & V is open holds ex W be Subset of [: I[01] , ( Sspace 0[01] ):] st p in W & W is open & (Ft .: W) c= V

      proof

        let p be Point of [: I[01] , ( Sspace 0[01] ):], V be Subset of R^1 such that

         A21: (Ft . p) in V & V is open;

        consider p1 be Point of I[01] , p2 be Point of ( Sspace 0[01] ) such that

         A22: p = [p1, p2] by A15, DOMAIN_1: 1;

         P[p1, p2, (Ft . (p1,p2))] by A8, Lm14;

        then

        consider W1 be Subset of I[01] such that

         A23: p1 in W1 and

         A24: W1 is open and

         A25: (ft .: W1) c= V by A6, A21, A22, JGRAPH_2: 10;

        reconsider W1 as non empty Subset of I[01] by A23;

        take W = [:W1, ( [#] ( Sspace 0[01] )):];

        thus p in W by A22, A23, ZFMISC_1:def 2;

        thus W is open by A24, BORSUK_1: 6;

        let y be object;

        assume y in (Ft .: W);

        then

        consider x be Element of [: I[01] , ( Sspace 0[01] ):] such that

         A26: x in W and

         A27: y = (Ft . x) by FUNCT_2: 65;

        consider x1 be Element of W1, x2 be Point of ( Sspace 0[01] ) such that

         A28: x = [x1, x2] by A26, DOMAIN_1: 1;

         P[x1, x2, (Ft . (x1,x2))] & (ft . x1) in (ft .: W1) by A8, Lm14, FUNCT_2: 35;

        hence thesis by A25, A27, A28;

      end;

      then

       A29: Ft is continuous by JGRAPH_2: 10;

      take yt = (ft . j1);

      

       A30: [j1, j0] in [:I, { 0 }:] by Lm4, ZFMISC_1: 87;

      reconsider ft as Path of xt, yt by A4, A6, BORSUK_2:def 4;

      

       A31: [j0, j0] in [:I, { 0 }:] by Lm4, ZFMISC_1: 87;

      

       A32: ( dom F) = the carrier of [: I[01] , I[01] :] by FUNCT_2:def 1;

      then

       A33: [:I, { 0 }:] c= ( dom F) by Lm3, Lm5, ZFMISC_1: 95;

      then ( dom (F | [:I, { 0 }:])) = [:I, { 0 }:] by RELAT_1: 62;

      then (F | [:I, { 0 }:]) = ( CircleMap * Ft) by A14, A13, A16, Lm12, FUNCT_1: 2, RELAT_1: 27;

      then

      consider G be Function of [: I[01] , I[01] :], R^1 such that

       A34: G is continuous and

       A35: F = ( CircleMap * G) and

       A36: (G | [:I, { 0 }:]) = Ft and

       A37: for H be Function of [: I[01] , I[01] :], R^1 st H is continuous & F = ( CircleMap * H) & (H | [:the carrier of I[01] , { 0 }:]) = Ft holds G = H by A2, A29, Th22;

      set sM0 = ( Prj2 (j0,G));

      

       A38: for x be Point of I[01] holds (cP1 . x) = (( CircleMap * sM0) . x)

      proof

        let x be Point of I[01] ;

        

        thus (( CircleMap * sM0) . x) = ( CircleMap . (sM0 . x)) by FUNCT_2: 15

        .= ( CircleMap . (G . (j0,x))) by Def3

        .= (( CircleMap * G) . (j0,x)) by Lm5, BINOP_1: 18

        .= x0 by A1, A35, BORSUK_6:def 11

        .= (cP1 . x) by TOPALG_3: 21;

      end;

      set g2 = ( I[01] --> yt);

      

       A39: ( CircleMap . yt) = (P . j1) by A5, FUNCT_2: 15

      .= y0 by BORSUK_2:def 4;

      

       A40: for x be Point of I[01] holds (cP2 . x) = (( CircleMap * g2) . x)

      proof

        let x be Point of I[01] ;

        

        thus (cP2 . x) = y0 by TOPALG_3: 21

        .= ( CircleMap . (g2 . x)) by A39, TOPALG_3: 4

        .= (( CircleMap * g2) . x) by FUNCT_2: 15;

      end;

      

       A41: ( CircleMap . yt) in {y0} by A39, TARSKI:def 1;

      then yt in ( CircleMap " {y0}) by FUNCT_2: 38;

      then

      consider ft2 be Function of I[01] , R^1 such that (ft2 . 0 ) = yt and cP2 = ( CircleMap * ft2) and ft2 is continuous and

       A42: for f1 be Function of I[01] , R^1 st f1 is continuous & cP2 = ( CircleMap * f1) & (f1 . 0 ) = yt holds ft2 = f1 by Th23;

      (g2 . j0) = yt by TOPALG_3: 4;

      then

       A43: ft2 = g2 by A42, A40, FUNCT_2: 63;

      set sM1 = ( Prj2 (j1,G));

      

       A44: for x be Point of I[01] holds (cP2 . x) = (( CircleMap * sM1) . x)

      proof

        let x be Point of I[01] ;

        

        thus (( CircleMap * sM1) . x) = ( CircleMap . (sM1 . x)) by FUNCT_2: 15

        .= ( CircleMap . (G . (j1,x))) by Def3

        .= (( CircleMap * G) . (j1,x)) by Lm5, BINOP_1: 18

        .= y0 by A1, A35, BORSUK_6:def 11

        .= (cP2 . x) by TOPALG_3: 21;

      end;

      (sM1 . 0 ) = (G . (j1,j0)) by Def3

      .= (Ft . (j1,j0)) by A36, A30, FUNCT_1: 49

      .= yt by A8, Lm4;

      then

       A45: ft2 = sM1 by A34, A42, A44, FUNCT_2: 63;

      (sM0 . 0 ) = (G . (j0,j0)) by Def3

      .= (Ft . (j0,j0)) by A36, A31, FUNCT_1: 49

      .= xt by A4, A8, Lm4;

      then

       A46: ft1 = sM0 by A34, A11, A38, FUNCT_2: 63;

      set Qt = ( Prj1 (j1,G));

      

       A47: (Qt . 0 ) = (G . (j0,j1)) by Def2

      .= (sM0 . j1) by Def3

      .= xt by A46, A12, TOPALG_3: 4;

      (Qt . 1) = (G . (j1,j1)) by Def2

      .= (sM1 . j1) by Def3

      .= yt by A45, A43, TOPALG_3: 4;

      then

      reconsider Qt as Path of xt, yt by A34, A47, BORSUK_2:def 4;

       A48:

      now

        let s be Point of I[01] ;

         [s, 0 ] in [:I, { 0 }:] by Lm4, ZFMISC_1: 87;

        

        hence (G . (s, 0 )) = (Ft . (s,j0)) by A36, FUNCT_1: 49

        .= (ft . s) by A8, Lm4;

        thus (G . (s,1)) = (Qt . s) by Def2;

        let t be Point of I[01] ;

        

        thus (G . ( 0 ,t)) = (sM0 . t) by Def3

        .= xt by A46, A12, TOPALG_3: 4;

        

        thus (G . (1,t)) = (sM1 . t) by Def3

        .= yt by A45, A43, TOPALG_3: 4;

      end;

      then (ft,Qt) are_homotopic by A34;

      then

      reconsider G as Homotopy of ft, Qt by A34, A48, BORSUK_6:def 11;

      take ft, Qt;

      take G;

      thus

       A49: (ft,Qt) are_homotopic by A34, A48;

      thus F = ( CircleMap * G) by A35;

      thus yt in ( CircleMap " {y0}) by A41, FUNCT_2: 38;

      let F1 be Homotopy of ft, Qt such that

       A50: F = ( CircleMap * F1);

      

       A51: ( dom F1) = the carrier of [: I[01] , I[01] :] by FUNCT_2:def 1;

      then

       A52: ( dom (F1 | [:I, { 0 }:])) = [:I, { 0 }:] by A32, A33, RELAT_1: 62;

      for x be object st x in ( dom (F1 | [:I, { 0 }:])) holds ((F1 | [:I, { 0 }:]) . x) = (Ft . x)

      proof

        let x be object;

        assume

         A53: x in ( dom (F1 | [:I, { 0 }:]));

        then

        consider x1,x2 be object such that

         A54: x1 in I and

         A55: x2 in { 0 } and

         A56: x = [x1, x2] by A52, ZFMISC_1:def 2;

        

         A57: x2 = 0 by A55, TARSKI:def 1;

        

        thus ((F1 | [:I, { 0 }:]) . x) = (F1 . (x1,x2)) by A53, A56, FUNCT_1: 47

        .= (ft . x1) by A49, A54, A57, BORSUK_6:def 11

        .= (Ft . (x1,x2)) by A8, A54, A55

        .= (Ft . x) by A56;

      end;

      then (F1 | [:I, { 0 }:]) = Ft by A32, A33, A14, A51, RELAT_1: 62;

      hence thesis by A37, A50;

    end;

    definition

      :: TOPALG_5:def5

      func Ciso -> Function of INT.Group , ( pi_1 (( Tunit_circle 2), c[10] )) means

      : Def5: for n be Integer holds (it . n) = ( Class (( EqRel (( Tunit_circle 2), c[10] )),( cLoop n)));

      existence

      proof

        defpred P[ Integer, set] means $2 = ( Class (( EqRel (TUC, c[10] )),( cLoop $1)));

        

         A1: for x be Element of INT holds ex y be Element of ( pi_1 (TUC, c[10] )) st P[x, y]

        proof

          let x be Element of INT ;

          reconsider y = ( Class (( EqRel (TUC, c[10] )),( cLoop x))) as Element of ( pi_1 (TUC, c[10] )) by TOPALG_1: 47;

          take y;

          thus thesis;

        end;

        consider f be Function of INT , the carrier of ( pi_1 (TUC, c[10] )) such that

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

        reconsider f as Function of INT.Group , ( pi_1 (TUC, c[10] ));

        take f;

        let n be Integer;

        n in INT by INT_1:def 2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of INT.Group , ( pi_1 (TUC, c[10] )) such that

         A3: for n be Integer holds (f . n) = ( Class (( EqRel (TUC, c[10] )),( cLoop n))) and

         A4: for n be Integer holds (g . n) = ( Class (( EqRel (TUC, c[10] )),( cLoop n)));

        for x be Element of INT.Group holds (f . x) = (g . x)

        proof

          let x be Element of INT.Group ;

          

          thus (f . x) = ( Class (( EqRel (TUC, c[10] )),( cLoop x))) by A3

          .= (g . x) by A4;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPALG_5:25

    

     Th25: for i be Integer, f be Path of ( R^1 0 ), ( R^1 i) holds ( Ciso . i) = ( Class (( EqRel (( Tunit_circle 2), c[10] )),( CircleMap * f)))

    proof

      let i be Integer;

      let f be Path of ( R^1 0 ), ( R^1 i);

      set P = ( CircleMap * f);

      

       A1: (P . 0 ) = ( CircleMap . (f . j0)) by FUNCT_2: 15

      .= ( CircleMap . ( R^1 0 )) by BORSUK_2:def 4

      .= ( CircleMap . 0 ) by TOPREALB:def 2

      .= |[( cos ((2 * PI ) * 0 )), ( sin ((2 * PI ) * 0 ))]| by TOPREALB:def 11

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

      (P . 1) = ( CircleMap . (f . j1)) by FUNCT_2: 15

      .= ( CircleMap . ( R^1 i)) by BORSUK_2:def 4

      .= ( CircleMap . i) by TOPREALB:def 2

      .= |[( cos (((2 * PI ) * i) + 0 )), ( sin (((2 * PI ) * i) + 0 ))]| by TOPREALB:def 11

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

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

      then

      reconsider P as Loop of c[10] by A1, BORSUK_2:def 4;

      

       A2: ( cLoop i) = ( CircleMap * ( ExtendInt i)) by Th20;

      

       A3: (( cLoop i),P) are_homotopic

      proof

        reconsider J = R^1 as non empty interval SubSpace of R^1 ;

        reconsider r0 = ( R^1 0 ), ri = ( R^1 i) as Point of J;

        reconsider O = ( ExtendInt i), ff = f as Path of r0, ri;

        reconsider G = ( R1Homotopy (O,ff)) as Function of [: I[01] , I[01] :], R^1 ;

        take F = ( CircleMap * G);

        thus F is continuous;

        let s be Point of I[01] ;

        

        thus (F . (s, 0 )) = ( CircleMap . (G . (s,j0))) by Lm5, BINOP_1: 18

        .= ( CircleMap . (((1 - j0) * (( ExtendInt i) . s)) + (j0 * (f . s)))) by TOPALG_2:def 4

        .= (( cLoop i) . s) by A2, FUNCT_2: 15;

        

        thus (F . (s,1)) = ( CircleMap . (G . (s,j1))) by Lm5, BINOP_1: 18

        .= ( CircleMap . (((1 - j1) * (( ExtendInt i) . s)) + (j1 * (f . s)))) by TOPALG_2:def 4

        .= (P . s) by FUNCT_2: 15;

        

        thus (F . ( 0 ,s)) = ( CircleMap . (G . (j0,s))) by Lm5, BINOP_1: 18

        .= ( CircleMap . (((1 - s) * (( ExtendInt i) . j0)) + (s * (f . j0)))) by TOPALG_2:def 4

        .= ( CircleMap . (((1 - s) * ( R^1 0 )) + (s * (f . j0)))) by BORSUK_2:def 4

        .= ( CircleMap . (((1 - s) * ( R^1 0 )) + (s * ( R^1 0 )))) by BORSUK_2:def 4

        .= ( CircleMap . (((1 - s) * 0 ) + (s * 0 ))) by TOPREALB:def 2

        .= c[10] by TOPREALB: 32;

        

        thus (F . (1,s)) = ( CircleMap . (G . (j1,s))) by Lm5, BINOP_1: 18

        .= ( CircleMap . (((1 - s) * (( ExtendInt i) . j1)) + (s * (f . j1)))) by TOPALG_2:def 4

        .= ( CircleMap . (((1 - s) * ( R^1 i)) + (s * (f . j1)))) by BORSUK_2:def 4

        .= ( CircleMap . (((1 - s) * ( R^1 i)) + (s * ( R^1 i)))) by BORSUK_2:def 4

        .= ( CircleMap . i) by TOPREALB:def 2

        .= c[10] by TOPREALB: 32;

      end;

      

      thus ( Ciso . i) = ( Class (( EqRel (TUC, c[10] )),( cLoop i))) by Def5

      .= ( Class (( EqRel (TUC, c[10] )),( CircleMap * f))) by A3, TOPALG_1: 46;

    end;

    registration

      cluster Ciso -> multiplicative;

      coherence

      proof

        set f = Ciso ;

        let x,y be Element of INT.Group ;

        consider fX,fY be Loop of c[10] such that

         A1: (f . x) = ( Class (( EqRel (TUC, c[10] )),fX)) and

         A2: (f . y) = ( Class (( EqRel (TUC, c[10] )),fY)) and

         A3: (the multF of ( pi_1 (TUC, c[10] )) . ((f . x),(f . y))) = ( Class (( EqRel (TUC, c[10] )),(fX + fY))) by TOPALG_1:def 5;

        (f . y) = ( Class (( EqRel (TUC, c[10] )),( cLoop y))) by Def5;

        then

         A4: (fY,( cLoop y)) are_homotopic by A2, TOPALG_1: 46;

        reconsider tx = ( AffineMap (1,x)) as Function of R^1 , R^1 by TOPMETR: 17;

        set p = (tx * ( ExtendInt y));

        

         A5: (p . 0 ) = (tx . (( ExtendInt y) . j0)) by FUNCT_2: 15

        .= (tx . (y * j0)) by Def1

        .= ((1 * 0 ) + x) by FCONT_1:def 4

        .= ( R^1 x) by TOPREALB:def 2;

        

         A6: (p . 1) = (tx . (( ExtendInt y) . j1)) by FUNCT_2: 15

        .= (tx . (y * j1)) by Def1

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

        .= ( R^1 (x + y)) by TOPREALB:def 2;

        tx is being_homeomorphism by JORDAN16: 20;

        then tx is continuous;

        then

        reconsider p as Path of ( R^1 x), ( R^1 (x + y)) by A5, A6, BORSUK_2:def 4;

        

         A7: for a be Point of I[01] holds (( CircleMap * (( ExtendInt x) + p)) . a) = ((( cLoop x) + ( cLoop y)) . a)

        proof

          let a be Point of I[01] ;

          per cases ;

            suppose

             A8: a <= (1 / 2);

            then

             A9: (2 * a) is Point of I[01] by BORSUK_6: 3;

            

            thus (( CircleMap * (( ExtendInt x) + p)) . a) = ( CircleMap . ((( ExtendInt x) + p) . a)) by FUNCT_2: 15

            .= ( CircleMap . (( ExtendInt x) . (2 * a))) by A8, BORSUK_6:def 2

            .= ( CircleMap . (x * (2 * a))) by A9, Def1

            .= |[( cos ((2 * PI ) * (x * (2 * a)))), ( sin ((2 * PI ) * (x * (2 * a))))]| by TOPREALB:def 11

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

            .= (( cLoop x) . (2 * a)) by A9, Def4

            .= ((( cLoop x) + ( cLoop y)) . a) by A8, BORSUK_6:def 2;

          end;

            suppose

             A10: (1 / 2) <= a;

            then

             A11: ((2 * a) - 1) is Point of I[01] by BORSUK_6: 4;

            

            thus (( CircleMap * (( ExtendInt x) + p)) . a) = ( CircleMap . ((( ExtendInt x) + p) . a)) by FUNCT_2: 15

            .= ( CircleMap . (p . ((2 * a) - 1))) by A10, BORSUK_6:def 2

            .= ( CircleMap . (tx . (( ExtendInt y) . ((2 * a) - 1)))) by A11, FUNCT_2: 15

            .= ( CircleMap . (tx . (y * ((2 * a) - 1)))) by A11, Def1

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

            .= |[( cos ((2 * PI ) * ((y * ((2 * a) - 1)) + x))), ( sin ((2 * PI ) * ((y * ((2 * a) - 1)) + x)))]| by TOPREALB:def 11

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

            .= |[( cos (((2 * PI ) * y) * ((2 * a) - 1))), ( sin (((2 * PI ) * y) * ((2 * a) - 1)))]| by COMPLEX2: 8

            .= (( cLoop y) . ((2 * a) - 1)) by A11, Def4

            .= ((( cLoop x) + ( cLoop y)) . a) by A10, BORSUK_6:def 2;

          end;

        end;

        (f . x) = ( Class (( EqRel (TUC, c[10] )),( cLoop x))) by Def5;

        then (fX,( cLoop x)) are_homotopic by A1, TOPALG_1: 46;

        then

         A12: ((fX + fY),(( cLoop x) + ( cLoop y))) are_homotopic by A4, BORSUK_6: 76;

        

        thus (f . (x * y)) = ( Class (( EqRel (TUC, c[10] )),( CircleMap * (( ExtendInt x) + p)))) by Th25

        .= ( Class (( EqRel (TUC, c[10] )),(( cLoop x) + ( cLoop y)))) by A7, FUNCT_2: 63

        .= ((f . x) * (f . y)) by A3, A12, TOPALG_1: 46;

      end;

    end

    registration

      cluster Ciso -> one-to-one onto;

      coherence

      proof

        thus Ciso is one-to-one

        proof

          set xt = ( R^1 0 );

          let m,n be object;

          assume that

           A1: m in ( dom Ciso ) & n in ( dom Ciso ) and

           A2: ( Ciso . m) = ( Ciso . n);

          reconsider m, n as Integer by A1;

          ( Ciso . m) = ( Class (( EqRel (TUC, c[10] )),( cLoop m))) & ( Ciso . n) = ( Class (( EqRel (TUC, c[10] )),( cLoop n))) by Def5;

          then

           A3: (( cLoop m),( cLoop n)) are_homotopic by A2, TOPALG_1: 46;

          then

          consider F be Function of [: I[01] , I[01] :], TUC such that

           A4: F is continuous and

           A5: for s be Point of I[01] holds (F . (s, 0 )) = (( cLoop m) . s) & (F . (s,1)) = (( cLoop n) . s) & for t be Point of I[01] holds (F . ( 0 ,t)) = c[10] & (F . (1,t)) = c[10] ;

          

           A6: xt in ( CircleMap " { c[10] }) by Lm1, TOPREALB: 33, TOPREALB:def 2;

          then

          consider ftm be Function of I[01] , R^1 such that (ftm . 0 ) = xt and ( cLoop m) = ( CircleMap * ftm) and ftm is continuous and

           A7: for f1 be Function of I[01] , R^1 st f1 is continuous & ( cLoop m) = ( CircleMap * f1) & (f1 . 0 ) = xt holds ftm = f1 by Th23;

          F is Homotopy of ( cLoop m), ( cLoop n) by A3, A4, A5, BORSUK_6:def 11;

          then

          consider yt be Point of R^1 , Pt,Qt be Path of xt, yt, Ft be Homotopy of Pt, Qt such that

           A8: (Pt,Qt) are_homotopic and

           A9: F = ( CircleMap * Ft) and yt in ( CircleMap " { c[10] }) and for F1 be Homotopy of Pt, Qt st F = ( CircleMap * F1) holds Ft = F1 by A3, A6, Th24;

          

           A10: ( cLoop n) = ( CircleMap * ( ExtendInt n)) by Th20;

          set ft0 = ( Prj1 (j0,Ft));

           A11:

          now

            let x be Point of I[01] ;

            

            thus (( CircleMap * ft0) . x) = ( CircleMap . (ft0 . x)) by FUNCT_2: 15

            .= ( CircleMap . (Ft . (x,j0))) by Def2

            .= (F . (x,j0)) by A9, Lm5, BINOP_1: 18

            .= (( cLoop m) . x) by A5;

          end;

          (ft0 . 0 ) = (Ft . (j0,j0)) by Def2

          .= xt by A8, BORSUK_6:def 11;

          then

           A12: ft0 = ftm by A7, A11, FUNCT_2: 63;

          set ft1 = ( Prj1 (j1,Ft));

           A13:

          now

            let x be Point of I[01] ;

            

            thus (( CircleMap * ft1) . x) = ( CircleMap . (ft1 . x)) by FUNCT_2: 15

            .= ( CircleMap . (Ft . (x,j1))) by Def2

            .= (F . (x,j1)) by A9, Lm5, BINOP_1: 18

            .= (( cLoop n) . x) by A5;

          end;

          consider ftn be Function of I[01] , R^1 such that (ftn . 0 ) = xt and ( cLoop n) = ( CircleMap * ftn) and ftn is continuous and

           A14: for f1 be Function of I[01] , R^1 st f1 is continuous & ( cLoop n) = ( CircleMap * f1) & (f1 . 0 ) = xt holds ftn = f1 by A6, Th23;

          

           A15: ( cLoop m) = ( CircleMap * ( ExtendInt m)) by Th20;

          (ft1 . 0 ) = (Ft . (j0,j1)) by Def2

          .= xt by A8, BORSUK_6:def 11;

          then

           A16: ft1 = ftn by A14, A13, FUNCT_2: 63;

          (( ExtendInt n) . 0 ) = (n * j0) by Def1

          .= xt by TOPREALB:def 2;

          then ( ExtendInt n) = ftn by A14, A10;

          then

           A17: (ft1 . j1) = (n * 1) by A16, Def1;

          (( ExtendInt m) . 0 ) = (m * j0) by Def1

          .= xt by TOPREALB:def 2;

          then ( ExtendInt m) = ftm by A7, A15;

          then

           A18: (ft0 . j1) = (m * 1) by A12, Def1;

          (ft0 . j1) = (Ft . (j1,j0)) by Def2

          .= yt by A8, BORSUK_6:def 11

          .= (Ft . (j1,j1)) by A8, BORSUK_6:def 11

          .= (ft1 . j1) by Def2;

          hence thesis by A18, A17;

        end;

        thus ( rng Ciso ) c= the carrier of ( pi_1 (TUC, c[10] ));

        let q be object;

        assume q in the carrier of ( pi_1 (TUC, c[10] ));

        then

        consider f be Loop of c[10] such that

         A19: q = ( Class (( EqRel (TUC, c[10] )),f)) by TOPALG_1: 47;

        ( R^1 0 ) in ( CircleMap " { c[10] }) by Lm1, TOPREALB: 33, TOPREALB:def 2;

        then

        consider ft be Function of I[01] , R^1 such that

         A20: (ft . 0 ) = ( R^1 0 ) and

         A21: f = ( CircleMap * ft) and

         A22: ft is continuous and for f1 be Function of I[01] , R^1 st f1 is continuous & f = ( CircleMap * f1) & (f1 . 0 ) = ( R^1 0 ) holds ft = f1 by Th23;

        

         A23: (ft . 1) in REAL by XREAL_0:def 1;

        ( CircleMap . (ft . j1)) = (( CircleMap * ft) . j1) by FUNCT_2: 15

        .= c[10] by A21, BORSUK_2:def 4;

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

        then

         A24: (ft . 1) in INT by Lm12, FUNCT_1:def 7, TOPREALB: 33, A23;

        (ft . 1) = ( R^1 (ft . 1)) by TOPREALB:def 2;

        then ft is Path of ( R^1 0 ), ( R^1 (ft . 1)) by A20, A22, BORSUK_2:def 4;

        then ( dom Ciso ) = INT & ( Ciso . (ft . 1)) = ( Class (( EqRel (TUC, c[10] )),( CircleMap * ft))) by A24, Th25, FUNCT_2:def 1;

        hence thesis by A19, A21, A24, FUNCT_1:def 3;

      end;

    end

    theorem :: TOPALG_5:26

     Ciso is bijective;

    

     Lm16: for r be positive Real, o be Point of ( TOP-REAL 2), x be Point of ( Tcircle (o,r)) holds ( INT.Group ,( pi_1 (( Tcircle (o,r)),x))) are_isomorphic

    proof

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

      TUC = ( Tcircle (( 0. ( TOP-REAL 2)),1)) by TOPREALB:def 7;

      then (( pi_1 (TUC, c[10] )),( pi_1 (( Tcircle (o,r)),x))) are_isomorphic by TOPALG_3: 33, TOPREALB: 20;

      then

      consider h be Homomorphism of ( pi_1 (TUC, c[10] )), ( pi_1 (( Tcircle (o,r)),x)) such that

       A1: h is bijective;

      take (h * Ciso );

      thus thesis by A1, GROUP_6: 64;

    end;

    theorem :: TOPALG_5:27

    

     Th27: for S be being_simple_closed_curve SubSpace of ( TOP-REAL 2), x be Point of S holds ( INT.Group ,( pi_1 (S,x))) are_isomorphic

    proof

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

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

      ( INT.Group ,( pi_1 (( Tcircle (o,r)),y))) are_isomorphic & (( pi_1 (( Tcircle (o,r)),y)),( pi_1 (S,x))) are_isomorphic by Lm16, TOPALG_3: 33, TOPREALB: 11;

      hence thesis by GROUP_6: 67;

    end;

    registration

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

      cluster ( pi_1 (S,x)) -> infinite;

      coherence

      proof

        ( INT.Group ,( pi_1 (S,x))) are_isomorphic by Th27;

        hence thesis by GROUP_6: 74;

      end;

    end