borsuk_2.miz



    begin

    reserve T,T1,T2,S for non empty TopSpace;

    

     Lm1: for r be Real holds 0 <= r & r <= 1 iff r in the carrier of I[01]

    proof

      let r be Real;

      

       A1: [. 0 , 1.] = { r1 where r1 be Real : 0 <= r1 & r1 <= 1 } by RCOMP_1:def 1;

      thus 0 <= r & r <= 1 implies r in the carrier of I[01] by A1, BORSUK_1: 40;

      assume r in the carrier of I[01] ;

      then ex r2 be Real st r2 = r & 0 <= r2 & r2 <= 1 by A1, BORSUK_1: 40;

      hence thesis;

    end;

    scheme :: BORSUK_2:sch1

    FrCard { A() -> non empty set , X() -> set , F( object) -> set , P[ set] } :

( card { F(w) where w be Element of A() : w in X() & P[w] }) c= ( card X());

      consider f be Function such that

       A1: ( dom f) = X() & for x be object st x in X() holds (f . x) = F(x) from FUNCT_1:sch 3;

      { F(w) where w be Element of A() : w in X() & P[w] } c= ( rng f)

      proof

        let x be object;

        assume x in { F(w) where w be Element of A() : w in X() & P[w] };

        then

        consider w be Element of A() such that

         A2: x = F(w) and

         A3: w in X() and P[w];

        (f . w) = x by A1, A2, A3;

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

      end;

      hence thesis by A1, CARD_1: 12;

    end;

    theorem :: BORSUK_2:1

    for f be Function of T1, S, g be Function of T2, S st T1 is SubSpace of T & T2 is SubSpace of T & (( [#] T1) \/ ( [#] T2)) = ( [#] T) & T1 is compact & T2 is compact & T is T_2 & f is continuous & g is continuous & (for p be set st p in (( [#] T1) /\ ( [#] T2)) holds (f . p) = (g . p)) holds ex h be Function of T, S st h = (f +* g) & h is continuous

    proof

      let f be Function of T1, S, g be Function of T2, S;

      assume that

       A1: T1 is SubSpace of T and

       A2: T2 is SubSpace of T and

       A3: (( [#] T1) \/ ( [#] T2)) = ( [#] T) and

       A4: T1 is compact and

       A5: T2 is compact and

       A6: T is T_2 and

       A7: f is continuous and

       A8: g is continuous and

       A9: for p be set st p in (( [#] T1) /\ ( [#] T2)) holds (f . p) = (g . p);

      set h = (f +* g);

      

       A10: ( dom g) = ( [#] T2) by FUNCT_2:def 1;

      

       A11: ( dom f) = ( [#] T1) by FUNCT_2:def 1;

      then

       A12: ( dom h) = the carrier of T by A3, A10, FUNCT_4:def 1;

      ( rng h) c= (( rng f) \/ ( rng g)) by FUNCT_4: 17;

      then

      reconsider h as Function of T, S by A12, FUNCT_2: 2, XBOOLE_1: 1;

      take h;

      thus h = (f +* g);

      for P be Subset of S st P is closed holds (h " P) is closed

      proof

        let P be Subset of S;

        reconsider P3 = (f " P) as Subset of T1;

        reconsider P4 = (g " P) as Subset of T2;

        ( [#] T1) c= ( [#] T) by A3, XBOOLE_1: 7;

        then

        reconsider P1 = (f " P) as Subset of T by XBOOLE_1: 1;

        ( [#] T2) c= ( [#] T) by A3, XBOOLE_1: 7;

        then

        reconsider P2 = (g " P) as Subset of T by XBOOLE_1: 1;

        

         A13: ( dom h) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1;

         A14:

        now

          let x be object;

          thus x in ((h " P) /\ ( [#] T2)) implies x in (g " P)

          proof

            assume

             A15: x in ((h " P) /\ ( [#] T2));

            then x in (h " P) by XBOOLE_0:def 4;

            then

             A16: (h . x) in P by FUNCT_1:def 7;

            (g . x) = (h . x) by A10, A15, FUNCT_4: 13;

            hence thesis by A10, A15, A16, FUNCT_1:def 7;

          end;

          assume

           A17: x in (g " P);

          then

           A18: x in ( dom g) by FUNCT_1:def 7;

          (g . x) in P by A17, FUNCT_1:def 7;

          then

           A19: (h . x) in P by A18, FUNCT_4: 13;

          x in ( dom h) by A13, A18, XBOOLE_0:def 3;

          then x in (h " P) by A19, FUNCT_1:def 7;

          hence x in ((h " P) /\ ( [#] T2)) by A17, XBOOLE_0:def 4;

        end;

        

         A20: for x be set st x in ( [#] T1) holds (h . x) = (f . x)

        proof

          let x be set such that

           A21: x in ( [#] T1);

          now

            per cases ;

              suppose

               A22: x in ( [#] T2);

              then x in (( [#] T1) /\ ( [#] T2)) by A21, XBOOLE_0:def 4;

              then (f . x) = (g . x) by A9;

              hence thesis by A10, A22, FUNCT_4: 13;

            end;

              suppose not x in ( [#] T2);

              hence thesis by A10, FUNCT_4: 11;

            end;

          end;

          hence thesis;

        end;

        now

          let x be object;

          thus x in ((h " P) /\ ( [#] T1)) implies x in (f " P)

          proof

            assume

             A23: x in ((h " P) /\ ( [#] T1));

            then x in (h " P) by XBOOLE_0:def 4;

            then

             A24: (h . x) in P by FUNCT_1:def 7;

            (f . x) = (h . x) by A20, A23;

            hence thesis by A11, A23, A24, FUNCT_1:def 7;

          end;

          assume

           A25: x in (f " P);

          then x in ( dom f) by FUNCT_1:def 7;

          then

           A26: x in ( dom h) by A13, XBOOLE_0:def 3;

          (f . x) in P by A25, FUNCT_1:def 7;

          then (h . x) in P by A20, A25;

          then x in (h " P) by A26, FUNCT_1:def 7;

          hence x in ((h " P) /\ ( [#] T1)) by A25, XBOOLE_0:def 4;

        end;

        then

         A27: ((h " P) /\ ( [#] T1)) = (f " P) by TARSKI: 2;

        assume

         A28: P is closed;

        then P3 is closed by A7;

        then P3 is compact by A4, COMPTS_1: 8;

        then

         A29: P1 is compact by A1, COMPTS_1: 19;

        P4 is closed by A8, A28;

        then P4 is compact by A5, COMPTS_1: 8;

        then

         A30: P2 is compact by A2, COMPTS_1: 19;

        (h " P) = ((h " P) /\ (( [#] T1) \/ ( [#] T2))) by A11, A10, A13, RELAT_1: 132, XBOOLE_1: 28

        .= (((h " P) /\ ( [#] T1)) \/ ((h " P) /\ ( [#] T2))) by XBOOLE_1: 23;

        then (h " P) = ((f " P) \/ (g " P)) by A27, A14, TARSKI: 2;

        hence thesis by A6, A29, A30;

      end;

      hence thesis;

    end;

    registration

      let T be TopStruct;

      cluster ( id T) -> open continuous;

      coherence by FUNCT_1: 92, FUNCT_2: 94;

    end

    registration

      let T be TopStruct;

      cluster continuous one-to-one for Function of T, T;

      existence

      proof

        take ( id T);

        thus thesis;

      end;

    end

    theorem :: BORSUK_2:2

    for S,T be non empty TopSpace, f be Function of S, T st f is being_homeomorphism holds (f " ) is open

    proof

      let S,T be non empty TopSpace, f be Function of S, T;

      assume f is being_homeomorphism;

      then

       A1: ( rng f) = ( [#] T) & f is one-to-one continuous by TOPS_2:def 5;

      let P be Subset of T;

      (f " P) = ((f " ) .: P) by A1, TOPS_2: 55;

      hence thesis by A1, TOPS_2: 43;

    end;

    begin

    theorem :: BORSUK_2:3

    

     Th3: for T be non empty TopSpace, a be Point of T holds ex f be Function of I[01] , T st f is continuous & (f . 0 ) = a & (f . 1) = a

    proof

      let T be non empty TopSpace, a be Point of T;

      take ( I[01] --> a);

      thus thesis by BORSUK_1:def 14, BORSUK_1:def 15, FUNCOP_1: 7;

    end;

    definition

      let T be TopStruct, a,b be Point of T;

      :: BORSUK_2:def1

      pred a,b are_connected means ex f be Function of I[01] , T st f is continuous & (f . 0 ) = a & (f . 1) = b;

    end

    definition

      let T be non empty TopSpace, a,b be Point of T;

      :: original: are_connected

      redefine

      pred a,b are_connected ;

      reflexivity by Th3;

    end

    definition

      let T be TopStruct;

      let a,b be Point of T;

      assume

       A1: (a,b) are_connected ;

      :: BORSUK_2:def2

      mode Path of a,b -> Function of I[01] , T means

      : Def2: it is continuous & (it . 0 ) = a & (it . 1) = b;

      existence by A1;

    end

    registration

      let T be non empty TopSpace;

      let a be Point of T;

      cluster continuous for Path of a, a;

      existence

      proof

        set IT = ( I[01] --> a);

        

         A1: (a,a) are_connected ;

        (IT . 0 ) = a & (IT . 1) = a by BORSUK_1:def 14, BORSUK_1:def 15, FUNCOP_1: 7;

        then IT is Path of a, a by A1, Def2;

        hence thesis;

      end;

    end

    definition

      let T be TopStruct;

      :: BORSUK_2:def3

      attr T is pathwise_connected means

      : Def3: for a,b be Point of T holds (a,b) are_connected ;

      correctness ;

    end

    registration

      cluster strict pathwise_connected non empty for TopSpace;

      existence

      proof

        set T = ( I[01] | { 0[01] });

         0[01] in { 0[01] } by TARSKI:def 1;

        then

        reconsider nl = 0[01] as Point of T by PRE_TOPC: 8;

        

         A1: the carrier of T = { 0[01] } by PRE_TOPC: 8;

        for a,b be Point of T holds (a,b) are_connected

        proof

          reconsider f = ( I[01] --> nl) as Function of I[01] , T;

          let a,b be Point of T;

          take f;

          thus f is continuous;

          a = nl & b = nl by A1, TARSKI:def 1;

          hence thesis by BORSUK_1:def 15, FUNCOP_1: 7;

        end;

        then T is pathwise_connected;

        hence thesis;

      end;

    end

    definition

      let T be pathwise_connected TopStruct;

      let a,b be Point of T;

      :: original: Path

      redefine

      :: BORSUK_2:def4

      mode Path of a,b means

      : Def4: it is continuous & (it . 0 ) = a & (it . 1) = b;

      compatibility

      proof

        (a,b) are_connected by Def3;

        hence thesis by Def2;

      end;

    end

    registration

      let T be pathwise_connected TopStruct;

      let a,b be Point of T;

      cluster -> continuous for Path of a, b;

      coherence by Def4;

    end

    reserve GY for non empty TopSpace,

r,s for Real;

    

     Lm2: 0 in [. 0 , 1.] & 1 in [. 0 , 1.] by XXREAL_1: 1;

    registration

      cluster pathwise_connected -> connected for non empty TopSpace;

      coherence

      proof

        let GX be non empty TopSpace;

        assume

         A1: for x,y be Point of GX holds (x,y) are_connected ;

        for x,y be Point of GX holds ex GY st (GY is connected & ex f be Function of GY, GX st f is continuous & x in ( rng f) & y in ( rng f))

        proof

          let x,y be Point of GX;

          (x,y) are_connected by A1;

          then

          consider h be Function of I[01] , GX such that

           A2: h is continuous and

           A3: x = (h . 0 ) and

           A4: y = (h . 1);

          1 in ( dom h) by Lm2, BORSUK_1: 40, FUNCT_2:def 1;

          then

           A5: y in ( rng h) by A4, FUNCT_1:def 3;

           0 in ( dom h) by Lm2, BORSUK_1: 40, FUNCT_2:def 1;

          then x in ( rng h) by A3, FUNCT_1:def 3;

          hence thesis by A2, A5, TREAL_1: 19;

        end;

        hence thesis by TOPS_2: 63;

      end;

    end

    begin

    

     Lm3: for G be non empty TopSpace, w1,w2,w3 be Point of G, h1,h2 be Function of I[01] , G st h1 is continuous & w1 = (h1 . 0 ) & w2 = (h1 . 1) & h2 is continuous & w2 = (h2 . 0 ) & w3 = (h2 . 1) holds ex h3 be Function of I[01] , G st h3 is continuous & w1 = (h3 . 0 ) & w3 = (h3 . 1) & ( rng h3) c= (( rng h1) \/ ( rng h2))

    proof

      let G be non empty TopSpace, w1,w2,w3 be Point of G, h1,h2 be Function of I[01] , G;

      assume that

       A1: h1 is continuous and

       A2: w1 = (h1 . 0 ) and

       A3: w2 = (h1 . 1) and

       A4: h2 is continuous and

       A5: w2 = (h2 . 0 ) and

       A6: w3 = (h2 . 1);

      (w2,w3) are_connected by A4, A5, A6;

      then

      reconsider g2 = h2 as Path of w2, w3 by A4, A5, A6, Def2;

      (w1,w2) are_connected by A1, A2, A3;

      then

      reconsider g1 = h1 as Path of w1, w2 by A1, A2, A3, Def2;

      set P1 = g1, P2 = g2, p1 = w1, p3 = w3;

      ex P0 be Path of p1, p3 st P0 is continuous & (P0 . 0 ) = p1 & (P0 . 1) = p3 & for t be Point of I[01] , t9 be Real st t = t9 holds ( 0 <= t9 & t9 <= (1 / 2) implies (P0 . t) = (P1 . (2 * t9))) & ((1 / 2) <= t9 & t9 <= 1 implies (P0 . t) = (P2 . ((2 * t9) - 1)))

      proof

        (1 / 2) in { r : 0 <= r & r <= 1 };

        then

        reconsider pol = (1 / 2) as Point of I[01] by BORSUK_1: 40, RCOMP_1:def 1;

        reconsider T1 = ( Closed-Interval-TSpace ( 0 ,(1 / 2))), T2 = ( Closed-Interval-TSpace ((1 / 2),1)) as SubSpace of I[01] by TOPMETR: 20, TREAL_1: 3;

        set e2 = ( P[01] ((1 / 2),1,( (#) ( 0 ,1)),(( 0 ,1) (#) )));

        set e1 = ( P[01] ( 0 ,(1 / 2),( (#) ( 0 ,1)),(( 0 ,1) (#) )));

        set E1 = (P1 * e1);

        set E2 = (P2 * e2);

        set f = (E1 +* E2);

        

         A7: ( dom e1) = the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by FUNCT_2:def 1

        .= [. 0 , (1 / 2).] by TOPMETR: 18;

        

         A8: ( dom e2) = the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def 1

        .= [.(1 / 2), 1.] by TOPMETR: 18;

        reconsider gg = E2 as Function of T2, G by TOPMETR: 20;

        reconsider ff = E1 as Function of T1, G by TOPMETR: 20;

        

         A9: for t9 be Real st (1 / 2) <= t9 & t9 <= 1 holds (E2 . t9) = (P2 . ((2 * t9) - 1))

        proof

          reconsider r1 = ( (#) ( 0 ,1)), r2 = (( 0 ,1) (#) ) as Real;

          ( dom e2) = the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def 1;

          

          then

           A10: ( dom e2) = [.(1 / 2), 1.] by TOPMETR: 18

          .= { r : (1 / 2) <= r & r <= 1 } by RCOMP_1:def 1;

          let t9 be Real;

          assume (1 / 2) <= t9 & t9 <= 1;

          then

           A11: t9 in ( dom e2) by A10;

          then

          reconsider s = t9 as Point of ( Closed-Interval-TSpace ((1 / 2),1));

          (e2 . s) = ((((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))) by TREAL_1: 11

          .= ((2 * t9) - 1) by TREAL_1: 5;

          hence thesis by A11, FUNCT_1: 13;

        end;

        

         A12: for t9 be Real st 0 <= t9 & t9 <= (1 / 2) holds (E1 . t9) = (P1 . (2 * t9))

        proof

          reconsider r1 = ( (#) ( 0 ,1)), r2 = (( 0 ,1) (#) ) as Real;

          ( dom e1) = the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by FUNCT_2:def 1;

          

          then

           A13: ( dom e1) = [. 0 , (1 / 2).] by TOPMETR: 18

          .= { r : 0 <= r & r <= (1 / 2) } by RCOMP_1:def 1;

          let t9 be Real;

          assume 0 <= t9 & t9 <= (1 / 2);

          then

           A14: t9 in ( dom e1) by A13;

          then

          reconsider s = t9 as Point of ( Closed-Interval-TSpace ( 0 ,(1 / 2)));

          (e1 . s) = ((((r2 - r1) / ((1 / 2) - 0 )) * t9) + ((((1 / 2) * r1) - ( 0 * r2)) / ((1 / 2) - 0 ))) by TREAL_1: 11

          .= (2 * t9) by TREAL_1: 5;

          hence thesis by A14, FUNCT_1: 13;

        end;

        

        then

         A15: (ff . (1 / 2)) = (P2 . ((2 * (1 / 2)) - 1)) by A3, A5

        .= (gg . pol) by A9;

        ( [#] T1) = [. 0 , (1 / 2).] & ( [#] T2) = [.(1 / 2), 1.] by TOPMETR: 18;

        then

         A16: (( [#] T1) \/ ( [#] T2)) = ( [#] I[01] ) & (( [#] T1) /\ ( [#] T2)) = {pol} by BORSUK_1: 40, XXREAL_1: 174, XXREAL_1: 418;

        

         A17: T2 is compact by HEINE: 4;

        ( dom P1) = the carrier of I[01] by FUNCT_2:def 1;

        then

         A18: ( rng e1) c= ( dom P1) by TOPMETR: 20;

        ( dom P2) = the carrier of I[01] & ( rng e2) c= the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by FUNCT_2:def 1;

        then

         A19: ( dom E2) = ( dom e2) by RELAT_1: 27, TOPMETR: 20;

         not 0 in { r : (1 / 2) <= r & r <= 1 }

        proof

          assume 0 in { r : (1 / 2) <= r & r <= 1 };

          then ex rr be Real st rr = 0 & (1 / 2) <= rr & rr <= 1;

          hence thesis;

        end;

        then not 0 in ( dom E2) by A8, A19, RCOMP_1:def 1;

        

        then

         A20: (f . 0 ) = (E1 . 0 ) by FUNCT_4: 11

        .= (P1 . (2 * 0 )) by A12

        .= p1 by A2;

        

         A21: ( dom f) = (( dom E1) \/ ( dom E2)) by FUNCT_4:def 1

        .= ( [. 0 , (1 / 2).] \/ [.(1 / 2), 1.]) by A7, A8, A18, A19, RELAT_1: 27

        .= the carrier of I[01] by BORSUK_1: 40, XXREAL_1: 174;

        ( rng f) c= (( rng E1) \/ ( rng E2)) by FUNCT_4: 17;

        then

         A22: ( rng f) c= the carrier of G by XBOOLE_1: 1;

        

         A23: R^1 is T_2 & T1 is compact by HEINE: 4, PCOMPS_1: 34, TOPMETR:def 6;

        reconsider f as Function of I[01] , G by A21, A22, FUNCT_2:def 1, RELSET_1: 4;

        e1 is continuous & e2 is continuous by TREAL_1: 12;

        then

        reconsider f as continuous Function of I[01] , G by A1, A4, A15, A16, A23, A17, COMPTS_1: 20, TOPMETR: 20;

        1 in { r : (1 / 2) <= r & r <= 1 };

        then 1 in ( dom E2) by A8, A19, RCOMP_1:def 1;

        

        then

         A24: (f . 1) = (E2 . 1) by FUNCT_4: 13

        .= (P2 . ((2 * 1) - 1)) by A9

        .= p3 by A6;

        then (p1,p3) are_connected by A20;

        then

        reconsider f as Path of p1, p3 by A20, A24, Def2;

        for t be Point of I[01] , t9 be Real st t = t9 holds ( 0 <= t9 & t9 <= (1 / 2) implies (f . t) = (P1 . (2 * t9))) & ((1 / 2) <= t9 & t9 <= 1 implies (f . t) = (P2 . ((2 * t9) - 1)))

        proof

          let t be Point of I[01] , t9 be Real;

          assume

           A25: t = t9;

          thus 0 <= t9 & t9 <= (1 / 2) implies (f . t) = (P1 . (2 * t9))

          proof

            assume

             A26: 0 <= t9 & t9 <= (1 / 2);

            then t9 in { r : 0 <= r & r <= (1 / 2) };

            then

             A27: t9 in [. 0 , (1 / 2).] by RCOMP_1:def 1;

            per cases ;

              suppose

               A28: t9 <> (1 / 2);

               not t9 in ( dom E2)

              proof

                assume t9 in ( dom E2);

                then t9 in ( [. 0 , (1 / 2).] /\ [.(1 / 2), 1.]) by A8, A19, A27, XBOOLE_0:def 4;

                then t9 in {(1 / 2)} by XXREAL_1: 418;

                hence thesis by A28, TARSKI:def 1;

              end;

              

              then (f . t) = (E1 . t) by A25, FUNCT_4: 11

              .= (P1 . (2 * t9)) by A12, A25, A26;

              hence thesis;

            end;

              suppose

               A29: t9 = (1 / 2);

              (1 / 2) in { r : (1 / 2) <= r & r <= 1 };

              then (1 / 2) in [.(1 / 2), 1.] by RCOMP_1:def 1;

              then (1 / 2) in the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by TOPMETR: 18;

              then t in ( dom E2) by A25, A29, FUNCT_2:def 1, TOPMETR: 20;

              

              then (f . t) = (E2 . (1 / 2)) by A25, A29, FUNCT_4: 13

              .= (P1 . (2 * t9)) by A12, A15, A29;

              hence thesis;

            end;

          end;

          thus (1 / 2) <= t9 & t9 <= 1 implies (f . t) = (P2 . ((2 * t9) - 1))

          proof

            assume

             A30: (1 / 2) <= t9 & t9 <= 1;

            then t9 in { r : (1 / 2) <= r & r <= 1 };

            then t9 in [.(1 / 2), 1.] by RCOMP_1:def 1;

            

            then (f . t) = (E2 . t) by A8, A19, A25, FUNCT_4: 13

            .= (P2 . ((2 * t9) - 1)) by A9, A25, A30;

            hence thesis;

          end;

        end;

        hence thesis by A20, A24;

      end;

      then

      consider P0 be Path of p1, p3 such that

       A31: P0 is continuous & (P0 . 0 ) = p1 & (P0 . 1) = p3 and

       A32: for t be Point of I[01] , t9 be Real st t = t9 holds ( 0 <= t9 & t9 <= (1 / 2) implies (P0 . t) = (P1 . (2 * t9))) & ((1 / 2) <= t9 & t9 <= 1 implies (P0 . t) = (P2 . ((2 * t9) - 1)));

      ( rng P0) c= (( rng P1) \/ ( rng P2))

      proof

        

         A33: ( dom g2) = the carrier of I[01] by FUNCT_2:def 1;

        let x be object;

        

         A34: ( dom g1) = the carrier of I[01] by FUNCT_2:def 1;

        assume x in ( rng P0);

        then

        consider z be object such that

         A35: z in ( dom P0) and

         A36: x = (P0 . z) by FUNCT_1:def 3;

        reconsider r = z as Real by A35;

        

         A37: 0 <= r by A35, BORSUK_1: 40, XXREAL_1: 1;

        

         A38: r <= 1 by A35, BORSUK_1: 40, XXREAL_1: 1;

        per cases ;

          suppose

           A39: r <= (1 / 2);

          then

           A40: (2 * r) <= (2 * (1 / 2)) by XREAL_1: 64;

           0 <= (2 * r) by A37, XREAL_1: 127;

          then

           A41: (2 * r) in the carrier of I[01] by A40, BORSUK_1: 40, XXREAL_1: 1;

          (P0 . z) = (P1 . (2 * r)) by A32, A35, A37, A39;

          then (P0 . z) in ( rng g1) by A34, A41, FUNCT_1:def 3;

          hence thesis by A36, XBOOLE_0:def 3;

        end;

          suppose

           A42: r > (1 / 2);

          (2 * r) <= (2 * 1) by A38, XREAL_1: 64;

          then (2 * r) <= (1 + 1);

          then

           A43: ((2 * r) - 1) <= 1 by XREAL_1: 20;

          (2 * (1 / 2)) = 1;

          then ( 0 + 1) <= (2 * r) by A42, XREAL_1: 64;

          then 0 <= ((2 * r) - 1) by XREAL_1: 19;

          then

           A44: ((2 * r) - 1) in the carrier of I[01] by A43, BORSUK_1: 40, XXREAL_1: 1;

          (P0 . z) = (P2 . ((2 * r) - 1)) by A32, A35, A38, A42;

          then (P0 . z) in ( rng g2) by A33, A44, FUNCT_1:def 3;

          hence thesis by A36, XBOOLE_0:def 3;

        end;

      end;

      hence thesis by A31;

    end;

    definition

      let T be non empty TopSpace;

      let a,b,c be Point of T;

      let P be Path of a, b, Q be Path of b, c;

      :: BORSUK_2:def5

      func P + Q -> Path of a, c means

      : Def5: for t be Point of I[01] holds (t <= (1 / 2) implies (it . t) = (P . (2 * t))) & ((1 / 2) <= t implies (it . t) = (Q . ((2 * t) - 1)));

      existence

      proof

        (1 / 2) in { r : 0 <= r & r <= 1 };

        then

        reconsider pol = (1 / 2) as Point of I[01] by BORSUK_1: 40, RCOMP_1:def 1;

        reconsider T1 = ( Closed-Interval-TSpace ( 0 ,(1 / 2))), T2 = ( Closed-Interval-TSpace ((1 / 2),1)) as SubSpace of I[01] by TOPMETR: 20, TREAL_1: 3;

        set e2 = ( P[01] ((1 / 2),1,( (#) ( 0 ,1)),(( 0 ,1) (#) )));

        set e1 = ( P[01] ( 0 ,(1 / 2),( (#) ( 0 ,1)),(( 0 ,1) (#) )));

        set E1 = (P * e1);

        set E2 = (Q * e2);

        set f = (E1 +* E2);

        

         A3: ( dom e1) = the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by FUNCT_2:def 1

        .= [. 0 , (1 / 2).] by TOPMETR: 18;

        

         A4: ( dom e2) = the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def 1

        .= [.(1 / 2), 1.] by TOPMETR: 18;

        

         A5: for t9 be Real st (1 / 2) <= t9 & t9 <= 1 holds (E2 . t9) = (Q . ((2 * t9) - 1))

        proof

          reconsider r1 = ( (#) ( 0 ,1)), r2 = (( 0 ,1) (#) ) as Real;

          ( dom e2) = the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by FUNCT_2:def 1;

          

          then

           A6: ( dom e2) = [.(1 / 2), 1.] by TOPMETR: 18

          .= { r : (1 / 2) <= r & r <= 1 } by RCOMP_1:def 1;

          let t9 be Real;

          assume (1 / 2) <= t9 & t9 <= 1;

          then

           A7: t9 in ( dom e2) by A6;

          then

          reconsider s = t9 as Point of ( Closed-Interval-TSpace ((1 / 2),1));

          (e2 . s) = ((((r2 - r1) / (1 - (1 / 2))) * t9) + (((1 * r1) - ((1 / 2) * r2)) / (1 - (1 / 2)))) by TREAL_1: 11

          .= ((2 * t9) - 1) by TREAL_1: 5;

          hence thesis by A7, FUNCT_1: 13;

        end;

        reconsider gg = E2 as Function of T2, T by TOPMETR: 20;

        reconsider ff = E1 as Function of T1, T by TOPMETR: 20;

        

         A8: e1 is continuous Function of ( Closed-Interval-TSpace ( 0 ,(1 / 2))), ( Closed-Interval-TSpace ( 0 ,1)) & e2 is continuous by TREAL_1: 12;

        ( rng f) c= (( rng E1) \/ ( rng E2)) by FUNCT_4: 17;

        then

         A9: ( rng f) c= the carrier of T by XBOOLE_1: 1;

        

         A10: R^1 is T_2 & T1 is compact by HEINE: 4, PCOMPS_1: 34, TOPMETR:def 6;

        

         A11: for t9 be Real st 0 <= t9 & t9 <= (1 / 2) holds (E1 . t9) = (P . (2 * t9))

        proof

          reconsider r1 = ( (#) ( 0 ,1)), r2 = (( 0 ,1) (#) ) as Real;

          ( dom e1) = the carrier of ( Closed-Interval-TSpace ( 0 ,(1 / 2))) by FUNCT_2:def 1;

          

          then

           A12: ( dom e1) = [. 0 , (1 / 2).] by TOPMETR: 18

          .= { r : 0 <= r & r <= (1 / 2) } by RCOMP_1:def 1;

          let t9 be Real;

          assume 0 <= t9 & t9 <= (1 / 2);

          then

           A13: t9 in ( dom e1) by A12;

          then

          reconsider s = t9 as Point of ( Closed-Interval-TSpace ( 0 ,(1 / 2)));

          (e1 . s) = ((((r2 - r1) / ((1 / 2) - 0 )) * t9) + ((((1 / 2) * r1) - ( 0 * r2)) / (1 / 2))) by TREAL_1: 11

          .= (2 * t9) by TREAL_1: 5;

          hence thesis by A13, FUNCT_1: 13;

        end;

        

        then

         A14: (ff . (1 / 2)) = (P . (2 * (1 / 2)))

        .= b by A1, Def2

        .= (Q . ((2 * (1 / 2)) - 1)) by A2, Def2

        .= (gg . pol) by A5;

        ( dom P) = the carrier of I[01] by FUNCT_2:def 1;

        then

         A15: ( rng e1) c= ( dom P) by TOPMETR: 20;

        ( dom Q) = the carrier of I[01] & ( rng e2) c= the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by FUNCT_2:def 1;

        then

         A16: ( dom E2) = ( dom e2) by RELAT_1: 27, TOPMETR: 20;

         not 0 in { r : (1 / 2) <= r & r <= 1 }

        proof

          assume 0 in { r : (1 / 2) <= r & r <= 1 };

          then ex rr be Real st rr = 0 & (1 / 2) <= rr & rr <= 1;

          hence thesis;

        end;

        then not 0 in ( dom E2) by A4, A16, RCOMP_1:def 1;

        

        then

         A17: (f . 0 ) = (E1 . 0 ) by FUNCT_4: 11

        .= (P . (2 * 0 )) by A11

        .= a by A1, Def2;

        

         A18: ( dom f) = (( dom E1) \/ ( dom E2)) by FUNCT_4:def 1

        .= ( [. 0 , (1 / 2).] \/ [.(1 / 2), 1.]) by A3, A4, A15, A16, RELAT_1: 27

        .= the carrier of I[01] by BORSUK_1: 40, XXREAL_1: 174;

        ( [#] T1) = [. 0 , (1 / 2).] & ( [#] T2) = [.(1 / 2), 1.] by TOPMETR: 18;

        then

         A19: (( [#] T1) \/ ( [#] T2)) = ( [#] I[01] ) & (( [#] T1) /\ ( [#] T2)) = {pol} by BORSUK_1: 40, XXREAL_1: 174, XXREAL_1: 418;

        

         A20: T2 is compact by HEINE: 4;

        reconsider f as Function of I[01] , T by A18, A9, FUNCT_2:def 1, RELSET_1: 4;

        P is continuous & Q is continuous by A1, A2, Def2;

        then

        reconsider f as continuous Function of I[01] , T by A8, A14, A19, A10, A20, COMPTS_1: 20, TOPMETR: 20;

        1 in { r : (1 / 2) <= r & r <= 1 };

        then 1 in ( dom E2) by A4, A16, RCOMP_1:def 1;

        

        then

         A21: (f . 1) = (E2 . 1) by FUNCT_4: 13

        .= (Q . ((2 * 1) - 1)) by A5

        .= c by A2, Def2;

        then (a,c) are_connected by A17;

        then

        reconsider f as Path of a, c by A17, A21, Def2;

        for t be Point of I[01] holds (t <= (1 / 2) implies (f . t) = (P . (2 * t))) & ((1 / 2) <= t implies (f . t) = (Q . ((2 * t) - 1)))

        proof

          let t be Point of I[01] ;

          

           A22: 0 <= t by Lm1;

          thus t <= (1 / 2) implies (f . t) = (P . (2 * t))

          proof

            assume

             A23: t <= (1 / 2);

            then t in { r : 0 <= r & r <= (1 / 2) } by A22;

            then

             A24: t in [. 0 , (1 / 2).] by RCOMP_1:def 1;

            per cases ;

              suppose

               A25: t <> (1 / 2);

               not t in ( dom E2)

              proof

                assume t in ( dom E2);

                then t in ( [. 0 , (1 / 2).] /\ [.(1 / 2), 1.]) by A4, A16, A24, XBOOLE_0:def 4;

                then t in {(1 / 2)} by XXREAL_1: 418;

                hence thesis by A25, TARSKI:def 1;

              end;

              

              then (f . t) = (E1 . t) by FUNCT_4: 11

              .= (P . (2 * t)) by A11, A22, A23;

              hence thesis;

            end;

              suppose

               A26: t = (1 / 2);

              (1 / 2) in { r : (1 / 2) <= r & r <= 1 };

              then (1 / 2) in [.(1 / 2), 1.] by RCOMP_1:def 1;

              then (1 / 2) in the carrier of ( Closed-Interval-TSpace ((1 / 2),1)) by TOPMETR: 18;

              then t in ( dom E2) by A26, FUNCT_2:def 1, TOPMETR: 20;

              

              then (f . t) = (E1 . t) by A14, A26, FUNCT_4: 13

              .= (P . (2 * t)) by A11, A22, A23;

              hence thesis;

            end;

          end;

          

           A27: t <= 1 by Lm1;

          thus (1 / 2) <= t implies (f . t) = (Q . ((2 * t) - 1))

          proof

            assume

             A28: (1 / 2) <= t;

            then t in { r : (1 / 2) <= r & r <= 1 } by A27;

            then t in [.(1 / 2), 1.] by RCOMP_1:def 1;

            

            then (f . t) = (E2 . t) by A4, A16, FUNCT_4: 13

            .= (Q . ((2 * t) - 1)) by A5, A27, A28;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        let A,B be Path of a, c such that

         A29: for t be Point of I[01] holds (t <= (1 / 2) implies (A . t) = (P . (2 * t))) & ((1 / 2) <= t implies (A . t) = (Q . ((2 * t) - 1))) and

         A30: for t be Point of I[01] holds (t <= (1 / 2) implies (B . t) = (P . (2 * t))) & ((1 / 2) <= t implies (B . t) = (Q . ((2 * t) - 1)));

        

         A31: for x be object st x in ( dom A) holds (A . x) = (B . x)

        proof

          let x be object;

          assume

           A32: x in ( dom A);

          then

          reconsider y = x as Point of I[01] ;

          x in the carrier of I[01] by A32;

          then x in { r : 0 <= r & r <= 1 } by BORSUK_1: 40, RCOMP_1:def 1;

          then

          consider r9 be Real such that

           A33: r9 = x and 0 <= r9 and r9 <= 1;

          per cases ;

            suppose

             A34: r9 <= (1 / 2);

            

            then (A . y) = (P . (2 * r9)) by A29, A33

            .= (B . y) by A30, A33, A34;

            hence thesis;

          end;

            suppose

             A35: (1 / 2) < r9;

            

            then (A . y) = (Q . ((2 * r9) - 1)) by A29, A33

            .= (B . y) by A30, A33, A35;

            hence thesis;

          end;

        end;

        ( dom B) = the carrier of I[01] by FUNCT_2:def 1;

        then ( dom A) = ( dom B) by FUNCT_2:def 1;

        hence thesis by A31, FUNCT_1: 2;

      end;

    end

    registration

      let T be non empty TopSpace;

      let a be Point of T;

      cluster constant for Path of a, a;

      existence

      proof

        set IT = ( I[01] --> a);

        

         A1: (IT . 0 ) = a & (IT . 1) = a by BORSUK_1:def 14, BORSUK_1:def 15, FUNCOP_1: 7;

        (a,a) are_connected ;

        then

        reconsider IT as Path of a, a by A1, Def2;

        for n1,n2 be object st n1 in ( dom IT) & n2 in ( dom IT) holds (IT . n1) = (IT . n2)

        proof

          let n1,n2 be object;

          assume that

           A2: n1 in ( dom IT) and

           A3: n2 in ( dom IT);

          (IT . n1) = a by A2, FUNCOP_1: 7

          .= (IT . n2) by A3, FUNCOP_1: 7;

          hence thesis;

        end;

        then IT is constant by FUNCT_1:def 10;

        hence thesis;

      end;

    end

    ::$Canceled

    theorem :: BORSUK_2:5

    for T be non empty TopSpace, a be Point of T, P be constant Path of a, a holds P = ( I[01] --> a)

    proof

      let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;

      set IT = ( I[01] --> a);

      

       A1: ( dom P) = the carrier of I[01] by FUNCT_2:def 1;

      

       A2: (a,a) are_connected ;

      

       A3: for x be object st x in the carrier of I[01] holds (P . x) = (IT . x)

      proof

         0 in { r : 0 <= r & r <= 1 };

        then

         A4: 0 in the carrier of I[01] by BORSUK_1: 40, RCOMP_1:def 1;

        let x be object;

        assume

         A5: x in the carrier of I[01] ;

        (P . 0 ) = a by A2, Def2;

        

        then (P . x) = a by A1, A5, A4, FUNCT_1:def 10

        .= (IT . x) by A5, FUNCOP_1: 7;

        hence thesis;

      end;

      ( dom IT) = the carrier of I[01] by FUNCT_2:def 1;

      hence thesis by A1, A3, FUNCT_1: 2;

    end;

    theorem :: BORSUK_2:6

    

     Th5: for T be non empty TopSpace, a be Point of T, P be constant Path of a, a holds (P + P) = P

    proof

      let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;

      

       A1: the carrier of I[01] = ( dom P) by FUNCT_2:def 1;

      

       A2: for x be object st x in the carrier of I[01] holds (P . x) = ((P + P) . x)

      proof

        let x be object;

        assume

         A3: x in the carrier of I[01] ;

        then

        reconsider p = x as Point of I[01] ;

        x in { r : 0 <= r & r <= 1 } by A3, BORSUK_1: 40, RCOMP_1:def 1;

        then

        consider r be Real such that

         A4: r = x and

         A5: 0 <= r and

         A6: r <= 1;

        per cases ;

          suppose

           A7: r < (1 / 2);

          then

           A8: (r * 2) < ((1 / 2) * 2) by XREAL_1: 68;

          (2 * r) >= 0 by A5, XREAL_1: 127;

          then (2 * r) in { e where e be Real : 0 <= e & e <= 1 } by A8;

          then (2 * r) in the carrier of I[01] by BORSUK_1: 40, RCOMP_1:def 1;

          then (P . (2 * r)) = (P . p) by A1, FUNCT_1:def 10;

          hence thesis by A4, A7, Def5;

        end;

          suppose

           A9: r >= (1 / 2);

          then (r * 2) >= ((1 / 2) * 2) by XREAL_1: 64;

          then (2 * r) >= (1 + 0 );

          then

           A10: ((2 * r) - 1) >= 0 by XREAL_1: 19;

          (r * 2) <= (1 * 2) by A6, XREAL_1: 64;

          then ((2 * r) - 1) <= (2 - 1) by XREAL_1: 13;

          then ((2 * r) - 1) in { e where e be Real : 0 <= e & e <= 1 } by A10;

          then ((2 * r) - 1) in the carrier of I[01] by BORSUK_1: 40, RCOMP_1:def 1;

          then (P . ((2 * r) - 1)) = (P . p) by A1, FUNCT_1:def 10;

          hence thesis by A4, A9, Def5;

        end;

      end;

      ( dom (P + P)) = the carrier of I[01] by FUNCT_2:def 1;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    registration

      let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;

      cluster (P + P) -> constant;

      coherence by Th5;

    end

    definition

      let T be non empty TopSpace;

      let a,b be Point of T;

      let P be Path of a, b;

      assume

       A1: (a,b) are_connected ;

      :: BORSUK_2:def6

      func - P -> Path of b, a means

      : Def6: for t be Point of I[01] holds (it . t) = (P . (1 - t));

      existence

      proof

        set e = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))));

        reconsider f = (P * e) as Function of I[01] , T by TOPMETR: 20;

        

         A2: for t be Point of I[01] holds (f . t) = (P . (1 - t))

        proof

          let t be Point of I[01] ;

          reconsider ee = t as Point of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 20;

          

           A3: (( 0 ,1) (#) ) = 1 & ( (#) ( 0 ,1)) = 0 by TREAL_1:def 1, TREAL_1:def 2;

          t in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 20;

          then t in ( dom e) by FUNCT_2:def 1;

          

          then (f . t) = (P . (e . ee)) by FUNCT_1: 13

          .= (P . ((( 0 - 1) * t) + 1)) by A3, TREAL_1: 7

          .= (P . (1 - (1 * t)));

          hence thesis;

        end;

         0 in { r : 0 <= r & r <= 1 };

        then 0 in [. 0 , 1.] by RCOMP_1:def 1;

        then 0 in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 18;

        then

         A4: 0 in ( dom e) by FUNCT_2:def 1;

        (e . 0 ) = (e . ( (#) ( 0 ,1))) by TREAL_1:def 1

        .= (( 0 ,1) (#) ) by TREAL_1: 9

        .= 1 by TREAL_1:def 2;

        

        then

         A5: (f . 0 ) = (P . 1) by A4, FUNCT_1: 13

        .= b by A1, Def2;

        1 in { r : 0 <= r & r <= 1 };

        then 1 in [. 0 , 1.] by RCOMP_1:def 1;

        then 1 in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 18;

        then

         A6: 1 in ( dom e) by FUNCT_2:def 1;

        (e . 1) = (e . (( 0 ,1) (#) )) by TREAL_1:def 2

        .= ( (#) ( 0 ,1)) by TREAL_1: 9

        .= 0 by TREAL_1:def 1;

        

        then

         A7: (f . 1) = (P . 0 ) by A6, FUNCT_1: 13

        .= a by A1, Def2;

        

         A8: P is continuous & e is continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace ( 0 ,1)) by A1, Def2, TREAL_1: 8;

        then (b,a) are_connected by A5, A7, TOPMETR: 20;

        then

        reconsider f as Path of b, a by A5, A7, A8, Def2, TOPMETR: 20;

        take f;

        thus thesis by A2;

      end;

      uniqueness

      proof

        let R,Q be Path of b, a such that

         A9: for t be Point of I[01] holds (R . t) = (P . (1 - t)) and

         A10: for t be Point of I[01] holds (Q . t) = (P . (1 - t));

        

         A11: for x be object st x in the carrier of I[01] holds (R . x) = (Q . x)

        proof

          let x be object;

          assume x in the carrier of I[01] ;

          then

          reconsider x9 = x as Point of I[01] ;

          (R . x9) = (P . (1 - x9)) by A9

          .= (Q . x9) by A10;

          hence thesis;

        end;

        ( dom R) = the carrier of I[01] & the carrier of I[01] = ( dom Q) by FUNCT_2:def 1;

        hence thesis by A11, FUNCT_1: 2;

      end;

    end

    

     Lm4: for r be Real st 0 <= r & r <= 1 holds 0 <= (1 - r) & (1 - r) <= 1

    proof

      let r be Real;

      assume 0 <= r & r <= 1;

      then (1 - 1) <= (1 - r) & (1 - r) <= (1 - 0 ) by XREAL_1: 13;

      hence thesis;

    end;

    

     Lm5: for r be Real st r in the carrier of I[01] holds (1 - r) in the carrier of I[01]

    proof

      let r be Real;

      assume r in the carrier of I[01] ;

      then 0 <= r & r <= 1 by Lm1;

      then 0 <= (1 - r) & (1 - r) <= 1 by Lm4;

      hence thesis by Lm1;

    end;

    theorem :: BORSUK_2:7

    

     Th6: for T be non empty TopSpace, a be Point of T, P be constant Path of a, a holds ( - P) = P

    proof

      let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;

      

       A1: ( dom P) = the carrier of I[01] by FUNCT_2:def 1;

      

       A2: for x be object st x in the carrier of I[01] holds (P . x) = (( - P) . x)

      proof

        let x be object;

        assume

         A3: x in the carrier of I[01] ;

        then

        reconsider x2 = x as Real;

        reconsider x3 = (1 - x2) as Point of I[01] by A3, Lm5;

        (( - P) . x) = (P . x3) by A3, Def6

        .= (P . x) by A1, A3, FUNCT_1:def 10;

        hence thesis;

      end;

      ( dom ( - P)) = the carrier of I[01] by FUNCT_2:def 1;

      hence thesis by A1, A2, FUNCT_1: 2;

    end;

    registration

      let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;

      cluster ( - P) -> constant;

      coherence by Th6;

    end

    begin

    theorem :: BORSUK_2:8

    

     Th7: for X,Y be non empty TopSpace holds for A be Subset-Family of Y holds for f be Function of X, Y holds (f " ( union A)) = ( union (f " A))

    proof

      let X,Y be non empty TopSpace, A be Subset-Family of Y, f be Function of X, Y;

      thus (f " ( union A)) c= ( union (f " A))

      proof

        reconsider uA = ( union A) as Subset of Y;

        let x be object;

        assume

         A1: x in (f " ( union A));

        then (f . x) in uA by FUNCT_2: 38;

        then

        consider YY be set such that

         A2: (f . x) in YY and

         A3: YY in A by TARSKI:def 4;

        reconsider fY = (f " YY) as Subset of X;

        

         A4: fY in (f " A) by A3, FUNCT_2:def 9;

        x in (f " YY) by A1, A2, FUNCT_2: 38;

        hence thesis by A4, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union (f " A));

      then

      consider YY be set such that

       A5: x in YY and

       A6: YY in (f " A) by TARSKI:def 4;

      x in the carrier of X by A5, A6;

      then

       A7: x in ( dom f) by FUNCT_2:def 1;

      reconsider B1 = YY as Subset of X by A6;

      consider B be Subset of Y such that

       A8: B in A and

       A9: B1 = (f " B) by A6, FUNCT_2:def 9;

      (f . x) in B by A5, A9, FUNCT_1:def 7;

      then (f . x) in ( union A) by A8, TARSKI:def 4;

      hence thesis by A7, FUNCT_1:def 7;

    end;

    definition

      let S1,S2,T1,T2 be non empty TopSpace;

      let f be Function of S1, S2, g be Function of T1, T2;

      :: original: [:

      redefine

      func [:f,g:] -> Function of [:S1, T1:], [:S2, T2:] ;

      coherence

      proof

        set h = [:f, g:];

        ( rng h) c= [:the carrier of S2, the carrier of T2:];

        then

         A1: ( rng h) c= the carrier of [:S2, T2:] by BORSUK_1:def 2;

        ( dom h) = [:the carrier of S1, the carrier of T1:] by FUNCT_2:def 1

        .= the carrier of [:S1, T1:] by BORSUK_1:def 2;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: BORSUK_2:9

    

     Th8: for S1,S2,T1,T2 be non empty TopSpace, f be continuous Function of S1, T1, g be continuous Function of S2, T2, P1,P2 be Subset of [:T1, T2:] holds (P2 in ( Base-Appr P1) implies ( [:f, g:] " P2) is open)

    proof

      let S1,S2,T1,T2 be non empty TopSpace, f be continuous Function of S1, T1, g be continuous Function of S2, T2, P1,P2 be Subset of [:T1, T2:];

      assume P2 in ( Base-Appr P1);

      then

      consider X11 be Subset of T1, Y11 be Subset of T2 such that

       A1: P2 = [:X11, Y11:] and [:X11, Y11:] c= P1 and

       A2: X11 is open and

       A3: Y11 is open;

      ( [#] T1) <> {} ;

      then

       A4: (f " X11) is open by A2, TOPS_2: 43;

      ( [#] T2) <> {} ;

      then

       A5: (g " Y11) is open by A3, TOPS_2: 43;

      ( [:f, g:] " P2) = [:(f " X11), (g " Y11):] by A1, FUNCT_3: 73;

      hence thesis by A4, A5, BORSUK_1: 6;

    end;

    theorem :: BORSUK_2:10

    

     Th9: for S1,S2,T1,T2 be non empty TopSpace, f be continuous Function of S1, T1, g be continuous Function of S2, T2, P2 be Subset of [:T1, T2:] holds (P2 is open implies ( [:f, g:] " P2) is open)

    proof

      let S1,S2,T1,T2 be non empty TopSpace, f be continuous Function of S1, T1, g be continuous Function of S2, T2, P2 be Subset of [:T1, T2:];

      reconsider Kill = ( [:f, g:] " ( Base-Appr P2)) as Subset-Family of [:S1, S2:];

      for P be Subset of [:S1, S2:] holds P in Kill implies P is open

      proof

        let P be Subset of [:S1, S2:];

        assume P in Kill;

        then ex B be Subset of [:T1, T2:] st B in ( Base-Appr P2) & P = ( [:f, g:] " B) by FUNCT_2:def 9;

        hence thesis by Th8;

      end;

      then

       A1: Kill is open by TOPS_2:def 1;

      assume P2 is open;

      then P2 = ( union ( Base-Appr P2)) by BORSUK_1: 13;

      then ( [:f, g:] " P2 qua Subset of [:T1, T2:]) = ( union ( [:f, g:] " ( Base-Appr P2))) by Th7;

      hence thesis by A1, TOPS_2: 19;

    end;

    registration

      let S1,S2,T1,T2 be non empty TopSpace, f be continuous Function of S1, T1, g be continuous Function of S2, T2;

      cluster [:f, g:] -> continuous;

      coherence

      proof

        ( [#] [:T1, T2:]) <> {} & for P1 be Subset of [:T1, T2:] st P1 is open holds ( [:f, g:] " P1) is open by Th9;

        hence thesis by TOPS_2: 43;

      end;

    end

    registration

      let T1,T2 be T_0 TopSpace;

      cluster [:T1, T2:] -> T_0;

      coherence

      proof

        set T = [:T1, T2:];

        per cases ;

          suppose T1 is empty or T2 is empty;

          hence thesis;

        end;

          suppose that

           A1: T1 is non empty and

           A2: T2 is non empty;

          

           A3: the carrier of T is non empty by A1, A2;

          now

            let p,q be Point of T;

            assume

             A4: p <> q;

            q in the carrier of T by A3;

            then q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

            then

            consider z,v be object such that

             A5: z in the carrier of T1 and

             A6: v in the carrier of T2 and

             A7: q = [z, v] by ZFMISC_1:def 2;

            p in the carrier of T by A3;

            then p in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

            then

            consider x,y be object such that

             A8: x in the carrier of T1 and

             A9: y in the carrier of T2 and

             A10: p = [x, y] by ZFMISC_1:def 2;

            reconsider y, v as Point of T2 by A9, A6;

            reconsider x, z as Point of T1 by A8, A5;

            per cases ;

              suppose x <> z;

              then

              consider V1 be Subset of T1 such that

               A11: V1 is open and

               A12: x in V1 & not z in V1 or z in V1 & not x in V1 by A1, T_0TOPSP:def 7;

              set X = [:V1, ( [#] T2):];

               A13:

              now

                per cases by A12;

                  suppose x in V1 & not z in V1;

                  hence p in X & not q in X or q in X & not p in X by A9, A10, A7, ZFMISC_1: 87;

                end;

                  suppose z in V1 & not x in V1;

                  hence p in X & not q in X or q in X & not p in X by A10, A6, A7, ZFMISC_1: 87;

                end;

              end;

              X is open by A11, BORSUK_1: 6;

              hence ex X be Subset of T st X is open & (p in X & not q in X or q in X & not p in X) by A13;

            end;

              suppose x = z;

              then

              consider V1 be Subset of T2 such that

               A14: V1 is open and

               A15: y in V1 & not v in V1 or v in V1 & not y in V1 by A4, A10, A7, A2, T_0TOPSP:def 7;

              set X = [:( [#] T1), V1:];

               A16:

              now

                per cases by A15;

                  suppose y in V1 & not v in V1;

                  hence p in X & not q in X or q in X & not p in X by A8, A10, A7, ZFMISC_1: 87;

                end;

                  suppose v in V1 & not y in V1;

                  hence p in X & not q in X or q in X & not p in X by A10, A5, A7, ZFMISC_1: 87;

                end;

              end;

              X is open by A14, BORSUK_1: 6;

              hence ex X be Subset of T st X is open & (p in X & not q in X or q in X & not p in X) by A16;

            end;

          end;

          hence thesis;

        end;

      end;

    end

    registration

      let T1,T2 be T_1 TopSpace;

      cluster [:T1, T2:] -> T_1;

      coherence

      proof

        set T = [:T1, T2:];

        per cases ;

          suppose T1 is empty or T2 is empty;

          hence thesis;

        end;

          suppose T1 is non empty & T2 is non empty;

          then

           A1: the carrier of [:T1, T2:] is non empty;

          let p,q be Point of T;

          assume

           A2: p <> q;

          q in the carrier of T by A1;

          then q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

          then

          consider z,v be object such that

           A3: z in the carrier of T1 and

           A4: v in the carrier of T2 and

           A5: q = [z, v] by ZFMISC_1:def 2;

          p in the carrier of T by A1;

          then p in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

          then

          consider x,y be object such that

           A6: x in the carrier of T1 and

           A7: y in the carrier of T2 and

           A8: p = [x, y] by ZFMISC_1:def 2;

          reconsider y, v as Point of T2 by A7, A4;

          reconsider x, z as Point of T1 by A6, A3;

          per cases ;

            suppose x <> z;

            then

            consider Y,V be Subset of T1 such that

             A9: Y is open & V is open and

             A10: x in Y and

             A11: not z in Y and

             A12: z in V and

             A13: not x in V by URYSOHN1:def 7;

            set X = [:Y, ( [#] T2):], Z = [:V, ( [#] T2):];

            

             A14: ( not q in X) & not p in Z by A8, A5, A11, A13, ZFMISC_1: 87;

            

             A15: X is open & Z is open by A9, BORSUK_1: 6;

            p in X & q in Z by A7, A8, A4, A5, A10, A12, ZFMISC_1: 87;

            hence thesis by A15, A14;

          end;

            suppose x = z;

            then

            consider Y,V be Subset of T2 such that

             A16: Y is open & V is open and

             A17: y in Y and

             A18: not v in Y and

             A19: v in V and

             A20: not y in V by A2, A8, A5, URYSOHN1:def 7;

            reconsider Y, V as Subset of T2;

            set X = [:( [#] T1), Y:], Z = [:( [#] T1), V:];

            

             A21: ( not p in Z) & not q in X by A8, A5, A18, A20, ZFMISC_1: 87;

            

             A22: X is open & Z is open by A16, BORSUK_1: 6;

            p in X & q in Z by A6, A8, A3, A5, A17, A19, ZFMISC_1: 87;

            hence thesis by A22, A21;

          end;

        end;

      end;

    end

    registration

      let T1,T2 be T_2 TopSpace;

      cluster [:T1, T2:] -> T_2;

      coherence

      proof

        set T = [:T1, T2:];

        per cases ;

          suppose T1 is empty or T2 is empty;

          hence thesis;

        end;

          suppose T1 is non empty & T2 is non empty;

          then

           A1: the carrier of T is non empty;

          let p,q be Point of T;

          assume

           A2: p <> q;

          q in the carrier of T by A1;

          then q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

          then

          consider z,v be object such that

           A3: z in the carrier of T1 and

           A4: v in the carrier of T2 and

           A5: q = [z, v] by ZFMISC_1:def 2;

          p in the carrier of T by A1;

          then p in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;

          then

          consider x,y be object such that

           A6: x in the carrier of T1 and

           A7: y in the carrier of T2 and

           A8: p = [x, y] by ZFMISC_1:def 2;

          reconsider y, v as Point of T2 by A7, A4;

          reconsider x, z as Point of T1 by A6, A3;

          per cases ;

            suppose x <> z;

            then

            consider Y,V be Subset of T1 such that

             A9: Y is open & V is open and

             A10: x in Y & z in V and

             A11: Y misses V by PRE_TOPC:def 10;

            reconsider Y, V as Subset of T1;

            reconsider X = [:Y, ( [#] T2):], Z = [:V, ( [#] T2):] as Subset of T;

            

             A12: X misses Z by A11, ZFMISC_1: 104;

            

             A13: X is open & Z is open by A9, BORSUK_1: 6;

            p in X & q in Z by A7, A8, A4, A5, A10, ZFMISC_1: 87;

            hence thesis by A13, A12;

          end;

            suppose x = z;

            then

            consider Y,V be Subset of T2 such that

             A14: Y is open & V is open and

             A15: y in Y & v in V and

             A16: Y misses V by A2, A8, A5, PRE_TOPC:def 10;

            reconsider Y, V as Subset of T2;

            reconsider X = [:( [#] T1), Y:], Z = [:( [#] T1), V:] as Subset of T;

            

             A17: X misses Z by A16, ZFMISC_1: 104;

            

             A18: X is open & Z is open by A14, BORSUK_1: 6;

            p in X & q in Z by A6, A8, A3, A5, A15, ZFMISC_1: 87;

            hence thesis by A18, A17;

          end;

        end;

      end;

    end

    registration

      cluster I[01] -> compact T_2;

      coherence

      proof

         I[01] = ( TopSpaceMetr ( Closed-Interval-MSpace ( 0 ,1))) by TOPMETR: 20, TOPMETR:def 7;

        hence thesis by HEINE: 4, PCOMPS_1: 34, TOPMETR: 20;

      end;

    end

    definition

      let T be non empty TopStruct;

      let a,b be Point of T;

      let P,Q be Path of a, b;

      :: BORSUK_2:def7

      pred P,Q are_homotopic means ex f be Function of [: I[01] , I[01] :], T st f is continuous & for t be Point of I[01] holds (f . (t, 0 )) = (P . t) & (f . (t,1)) = (Q . t) & (f . ( 0 ,t)) = a & (f . (1,t)) = b;

      symmetry

      proof

        ( id the carrier of I[01] ) = ( id I[01] );

        then

        reconsider fA = ( id the carrier of I[01] ) as continuous Function of I[01] , I[01] ;

        set LL = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))));

        reconsider fB = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1)))) as continuous Function of I[01] , I[01] by TOPMETR: 20, TREAL_1: 8;

        let P,Q be Path of a, b;

        given f be Function of [: I[01] , I[01] :], T such that

         A1: f is continuous and

         A2: for s be Point of I[01] holds (f . (s, 0 )) = (P . s) & (f . (s,1)) = (Q . s) & (f . ( 0 ,s)) = a & (f . (1,s)) = b;

        set F = [:fA, fB:];

        reconsider ff = (f * F) as Function of [: I[01] , I[01] :], T;

        

         A3: ( dom ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))))) = the carrier of I[01] by FUNCT_2:def 1, TOPMETR: 20;

        

         A4: for s be Point of I[01] holds (ff . (s, 0 )) = (Q . s) & (ff . (s,1)) = (P . s)

        proof

          let s be Point of I[01] ;

          

           A5: for t be Point of I[01] , t9 be Real st t = t9 holds (LL . t) = (1 - t9)

          proof

            let t be Point of I[01] , t9 be Real;

            assume

             A6: t = t9;

            reconsider ee = t as Point of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 20;

            

             A7: (( 0 ,1) (#) ) = 1 & ( (#) ( 0 ,1)) = 0 by TREAL_1:def 1, TREAL_1:def 2;

            (LL . t) = (LL . ee)

            .= ((( 0 - 1) * t9) + 1) by A6, A7, TREAL_1: 7

            .= (1 - (1 * t9));

            hence thesis;

          end;

          

           A8: ( dom ( id the carrier of I[01] )) = the carrier of I[01] ;

          

           A9: ( dom F) = [:( dom ( id the carrier of I[01] )), ( dom ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))))):] by FUNCT_3:def 8;

          

           A10: 1 in ( dom ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))))) by A3, Lm1;

          then

           A11: [s, 1] in ( dom F) by A9, ZFMISC_1: 87;

          

           A12: 0 in ( dom LL) by A3, Lm1;

          then

           A13: [s, 0 ] in ( dom F) by A9, ZFMISC_1: 87;

          (F . (s,1)) = [(( id the carrier of I[01] ) . s), (( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1)))) . 1)] by A8, A10, FUNCT_3:def 8

          .= [s, (LL . 1[01] )]

          .= [s, (1 - 1)] by A5

          .= [s, 0 ];

          

          then

           A14: (ff . (s,1)) = (f . (s, 0 )) by A11, FUNCT_1: 13

          .= (P . s) by A2;

          (F . (s, 0 )) = [(( id the carrier of I[01] ) . s), (LL . 0 )] by A8, A12, FUNCT_3:def 8

          .= [s, (LL . 0[01] )]

          .= [s, (1 - 0 )] by A5

          .= [s, 1];

          

          then (ff . (s, 0 )) = (f . (s,1)) by A13, FUNCT_1: 13

          .= (Q . s) by A2;

          hence thesis by A14;

        end;

        

         A15: for t be Point of I[01] holds (ff . ( 0 ,t)) = a & (ff . (1,t)) = b

        proof

          let t be Point of I[01] ;

          reconsider tt = t as Real;

          for t be Point of I[01] , t9 be Real st t = t9 holds (LL . t) = (1 - t9)

          proof

            let t be Point of I[01] , t9 be Real;

            assume

             A16: t = t9;

            reconsider ee = t as Point of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 20;

            

             A17: (( 0 ,1) (#) ) = 1 & ( (#) ( 0 ,1)) = 0 by TREAL_1:def 1, TREAL_1:def 2;

            (LL . t) = (LL . ee)

            .= ((( 0 - 1) * t9) + 1) by A16, A17, TREAL_1: 7

            .= (1 - (1 * t9));

            hence thesis;

          end;

          then

           A18: (( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1)))) . t) = (1 - tt);

          reconsider t9 = (1 - tt) as Point of I[01] by Lm5;

          

           A19: ( dom ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))))) = the carrier of I[01] by FUNCT_2:def 1, TOPMETR: 20;

          

           A20: 0 in ( dom ( id the carrier of I[01] )) by Lm1;

          

           A21: ( dom F) = [:( dom ( id the carrier of I[01] )), ( dom ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))))):] by FUNCT_3:def 8;

          then

           A22: [ 0 , t] in ( dom F) by A19, A20, ZFMISC_1: 87;

          

           A23: 1 in ( dom ( id the carrier of I[01] )) by Lm1;

          then

           A24: [1, t] in ( dom F) by A19, A21, ZFMISC_1: 87;

          (F . (1,t)) = [(( id the carrier of I[01] ) . 1), (( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1)))) . t)] by A19, A23, FUNCT_3:def 8

          .= [1, (1 - tt)] by A18, A23, FUNCT_1: 18;

          

          then

           A25: (ff . (1,t)) = (f . (1,t9)) by A24, FUNCT_1: 13

          .= b by A2;

          (F . ( 0 ,t)) = [(( id the carrier of I[01] ) . 0 ), (( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1)))) . t)] by A19, A20, FUNCT_3:def 8

          .= [ 0 , (1 - tt)] by A18, A20, FUNCT_1: 18;

          

          then (ff . ( 0 ,t)) = (f . ( 0 ,t9)) by A22, FUNCT_1: 13

          .= a by A2;

          hence thesis by A25;

        end;

        ff is continuous by A1, TOPS_2: 46;

        hence thesis by A4, A15;

      end;

    end

    ::$Canceled

    theorem :: BORSUK_2:12

    

     Th10: for T be non empty TopSpace, a,b be Point of T, P be Path of a, b st (a,b) are_connected holds (P,P) are_homotopic

    proof

      let T be non empty TopSpace;

      let a,b be Point of T;

      let P be Path of a, b;

      defpred Z[ object, object] means $2 = (P . ($1 `1 ));

      

       A1: for x be object st x in [:the carrier of I[01] , the carrier of I[01] :] holds ex y be object st y in the carrier of T & Z[x, y]

      proof

        let x be object;

        assume x in [:the carrier of I[01] , the carrier of I[01] :];

        then (x `1 ) in the carrier of I[01] by MCART_1: 10;

        hence thesis by FUNCT_2: 5;

      end;

      consider f be Function of [:the carrier of I[01] , the carrier of I[01] :], the carrier of T such that

       A2: for x be object st x in [:the carrier of I[01] , the carrier of I[01] :] holds Z[x, (f . x)] from FUNCT_2:sch 1( A1);

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

      then

      reconsider f as Function of the carrier of [: I[01] , I[01] :], the carrier of T;

      reconsider f as Function of [: I[01] , I[01] :], T;

      assume

       A3: (a,b) are_connected ;

      

       A4: for t be Point of I[01] holds (f . ( 0 ,t)) = a & (f . (1,t)) = b

      proof

        let t be Point of I[01] ;

        set t0 = [ 0 , t], t1 = [1, t];

         0 in the carrier of I[01] by Lm1;

        then t0 in [:the carrier of I[01] , the carrier of I[01] :] by ZFMISC_1: 87;

        then

         A5: (f . t0) = (P . (t0 `1 )) by A2;

        1 in the carrier of I[01] by Lm1;

        then t1 in [:the carrier of I[01] , the carrier of I[01] :] by ZFMISC_1: 87;

        then

         A6: (f . t1) = (P . (t1 `1 )) by A2;

        (P . 0 ) = a & (P . 1) = b by A3, Def2;

        hence thesis by A5, A6;

      end;

      

       A7: for W be Point of [: I[01] , I[01] :], G be a_neighborhood of (f . W) holds ex H be a_neighborhood of W st (f .: H) c= G

      proof

        let W be Point of [: I[01] , I[01] :], G be a_neighborhood of (f . W);

        W in the carrier of [: I[01] , I[01] :];

        then

         A8: W in [:the carrier of I[01] , the carrier of I[01] :] by BORSUK_1:def 2;

        then

        reconsider W1 = (W `1 ) as Point of I[01] by MCART_1: 10;

        

         A9: ex x,y be object st [x, y] = W by A8, RELAT_1:def 1;

        reconsider G9 = G as a_neighborhood of (P . W1) by A2, A8;

        the carrier of I[01] c= the carrier of I[01] ;

        then

        reconsider AI = the carrier of I[01] as Subset of I[01] ;

        AI = ( [#] I[01] );

        then ( Int AI) = the carrier of I[01] by TOPS_1: 15;

        then

         A10: (W `2 ) in ( Int AI) by A8, MCART_1: 10;

        P is continuous by A3, Def2;

        then

        consider H be a_neighborhood of W1 such that

         A11: (P .: H) c= G9;

        set HH = [:H, the carrier of I[01] :];

        HH c= [:the carrier of I[01] , the carrier of I[01] :] by ZFMISC_1: 95;

        then

        reconsider HH as Subset of [: I[01] , I[01] :] by BORSUK_1:def 2;

        W1 in ( Int H) & ( Int HH) = [:( Int H), ( Int AI):] by BORSUK_1: 7, CONNSP_2:def 1;

        then W in ( Int HH) by A9, A10, ZFMISC_1:def 2;

        then

        reconsider HH as a_neighborhood of W by CONNSP_2:def 1;

        take HH;

        (f .: HH) c= G

        proof

          let a be object;

          assume a in (f .: HH);

          then

          consider b be object such that

           A12: b in ( dom f) and

           A13: b in HH and

           A14: a = (f . b) by FUNCT_1:def 6;

          reconsider b as Point of [: I[01] , I[01] :] by A12;

          

           A15: ( dom P) = the carrier of I[01] & (b `1 ) in H by A13, FUNCT_2:def 1, MCART_1: 10;

          ( dom f) = [:the carrier of I[01] , the carrier of I[01] :] by FUNCT_2:def 1;

          then (f . b) = (P . (b `1 )) by A2, A12;

          then (f . b) in (P .: H) by A15, FUNCT_1:def 6;

          hence thesis by A11, A14;

        end;

        hence thesis;

      end;

      take f;

      for s be Point of I[01] holds (f . (s, 0 )) = (P . s) & (f . (s,1)) = (P . s)

      proof

        let s be Point of I[01] ;

        reconsider s0 = [s, 0 ], s1 = [s, 1] as set;

        1 in the carrier of I[01] by Lm1;

        then s1 in [:the carrier of I[01] , the carrier of I[01] :] by ZFMISC_1: 87;

        then

         A16: Z[s1, (f . s1)] by A2;

         0 in the carrier of I[01] by Lm1;

        then s0 in [:the carrier of I[01] , the carrier of I[01] :] by ZFMISC_1: 87;

        then Z[s0, (f . s0)] by A2;

        hence thesis by A16;

      end;

      hence thesis by A7, A4;

    end;

    definition

      let T be non empty pathwise_connected TopSpace;

      let a,b be Point of T;

      let P,Q be Path of a, b;

      :: original: are_homotopic

      redefine

      pred P,Q are_homotopic ;

      reflexivity by Th10, Def3;

    end

    theorem :: BORSUK_2:13

    for G be non empty TopSpace, w1,w2,w3 be Point of G, h1,h2 be Function of I[01] , G st h1 is continuous & w1 = (h1 . 0 ) & w2 = (h1 . 1) & h2 is continuous & w2 = (h2 . 0 ) & w3 = (h2 . 1) holds ex h3 be Function of I[01] , G st h3 is continuous & w1 = (h3 . 0 ) & w3 = (h3 . 1) & ( rng h3) c= (( rng h1) \/ ( rng h2)) by Lm3;

    theorem :: BORSUK_2:14

    for T be non empty TopSpace, a,b,c be Point of T, G1 be Path of a, b, G2 be Path of b, c st G1 is continuous & G2 is continuous & (G1 . 0 ) = a & (G1 . 1) = b & (G2 . 0 ) = b & (G2 . 1) = c holds (G1 + G2) is continuous & ((G1 + G2) . 0 ) = a & ((G1 + G2) . 1) = c

    proof

      let T be non empty TopSpace, a,b,c be Point of T, G1 be Path of a, b, G2 be Path of b, c;

      assume G1 is continuous & G2 is continuous & (G1 . 0 ) = a & (G1 . 1) = b & (G2 . 0 ) = b & (G2 . 1) = c;

      then ex h be Function of I[01] , T st h is continuous & (h . 0 ) = a & (h . 1) = c & ( rng h) c= (( rng G1) \/ ( rng G2)) by Lm3;

      then (a,c) are_connected ;

      hence thesis by Def2;

    end;

    registration

      let T be non empty TopSpace;

      cluster non empty compact connected for Subset of T;

      existence

      proof

        take { the Element of T};

        thus thesis;

      end;

    end

    theorem :: BORSUK_2:15

    

     Th13: for T be non empty TopSpace, a,b be Point of T st (ex f be Function of I[01] , T st f is continuous & (f . 0 ) = a & (f . 1) = b) holds ex g be Function of I[01] , T st g is continuous & (g . 0 ) = b & (g . 1) = a

    proof

      set e = ( L[01] ((( 0 ,1) (#) ),( (#) ( 0 ,1))));

      let T be non empty TopSpace, a,b be Point of T;

      given P be Function of I[01] , T such that

       A1: P is continuous and

       A2: (P . 0 ) = a & (P . 1) = b;

      set f = (P * e);

      reconsider f as Function of I[01] , T by TOPMETR: 20;

      take f;

      e is continuous Function of ( Closed-Interval-TSpace ( 0 ,1)), ( Closed-Interval-TSpace ( 0 ,1)) by TREAL_1: 8;

      hence f is continuous by A1, TOPMETR: 20;

      

       A3: (e . 1) = (e . (( 0 ,1) (#) )) by TREAL_1:def 2

      .= ( (#) ( 0 ,1)) by TREAL_1: 9

      .= 0 by TREAL_1:def 1;

      1 in [. 0 , 1.] by XXREAL_1: 1;

      then 1 in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 18;

      then

       A4: 1 in ( dom e) by FUNCT_2:def 1;

       0 in [. 0 , 1.] by XXREAL_1: 1;

      then 0 in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by TOPMETR: 18;

      then

       A5: 0 in ( dom e) by FUNCT_2:def 1;

      (e . 0 ) = (e . ( (#) ( 0 ,1))) by TREAL_1:def 1

      .= (( 0 ,1) (#) ) by TREAL_1: 9

      .= 1 by TREAL_1:def 2;

      hence thesis by A2, A3, A5, A4, FUNCT_1: 13;

    end;

    registration

      cluster I[01] -> pathwise_connected;

      coherence

      proof

        let a,b be Point of I[01] ;

        per cases ;

          suppose

           A1: a <= b;

          then

          reconsider B = [.a, b.] as non empty Subset of I[01] by BORSUK_1: 40, XXREAL_1: 1, XXREAL_2:def 12;

           0 <= a & b <= 1 by BORSUK_1: 43;

          then

           A2: ( Closed-Interval-TSpace (a,b)) = ( I[01] | B) by A1, TOPMETR: 24;

          the carrier of ( I[01] | B) c= the carrier of I[01] by BORSUK_1: 1;

          then

          reconsider g = ( L[01] (( (#) (a,b)),((a,b) (#) ))) as Function of the carrier of I[01] , the carrier of I[01] by A2, FUNCT_2: 7, TOPMETR: 20;

          reconsider g as Function of I[01] , I[01] ;

          take g;

          thus g is continuous by A1, A2, PRE_TOPC: 26, TOPMETR: 20, TREAL_1: 8;

           0 = ( (#) ( 0 ,1)) by TREAL_1:def 1;

          

          hence (g . 0 ) = ( (#) (a,b)) by A1, TREAL_1: 9

          .= a by A1, TREAL_1:def 1;

          1 = (( 0 ,1) (#) ) by TREAL_1:def 2;

          

          hence (g . 1) = ((a,b) (#) ) by A1, TREAL_1: 9

          .= b by A1, TREAL_1:def 2;

        end;

          suppose

           A3: b <= a;

          then

          reconsider B = [.b, a.] as non empty Subset of I[01] by BORSUK_1: 40, XXREAL_1: 1, XXREAL_2:def 12;

           0 <= b & a <= 1 by BORSUK_1: 43;

          then

           A4: ( Closed-Interval-TSpace (b,a)) = ( I[01] | B) by A3, TOPMETR: 24;

          the carrier of ( I[01] | B) c= the carrier of I[01] by BORSUK_1: 1;

          then

          reconsider g = ( L[01] (( (#) (b,a)),((b,a) (#) ))) as Function of the carrier of I[01] , the carrier of I[01] by A4, FUNCT_2: 7, TOPMETR: 20;

          reconsider g as Function of I[01] , I[01] ;

           0 = ( (#) ( 0 ,1)) by TREAL_1:def 1;

          

          then

           A5: (g . 0 ) = ( (#) (b,a)) by A3, TREAL_1: 9

          .= b by A3, TREAL_1:def 1;

          1 = (( 0 ,1) (#) ) by TREAL_1:def 2;

          

          then

           A6: (g . 1) = ((b,a) (#) ) by A3, TREAL_1: 9

          .= a by A3, TREAL_1:def 2;

          

           A7: g is continuous by A3, A4, PRE_TOPC: 26, TOPMETR: 20, TREAL_1: 8;

          then (b,a) are_connected by A5, A6;

          then

          reconsider P = g as Path of b, a by A7, A5, A6, Def2;

          take ( - P);

          ex t be Function of I[01] , I[01] st t is continuous & (t . 0 ) = a & (t . 1) = b by A7, A5, A6, Th13;

          then (a,b) are_connected ;

          hence thesis by Def2;

        end;

      end;

    end