topalg_1.miz



    begin

    reserve p,q,x,y for Real,

n for Nat;

    theorem :: TOPALG_1:1

    for G,H be set, g be Function of G, H, h be Function of H, G st (h * g) = ( id G) & (g * h) = ( id H) holds h is bijective by FUNCT_2: 23;

    theorem :: TOPALG_1:2

    

     Th2: for X be Subset of I[01] , a be Point of I[01] st X = ].a, 1.] holds (X ` ) = [. 0 , a.]

    proof

      set I = the carrier of I[01] ;

      let X be Subset of I[01] , a be Point of I[01] such that

       A1: X = ].a, 1.];

      set Y = [. 0 , a.];

      

       A2: (X ` ) = (I \ X) by SUBSET_1:def 4;

      hereby

        let x be object;

        assume

         A3: x in (X ` );

        then

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

         not x in X by A2, A3, XBOOLE_0:def 5;

        then

         A4: y <= a or y > 1 by A1, XXREAL_1: 2;

         0 <= y by BORSUK_1: 43;

        hence x in Y by A4, BORSUK_1: 43, XXREAL_1: 1;

      end;

      let x be object;

      assume

       A5: x in Y;

      then

      reconsider y = x as Real;

      

       A6: 0 <= y by A5, XXREAL_1: 1;

      

       A7: y <= a by A5, XXREAL_1: 1;

      a <= 1 by BORSUK_1: 43;

      then y <= 1 by A7, XXREAL_0: 2;

      then

       A8: y in I by A6, BORSUK_1: 43;

       not y in X by A1, A7, XXREAL_1: 2;

      hence thesis by A2, A8, XBOOLE_0:def 5;

    end;

    theorem :: TOPALG_1:3

    

     Th3: for X be Subset of I[01] , a be Point of I[01] st X = [. 0 , a.[ holds (X ` ) = [.a, 1.]

    proof

      set I = the carrier of I[01] ;

      let X be Subset of I[01] , a be Point of I[01] such that

       A1: X = [. 0 , a.[;

      set Y = [.a, 1.];

      

       A2: (X ` ) = (I \ X) by SUBSET_1:def 4;

      hereby

        let x be object;

        assume

         A3: x in (X ` );

        then

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

         not x in X by A2, A3, XBOOLE_0:def 5;

        then

         A4: y >= a or y < 0 by A1, XXREAL_1: 3;

        y <= 1 by BORSUK_1: 43;

        hence x in Y by A4, BORSUK_1: 43, XXREAL_1: 1;

      end;

      let x be object;

      assume

       A5: x in Y;

      then

      reconsider y = x as Real;

      

       A6: a <= y by A5, XXREAL_1: 1;

      then

       A7: not y in X by A1, XXREAL_1: 3;

      

       A8: 0 <= a by BORSUK_1: 43;

      y <= 1 by A5, XXREAL_1: 1;

      then y in I by A6, A8, BORSUK_1: 43;

      hence thesis by A2, A7, XBOOLE_0:def 5;

    end;

    theorem :: TOPALG_1:4

    

     Th4: for X be Subset of I[01] , a be Point of I[01] st X = ].a, 1.] holds X is open

    proof

      let X be Subset of I[01] , a be Point of I[01] such that

       A1: X = ].a, 1.];

      set Y = [. 0 , a.];

      Y c= the carrier of I[01]

      proof

        let x be object;

        

         A2: a <= 1 by BORSUK_1: 43;

        assume

         A3: x in Y;

        then

        reconsider x as Real;

        

         A4: 0 <= x by A3, XXREAL_1: 1;

        x <= a by A3, XXREAL_1: 1;

        then x <= 1 by A2, XXREAL_0: 2;

        hence thesis by A4, BORSUK_1: 43;

      end;

      then

      reconsider Y as Subset of I[01] ;

      Y is closed & (X ` ) = Y by A1, Th2, BORSUK_4: 23;

      hence thesis by TOPS_1: 4;

    end;

    theorem :: TOPALG_1:5

    

     Th5: for X be Subset of I[01] , a be Point of I[01] st X = [. 0 , a.[ holds X is open

    proof

      let X be Subset of I[01] , a be Point of I[01] such that

       A1: X = [. 0 , a.[;

      set Y = [.a, 1.];

      Y c= the carrier of I[01]

      proof

        let x be object;

        

         A2: 0 <= a by BORSUK_1: 43;

        assume

         A3: x in Y;

        then

        reconsider x as Real;

        x <= 1 & a <= x by A3, XXREAL_1: 1;

        hence thesis by A2, BORSUK_1: 43;

      end;

      then

      reconsider Y as Subset of I[01] ;

      Y is closed & (X ` ) = Y by A1, Th3, BORSUK_4: 23;

      hence thesis by TOPS_1: 4;

    end;

    theorem :: TOPALG_1:6

    for f be real-valued FinSequence holds (x * ( - f)) = ( - (x * f))

    proof

      let f be real-valued FinSequence;

      

      thus (x * ( - f)) = (x * (( - 1) * f))

      .= ((( - 1) * x) * f) by RVSUM_1: 49

      .= ( - (x * f)) by RVSUM_1: 49;

    end;

    theorem :: TOPALG_1:7

    

     Th7: for f,g be real-valued FinSequence holds (x * (f - g)) = ((x * f) - (x * g)) by RFUNCT_1: 18;

    theorem :: TOPALG_1:8

    

     Th8: for f be real-valued FinSequence holds ((x - y) * f) = ((x * f) - (y * f))

    proof

      let f be real-valued FinSequence;

      

       A1: ( dom ((x - y) * f)) = ( dom f) by VALUED_1:def 5;

      

       A2: ( dom ((x * f) - (y * f))) = (( dom (x * f)) /\ ( dom (y * f))) by VALUED_1: 12;

      

       A3: ( dom (x * f)) = ( dom f) by VALUED_1:def 5;

      

       A4: ( dom (y * f)) = ( dom f) by VALUED_1:def 5;

      now

        let n;

        assume

         A5: n in ( dom ((x - y) * f));

        

        thus (((x - y) * f) . n) = ((x - y) * (f . n)) by VALUED_1: 6

        .= ((x * (f . n)) - (y * (f . n)))

        .= ((x * (f . n)) - ((y * f) . n)) by VALUED_1: 6

        .= (((x * f) . n) - ((y * f) . n)) by VALUED_1: 6

        .= (((x * f) - (y * f)) . n) by A1, A2, A3, A4, A5, VALUED_1: 13;

      end;

      hence thesis by A1, A2, A3, A4;

    end;

    theorem :: TOPALG_1:9

    

     Th9: for f,g,h,k be real-valued FinSequence holds ((f + g) - (h + k)) = ((f - h) + (g - k))

    proof

      let f,g,h,k be real-valued FinSequence;

      

      thus ((f + g) - (h + k)) = (f + (g + ( - (h + k)))) by RVSUM_1: 15

      .= (f + (g + (( - h) + ( - k)))) by RVSUM_1: 26

      .= (f + (( - h) + (g + ( - k)))) by RVSUM_1: 15

      .= ((f + ( - h)) + (g + ( - k))) by RVSUM_1: 15

      .= ((f - h) + (g + ( - k)))

      .= ((f - h) + (g - k));

    end;

    theorem :: TOPALG_1:10

    

     Th10: for f be Element of ( REAL n) st 0 <= x & x <= 1 holds |.(x * f).| <= |.f.|

    proof

      let f be Element of ( REAL n) such that

       A1: 0 <= x and

       A2: x <= 1;

       |.(x * f).| = ( |.x.| * |.f.|) & x = |.x.| by A1, ABSVALUE:def 1, EUCLID: 11;

      then |.(x * f).| <= (1 * |.f.|) by A1, A2, XREAL_1: 66;

      hence thesis;

    end;

    theorem :: TOPALG_1:11

    for f be Element of ( REAL n), p be Point of I[01] holds |.(p * f).| <= |.f.|

    proof

      let f be Element of ( REAL n), p be Point of I[01] ;

       [. 0 , 1.] = { r where r be Real : 0 <= r & r <= 1 } & p in the carrier of I[01] by RCOMP_1:def 1;

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

      hence thesis by Th10;

    end;

    theorem :: TOPALG_1:12

    for e1,e2,e3,e4,e5,e6 be Point of ( Euclid n), p1,p2,p3,p4 be Point of ( TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = (p1 + p3) & e6 = (p2 + p4) & ( dist (e1,e2)) < x & ( dist (e3,e4)) < y holds ( dist (e5,e6)) < (x + y)

    proof

      let e1,e2,e3,e4,e5,e6 be Point of ( Euclid n), p1,p2,p3,p4 be Point of ( TOP-REAL n) such that

       A1: e1 = p1 and

       A2: e2 = p2 and

       A3: e3 = p3 and

       A4: e4 = p4 and

       A5: e5 = (p1 + p3) and

       A6: e6 = (p2 + p4) and

       A7: ( dist (e1,e2)) < x & ( dist (e3,e4)) < y;

      reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of ( REAL n) by A1, A2, A3, A4, A5, A6, EUCLID: 22;

      

       A8: |.((f1 - f2) + (f3 - f4)).| <= ( |.(f1 - f2).| + |.(f3 - f4).|) & (( dist (e1,e2)) + ( dist (e3,e4))) < (x + y) by A7, EUCLID: 12, XREAL_1: 8;

      reconsider u1 = f1, u2 = f2, u3 = f3, u4 = f4, u6 = f6 as Element of (n -tuples_on REAL ) by EUCLID:def 1;

      (u2 + u4) = u6 by A2, A4, A6;

      

      then

       A9: ((f1 + f3) - f6) = ((u1 - u2) + (u3 - u4)) by Th9

      .= ((f1 - f2) + (f3 - f4));

      

       A10: ( dist (e1,e2)) = |.(f1 - f2).| & ( dist (e3,e4)) = |.(f3 - f4).| by SPPOL_1: 5;

      ( dist (e5,e6)) = |.(f5 - f6).| by SPPOL_1: 5

      .= |.((f1 - f2) + (f3 - f4)).| by A1, A3, A5, A9;

      hence thesis by A10, A8, XXREAL_0: 2;

    end;

    theorem :: TOPALG_1:13

    

     Th13: for e1,e2,e5,e6 be Point of ( Euclid n), p1,p2 be Point of ( TOP-REAL n) st e1 = p1 & e2 = p2 & e5 = (y * p1) & e6 = (y * p2) & ( dist (e1,e2)) < x & y <> 0 holds ( dist (e5,e6)) < ( |.y.| * x)

    proof

      let e1,e2,e5,e6 be Point of ( Euclid n), p1,p2 be Point of ( TOP-REAL n) such that

       A1: e1 = p1 and

       A2: e2 = p2 and

       A3: e5 = (y * p1) and

       A4: e6 = (y * p2) and

       A5: ( dist (e1,e2)) < x and

       A6: y <> 0 ;

      reconsider f1 = e1, f2 = e2, f5 = e5, f6 = e6 as Element of ( REAL n) by A1, A2, A3, A4, EUCLID: 22;

      

       A7: ( dist (e1,e2)) = |.(f1 - f2).| by SPPOL_1: 5;

      

       A8: 0 < |.y.| by A6, COMPLEX1: 47;

      ( dist (e5,e6)) = |.(f5 - f6).| by SPPOL_1: 5

      .= |.((y * f1) - f6).| by A1, A3

      .= |.((y * f1) - (y * f2)).| by A2, A4

      .= |.(y * (f1 - f2)).| by Th7

      .= ( |.y.| * |.(f1 - f2).|) by EUCLID: 11;

      hence thesis by A5, A7, A8, XREAL_1: 68;

    end;

    theorem :: TOPALG_1:14

    

     Th14: for e1,e2,e3,e4,e5,e6 be Point of ( Euclid n), p1,p2,p3,p4 be Point of ( TOP-REAL n) st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = ((x * p1) + (y * p3)) & e6 = ((x * p2) + (y * p4)) & ( dist (e1,e2)) < p & ( dist (e3,e4)) < q & x <> 0 & y <> 0 holds ( dist (e5,e6)) < (( |.x.| * p) + ( |.y.| * q))

    proof

      let e1,e2,e3,e4,e5,e6 be Point of ( Euclid n), p1,p2,p3,p4 be Point of ( TOP-REAL n) such that

       A1: e1 = p1 and

       A2: e2 = p2 and

       A3: e3 = p3 and

       A4: e4 = p4 and

       A5: e5 = ((x * p1) + (y * p3)) and

       A6: e6 = ((x * p2) + (y * p4)) and

       A7: ( dist (e1,e2)) < p and

       A8: ( dist (e3,e4)) < q and

       A9: x <> 0 and

       A10: y <> 0 ;

      reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element of ( REAL n) by A1, A2, A3, A4, A5, A6, EUCLID: 22;

      

       A11: (x * f2) = (x * p2) & (y * f4) = (y * p4) by A2, A4;

      (x * f1) = (x * p1) & (y * f3) = (y * p3) by A1, A3;

      then

       A12: f5 = ((x * f1) + (y * f3)) by A5;

      

       A13: 0 < |.y.| by A10, COMPLEX1: 47;

      ( dist (e3,e4)) = |.(f3 - f4).| by SPPOL_1: 5;

      then

       A14: ( |.y.| * |.(f3 - f4).|) < ( |.y.| * q) by A8, A13, XREAL_1: 68;

      

       A15: 0 < |.x.| by A9, COMPLEX1: 47;

      ( dist (e1,e2)) = |.(f1 - f2).| by SPPOL_1: 5;

      then ( |.x.| * |.(f1 - f2).|) < ( |.x.| * p) by A7, A15, XREAL_1: 68;

      then

       A16: (( |.x.| * |.(f1 - f2).|) + ( |.y.| * |.(f3 - f4).|)) < (( |.x.| * p) + ( |.y.| * q)) by A14, XREAL_1: 8;

       |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= ( |.(x * (f1 - f2)).| + |.(y * (f3 - f4)).|) by EUCLID: 12;

      then |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= ( |.(x * (f1 - f2)).| + ( |.y.| * |.(f3 - f4).|)) by EUCLID: 11;

      then

       A17: |.((x * (f1 - f2)) + (y * (f3 - f4))).| <= (( |.x.| * |.(f1 - f2).|) + ( |.y.| * |.(f3 - f4).|)) by EUCLID: 11;

      ( dist (e5,e6)) = |.(f5 - f6).| by SPPOL_1: 5

      .= |.(((x * f1) + (y * f3)) - ((x * f2) + (y * f4))).| by A6, A12, A11

      .= |.(((x * f1) - (x * f2)) + ((y * f3) - (y * f4))).| by Th9

      .= |.((x * (f1 - f2)) + ((y * f3) - (y * f4))).| by Th7

      .= |.((x * (f1 - f2)) + (y * (f3 - f4))).| by Th7;

      hence thesis by A17, A16, XXREAL_0: 2;

    end;

    

     Lm1: for X be non empty TopSpace, f1,f2,g be Function of X, ( TOP-REAL n) st f1 is continuous & f2 is continuous & for p be Point of X holds (g . p) = ((f1 . p) + (f2 . p)) holds g is continuous

    proof

      let X be non empty TopSpace, f1,f2,g be Function of X, ( TOP-REAL n) such that

       A1: f1 is continuous & f2 is continuous and

       A2: for p be Point of X holds (g . p) = ((f1 . p) + (f2 . p));

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

       A3: for r be Point of X holds (h . r) = ((f1 . r) + (f2 . r)) and

       A4: h is continuous by A1, JGRAPH_6: 12;

      for x be Point of X holds (g . x) = (h . x)

      proof

        let x be Point of X;

        

        thus (g . x) = ((f1 . x) + (f2 . x)) by A2

        .= (h . x) by A3;

      end;

      hence thesis by A4, FUNCT_2: 63;

    end;

    theorem :: TOPALG_1:15

    

     Th15: for X be non empty TopSpace, f,g be Function of X, ( TOP-REAL n) st f is continuous & for p be Point of X holds (g . p) = (y * (f . p)) holds g is continuous

    proof

      let X be non empty TopSpace, f,g be Function of X, ( TOP-REAL n) such that

       A1: f is continuous and

       A2: for p be Point of X holds (g . p) = (y * (f . p));

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

      proof

        let p be Point of X, V be Subset of ( TOP-REAL n);

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

        reconsider r1 = (f . p) as Point of ( Euclid n) by TOPREAL3: 8;

        assume (g . p) in V & V is open;

        then (g . p) in ( Int V) by TOPS_1: 23;

        then

        consider r0 be Real such that

         A3: r0 > 0 and

         A4: ( Ball (r,r0)) c= V by GOBOARD6: 5;

        reconsider G1 = ( Ball (r1,(r0 / |.y.|))) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

        per cases ;

          suppose

           A5: y <> 0 ;

          

           A6: G1 is open by GOBOARD6: 3;

          

           A7: 0 < |.y.| by A5, COMPLEX1: 47;

          then r1 in G1 by A3, GOBOARD6: 1, XREAL_1: 139;

          then

          consider W1 be Subset of X such that

           A8: p in W1 and

           A9: W1 is open and

           A10: (f .: W1) c= G1 by A1, A6, JGRAPH_2: 10;

          take W1;

          thus p in W1 by A8;

          thus W1 is open by A9;

          (g .: W1) c= ( Ball (r,r0))

          proof

            let x be object;

            assume x in (g .: W1);

            then

            consider z be object such that

             A11: z in ( dom g) and

             A12: z in W1 and

             A13: (g . z) = x by FUNCT_1:def 6;

            reconsider z as Point of X by A11;

            

             A14: x = (y * (f . z)) by A2, A13;

            then

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

            reconsider ea1 = (f . z) as Point of ( Euclid n) by TOPREAL3: 8;

            z in the carrier of X;

            then z in ( dom f) by FUNCT_2:def 1;

            then (f . z) in (f .: W1) by A12, FUNCT_1:def 6;

            then

             A15: ( dist (r1,ea1)) < (r0 / |.y.|) by A10, METRIC_1: 11;

            r = (y * (f . p)) by A2;

            then ( dist (r,e1x)) < ( |.y.| * (r0 / |.y.|)) by A5, A14, A15, Th13;

            then ( dist (r,e1x)) < r0 by A7, XCMPLX_1: 87;

            hence thesis by METRIC_1: 11;

          end;

          hence thesis by A4;

        end;

          suppose

           A16: y = 0 ;

          

           A17: r = (y * (f . p)) by A2

          .= ( 0. ( TOP-REAL n)) by A16, RLVECT_1: 10;

          take W = ( [#] X);

          thus p in W;

          thus W is open;

          let x be object;

          assume x in (g .: W);

          then

          consider z be object such that z in ( dom g) and

           A18: z in W and

           A19: (g . z) = x by FUNCT_1:def 6;

          reconsider z as Point of X by A18;

          x = (y * (f . z)) by A2, A19

          .= ( 0. ( TOP-REAL n)) by A16, RLVECT_1: 10;

          then x in ( Ball (r,r0)) by A3, A17, GOBOARD6: 1;

          hence thesis by A4;

        end;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPALG_1:16

    for X be non empty TopSpace, f1,f2,g be Function of X, ( TOP-REAL n) st f1 is continuous & f2 is continuous & for p be Point of X holds (g . p) = ((x * (f1 . p)) + (y * (f2 . p))) holds g is continuous

    proof

      let X be non empty TopSpace, f1,f2,g be Function of X, ( TOP-REAL n) such that

       A1: f1 is continuous and

       A2: f2 is continuous and

       A3: for p be Point of X holds (g . p) = ((x * (f1 . p)) + (y * (f2 . p)));

      per cases ;

        suppose that

         A4: x <> 0 and

         A5: y <> 0 ;

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

        proof

          let p be Point of X, V be Subset of ( TOP-REAL n);

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

          assume (g . p) in V & V is open;

          then (g . p) in ( Int V) by TOPS_1: 23;

          then

          consider r0 be Real such that

           A6: r0 > 0 and

           A7: ( Ball (r,r0)) c= V by GOBOARD6: 5;

          

           A8: (r0 / 2) > 0 by A6, XREAL_1: 215;

          reconsider r2 = (f2 . p) as Point of ( Euclid n) by TOPREAL3: 8;

          reconsider G2 = ( Ball (r2,((r0 / 2) / |.y.|))) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

          

           A9: G2 is open by GOBOARD6: 3;

          reconsider r1 = (f1 . p) as Point of ( Euclid n) by TOPREAL3: 8;

          reconsider G1 = ( Ball (r1,((r0 / 2) / |.x.|))) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

          

           A10: G1 is open by GOBOARD6: 3;

          

           A11: |.y.| > 0 by A5, COMPLEX1: 47;

          then r2 in G2 by A8, GOBOARD6: 1, XREAL_1: 139;

          then

          consider W2 be Subset of X such that

           A12: p in W2 and

           A13: W2 is open and

           A14: (f2 .: W2) c= G2 by A2, A9, JGRAPH_2: 10;

          

           A15: |.x.| > 0 by A4, COMPLEX1: 47;

          then r1 in G1 by A8, GOBOARD6: 1, XREAL_1: 139;

          then

          consider W1 be Subset of X such that

           A16: p in W1 and

           A17: W1 is open and

           A18: (f1 .: W1) c= G1 by A1, A10, JGRAPH_2: 10;

          take W = (W1 /\ W2);

          thus p in W by A16, A12, XBOOLE_0:def 4;

          thus W is open by A17, A13;

          (g .: W) c= ( Ball (r,r0))

          proof

            let a be object;

            assume a in (g .: W);

            then

            consider z be object such that

             A19: z in ( dom g) and

             A20: z in W and

             A21: (g . z) = a by FUNCT_1:def 6;

            

             A22: z in W1 by A20, XBOOLE_0:def 4;

            reconsider z as Point of X by A19;

            reconsider ea2 = (f2 . z) as Point of ( Euclid n) by TOPREAL3: 8;

            reconsider ea1 = (f1 . z) as Point of ( Euclid n) by TOPREAL3: 8;

            

             A23: z in the carrier of X;

            then

             A24: z in ( dom f2) by FUNCT_2:def 1;

            z in W2 by A20, XBOOLE_0:def 4;

            then (f2 . z) in (f2 .: W2) by A24, FUNCT_1:def 6;

            then

             A25: ( dist (r2,ea2)) < ((r0 / 2) / |.y.|) by A14, METRIC_1: 11;

            z in ( dom f1) by A23, FUNCT_2:def 1;

            then (f1 . z) in (f1 .: W1) by A22, FUNCT_1:def 6;

            then

             A26: ( dist (r1,ea1)) < ((r0 / 2) / |.x.|) by A18, METRIC_1: 11;

            

             A27: a = ((x * (f1 . z)) + (y * (f2 . z))) by A3, A21;

            then

            reconsider e1x = a as Point of ( Euclid n) by TOPREAL3: 8;

            r = ((x * (f1 . p)) + (y * (f2 . p))) by A3;

            then ( dist (r,e1x)) < (( |.x.| * ((r0 / 2) / |.x.|)) + ( |.y.| * ((r0 / 2) / |.y.|))) by A4, A5, A27, A26, A25, Th14;

            then ( dist (r,e1x)) < (( |.x.| * ((r0 / |.x.|) / 2)) + ( |.y.| * ((r0 / 2) / |.y.|))) by XCMPLX_1: 48;

            then ( dist (r,e1x)) < (( |.x.| * ((r0 / |.x.|) / 2)) + ( |.y.| * ((r0 / |.y.|) / 2))) by XCMPLX_1: 48;

            then ( dist (r,e1x)) < ((r0 / 2) + ( |.y.| * ((r0 / |.y.|) / 2))) by A15, XCMPLX_1: 97;

            then ( dist (r,e1x)) < ((r0 / 2) + (r0 / 2)) by A11, XCMPLX_1: 97;

            hence thesis by METRIC_1: 11;

          end;

          hence thesis by A7;

        end;

        hence thesis by JGRAPH_2: 10;

      end;

        suppose

         A28: x = 0 ;

        for p be Point of X holds (g . p) = (y * (f2 . p))

        proof

          let p be Point of X;

          

          thus (g . p) = ((x * (f1 . p)) + (y * (f2 . p))) by A3

          .= (( 0. ( TOP-REAL n)) + (y * (f2 . p))) by A28, RLVECT_1: 10

          .= (y * (f2 . p)) by RLVECT_1: 4;

        end;

        hence thesis by A2, Th15;

      end;

        suppose

         A29: y = 0 ;

        for p be Point of X holds (g . p) = (x * (f1 . p))

        proof

          let p be Point of X;

          

          thus (g . p) = ((x * (f1 . p)) + (y * (f2 . p))) by A3

          .= ((x * (f1 . p)) + ( 0. ( TOP-REAL n))) by A29, RLVECT_1: 10

          .= (x * (f1 . p)) by RLVECT_1: 4;

        end;

        hence thesis by A1, Th15;

      end;

    end;

    theorem :: TOPALG_1:17

    

     Th17: for F be Function of [:( TOP-REAL n), I[01] :], ( TOP-REAL n) st for x be Point of ( TOP-REAL n), i be Point of I[01] holds (F . (x,i)) = ((1 - i) * x) holds F is continuous

    proof

      set I = the carrier of I[01] ;

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

       A1: for x be Point of ( TOP-REAL n), i be Point of I[01] holds (F . (x,i)) = ((1 - i) * x);

      

       A2: ( REAL n) = (n -tuples_on REAL ) by EUCLID:def 1;

      

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

      for p be Point of [:( TOP-REAL n), I[01] :], V be Subset of ( TOP-REAL n) st (F . p) in V & V is open holds ex W be Subset of [:( TOP-REAL n), I[01] :] st p in W & W is open & (F .: W) c= V

      proof

        let p be Point of [:( TOP-REAL n), I[01] :], V be Subset of ( TOP-REAL n);

        reconsider ep = (F . p) as Point of ( Euclid n) by TOPREAL3: 8;

        consider x be Point of ( TOP-REAL n), i be Point of I[01] such that

         A4: p = [x, i] by BORSUK_1: 10;

        

         A5: ep = (F . (x,i)) by A4

        .= ((1 - i) * x) by A1;

        reconsider fx = x as Element of ( REAL n) by EUCLID: 22;

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

        assume (F . p) in V & V is open;

        then (F . p) in ( Int V) by TOPS_1: 23;

        then

        consider r0 be Real such that

         A6: r0 > 0 and

         A7: ( Ball (ep,r0)) c= V by GOBOARD6: 5;

        

         A8: (r0 / 2) > 0 by A6, XREAL_1: 139;

        per cases ;

          suppose

           A9: (1 - i) > 0 ;

          then ( - ( - (1 - i))) > ( - 0 );

          then ( - (1 - i)) < 0 ;

          then

           A10: ((i - 1) * ((2 * (1 - i)) * |.fx.|)) <= 0 by A9;

          set t = (((2 * (1 - i)) * |.fx.|) + r0);

          set c = (((1 - i) * r0) / t);

          (i + c) = (((i * t) / t) + (((1 - i) * r0) / t)) by A6, A9, XCMPLX_1: 89

          .= (((i * t) + ((1 - i) * r0)) / t) by XCMPLX_1: 62

          .= (((((i * 2) * (1 - i)) * |.fx.|) + r0) / t);

          

          then ((i + c) - 1) = ((((((i * 2) * (1 - i)) * |.fx.|) + r0) / t) - (t / t)) by A6, A9, XCMPLX_1: 60

          .= ((((((i * 2) * (1 - i)) * |.fx.|) + r0) - t) / t) by XCMPLX_1: 120;

          then

           A11: (((i + c) - 1) + 1) <= ( 0 + 1) by A6, A9, A10, XREAL_1: 7;

          set X1 = ].(i - c), (i + c).[;

          set X2 = (X1 /\ I);

          reconsider X2 as Subset of I[01] by XBOOLE_1: 17;

          reconsider B = ( Ball (lx,((r0 / 2) / (1 - i)))) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

          take W = [:B, X2:];

           0 < ((1 - i) * r0) by A6, A9, XREAL_1: 129;

          then

           A12: 0 < c by A6, A9, XREAL_1: 139;

          then |.(i - i).| < c by ABSVALUE:def 1;

          then i in X1 by RCOMP_1: 1;

          then

           A13: i in X2 by XBOOLE_0:def 4;

           0 <= i by BORSUK_1: 43;

          then

           A14: (i + c) is Point of I[01] by A6, A9, A11, BORSUK_1: 43;

           A15:

          now

            per cases ;

              suppose

               A16: 0 <= (i - c);

              X1 c= the carrier of I[01]

              proof

                let a be object;

                assume

                 A17: a in X1;

                then

                reconsider a as Real;

                a < (i + c) by A17, XXREAL_1: 4;

                then

                 A18: a < 1 by A11, XXREAL_0: 2;

                 0 < a by A16, A17, XXREAL_1: 4;

                hence thesis by A18, BORSUK_1: 43;

              end;

              then

              reconsider X1 as Subset of I[01] ;

              now

                per cases ;

                  suppose (i - c) <= (i + c);

                  then (i - c) <= 1 by A11, XXREAL_0: 2;

                  then (i - c) is Point of I[01] by A16, BORSUK_1: 43;

                  hence X1 is open by A14, BORSUK_4: 45;

                end;

                  suppose (i - c) > (i + c);

                  then X1 = ( {} I[01] ) by XXREAL_1: 28;

                  hence X1 is open;

                end;

              end;

              hence X2 is open by A3;

            end;

              suppose

               A19: (i - c) < 0 ;

              X2 = [. 0 , (i + c).[

              proof

                hereby

                  let a be object;

                  assume

                   A20: a in X2;

                  then

                  reconsider b = a as Real;

                  a in X1 by A20, XBOOLE_0:def 4;

                  then

                   A21: b < (i + c) by XXREAL_1: 4;

                   0 <= b by A20, BORSUK_1: 43;

                  hence a in [. 0 , (i + c).[ by A21, XXREAL_1: 3;

                end;

                let a be object;

                assume

                 A22: a in [. 0 , (i + c).[;

                then

                reconsider b = a as Real;

                

                 A23: 0 <= b by A22, XXREAL_1: 3;

                

                 A24: b < (i + c) by A22, XXREAL_1: 3;

                then b <= 1 by A11, XXREAL_0: 2;

                then

                 A25: a in I by A23, BORSUK_1: 40, XXREAL_1: 1;

                a in X1 by A19, A24, A23, XXREAL_1: 4;

                hence thesis by A25, XBOOLE_0:def 4;

              end;

              hence X2 is open by A14, Th5;

            end;

          end;

          x in B by A8, A9, GOBOARD6: 1, XREAL_1: 139;

          hence p in W by A4, A13, ZFMISC_1: 87;

          B is open by GOBOARD6: 3;

          hence W is open by A15, BORSUK_1: 6;

          

           A26: 0 < (2 * (1 - i)) by A9, XREAL_1: 129;

          (F .: W) c= ( Ball (ep,r0))

          proof

            let m be object;

            assume m in (F .: W);

            then

            consider z be object such that

             A27: z in ( dom F) and

             A28: z in W and

             A29: (F . z) = m by FUNCT_1:def 6;

            reconsider z as Point of [:( TOP-REAL n), I[01] :] by A27;

            consider y be Point of ( TOP-REAL n), j be Point of I[01] such that

             A30: z = [y, j] by BORSUK_1: 10;

            reconsider ez = (F . z), ey = y as Point of ( Euclid n) by TOPREAL3: 8;

            reconsider fp = ep, fz = ez, fe = ((1 - i) * y), fy = y as Element of ( REAL n) by EUCLID: 22;

            

             A31: ((1 - i) * ((r0 / (1 - i)) / 2)) = (r0 / 2) & ((r0 / 2) / (1 - i)) = ((r0 / (1 - i)) / 2) by A9, XCMPLX_1: 48, XCMPLX_1: 97;

            fy in B by A28, A30, ZFMISC_1: 87;

            then

             A32: ( dist (lx,ey)) < ((r0 / 2) / (1 - i)) by METRIC_1: 11;

            j in X2 by A28, A30, ZFMISC_1: 87;

            then j in X1 by XBOOLE_0:def 4;

            then |.(j - i).| < c by RCOMP_1: 1;

            then |.(i - j).| < c by UNIFORM1: 11;

            then

             A33: ( |.(i - j).| * |.fy.|) <= (c * |.fy.|) by XREAL_1: 64;

            reconsider yy = ey as Element of (n -tuples_on REAL ) by A2, EUCLID: 22;

            ez = (F . (y,j)) by A30

            .= ((1 - j) * y) by A1;

            then (fe - fz) = (((1 - i) * yy) - ((1 - j) * yy));

            

            then

             A34: |.(fe - fz).| = |.(((1 - i) - (1 - j)) * fy).| by Th8

            .= ( |.(j - i).| * |.fy.|) by EUCLID: 11

            .= ( |.(i - j).| * |.fy.|) by UNIFORM1: 11;

            reconsider gx = fx, gy = fy as Element of (n -tuples_on REAL ) by EUCLID:def 1;

            

             A35: ( dist (ep,ez)) = |.(fp - fz).| & |.(fp - fz).| <= ( |.(fp - fe).| + |.(fe - fz).|) by EUCLID: 19, SPPOL_1: 5;

            

             A36: ((1 - i) * (fx - fy)) = ((1 - i) * (gx - gy))

            .= (((1 - i) * gx) - ((1 - i) * gy)) by Th7

            .= (((1 - i) * fx) - ((1 - i) * fy))

            .= (((1 - i) * fx) - fe);

            

             A37: ( dist (lx,ey)) = |.(fx - fy).| by SPPOL_1: 5;

            then ((1 - i) * |.(fx - fy).|) < ((1 - i) * ((r0 / 2) / (1 - i))) by A9, A32, XREAL_1: 68;

            then ( |.(1 - i).| * |.(fx - fy).|) < (r0 / 2) by A9, A31, ABSVALUE:def 1;

            then

             A38: |.(((1 - i) * fx) - fe).| < (r0 / 2) by A36, EUCLID: 11;

             |.(fx - fy).| = |.(fy - fx).| & ( |.fy.| - |.fx.|) <= |.(fy - fx).| by EUCLID: 15, EUCLID: 18;

            then ( |.fy.| - |.fx.|) < ((r0 / 2) / (1 - i)) by A32, A37, XXREAL_0: 2;

            then |.fy.| < ( |.fx.| + ((r0 / 2) / (1 - i))) by XREAL_1: 19;

            then

             A39: (c * |.fy.|) < (c * ( |.fx.| + ((r0 / 2) / (1 - i)))) by A12, XREAL_1: 68;

            (c * ( |.fx.| + ((r0 / 2) / (1 - i)))) = (c * ( |.fx.| + (r0 / (2 * (1 - i))))) by XCMPLX_1: 78

            .= (c * ((( |.fx.| * (2 * (1 - i))) / (2 * (1 - i))) + (r0 / (2 * (1 - i))))) by A26, XCMPLX_1: 89

            .= (c * ((( |.fx.| * (2 * (1 - i))) + r0) / (2 * (1 - i)))) by XCMPLX_1: 62

            .= (((1 - i) * r0) / (2 * (1 - i))) by A6, A9, XCMPLX_1: 98

            .= (r0 / 2) by A9, XCMPLX_1: 91;

            then

             A40: ( |.(i - j).| * |.fy.|) <= (r0 / 2) by A33, A39, XXREAL_0: 2;

            fp = ((1 - i) * x) by A5

            .= ((1 - i) * fx);

            then ( |.(fp - fe).| + |.(fe - fz).|) < ((r0 / 2) + (r0 / 2)) by A34, A40, A38, XREAL_1: 8;

            then ( dist (ep,ez)) < r0 by A35, XXREAL_0: 2;

            hence thesis by A29, METRIC_1: 11;

          end;

          hence thesis by A7;

        end;

          suppose

           A41: (1 - i) <= 0 ;

          

           A42: i <= 1 by BORSUK_1: 43;

          ((1 - i) + i) <= ( 0 + i) by A41, XREAL_1: 6;

          then

           A43: i = 1 by A42, XXREAL_0: 1;

          set t = ( |.fx.| + r0);

          reconsider B = ( Ball (lx,r0)) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

          set c = (r0 / t);

          set X1 = ].(1 - c), 1.];

          

           A44: x in B by A6, GOBOARD6: 1;

          ( 0 + r0) <= t by XREAL_1: 7;

          then

           A45: c <= 1 by A6, XREAL_1: 185;

          then

           A46: (c - c) <= (1 - c) by XREAL_1: 9;

          X1 c= I

          proof

            let s be object;

            assume

             A47: s in X1;

            then

            reconsider s as Real;

            s <= 1 & (1 - c) < s by A47, XXREAL_1: 2;

            hence thesis by A46, BORSUK_1: 43;

          end;

          then

          reconsider X1 as Subset of I[01] ;

          c is Point of I[01] by A6, A45, BORSUK_1: 43;

          then (1 - c) is Point of I[01] by JORDAN5B: 4;

          then

           A48: X1 is open by Th4;

          take W = [:B, X1:];

          

           A49: 0 < c by A6, XREAL_1: 139;

          then (1 - c) < (1 - 0 ) by XREAL_1: 15;

          then i in X1 by A43, XXREAL_1: 2;

          hence p in W by A4, A44, ZFMISC_1: 87;

          B is open by GOBOARD6: 3;

          hence W is open by A48, BORSUK_1: 6;

          (F .: W) c= ( Ball (ep,r0))

          proof

            let m be object;

            assume m in (F .: W);

            then

            consider z be object such that

             A50: z in ( dom F) and

             A51: z in W and

             A52: (F . z) = m by FUNCT_1:def 6;

            reconsider z as Point of [:( TOP-REAL n), I[01] :] by A50;

            consider y be Point of ( TOP-REAL n), j be Point of I[01] such that

             A53: z = [y, j] by BORSUK_1: 10;

            reconsider ez = (F . z), ey = y as Point of ( Euclid n) by TOPREAL3: 8;

            reconsider fp = ep, fz = ez, fy = y as Element of ( REAL n) by EUCLID: 22;

            fy in B by A51, A53, ZFMISC_1: 87;

            then

             A54: ( dist (lx,ey)) < r0 by METRIC_1: 11;

            

             A55: ez = (F . (y,j)) by A53

            .= ((1 - j) * y) by A1;

            fp = ((1 - i) * x) by A5

            .= ( 0. ( TOP-REAL n)) by A43, RLVECT_1: 10;

            

            then

             A56: (fz - fp) = ((F . z) - ( 0. ( TOP-REAL n)))

            .= fz by RLVECT_1: 13;

            

             A57: ( |.fy.| - |.fx.|) <= |.(fy - fx).| by EUCLID: 15;

            ( dist (lx,ey)) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| by EUCLID: 18, SPPOL_1: 5;

            then ( |.fy.| - |.fx.|) < r0 by A54, A57, XXREAL_0: 2;

            then

             A58: |.fy.| < t by XREAL_1: 19;

             A59:

            now

              per cases ;

                suppose j < 1;

                then

                 A60: (j - j) < (1 - j) by XREAL_1: 14;

                j in X1 by A51, A53, ZFMISC_1: 87;

                then (1 - c) < j by XXREAL_1: 2;

                then ((1 - c) + c) < (j + c) by XREAL_1: 8;

                then (1 - j) < ((j + c) - j) by XREAL_1: 14;

                then (r0 / (1 - j)) > (r0 / c) by A6, A60, XREAL_1: 76;

                then t < (r0 / (1 - j)) by A49, XCMPLX_1: 54;

                then |.fy.| < (r0 / (1 - j)) by A58, XXREAL_0: 2;

                then ((1 - j) * |.fy.|) < ((1 - j) * (r0 / (1 - j))) by A60, XREAL_1: 68;

                hence ((1 - j) * |.fy.|) < r0 by A60, XCMPLX_1: 87;

              end;

                suppose

                 A61: j >= 1;

                j <= 1 by BORSUK_1: 43;

                then j = 1 by A61, XXREAL_0: 1;

                hence ((1 - j) * |.fy.|) < r0 by A6;

              end;

            end;

            (1 - j) is Point of I[01] by JORDAN5B: 4;

            then

             A62: 0 <= (1 - j) by BORSUK_1: 43;

            ( dist (ep,ez)) = |.(fz - fp).| by SPPOL_1: 5

            .= |.fz.| by A56

            .= |.((1 - j) * fy).| by A55

            .= ( |.(1 - j).| * |.fy.|) by EUCLID: 11

            .= ((1 - j) * |.fy.|) by A62, ABSVALUE:def 1;

            hence thesis by A52, A59, METRIC_1: 11;

          end;

          hence thesis by A7;

        end;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPALG_1:18

    

     Th18: for F be Function of [:( TOP-REAL n), I[01] :], ( TOP-REAL n) st for x be Point of ( TOP-REAL n), i be Point of I[01] holds (F . (x,i)) = (i * x) holds F is continuous

    proof

      set I = the carrier of I[01] ;

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

       A1: for x be Point of ( TOP-REAL n), i be Point of I[01] holds (F . (x,i)) = (i * x);

      

       A2: ( REAL n) = (n -tuples_on REAL ) by EUCLID:def 1;

      

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

      for p be Point of [:( TOP-REAL n), I[01] :], V be Subset of ( TOP-REAL n) st (F . p) in V & V is open holds ex W be Subset of [:( TOP-REAL n), I[01] :] st p in W & W is open & (F .: W) c= V

      proof

        let p be Point of [:( TOP-REAL n), I[01] :], V be Subset of ( TOP-REAL n);

        reconsider ep = (F . p) as Point of ( Euclid n) by TOPREAL3: 8;

        consider x be Point of ( TOP-REAL n), i be Point of I[01] such that

         A4: p = [x, i] by BORSUK_1: 10;

        

         A5: ep = (F . (x,i)) by A4

        .= (i * x) by A1;

        reconsider fx = x as Element of ( REAL n) by EUCLID: 22;

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

        assume (F . p) in V & V is open;

        then (F . p) in ( Int V) by TOPS_1: 23;

        then

        consider r0 be Real such that

         A6: r0 > 0 and

         A7: ( Ball (ep,r0)) c= V by GOBOARD6: 5;

        

         A8: (r0 / 2) > 0 by A6, XREAL_1: 139;

        per cases ;

          suppose

           A9: i > 0 ;

          set t = (((2 * i) * |.fx.|) + r0);

          set c = ((i * r0) / t);

          i <= 1 by BORSUK_1: 43;

          then (1 - 1) >= (i - 1) by XREAL_1: 9;

          then (((2 * i) * |.fx.|) * (i - 1)) <= 0 by A9;

          then

           A10: (((i * ((2 * i) * |.fx.|)) - ((2 * i) * |.fx.|)) - r0) < (r0 - r0) by A6;

          

           A11: (i - c) = (((i * t) / t) - ((i * r0) / t)) by A6, A9, XCMPLX_1: 89

          .= (((i * t) - (i * r0)) / t) by XCMPLX_1: 120

          .= ((i * ((2 * i) * |.fx.|)) / t);

          

          then ((i - c) - 1) = (((i * ((2 * i) * |.fx.|)) / t) - (t / t)) by A6, A9, XCMPLX_1: 60

          .= (((i * ((2 * i) * |.fx.|)) - t) / t) by XCMPLX_1: 120;

          then ((i - c) - 1) < 0 by A6, A9, A10, XREAL_1: 141;

          then (((i - c) - 1) + 1) < ( 0 + 1) by XREAL_1: 8;

          then

           A12: (i - c) is Point of I[01] by A6, A9, A11, BORSUK_1: 43;

          set X1 = ].(i - c), (i + c).[;

          set X2 = (X1 /\ I);

          reconsider X2 as Subset of I[01] by XBOOLE_1: 17;

          reconsider B = ( Ball (lx,((r0 / 2) / i))) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

          take W = [:B, X2:];

           0 < (i * r0) by A6, A9, XREAL_1: 129;

          then

           A13: 0 < c by A6, A9, XREAL_1: 139;

          then |.(i - i).| < c by ABSVALUE:def 1;

          then i in X1 by RCOMP_1: 1;

          then

           A14: i in X2 by XBOOLE_0:def 4;

          

           A15: 0 <= (i - c) by A6, A9, A11;

           A16:

          now

            per cases ;

              suppose

               A17: (i + c) <= 1;

              X1 c= the carrier of I[01]

              proof

                let a be object;

                assume

                 A18: a in X1;

                then

                reconsider a as Real;

                a < (i + c) by A18, XXREAL_1: 4;

                then

                 A19: a < 1 by A17, XXREAL_0: 2;

                 0 < a by A6, A9, A11, A18, XXREAL_1: 4;

                hence thesis by A19, BORSUK_1: 43;

              end;

              then

              reconsider X1 as Subset of I[01] ;

              (i + c) is Point of I[01] by A6, A9, A17, BORSUK_1: 43;

              then X1 is open by A12, BORSUK_4: 45;

              hence X2 is open by A3;

            end;

              suppose

               A20: (i + c) > 1;

              X2 = ].(i - c), 1.]

              proof

                hereby

                  let a be object;

                  assume

                   A21: a in X2;

                  then

                  reconsider b = a as Real;

                  a in X1 by A21, XBOOLE_0:def 4;

                  then

                   A22: (i - c) < b by XXREAL_1: 4;

                  b <= 1 by A21, BORSUK_1: 43;

                  hence a in ].(i - c), 1.] by A22, XXREAL_1: 2;

                end;

                let a be object;

                assume

                 A23: a in ].(i - c), 1.];

                then

                reconsider b = a as Real;

                

                 A24: (i - c) < b by A23, XXREAL_1: 2;

                

                 A25: b <= 1 by A23, XXREAL_1: 2;

                then b < (i + c) by A20, XXREAL_0: 2;

                then

                 A26: a in X1 by A24, XXREAL_1: 4;

                a in I by A15, A24, A25, BORSUK_1: 40, XXREAL_1: 1;

                hence thesis by A26, XBOOLE_0:def 4;

              end;

              hence X2 is open by A12, Th4;

            end;

          end;

          x in B by A8, A9, GOBOARD6: 1, XREAL_1: 139;

          hence p in W by A4, A14, ZFMISC_1: 87;

          B is open by GOBOARD6: 3;

          hence W is open by A16, BORSUK_1: 6;

          

           A27: 0 < (2 * i) by A9, XREAL_1: 129;

          (F .: W) c= ( Ball (ep,r0))

          proof

            let m be object;

            assume m in (F .: W);

            then

            consider z be object such that

             A28: z in ( dom F) and

             A29: z in W and

             A30: (F . z) = m by FUNCT_1:def 6;

            reconsider z as Point of [:( TOP-REAL n), I[01] :] by A28;

            consider y be Point of ( TOP-REAL n), j be Point of I[01] such that

             A31: z = [y, j] by BORSUK_1: 10;

            reconsider ez = (F . z), ey = y as Point of ( Euclid n) by TOPREAL3: 8;

            reconsider fp = ep, fz = ez, fe = (i * y), fy = y as Element of ( REAL n) by EUCLID: 22;

            

             A32: (i * ((r0 / i) / 2)) = (r0 / 2) & ((r0 / 2) / i) = ((r0 / i) / 2) by A9, XCMPLX_1: 48, XCMPLX_1: 97;

            fy in B by A29, A31, ZFMISC_1: 87;

            then

             A33: ( dist (lx,ey)) < ((r0 / 2) / i) by METRIC_1: 11;

            j in X2 by A29, A31, ZFMISC_1: 87;

            then j in X1 by XBOOLE_0:def 4;

            then |.(j - i).| < c by RCOMP_1: 1;

            then |.(i - j).| < c by UNIFORM1: 11;

            then

             A34: ( |.(i - j).| * |.fy.|) <= (c * |.fy.|) by XREAL_1: 64;

            reconsider yy = ey as Element of (n -tuples_on REAL ) by A2, EUCLID: 22;

            ez = (F . (y,j)) by A31

            .= (j * y) by A1;

            then (fe - fz) = ((i * yy) - (j * yy));

            

            then

             A35: |.(fe - fz).| = |.((i - j) * fy).| by Th8

            .= ( |.(i - j).| * |.fy.|) by EUCLID: 11;

            reconsider yy = y as Element of (n -tuples_on REAL ) by A2, EUCLID: 22;

            

             A36: ( dist (ep,ez)) = |.(fp - fz).| & |.(fp - fz).| <= ( |.(fp - fe).| + |.(fe - fz).|) by EUCLID: 19, SPPOL_1: 5;

            

             A37: ( dist (lx,ey)) = |.(fx - fy).| by SPPOL_1: 5;

            then (i * |.(fx - fy).|) < (i * ((r0 / 2) / i)) by A9, A33, XREAL_1: 68;

            then

             A38: ( |.i.| * |.(fx - fy).|) < (r0 / 2) by A9, A32, ABSVALUE:def 1;

             |.(fx - fy).| = |.(fy - fx).| & ( |.fy.| - |.fx.|) <= |.(fy - fx).| by EUCLID: 15, EUCLID: 18;

            then ( |.fy.| - |.fx.|) < ((r0 / 2) / i) by A33, A37, XXREAL_0: 2;

            then |.fy.| < ( |.fx.| + ((r0 / 2) / i)) by XREAL_1: 19;

            then

             A39: (c * |.fy.|) < (c * ( |.fx.| + ((r0 / 2) / i))) by A13, XREAL_1: 68;

            (c * ( |.fx.| + ((r0 / 2) / i))) = (c * ( |.fx.| + (r0 / (2 * i)))) by XCMPLX_1: 78

            .= (c * ((( |.fx.| * (2 * i)) / (2 * i)) + (r0 / (2 * i)))) by A27, XCMPLX_1: 89

            .= (c * ((( |.fx.| * (2 * i)) + r0) / (2 * i))) by XCMPLX_1: 62

            .= ((i * r0) / (2 * i)) by A6, A9, XCMPLX_1: 98

            .= (r0 / 2) by A9, XCMPLX_1: 91;

            then

             A40: ( |.(i - j).| * |.fy.|) <= (r0 / 2) by A34, A39, XXREAL_0: 2;

            ((i * fx) - fe) = ((i * fx) - (i * yy))

            .= (i * (fx - fy)) by Th7;

            then

             A41: |.((i * fx) - fe).| < (r0 / 2) by A38, EUCLID: 11;

            ((i * fx) - fe) = (fp - fe) by A5;

            then ( |.(fp - fe).| + |.(fe - fz).|) < ((r0 / 2) + (r0 / 2)) by A35, A40, A41, XREAL_1: 8;

            then ( dist (ep,ez)) < r0 by A36, XXREAL_0: 2;

            hence thesis by A30, METRIC_1: 11;

          end;

          hence thesis by A7;

        end;

          suppose

           A42: i <= 0 ;

          set t = ( |.fx.| + r0);

          reconsider B = ( Ball (lx,r0)) as Subset of ( TOP-REAL n) by TOPREAL3: 8;

          set c = (r0 / t);

          set X1 = [. 0 , c.[;

          

           A43: 0 < c by A6, XREAL_1: 139;

          ( 0 + r0) <= t by XREAL_1: 7;

          then

           A44: c <= 1 by A6, XREAL_1: 185;

          

           A45: X1 c= I

          proof

            let s be object;

            assume

             A46: s in X1;

            then

            reconsider s as Real;

            s < c by A46, XXREAL_1: 3;

            then

             A47: s <= 1 by A44, XXREAL_0: 2;

             0 <= s by A46, XXREAL_1: 3;

            hence thesis by A47, BORSUK_1: 43;

          end;

          

           A48: B is open by GOBOARD6: 3;

          reconsider X1 as Subset of I[01] by A45;

          take W = [:B, X1:];

          

           A49: x in B by A6, GOBOARD6: 1;

          

           A50: i = 0 by A42, BORSUK_1: 43;

          then i in X1 by A43, XXREAL_1: 3;

          hence p in W by A4, A49, ZFMISC_1: 87;

          c is Point of I[01] by A6, A44, BORSUK_1: 43;

          then X1 is open by Th5;

          hence W is open by A48, BORSUK_1: 6;

          (F .: W) c= ( Ball (ep,r0))

          proof

            let m be object;

            assume m in (F .: W);

            then

            consider z be object such that

             A51: z in ( dom F) and

             A52: z in W and

             A53: (F . z) = m by FUNCT_1:def 6;

            reconsider z as Point of [:( TOP-REAL n), I[01] :] by A51;

            consider y be Point of ( TOP-REAL n), j be Point of I[01] such that

             A54: z = [y, j] by BORSUK_1: 10;

            reconsider ez = (F . z), ey = y as Point of ( Euclid n) by TOPREAL3: 8;

            reconsider fp = ep, fz = ez, fy = y as Element of ( REAL n) by EUCLID: 22;

            fy in B by A52, A54, ZFMISC_1: 87;

            then

             A55: ( dist (lx,ey)) < r0 by METRIC_1: 11;

            

             A56: ez = (F . (y,j)) by A54

            .= (j * y) by A1;

            fp = (i * x) by A5

            .= ( 0. ( TOP-REAL n)) by A50, RLVECT_1: 10;

            

            then

             A57: (fz - fp) = ((F . z) - ( 0. ( TOP-REAL n)))

            .= fz by RLVECT_1: 13;

            

             A58: ( |.fy.| - |.fx.|) <= |.(fy - fx).| by EUCLID: 15;

            ( dist (lx,ey)) = |.(fx - fy).| & |.(fx - fy).| = |.(fy - fx).| by EUCLID: 18, SPPOL_1: 5;

            then ( |.fy.| - |.fx.|) < r0 by A55, A58, XXREAL_0: 2;

            then

             A59: |.fy.| < t by XREAL_1: 19;

             A60:

            now

              per cases ;

                suppose

                 A61: 0 < j;

                j in X1 by A52, A54, ZFMISC_1: 87;

                then j < c by XXREAL_1: 3;

                then (r0 / j) > (r0 / c) by A6, A61, XREAL_1: 76;

                then t < (r0 / j) by A43, XCMPLX_1: 54;

                then |.fy.| < (r0 / j) by A59, XXREAL_0: 2;

                then (j * |.fy.|) < (j * (r0 / j)) by A61, XREAL_1: 68;

                hence (j * |.fy.|) < r0 by A61, XCMPLX_1: 87;

              end;

                suppose j <= 0 ;

                hence (j * |.fy.|) < r0 by A6;

              end;

            end;

            

             A62: 0 <= j by BORSUK_1: 43;

            ( dist (ep,ez)) = |.(fz - fp).| by SPPOL_1: 5

            .= |.fz.| by A57

            .= |.(j * fy).| by A56

            .= ( |.j.| * |.fy.|) by EUCLID: 11

            .= (j * |.fy.|) by A62, ABSVALUE:def 1;

            hence thesis by A53, A60, METRIC_1: 11;

          end;

          hence thesis by A7;

        end;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    begin

    reserve X for non empty TopSpace,

a,b,c,d,e,f for Point of X,

T for non empty pathwise_connected TopSpace,

a1,b1,c1,d1,e1,f1 for Point of T;

    theorem :: TOPALG_1:19

    

     Th19: (a,b) are_connected & (b,c) are_connected implies for A1,A2 be Path of a, b, B be Path of b, c holds (A1,A2) are_homotopic implies (A1,((A2 + B) + ( - B))) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (b,c) are_connected ;

      set X = the constant Path of b, b;

      let A1,A2 be Path of a, b, B be Path of b, c;

      

       A3: (A1,(A1 + X)) are_homotopic by A1, BORSUK_6: 80;

      assume

       A4: (A1,A2) are_homotopic ;

      ((B + ( - B)),X) are_homotopic by A2, BORSUK_6: 84;

      then ((A2 + (B + ( - B))),(A1 + X)) are_homotopic by A1, A4, BORSUK_6: 75;

      then

       A5: ((A2 + (B + ( - B))),A1) are_homotopic by A3, BORSUK_6: 79;

      ((A2 + (B + ( - B))),((A2 + B) + ( - B))) are_homotopic by A1, A2, BORSUK_6: 73;

      hence thesis by A5, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:20

    for A1,A2 be Path of a1, b1, B be Path of b1, c1 holds (A1,A2) are_homotopic implies (A1,((A2 + B) + ( - B))) are_homotopic

    proof

      let A1,A2 be Path of a1, b1;

      (a1,b1) are_connected & (b1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by Th19;

    end;

    theorem :: TOPALG_1:21

    

     Th21: (a,b) are_connected & (c,b) are_connected implies for A1,A2 be Path of a, b, B be Path of c, b holds (A1,A2) are_homotopic implies (A1,((A2 + ( - B)) + B)) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (c,b) are_connected ;

      set X = the constant Path of b, b;

      let A1,A2 be Path of a, b, B be Path of c, b;

      

       A3: (A1,(A1 + X)) are_homotopic by A1, BORSUK_6: 80;

      assume

       A4: (A1,A2) are_homotopic ;

      ((( - B) + B),X) are_homotopic by A2, BORSUK_6: 86;

      then ((A2 + (( - B) + B)),(A1 + X)) are_homotopic by A1, A4, BORSUK_6: 75;

      then

       A5: ((A2 + (( - B) + B)),A1) are_homotopic by A3, BORSUK_6: 79;

      ((A2 + (( - B) + B)),((A2 + ( - B)) + B)) are_homotopic by A1, A2, BORSUK_6: 73;

      hence thesis by A5, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:22

    for A1,A2 be Path of a1, b1, B be Path of c1, b1 holds (A1,A2) are_homotopic implies (A1,((A2 + ( - B)) + B)) are_homotopic

    proof

      (a1,b1) are_connected & (c1,b1) are_connected by BORSUK_2:def 3;

      hence thesis by Th21;

    end;

    theorem :: TOPALG_1:23

    

     Th23: (a,b) are_connected & (c,a) are_connected implies for A1,A2 be Path of a, b, B be Path of c, a holds (A1,A2) are_homotopic implies (A1,((( - B) + B) + A2)) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (c,a) are_connected ;

      set X = the constant Path of a, a;

      let A1,A2 be Path of a, b, B be Path of c, a;

      

       A3: (A1,(X + A1)) are_homotopic by A1, BORSUK_6: 82;

      assume

       A4: (A1,A2) are_homotopic ;

      ((( - B) + B),X) are_homotopic by A2, BORSUK_6: 86;

      then (((( - B) + B) + A2),(X + A1)) are_homotopic by A1, A4, BORSUK_6: 75;

      hence thesis by A3, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:24

    for A1,A2 be Path of a1, b1, B be Path of c1, a1 holds (A1,A2) are_homotopic implies (A1,((( - B) + B) + A2)) are_homotopic

    proof

      (a1,b1) are_connected & (c1,a1) are_connected by BORSUK_2:def 3;

      hence thesis by Th23;

    end;

    theorem :: TOPALG_1:25

    

     Th25: (a,b) are_connected & (a,c) are_connected implies for A1,A2 be Path of a, b, B be Path of a, c holds (A1,A2) are_homotopic implies (A1,((B + ( - B)) + A2)) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (a,c) are_connected ;

      set X = the constant Path of a, a;

      let A1,A2 be Path of a, b, B be Path of a, c;

      

       A3: (A1,(X + A1)) are_homotopic by A1, BORSUK_6: 82;

      assume

       A4: (A1,A2) are_homotopic ;

      ((B + ( - B)),X) are_homotopic by A2, BORSUK_6: 84;

      then (((B + ( - B)) + A2),(X + A1)) are_homotopic by A1, A4, BORSUK_6: 75;

      hence thesis by A3, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:26

    for A1,A2 be Path of a1, b1, B be Path of a1, c1 holds (A1,A2) are_homotopic implies (A1,((B + ( - B)) + A2)) are_homotopic

    proof

      (a1,b1) are_connected & (a1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by Th25;

    end;

    theorem :: TOPALG_1:27

    

     Th27: (a,b) are_connected & (c,b) are_connected implies for A,B be Path of a, b, C be Path of b, c st ((A + C),(B + C)) are_homotopic holds (A,B) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (c,b) are_connected ;

      let A,B be Path of a, b, C be Path of b, c;

      

       A3: (((A + C) + ( - C)),A) are_homotopic by A1, A2, Th19, BORSUK_2: 12;

      assume

       A4: ((A + C),(B + C)) are_homotopic ;

      (a,c) are_connected & (( - C),( - C)) are_homotopic by A1, A2, BORSUK_2: 12, BORSUK_6: 42;

      then (((A + C) + ( - C)),((B + C) + ( - C))) are_homotopic by A2, A4, BORSUK_6: 75;

      then

       A5: (A,((B + C) + ( - C))) are_homotopic by A3, BORSUK_6: 79;

      (((B + C) + ( - C)),B) are_homotopic by A1, A2, Th19, BORSUK_2: 12;

      hence thesis by A5, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:28

    for A,B be Path of a1, b1, C be Path of b1, c1 st ((A + C),(B + C)) are_homotopic holds (A,B) are_homotopic

    proof

      (a1,b1) are_connected & (c1,b1) are_connected by BORSUK_2:def 3;

      hence thesis by Th27;

    end;

    theorem :: TOPALG_1:29

    

     Th29: (a,b) are_connected & (a,c) are_connected implies for A,B be Path of a, b, C be Path of c, a st ((C + A),(C + B)) are_homotopic holds (A,B) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (a,c) are_connected ;

      let A,B be Path of a, b, C be Path of c, a;

      

       A3: (((( - C) + C) + A),(( - C) + (C + A))) are_homotopic by A1, A2, BORSUK_6: 73;

      assume

       A4: ((C + A),(C + B)) are_homotopic ;

      (b,c) are_connected & (( - C),( - C)) are_homotopic by A1, A2, BORSUK_2: 12, BORSUK_6: 42;

      then ((( - C) + (C + A)),(( - C) + (C + B))) are_homotopic by A2, A4, BORSUK_6: 75;

      then

       A5: (((( - C) + C) + A),(( - C) + (C + B))) are_homotopic by A3, BORSUK_6: 79;

      (((( - C) + C) + B),(( - C) + (C + B))) are_homotopic by A1, A2, BORSUK_6: 73;

      then

       A6: (((( - C) + C) + A),((( - C) + C) + B)) are_homotopic by A5, BORSUK_6: 79;

      (((( - C) + C) + A),A) are_homotopic by A1, A2, Th23, BORSUK_2: 12;

      then

       A7: (A,((( - C) + C) + B)) are_homotopic by A6, BORSUK_6: 79;

      (((( - C) + C) + B),B) are_homotopic by A1, A2, Th23, BORSUK_2: 12;

      hence thesis by A7, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:30

    for A,B be Path of a1, b1, C be Path of c1, a1 st ((C + A),(C + B)) are_homotopic holds (A,B) are_homotopic

    proof

      (a1,b1) are_connected & (a1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by Th29;

    end;

    theorem :: TOPALG_1:31

    

     Th31: (a,b) are_connected & (b,c) are_connected & (c,d) are_connected & (d,e) are_connected implies for A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e holds ((((A + B) + C) + D),((A + (B + C)) + D)) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected & (b,c) are_connected and

       A2: (c,d) are_connected and

       A3: (d,e) are_connected ;

      (a,c) are_connected by A1, BORSUK_6: 42;

      then

       A4: (a,d) are_connected by A2, BORSUK_6: 42;

      let A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e;

      (((A + B) + C),(A + (B + C))) are_homotopic & (D,D) are_homotopic by A1, A2, A3, BORSUK_2: 12, BORSUK_6: 73;

      hence thesis by A3, A4, BORSUK_6: 75;

    end;

    theorem :: TOPALG_1:32

    for A be Path of a1, b1, B be Path of b1, c1, C be Path of c1, d1, D be Path of d1, e1 holds ((((A + B) + C) + D),((A + (B + C)) + D)) are_homotopic

    proof

      

       A1: (c1,d1) are_connected & (d1,e1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (b1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, Th31;

    end;

    theorem :: TOPALG_1:33

    

     Th33: (a,b) are_connected & (b,c) are_connected & (c,d) are_connected & (d,e) are_connected implies for A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e holds ((((A + B) + C) + D),(A + ((B + C) + D))) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (b,c) are_connected & (c,d) are_connected and

       A3: (d,e) are_connected ;

      let A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e;

      

       A4: ((A + (B + C)),((A + B) + C)) are_homotopic & (D,D) are_homotopic by A1, A2, A3, BORSUK_2: 12, BORSUK_6: 73;

      

       A5: (b,d) are_connected by A2, BORSUK_6: 42;

      then (a,d) are_connected by A1, BORSUK_6: 42;

      then

       A6: (((A + (B + C)) + D),(((A + B) + C) + D)) are_homotopic by A3, A4, BORSUK_6: 75;

      (((A + (B + C)) + D),(A + ((B + C) + D))) are_homotopic by A1, A3, A5, BORSUK_6: 73;

      hence thesis by A6, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:34

    for A be Path of a1, b1, B be Path of b1, c1, C be Path of c1, d1, D be Path of d1, e1 holds ((((A + B) + C) + D),(A + ((B + C) + D))) are_homotopic

    proof

      

       A1: (c1,d1) are_connected & (d1,e1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (b1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, Th33;

    end;

    theorem :: TOPALG_1:35

    

     Th35: (a,b) are_connected & (b,c) are_connected & (c,d) are_connected & (d,e) are_connected implies for A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e holds (((A + (B + C)) + D),((A + B) + (C + D))) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected & (b,c) are_connected and

       A2: (c,d) are_connected & (d,e) are_connected ;

      let A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e;

      (a,c) are_connected by A1, BORSUK_6: 42;

      then

       A3: ((((A + B) + C) + D),((A + B) + (C + D))) are_homotopic by A2, BORSUK_6: 73;

      ((((A + B) + C) + D),((A + (B + C)) + D)) are_homotopic by A1, A2, Th31;

      hence thesis by A3, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:36

    for A be Path of a1, b1, B be Path of b1, c1, C be Path of c1, d1, D be Path of d1, e1 holds (((A + (B + C)) + D),((A + B) + (C + D))) are_homotopic

    proof

      

       A1: (c1,d1) are_connected & (d1,e1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (b1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, Th35;

    end;

    theorem :: TOPALG_1:37

    

     Th37: (a,b) are_connected & (b,c) are_connected & (b,d) are_connected implies for A be Path of a, b, B be Path of d, b, C be Path of b, c holds ((((A + ( - B)) + B) + C),(A + C)) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (b,c) are_connected and

       A3: (b,d) are_connected ;

      let A be Path of a, b, B be Path of d, b, C be Path of b, c;

      

       A4: ((((A + ( - B)) + B) + C),(A + ((( - B) + B) + C))) are_homotopic by A1, A2, A3, Th33;

      set X = the constant Path of b, b;

      (C,C) are_homotopic & ((( - B) + B),X) are_homotopic by A2, A3, BORSUK_2: 12, BORSUK_6: 86;

      then

       A5: (((( - B) + B) + C),(X + C)) are_homotopic by A2, BORSUK_6: 75;

      ((X + C),C) are_homotopic by A2, BORSUK_6: 82;

      then

       A6: (((( - B) + B) + C),C) are_homotopic by A5, BORSUK_6: 79;

      (A,A) are_homotopic by A1, BORSUK_2: 12;

      then ((A + ((( - B) + B) + C)),(A + C)) are_homotopic by A1, A2, A6, BORSUK_6: 75;

      hence thesis by A4, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:38

    for A be Path of a1, b1, B be Path of d1, b1, C be Path of b1, c1 holds ((((A + ( - B)) + B) + C),(A + C)) are_homotopic

    proof

      

       A1: (b1,d1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (b1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, Th37;

    end;

    theorem :: TOPALG_1:39

    

     Th39: (a,b) are_connected & (a,c) are_connected & (c,d) are_connected implies for A be Path of a, b, B be Path of c, d, C be Path of a, c holds (((((A + ( - A)) + C) + B) + ( - B)),C) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected and

       A2: (a,c) are_connected and

       A3: (c,d) are_connected ;

      let A be Path of a, b, B be Path of c, d, C be Path of a, c;

      ((B + ( - B)),(B + ( - B))) are_homotopic & (((A + ( - A)) + C),C) are_homotopic by A1, A2, Th25, BORSUK_2: 12;

      then

       A4: ((((A + ( - A)) + C) + (B + ( - B))),(C + (B + ( - B)))) are_homotopic by A2, BORSUK_6: 75;

      (C,((C + B) + ( - B))) are_homotopic & (((C + B) + ( - B)),(C + (B + ( - B)))) are_homotopic by A2, A3, Th19, BORSUK_2: 12, BORSUK_6: 73;

      then

       A5: (C,(C + (B + ( - B)))) are_homotopic by BORSUK_6: 79;

      (((((A + ( - A)) + C) + B) + ( - B)),(((A + ( - A)) + C) + (B + ( - B)))) are_homotopic by A2, A3, BORSUK_6: 73;

      then (((((A + ( - A)) + C) + B) + ( - B)),(C + (B + ( - B)))) are_homotopic by A4, BORSUK_6: 79;

      hence thesis by A5, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:40

    for A be Path of a1, b1, B be Path of c1, d1, C be Path of a1, c1 holds (((((A + ( - A)) + C) + B) + ( - B)),C) are_homotopic

    proof

      

       A1: (c1,d1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (a1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, Th39;

    end;

    theorem :: TOPALG_1:41

    

     Th41: (a,b) are_connected & (a,c) are_connected & (d,c) are_connected implies for A be Path of a, b, B be Path of c, d, C be Path of a, c holds (((A + ((( - A) + C) + B)) + ( - B)),C) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected & (a,c) are_connected and

       A2: (d,c) are_connected ;

      let A be Path of a, b, B be Path of c, d, C be Path of a, c;

      

       A3: (((((A + ( - A)) + C) + B) + ( - B)),C) are_homotopic by A1, A2, Th39;

      

       A4: (( - B),( - B)) are_homotopic by A2, BORSUK_2: 12;

      ((A + ((( - A) + C) + B)),(((A + ( - A)) + C) + B)) are_homotopic & (a,d) are_connected by A1, A2, Th33, BORSUK_6: 42;

      then (((A + ((( - A) + C) + B)) + ( - B)),((((A + ( - A)) + C) + B) + ( - B))) are_homotopic by A2, A4, BORSUK_6: 75;

      hence thesis by A3, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:42

    for A be Path of a1, b1, B be Path of c1, d1, C be Path of a1, c1 holds (((A + ((( - A) + C) + B)) + ( - B)),C) are_homotopic

    proof

      

       A1: (a1,c1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (d1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, Th41;

    end;

    theorem :: TOPALG_1:43

    

     Th43: (a,b) are_connected & (b,c) are_connected & (c,d) are_connected & (d,e) are_connected & (a,f) are_connected implies for A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e, E be Path of f, c holds (((A + (B + C)) + D),(((A + B) + ( - E)) + ((E + C) + D))) are_homotopic

    proof

      assume that

       A1: (a,b) are_connected & (b,c) are_connected and

       A2: (c,d) are_connected & (d,e) are_connected and

       A3: (a,f) are_connected ;

      let A be Path of a, b, B be Path of b, c, C be Path of c, d, D be Path of d, e, E be Path of f, c;

      

       A4: (((A + B) + ( - E)),((A + B) + ( - E))) are_homotopic by A3, BORSUK_2: 12;

      

       A5: (a,c) are_connected by A1, BORSUK_6: 42;

      then

       A6: (f,c) are_connected by A3, BORSUK_6: 42;

      then

       A7: ((E + (C + D)),((E + C) + D)) are_homotopic by A2, BORSUK_6: 73;

      

       A8: (c,e) are_connected by A2, BORSUK_6: 42;

      then

       A9: ((((A + B) + ( - E)) + (E + (C + D))),((((A + B) + ( - E)) + E) + (C + D))) are_homotopic by A3, A6, BORSUK_6: 73;

      

       A10: (((A + B) + (C + D)),((A + (B + C)) + D)) are_homotopic by A1, A2, Th35;

      (f,e) are_connected by A8, A6, BORSUK_6: 42;

      then ((((A + B) + ( - E)) + (E + (C + D))),(((A + B) + ( - E)) + ((E + C) + D))) are_homotopic by A3, A7, A4, BORSUK_6: 75;

      then

       A11: (((((A + B) + ( - E)) + E) + (C + D)),(((A + B) + ( - E)) + ((E + C) + D))) are_homotopic by A9, BORSUK_6: 79;

      (((((A + B) + ( - E)) + E) + (C + D)),((A + B) + (C + D))) are_homotopic by A5, A8, A6, Th37;

      then (((A + (B + C)) + D),((((A + B) + ( - E)) + E) + (C + D))) are_homotopic by A10, BORSUK_6: 79;

      hence thesis by A11, BORSUK_6: 79;

    end;

    theorem :: TOPALG_1:44

    for A be Path of a1, b1, B be Path of b1, c1, C be Path of c1, d1, D be Path of d1, e1, E be Path of f1, c1 holds (((A + (B + C)) + D),(((A + B) + ( - E)) + ((E + C) + D))) are_homotopic

    proof

      

       A1: (c1,d1) are_connected & (d1,e1) are_connected by BORSUK_2:def 3;

      

       A2: (a1,f1) are_connected by BORSUK_2:def 3;

      (a1,b1) are_connected & (b1,c1) are_connected by BORSUK_2:def 3;

      hence thesis by A1, A2, Th43;

    end;

    begin

    definition

      let T be TopStruct, t be Point of T;

      mode Loop of t is Path of t, t;

    end

    definition

      let T be non empty TopStruct, t1,t2 be Point of T;

      defpred P[ object] means $1 is Path of t1, t2;

      :: TOPALG_1:def1

      func Paths (t1,t2) -> set means

      : Def1: for x be object holds x in it iff x is Path of t1, t2;

      existence

      proof

        consider X be set such that

         A1: for x be object holds x in X iff x in ( Funcs (the carrier of I[01] ,the carrier of T)) & P[x] from XBOOLE_0:sch 1;

        take X;

        let x be object;

        thus x in X implies x is Path of t1, t2 by A1;

        assume

         A2: x is Path of t1, t2;

        then x in ( Funcs (the carrier of I[01] ,the carrier of T)) by FUNCT_2: 8;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        thus for X1,X2 be set st (for x be object holds x in X1 iff P[x]) & (for x be object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;

      end;

    end

    registration

      let T be non empty TopStruct, t1,t2 be Point of T;

      cluster ( Paths (t1,t2)) -> non empty;

      coherence

      proof

         the Path of t1, t2 in ( Paths (t1,t2)) by Def1;

        hence thesis;

      end;

    end

    definition

      let T be non empty TopStruct, t be Point of T;

      :: TOPALG_1:def2

      func Loops (t) -> set equals ( Paths (t,t));

      coherence ;

    end

    registration

      let T be non empty TopStruct, t be Point of T;

      cluster ( Loops t) -> non empty;

      coherence ;

    end

    

     Lm2: for X be non empty TopSpace, a,b be Point of X st (a,b) are_connected holds ex E be Equivalence_Relation of ( Paths (a,b)) st for x,y be object holds [x, y] in E iff x in ( Paths (a,b)) & y in ( Paths (a,b)) & ex P,Q be Path of a, b st P = x & Q = y & (P,Q) are_homotopic

    proof

      let X be non empty TopSpace, a,b be Point of X such that

       A1: (a,b) are_connected ;

      defpred P[ object, object] means ex P,Q be Path of a, b st P = $1 & Q = $2 & (P,Q) are_homotopic ;

      

       A2: for x be object st x in ( Paths (a,b)) holds P[x, x]

      proof

        let x be object;

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

        then

        reconsider x as Path of a, b by Def1;

        (x,x) are_homotopic by A1, BORSUK_2: 12;

        hence thesis;

      end;

      

       A3: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z] by BORSUK_6: 79;

      

       A4: for x,y be object st P[x, y] holds P[y, x];

      thus ex EqR be Equivalence_Relation of ( Paths (a,b)) st for x,y be object holds [x, y] in EqR iff x in ( Paths (a,b)) & y in ( Paths (a,b)) & P[x, y] from EQREL_1:sch 1( A2, A4, A3);

    end;

    definition

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

      :: TOPALG_1:def3

      func EqRel (X,a,b) -> Relation of ( Paths (a,b)) means

      : Def3: for P,Q be Path of a, b holds [P, Q] in it iff (P,Q) are_homotopic ;

      existence

      proof

        consider E be Equivalence_Relation of ( Paths (a,b)) such that

         A2: for x,y be object holds [x, y] in E iff x in ( Paths (a,b)) & y in ( Paths (a,b)) & ex P,Q be Path of a, b st P = x & Q = y & (P,Q) are_homotopic by A1, Lm2;

        take E;

        let P,Q be Path of a, b;

        thus [P, Q] in E implies (P,Q) are_homotopic

        proof

          assume [P, Q] in E;

          then ex P1,Q1 be Path of a, b st P1 = P & Q1 = Q & (P1,Q1) are_homotopic by A2;

          hence thesis;

        end;

        P in ( Paths (a,b)) & Q in ( Paths (a,b)) by Def1;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let E,F be Relation of ( Paths (a,b)) such that

         A3: for P,Q be Path of a, b holds [P, Q] in E iff (P,Q) are_homotopic and

         A4: for P,Q be Path of a, b holds [P, Q] in F iff (P,Q) are_homotopic ;

        let x,y be object;

        thus [x, y] in E implies [x, y] in F

        proof

          assume

           A5: [x, y] in E;

          then x in ( Paths (a,b)) & y in ( Paths (a,b)) by ZFMISC_1: 87;

          then

          reconsider x, y as Path of a, b by Def1;

          (x,y) are_homotopic by A3, A5;

          hence thesis by A4;

        end;

        assume

         A6: [x, y] in F;

        then x in ( Paths (a,b)) & y in ( Paths (a,b)) by ZFMISC_1: 87;

        then

        reconsider x, y as Path of a, b by Def1;

        (x,y) are_homotopic by A4, A6;

        hence thesis by A3;

      end;

    end

    

     Lm3: (a,b) are_connected implies ( EqRel (X,a,b)) is non empty total symmetric transitive

    proof

      set E = ( EqRel (X,a,b));

      set W = ( Paths (a,b));

      assume

       A1: (a,b) are_connected ;

      then

      consider EqR be Equivalence_Relation of W such that

       A2: for x,y be object holds [x, y] in EqR iff x in W & y in W & ex P,Q be Path of a, b st P = x & Q = y & (P,Q) are_homotopic by Lm2;

      E = EqR

      proof

        let x,y be object;

        thus [x, y] in E implies [x, y] in EqR

        proof

          assume

           A3: [x, y] in E;

          then

           A4: x in W & y in W by ZFMISC_1: 87;

          then

          reconsider x, y as Path of a, b by Def1;

          (x,y) are_homotopic by A1, A3, Def3;

          hence thesis by A2, A4;

        end;

        assume

         A5: [x, y] in EqR;

        then x in W & y in W by ZFMISC_1: 87;

        then

        reconsider x, y as Path of a, b by Def1;

        ex P,Q be Path of a, b st P = x & Q = y & (P,Q) are_homotopic by A2, A5;

        hence thesis by A1, Def3;

      end;

      hence thesis by EQREL_1: 9, RELAT_1: 40;

    end;

    theorem :: TOPALG_1:45

    

     Th45: (a,b) are_connected implies for P,Q be Path of a, b holds Q in ( Class (( EqRel (X,a,b)),P)) iff (P,Q) are_homotopic

    proof

      set E = ( EqRel (X,a,b));

      assume

       A1: (a,b) are_connected ;

      let P,Q be Path of a, b;

      

       A2: E is non empty total symmetric transitive by A1, Lm3;

      hereby

        assume Q in ( Class (E,P));

        then [Q, P] in E by A2, EQREL_1: 19;

        hence (P,Q) are_homotopic by A1, Def3;

      end;

      assume (P,Q) are_homotopic ;

      then [Q, P] in E by A1, Def3;

      hence thesis by A2, EQREL_1: 19;

    end;

    theorem :: TOPALG_1:46

    

     Th46: (a,b) are_connected implies for P,Q be Path of a, b holds ( Class (( EqRel (X,a,b)),P)) = ( Class (( EqRel (X,a,b)),Q)) iff (P,Q) are_homotopic

    proof

      set E = ( EqRel (X,a,b));

      assume

       A1: (a,b) are_connected ;

      let P,Q be Path of a, b;

      

       A2: Q in ( Paths (a,b)) by Def1;

      

       A3: E is non empty total symmetric transitive by A1, Lm3;

      hereby

        assume ( Class (E,P)) = ( Class (E,Q));

        then P in ( Class (E,Q)) by A3, A2, EQREL_1: 23;

        hence (P,Q) are_homotopic by A1, Th45;

      end;

      assume (P,Q) are_homotopic ;

      then P in ( Class (E,Q)) by A1, Th45;

      hence thesis by A3, A2, EQREL_1: 23;

    end;

    definition

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

      :: TOPALG_1:def4

      func EqRel (X,a) -> Relation of ( Loops a) equals ( EqRel (X,a,a));

      coherence ;

    end

    registration

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

      cluster ( EqRel (X,a)) -> non empty total symmetric transitive;

      coherence by Lm3;

    end

    definition

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

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

      set A = ( Class E);

      set W = ( Loops a);

      :: TOPALG_1:def5

      func FundamentalGroup (X,a) -> strict multMagma means

      : Def5: the carrier of it = ( Class ( EqRel (X,a))) & for x,y be Element of it holds ex P,Q be Loop of a st x = ( Class (( EqRel (X,a)),P)) & y = ( Class (( EqRel (X,a)),Q)) & (the multF of it . (x,y)) = ( Class (( EqRel (X,a)),(P + Q)));

      existence

      proof

        defpred P[ set, set, set] means ex P,Q be Loop of a st $1 = ( Class (E,P)) & $2 = ( Class (E,Q)) & $3 = ( Class (E,(P + Q)));

        

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

        proof

          let x,y be Element of A;

          x in A;

          then

          consider P be object such that

           A2: P in W and

           A3: x = ( Class (E,P)) by EQREL_1:def 3;

          y in A;

          then

          consider Q be object such that

           A4: Q in W and

           A5: y = ( Class (E,Q)) by EQREL_1:def 3;

          reconsider P, Q as Loop of a by A2, A4, Def1;

          (P + Q) in W by Def1;

          then

          reconsider z = ( Class (E,(P + Q))) as Element of A by EQREL_1:def 3;

          take z;

          thus thesis by A3, A5;

        end;

        consider g be BinOp of A such that

         A6: for a,b be Element of A holds P[a, b, (g . (a,b))] from BINOP_1:sch 3( A1);

        take multMagma (# A, g #);

        thus thesis by A6;

      end;

      uniqueness

      proof

        let F,G be strict multMagma such that

         A7: the carrier of F = ( Class E) and

         A8: for x,y be Element of F holds ex P,Q be Loop of a st x = ( Class (E,P)) & y = ( Class (E,Q)) & (the multF of F . (x,y)) = ( Class (E,(P + Q))) and

         A9: the carrier of G = A and

         A10: for x,y be Element of G holds ex P,Q be Loop of a st x = ( Class (E,P)) & y = ( Class (E,Q)) & (the multF of G . (x,y)) = ( Class (E,(P + Q)));

        set g = the multF of G;

        set f = the multF of F;

        for c,d be Element of F holds (f . (c,d)) = (g . (c,d))

        proof

          let c,d be Element of F;

          consider P1,Q1 be Loop of a such that

           A11: c = ( Class (E,P1)) & d = ( Class (E,Q1)) and

           A12: (f . (c,d)) = ( Class (E,(P1 + Q1))) by A8;

          consider P2,Q2 be Loop of a such that

           A13: c = ( Class (E,P2)) & d = ( Class (E,Q2)) and

           A14: (g . (c,d)) = ( Class (E,(P2 + Q2))) by A7, A9, A10;

          (P1,P2) are_homotopic & (Q1,Q2) are_homotopic by A11, A13, Th46;

          then ((P1 + Q1),(P2 + Q2)) are_homotopic by BORSUK_6: 75;

          hence thesis by A12, A14, Th46;

        end;

        hence thesis by A7, A9, BINOP_1: 2;

      end;

    end

    notation

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

      synonym pi_1 (X,a) for FundamentalGroup (X,a);

    end

    registration

      let X be non empty TopSpace;

      let a be Point of X;

      cluster ( pi_1 (X,a)) -> non empty;

      coherence

      proof

        the carrier of ( pi_1 (X,a)) = ( Class ( EqRel (X,a))) by Def5;

        hence the carrier of ( pi_1 (X,a)) is non empty;

      end;

    end

    theorem :: TOPALG_1:47

    

     Th47: for x be set holds x in the carrier of ( pi_1 (X,a)) iff ex P be Loop of a st x = ( Class (( EqRel (X,a)),P))

    proof

      let x be set;

      

       A1: the carrier of ( pi_1 (X,a)) = ( Class ( EqRel (X,a))) by Def5;

      hereby

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

        then

        consider P be Element of ( Loops a) such that

         A2: x = ( Class (( EqRel (X,a)),P)) by A1, EQREL_1: 36;

        reconsider P as Loop of a by Def1;

        take P;

        thus x = ( Class (( EqRel (X,a)),P)) by A2;

      end;

      given P be Loop of a such that

       A3: x = ( Class (( EqRel (X,a)),P));

      P in ( Loops a) by Def1;

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

    end;

    

     Lm4: for S be non empty TopSpace, s be Point of S holds for x,y be Element of ( pi_1 (S,s)) holds for P,Q be Loop of s st x = ( Class (( EqRel (S,s)),P)) & y = ( Class (( EqRel (S,s)),Q)) holds (x * y) = ( Class (( EqRel (S,s)),(P + Q)))

    proof

      let S be non empty TopSpace;

      let s be Point of S;

      set X = ( pi_1 (S,s));

      let x,y be Element of X;

      let P,Q be Loop of s;

      consider P1,Q1 be Loop of s such that

       A1: x = ( Class (( EqRel (S,s)),P1)) & y = ( Class (( EqRel (S,s)),Q1)) and

       A2: (the multF of X . (x,y)) = ( Class (( EqRel (S,s)),(P1 + Q1))) by Def5;

      assume x = ( Class (( EqRel (S,s)),P)) & y = ( Class (( EqRel (S,s)),Q));

      then (P,P1) are_homotopic & (Q,Q1) are_homotopic by A1, Th46;

      then ((P + Q),(P1 + Q1)) are_homotopic by BORSUK_6: 75;

      hence thesis by A2, Th46;

    end;

    registration

      let X be non empty TopSpace;

      let a be Point of X;

      cluster ( pi_1 (X,a)) -> associative Group-like;

      coherence

      proof

        set C = the constant Loop of a;

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

        set G = ( pi_1 (X,a));

        set e = ( Class (E,C));

        C in ( Loops a) by Def1;

        then

         A1: e in ( Class E) by EQREL_1:def 3;

        thus G is associative

        proof

          let x,y,z be Element of G;

          consider A be Loop of a such that

           A2: x = ( Class (E,A)) by Th47;

          consider B be Loop of a such that

           A3: y = ( Class (E,B)) by Th47;

          consider BC be Loop of a such that

           A4: (y * z) = ( Class (E,BC)) by Th47;

          consider C be Loop of a such that

           A5: z = ( Class (E,C)) by Th47;

          (y * z) = ( Class (E,(B + C))) by A3, A5, Lm4;

          then (A,A) are_homotopic & (BC,(B + C)) are_homotopic by A4, Th46, BORSUK_2: 12;

          then

           A6: ((A + BC),(A + (B + C))) are_homotopic by BORSUK_6: 75;

          consider AB be Loop of a such that

           A7: (x * y) = ( Class (E,AB)) by Th47;

          (x * y) = ( Class (E,(A + B))) by A2, A3, Lm4;

          then (C,C) are_homotopic & (AB,(A + B)) are_homotopic by A7, Th46, BORSUK_2: 12;

          then

           A8: ((AB + C),((A + B) + C)) are_homotopic by BORSUK_6: 75;

          

           A9: (((A + B) + C),(A + (B + C))) are_homotopic by BORSUK_6: 73;

          

          thus ((x * y) * z) = ( Class (E,(AB + C))) by A5, A7, Lm4

          .= ( Class (E,((A + B) + C))) by A8, Th46

          .= ( Class (E,(A + (B + C)))) by A9, Th46

          .= ( Class (E,(A + BC))) by A6, Th46

          .= (x * (y * z)) by A2, A4, Lm4;

        end;

        reconsider e as Element of G by A1, Def5;

        take e;

        let h be Element of G;

        consider A be Loop of a such that

         A10: h = ( Class (E,A)) by Th47;

        

         A11: ((A + C),A) are_homotopic by BORSUK_6: 80;

        

        thus (h * e) = ( Class (E,(A + C))) by A10, Lm4

        .= h by A10, A11, Th46;

        

         A12: ((C + A),A) are_homotopic by BORSUK_6: 82;

        

        thus (e * h) = ( Class (E,(C + A))) by A10, Lm4

        .= h by A10, A12, Th46;

        set x = ( Class (E,( - A)));

        ( - A) in ( Loops a) by Def1;

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

        then

        reconsider x as Element of G by Def5;

        take x;

        

         A13: ((A + ( - A)),C) are_homotopic by BORSUK_6: 84;

        

        thus (h * x) = ( Class (E,(A + ( - A)))) by A10, Lm4

        .= e by A13, Th46;

        

         A14: ((( - A) + A),C) are_homotopic by BORSUK_6: 86;

        

        thus (x * h) = ( Class (E,(( - A) + A))) by A10, Lm4

        .= e by A14, Th46;

      end;

    end

    definition

      let T be non empty TopSpace, x0,x1 be Point of T, P be Path of x0, x1;

      assume

       A1: (x0,x1) are_connected ;

      :: TOPALG_1:def6

      func pi_1-iso (P) -> Function of ( pi_1 (T,x1)), ( pi_1 (T,x0)) means

      : Def6: for Q be Loop of x1 holds (it . ( Class (( EqRel (T,x1)),Q))) = ( Class (( EqRel (T,x0)),((P + Q) + ( - P))));

      existence

      proof

        defpred P[ set, set] means ex L be Loop of x1 st $1 = ( Class (( EqRel (T,x1)),L)) & $2 = ( Class (( EqRel (T,x0)),((P + L) + ( - P))));

        

         A2: (P,P) are_homotopic by A1, BORSUK_2: 12;

        

         A3: for x be Element of ( pi_1 (T,x1)) holds ex y be Element of ( pi_1 (T,x0)) st P[x, y]

        proof

          let x be Element of ( pi_1 (T,x1));

          consider Q be Loop of x1 such that

           A4: x = ( Class (( EqRel (T,x1)),Q)) by Th47;

          reconsider y = ( Class (( EqRel (T,x0)),((P + Q) + ( - P)))) as Element of ( pi_1 (T,x0)) by Th47;

          take y;

          thus thesis by A4;

        end;

        consider f be Function of the carrier of ( pi_1 (T,x1)), the carrier of ( pi_1 (T,x0)) such that

         A5: for x be Element of ( pi_1 (T,x1)) holds P[x, (f . x)] from FUNCT_2:sch 3( A3);

        reconsider f as Function of ( pi_1 (T,x1)), ( pi_1 (T,x0));

        take f;

        let Q be Loop of x1;

        the carrier of ( pi_1 (T,x1)) = ( Class ( EqRel (T,x1))) & Q in ( Loops x1) by Def1, Def5;

        then ( Class (( EqRel (T,x1)),Q)) is Element of ( pi_1 (T,x1)) by EQREL_1:def 3;

        then

        consider L be Loop of x1 such that

         A6: ( Class (( EqRel (T,x1)),Q)) = ( Class (( EqRel (T,x1)),L)) and

         A7: (f . ( Class (( EqRel (T,x1)),Q))) = ( Class (( EqRel (T,x0)),((P + L) + ( - P)))) by A5;

        

         A8: (( - P),( - P)) are_homotopic by A1, BORSUK_2: 12;

        (L,Q) are_homotopic by A6, Th46;

        then ((P + L),(P + Q)) are_homotopic by A1, A2, BORSUK_6: 75;

        then (((P + L) + ( - P)),((P + Q) + ( - P))) are_homotopic by A1, A8, BORSUK_6: 75;

        hence thesis by A7, Th46;

      end;

      uniqueness

      proof

        let f1,f2 be Function of ( pi_1 (T,x1)), ( pi_1 (T,x0)) such that

         A9: for Q be Loop of x1 holds (f1 . ( Class (( EqRel (T,x1)),Q))) = ( Class (( EqRel (T,x0)),((P + Q) + ( - P)))) and

         A10: for Q be Loop of x1 holds (f2 . ( Class (( EqRel (T,x1)),Q))) = ( Class (( EqRel (T,x0)),((P + Q) + ( - P))));

        for x be Element of ( pi_1 (T,x1)) holds (f1 . x) = (f2 . x)

        proof

          let x be Element of ( pi_1 (T,x1));

          consider L be Loop of x1 such that

           A11: x = ( Class (( EqRel (T,x1)),L)) by Th47;

          

          thus (f1 . x) = ( Class (( EqRel (T,x0)),((P + L) + ( - P)))) by A9, A11

          .= (f2 . x) by A10, A11;

        end;

        hence thesis;

      end;

    end

    reserve x0,x1 for Point of X,

P,Q for Path of x0, x1,

y0,y1 for Point of T,

R,V for Path of y0, y1;

    theorem :: TOPALG_1:48

    

     Th48: (x0,x1) are_connected & (P,Q) are_homotopic implies ( pi_1-iso P) = ( pi_1-iso Q)

    proof

      assume that

       A1: (x0,x1) are_connected and

       A2: (P,Q) are_homotopic ;

      for x be Element of ( pi_1 (X,x1)) holds (( pi_1-iso P) . x) = (( pi_1-iso Q) . x)

      proof

        

         A3: (( - P),( - Q)) are_homotopic by A1, A2, BORSUK_6: 77;

        let x be Element of ( pi_1 (X,x1));

        consider L be Loop of x1 such that

         A4: x = ( Class (( EqRel (X,x1)),L)) by Th47;

        (L,L) are_homotopic by BORSUK_2: 12;

        then ((P + L),(Q + L)) are_homotopic by A1, A2, BORSUK_6: 75;

        then

         A5: (((P + L) + ( - P)),((Q + L) + ( - Q))) are_homotopic by A1, A3, BORSUK_6: 75;

        

        thus (( pi_1-iso P) . x) = ( Class (( EqRel (X,x0)),((P + L) + ( - P)))) by A1, A4, Def6

        .= ( Class (( EqRel (X,x0)),((Q + L) + ( - Q)))) by A5, Th46

        .= (( pi_1-iso Q) . x) by A1, A4, Def6;

      end;

      hence thesis;

    end;

    theorem :: TOPALG_1:49

    (R,V) are_homotopic implies ( pi_1-iso R) = ( pi_1-iso V) by Th48, BORSUK_2:def 3;

    theorem :: TOPALG_1:50

    

     Th50: (x0,x1) are_connected implies ( pi_1-iso P) is Homomorphism of ( pi_1 (X,x1)), ( pi_1 (X,x0))

    proof

      set f = ( pi_1-iso P);

      assume

       A1: (x0,x1) are_connected ;

      now

        let x,y be Element of ( pi_1 (X,x1));

        consider A be Loop of x1 such that

         A2: x = ( Class (( EqRel (X,x1)),A)) by Th47;

        consider B be Loop of x1 such that

         A3: y = ( Class (( EqRel (X,x1)),B)) by Th47;

        consider D be Loop of x0 such that

         A4: (f . y) = ( Class (( EqRel (X,x0)),D)) by Th47;

        (f . y) = ( Class (( EqRel (X,x0)),((P + B) + ( - P)))) by A1, A3, Def6;

        then

         A5: (D,((P + B) + ( - P))) are_homotopic by A4, Th46;

        

         A6: (((P + (A + B)) + ( - P)),(((P + A) + ( - P)) + ((P + B) + ( - P)))) are_homotopic by A1, Th43;

        consider C be Loop of x0 such that

         A7: (f . x) = ( Class (( EqRel (X,x0)),C)) by Th47;

        (f . x) = ( Class (( EqRel (X,x0)),((P + A) + ( - P)))) by A1, A2, Def6;

        then (C,((P + A) + ( - P))) are_homotopic by A7, Th46;

        then ((C + D),(((P + A) + ( - P)) + ((P + B) + ( - P)))) are_homotopic by A5, BORSUK_6: 75;

        then

         A8: (((P + (A + B)) + ( - P)),(C + D)) are_homotopic by A6, BORSUK_6: 79;

        

        thus (f . (x * y)) = (f . ( Class (( EqRel (X,x1)),(A + B)))) by A2, A3, Lm4

        .= ( Class (( EqRel (X,x0)),((P + (A + B)) + ( - P)))) by A1, Def6

        .= ( Class (( EqRel (X,x0)),(C + D))) by A8, Th46

        .= ((f . x) * (f . y)) by A7, A4, Lm4;

      end;

      hence thesis by GROUP_6:def 6;

    end;

    registration

      let T be non empty pathwise_connected TopSpace, x0,x1 be Point of T, P be Path of x0, x1;

      cluster ( pi_1-iso P) -> multiplicative;

      coherence by Th50, BORSUK_2:def 3;

    end

    theorem :: TOPALG_1:51

    

     Th51: (x0,x1) are_connected implies ( pi_1-iso P) is one-to-one

    proof

      assume

       A1: (x0,x1) are_connected ;

      set f = ( pi_1-iso P);

      let a,b be object such that

       A2: a in ( dom f) and

       A3: b in ( dom f) and

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

      consider B be Loop of x1 such that

       A5: b = ( Class (( EqRel (X,x1)),B)) by A3, Th47;

      

       A6: (f . b) = ( Class (( EqRel (X,x0)),((P + B) + ( - P)))) by A1, A5, Def6;

      consider A be Loop of x1 such that

       A7: a = ( Class (( EqRel (X,x1)),A)) by A2, Th47;

      (f . a) = ( Class (( EqRel (X,x0)),((P + A) + ( - P)))) by A1, A7, Def6;

      then (((P + A) + ( - P)),((P + B) + ( - P))) are_homotopic by A4, A6, Th46;

      then ((P + A),(P + B)) are_homotopic by A1, Th27;

      then (A,B) are_homotopic by A1, Th29;

      hence thesis by A7, A5, Th46;

    end;

    theorem :: TOPALG_1:52

    

     Th52: (x0,x1) are_connected implies ( pi_1-iso P) is onto

    proof

      assume

       A1: (x0,x1) are_connected ;

      set f = ( pi_1-iso P);

      thus ( rng f) c= the carrier of ( pi_1 (X,x0));

      let y be object;

      assume y in the carrier of ( pi_1 (X,x0));

      then

      consider Y be Loop of x0 such that

       A2: y = ( Class (( EqRel (X,x0)),Y)) by Th47;

      

       A3: (((P + ((( - P) + Y) + P)) + ( - P)),Y) are_homotopic by A1, Th41;

      set Z = ( Class (( EqRel (X,x1)),((( - P) + Y) + P)));

      ( dom f) = the carrier of ( pi_1 (X,x1)) by FUNCT_2:def 1;

      then

       A4: Z in ( dom f) by Th47;

      (f . Z) = ( Class (( EqRel (X,x0)),((P + ((( - P) + Y) + P)) + ( - P)))) by A1, Def6

      .= y by A2, A3, Th46;

      hence thesis by A4, FUNCT_1:def 3;

    end;

    registration

      let T be non empty pathwise_connected TopSpace, x0,x1 be Point of T, P be Path of x0, x1;

      cluster ( pi_1-iso P) -> one-to-one onto;

      coherence by Th51, Th52, BORSUK_2:def 3;

    end

    theorem :: TOPALG_1:53

    

     Th53: (x0,x1) are_connected implies (( pi_1-iso P) " ) = ( pi_1-iso ( - P))

    proof

      set f = ( pi_1-iso P);

      set g = ( pi_1-iso ( - P));

      assume

       A1: (x0,x1) are_connected ;

      then f is one-to-one onto by Th51, Th52;

      then

       A2: (f " ) = (f qua Function " ) by TOPS_2:def 4;

      

       A3: f is one-to-one by A1, Th51;

      for x be Element of ( pi_1 (X,x0)) holds ((f " ) . x) = (g . x)

      proof

        let x be Element of ( pi_1 (X,x0));

        consider Q be Loop of x0 such that

         A4: x = ( Class (( EqRel (X,x0)),Q)) by Th47;

        ( - ( - P)) = P by A1, BORSUK_6: 43;

        then

         A5: (((P + ((( - P) + Q) + ( - ( - P)))) + ( - P)),Q) are_homotopic by A1, Th41;

        ( dom f) = the carrier of ( pi_1 (X,x1)) by FUNCT_2:def 1;

        then

         A6: ( Class (( EqRel (X,x1)),((( - P) + Q) + ( - ( - P))))) in ( dom f) by Th47;

        (f . ( Class (( EqRel (X,x1)),((( - P) + Q) + ( - ( - P)))))) = ( Class (( EqRel (X,x0)),((P + ((( - P) + Q) + ( - ( - P)))) + ( - P)))) by A1, Def6

        .= x by A4, A5, Th46;

        

        hence ((f " ) . x) = ( Class (( EqRel (X,x1)),((( - P) + Q) + ( - ( - P))))) by A3, A2, A6, FUNCT_1: 32

        .= (g . x) by A1, A4, Def6;

      end;

      hence thesis;

    end;

    theorem :: TOPALG_1:54

    (( pi_1-iso R) " ) = ( pi_1-iso ( - R)) by Th53, BORSUK_2:def 3;

    theorem :: TOPALG_1:55

    

     Th55: (x0,x1) are_connected implies for h be Homomorphism of ( pi_1 (X,x1)), ( pi_1 (X,x0)) st h = ( pi_1-iso P) holds h is bijective by Th51, Th52;

    theorem :: TOPALG_1:56

    ( pi_1-iso R) is bijective;

    theorem :: TOPALG_1:57

    (x0,x1) are_connected implies (( pi_1 (X,x0)),( pi_1 (X,x1))) are_isomorphic

    proof

      set P = the Path of x1, x0;

      assume

       A1: (x0,x1) are_connected ;

      then

      reconsider h = ( pi_1-iso P) as Homomorphism of ( pi_1 (X,x0)), ( pi_1 (X,x1)) by Th50;

      take h;

      thus thesis by A1, Th55;

    end;

    theorem :: TOPALG_1:58

    (( pi_1 (T,y0)),( pi_1 (T,y1))) are_isomorphic

    proof

      set R = the Path of y1, y0;

      take ( pi_1-iso R);

      thus thesis;

    end;

    begin

    definition

      let n be Nat, P,Q be Function of I[01] , ( TOP-REAL n);

      :: TOPALG_1:def7

      func RealHomotopy (P,Q) -> Function of [: I[01] , I[01] :], ( TOP-REAL n) means

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

      existence

      proof

        set I = the carrier of I[01] ;

        deffunc F( Element of I, Element of I) = (((1 - $2) * (P . $1)) + ($2 * (Q . $1)));

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

         A1: for x,y be Element of I holds (F . (x,y)) = F(x,y) from BINOP_1:sch 4;

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

        then

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

        take F;

        let x,y be Element of I;

        thus thesis by A1;

      end;

      uniqueness

      proof

        set I = the carrier of I[01] ;

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

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

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

        

         A4: 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 A2

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

        end;

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

        hence f = g by A4, BINOP_1: 2;

      end;

    end

    

     Lm5: for P,Q be continuous Function of I[01] , ( TOP-REAL n) holds ( RealHomotopy (P,Q)) is continuous

    proof

      set I = the carrier of I[01] ;

      let P,Q be continuous Function of I[01] , ( TOP-REAL n);

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

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

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

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

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

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

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

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

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

       A2: for x be Element of T, 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] :] = [:T, I:] by BORSUK_1:def 2;

      then

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

      

       A3: Pb is continuous by A2, Th18;

      

       A4: for p be Point of [: I[01] , I[01] :] holds (F . p) = (((Pa * PI) . p) + ((Pb * QI) . p))

      proof

        

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

        

         A6: ( 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

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

        

         A8: ( dom ( id I[01] )) = I & (( id I[01] ) . t) = t by FUNCT_1: 18, FUNCT_2:def 1;

        

         A9: ((Pb * QI) . p) = (Pb . (QI . (s,t))) by A7, FUNCT_2: 15

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

        .= (t * (Q . s)) by A2;

        

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

        .= (Pa . ((P . s),t)) by A6, A8, FUNCT_3:def 8

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

        

        thus (F . p) = (F . (s,t)) by A7

        .= (((Pa * PI) . p) + ((Pb * QI) . p)) by A10, A9, Def7;

      end;

      Pa is continuous by A1, Th17;

      hence thesis by A3, A4, Lm1;

    end;

    

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

    proof

      let a,b be Point of ( TOP-REAL n), P,Q be Path of a, b;

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

      let s be Point of I[01] ;

      

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

      .= ((P . s) + ( 0 * (Q . s))) by RLVECT_1:def 8

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

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

      

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

      .= (( 0. ( TOP-REAL n)) + (1 * (Q . s))) by RLVECT_1: 10

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

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

      let t be Point of I[01] ;

      

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

      

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

      .= (((1 * a) - (t * a)) + (t * a)) by A1, RLVECT_1: 35

      .= (1 * a) by RLVECT_4: 1

      .= a by RLVECT_1:def 8;

      

       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 Def7

      .= (((1 * b) - (t * b)) + (t * b)) by A2, RLVECT_1: 35

      .= (1 * b) by RLVECT_4: 1

      .= b by RLVECT_1:def 8;

    end;

    theorem :: TOPALG_1:59

    

     Th59: for a,b be Point of ( TOP-REAL n), P,Q be Path of a, b holds (P,Q) are_homotopic

    proof

      let a,b be Point of ( TOP-REAL n), P,Q be Path of a, b;

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

      thus F is continuous by Lm5;

      thus thesis by Lm6;

    end;

    registration

      let n be Nat, a,b be Point of ( TOP-REAL n), 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 Th59;

        hence thesis by BORSUK_6:def 11;

      end;

    end

    theorem :: TOPALG_1:60

    

     Th60: for a be Point of ( TOP-REAL n), C be Loop of a holds the carrier of ( pi_1 (( TOP-REAL n),a)) = {( Class (( EqRel (( TOP-REAL n),a)),C))}

    proof

      let a be Point of ( TOP-REAL n), C be Loop of a;

      set X = ( TOP-REAL n);

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

      hereby

        let x be object;

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

        then

        consider P be Loop of a such that

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

        (P,C) are_homotopic by Th59;

        then x = ( Class (E,C)) by A1, Th46;

        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 Def1;

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

      hence thesis by Def5;

    end;

    registration

      let n be Nat;

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

      cluster ( pi_1 (( TOP-REAL n),a)) -> trivial;

      coherence

      proof

        set C = the constant Loop of a;

        set X = ( TOP-REAL n);

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

        the carrier of ( pi_1 (X,a)) = ( Class E) by Def5;

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

        hence thesis by Def5;

      end;

    end

    theorem :: TOPALG_1:61

    for S be non empty TopSpace, s be Point of S holds for x,y be Element of ( pi_1 (S,s)) holds for P,Q be Loop of s st x = ( Class (( EqRel (S,s)),P)) & y = ( Class (( EqRel (S,s)),Q)) holds (x * y) = ( Class (( EqRel (S,s)),(P + Q))) by Lm4;

    theorem :: TOPALG_1:62

    

     Th62: for C be constant Loop of a holds ( 1_ ( pi_1 (X,a))) = ( Class (( EqRel (X,a)),C))

    proof

      let C be constant Loop of a;

      set G = ( pi_1 (X,a));

      reconsider g = ( Class (( EqRel (X,a)),C)) as Element of G by Th47;

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

      now

        let h be Element of G;

        consider P be Loop of a such that

         A1: h = ( Class (E,P)) by Th47;

        

         A2: (P,(P + C)) are_homotopic by BORSUK_6: 80;

        

        thus (h * g) = ( Class (E,(P + C))) by A1, Lm4

        .= h by A1, A2, Th46;

        

         A3: (P,(C + P)) are_homotopic by BORSUK_6: 82;

        

        thus (g * h) = ( Class (E,(C + P))) by A1, Lm4

        .= h by A1, A3, Th46;

      end;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: TOPALG_1:63

    for x,y be Element of ( pi_1 (X,a)), P be Loop of a st x = ( Class (( EqRel (X,a)),P)) & y = ( Class (( EqRel (X,a)),( - P))) holds (x " ) = y

    proof

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

      set G = ( pi_1 (X,a));

      let x,y be Element of G, P be Loop of a such that

       A1: x = ( Class (E,P)) & y = ( Class (E,( - P)));

      set C = the constant Loop of a;

      

       A2: ((( - P) + P),C) are_homotopic by BORSUK_6: 86;

      

       A3: (y * x) = ( Class (E,(( - P) + P))) by A1, Lm4

      .= ( Class (E,C)) by A2, Th46

      .= ( 1_ G) by Th62;

      

       A4: ((P + ( - P)),C) are_homotopic by BORSUK_6: 84;

      (x * y) = ( Class (E,(P + ( - P)))) by A1, Lm4

      .= ( Class (E,C)) by A4, Th46

      .= ( 1_ G) by Th62;

      hence thesis by A3, GROUP_1:def 5;

    end;

    registration

      let n;

      let P,Q be continuous Function of I[01] , ( TOP-REAL n);

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

      coherence by Lm5;

    end

    theorem :: TOPALG_1:64

    for a,b be Point of ( TOP-REAL n), P,Q be Path of a, b holds ( RealHomotopy (P,Q)) is Homotopy of P, Q

    proof

      let a,b be Point of ( TOP-REAL n), P,Q be Path of a, b;

      thus (P,Q) are_homotopic by Th59;

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

      thus thesis by Lm6;

    end;

    theorem :: TOPALG_1:65

    (a,b) are_connected implies ( EqRel (X,a,b)) is non empty total symmetric transitive by Lm3;