topalg_4.miz



    begin

    

     Lm1: 1 in {1, 2} by TARSKI:def 2;

    

     Lm2: 2 in {1, 2} by TARSKI:def 2;

    theorem :: TOPALG_4:1

    

     Th1: for G,H be non empty multMagma, x be Element of ( product <*G, H*>) holds ex g be Element of G, h be Element of H st x = <*g, h*>

    proof

      let G,H be non empty multMagma, x be Element of ( product <*G, H*>);

      the carrier of ( product <*G, H*>) = ( product ( Carrier <*G, H*>)) by GROUP_7:def 2;

      then

      consider g be Function such that

       A1: x = g and

       A2: ( dom g) = ( dom ( Carrier <*G, H*>)) and

       A3: for y be object st y in ( dom ( Carrier <*G, H*>)) holds (g . y) in (( Carrier <*G, H*>) . y) by CARD_3:def 5;

      

       A4: ex R be 1-sorted st R = ( <*G, H*> . 2) & (( Carrier <*G, H*>) . 2) = the carrier of R by Lm2, PRALG_1:def 15;

      

       A5: ( dom ( Carrier <*G, H*>)) = {1, 2} by PARTFUN1:def 2;

      then

      reconsider g as FinSequence by A2, FINSEQ_1: 2, FINSEQ_1:def 2;

      (g . 2) in (( Carrier <*G, H*>) . 2) by A3, A5, Lm2;

      then

      reconsider h1 = (g . 2) as Element of H by A4, FINSEQ_1: 44;

      

       A6: ex R be 1-sorted st R = ( <*G, H*> . 1) & (( Carrier <*G, H*>) . 1) = the carrier of R by Lm1, PRALG_1:def 15;

      (g . 1) in (( Carrier <*G, H*>) . 1) by A3, A5, Lm1;

      then

      reconsider g1 = (g . 1) as Element of G by A6, FINSEQ_1: 44;

      take g1, h1;

      ( len g) = 2 by A2, A5, FINSEQ_1: 2, FINSEQ_1:def 3;

      hence thesis by A1, FINSEQ_1: 44;

    end;

    definition

      let G1,G2,H1,H2 be non empty multMagma, f be Function of G1, H1, g be Function of G2, H2;

      :: TOPALG_4:def1

      func Gr2Iso (f,g) -> Function of ( product <*G1, G2*>), ( product <*H1, H2*>) means

      : Def1: for x be Element of ( product <*G1, G2*>) holds ex x1 be Element of G1, x2 be Element of G2 st x = <*x1, x2*> & (it . x) = <*(f . x1), (g . x2)*>;

      existence

      proof

        defpred P[ set, set] means ex x1 be Element of G1, x2 be Element of G2 st $1 = <*x1, x2*> & $2 = <*(f . x1), (g . x2)*>;

        

         A1: for x be Element of ( product <*G1, G2*>) holds ex y be Element of ( product <*H1, H2*>) st P[x, y]

        proof

          let x be Element of ( product <*G1, G2*>);

          consider a be Element of G1, h be Element of G2 such that

           A2: x = <*a, h*> by Th1;

          take <*(f . a), (g . h)*>, a, h;

          thus thesis by A2;

        end;

        ex h be Function of ( product <*G1, G2*>), ( product <*H1, H2*>) st for x be Element of ( product <*G1, G2*>) holds P[x, (h . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let F,G be Function of ( product <*G1, G2*>), ( product <*H1, H2*>) such that

         A3: for x be Element of ( product <*G1, G2*>) holds ex x1 be Element of G1, x2 be Element of G2 st x = <*x1, x2*> & (F . x) = <*(f . x1), (g . x2)*> and

         A4: for x be Element of ( product <*G1, G2*>) holds ex x1 be Element of G1, x2 be Element of G2 st x = <*x1, x2*> & (G . x) = <*(f . x1), (g . x2)*>;

        now

          let x be Element of ( product <*G1, G2*>);

          consider x1 be Element of G1, x2 be Element of G2 such that

           A5: x = <*x1, x2*> and

           A6: (F . x) = <*(f . x1), (g . x2)*> by A3;

          consider y1 be Element of G1, y2 be Element of G2 such that

           A7: x = <*y1, y2*> and

           A8: (G . x) = <*(f . y1), (g . y2)*> by A4;

          x1 = y1 by A5, A7, FINSEQ_1: 77;

          hence (F . x) = (G . x) by A5, A6, A7, A8, FINSEQ_1: 77;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPALG_4:2

    for G1,G2,H1,H2 be non empty multMagma, f be Function of G1, H1, g be Function of G2, H2, x1 be Element of G1, x2 be Element of G2 holds (( Gr2Iso (f,g)) . <*x1, x2*>) = <*(f . x1), (g . x2)*>

    proof

      let G1,G2,H1,H2 be non empty multMagma, f be Function of G1, H1, g be Function of G2, H2, x1 be Element of G1, x2 be Element of G2;

      consider y1 be Element of G1, y2 be Element of G2 such that

       A1: <*y1, y2*> = <*x1, x2*> and

       A2: (( Gr2Iso (f,g)) . <*x1, x2*>) = <*(f . y1), (g . y2)*> by Def1;

      x1 = y1 by A1, FINSEQ_1: 77;

      hence thesis by A1, A2, FINSEQ_1: 77;

    end;

    registration

      let G1,G2,H1,H2 be Group, f be Homomorphism of G1, H1, g be Homomorphism of G2, H2;

      cluster ( Gr2Iso (f,g)) -> multiplicative;

      coherence

      proof

        set h = ( Gr2Iso (f,g));

        let a,b be Element of ( product <*G1, G2*>);

        consider a1 be Element of G1, a2 be Element of G2 such that

         A1: a = <*a1, a2*> and

         A2: (h . a) = <*(f . a1), (g . a2)*> by Def1;

        consider b1 be Element of G1, b2 be Element of G2 such that

         A3: b = <*b1, b2*> and

         A4: (h . b) = <*(f . b1), (g . b2)*> by Def1;

        

         A5: (b . 2) = b2 by A3, FINSEQ_1: 44;

        consider r1 be Element of G1, r2 be Element of G2 such that

         A6: (a * b) = <*r1, r2*> and

         A7: (h . (a * b)) = <*(f . r1), (g . r2)*> by Def1;

        G2 = ( <*G1, G2*> . 2) & (a . 2) = a2 by A1, FINSEQ_1: 44;

        then (a2 * b2) = ( <*r1, r2*> . 2) by A6, A5, Lm2, GROUP_7: 1;

        

        then

         A8: (g . r2) = (g . (a2 * b2)) by FINSEQ_1: 44

        .= ((g . a2) * (g . b2)) by GROUP_6:def 6;

        

         A9: (b . 1) = b1 by A3, FINSEQ_1: 44;

        G1 = ( <*G1, G2*> . 1) & (a . 1) = a1 by A1, FINSEQ_1: 44;

        then (a1 * b1) = ( <*r1, r2*> . 1) by A6, A9, Lm1, GROUP_7: 1;

        

        then (f . r1) = (f . (a1 * b1)) by FINSEQ_1: 44

        .= ((f . a1) * (f . b1)) by GROUP_6:def 6;

        hence (h . (a * b)) = ((h . a) * (h . b)) by A2, A4, A7, A8, GROUP_7: 29;

      end;

    end

    theorem :: TOPALG_4:3

    

     Th3: for G1,G2,H1,H2 be non empty multMagma, f be Function of G1, H1, g be Function of G2, H2 st f is one-to-one & g is one-to-one holds ( Gr2Iso (f,g)) is one-to-one

    proof

      let G1,G2,H1,H2 be non empty multMagma;

      let f be Function of G1, H1, g be Function of G2, H2 such that

       A1: f is one-to-one and

       A2: g is one-to-one;

      let a,b be object;

      set h = ( Gr2Iso (f,g));

      assume a in ( dom h);

      then

      consider a1 be Element of G1, a2 be Element of G2 such that

       A3: a = <*a1, a2*> and

       A4: (h . a) = <*(f . a1), (g . a2)*> by Def1;

      assume b in ( dom h);

      then

      consider b1 be Element of G1, b2 be Element of G2 such that

       A5: b = <*b1, b2*> and

       A6: (h . b) = <*(f . b1), (g . b2)*> by Def1;

      assume

       A7: (h . a) = (h . b);

      then ( dom f) = the carrier of G1 & (f . a1) = (f . b1) by A4, A6, FINSEQ_1: 77, FUNCT_2:def 1;

      then

       A8: a1 = b1 by A1;

      ( dom g) = the carrier of G2 & (g . a2) = (g . b2) by A4, A6, A7, FINSEQ_1: 77, FUNCT_2:def 1;

      hence thesis by A2, A3, A5, A8;

    end;

    theorem :: TOPALG_4:4

    

     Th4: for G1,G2,H1,H2 be non empty multMagma, f be Function of G1, H1, g be Function of G2, H2 st f is onto & g is onto holds ( Gr2Iso (f,g)) is onto

    proof

      let G1,G2,H1,H2 be non empty multMagma;

      let f be Function of G1, H1, g be Function of G2, H2 such that

       A1: ( rng f) = the carrier of H1 and

       A2: ( rng g) = the carrier of H2;

      set h = ( Gr2Iso (f,g));

      thus ( rng h) c= the carrier of ( product <*H1, H2*>);

      let a be object;

      assume a in the carrier of ( product <*H1, H2*>);

      then

      consider x be Element of H1, y be Element of H2 such that

       A3: a = <*x, y*> by Th1;

      consider a2 be object such that

       A4: a2 in ( dom g) and

       A5: (g . a2) = y by A2, FUNCT_1:def 3;

      consider a1 be object such that

       A6: a1 in ( dom f) and

       A7: (f . a1) = x by A1, FUNCT_1:def 3;

      ( dom h) = the carrier of ( product <*G1, G2*>) & for g be Element of G1, h be Element of G2 holds <*g, h*> in the carrier of ( product <*G1, G2*>) by FUNCT_2:def 1;

      then

       A8: <*a1, a2*> in ( dom h) by A6, A4;

      then

      consider k1 be Element of G1, k2 be Element of G2 such that

       A9: <*a1, a2*> = <*k1, k2*> and

       A10: (h . <*a1, a2*>) = <*(f . k1), (g . k2)*> by Def1;

      a1 = k1 & a2 = k2 by A9, FINSEQ_1: 77;

      hence thesis by A3, A7, A5, A8, A10, FUNCT_1:def 3;

    end;

    theorem :: TOPALG_4:5

    

     Th5: for G1,G2,H1,H2 be Group, f be Homomorphism of G1, H1, g be Homomorphism of G2, H2 st f is bijective & g is bijective holds ( Gr2Iso (f,g)) is bijective by Th4, Th3;

    theorem :: TOPALG_4:6

    

     Th6: for G1,G2,H1,H2 be Group st (G1,H1) are_isomorphic & (G2,H2) are_isomorphic holds (( product <*G1, G2*>),( product <*H1, H2*>)) are_isomorphic

    proof

      let G1,G2,H1,H2 be Group;

      given h1 be Homomorphism of G1, H1 such that

       A1: h1 is bijective;

      given h2 be Homomorphism of G2, H2 such that

       A2: h2 is bijective;

      take ( Gr2Iso (h1,h2));

      thus thesis by A1, A2, Th5;

    end;

    begin

    set I = the carrier of I[01] ;

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

    reserve S,T,Y for non empty TopSpace,

s,s1,s2,s3 for Point of S,

t,t1,t2,t3 for Point of T,

l1,l2 for Path of [s1, t1], [s2, t2],

H for Homotopy of l1, l2;

    theorem :: TOPALG_4:7

    

     Th7: for f,g be Function st ( dom f) = ( dom g) holds ( pr1 <:f, g:>) = f

    proof

      let f,g be Function such that

       A1: ( dom f) = ( dom g);

      

       A2: ( dom ( pr1 <:f, g:>)) = ( dom <:f, g:>) by MCART_1:def 12;

      

       A3: for x be object st x in ( dom ( pr1 <:f, g:>)) holds (( pr1 <:f, g:>) . x) = (f . x)

      proof

        let x be object such that

         A4: x in ( dom ( pr1 <:f, g:>));

        

        thus (( pr1 <:f, g:>) . x) = (( <:f, g:> . x) `1 ) by A2, A4, MCART_1:def 12

        .= ( [(f . x), (g . x)] `1 ) by A2, A4, FUNCT_3:def 7

        .= (f . x);

      end;

      ( dom <:f, g:>) = (( dom f) /\ ( dom g)) by FUNCT_3:def 7

      .= ( dom f) by A1;

      hence thesis by A2, A3;

    end;

    theorem :: TOPALG_4:8

    

     Th8: for f,g be Function st ( dom f) = ( dom g) holds ( pr2 <:f, g:>) = g

    proof

      let f,g be Function such that

       A1: ( dom f) = ( dom g);

      

       A2: ( dom ( pr2 <:f, g:>)) = ( dom <:f, g:>) by MCART_1:def 13;

      

       A3: for x be object st x in ( dom ( pr2 <:f, g:>)) holds (( pr2 <:f, g:>) . x) = (g . x)

      proof

        let x be object such that

         A4: x in ( dom ( pr2 <:f, g:>));

        

        thus (( pr2 <:f, g:>) . x) = (( <:f, g:> . x) `2 ) by A2, A4, MCART_1:def 13

        .= ( [(f . x), (g . x)] `2 ) by A2, A4, FUNCT_3:def 7

        .= (g . x);

      end;

      ( dom <:f, g:>) = (( dom f) /\ ( dom g)) by FUNCT_3:def 7

      .= ( dom g) by A1;

      hence thesis by A2, A3;

    end;

    definition

      let S, T, Y;

      let f be Function of Y, S;

      let g be Function of Y, T;

      :: original: <:

      redefine

      func <:f,g:> -> Function of Y, [:S, T:] ;

      coherence

      proof

        ( dom f) = the carrier of Y & ( dom g) = the carrier of Y by FUNCT_2:def 1;

        then

         A1: ( dom <:f, g:>) = the carrier of Y by FUNCT_3: 50;

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;

        hence thesis by A1;

      end;

    end

    definition

      let S, T, Y;

      let f be Function of Y, [:S, T:];

      :: original: pr1

      redefine

      func pr1 f -> Function of Y, S ;

      coherence

      proof

        

         A1: ( dom ( pr1 f)) = ( dom f) by MCART_1:def 12;

        

         A2: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;

        

         A3: ( rng ( pr1 f)) c= the carrier of S

        proof

          let y be object;

          assume y in ( rng ( pr1 f));

          then

          consider x be object such that

           A4: x in ( dom ( pr1 f)) and

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

          (( pr1 f) . x) = ((f . x) `1 ) & (f . x) in ( rng f) by A1, A4, FUNCT_1:def 3, MCART_1:def 12;

          hence thesis by A2, A5, MCART_1: 10;

        end;

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

        hence thesis by A1, A3, FUNCT_2: 2;

      end;

      :: original: pr2

      redefine

      func pr2 f -> Function of Y, T ;

      coherence

      proof

        

         A6: ( dom ( pr2 f)) = ( dom f) by MCART_1:def 13;

        

         A7: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;

        

         A8: ( rng ( pr2 f)) c= the carrier of T

        proof

          let y be object;

          assume y in ( rng ( pr2 f));

          then

          consider x be object such that

           A9: x in ( dom ( pr2 f)) and

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

          (( pr2 f) . x) = ((f . x) `2 ) & (f . x) in ( rng f) by A6, A9, FUNCT_1:def 3, MCART_1:def 13;

          hence thesis by A7, A10, MCART_1: 10;

        end;

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

        hence thesis by A6, A8, FUNCT_2: 2;

      end;

    end

    theorem :: TOPALG_4:9

    

     Th9: for f be continuous Function of Y, [:S, T:] holds ( pr1 f) is continuous

    proof

      let f be continuous Function of Y, [:S, T:];

      set g = ( pr1 f);

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

      proof

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

         A1: (g . p) in V and

         A2: V is open;

        

         A3: [:V, ( [#] T):] is open by A2, BORSUK_1: 6;

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;

        then

        consider s,t be object such that s in the carrier of S and

         A4: t in the carrier of T and

         A5: (f . p) = [s, t] by ZFMISC_1:def 2;

        

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

        

        then (g . p) = ( [s, t] `1 ) by A5, MCART_1:def 12

        .= s;

        then (f . p) in [:V, ( [#] T):] by A1, A4, A5, ZFMISC_1: 87;

        then

        consider W be Subset of Y such that

         A7: p in W & W is open and

         A8: (f .: W) c= [:V, ( [#] T):] by A3, JGRAPH_2: 10;

        take W;

        thus p in W & W is open by A7;

        let y be object;

        assume y in (g .: W);

        then

        consider x be Point of Y such that

         A9: x in W and

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

        

         A11: (g . x) = ((f . x) `1 ) by A6, MCART_1:def 12;

        (f . x) in (f .: W) by A6, A9, FUNCT_1:def 6;

        hence thesis by A8, A10, A11, MCART_1: 10;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPALG_4:10

    

     Th10: for f be continuous Function of Y, [:S, T:] holds ( pr2 f) is continuous

    proof

      let f be continuous Function of Y, [:S, T:];

      set g = ( pr2 f);

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

      proof

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

         A1: (g . p) in V and

         A2: V is open;

        

         A3: [:( [#] S), V:] is open by A2, BORSUK_1: 6;

        the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;

        then

        consider s,t be object such that

         A4: s in the carrier of S and t in the carrier of T and

         A5: (f . p) = [s, t] by ZFMISC_1:def 2;

        

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

        

        then (g . p) = ( [s, t] `2 ) by A5, MCART_1:def 13

        .= t;

        then (f . p) in [:( [#] S), V:] by A1, A4, A5, ZFMISC_1: 87;

        then

        consider W be Subset of Y such that

         A7: p in W & W is open and

         A8: (f .: W) c= [:( [#] S), V:] by A3, JGRAPH_2: 10;

        take W;

        thus p in W & W is open by A7;

        let y be object;

        assume y in (g .: W);

        then

        consider x be Point of Y such that

         A9: x in W and

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

        

         A11: (g . x) = ((f . x) `2 ) by A6, MCART_1:def 13;

        (f . x) in (f .: W) by A6, A9, FUNCT_1:def 6;

        hence thesis by A8, A10, A11, MCART_1: 10;

      end;

      hence thesis by JGRAPH_2: 10;

    end;

    theorem :: TOPALG_4:11

    

     Th11: ( [s1, t1], [s2, t2]) are_connected implies (s1,s2) are_connected

    proof

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

       A1: L is continuous and

       A2: (L . 0 ) = [s1, t1] and

       A3: (L . 1) = [s2, t2];

      take f = ( pr1 L);

      thus f is continuous by A1, Th9;

      

       A4: ( dom f) = I & ( dom f) = ( dom L) by FUNCT_2:def 1, MCART_1:def 12;

      then j0 in ( dom L);

      

      hence (f . 0 ) = ( [s1, t1] `1 ) by A2, MCART_1:def 12

      .= s1;

      j1 in ( dom L) by A4;

      

      hence (f . 1) = ( [s2, t2] `1 ) by A3, MCART_1:def 12

      .= s2;

    end;

    theorem :: TOPALG_4:12

    

     Th12: ( [s1, t1], [s2, t2]) are_connected implies (t1,t2) are_connected

    proof

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

       A1: L is continuous and

       A2: (L . 0 ) = [s1, t1] and

       A3: (L . 1) = [s2, t2];

      take f = ( pr2 L);

      thus f is continuous by A1, Th10;

      

       A4: ( dom f) = I & ( dom f) = ( dom L) by FUNCT_2:def 1, MCART_1:def 13;

      then j0 in ( dom L);

      

      hence (f . 0 ) = ( [s1, t1] `2 ) by A2, MCART_1:def 13

      .= t1;

      j1 in ( dom L) by A4;

      

      hence (f . 1) = ( [s2, t2] `2 ) by A3, MCART_1:def 13

      .= t2;

    end;

    theorem :: TOPALG_4:13

    

     Th13: ( [s1, t1], [s2, t2]) are_connected implies for L be Path of [s1, t1], [s2, t2] holds ( pr1 L) is Path of s1, s2

    proof

      assume

       A1: ( [s1, t1], [s2, t2]) are_connected ;

      let L be Path of [s1, t1], [s2, t2];

      set f = ( pr1 L);

      

       A2: ( dom f) = I & ( dom f) = ( dom L) by FUNCT_2:def 1, MCART_1:def 12;

      then j0 in ( dom L);

      

      then

       A3: (f . 0 ) = ((L . 0 ) `1 ) by MCART_1:def 12

      .= ( [s1, t1] `1 ) by A1, BORSUK_2:def 2

      .= s1;

      j1 in ( dom L) by A2;

      

      then

       A4: (f . 1) = ((L . 1) `1 ) by MCART_1:def 12

      .= ( [s2, t2] `1 ) by A1, BORSUK_2:def 2

      .= s2;

      L is continuous by A1, BORSUK_2:def 2;

      then

       A5: f is continuous by Th9;

      then (s1,s2) are_connected by A3, A4;

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

    end;

    theorem :: TOPALG_4:14

    

     Th14: ( [s1, t1], [s2, t2]) are_connected implies for L be Path of [s1, t1], [s2, t2] holds ( pr2 L) is Path of t1, t2

    proof

      assume

       A1: ( [s1, t1], [s2, t2]) are_connected ;

      let L be Path of [s1, t1], [s2, t2];

      set f = ( pr2 L);

      

       A2: ( dom f) = I & ( dom f) = ( dom L) by FUNCT_2:def 1, MCART_1:def 13;

      then j0 in ( dom L);

      

      then

       A3: (f . 0 ) = ((L . 0 ) `2 ) by MCART_1:def 13

      .= ( [s1, t1] `2 ) by A1, BORSUK_2:def 2

      .= t1;

      j1 in ( dom L) by A2;

      

      then

       A4: (f . 1) = ((L . 1) `2 ) by MCART_1:def 13

      .= ( [s2, t2] `2 ) by A1, BORSUK_2:def 2

      .= t2;

      L is continuous by A1, BORSUK_2:def 2;

      then

       A5: f is continuous by Th10;

      then (t1,t2) are_connected by A3, A4;

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

    end;

    theorem :: TOPALG_4:15

    

     Th15: (s1,s2) are_connected & (t1,t2) are_connected implies ( [s1, t1], [s2, t2]) are_connected

    proof

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

       A1: f is continuous and

       A2: (f . 0 ) = s1 and

       A3: (f . 1) = s2;

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

       A4: g is continuous and

       A5: (g . 0 ) = t1 and

       A6: (g . 1) = t2;

      take <:f, g:>;

      thus <:f, g:> is continuous by A1, A4, YELLOW12: 41;

      

       A7: ( dom f) = I & ( dom g) = I by FUNCT_2:def 1;

      

      hence ( <:f, g:> . 0 ) = [(f . j0), (g . j0)] by FUNCT_3: 49

      .= [s1, t1] by A2, A5;

      

      thus ( <:f, g:> . 1) = [(f . j1), (g . j1)] by A7, FUNCT_3: 49

      .= [s2, t2] by A3, A6;

    end;

    theorem :: TOPALG_4:16

    

     Th16: (s1,s2) are_connected & (t1,t2) are_connected implies for L1 be Path of s1, s2, L2 be Path of t1, t2 holds <:L1, L2:> is Path of [s1, t1], [s2, t2]

    proof

      assume that

       A1: (s1,s2) are_connected and

       A2: (t1,t2) are_connected ;

      let L1 be Path of s1, s2, L2 be Path of t1, t2;

      L1 is continuous & L2 is continuous by A1, A2, BORSUK_2:def 2;

      then

       A3: <:L1, L2:> is continuous by YELLOW12: 41;

      

       A4: ( dom L1) = I & ( dom L2) = I by FUNCT_2:def 1;

      

      then

       A5: ( <:L1, L2:> . j1) = [(L1 . j1), (L2 . j1)] by FUNCT_3: 49

      .= [s2, (L2 . j1)] by A1, BORSUK_2:def 2

      .= [s2, t2] by A2, BORSUK_2:def 2;

      

       A6: ( <:L1, L2:> . j0) = [(L1 . j0), (L2 . j0)] by A4, FUNCT_3: 49

      .= [s1, (L2 . j0)] by A1, BORSUK_2:def 2

      .= [s1, t1] by A2, BORSUK_2:def 2;

      then ( [s1, t1], [s2, t2]) are_connected by A3, A5;

      hence thesis by A3, A6, A5, BORSUK_2:def 2;

    end;

    definition

      let S,T be non empty pathwise_connected TopSpace, s1,s2 be Point of S, t1,t2 be Point of T, L1 be Path of s1, s2, L2 be Path of t1, t2;

      :: original: <:

      redefine

      func <:L1,L2:> -> Path of [s1, t1], [s2, t2] ;

      coherence

      proof

        (s1,s2) are_connected & (t1,t2) are_connected by BORSUK_2:def 3;

        hence thesis by Th16;

      end;

    end

    definition

      let S,T be non empty TopSpace, s be Point of S, t be Point of T, L1 be Loop of s, L2 be Loop of t;

      :: original: <:

      redefine

      func <:L1,L2:> -> Loop of [s, t] ;

      coherence by Th16;

    end

    registration

      let S,T be non empty pathwise_connected TopSpace;

      cluster [:S, T:] -> pathwise_connected;

      coherence

      proof

        let a,b be Point of [:S, T:];

        consider a1 be Point of S, a2 be Point of T such that

         A1: a = [a1, a2] by BORSUK_1: 10;

        consider b1 be Point of S, b2 be Point of T such that

         A2: b = [b1, b2] by BORSUK_1: 10;

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

        hence thesis by A1, A2, Th15;

      end;

    end

    definition

      let S,T be non empty pathwise_connected TopSpace, s1,s2 be Point of S, t1,t2 be Point of T, L be Path of [s1, t1], [s2, t2];

      :: original: pr1

      redefine

      func pr1 L -> Path of s1, s2 ;

      coherence by BORSUK_2:def 3, Th13;

      :: original: pr2

      redefine

      func pr2 L -> Path of t1, t2 ;

      coherence by BORSUK_2:def 3, Th14;

    end

    definition

      let S,T be non empty TopSpace, s be Point of S, t be Point of T, L be Loop of [s, t];

      :: original: pr1

      redefine

      func pr1 L -> Loop of s ;

      coherence by Th13;

      :: original: pr2

      redefine

      func pr2 L -> Loop of t ;

      coherence by Th14;

    end

    

     Lm3: (l1,l2) are_homotopic implies ( pr1 H) is continuous & for a be Point of I[01] holds (( pr1 H) . (a, 0 )) = (( pr1 l1) . a) & (( pr1 H) . (a,1)) = (( pr1 l2) . a) & for b be Point of I[01] holds (( pr1 H) . ( 0 ,b)) = s1 & (( pr1 H) . (1,b)) = s2

    proof

      

       A1: ( dom l1) = I by FUNCT_2:def 1;

      

       A2: ( dom l2) = I by FUNCT_2:def 1;

      assume

       A3: (l1,l2) are_homotopic ;

      then H is continuous by BORSUK_6:def 11;

      hence ( pr1 H) is continuous by Th9;

      let a be Point of I[01] ;

      

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

      

      hence (( pr1 H) . (a, 0 )) = ((H . [a, j0]) `1 ) by MCART_1:def 12

      .= ((H . (a,j0)) `1 )

      .= ((l1 . a) `1 ) by A3, BORSUK_6:def 11

      .= (( pr1 l1) . a) by A1, MCART_1:def 12;

      

      thus (( pr1 H) . (a,1)) = ((H . [a, j1]) `1 ) by A4, MCART_1:def 12

      .= ((H . (a,j1)) `1 )

      .= ((l2 . a) `1 ) by A3, BORSUK_6:def 11

      .= (( pr1 l2) . a) by A2, MCART_1:def 12;

      let b be Point of I[01] ;

      

      thus (( pr1 H) . ( 0 ,b)) = ((H . [j0, b]) `1 ) by A4, MCART_1:def 12

      .= ((H . (j0,b)) `1 )

      .= ( [s1, t1] `1 ) by A3, BORSUK_6:def 11

      .= s1;

      

      thus (( pr1 H) . (1,b)) = ((H . [j1, b]) `1 ) by A4, MCART_1:def 12

      .= ((H . (j1,b)) `1 )

      .= ( [s2, t2] `1 ) by A3, BORSUK_6:def 11

      .= s2;

    end;

    

     Lm4: (l1,l2) are_homotopic implies ( pr2 H) is continuous & for a be Point of I[01] holds (( pr2 H) . (a, 0 )) = (( pr2 l1) . a) & (( pr2 H) . (a,1)) = (( pr2 l2) . a) & for b be Point of I[01] holds (( pr2 H) . ( 0 ,b)) = t1 & (( pr2 H) . (1,b)) = t2

    proof

      

       A1: ( dom l1) = I by FUNCT_2:def 1;

      

       A2: ( dom l2) = I by FUNCT_2:def 1;

      assume

       A3: (l1,l2) are_homotopic ;

      then H is continuous by BORSUK_6:def 11;

      hence ( pr2 H) is continuous by Th10;

      let a be Point of I[01] ;

      

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

      

      hence (( pr2 H) . (a, 0 )) = ((H . [a, j0]) `2 ) by MCART_1:def 13

      .= ((H . (a,j0)) `2 )

      .= ((l1 . a) `2 ) by A3, BORSUK_6:def 11

      .= (( pr2 l1) . a) by A1, MCART_1:def 13;

      

      thus (( pr2 H) . (a,1)) = ((H . [a, j1]) `2 ) by A4, MCART_1:def 13

      .= ((H . (a,j1)) `2 )

      .= ((l2 . a) `2 ) by A3, BORSUK_6:def 11

      .= (( pr2 l2) . a) by A2, MCART_1:def 13;

      let b be Point of I[01] ;

      

      thus (( pr2 H) . ( 0 ,b)) = ((H . [j0, b]) `2 ) by A4, MCART_1:def 13

      .= ((H . (j0,b)) `2 )

      .= ( [s1, t1] `2 ) by A3, BORSUK_6:def 11

      .= t1;

      

      thus (( pr2 H) . (1,b)) = ((H . [j1, b]) `2 ) by A4, MCART_1:def 13

      .= ((H . (j1,b)) `2 )

      .= ( [s2, t2] `2 ) by A3, BORSUK_6:def 11

      .= t2;

    end;

    theorem :: TOPALG_4:17

    for p,q be Path of s1, s2 st p = ( pr1 l1) & q = ( pr1 l2) & (l1,l2) are_homotopic holds ( pr1 H) is Homotopy of p, q

    proof

      let p,q be Path of s1, s2 such that

       A1: p = ( pr1 l1) & q = ( pr1 l2) & (l1,l2) are_homotopic ;

      thus (p,q) are_homotopic

      proof

        take ( pr1 H);

        thus thesis by A1, Lm3;

      end;

      thus thesis by A1, Lm3;

    end;

    theorem :: TOPALG_4:18

    for p,q be Path of t1, t2 st p = ( pr2 l1) & q = ( pr2 l2) & (l1,l2) are_homotopic holds ( pr2 H) is Homotopy of p, q

    proof

      let p,q be Path of t1, t2 such that

       A1: p = ( pr2 l1) & q = ( pr2 l2) & (l1,l2) are_homotopic ;

      thus (p,q) are_homotopic

      proof

        take ( pr2 H);

        thus thesis by A1, Lm4;

      end;

      thus thesis by A1, Lm4;

    end;

    theorem :: TOPALG_4:19

    

     Th19: for p,q be Path of s1, s2 st p = ( pr1 l1) & q = ( pr1 l2) & (l1,l2) are_homotopic holds (p,q) are_homotopic

    proof

      let p,q be Path of s1, s2 such that

       A1: p = ( pr1 l1) & q = ( pr1 l2) and

       A2: (l1,l2) are_homotopic ;

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

       A3: f is continuous & for a be Point of I[01] holds (f . (a, 0 )) = (l1 . a) & (f . (a,1)) = (l2 . a) & for b be Point of I[01] holds (f . ( 0 ,b)) = [s1, t1] & (f . (1,b)) = [s2, t2] by A2;

      take ( pr1 f);

      f is Homotopy of l1, l2 by A2, A3, BORSUK_6:def 11;

      hence thesis by A1, A2, Lm3;

    end;

    theorem :: TOPALG_4:20

    

     Th20: for p,q be Path of t1, t2 st p = ( pr2 l1) & q = ( pr2 l2) & (l1,l2) are_homotopic holds (p,q) are_homotopic

    proof

      let p,q be Path of t1, t2 such that

       A1: p = ( pr2 l1) & q = ( pr2 l2) and

       A2: (l1,l2) are_homotopic ;

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

       A3: f is continuous & for a be Point of I[01] holds (f . (a, 0 )) = (l1 . a) & (f . (a,1)) = (l2 . a) & for b be Point of I[01] holds (f . ( 0 ,b)) = [s1, t1] & (f . (1,b)) = [s2, t2] by A2;

      take ( pr2 f);

      f is Homotopy of l1, l2 by A2, A3, BORSUK_6:def 11;

      hence thesis by A1, A2, Lm4;

    end;

    

     Lm5: for p,q be Path of s1, s2, x,y be Path of t1, t2, f be Homotopy of p, q, g be Homotopy of x, y st p = ( pr1 l1) & q = ( pr1 l2) & x = ( pr2 l1) & y = ( pr2 l2) & (p,q) are_homotopic & (x,y) are_homotopic holds <:f, g:> is continuous & for a be Point of I[01] holds ( <:f, g:> . (a, 0 )) = (l1 . a) & ( <:f, g:> . (a,1)) = (l2 . a) & for b be Point of I[01] holds ( <:f, g:> . ( 0 ,b)) = [s1, t1] & ( <:f, g:> . (1,b)) = [s2, t2]

    proof

      let p,q be Path of s1, s2, x,y be Path of t1, t2, f be Homotopy of p, q, g be Homotopy of x, y such that

       A1: p = ( pr1 l1) and

       A2: q = ( pr1 l2) and

       A3: x = ( pr2 l1) and

       A4: y = ( pr2 l2) and

       A5: (p,q) are_homotopic and

       A6: (x,y) are_homotopic ;

      set h = <:f, g:>;

      f is continuous & g is continuous by A5, A6, BORSUK_6:def 11;

      hence h is continuous by YELLOW12: 41;

      let a be Point of I[01] ;

      

       A7: ( dom l1) = I by FUNCT_2:def 1;

      

       A8: the carrier of [:S, T:] = [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;

      

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

      

      hence (h . (a, 0 )) = [(f . [a, j0]), (g . [a, j0])] by FUNCT_3: 49

      .= [(f . (a,j0)), (g . (a,j0))]

      .= [(( pr1 l1) . a), (g . (a,j0))] by A1, A5, BORSUK_6:def 11

      .= [(( pr1 l1) . a), (( pr2 l1) . a)] by A3, A6, BORSUK_6:def 11

      .= [((l1 . a) `1 ), (( pr2 l1) . a)] by A7, MCART_1:def 12

      .= [((l1 . a) `1 ), ((l1 . a) `2 )] by A7, MCART_1:def 13

      .= (l1 . a) by A8, MCART_1: 21;

      

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

      

      thus (h . (a,1)) = [(f . [a, j1]), (g . [a, j1])] by A9, FUNCT_3: 49

      .= [(f . (a,j1)), (g . (a,j1))]

      .= [(( pr1 l2) . a), (g . (a,j1))] by A2, A5, BORSUK_6:def 11

      .= [(( pr1 l2) . a), (( pr2 l2) . a)] by A4, A6, BORSUK_6:def 11

      .= [((l2 . a) `1 ), (( pr2 l2) . a)] by A10, MCART_1:def 12

      .= [((l2 . a) `1 ), ((l2 . a) `2 )] by A10, MCART_1:def 13

      .= (l2 . a) by A8, MCART_1: 21;

      let b be Point of I[01] ;

      

      thus (h . ( 0 ,b)) = [(f . [j0, b]), (g . [j0, b])] by A9, FUNCT_3: 49

      .= [(f . (j0,b)), (g . (j0,b))]

      .= [s1, (g . (j0,b))] by A5, BORSUK_6:def 11

      .= [s1, t1] by A6, BORSUK_6:def 11;

      

      thus (h . (1,b)) = [(f . [j1, b]), (g . [j1, b])] by A9, FUNCT_3: 49

      .= [(f . (j1,b)), (g . (j1,b))]

      .= [s2, (g . (j1,b))] by A5, BORSUK_6:def 11

      .= [s2, t2] by A6, BORSUK_6:def 11;

    end;

    theorem :: TOPALG_4:21

    for p,q be Path of s1, s2, x,y be Path of t1, t2, f be Homotopy of p, q, g be Homotopy of x, y st p = ( pr1 l1) & q = ( pr1 l2) & x = ( pr2 l1) & y = ( pr2 l2) & (p,q) are_homotopic & (x,y) are_homotopic holds <:f, g:> is Homotopy of l1, l2

    proof

      let p,q be Path of s1, s2, x,y be Path of t1, t2, f be Homotopy of p, q, g be Homotopy of x, y such that

       A1: p = ( pr1 l1) & q = ( pr1 l2) & x = ( pr2 l1) & y = ( pr2 l2) & (p,q) are_homotopic & (x,y) are_homotopic ;

      thus (l1,l2) are_homotopic

      proof

        take <:f, g:>;

        thus thesis by A1, Lm5;

      end;

      thus thesis by A1, Lm5;

    end;

    theorem :: TOPALG_4:22

    

     Th22: for p,q be Path of s1, s2, x,y be Path of t1, t2 st p = ( pr1 l1) & q = ( pr1 l2) & x = ( pr2 l1) & y = ( pr2 l2) & (p,q) are_homotopic & (x,y) are_homotopic holds (l1,l2) are_homotopic

    proof

      let p,q be Path of s1, s2, x,y be Path of t1, t2 such that

       A1: p = ( pr1 l1) & q = ( pr1 l2) and

       A2: x = ( pr2 l1) & y = ( pr2 l2) and

       A3: (p,q) are_homotopic and

       A4: (x,y) are_homotopic ;

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

       A5: g is continuous & for a be Point of I[01] holds (g . (a, 0 )) = (( pr2 l1) . a) & (g . (a,1)) = (( pr2 l2) . a) & for b be Point of I[01] holds (g . ( 0 ,b)) = t1 & (g . (1,b)) = t2 by A2, A4;

      

       A6: g is Homotopy of x, y by A2, A4, A5, BORSUK_6:def 11;

      consider f be Function of [: I[01] , I[01] :], S such that

       A7: f is continuous & for a be Point of I[01] holds (f . (a, 0 )) = (( pr1 l1) . a) & (f . (a,1)) = (( pr1 l2) . a) & for b be Point of I[01] holds (f . ( 0 ,b)) = s1 & (f . (1,b)) = s2 by A1, A3;

      take <:f, g:>;

      f is Homotopy of p, q by A1, A3, A7, BORSUK_6:def 11;

      hence thesis by A1, A2, A3, A4, A6, Lm5;

    end;

    theorem :: TOPALG_4:23

    

     Th23: for l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3], p1 be Path of s1, s2, p2 be Path of s2, s3 st ( [s1, t1], [s2, t2]) are_connected & ( [s2, t2], [s3, t3]) are_connected & p1 = ( pr1 l1) & p2 = ( pr1 l2) holds ( pr1 (l1 + l2)) = (p1 + p2)

    proof

      let l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3], p1 be Path of s1, s2, p2 be Path of s2, s3 such that

       A1: ( [s1, t1], [s2, t2]) are_connected & ( [s2, t2], [s3, t3]) are_connected and

       A2: p1 = ( pr1 l1) and

       A3: p2 = ( pr1 l2);

      

       A4: (s1,s2) are_connected & (s2,s3) are_connected by A1, Th11;

      now

        

         A5: ( dom l2) = I by FUNCT_2:def 1;

        

         A6: ( dom l1) = I by FUNCT_2:def 1;

        let x be Element of I[01] ;

        

         A7: ( dom (l1 + l2)) = I by FUNCT_2:def 1;

        per cases ;

          suppose

           A8: x <= (1 / 2);

          then

           A9: (2 * x) is Point of I[01] by BORSUK_6: 3;

          

          thus (( pr1 (l1 + l2)) . x) = (((l1 + l2) . x) `1 ) by A7, MCART_1:def 12

          .= ((l1 . (2 * x)) `1 ) by A1, A8, BORSUK_2:def 5

          .= (p1 . (2 * x)) by A2, A6, A9, MCART_1:def 12

          .= ((p1 + p2) . x) by A4, A8, BORSUK_2:def 5;

        end;

          suppose

           A10: x >= (1 / 2);

          then

           A11: ((2 * x) - 1) is Point of I[01] by BORSUK_6: 4;

          

          thus (( pr1 (l1 + l2)) . x) = (((l1 + l2) . x) `1 ) by A7, MCART_1:def 12

          .= ((l2 . ((2 * x) - 1)) `1 ) by A1, A10, BORSUK_2:def 5

          .= (p2 . ((2 * x) - 1)) by A3, A5, A11, MCART_1:def 12

          .= ((p1 + p2) . x) by A4, A10, BORSUK_2:def 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPALG_4:24

    for S,T be non empty pathwise_connected TopSpace, s1,s2,s3 be Point of S, t1,t2,t3 be Point of T, l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3] holds ( pr1 (l1 + l2)) = (( pr1 l1) + ( pr1 l2))

    proof

      let S,T be non empty pathwise_connected TopSpace, s1,s2,s3 be Point of S, t1,t2,t3 be Point of T, l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3];

      ( [s1, t1], [s2, t2]) are_connected & ( [s2, t2], [s3, t3]) are_connected by BORSUK_2:def 3;

      hence thesis by Th23;

    end;

    theorem :: TOPALG_4:25

    

     Th25: for l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3], p1 be Path of t1, t2, p2 be Path of t2, t3 st ( [s1, t1], [s2, t2]) are_connected & ( [s2, t2], [s3, t3]) are_connected & p1 = ( pr2 l1) & p2 = ( pr2 l2) holds ( pr2 (l1 + l2)) = (p1 + p2)

    proof

      let l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3], p1 be Path of t1, t2, p2 be Path of t2, t3 such that

       A1: ( [s1, t1], [s2, t2]) are_connected & ( [s2, t2], [s3, t3]) are_connected and

       A2: p1 = ( pr2 l1) and

       A3: p2 = ( pr2 l2);

      

       A4: (t1,t2) are_connected & (t2,t3) are_connected by A1, Th12;

      now

        

         A5: ( dom l2) = I by FUNCT_2:def 1;

        

         A6: ( dom l1) = I by FUNCT_2:def 1;

        let x be Element of I[01] ;

        

         A7: ( dom (l1 + l2)) = I by FUNCT_2:def 1;

        per cases ;

          suppose

           A8: x <= (1 / 2);

          then

           A9: (2 * x) is Point of I[01] by BORSUK_6: 3;

          

          thus (( pr2 (l1 + l2)) . x) = (((l1 + l2) . x) `2 ) by A7, MCART_1:def 13

          .= ((l1 . (2 * x)) `2 ) by A1, A8, BORSUK_2:def 5

          .= (p1 . (2 * x)) by A2, A6, A9, MCART_1:def 13

          .= ((p1 + p2) . x) by A4, A8, BORSUK_2:def 5;

        end;

          suppose

           A10: x >= (1 / 2);

          then

           A11: ((2 * x) - 1) is Point of I[01] by BORSUK_6: 4;

          

          thus (( pr2 (l1 + l2)) . x) = (((l1 + l2) . x) `2 ) by A7, MCART_1:def 13

          .= ((l2 . ((2 * x) - 1)) `2 ) by A1, A10, BORSUK_2:def 5

          .= (p2 . ((2 * x) - 1)) by A3, A5, A11, MCART_1:def 13

          .= ((p1 + p2) . x) by A4, A10, BORSUK_2:def 5;

        end;

      end;

      hence thesis;

    end;

    theorem :: TOPALG_4:26

    for S,T be non empty pathwise_connected TopSpace, s1,s2,s3 be Point of S, t1,t2,t3 be Point of T, l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3] holds ( pr2 (l1 + l2)) = (( pr2 l1) + ( pr2 l2))

    proof

      let S,T be non empty pathwise_connected TopSpace, s1,s2,s3 be Point of S, t1,t2,t3 be Point of T, l1 be Path of [s1, t1], [s2, t2], l2 be Path of [s2, t2], [s3, t3];

      ( [s1, t1], [s2, t2]) are_connected & ( [s2, t2], [s3, t3]) are_connected by BORSUK_2:def 3;

      hence thesis by Th25;

    end;

    definition

      let S,T be non empty TopSpace, s be Point of S, t be Point of T;

      set pS = ( pi_1 ( [:S, T:], [s, t]));

      set G = <*( pi_1 (S,s)), ( pi_1 (T,t))*>;

      set pT = ( product G);

      :: TOPALG_4:def2

      func FGPrIso (s,t) -> Function of ( pi_1 ( [:S, T:], [s, t])), ( product <*( pi_1 (S,s)), ( pi_1 (T,t))*>) means

      : Def2: for x be Point of ( pi_1 ( [:S, T:], [s, t])) holds ex l be Loop of [s, t] st x = ( Class (( EqRel ( [:S, T:], [s, t])),l)) & (it . x) = <*( Class (( EqRel (S,s)),( pr1 l))), ( Class (( EqRel (T,t)),( pr2 l)))*>;

      existence

      proof

        defpred P[ set, set] means ex l be Loop of [s, t] st $1 = ( Class (( EqRel ( [:S, T:], [s, t])),l)) & $2 = <*( Class (( EqRel (S,s)),( pr1 l))), ( Class (( EqRel (T,t)),( pr2 l)))*>;

        

         A1: for x be Element of pS holds ex y be Element of pT st P[x, y]

        proof

          let x be Element of pS;

          consider l be Loop of [s, t] such that

           A2: x = ( Class (( EqRel ( [:S, T:], [s, t])),l)) by TOPALG_1: 47;

          set B = ( Class (( EqRel (T,t)),( pr2 l)));

          set A = ( Class (( EqRel (S,s)),( pr1 l)));

          

           A3: ( dom ( Carrier G)) = {1, 2} by PARTFUN1:def 2;

           A4:

          now

            let x be object such that

             A5: x in ( dom ( Carrier G));

            

             A6: x = 1 or x = 2 by A5, TARSKI:def 2;

            

             A7: ( <*A, B*> . 1) = A & ( <*A, B*> . 2) = B by FINSEQ_1: 44;

            

             A8: (G . 1) = ( pi_1 (S,s)) & (G . 2) = ( pi_1 (T,t)) by FINSEQ_1: 44;

            ex R be 1-sorted st R = (G . x) & (( Carrier G) . x) = the carrier of R by A5, PRALG_1:def 15;

            hence ( <*A, B*> . x) in (( Carrier G) . x) by A8, A7, A6, TOPALG_1: 47;

          end;

          the carrier of pT = ( product ( Carrier G)) & ( dom <*A, B*>) = {1, 2} by FINSEQ_1: 2, FINSEQ_1: 89, GROUP_7:def 2;

          then

          reconsider y = <*A, B*> as Element of pT by A3, A4, CARD_3: 9;

          take y, l;

          thus thesis by A2;

        end;

        ex h be Function of pS, pT st for x be Element of pS holds P[x, (h . x)] from FUNCT_2:sch 3( A1);

        hence thesis;

      end;

      uniqueness

      proof

        let f,g be Function of pS, pT such that

         A9: for x be Point of ( pi_1 ( [:S, T:], [s, t])) holds ex l be Loop of [s, t] st x = ( Class (( EqRel ( [:S, T:], [s, t])),l)) & (f . x) = <*( Class (( EqRel (S,s)),( pr1 l))), ( Class (( EqRel (T,t)),( pr2 l)))*> and

         A10: for x be Point of ( pi_1 ( [:S, T:], [s, t])) holds ex l be Loop of [s, t] st x = ( Class (( EqRel ( [:S, T:], [s, t])),l)) & (g . x) = <*( Class (( EqRel (S,s)),( pr1 l))), ( Class (( EqRel (T,t)),( pr2 l)))*>;

        now

          let x be Point of pS;

          consider l1 be Loop of [s, t] such that

           A11: x = ( Class (( EqRel ( [:S, T:], [s, t])),l1)) and

           A12: (f . x) = <*( Class (( EqRel (S,s)),( pr1 l1))), ( Class (( EqRel (T,t)),( pr2 l1)))*> by A9;

          consider l2 be Loop of [s, t] such that

           A13: x = ( Class (( EqRel ( [:S, T:], [s, t])),l2)) and

           A14: (g . x) = <*( Class (( EqRel (S,s)),( pr1 l2))), ( Class (( EqRel (T,t)),( pr2 l2)))*> by A10;

          

           A15: (l1,l2) are_homotopic by A11, A13, TOPALG_1: 46;

          then (( pr2 l1),( pr2 l2)) are_homotopic by Th20;

          then

           A16: ( Class (( EqRel (T,t)),( pr2 l1))) = ( Class (( EqRel (T,t)),( pr2 l2))) by TOPALG_1: 46;

          (( pr1 l1),( pr1 l2)) are_homotopic by A15, Th19;

          hence (f . x) = (g . x) by A12, A14, A16, TOPALG_1: 46;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPALG_4:27

    

     Th27: for x be Point of ( pi_1 ( [:S, T:], [s, t])), l be Loop of [s, t] st x = ( Class (( EqRel ( [:S, T:], [s, t])),l)) holds (( FGPrIso (s,t)) . x) = <*( Class (( EqRel (S,s)),( pr1 l))), ( Class (( EqRel (T,t)),( pr2 l)))*>

    proof

      let x be Point of ( pi_1 ( [:S, T:], [s, t])), l be Loop of [s, t];

      consider l1 be Loop of [s, t] such that

       A1: x = ( Class (( EqRel ( [:S, T:], [s, t])),l1)) and

       A2: (( FGPrIso (s,t)) . x) = <*( Class (( EqRel (S,s)),( pr1 l1))), ( Class (( EqRel (T,t)),( pr2 l1)))*> by Def2;

      assume x = ( Class (( EqRel ( [:S, T:], [s, t])),l));

      then

       A3: (l,l1) are_homotopic by A1, TOPALG_1: 46;

      then (( pr2 l),( pr2 l1)) are_homotopic by Th20;

      then

       A4: ( Class (( EqRel (T,t)),( pr2 l))) = ( Class (( EqRel (T,t)),( pr2 l1))) by TOPALG_1: 46;

      (( pr1 l),( pr1 l1)) are_homotopic by A3, Th19;

      hence thesis by A2, A4, TOPALG_1: 46;

    end;

    theorem :: TOPALG_4:28

    

     Th28: for l be Loop of [s, t] holds (( FGPrIso (s,t)) . ( Class (( EqRel ( [:S, T:], [s, t])),l))) = <*( Class (( EqRel (S,s)),( pr1 l))), ( Class (( EqRel (T,t)),( pr2 l)))*>

    proof

      let l be Loop of [s, t];

      ( Class (( EqRel ( [:S, T:], [s, t])),l)) is Point of ( pi_1 ( [:S, T:], [s, t])) by TOPALG_1: 47;

      hence thesis by Th27;

    end;

    registration

      let S,T be non empty TopSpace, s be Point of S, t be Point of T;

      cluster ( FGPrIso (s,t)) -> one-to-one onto;

      coherence

      proof

        set F = ( FGPrIso (s,t));

        set G = <*( pi_1 (S,s)), ( pi_1 (T,t))*>;

        set pS = ( pi_1 ( [:S, T:], [s, t]));

        set pT = ( product G);

        

         A1: the carrier of pT = ( product ( Carrier G)) by GROUP_7:def 2;

        thus F is one-to-one

        proof

          let a,b be object;

          assume a in ( dom F);

          then

          consider la be Loop of [s, t] such that

           A2: a = ( Class (( EqRel ( [:S, T:], [s, t])),la)) and

           A3: (F . a) = <*( Class (( EqRel (S,s)),( pr1 la))), ( Class (( EqRel (T,t)),( pr2 la)))*> by Def2;

          assume b in ( dom F);

          then

          consider lb be Loop of [s, t] such that

           A4: b = ( Class (( EqRel ( [:S, T:], [s, t])),lb)) and

           A5: (F . b) = <*( Class (( EqRel (S,s)),( pr1 lb))), ( Class (( EqRel (T,t)),( pr2 lb)))*> by Def2;

          assume

           A6: (F . a) = (F . b);

          then ( Class (( EqRel (T,t)),( pr2 la))) = ( Class (( EqRel (T,t)),( pr2 lb))) by A3, A5, FINSEQ_1: 77;

          then

           A7: (( pr2 la),( pr2 lb)) are_homotopic by TOPALG_1: 46;

          ( Class (( EqRel (S,s)),( pr1 la))) = ( Class (( EqRel (S,s)),( pr1 lb))) by A3, A5, A6, FINSEQ_1: 77;

          then (( pr1 la),( pr1 lb)) are_homotopic by TOPALG_1: 46;

          then (la,lb) are_homotopic by A7, Th22;

          hence thesis by A2, A4, TOPALG_1: 46;

        end;

        thus ( rng F) c= the carrier of pT;

        let y be object;

        assume y in the carrier of pT;

        then

        consider g be Function such that

         A8: y = g and

         A9: ( dom g) = ( dom ( Carrier G)) and

         A10: for z be object st z in ( dom ( Carrier G)) holds (g . z) in (( Carrier G) . z) by A1, CARD_3:def 5;

        

         A11: ( dom ( Carrier G)) = {1, 2} by PARTFUN1:def 2;

        then

        reconsider g as FinSequence by A9, FINSEQ_1: 2, FINSEQ_1:def 2;

        

         A12: ( len g) = 2 by A9, A11, FINSEQ_1: 2, FINSEQ_1:def 3;

        

         A13: (ex R2 be 1-sorted st R2 = (G . 2) & (( Carrier G) . 2) = the carrier of R2) & (G . 2) = ( pi_1 (T,t)) by Lm2, FINSEQ_1: 44, PRALG_1:def 15;

        (g . 2) in (( Carrier G) . 2) by A10, A11, Lm2;

        then

        consider l2 be Loop of t such that

         A14: (g . 2) = ( Class (( EqRel (T,t)),l2)) by A13, TOPALG_1: 47;

        

         A15: (ex R1 be 1-sorted st R1 = (G . 1) & (( Carrier G) . 1) = the carrier of R1) & (G . 1) = ( pi_1 (S,s)) by Lm1, FINSEQ_1: 44, PRALG_1:def 15;

        (g . 1) in (( Carrier G) . 1) by A10, A11, Lm1;

        then

        consider l1 be Loop of s such that

         A16: (g . 1) = ( Class (( EqRel (S,s)),l1)) by A15, TOPALG_1: 47;

        set x = ( Class (( EqRel ( [:S, T:], [s, t])), <:l1, l2:>));

        

         A17: ( dom l1) = I by FUNCT_2:def 1

        .= ( dom l2) by FUNCT_2:def 1;

        ( dom F) = the carrier of pS by FUNCT_2:def 1;

        then

         A18: x in ( dom F) by TOPALG_1: 47;

        (F . x) = <*( Class (( EqRel (S,s)),( pr1 <:l1, l2:>))), ( Class (( EqRel (T,t)),( pr2 <:l1, l2:>)))*> by Th28

        .= <*( Class (( EqRel (S,s)),l1)), ( Class (( EqRel (T,t)),( pr2 <:l1, l2:>)))*> by A17, Th7

        .= <*( Class (( EqRel (S,s)),l1)), ( Class (( EqRel (T,t)),l2))*> by A17, Th8

        .= y by A8, A12, A16, A14, FINSEQ_1: 44;

        hence thesis by A18, FUNCT_1:def 3;

      end;

    end

    registration

      let S,T be non empty TopSpace, s be Point of S, t be Point of T;

      cluster ( FGPrIso (s,t)) -> multiplicative;

      coherence

      proof

        set F = ( FGPrIso (s,t));

        let a,b be Element of ( pi_1 ( [:S, T:], [s, t]));

        consider la be Loop of [s, t] such that

         A1: a = ( Class (( EqRel ( [:S, T:], [s, t])),la)) and

         A2: (F . a) = <*( Class (( EqRel (S,s)),( pr1 la))), ( Class (( EqRel (T,t)),( pr2 la)))*> by Def2;

        consider lb be Loop of [s, t] such that

         A3: b = ( Class (( EqRel ( [:S, T:], [s, t])),lb)) and

         A4: (F . b) = <*( Class (( EqRel (S,s)),( pr1 lb))), ( Class (( EqRel (T,t)),( pr2 lb)))*> by Def2;

        reconsider B1 = ( Class (( EqRel (T,t)),( pr2 la))), B2 = ( Class (( EqRel (T,t)),( pr2 lb))) as Element of ( pi_1 (T,t)) by TOPALG_1: 47;

        reconsider A1 = ( Class (( EqRel (S,s)),( pr1 la))), A2 = ( Class (( EqRel (S,s)),( pr1 lb))) as Element of ( pi_1 (S,s)) by TOPALG_1: 47;

        consider lab be Loop of [s, t] such that

         A5: (a * b) = ( Class (( EqRel ( [:S, T:], [s, t])),lab)) and

         A6: (F . (a * b)) = <*( Class (( EqRel (S,s)),( pr1 lab))), ( Class (( EqRel (T,t)),( pr2 lab)))*> by Def2;

        (a * b) = ( Class (( EqRel ( [:S, T:], [s, t])),(la + lb))) by A1, A3, TOPALG_1: 61;

        then

         A7: (lab,(la + lb)) are_homotopic by A5, TOPALG_1: 46;

        then

         A8: (( pr1 lab),( pr1 (la + lb))) are_homotopic by Th19;

        

         A9: (( pr2 lab),( pr2 (la + lb))) are_homotopic by A7, Th20;

        

         A10: (B1 * B2) = ( Class (( EqRel (T,t)),(( pr2 la) + ( pr2 lb)))) by TOPALG_1: 61

        .= ( Class (( EqRel (T,t)),( pr2 (la + lb)))) by Th25

        .= ( Class (( EqRel (T,t)),( pr2 lab))) by A9, TOPALG_1: 46;

        (A1 * A2) = ( Class (( EqRel (S,s)),(( pr1 la) + ( pr1 lb)))) by TOPALG_1: 61

        .= ( Class (( EqRel (S,s)),( pr1 (la + lb)))) by Th23

        .= ( Class (( EqRel (S,s)),( pr1 lab))) by A8, TOPALG_1: 46;

        hence (F . (a * b)) = ((F . a) * (F . b)) by A2, A4, A6, A10, GROUP_7: 29;

      end;

    end

    theorem :: TOPALG_4:29

    ( FGPrIso (s,t)) is bijective;

    theorem :: TOPALG_4:30

    

     Th30: (( pi_1 ( [:S, T:], [s, t])),( product <*( pi_1 (S,s)), ( pi_1 (T,t))*>)) are_isomorphic

    proof

      take ( FGPrIso (s,t));

      thus thesis;

    end;

    theorem :: TOPALG_4:31

    for f be Homomorphism of ( pi_1 (S,s1)), ( pi_1 (S,s2)), g be Homomorphism of ( pi_1 (T,t1)), ( pi_1 (T,t2)) st f is bijective & g is bijective holds (( Gr2Iso (f,g)) * ( FGPrIso (s1,t1))) is bijective

    proof

      let f be Homomorphism of ( pi_1 (S,s1)), ( pi_1 (S,s2)), g be Homomorphism of ( pi_1 (T,t1)), ( pi_1 (T,t2));

      assume f is bijective & g is bijective;

      then

       A1: ( Gr2Iso (f,g)) is bijective by Th5;

      ( FGPrIso (s1,t1)) is bijective;

      hence thesis by A1, GROUP_6: 64;

    end;

    theorem :: TOPALG_4:32

    for S,T be non empty pathwise_connected TopSpace, s1,s2 be Point of S, t1,t2 be Point of T holds (( pi_1 ( [:S, T:], [s1, t1])),( product <*( pi_1 (S,s2)), ( pi_1 (T,t2))*>)) are_isomorphic

    proof

      let S,T be non empty pathwise_connected TopSpace, s1,s2 be Point of S, t1,t2 be Point of T;

      (( pi_1 (S,s1)),( pi_1 (S,s2))) are_isomorphic & (( pi_1 (T,t1)),( pi_1 (T,t2))) are_isomorphic by TOPALG_3: 33;

      then

       A1: (( product <*( pi_1 (S,s1)), ( pi_1 (T,t1))*>),( product <*( pi_1 (S,s2)), ( pi_1 (T,t2))*>)) are_isomorphic by Th6;

      (( pi_1 ( [:S, T:], [s1, t1])),( product <*( pi_1 (S,s1)), ( pi_1 (T,t1))*>)) are_isomorphic by Th30;

      hence thesis by A1, GROUP_6: 67;

    end;