topalg_2.miz

    begin

    reserve n for Element of NAT ,

a,b for Real;

    registration

      let n be Nat;

      cluster non empty convex for Subset of ( TOP-REAL n);

      existence

      proof

        set a = the Point of ( TOP-REAL n);

        take ( LSeg (a,a));

        thus thesis;

      end;

    end

    definition

      let n be Element of NAT , T be SubSpace of ( TOP-REAL n);

      :: TOPALG_2:def1

      attr T is convex means

      : Def1: ( [#] T) is convex Subset of ( TOP-REAL n);

    end

    registration

      let n be Element of NAT ;

      cluster convex -> pathwise_connected for non empty SubSpace of ( TOP-REAL n);

      coherence

      proof

        let T be non empty SubSpace of ( TOP-REAL n);

        assume

         A1: ( [#] T) is convex Subset of ( TOP-REAL n);

        let a,b be Point of T;



         A2: the carrier of T is Subset of ( TOP-REAL n) by TSEP_1: 1;

        a in the carrier of T & b in the carrier of T;

        then

        reconsider a1 = a, b1 = b as Point of ( TOP-REAL n) by A2;

        per cases ;

          suppose

           A3: a1 <> b1;

          ( [#] (( TOP-REAL n) | ( LSeg (a1,b1)))) = ( LSeg (a1,b1)) by PRE_TOPC:def 5;

          then

           A4: the carrier of (( TOP-REAL n) | ( LSeg (a1,b1))) c= the carrier of T by A1, JORDAN1:def 1;

          then

           A5: (( TOP-REAL n) | ( LSeg (a1,b1))) is SubSpace of T by TSEP_1: 4;

          ( LSeg (a1,b1)) is_an_arc_of (a1,b1) by A3, TOPREAL1: 9;

          then

          consider h be Function of I[01] , (( TOP-REAL n) | ( LSeg (a1,b1))) such that

           A6: h is being_homeomorphism and

           A7: (h . 0 ) = a1 & (h . 1) = b1 by TOPREAL1:def 1;

          reconsider f = h as Function of I[01] , T by A4, FUNCT_2: 7;

          take f;

          h is continuous by A6, TOPS_2:def 5;

          hence f is continuous by A5, PRE_TOPC: 26;

          thus thesis by A7;

        end;

          suppose a1 = b1;

          hence (a,b) are_connected ;

        end;

      end;

    end

    registration

      let n be Element of NAT ;

      cluster strict non empty convex for SubSpace of ( TOP-REAL n);

      existence

      proof

         the TopStruct of ( TOP-REAL n) is SubSpace of the TopStruct of ( TOP-REAL n) by TSEP_1: 2;

        then

        reconsider T = the TopStruct of ( TOP-REAL n) as SubSpace of ( TOP-REAL n) by PRE_TOPC: 35;

        take T;

        thus T is strict non empty;

        ( [#] ( TOP-REAL n)) = ( [#] the TopStruct of ( TOP-REAL n));

        hence ( [#] T) is convex Subset of ( TOP-REAL n);

      end;

    end

    theorem :: TOPALG_2:1

    for X be non empty TopSpace, Y be non empty SubSpace of X, x1,x2 be Point of X, y1,y2 be Point of Y, f be Path of y1, y2 st x1 = y1 & x2 = y2 & (y1,y2) are_connected holds f is Path of x1, x2

    proof

      let X be non empty TopSpace, Y be non empty SubSpace of X, x1,x2 be Point of X, y1,y2 be Point of Y, f be Path of y1, y2 such that

       A1: x1 = y1 & x2 = y2 and

       A2: (y1,y2) are_connected ;

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

      then

      reconsider g = f as Function of I[01] , X by FUNCT_2: 7;

      f is continuous by A2, BORSUK_2:def 2;

      then

       A3: g is continuous by PRE_TOPC: 26;



       A4: (g . 0 ) = x1 & (g . 1) = x2 by A1, A2, BORSUK_2:def 2;

      then (x1,x2) are_connected by A3;

      hence thesis by A4, A3, BORSUK_2:def 2;

    end;

    set I = the carrier of I[01] ;



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



     Lm2: the carrier of [:( TOP-REAL 1), I[01] :] = [:the carrier of ( TOP-REAL 1), I:] by BORSUK_1:def 2;



     Lm3: the carrier of [: R^1 , I[01] :] = [:the carrier of R^1 , I:] by BORSUK_1:def 2;



     Lm4: ( dom ( id I[01] )) = I by FUNCT_2:def 1;

    definition

      let n be Element of NAT , T be non empty convex SubSpace of ( TOP-REAL n), P,Q be Function of I[01] , T;

      :: TOPALG_2:def2

      func ConvexHomotopy (P,Q) -> Function of [: I[01] , I[01] :], T means

      : Def2: for s,t be Element of I[01] , a1,b1 be Point of ( TOP-REAL n) st a1 = (P . s) & b1 = (Q . s) holds (it . (s,t)) = (((1 - t) * a1) + (t * b1));

      existence

      proof

        defpred P[ Element of I, Element of I, set] means ex a1,b1 be Point of ( TOP-REAL n) st a1 = (P . $1) & b1 = (Q . $1) & $3 = (((1 - $2) * a1) + ($2 * b1));



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

        proof

          let x,y be Element of I;



           A2: the carrier of T is Subset of ( TOP-REAL n) by TSEP_1: 1;

          (P . x) in the carrier of T & (Q . x) in the carrier of T;

          then

          reconsider a1 = (P . x), b1 = (Q . x) as Point of ( TOP-REAL n) by A2;

          set z = (((1 - y) * a1) + (y * b1));



           A3: y <= 1 by BORSUK_1: 43;

          ( [#] T) is convex Subset of ( TOP-REAL n) by Def1;

          then

           A4: ( LSeg (a1,b1)) c= ( [#] T) by JORDAN1:def 1;

          y is Real & 0 <= y by BORSUK_1: 43;

          then z in ( LSeg (a1,b1)) by A3;

          hence thesis by A4;

        end;

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

         A5: for x,y be Element of I holds P[x, y, (F . (x,y))] from BINOP_1:sch 3( A1);

        reconsider F as Function of [: I[01] , I[01] :], T by Lm1;

        take F;

        let x,y be Element of I;

        ex a1,b1 be Point of ( TOP-REAL n) st a1 = (P . x) & b1 = (Q . x) & (F . (x,y)) = (((1 - y) * a1) + (y * b1)) by A5;

        hence thesis;

      end;

      uniqueness

      proof

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

         A6: for s,t be Element of I[01] , a1,b1 be Point of ( TOP-REAL n) st a1 = (P . s) & b1 = (Q . s) holds (f . (s,t)) = (((1 - t) * a1) + (t * b1)) and

         A7: for s,t be Element of I[01] , a1,b1 be Point of ( TOP-REAL n) st a1 = (P . s) & b1 = (Q . s) holds (g . (s,t)) = (((1 - t) * a1) + (t * b1));

        for s,t be Element of I holds (f . (s,t)) = (g . (s,t))

        proof

          let s,t be Element of I;

          reconsider a1 = (P . s), b1 = (Q . s) as Point of ( TOP-REAL n) by PRE_TOPC: 25;

          (f . (s,t)) = (((1 - t) * a1) + (t * b1)) by A6;

          hence thesis by A7;

        end;

        hence f = g by Lm1, BINOP_1: 2;

      end;

    end



     Lm5: for T be non empty convex SubSpace of ( TOP-REAL n), P,Q be continuous Function of I[01] , T holds ( ConvexHomotopy (P,Q)) is continuous

    proof

      let T be non empty convex SubSpace of ( TOP-REAL n), P,Q be continuous Function of I[01] , T;

      set F = ( ConvexHomotopy (P,Q));



       A1: the carrier of T is Subset of ( TOP-REAL n) by TSEP_1: 1;

      then

      reconsider G = F as Function of [: I[01] , I[01] :], ( TOP-REAL n) by FUNCT_2: 7;

      reconsider P1 = P, Q1 = Q as Function of I[01] , ( TOP-REAL n) by A1, FUNCT_2: 7;

      set E = the carrier of ( TOP-REAL n);

      set PI = [:P, ( id I[01] ):];

      set QI = [:Q, ( id I[01] ):];

      reconsider P1, Q1 as continuous Function of I[01] , ( TOP-REAL n) by PRE_TOPC: 26;

      set P1I = [:P1, ( id I[01] ):];

      set Q1I = [:Q1, ( id I[01] ):];

      deffunc Fb( Element of E, Element of I) = ($2 * $1);

      deffunc Fa( Element of E, Element of I) = ((1 - $2) * $1);

      consider Pa be Function of [:E, I:], E such that

       A2: for x be Element of E, i be Element of I holds (Pa . (x,i)) = Fa(x,i) from BINOP_1:sch 4;

      consider Pb be Function of [:E, I:], E such that

       A3: for x be Element of E, i be Element of I holds (Pb . (x,i)) = Fb(x,i) from BINOP_1:sch 4;

      the carrier of [:( TOP-REAL n), I[01] :] = [:E, I:] by BORSUK_1:def 2;

      then

      reconsider Pa, Pb as Function of [:( TOP-REAL n), I[01] :], ( TOP-REAL n);



       A4: Pb is continuous by A3, TOPALG_1: 18;

      Pa is continuous by A2, TOPALG_1: 17;

      then

      consider g be Function of [: I[01] , I[01] :], ( TOP-REAL n) such that

       A5: for r be Point of [: I[01] , I[01] :] holds (g . r) = (((Pa * P1I) . r) + ((Pb * Q1I) . r)) and

       A6: g is continuous by A4, JGRAPH_6: 12;



       A7: for p be Point of [: I[01] , I[01] :] holds (G . p) = (((Pa * P1I) . p) + ((Pb * Q1I) . p))

      proof



         A8: ( dom Q) = I by FUNCT_2:def 1;



         A9: ( dom P) = I by FUNCT_2:def 1;

        let p be Point of [: I[01] , I[01] :];

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

         A10: p = [s, t] by BORSUK_1: 10;

        reconsider a1 = (P . s), b1 = (Q . s) as Point of ( TOP-REAL n) by PRE_TOPC: 25;



         A11: (F . (s,t)) = (((1 - t) * a1) + (t * b1)) by Def2;



         A12: (( id I[01] ) . t) = t by FUNCT_1: 18;



         A13: ((Pb * QI) . p) = (Pb . (QI . (s,t))) by A10, FUNCT_2: 15

        .= (Pb . ((Q . s),t)) by A8, A12, Lm4, FUNCT_3:def 8

        .= (t * (Q1 . s)) by A3;

        ((Pa * PI) . p) = (Pa . (PI . (s,t))) by A10, FUNCT_2: 15

        .= (Pa . ((P . s),t)) by A9, A12, Lm4, FUNCT_3:def 8

        .= ((1 - t) * (P1 . s)) by A2;

        hence thesis by A10, A13, A11;

      end;

      for p be Point of [: I[01] , I[01] :] holds (G . p) = (g . p)

      proof

        let p be Point of [: I[01] , I[01] :];



        thus (G . p) = (((Pa * P1I) . p) + ((Pb * Q1I) . p)) by A7

        .= (g . p) by A5;

      end;

      hence thesis by A6, FUNCT_2: 63, PRE_TOPC: 27;

    end;



     Lm6: for T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b holds for s be Point of I[01] holds (( ConvexHomotopy (P,Q)) . (s, 0 )) = (P . s) & (( ConvexHomotopy (P,Q)) . (s,1)) = (Q . s) & for t be Point of I[01] holds (( ConvexHomotopy (P,Q)) . ( 0 ,t)) = a & (( ConvexHomotopy (P,Q)) . (1,t)) = b

    proof

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

      let T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b;

      set F = ( ConvexHomotopy (P,Q));

      let s be Point of I[01] ;

      reconsider a1 = (P . s), b1 = (Q . s) as Point of ( TOP-REAL n) by PRE_TOPC: 25;



       A1: (P . x0) = a by BORSUK_2:def 4;

      (F . (s,x0)) = (((1 - x0) * a1) + (x0 * b1)) by Def2;



      hence (F . (s, 0 )) = (a1 + ( 0 * b1)) by RLVECT_1:def 8

      .= (a1 + ( 0. ( TOP-REAL n))) by RLVECT_1: 10

      .= (P . s) by RLVECT_1: 4;

      (F . (s,x1)) = (((1 - x1) * a1) + (x1 * b1)) by Def2;



      hence (F . (s,1)) = (( 0. ( TOP-REAL n)) + (1 * b1)) by RLVECT_1: 10

      .= (( 0. ( TOP-REAL n)) + b1) by RLVECT_1:def 8

      .= (Q . s) by RLVECT_1: 4;

      reconsider a1 = (P . x0), b1 = (Q . x0) as Point of ( TOP-REAL n) by PRE_TOPC: 25;

      let t be Point of I[01] ;

      (F . ( 0 ,t)) = (((1 - t) * a1) + (t * b1)) & (Q . x0) = a by Def2, BORSUK_2:def 4;



      hence (F . ( 0 ,t)) = (((1 * a1) - (t * a1)) + (t * a1)) by A1, RLVECT_1: 35

      .= (1 * a1) by RLVECT_4: 1

      .= a by A1, RLVECT_1:def 8;



       A2: (Q . x1) = b by BORSUK_2:def 4;

      reconsider a1 = (P . x1), b1 = (Q . x1) as Point of ( TOP-REAL n) by PRE_TOPC: 25;



       A3: (P . x1) = b by BORSUK_2:def 4;

      (F . (1,t)) = (((1 - t) * a1) + (t * b1)) by Def2;



      hence (F . (1,t)) = (((1 * a1) - (t * b1)) + (t * a1)) by A3, A2, RLVECT_1: 35

      .= (1 * b1) by A3, A2, RLVECT_4: 1

      .= b by A2, RLVECT_1:def 8;

    end;

    theorem :: TOPALG_2:2



     Th2: for T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b holds (P,Q) are_homotopic

    proof

      let T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b;

      take F = ( ConvexHomotopy (P,Q));

      thus F is continuous by Lm5;

      thus thesis by Lm6;

    end;

    registration

      let n be Element of NAT , T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b;

      cluster -> continuous for Homotopy of P, Q;

      coherence

      proof

        let F be Homotopy of P, Q;

        (P,Q) are_homotopic by Th2;

        hence thesis by BORSUK_6:def 11;

      end;

    end

    theorem :: TOPALG_2:3



     Th3: for T be non empty convex SubSpace of ( TOP-REAL n), a be Point of T, C be Loop of a holds the carrier of ( pi_1 (T,a)) = {( Class (( EqRel (T,a)),C))}

    proof

      let T be non empty convex SubSpace of ( TOP-REAL n), a be Point of T, C be Loop of a;

      set E = ( EqRel (T,a));

      hereby

        let x be object;

        assume x in the carrier of ( pi_1 (T,a));

        then

        consider P be Loop of a such that

         A1: x = ( Class (E,P)) by TOPALG_1: 47;

        (P,C) are_homotopic by Th2;

        then x = ( Class (E,C)) by A1, TOPALG_1: 46;

        hence x in {( Class (E,C))} by TARSKI:def 1;

      end;

      let x be object;

      assume x in {( Class (E,C))};

      then

       A2: x = ( Class (E,C)) by TARSKI:def 1;

      C in ( Loops a) by TOPALG_1:def 1;

      then x in ( Class E) by A2, EQREL_1:def 3;

      hence thesis by TOPALG_1:def 5;

    end;

    registration

      let n be Element of NAT , T be non empty convex SubSpace of ( TOP-REAL n), a be Point of T;

      cluster ( pi_1 (T,a)) -> trivial;

      coherence

      proof

        set C = the constant Loop of a;

        set E = ( EqRel (T,a));

        the carrier of ( pi_1 (T,a)) = ( Class E) by TOPALG_1:def 5;

        then {( Class (E,C))} = ( Class E) by Th3;

        hence thesis by TOPALG_1:def 5;

      end;

    end

    begin

    theorem :: TOPALG_2:4



     Th4: ( |[a]| /. 1) = a

    proof

      reconsider y = a as Element of REAL by XREAL_0:def 1;



      thus ( |[a]| /. 1) = ( <*y*> /. 1)

      .= a by FINSEQ_4: 16;

    end;

    theorem :: TOPALG_2:5

    a <= b implies [.a, b.] = { (((1 - l) * a) + (l * b)) where l be Real : 0 <= l & l <= 1 }

    proof

      set X = { (((1 - l) * a) + (l * b)) where l be Real : 0 <= l & l <= 1 };

      assume

       A1: a <= b;

      hereby

        let x be object;

        assume

         A2: x in [.a, b.];

        then

        reconsider y = x as Real;



         A3: a <= y & y <= b by A2, XXREAL_1: 1;

        per cases by A1, XXREAL_0: 1;

          suppose a < b;

          then

           A4: (b - a) > (b - b) by XREAL_1: 15;

          reconsider l = ((y - a) / (b - a)) as Real;

          l in the carrier of ( Closed-Interval-TSpace ( 0 ,1)) by A3, BORSUK_6: 2;

          then l in [. 0 , 1.] by TOPMETR: 18;

          then

           A5: 0 <= l & l <= 1 by XXREAL_1: 1;

          (((1 - l) * a) + (l * b)) = (a + (l * (b - a)))

          .= (a + (y - a)) by A4, XCMPLX_1: 87

          .= y;

          hence x in X by A5;

        end;

          suppose a = b;

          then (((1 - 1) * a) + (1 * b)) = y by A3, XXREAL_0: 1;

          hence x in X;

        end;

      end;

      let x be object;

      assume x in X;

      then

      consider l be Real such that

       A6: x = (((1 - l) * a) + (l * b)) and

       A7: 0 <= l & l <= 1;

      a <= (((1 - l) * a) + (l * b)) & (((1 - l) * a) + (l * b)) <= b by A1, A7, XREAL_1: 172, XREAL_1: 173;

      hence thesis by A6, XXREAL_1: 1;

    end;

    theorem :: TOPALG_2:6



     Th6: for F be Function of [: R^1 , I[01] :], R^1 st for x be Point of R^1 , i be Point of I[01] holds (F . (x,i)) = ((1 - i) * x) holds F is continuous

    proof

      deffunc Fa( Element of ( TOP-REAL 1), Element of I) = ((1 - $2) * $1);

      consider G be Function of [:the carrier of ( TOP-REAL 1), I:], the carrier of ( TOP-REAL 1) such that

       A1: for x be Point of ( TOP-REAL 1), i be Point of I[01] holds (G . (x,i)) = Fa(x,i) from BINOP_1:sch 4;

      reconsider G as Function of [:( TOP-REAL 1), I[01] :], ( TOP-REAL 1) by Lm2;

      consider f be Function of ( TOP-REAL 1), R^1 such that

       A2: for p be Element of ( TOP-REAL 1) holds (f . p) = (p /. 1) by JORDAN2B: 1;



       A3: f is being_homeomorphism by A2, JORDAN2B: 28;

      then

       A4: f is continuous by TOPS_2:def 5;

      let F be Function of [: R^1 , I[01] :], R^1 such that

       A5: for x be Point of R^1 , i be Point of I[01] holds (F . (x,i)) = ((1 - i) * x);



       A6: for x be Point of [: R^1 , I[01] :] holds (F . x) = ((f * (G * [:(f " ), ( id I[01] ):])) . x)

      proof

        reconsider ff = f as Function;

        let x be Point of [: R^1 , I[01] :];

        consider a be Point of R^1 , b be Point of I[01] such that

         A7: x = [a, b] by BORSUK_1: 10;



         A8: ( dom (f " )) = the carrier of R^1 by FUNCT_2:def 1;

        ( rng f) = ( [#] R^1 ) by A3, TOPS_2:def 5;

        then

         A9: f is onto by FUNCT_2:def 3;



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

        set g = (ff " );

        consider z be Real such that

         A11: ((1 - b) * ((f " ) . a)) = <*z*> by JORDAN2B: 20;

        reconsider zz = z as Element of REAL by XREAL_0:def 1;



         A12: <*a*> = |[a]|;

        then

        reconsider w = <*a*> as Element of ( REAL 1) by EUCLID: 22;



         A13: ff is one-to-one by A3, TOPS_2:def 5;

        (f . <*a*>) = ( |[a]| /. 1) by A2

        .= a by Th4;

        then <*a*> = (g . a) by A10, A13, A12, FUNCT_1: 32;

        then

         A14: w = ((f /" ) . a) by A9, A13, TOPS_2:def 4;



         A15: <*z*> = ((1 - b) * ((f /" ) . a)) by A11

        .= ((1 - b) * w) by A14

        .= <*((1 - b) * a)*> by RVSUM_1: 47;



        thus ((f * (G * [:(f " ), ( id I[01] ):])) . x) = (f . ((G * [:(f " ), ( id I[01] ):]) . x)) by FUNCT_2: 15

        .= (f . (G . ( [:(f " ), ( id I[01] ):] . (a,b)))) by A7, FUNCT_2: 15

        .= (f . (G . (((f " ) . a),(( id I[01] ) . b)))) by A8, Lm4, FUNCT_3:def 8

        .= (f . (G . (((f " ) . a),b))) by FUNCT_1: 18

        .= (f . ((1 - b) * ((f " ) . a))) by A1

        .= (((1 - b) * ((f " ) . a)) /. 1) by A2

        .= ( <*zz*> /. 1) by A11

        .= z by FINSEQ_4: 16

        .= ((1 - b) * a) by A15, FINSEQ_1: 76

        .= (F . (a,b)) by A5

        .= (F . x) by A7;

      end;

      (f " ) is continuous by A3, TOPS_2:def 5;

      then

       A16: [:(f " ), ( id I[01] ):] is continuous;

      G is continuous by A1, TOPALG_1: 17;

      hence thesis by A4, A16, A6, FUNCT_2: 63;

    end;

    theorem :: TOPALG_2:7



     Th7: for F be Function of [: R^1 , I[01] :], R^1 st for x be Point of R^1 , i be Point of I[01] holds (F . (x,i)) = (i * x) holds F is continuous

    proof

      deffunc Fa( Element of ( TOP-REAL 1), Element of I) = ($2 * $1);

      consider G be Function of [:the carrier of ( TOP-REAL 1), I:], the carrier of ( TOP-REAL 1) such that

       A1: for x be Point of ( TOP-REAL 1), i be Point of I[01] holds (G . (x,i)) = Fa(x,i) from BINOP_1:sch 4;

      reconsider G as Function of [:( TOP-REAL 1), I[01] :], ( TOP-REAL 1) by Lm2;

      consider f be Function of ( TOP-REAL 1), R^1 such that

       A2: for p be Element of ( TOP-REAL 1) holds (f . p) = (p /. 1) by JORDAN2B: 1;



       A3: f is being_homeomorphism by A2, JORDAN2B: 28;

      then

       A4: f is continuous by TOPS_2:def 5;

      let F be Function of [: R^1 , I[01] :], R^1 such that

       A5: for x be Point of R^1 , i be Point of I[01] holds (F . (x,i)) = (i * x);



       A6: for x be Point of [: R^1 , I[01] :] holds (F . x) = ((f * (G * [:(f " ), ( id I[01] ):])) . x)

      proof

        reconsider ff = f as Function;

        let x be Point of [: R^1 , I[01] :];

        consider a be Point of R^1 , b be Point of I[01] such that

         A7: x = [a, b] by BORSUK_1: 10;



         A8: ( dom (f " )) = the carrier of R^1 by FUNCT_2:def 1;

        ( rng f) = ( [#] R^1 ) by A3, TOPS_2:def 5;

        then

         A9: f is onto by FUNCT_2:def 3;



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

        set g = (ff " );

        consider z be Real such that

         A11: (b * ((f " ) . a)) = <*z*> by JORDAN2B: 20;

        reconsider z as Element of REAL by XREAL_0:def 1;



         A12: <*a*> = |[a]|;

        then

        reconsider w = <*a*> as Element of ( REAL 1) by EUCLID: 22;



         A13: ff is one-to-one by A3, TOPS_2:def 5;

        (f . <*a*>) = ( |[a]| /. 1) by A2

        .= a by Th4;

        then <*a*> = (g . a) by A10, A13, A12, FUNCT_1: 32;

        then

         A14: w = ((f /" ) . a) by A9, A13, TOPS_2:def 4;



         A15: <*z*> = (b * ((f /" ) . a)) by A11

        .= (b * w) by A14

        .= <*(b * a)*> by RVSUM_1: 47;



        thus ((f * (G * [:(f " ), ( id I[01] ):])) . x) = (f . ((G * [:(f " ), ( id I[01] ):]) . x)) by FUNCT_2: 15

        .= (f . (G . ( [:(f " ), ( id I[01] ):] . (a,b)))) by A7, FUNCT_2: 15

        .= (f . (G . (((f " ) . a),(( id I[01] ) . b)))) by A8, Lm4, FUNCT_3:def 8

        .= (f . (G . (((f " ) . a),b))) by FUNCT_1: 18

        .= (f . (b * ((f " ) . a))) by A1

        .= ((b * ((f " ) . a)) /. 1) by A2

        .= ( <*z*> /. 1) by A11

        .= z by FINSEQ_4: 16

        .= (b * a) by A15, FINSEQ_1: 76

        .= (F . (a,b)) by A5

        .= (F . x) by A7;

      end;

      (f " ) is continuous by A3, TOPS_2:def 5;

      then

       A16: [:(f " ), ( id I[01] ):] is continuous;

      G is continuous by A1, TOPALG_1: 18;

      hence thesis by A4, A16, A6, FUNCT_2: 63;

    end;

    registration

      cluster non empty interval for Subset of R^1 ;

      existence by TOPMETR: 17;

    end

    registration

      let T be real-membered TopStruct;

      cluster interval for Subset of T;

      existence

      proof

        take ( {} T);

        thus thesis;

      end;

    end

    definition

      let T be real-membered TopStruct;

      :: TOPALG_2:def3

      attr T is interval means

      : Def3: ( [#] T) is interval;

    end



     Lm7: for T be SubSpace of R^1 st T = R^1 holds T is interval by TOPMETR: 17;

    registration

      cluster strict non empty interval for SubSpace of R^1 ;

      existence

      proof

        reconsider T = R^1 as strict non empty SubSpace of R^1 by TSEP_1: 2;

        take T;

        thus thesis by Lm7;

      end;

    end

    definition

      :: original: R^1

      redefine

      func R^1 -> interval SubSpace of R^1 ;

      coherence by Lm7, TSEP_1: 2;

    end

    theorem :: TOPALG_2:8



     Th8: for T be non empty interval SubSpace of R^1 , a,b be Point of T holds [.a, b.] c= the carrier of T

    proof

      let T be non empty interval SubSpace of R^1 , a,b be Point of T;

      reconsider a1 = a, b1 = b as Point of R^1 by PRE_TOPC: 25;

      ( [#] T) is interval Subset of T by Def3;

      then [.a1, b1.] c= the carrier of T by XXREAL_2:def 12;

      hence thesis;

    end;

    registration

      cluster interval -> pathwise_connected for non empty SubSpace of R^1 ;

      coherence

      proof

        let T be non empty SubSpace of R^1 such that

         A1: T is interval;

        let a,b be Point of T;

        per cases ;

          suppose

           A2: a <= b;

          set f = ( L[01] (( (#) (a,b)),((a,b) (#) )));

          set X = ( Closed-Interval-TSpace (a,b));



           A3: the carrier of X = [.a, b.] by A2, TOPMETR: 18;

           [.a, b.] c= the carrier of T by A1, Th8;

          then

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

          take f;

          the carrier of X is Subset of R^1 by TSEP_1: 1;

          then

          reconsider g = f as Function of I[01] , R^1 by FUNCT_2: 7, TOPMETR: 20;

          ( L[01] (( (#) (a,b)),((a,b) (#) ))) is continuous by A2, TREAL_1: 8;

          then g is continuous by PRE_TOPC: 26, TOPMETR: 20;

          hence f is continuous by PRE_TOPC: 27;



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

          .= ( (#) (a,b)) by A2, TREAL_1: 9

          .= a by A2, TREAL_1:def 1;



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

          .= ((a,b) (#) ) by A2, TREAL_1: 9

          .= b by A2, TREAL_1:def 2;

        end;

          suppose

           A4: b <= a;

          set f = ( L[01] (((b,a) (#) ),( (#) (b,a))));

          set X = ( Closed-Interval-TSpace (b,a));



           A5: the carrier of X = [.b, a.] by A4, TOPMETR: 18;

           [.b, a.] c= the carrier of T by A1, Th8;

          then

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

          take f;

          the carrier of X is Subset of R^1 by TSEP_1: 1;

          then

          reconsider g = f as Function of I[01] , R^1 by FUNCT_2: 7, TOPMETR: 20;

          ( L[01] (((b,a) (#) ),( (#) (b,a)))) is continuous by A4, TREAL_1: 8;

          then g is continuous by PRE_TOPC: 26, TOPMETR: 20;

          hence f is continuous by PRE_TOPC: 27;



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

          .= ((b,a) (#) ) by A4, TREAL_1: 9

          .= a by A4, TREAL_1:def 2;



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

          .= ( (#) (b,a)) by A4, TREAL_1: 9

          .= b by A4, TREAL_1:def 1;

        end;

      end;

    end

    theorem :: TOPALG_2:9



     Th9: a <= b implies ( Closed-Interval-TSpace (a,b)) is interval

    proof

      set X = ( Closed-Interval-TSpace (a,b));

      assume a <= b;

      then [.a, b.] = ( [#] X) by TOPMETR: 18;

      hence ( [#] X) is interval;

    end;

    theorem :: TOPALG_2:10



     Th10: I[01] is interval by Th9, TOPMETR: 20;

    theorem :: TOPALG_2:11

    a <= b implies ( Closed-Interval-TSpace (a,b)) is pathwise_connected

    proof

      assume a <= b;

      then

      reconsider X = ( Closed-Interval-TSpace (a,b)) as non empty interval SubSpace of R^1 by Th9;

      X is pathwise_connected;

      hence thesis;

    end;

    definition

      let T be non empty interval SubSpace of R^1 , P,Q be Function of I[01] , T;

      :: TOPALG_2:def4

      func R1Homotopy (P,Q) -> Function of [: I[01] , I[01] :], T means

      : Def4: for s,t be Element of I[01] holds (it . (s,t)) = (((1 - t) * (P . s)) + (t * (Q . s)));

      existence

      proof

        defpred P[ Element of I, Element of I, set] means $3 = (((1 - $2) * (P . $1)) + ($2 * (Q . $1)));



         A1: for m,n be Element of I holds ex z be Element of T st P[m, n, z]

        proof

          let m,n be Element of I;



           A2: 0 <= n by BORSUK_1: 43;

          set z = (((1 - n) * (P . m)) + (n * (Q . m)));



           A3: n <= 1 by BORSUK_1: 43;

          per cases ;

            suppose (P . m) <= (Q . m);

            then (P . m) <= z & z <= (Q . m) by A2, A3, XREAL_1: 172, XREAL_1: 173;

            then

             A4: z in [.(P . m), (Q . m).] by XXREAL_1: 1;

             [.(P . m), (Q . m).] c= the carrier of T by Th8;

            hence thesis by A4;

          end;

            suppose

             A5: (P . m) > (Q . m);

            (1 - 1) <= (1 - n) by A3, XREAL_1: 13;

            then ((1 - n) * (Q . m)) <= ((1 - n) * (P . m)) by A5, XREAL_1: 64;

            then

             A6: (((1 - n) * (Q . m)) + (n * (Q . m))) <= (((1 - n) * (P . m)) + (n * (Q . m))) by XREAL_1: 6;



             A7: [.(Q . m), (P . m).] c= the carrier of T by Th8;

            ((Q . m) - (P . m)) < ((Q . m) - (Q . m)) by A5, XREAL_1: 15;

            then (n * ((Q . m) - (P . m))) <= (n * 0 ) by A2, XREAL_1: 131;

            then ((P . m) + (n * ((Q . m) - (P . m)))) <= ((P . m) + 0 ) by XREAL_1: 6;

            then z in [.(Q . m), (P . m).] by A6, XXREAL_1: 1;

            hence thesis by A7;

          end;

        end;

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

         A8: for m,n be Element of I holds P[m, n, (F . (m,n))] from BINOP_1:sch 3( A1);

        reconsider F as Function of [: I[01] , I[01] :], T by Lm1;

        take F;

        let s,t be Element of I;

        thus thesis by A8;

      end;

      uniqueness

      proof

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

         A9: for s,t be Element of I[01] holds (f . (s,t)) = (((1 - t) * (P . s)) + (t * (Q . s))) and

         A10: for s,t be Element of I[01] holds (g . (s,t)) = (((1 - t) * (P . s)) + (t * (Q . s)));

        for s,t be Element of I holds (f . (s,t)) = (g . (s,t))

        proof

          let s,t be Element of I;



          thus (f . (s,t)) = (((1 - t) * (P . s)) + (t * (Q . s))) by A9

          .= (g . (s,t)) by A10;

        end;

        hence f = g by Lm1, BINOP_1: 2;

      end;

    end



     Lm8: for T be non empty interval SubSpace of R^1 , P,Q be continuous Function of I[01] , T holds ( R1Homotopy (P,Q)) is continuous

    proof

      set E = the carrier of R^1 ;

      let T be non empty interval SubSpace of R^1 , P,Q be continuous Function of I[01] , T;

      set F = ( R1Homotopy (P,Q));

      set PI = [:P, ( id I[01] ):];

      set QI = [:Q, ( id I[01] ):];

      defpred Fa[ Element of E, Element of I, set] means $3 = ((1 - $2) * $1);

      defpred Fb[ Element of E, Element of I, set] means $3 = ($2 * $1);



       A1: the carrier of T is Subset of R^1 by TSEP_1: 1;

      then

      reconsider G = F as Function of [: I[01] , I[01] :], R^1 by FUNCT_2: 7;

      reconsider P1 = P, Q1 = Q as Function of I[01] , R^1 by A1, FUNCT_2: 7;

      reconsider P1, Q1 as continuous Function of I[01] , R^1 by PRE_TOPC: 26;

      set P1I = [:P1, ( id I[01] ):];

      set Q1I = [:Q1, ( id I[01] ):];



       A2: for x be Element of E holds for y be Element of I holds ex z be Element of E st Fa[x, y, z]

      proof

        let x be Element of E;

        let y be Element of I;

        ((1 - y) * x) in REAL by XREAL_0:def 1;

        then

        reconsider z = ((1 - y) * x) as Element of E by TOPMETR: 17;

        take z;

        thus thesis;

      end;

      consider Pa be Function of [:E, I:], E such that

       A3: for x be Element of E, i be Element of I holds Fa[x, i, (Pa . (x,i))] from BINOP_1:sch 3( A2);



       A4: for x be Element of E holds for y be Element of I holds ex z be Element of E st Fb[x, y, z]

      proof

        let x be Element of E, y be Element of I;

        (y * x) in REAL by XREAL_0:def 1;

        hence thesis by TOPMETR: 17;

      end;

      consider Pb be Function of [:E, I:], E such that

       A5: for x be Element of E, i be Element of I holds Fb[x, i, (Pb . (x,i))] from BINOP_1:sch 3( A4);

      reconsider Pa, Pb as Function of [: R^1 , I[01] :], R^1 by Lm3;



       A6: Pb is continuous by A5, Th7;

      Pa is continuous by A3, Th6;

      then

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

       A7: for p be Point of [: I[01] , I[01] :], r1,r2 be Real st ((Pa * P1I) . p) = r1 & ((Pb * Q1I) . p) = r2 holds (g . p) = (r1 + r2) and

       A8: g is continuous by A6, JGRAPH_2: 19;



       A9: for p be Point of [: I[01] , I[01] :] holds (G . p) = (((Pa * P1I) . p) + ((Pb * Q1I) . p))

      proof



         A10: ( dom Q) = I by FUNCT_2:def 1;



         A11: ( dom P) = I by FUNCT_2:def 1;

        let p be Point of [: I[01] , I[01] :];

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

         A12: p = [s, t] by BORSUK_1: 10;

        reconsider a1 = (P . s), b1 = (Q . s) as Point of R^1 by PRE_TOPC: 25;



         A13: (P . s) in the carrier of T;



         A14: (F . (s,t)) = (((1 - t) * a1) + (t * b1)) by Def4;



         A15: (Q . s) in the carrier of T;



         A16: (( id I[01] ) . t) = t by FUNCT_1: 18;



         A17: ((Pb * QI) . p) = (Pb . (QI . (s,t))) by A12, FUNCT_2: 15

        .= (Pb . ((Q . s),t)) by A10, A16, Lm4, FUNCT_3:def 8

        .= (t * (Q . s)) by A1, A5, A15;

        ((Pa * PI) . p) = (Pa . (PI . (s,t))) by A12, FUNCT_2: 15

        .= (Pa . ((P . s),t)) by A11, A16, Lm4, FUNCT_3:def 8

        .= ((1 - t) * (P . s)) by A1, A3, A13;

        hence thesis by A12, A17, A14;

      end;

      for p be Point of [: I[01] , I[01] :] holds (G . p) = (g . p)

      proof

        let p be Point of [: I[01] , I[01] :];



        thus (G . p) = (((Pa * P1I) . p) + ((Pb * Q1I) . p)) by A9

        .= (g . p) by A7;

      end;

      hence thesis by A8, FUNCT_2: 63, PRE_TOPC: 27;

    end;



     Lm9: for T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b holds for s be Point of I[01] holds (( R1Homotopy (P,Q)) . (s, 0 )) = (P . s) & (( R1Homotopy (P,Q)) . (s,1)) = (Q . s) & for t be Point of I[01] holds (( R1Homotopy (P,Q)) . ( 0 ,t)) = a & (( R1Homotopy (P,Q)) . (1,t)) = b

    proof

      let T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b;

      set F = ( R1Homotopy (P,Q));

      let s be Point of I[01] ;



       A1: (P . 0[01] ) = a & (Q . 0[01] ) = a by BORSUK_2:def 4;



      thus (F . (s, 0 )) = (((1 - 0 ) * (P . s)) + ( 0 * (Q . s))) by Def4, BORSUK_1:def 14

      .= (P . s);



      thus (F . (s,1)) = (((1 - 1) * (P . s)) + (1 * (Q . s))) by Def4, BORSUK_1:def 15

      .= (Q . s);

      let t be Point of I[01] ;



      thus (F . ( 0 ,t)) = (((1 - t) * (P . 0[01] )) + (t * (Q . 0[01] ))) by Def4

      .= a by A1;



       A2: (P . 1[01] ) = b & (Q . 1[01] ) = b by BORSUK_2:def 4;



      thus (F . (1,t)) = (((1 - t) * (P . 1[01] )) + (t * (Q . 1[01] ))) by Def4

      .= b by A2;

    end;

    theorem :: TOPALG_2:12



     Th12: for T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b holds (P,Q) are_homotopic

    proof

      let T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b;

      take F = ( R1Homotopy (P,Q));

      thus F is continuous by Lm8;

      thus thesis by Lm9;

    end;

    registration

      let T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b;

      cluster -> continuous for Homotopy of P, Q;

      coherence

      proof

        let F be Homotopy of P, Q;

        (P,Q) are_homotopic by Th12;

        hence thesis by BORSUK_6:def 11;

      end;

    end

    theorem :: TOPALG_2:13



     Th13: for T be non empty interval SubSpace of R^1 , a be Point of T, C be Loop of a holds the carrier of ( pi_1 (T,a)) = {( Class (( EqRel (T,a)),C))}

    proof

      let T be non empty interval SubSpace of R^1 , a be Point of T, C be Loop of a;

      set E = ( EqRel (T,a));

      hereby

        let x be object;

        assume x in the carrier of ( pi_1 (T,a));

        then

        consider P be Loop of a such that

         A1: x = ( Class (E,P)) by TOPALG_1: 47;

        (P,C) are_homotopic by Th12;

        then x = ( Class (E,C)) by A1, TOPALG_1: 46;

        hence x in {( Class (E,C))} by TARSKI:def 1;

      end;

      let x be object;

      assume x in {( Class (E,C))};

      then

       A2: x = ( Class (E,C)) by TARSKI:def 1;

      C in ( Loops a) by TOPALG_1:def 1;

      then x in ( Class E) by A2, EQREL_1:def 3;

      hence thesis by TOPALG_1:def 5;

    end;

    registration

      let T be non empty interval SubSpace of R^1 , a be Point of T;

      cluster ( pi_1 (T,a)) -> trivial;

      coherence

      proof

        set C = the constant Loop of a;

        set E = ( EqRel (T,a));

        the carrier of ( pi_1 (T,a)) = ( Class E) by TOPALG_1:def 5;

        then {( Class (E,C))} = ( Class E) by Th13;

        hence thesis by TOPALG_1:def 5;

      end;

    end

    theorem :: TOPALG_2:14

    a <= b implies for x,y be Point of ( Closed-Interval-TSpace (a,b)), P,Q be Path of x, y holds (P,Q) are_homotopic

    proof

      assume

       A1: a <= b;

      let x,y be Point of ( Closed-Interval-TSpace (a,b)), P,Q be Path of x, y;

      ( Closed-Interval-TSpace (a,b)) is interval by A1, Th9;

      hence thesis by Th12;

    end;

    theorem :: TOPALG_2:15

    a <= b implies for x be Point of ( Closed-Interval-TSpace (a,b)), C be Loop of x holds the carrier of ( pi_1 (( Closed-Interval-TSpace (a,b)),x)) = {( Class (( EqRel (( Closed-Interval-TSpace (a,b)),x)),C))}

    proof

      assume

       A1: a <= b;

      let x be Point of ( Closed-Interval-TSpace (a,b)), C be Loop of x;

      ( Closed-Interval-TSpace (a,b)) is interval by A1, Th9;

      hence thesis by Th13;

    end;

    theorem :: TOPALG_2:16

    for x,y be Point of I[01] , P,Q be Path of x, y holds (P,Q) are_homotopic by Th10, Th12;

    theorem :: TOPALG_2:17

    for x be Point of I[01] , C be Loop of x holds the carrier of ( pi_1 ( I[01] ,x)) = {( Class (( EqRel ( I[01] ,x)),C))} by Th10, Th13;

    registration

      let x be Point of I[01] ;

      cluster ( pi_1 ( I[01] ,x)) -> trivial;

      coherence by Th10;

    end

    registration

      let n;

      let T be non empty convex SubSpace of ( TOP-REAL n), P,Q be continuous Function of I[01] , T;

      cluster ( ConvexHomotopy (P,Q)) -> continuous;

      coherence by Lm5;

    end

    theorem :: TOPALG_2:18

    for n be Element of NAT , T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b holds ( ConvexHomotopy (P,Q)) is Homotopy of P, Q

    proof

      let n be Element of NAT , T be non empty convex SubSpace of ( TOP-REAL n), a,b be Point of T, P,Q be Path of a, b;

      thus (P,Q) are_homotopic by Th2;

      thus ( ConvexHomotopy (P,Q)) is continuous;

      thus thesis by Lm6;

    end;

    registration

      let T be non empty interval SubSpace of R^1 , P,Q be continuous Function of I[01] , T;

      cluster ( R1Homotopy (P,Q)) -> continuous;

      coherence by Lm8;

    end

    theorem :: TOPALG_2:19

    for T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b holds ( R1Homotopy (P,Q)) is Homotopy of P, Q

    proof

      let T be non empty interval SubSpace of R^1 , a,b be Point of T, P,Q be Path of a, b;

      thus (P,Q) are_homotopic by Th12;

      thus ( R1Homotopy (P,Q)) is continuous;

      thus thesis by Lm9;

    end;