topalg_3.miz



    begin

    set I = the carrier of I[01] ;

    

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

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

    theorem :: TOPALG_3:1

    for A,B,a,b be set, f be Function of A, B st a in A & b in B holds (f +* (a .--> b)) is Function of A, B

    proof

      let A,B,a,b be set, f be Function of A, B such that

       A1: a in A and

       A2: b in B;

      

       A3: {a} c= A by A1, ZFMISC_1: 31;

      set g = (a .--> b);

      set f1 = (f +* g);

      ( rng g) = {b} by FUNCOP_1: 8;

      then ( rng g) c= B by A2, ZFMISC_1: 31;

      then

       A4: ( rng f1) c= (( rng f) \/ ( rng g)) & (( rng f) \/ ( rng g)) c= (B \/ B) by FUNCT_4: 17, XBOOLE_1: 13;

      ( dom f1) = (( dom f) \/ ( dom g)) by FUNCT_4:def 1

      .= (A \/ ( dom g)) by A2, FUNCT_2:def 1

      .= (A \/ {a})

      .= A by A3, XBOOLE_1: 12;

      hence thesis by A4, FUNCT_2: 2, XBOOLE_1: 1;

    end;

    theorem :: TOPALG_3:2

    for f be Function, X,x be set st (f | X) is one-to-one & x in ( rng (f | X)) holds ((f * ((f | X) " )) . x) = x

    proof

      let f be Function, X,x be set;

      set g = (f | X);

      assume that

       A1: g is one-to-one and

       A2: x in ( rng g);

      consider a be object such that

       A3: a in ( dom g) and

       A4: (g . a) = x by A2, FUNCT_1:def 3;

      ( dom g) = (( dom f) /\ X) by RELAT_1: 61;

      then

       A5: a in X by A3, XBOOLE_0:def 4;

      ( dom (g " )) = ( rng g) by A1, FUNCT_1: 32;

      

      hence ((f * (g " )) . x) = (f . ((g " ) . x)) by A2, FUNCT_1: 13

      .= (f . a) by A1, A3, A4, FUNCT_1: 32

      .= x by A4, A5, FUNCT_1: 49;

    end;

    theorem :: TOPALG_3:3

    

     Th3: for X,a,b be set, f be Function of X, {a, b} holds X = ((f " {a}) \/ (f " {b}))

    proof

      let X,a,b be set;

      let f be Function of X, {a, b};

      

      thus X = (f " {a, b}) by FUNCT_2: 40

      .= (f " ( {a} \/ {b})) by ENUMSET1: 1

      .= ((f " {a}) \/ (f " {b})) by RELAT_1: 140;

    end;

    theorem :: TOPALG_3:4

    for S,T be non empty 1-sorted, s be Point of S, t be Point of T holds ((S --> t) . s) = t;

    theorem :: TOPALG_3:5

    for T be non empty TopStruct, t be Point of T, A be Subset of T st A = {t} holds ( Sspace t) = (T | A)

    proof

      let T be non empty TopStruct, t be Point of T, A be Subset of T such that

       A1: A = {t};

      the carrier of ( Sspace t) = {t} by TEX_2:def 2

      .= ( [#] (T | A)) by A1, PRE_TOPC:def 5

      .= the carrier of (T | A);

      hence thesis by TSEP_1: 5;

    end;

    theorem :: TOPALG_3:6

    

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

    theorem :: TOPALG_3:7

    

     Th7: for T be non empty TopSpace holds T is connected iff not ex f be Function of T, ( 1TopSp { 0 , 1}) st f is continuous onto

    proof

      set X = { 0 }, Y = {1};

      set J = ( 1TopSp { 0 , 1});

      let T be non empty TopSpace;

      

       A1: the carrier of J = { 0 , 1} by PCOMPS_1: 5;

      then

      reconsider X, Y as non empty open Subset of J by TDLAT_3: 15, ZFMISC_1: 7;

      thus T is connected implies not ex f be Function of T, J st f is continuous onto

      proof

        assume

         A2: T is connected;

        given f be Function of T, J such that

         A3: f is continuous and

         A4: f is onto;

        set A = (f " X), B = (f " Y);

        ( rng f) = the carrier of J by A4;

        then

         A5: A <> ( {} T) & B <> ( {} T) by RELAT_1: 139;

        

         A6: the carrier of T = (A \/ B) & A misses B by A1, Th3, FUNCT_1: 71, ZFMISC_1: 11;

        ( [#] J) <> {} ;

        then A is open & B is open by A3, TOPS_2: 43;

        hence contradiction by A2, A5, A6, CONNSP_1: 11;

      end;

      reconsider j0 = 0 , j1 = 1 as Element of J by A1, TARSKI:def 2;

      assume

       A7: not ex f be Function of T, J st f is continuous onto;

      deffunc G( object) = j1;

      deffunc F( object) = j0;

      assume not thesis;

      then

      consider A,B be Subset of T such that

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

       A9: A <> ( {} T) and

       A10: B <> ( {} T) and

       A11: A is open & B is open and

       A12: A misses B by CONNSP_1: 11;

      defpred C[ object] means $1 in A;

      

       A13: for x be object st x in the carrier of T holds ( C[x] implies F(x) in the carrier of J) & ( not C[x] implies G(x) in the carrier of J);

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

       A14: for x be object st x in the carrier of T holds ( C[x] implies (f . x) = F(x)) & ( not C[x] implies (f . x) = G(x)) from FUNCT_2:sch 5( A13);

      reconsider f as Function of T, J;

      

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

      

       A16: (f " Y) = B

      proof

        hereby

          let x be object;

          assume

           A17: x in (f " Y);

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

          then (f . x) = 1 by TARSKI:def 1;

          then not C[x] by A14;

          hence x in B by A8, A17, XBOOLE_0:def 3;

        end;

        let x be object;

        assume

         A18: x in B;

        then not x in A by A12, XBOOLE_0: 3;

        then (f . x) = 1 by A14, A18;

        then (f . x) in Y by TARSKI:def 1;

        hence thesis by A15, A18, FUNCT_1:def 7;

      end;

      

       A19: (f " X) = A

      proof

        hereby

          let x be object;

          assume

           A20: x in (f " X);

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

          then (f . x) = 0 by TARSKI:def 1;

          hence x in A by A14, A20;

        end;

        let x be object;

        assume

         A21: x in A;

        then (f . x) = 0 by A14;

        then (f . x) in X by TARSKI:def 1;

        hence thesis by A15, A21, FUNCT_1:def 7;

      end;

      

       A22: ( rng f) = the carrier of J

      proof

        thus ( rng f) c= the carrier of J;

        let y be object;

        assume

         A23: y in the carrier of J;

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

          suppose

           A24: y = 0 ;

          consider x be object such that

           A25: x in (f " X) by A9, A19, XBOOLE_0:def 1;

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

          then

           A26: (f . x) = 0 by TARSKI:def 1;

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

          hence thesis by A24, A26, FUNCT_1:def 3;

        end;

          suppose

           A27: y = 1;

          consider x be object such that

           A28: x in (f " Y) by A10, A16, XBOOLE_0:def 1;

          (f . x) in Y by A28, FUNCT_1:def 7;

          then

           A29: (f . x) = 1 by TARSKI:def 1;

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

          hence thesis by A27, A29, FUNCT_1:def 3;

        end;

      end;

      then (f " ( {} J)) = ( {} T) & (f " ( [#] J)) = ( [#] T) by A15, RELAT_1: 134;

      then ( [#] J) <> {} & for P be Subset of J st P is open holds (f " P) is open by A1, A11, A19, A16, ZFMISC_1: 36;

      then

       A30: f is continuous by TOPS_2: 43;

      f is onto by A22;

      hence thesis by A7, A30;

    end;

    registration

      cluster empty -> connected for TopStruct;

      coherence ;

    end

    theorem :: TOPALG_3:8

    for T be TopSpace st the TopStruct of T is connected holds T is connected

    proof

      let T be TopSpace;

      set G = the TopStruct of T;

      assume

       A1: G is connected;

      let A,B be Subset of T such that

       A2: ( [#] T) = (A \/ B) & (A,B) are_separated ;

      reconsider A1 = A, B1 = B as Subset of G;

      ( [#] G) = (A1 \/ B1) & (A1,B1) are_separated by A2, Th6;

      then A1 = ( {} G) or B1 = ( {} G) by A1;

      hence thesis;

    end;

    registration

      let T be connected TopSpace;

      cluster the TopStruct of T -> connected;

      coherence

      proof

        set G = the TopStruct of T;

        let A,B be Subset of G such that

         A1: ( [#] G) = (A \/ B) & (A,B) are_separated ;

        reconsider A1 = A, B1 = B as Subset of T;

        ( [#] T) = (A1 \/ B1) & (A1,B1) are_separated by A1, Th6;

        then A1 = ( {} T) or B1 = ( {} T) by CONNSP_1:def 2;

        hence thesis;

      end;

    end

    theorem :: TOPALG_3:9

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

    proof

      let S,T be non empty TopSpace;

      given h be Function of S, T such that

       A1: h is being_homeomorphism;

      assume

       A2: for a,b be Point of S holds (a,b) are_connected ;

      let a,b be Point of T;

      (((h " ) . a),((h " ) . b)) are_connected by A2;

      then

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

       A3: f is continuous and

       A4: (f . 0 ) = ((h " ) . a) and

       A5: (f . 1) = ((h " ) . b);

      take g = (h * f);

      h is continuous by A1;

      hence g is continuous by A3;

      

       A6: h is one-to-one & ( rng h) = ( [#] T) by A1;

      

      thus (g . 0 ) = (h . ((h " ) . a)) by A4, BORSUK_1:def 14, FUNCT_2: 15

      .= ((h * (h " )) . a) by FUNCT_2: 15

      .= (( id T) . a) by A6, TOPS_2: 52

      .= a;

      

      thus (g . 1) = (h . ((h " ) . b)) by A5, BORSUK_1:def 15, FUNCT_2: 15

      .= ((h * (h " )) . b) by FUNCT_2: 15

      .= (( id T) . b) by A6, TOPS_2: 52

      .= b;

    end;

    registration

      cluster trivial -> pathwise_connected for non empty TopSpace;

      coherence

      proof

        let T be non empty TopSpace;

        assume

         A1: T is trivial;

        let a,b be Point of T;

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

        thus f is continuous;

        a = b by A1;

        hence thesis by BORSUK_1:def 14, BORSUK_1:def 15;

      end;

    end

    theorem :: TOPALG_3:10

    for T be SubSpace of ( TOP-REAL 2) st the carrier of T is Simple_closed_curve holds T is pathwise_connected

    proof

      let T be SubSpace of ( TOP-REAL 2);

      assume

       A1: the carrier of T is Simple_closed_curve;

      then

      reconsider P = the carrier of T as Simple_closed_curve;

      let a,b be Point of T;

      a in P & b in P;

      then

      reconsider p1 = a, p2 = b as Point of ( TOP-REAL 2);

      per cases ;

        suppose p1 <> p2;

        then

        consider P1,P2 be non empty Subset of ( TOP-REAL 2) such that

         A2: P1 is_an_arc_of (p1,p2) and P2 is_an_arc_of (p1,p2) and

         A3: P = (P1 \/ P2) and (P1 /\ P2) = {p1, p2} by TOPREAL2: 5;

        the carrier of (( TOP-REAL 2) | P1) = P1 by PRE_TOPC: 8;

        then

         A4: the carrier of (( TOP-REAL 2) | P1) c= P by A3, XBOOLE_1: 7;

        then

         A5: (( TOP-REAL 2) | P1) is SubSpace of T by TSEP_1: 4;

        consider f1 be Function of I[01] , (( TOP-REAL 2) | P1) such that

         A6: f1 is being_homeomorphism and

         A7: (f1 . 0 ) = p1 & (f1 . 1) = p2 by A2, TOPREAL1:def 1;

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

        take f;

        f1 is continuous by A6;

        hence f is continuous by A5, PRE_TOPC: 26;

        thus thesis by A7;

      end;

        suppose

         A8: p1 = p2;

        reconsider T1 = T as non empty SubSpace of ( TOP-REAL 2) by A1;

        reconsider a1 = a as Point of T1;

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

        take f;

        thus f is continuous;

        

        thus (f . 0 ) = (f . j0)

        .= a;

        

        thus (f . 1) = (f . j1)

        .= b by A8;

      end;

    end;

    theorem :: TOPALG_3:11

    for T be TopSpace holds ex F be Subset-Family of T st F = {the carrier of T} & F is Cover of T & F is open

    proof

      let T be TopSpace;

      set F = {the carrier of T};

      F c= ( bool the carrier of T)

      proof

        let a be object;

        assume a in F;

        then a = the carrier of T by TARSKI:def 1;

        hence thesis by ZFMISC_1:def 1;

      end;

      then

      reconsider F as Subset-Family of T;

      take F;

      thus F = {the carrier of T};

      the carrier of T c= ( union F) by ZFMISC_1: 25;

      hence F is Cover of T by SETFAM_1:def 11;

      let P be Subset of T;

      ( [#] T) = the carrier of T;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let T be TopSpace;

      cluster non empty mutually-disjoint open closed for Subset-Family of T;

      existence

      proof

        set F = {( {} T)};

        F c= ( bool the carrier of T)

        proof

          let a be object;

          assume a in F;

          then a = ( {} T) by TARSKI:def 1;

          hence thesis;

        end;

        then

        reconsider F as Subset-Family of T;

        take F;

        thus F is non empty mutually-disjoint by TAXONOM2: 10;

        thus F is open by TARSKI:def 1;

        let P be Subset of T;

        thus thesis by TARSKI:def 1;

      end;

    end

    theorem :: TOPALG_3:12

    for T be TopSpace, D be mutually-disjoint open Subset-Family of T, A be Subset of T, X be set st A is connected & X in D & X meets A & D is Cover of A holds A c= X

    proof

      let T be TopSpace;

      let D be mutually-disjoint open Subset-Family of T;

      let A be Subset of T;

      let X be set such that

       A1: (T | A) is connected and

       A2: X in D and

       A3: X meets A;

      consider x be object such that

       A4: x in X & x in A by A3, XBOOLE_0: 3;

      assume D is Cover of A;

      then

       A5: A c= ( union D) by SETFAM_1:def 11;

      let a be object;

      assume

       A6: a in A;

      then

      consider Z be set such that

       A7: a in Z and

       A8: Z in D by A5, TARSKI:def 4;

      set D2 = { (K /\ A) where K be Subset of T : K in D & not a in K };

      D2 c= ( bool A)

      proof

        let d be object;

        reconsider dd = d as set by TARSKI: 1;

        assume d in D2;

        then ex K1 be Subset of T st d = (K1 /\ A) & K1 in D & not a in K1;

        then dd c= A by XBOOLE_1: 17;

        hence thesis;

      end;

      then

      reconsider D2 as Subset-Family of (T | A) by PRE_TOPC: 8;

      assume not a in X;

      then

       A9: (X /\ A) in D2 by A2;

      x in (X /\ A) by A4, XBOOLE_0:def 4;

      then

       A10: x in ( union D2) by A9, TARSKI:def 4;

      set D1 = { (K /\ A) where K be Subset of T : K in D & a in K };

      D1 c= ( bool A)

      proof

        let d be object;

        reconsider dd = d as set by TARSKI: 1;

        assume d in D1;

        then ex K1 be Subset of T st d = (K1 /\ A) & K1 in D & a in K1;

        then dd c= A by XBOOLE_1: 17;

        hence thesis;

      end;

      then

      reconsider D1 as Subset-Family of (T | A) by PRE_TOPC: 8;

      

       A11: A c= (( union D1) \/ ( union D2))

      proof

        let b be object;

        assume

         A12: b in A;

        then

        consider Z be set such that

         A13: b in Z and

         A14: Z in D by A5, TARSKI:def 4;

        reconsider Z as Subset of T by A14;

        

         A15: b in (Z /\ A) by A12, A13, XBOOLE_0:def 4;

        per cases ;

          suppose a in Z;

          then (Z /\ A) in D1 by A14;

          then b in ( union D1) by A15, TARSKI:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose not a in Z;

          then (Z /\ A) in D2 by A14;

          then b in ( union D2) by A15, TARSKI:def 4;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      

       A16: (Z /\ A) in D1 by A7, A8;

      

       A17: ( [#] (T | A)) = A by PRE_TOPC:def 5;

      D1 is open

      proof

        let P be Subset of (T | A);

        assume P in D1;

        then

        consider K1 be Subset of T such that

         A18: P = (K1 /\ A) and

         A19: K1 in D and a in K1;

        K1 is open by A19, TOPS_2:def 1;

        hence thesis by A17, A18, TOPS_2: 24;

      end;

      then

       A20: ( union D1) is open by TOPS_2: 19;

      D2 is open

      proof

        let P be Subset of (T | A);

        assume P in D2;

        then

        consider K1 be Subset of T such that

         A21: P = (K1 /\ A) and

         A22: K1 in D and not a in K1;

        K1 is open by A22, TOPS_2:def 1;

        hence thesis by A17, A21, TOPS_2: 24;

      end;

      then

       A23: ( union D2) is open by TOPS_2: 19;

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

      then

       A24: A = (( union D1) \/ ( union D2)) by A11;

      a in (Z /\ A) by A6, A7, XBOOLE_0:def 4;

      then ( union D1) <> ( {} (T | A)) by A16, TARSKI:def 4;

      then ( union D1) meets ( union D2) by A1, A17, A20, A23, A24, A10, CONNSP_1: 11;

      then

      consider y be object such that

       A25: y in ( union D1) and

       A26: y in ( union D2) by XBOOLE_0: 3;

      consider Y2 be set such that

       A27: y in Y2 and

       A28: Y2 in D2 by A26, TARSKI:def 4;

      consider K2 be Subset of T such that

       A29: Y2 = (K2 /\ A) and

       A30: K2 in D & not a in K2 by A28;

      

       A31: y in K2 by A27, A29, XBOOLE_0:def 4;

      consider Y1 be set such that

       A32: y in Y1 and

       A33: Y1 in D1 by A25, TARSKI:def 4;

      consider K1 be Subset of T such that

       A34: Y1 = (K1 /\ A) and

       A35: K1 in D & a in K1 by A33;

      y in K1 by A32, A34, XBOOLE_0:def 4;

      then K1 meets K2 by A31, XBOOLE_0: 3;

      hence thesis by A35, A30, TAXONOM2:def 5;

    end;

    begin

    theorem :: TOPALG_3:13

    

     Th13: for S,T be TopSpace holds the TopStruct of [:S, T:] = [: the TopStruct of S, the TopStruct of T:]

    proof

      let S,T be TopSpace;

      

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

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

      for C1 be Subset of [:S, T:], C2 be Subset of [: the TopStruct of S, the TopStruct of T:] st C1 = C2 holds C1 is open iff C2 is open

      proof

        let C1 be Subset of [:S, T:];

        let C2 be Subset of [: the TopStruct of S, the TopStruct of T:];

        assume

         A2: C1 = C2;

        hereby

          assume C1 is open;

          then

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

           A3: C1 = ( union A) and

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

          reconsider AA = A as Subset-Family of [: the TopStruct of S, the TopStruct of T:] by A1;

          for e be set st e in AA holds ex X1 be Subset of the TopStruct of S, Y1 be Subset of the TopStruct of T st e = [:X1, Y1:] & X1 is open & Y1 is open

          proof

            let e be set;

            assume e in AA;

            then

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

             A5: e = [:X1, Y1:] & X1 is open & Y1 is open by A4;

            reconsider Y2 = Y1 as Subset of the TopStruct of T;

            reconsider X2 = X1 as Subset of the TopStruct of S;

            take X2, Y2;

            thus thesis by A5, TOPS_3: 76;

          end;

          hence C2 is open by A2, A3, BORSUK_1: 5;

        end;

        assume C2 is open;

        then

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

         A6: C2 = ( union A) and

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

        reconsider AA = A as Subset-Family of [:S, T:] by A1;

        for e be set st e in AA holds ex X1 be Subset of S, Y1 be Subset of T st e = [:X1, Y1:] & X1 is open & Y1 is open

        proof

          let e be set;

          assume e in AA;

          then

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

           A8: e = [:X1, Y1:] & X1 is open & Y1 is open by A7;

          reconsider Y2 = Y1 as Subset of T;

          reconsider X2 = X1 as Subset of S;

          take X2, Y2;

          thus thesis by A8, TOPS_3: 76;

        end;

        hence thesis by A2, A6, BORSUK_1: 5;

      end;

      hence thesis by A1, TOPS_3: 72;

    end;

    theorem :: TOPALG_3:14

    

     Th14: for S,T be TopSpace, A be Subset of S, B be Subset of T holds ( Cl [:A, B:]) = [:( Cl A), ( Cl B):]

    proof

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

      hereby

        let x be object;

        assume

         A1: x in ( Cl [:A, B:]);

        then

        reconsider S1 = S, T1 = T as non empty TopSpace;

        reconsider p = x as Point of [:S1, T1:] by A1;

        consider K be Basis of p such that

         A2: for Q be Subset of [:S1, T1:] st Q in K holds [:A, B:] meets Q by A1, YELLOW13: 17;

        consider p1 be Point of S1, p2 be Point of T1 such that

         A3: p = [p1, p2] by BORSUK_1: 10;

        for G be Subset of T1 st G is open & p2 in G holds B meets G

        proof

          let G be Subset of T1;

          assume G is open & p2 in G;

          then [p1, p2] in [:( [#] S1), G:] & [:( [#] S1), G:] is open by BORSUK_1: 6, ZFMISC_1: 87;

          then

          consider V be Subset of [:S1, T1:] such that

           A4: V in K and

           A5: V c= [:( [#] S1), G:] by A3, YELLOW_8:def 1;

           [:A, B:] meets V by A2, A4;

          then

          consider a be object such that

           A6: a in [:A, B:] & a in V by XBOOLE_0: 3;

          a in ( [:A, B:] /\ [:( [#] S1), G:]) by A5, A6, XBOOLE_0:def 4;

          then a in [:(A /\ ( [#] S1)), (B /\ G):] by ZFMISC_1: 100;

          then ex a1,a2 be object st a1 in (A /\ ( [#] S1)) & a2 in (B /\ G) & a = [a1, a2] by ZFMISC_1:def 2;

          hence thesis;

        end;

        then

         A7: p2 in ( Cl B) by PRE_TOPC:def 7;

        for G be Subset of S1 st G is open & p1 in G holds A meets G

        proof

          let G be Subset of S1;

          assume G is open & p1 in G;

          then [p1, p2] in [:G, ( [#] T1):] & [:G, ( [#] T1):] is open by BORSUK_1: 6, ZFMISC_1: 87;

          then

          consider V be Subset of [:S1, T1:] such that

           A8: V in K and

           A9: V c= [:G, ( [#] T1):] by A3, YELLOW_8:def 1;

           [:A, B:] meets V by A2, A8;

          then

          consider a be object such that

           A10: a in [:A, B:] & a in V by XBOOLE_0: 3;

          a in ( [:A, B:] /\ [:G, ( [#] T1):]) by A9, A10, XBOOLE_0:def 4;

          then a in [:(A /\ G), (B /\ ( [#] T1)):] by ZFMISC_1: 100;

          then ex a1,a2 be object st a1 in (A /\ G) & a2 in (B /\ ( [#] T1)) & a = [a1, a2] by ZFMISC_1:def 2;

          hence thesis;

        end;

        then p1 in ( Cl A) by PRE_TOPC:def 7;

        hence x in [:( Cl A), ( Cl B):] by A3, A7, ZFMISC_1: 87;

      end;

      let x be object;

      assume x in [:( Cl A), ( Cl B):];

      then

      consider x1,x2 be object such that

       A11: x1 in ( Cl A) and

       A12: x2 in ( Cl B) and

       A13: x = [x1, x2] by ZFMISC_1:def 2;

      reconsider S1 = S, T1 = T as non empty TopSpace by A11, A12;

      reconsider x1 as Point of S1 by A11;

      consider K1 be Basis of x1 such that

       A14: for Q be Subset of S1 st Q in K1 holds A meets Q by A11, YELLOW13: 17;

      reconsider x2 as Point of T1 by A12;

      consider K2 be Basis of x2 such that

       A15: for Q be Subset of T1 st Q in K2 holds B meets Q by A12, YELLOW13: 17;

      for G be Subset of [:S1, T1:] st G is open & [x1, x2] in G holds [:A, B:] meets G

      proof

        let G be Subset of [:S1, T1:] such that

         A16: G is open and

         A17: [x1, x2] in G;

        consider F be Subset-Family of [:S1, T1:] such that

         A18: G = ( union F) and

         A19: for e be set st e in F holds ex X1 be Subset of S1, Y1 be Subset of T1 st e = [:X1, Y1:] & X1 is open & Y1 is open by A16, BORSUK_1: 5;

        consider Z be set such that

         A20: [x1, x2] in Z and

         A21: Z in F by A17, A18, TARSKI:def 4;

        consider X1 be Subset of S1, Y1 be Subset of T1 such that

         A22: Z = [:X1, Y1:] and

         A23: X1 is open and

         A24: Y1 is open by A19, A21;

        x2 in Y1 by A20, A22, ZFMISC_1: 87;

        then

        consider V2 be Subset of T1 such that

         A25: V2 in K2 and

         A26: V2 c= Y1 by A24, YELLOW_8:def 1;

        B meets V2 by A15, A25;

        then

        consider a2 be object such that

         A27: a2 in B and

         A28: a2 in V2 by XBOOLE_0: 3;

        x1 in X1 by A20, A22, ZFMISC_1: 87;

        then

        consider V1 be Subset of S1 such that

         A29: V1 in K1 and

         A30: V1 c= X1 by A23, YELLOW_8:def 1;

        A meets V1 by A14, A29;

        then

        consider a1 be object such that

         A31: a1 in A and

         A32: a1 in V1 by XBOOLE_0: 3;

         [a1, a2] in Z by A22, A30, A32, A26, A28, ZFMISC_1: 87;

        then

         A33: [a1, a2] in ( union F) by A21, TARSKI:def 4;

         [a1, a2] in [:A, B:] by A31, A27, ZFMISC_1: 87;

        hence thesis by A18, A33, XBOOLE_0: 3;

      end;

      hence thesis by A13, PRE_TOPC:def 7;

    end;

    theorem :: TOPALG_3:15

    

     Th15: for S,T be TopSpace, A be closed Subset of S, B be closed Subset of T holds [:A, B:] is closed

    proof

      let S,T be TopSpace;

      let A be closed Subset of S;

      let B be closed Subset of T;

      ( Cl A) = A & ( Cl [:A, B:]) = [:( Cl A), ( Cl B):] by Th14, PRE_TOPC: 22;

      hence thesis by PRE_TOPC: 22;

    end;

    registration

      let A,B be connected TopSpace;

      cluster [:A, B:] -> connected;

      coherence

      proof

        set S = the TopStruct of A, T = the TopStruct of B;

        

         A1: the TopStruct of [:A, B:] = [:S, T:] by Th13;

        per cases ;

          suppose

           A2: [:S, T:] is non empty;

          now

            set J = ( 1TopSp { 0 , 1});

            given f be Function of [:S, T:], J such that

             A3: f is continuous and

             A4: f is onto;

            

             A5: the carrier of J = { 0 , 1} by PCOMPS_1: 5;

            then

            reconsider j0 = 0 , j1 = 1 as Element of J by TARSKI:def 2;

            

             A6: ( rng f) = the carrier of J by A4;

            then

            consider xy0 be object such that

             A7: xy0 in ( dom f) and

             A8: (f . xy0) = j0 by FUNCT_1:def 3;

            consider xy1 be object such that

             A9: xy1 in ( dom f) and

             A10: (f . xy1) = j1 by A6, FUNCT_1:def 3;

            

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

            then

            consider x0,y0 be object such that

             A12: x0 in the carrier of S and

             A13: y0 in the carrier of T and

             A14: xy0 = [x0, y0] by A7, ZFMISC_1:def 2;

            

             A15: ( dom f) = the carrier of [:S, T:] by FUNCT_2:def 1;

            consider x1,y1 be object such that

             A16: x1 in the carrier of S and

             A17: y1 in the carrier of T and

             A18: xy1 = [x1, y1] by A11, A9, ZFMISC_1:def 2;

            reconsider y0, y1 as Point of T by A13, A17;

            reconsider x0, x1 as Point of S by A12, A16;

            reconsider S, T as non empty TopSpace by A2;

            reconsider Y1 = {y1} as non empty Subset of T by ZFMISC_1: 31;

            set h = (f | [:( [#] S), Y1:]);

            

             A19: ( dom h) = [:( [#] S), Y1:] by A15, RELAT_1: 62;

            the carrier of [:S, (T | Y1):] = [:the carrier of S, the carrier of (T | Y1):] by BORSUK_1:def 2;

            then

             A20: ( dom h) = the carrier of [:S, (T | Y1):] by A19, PRE_TOPC: 8;

            ( rng h) c= the carrier of J;

            then

            reconsider h as Function of [:S, (T | Y1):], J by A20, FUNCT_2: 2;

            (S, [:(T | Y1), S:]) are_homeomorphic by BORSUK_3: 13;

            then [:(T | Y1), S:] is connected by TOPREAL6: 19;

            then

             A21: [:S, (T | Y1):] is connected by TOPREAL6: 19, YELLOW12: 44;

             [:S, (T | Y1):] = [:(S | ( [#] S)), (T | Y1):] by TSEP_1: 3

            .= ( [:S, T:] | [:( [#] S), Y1:]) by BORSUK_3: 22;

            then

             A22: h is continuous by A3, TOPMETR: 7;

             A23:

            now

              assume

               A24: (f . [x0, y1]) <> 1;

              h is onto

              proof

                thus ( rng h) c= the carrier of J;

                let y be object;

                

                 A25: y1 in Y1 by TARSKI:def 1;

                assume

                 A26: y in the carrier of J;

                per cases by A5, A26, TARSKI:def 2;

                  suppose

                   A27: y = 1;

                  

                   A28: [x1, y1] in ( dom h) by A19, A25, ZFMISC_1: 87;

                  then (h . [x1, y1]) = y by A10, A18, A19, A27, FUNCT_1: 49;

                  hence thesis by A28, FUNCT_1:def 3;

                end;

                  suppose

                   A29: y = 0 ;

                   [x0, y1] in ( dom f) by A15, A11, A12, A17, ZFMISC_1: 87;

                  then

                   A30: (f . [x0, y1]) in ( rng f) by FUNCT_1:def 3;

                  

                   A31: [x0, y1] in ( dom h) by A19, A25, ZFMISC_1: 87;

                  

                  then (h . [x0, y1]) = (f . [x0, y1]) by A19, FUNCT_1: 49

                  .= y by A5, A24, A29, A30, TARSKI:def 2;

                  hence thesis by A31, FUNCT_1:def 3;

                end;

              end;

              hence contradiction by A21, A22, Th7;

            end;

            reconsider X0 = {x0} as non empty Subset of S by ZFMISC_1: 31;

            set g = (f | [:X0, ( [#] T):]);

            

             A32: ( dom g) = [:X0, ( [#] T):] by A15, RELAT_1: 62;

            the carrier of [:(S | X0), T:] = [:the carrier of (S | X0), the carrier of T:] by BORSUK_1:def 2;

            then

             A33: ( dom g) = the carrier of [:(S | X0), T:] by A32, PRE_TOPC: 8;

            ( rng g) c= the carrier of J;

            then

            reconsider g as Function of [:(S | X0), T:], J by A33, FUNCT_2: 2;

            (T, [:(S | X0), T:]) are_homeomorphic by BORSUK_3: 13;

            then

             A34: [:(S | X0), T:] is connected by TOPREAL6: 19;

             [:(S | X0), T:] = [:(S | X0), (T | ( [#] T)):] by TSEP_1: 3

            .= ( [:S, T:] | [:X0, ( [#] T):]) by BORSUK_3: 22;

            then

             A35: g is continuous by A3, TOPMETR: 7;

            now

              assume

               A36: (f . [x0, y1]) <> 0 ;

              g is onto

              proof

                thus ( rng g) c= the carrier of J;

                let y be object;

                

                 A37: x0 in X0 by TARSKI:def 1;

                assume

                 A38: y in the carrier of J;

                per cases by A5, A38, TARSKI:def 2;

                  suppose

                   A39: y = 0 ;

                  

                   A40: [x0, y0] in ( dom g) by A32, A37, ZFMISC_1: 87;

                  then (g . [x0, y0]) = y by A8, A14, A32, A39, FUNCT_1: 49;

                  hence thesis by A40, FUNCT_1:def 3;

                end;

                  suppose

                   A41: y = 1;

                   [x0, y1] in ( dom f) by A15, A11, A12, A17, ZFMISC_1: 87;

                  then

                   A42: (f . [x0, y1]) in ( rng f) by FUNCT_1:def 3;

                  

                   A43: [x0, y1] in ( dom g) by A32, A37, ZFMISC_1: 87;

                  

                  then (g . [x0, y1]) = (f . [x0, y1]) by A32, FUNCT_1: 49

                  .= y by A5, A36, A41, A42, TARSKI:def 2;

                  hence thesis by A43, FUNCT_1:def 3;

                end;

              end;

              hence contradiction by A34, A35, Th7;

            end;

            hence contradiction by A23;

          end;

          hence thesis by A1, Th7;

        end;

          suppose [:S, T:] is empty;

          hence thesis by Th13;

        end;

      end;

    end

    theorem :: TOPALG_3:16

    for S,T be TopSpace, A be Subset of S, B be Subset of T st A is connected & B is connected holds [:A, B:] is connected

    proof

      let S,T be TopSpace;

      let A be Subset of S;

      let B be Subset of T;

      assume (S | A) is connected & (T | B) is connected;

      then

      reconsider SA = (S | A), TB = (T | B) as connected TopSpace;

       [:SA, TB:] is connected;

      hence ( [:S, T:] | [:A, B:]) is connected by BORSUK_3: 22;

    end;

    theorem :: TOPALG_3:17

    for S,T be TopSpace, Y be non empty TopSpace, A be Subset of S, f be Function of [:S, T:], Y, g be Function of [:(S | A), T:], Y st g = (f | [:A, the carrier of T:]) & f is continuous holds g is continuous

    proof

      let S,T be TopSpace, Y be non empty TopSpace;

      let A be Subset of S;

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

      let g be Function of [:(S | A), T:], Y;

      assume

       A1: g = (f | [:A, the carrier of T:]) & f is continuous;

      set TT = the TopStruct of T;

      

       A2: [:(S | A), TT:] = [:(S | A), (TT | ( [#] TT)):] by TSEP_1: 3

      .= ( [:S, TT:] | [:A, ( [#] TT):]) by BORSUK_3: 22;

       the TopStruct of [:S, T:] = [: the TopStruct of S, the TopStruct of T:] by Th13;

      then

       A3: the TopStruct of [:S, TT:] = the TopStruct of [:S, T:] by Th13;

       the TopStruct of [:(S | A), TT:] = the TopStruct of [:(S | A), T:] by Th13;

      hence thesis by A1, A3, A2, TOPMETR: 7;

    end;

    theorem :: TOPALG_3:18

    for S,T be TopSpace, Y be non empty TopSpace, A be Subset of T, f be Function of [:S, T:], Y, g be Function of [:S, (T | A):], Y st g = (f | [:the carrier of S, A:]) & f is continuous holds g is continuous

    proof

      let S,T be TopSpace, Y be non empty TopSpace;

      let A be Subset of T;

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

      let g be Function of [:S, (T | A):], Y;

      assume

       A1: g = (f | [:the carrier of S, A:]) & f is continuous;

      set SS = the TopStruct of S;

      

       A2: [:SS, (T | A):] = [:(SS | ( [#] SS)), (T | A):] by TSEP_1: 3

      .= ( [:SS, T:] | [:( [#] SS), A:]) by BORSUK_3: 22;

       the TopStruct of [:S, T:] = [: the TopStruct of S, the TopStruct of T:] by Th13;

      then

       A3: the TopStruct of [:SS, T:] = the TopStruct of [:S, T:] by Th13;

       the TopStruct of [:SS, (T | A):] = the TopStruct of [:S, (T | A):] by Th13;

      hence thesis by A1, A3, A2, TOPMETR: 7;

    end;

    theorem :: TOPALG_3:19

    for S,T,T1,T2,Y be non empty TopSpace, f be Function of [:Y, T1:], S, g be Function of [:Y, T2:], S, F1,F2 be closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = ( [#] T1) & F2 = ( [#] T2) & (( [#] T1) \/ ( [#] T2)) = ( [#] T) & f is continuous & g is continuous & (for p be set st p in (( [#] [:Y, T1:]) /\ ( [#] [:Y, T2:])) holds (f . p) = (g . p)) holds ex h be Function of [:Y, T:], S st h = (f +* g) & h is continuous

    proof

      let S,T,T1,T2,Y be non empty TopSpace, f be Function of [:Y, T1:], S, g be Function of [:Y, T2:], S, F1,F2 be closed Subset of T;

      assume that

       A1: T1 is SubSpace of T and

       A2: T2 is SubSpace of T and

       A3: F1 = ( [#] T1) and

       A4: F2 = ( [#] T2) and

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

       A6: f is continuous and

       A7: g is continuous and

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

      

       A9: ( dom f) = the carrier of [:Y, T1:] by FUNCT_2:def 1;

      set h = (f +* g);

      

       A10: the carrier of [:Y, T2:] = [:the carrier of Y, the carrier of T2:] by BORSUK_1:def 2;

      

       A11: [:Y, T2:] is SubSpace of [:Y, T:] by A2, BORSUK_3: 15;

      

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

      

       A13: ( dom g) = the carrier of [:Y, T2:] by FUNCT_2:def 1;

      

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

      

       A15: the carrier of [:Y, T1:] = [:the carrier of Y, the carrier of T1:] by BORSUK_1:def 2;

      then

       A16: ( dom h) = [:the carrier of Y, the carrier of T:] by A5, A10, A9, A13, A14, ZFMISC_1: 97;

      

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

      then

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

      take h;

      thus h = (f +* g);

      

       A18: [:Y, T1:] is SubSpace of [:Y, T:] by A1, BORSUK_3: 15;

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

      proof

        reconsider M = [:( [#] Y), F1:] as Subset of [:Y, T:];

        let P be Subset of S;

         A19:

        now

          let x be object;

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

          proof

            assume

             A20: x in ((h " P) /\ ( [#] [:Y, T2:]));

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

            then

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

            (g . x) = (h . x) by A13, A20, FUNCT_4: 13;

            hence thesis by A13, A20, A21, FUNCT_1:def 7;

          end;

          assume

           A22: x in (g " P);

          then

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

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

          then

           A24: (h . x) in P by A23, FUNCT_4: 13;

          x in ( dom h) by A14, A23, XBOOLE_0:def 3;

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

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

        end;

        

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

        proof

          let x be set such that

           A26: x in ( [#] [:Y, T1:]);

          now

            per cases ;

              suppose

               A27: x in ( [#] [:Y, T2:]);

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

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

              hence thesis by A13, A27, FUNCT_4: 13;

            end;

              suppose not x in ( [#] [:Y, T2:]);

              hence thesis by A13, FUNCT_4: 11;

            end;

          end;

          hence thesis;

        end;

        now

          let x be object;

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

          proof

            assume

             A28: x in ((h " P) /\ ( [#] [:Y, T1:]));

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

            then

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

            x in ( [#] [:Y, T1:]) by A28;

            then

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

            (f . x) = (h . x) by A25, A28;

            hence thesis by A29, A30, FUNCT_1:def 7;

          end;

          assume

           A31: x in (f " P);

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

          then

           A32: x in ( dom h) by A14, XBOOLE_0:def 3;

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

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

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

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

        end;

        then

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

        the carrier of T2 is Subset of T by A2, TSEP_1: 1;

        then ( [#] [:Y, T2:]) c= ( [#] [:Y, T:]) by A17, A10, ZFMISC_1: 95;

        then

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

        the carrier of T1 is Subset of T by A1, TSEP_1: 1;

        then ( [#] [:Y, T1:]) c= ( [#] [:Y, T:]) by A17, A15, ZFMISC_1: 95;

        then

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

        assume

         A34: P is closed;

        then (f " P) is closed by A6, PRE_TOPC:def 6;

        then

         A35: ex F01 be Subset of [:Y, T:] st F01 is closed & (f " P) = (F01 /\ ( [#] [:Y, T1:])) by A18, PRE_TOPC: 13;

        (h " P) = ((h " P) /\ (( [#] [:Y, T1:]) \/ ( [#] [:Y, T2:]))) by A17, A9, A13, A14, A16, XBOOLE_1: 28

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

        then

         A36: (h " P) = ((f " P) \/ (g " P)) by A33, A19, TARSKI: 2;

        M is closed & ( [#] [:Y, T1:]) = [:( [#] Y), F1:] by A3, Th15, BORSUK_3: 1;

        then

         A37: P1 is closed by A35;

        (g " P) is closed by A7, A34, PRE_TOPC:def 6;

        then

         A38: ex F02 be Subset of [:Y, T:] st F02 is closed & (g " P) = (F02 /\ ( [#] [:Y, T2:])) by A11, PRE_TOPC: 13;

        reconsider M = [:( [#] Y), F2:] as Subset of [:Y, T:];

        M is closed & ( [#] [:Y, T2:]) = [:( [#] Y), F2:] by A4, Th15, BORSUK_3: 1;

        then P2 is closed by A38;

        hence thesis by A36, A37;

      end;

      hence thesis by PRE_TOPC:def 6;

    end;

    theorem :: TOPALG_3:20

    for S,T,T1,T2,Y be non empty TopSpace, f be Function of [:T1, Y:], S, g be Function of [:T2, Y:], S, F1,F2 be closed Subset of T st T1 is SubSpace of T & T2 is SubSpace of T & F1 = ( [#] T1) & F2 = ( [#] T2) & (( [#] T1) \/ ( [#] T2)) = ( [#] T) & f is continuous & g is continuous & (for p be set st p in (( [#] [:T1, Y:]) /\ ( [#] [:T2, Y:])) holds (f . p) = (g . p)) holds ex h be Function of [:T, Y:], S st h = (f +* g) & h is continuous

    proof

      let S,T,T1,T2,Y be non empty TopSpace, f be Function of [:T1, Y:], S, g be Function of [:T2, Y:], S, F1,F2 be closed Subset of T;

      assume that

       A1: T1 is SubSpace of T and

       A2: T2 is SubSpace of T and

       A3: F1 = ( [#] T1) and

       A4: F2 = ( [#] T2) and

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

       A6: f is continuous and

       A7: g is continuous and

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

      

       A9: ( dom f) = the carrier of [:T1, Y:] by FUNCT_2:def 1;

      

       A10: Y is SubSpace of Y by TSEP_1: 2;

      then

       A11: [:T2, Y:] is SubSpace of [:T, Y:] by A2, BORSUK_3: 21;

      set h = (f +* g);

      

       A12: the carrier of [:T2, Y:] = [:the carrier of T2, the carrier of Y:] by BORSUK_1:def 2;

      

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

      

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

      

       A15: ( dom g) = the carrier of [:T2, Y:] by FUNCT_2:def 1;

      

       A16: the carrier of [:T1, Y:] = [:the carrier of T1, the carrier of Y:] by BORSUK_1:def 2;

      then

       A17: ( dom h) = [:the carrier of T, the carrier of Y:] by A5, A12, A9, A15, A13, ZFMISC_1: 97;

      

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

      then

      reconsider h as Function of [:T, Y:], S by A17, A14, FUNCT_2: 2, XBOOLE_1: 1;

      take h;

      thus h = (f +* g);

      

       A19: [:T1, Y:] is SubSpace of [:T, Y:] by A1, A10, BORSUK_3: 21;

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

      proof

        reconsider M = [:F1, ( [#] Y):] as Subset of [:T, Y:];

        let P be Subset of S;

         A20:

        now

          let x be object;

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

          proof

            assume

             A21: x in ((h " P) /\ ( [#] [:T2, Y:]));

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

            then

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

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

            hence thesis by A15, A21, A22, FUNCT_1:def 7;

          end;

          assume

           A23: x in (g " P);

          then

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

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

          then

           A25: (h . x) in P by A24, FUNCT_4: 13;

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

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

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

        end;

        

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

        proof

          let x be set such that

           A27: x in ( [#] [:T1, Y:]);

          now

            per cases ;

              suppose

               A28: x in ( [#] [:T2, Y:]);

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

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

              hence thesis by A15, A28, FUNCT_4: 13;

            end;

              suppose not x in ( [#] [:T2, Y:]);

              hence thesis by A15, FUNCT_4: 11;

            end;

          end;

          hence thesis;

        end;

        now

          let x be object;

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

          proof

            assume

             A29: x in ((h " P) /\ ( [#] [:T1, Y:]));

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

            then

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

            x in ( [#] [:T1, Y:]) by A29;

            then

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

            (f . x) = (h . x) by A26, A29;

            hence thesis by A30, A31, FUNCT_1:def 7;

          end;

          assume

           A32: x in (f " P);

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

          then

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

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

          then (h . x) in P by A26, A32;

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

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

        end;

        then

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

        the carrier of T2 is Subset of T by A2, TSEP_1: 1;

        then ( [#] [:T2, Y:]) c= ( [#] [:T, Y:]) by A18, A12, ZFMISC_1: 95;

        then

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

        the carrier of T1 is Subset of T by A1, TSEP_1: 1;

        then ( [#] [:T1, Y:]) c= ( [#] [:T, Y:]) by A18, A16, ZFMISC_1: 95;

        then

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

        assume

         A35: P is closed;

        then (f " P) is closed by A6, PRE_TOPC:def 6;

        then

         A36: ex F01 be Subset of [:T, Y:] st F01 is closed & (f " P) = (F01 /\ ( [#] [:T1, Y:])) by A19, PRE_TOPC: 13;

        (h " P) = ((h " P) /\ (( [#] [:T1, Y:]) \/ ( [#] [:T2, Y:]))) by A18, A9, A15, A13, A17, XBOOLE_1: 28

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

        then

         A37: (h " P) = ((f " P) \/ (g " P)) by A34, A20, TARSKI: 2;

        M is closed & ( [#] [:T1, Y:]) = [:F1, ( [#] Y):] by A3, Th15, BORSUK_3: 1;

        then

         A38: P1 is closed by A36;

        (g " P) is closed by A7, A35, PRE_TOPC:def 6;

        then

         A39: ex F02 be Subset of [:T, Y:] st F02 is closed & (g " P) = (F02 /\ ( [#] [:T2, Y:])) by A11, PRE_TOPC: 13;

        reconsider M = [:F2, ( [#] Y):] as Subset of [:T, Y:];

        M is closed & ( [#] [:T2, Y:]) = [:F2, ( [#] Y):] by A4, Th15, BORSUK_3: 1;

        then P2 is closed by A39;

        hence thesis by A37, A38;

      end;

      hence thesis by PRE_TOPC:def 6;

    end;

    begin

    registration

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

      cluster -> continuous for Loop of t;

      coherence

      proof

        (t,t) are_connected ;

        hence thesis by BORSUK_2:def 2;

      end;

    end

    theorem :: TOPALG_3:21

    for T be non empty TopSpace, t be Point of T, x be Point of I[01] , P be constant Loop of t holds (P . x) = t

    proof

      let T be non empty TopSpace, t be Point of T, x be Point of I[01] , P be constant Loop of t;

      P = ( I[01] --> t) by BORSUK_2: 5;

      hence thesis;

    end;

    theorem :: TOPALG_3:22

    

     Th22: for T be non empty TopSpace, t be Point of T, P be Loop of t holds (P . 0 ) = t & (P . 1) = t

    proof

      let T be non empty TopSpace, t be Point of T, P be Loop of t;

      (t,t) are_connected ;

      hence thesis by BORSUK_2:def 2;

    end;

    theorem :: TOPALG_3:23

    

     Th23: for S,T be non empty TopSpace, f be continuous Function of S, T, a,b be Point of S st (a,b) are_connected holds ((f . a),(f . b)) are_connected

    proof

      let S,T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a,b be Point of S;

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

       A1: g is continuous and

       A2: (g . 0 ) = a and

       A3: (g . 1) = b;

      take h = (f * g);

      thus h is continuous by A1;

      

      thus (h . 0 ) = (f . (g . j0)) by FUNCT_2: 15

      .= (f . a) by A2;

      

      thus (h . 1) = (f . (g . j1)) by FUNCT_2: 15

      .= (f . b) by A3;

    end;

    theorem :: TOPALG_3:24

    for S,T be non empty TopSpace, f be continuous Function of S, T, a,b be Point of S, P be Path of a, b st (a,b) are_connected holds (f * P) is Path of (f . a), (f . b)

    proof

      let S,T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a,b be Point of S;

      let P be Path of a, b;

      assume

       A1: (a,b) are_connected ;

      

       A2: ((f * P) . 1) = (f . (P . j1)) by FUNCT_2: 15

      .= (f . b) by A1, BORSUK_2:def 2;

      

       A3: ((f * P) . 0 ) = (f . (P . j0)) by FUNCT_2: 15

      .= (f . a) by A1, BORSUK_2:def 2;

      P is continuous & ((f . a),(f . b)) are_connected by A1, Th23, BORSUK_2:def 2;

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

    end;

    theorem :: TOPALG_3:25

    

     Th25: for S be non empty pathwise_connected TopSpace, T be non empty TopSpace, f be continuous Function of S, T, a,b be Point of S, P be Path of a, b holds (f * P) is Path of (f . a), (f . b)

    proof

      let S be non empty pathwise_connected TopSpace;

      let T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a,b be Point of S;

      let P be Path of a, b;

      

       A1: (a,b) are_connected by BORSUK_2:def 3;

      

       A2: ((f * P) . 1) = (f . (P . j1)) by FUNCT_2: 15

      .= (f . b) by A1, BORSUK_2:def 2;

      

       A3: ((f * P) . 0 ) = (f . (P . j0)) by FUNCT_2: 15

      .= (f . a) by A1, BORSUK_2:def 2;

      ((f . a),(f . b)) are_connected by A1, Th23;

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

    end;

    definition

      let S be non empty pathwise_connected TopSpace, T be non empty TopSpace, a,b be Point of S, P be Path of a, b, f be continuous Function of S, T;

      :: original: *

      redefine

      func f * P -> Path of (f . a), (f . b) ;

      coherence by Th25;

    end

    theorem :: TOPALG_3:26

    

     Th26: for S,T be non empty TopSpace, f be continuous Function of S, T, a be Point of S, P be Loop of a holds (f * P) is Loop of (f . a)

    proof

      let S,T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a be Point of S;

      let P be Loop of a;

      

       A1: ((f . a),(f . a)) are_connected ;

      

       A2: ((f * P) . 1) = (f . (P . j1)) by FUNCT_2: 15

      .= (f . a) by Th22;

      ((f * P) . 0 ) = (f . (P . j0)) by FUNCT_2: 15

      .= (f . a) by Th22;

      hence thesis by A2, A1, BORSUK_2:def 2;

    end;

    definition

      let S,T be non empty TopSpace, a be Point of S, P be Loop of a, f be continuous Function of S, T;

      :: original: *

      redefine

      func f * P -> Loop of (f . a) ;

      coherence by Th26;

    end

    theorem :: TOPALG_3:27

    

     Th27: for S,T be non empty TopSpace, f be continuous Function of S, T, a,b be Point of S, P,Q be Path of a, b, P1,Q1 be Path of (f . a), (f . b) st (P,Q) are_homotopic & P1 = (f * P) & Q1 = (f * Q) holds (P1,Q1) are_homotopic

    proof

      let S,T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a,b be Point of S;

      let P,Q be Path of a, b;

      let P1,Q1 be Path of (f . a), (f . b);

      assume that

       A1: (P,Q) are_homotopic and

       A2: P1 = (f * P) and

       A3: Q1 = (f * Q);

      set F = the Homotopy of P, Q;

      take G = (f * F);

      F is continuous by A1, BORSUK_6:def 11;

      hence G is continuous;

      let s be Point of I[01] ;

      

      thus (G . (s, 0 )) = (f . (F . (s,j0))) by Lm1, BINOP_1: 18

      .= (f . (P . s)) by A1, BORSUK_6:def 11

      .= (P1 . s) by A2, FUNCT_2: 15;

      

      thus (G . (s,1)) = (f . (F . (s,j1))) by Lm1, BINOP_1: 18

      .= (f . (Q . s)) by A1, BORSUK_6:def 11

      .= (Q1 . s) by A3, FUNCT_2: 15;

      

      thus (G . ( 0 ,s)) = (f . (F . (j0,s))) by Lm1, BINOP_1: 18

      .= (f . a) by A1, BORSUK_6:def 11;

      

      thus (G . (1,s)) = (f . (F . (j1,s))) by Lm1, BINOP_1: 18

      .= (f . b) by A1, BORSUK_6:def 11;

    end;

    theorem :: TOPALG_3:28

    for S,T be non empty TopSpace, f be continuous Function of S, T, a,b be Point of S, P,Q be Path of a, b, P1,Q1 be Path of (f . a), (f . b), F be Homotopy of P, Q st (P,Q) are_homotopic & P1 = (f * P) & Q1 = (f * Q) holds (f * F) is Homotopy of P1, Q1

    proof

      let S,T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a,b be Point of S;

      let P,Q be Path of a, b;

      let P1,Q1 be Path of (f . a), (f . b);

      let F be Homotopy of P, Q;

      assume that

       A1: (P,Q) are_homotopic and

       A2: P1 = (f * P) and

       A3: Q1 = (f * Q);

      thus (P1,Q1) are_homotopic by A1, A2, A3, Th27;

      set G = (f * F);

      F is continuous by A1, BORSUK_6:def 11;

      hence G is continuous;

      let s be Point of I[01] ;

      

      thus (G . (s, 0 )) = (f . (F . (s,j0))) by Lm1, BINOP_1: 18

      .= (f . (P . s)) by A1, BORSUK_6:def 11

      .= (P1 . s) by A2, FUNCT_2: 15;

      

      thus (G . (s,1)) = (f . (F . (s,j1))) by Lm1, BINOP_1: 18

      .= (f . (Q . s)) by A1, BORSUK_6:def 11

      .= (Q1 . s) by A3, FUNCT_2: 15;

      

      thus (G . ( 0 ,s)) = (f . (F . (j0,s))) by Lm1, BINOP_1: 18

      .= (f . a) by A1, BORSUK_6:def 11;

      

      thus (G . (1,s)) = (f . (F . (j1,s))) by Lm1, BINOP_1: 18

      .= (f . b) by A1, BORSUK_6:def 11;

    end;

    theorem :: TOPALG_3:29

    

     Th29: for S,T be non empty TopSpace, f be continuous Function of S, T, a,b,c be Point of S, P be Path of a, b, Q be Path of b, c, P1 be Path of (f . a), (f . b), Q1 be Path of (f . b), (f . c) st (a,b) are_connected & (b,c) are_connected & P1 = (f * P) & Q1 = (f * Q) holds (P1 + Q1) = (f * (P + Q))

    proof

      let S,T be non empty TopSpace;

      let f be continuous Function of S, T;

      let a,b,c be Point of S;

      let P be Path of a, b;

      let Q be Path of b, c;

      let P1 be Path of (f . a), (f . b);

      let Q1 be Path of (f . b), (f . c);

      assume that

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

       A2: P1 = (f * P) and

       A3: Q1 = (f * Q);

      for x be Point of I[01] holds ((P1 + Q1) . x) = ((f * (P + Q)) . x)

      proof

        let x be Point of I[01] ;

        

         A4: ((f . a),(f . b)) are_connected & ((f . b),(f . c)) are_connected by A1, Th23;

        per cases ;

          suppose

           A5: x <= (1 / 2);

          then

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

          

          thus ((P1 + Q1) . x) = (P1 . (2 * x)) by A4, A5, BORSUK_2:def 5

          .= (f . (P . (2 * x))) by A2, A6, FUNCT_2: 15

          .= (f . ((P + Q) . x)) by A1, A5, BORSUK_2:def 5

          .= ((f * (P + Q)) . x) by FUNCT_2: 15;

        end;

          suppose

           A7: x >= (1 / 2);

          then

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

          

          thus ((P1 + Q1) . x) = (Q1 . ((2 * x) - 1)) by A4, A7, BORSUK_2:def 5

          .= (f . (Q . ((2 * x) - 1))) by A3, A8, FUNCT_2: 15

          .= (f . ((P + Q) . x)) by A1, A7, BORSUK_2:def 5

          .= ((f * (P + Q)) . x) by FUNCT_2: 15;

        end;

      end;

      hence thesis;

    end;

    definition

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

      set pT = ( pi_1 (T,(f . s)));

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

      :: TOPALG_3:def1

      func FundGrIso (f,s) -> Function of ( pi_1 (S,s)), ( pi_1 (T,(f . s))) means

      : Def1: for x be Element of ( pi_1 (S,s)) holds ex ls be Loop of s st x = ( Class (( EqRel (S,s)),ls)) & (it . x) = ( Class (( EqRel (T,(f . s))),(f * ls)));

      existence

      proof

        defpred P[ set, set] means ex ls be Loop of s st $1 = ( Class (( EqRel (S,s)),ls)) & $2 = ( Class (( EqRel (T,(f . s))),(f * ls)));

        

         A2: 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 ls be Loop of s such that

           A3: x = ( Class (( EqRel (S,s)),ls)) by TOPALG_1: 47;

          reconsider lt = (f * ls) as Loop of (f . s) by A1, Th26;

          reconsider y = ( Class (( EqRel (T,(f . s))),lt)) as Element of pT by TOPALG_1: 47;

          take y, ls;

          thus thesis by A3;

        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( A2);

        hence thesis;

      end;

      uniqueness

      proof

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

         A4: for x be Element of pS holds ex ls be Loop of s st x = ( Class (( EqRel (S,s)),ls)) & (g . x) = ( Class (( EqRel (T,(f . s))),(f * ls))) and

         A5: for x be Element of pS holds ex ls be Loop of s st x = ( Class (( EqRel (S,s)),ls)) & (h . x) = ( Class (( EqRel (T,(f . s))),(f * ls)));

        now

          let x be Element of pS;

          consider lsg be Loop of s such that

           A6: x = ( Class (( EqRel (S,s)),lsg)) and

           A7: (g . x) = ( Class (( EqRel (T,(f . s))),(f * lsg))) by A4;

          consider lsh be Loop of s such that

           A8: x = ( Class (( EqRel (S,s)),lsh)) and

           A9: (h . x) = ( Class (( EqRel (T,(f . s))),(f * lsh))) by A5;

          reconsider ltg = (f * lsg), lth = (f * lsh) as Loop of (f . s) by A1, Th26;

          (lsg,lsh) are_homotopic by A6, A8, TOPALG_1: 46;

          then (ltg,lth) are_homotopic by A1, Th27;

          hence (g . x) = (h . x) by A7, A9, TOPALG_1: 46;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPALG_3:30

    for S,T be non empty TopSpace, s be Point of S, f be continuous Function of S, T, ls be Loop of s holds (( FundGrIso (f,s)) . ( Class (( EqRel (S,s)),ls))) = ( Class (( EqRel (T,(f . s))),(f * ls)))

    proof

      let S,T be non empty TopSpace;

      let s be Point of S;

      let f be continuous Function of S, T;

      let ls be Loop of s;

      reconsider x = ( Class (( EqRel (S,s)),ls)) as Element of ( pi_1 (S,s)) by TOPALG_1: 47;

      consider ls1 be Loop of s such that

       A1: x = ( Class (( EqRel (S,s)),ls1)) and

       A2: (( FundGrIso (f,s)) . x) = ( Class (( EqRel (T,(f . s))),(f * ls1))) by Def1;

      (ls,ls1) are_homotopic by A1, TOPALG_1: 46;

      then ((f * ls),(f * ls1)) are_homotopic by Th27;

      hence thesis by A2, TOPALG_1: 46;

    end;

    registration

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

      cluster ( FundGrIso (f,s)) -> multiplicative;

      coherence

      proof

        set h = ( FundGrIso (f,s));

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

        let a,b be Element of pS;

        consider lsa be Loop of s such that

         A1: a = ( Class (( EqRel (S,s)),lsa)) and

         A2: (h . a) = ( Class (( EqRel (T,(f . s))),(f * lsa))) by Def1;

        consider lsb be Loop of s such that

         A3: b = ( Class (( EqRel (S,s)),lsb)) and

         A4: (h . b) = ( Class (( EqRel (T,(f . s))),(f * lsb))) by Def1;

        

         A5: ((f * lsa) + (f * lsb)) = (f * (lsa + lsb)) by Th29;

        consider lsab be Loop of s such that

         A6: (a * b) = ( Class (( EqRel (S,s)),lsab)) and

         A7: (h . (a * b)) = ( Class (( EqRel (T,(f . s))),(f * lsab))) by Def1;

        (a * b) = ( Class (( EqRel (S,s)),(lsa + lsb))) by A1, A3, TOPALG_1: 61;

        then (lsab,(lsa + lsb)) are_homotopic by A6, TOPALG_1: 46;

        then ((f * lsab),((f * lsa) + (f * lsb))) are_homotopic by A5, Th27;

        

        hence (h . (a * b)) = ( Class (( EqRel (T,(f . s))),((f * lsa) + (f * lsb)))) by A7, TOPALG_1: 46

        .= ((h . a) * (h . b)) by A2, A4, TOPALG_1: 61;

      end;

    end

    theorem :: TOPALG_3:31

    

     Th31: for S,T be non empty TopSpace, s be Point of S, f be continuous Function of S, T st f is being_homeomorphism holds ( FundGrIso (f,s)) is bijective

    proof

      let S,T be non empty TopSpace;

      let s be Point of S;

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

      let f be continuous Function of S, T such that

       A1: f is being_homeomorphism;

      

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

      then

       A3: ((f qua Function " ) . (f . s)) = s by FUNCT_2: 26;

      set h = ( FundGrIso (f,s));

      set pT = ( pi_1 (T,(f . s)));

      

       A4: (f " ) is continuous by A1;

      

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

      then f is onto;

      then

       A6: (f qua Function " ) = (f " ) by A2, TOPS_2:def 4;

      

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

      

       A8: ( rng h) = the carrier of pT

      proof

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

        let y be object;

        assume y in the carrier of pT;

        then

        consider lt be Loop of (f . s) such that

         A9: y = ( Class (( EqRel (T,(f . s))),lt)) by TOPALG_1: 47;

        reconsider ls = ((f " ) * lt) as Loop of s by A4, A3, A6, Th26;

        set x = ( Class (( EqRel (S,s)),ls));

        

         A10: x in the carrier of pS by TOPALG_1: 47;

        then

        consider ls1 be Loop of s such that

         A11: x = ( Class (( EqRel (S,s)),ls1)) and

         A12: (h . x) = ( Class (( EqRel (T,(f . s))),(f * ls1))) by Def1;

        

         A13: (f * ls) = ((f * (f " )) * lt) by RELAT_1: 36

        .= (( id ( rng f)) * lt) by A5, A2, TOPS_2: 52

        .= lt by A5, FUNCT_2: 17;

        (ls,ls1) are_homotopic by A11, TOPALG_1: 46;

        then (lt,(f * ls1)) are_homotopic by A13, Th27;

        then (h . x) = y by A9, A12, TOPALG_1: 46;

        hence thesis by A7, A10, FUNCT_1:def 3;

      end;

      h is one-to-one

      proof

        let x1,x2 be object;

        assume x1 in ( dom h);

        then

        consider ls1 be Loop of s such that

         A14: x1 = ( Class (( EqRel (S,s)),ls1)) and

         A15: (h . x1) = ( Class (( EqRel (T,(f . s))),(f * ls1))) by Def1;

        assume x2 in ( dom h);

        then

        consider ls2 be Loop of s such that

         A16: x2 = ( Class (( EqRel (S,s)),ls2)) and

         A17: (h . x2) = ( Class (( EqRel (T,(f . s))),(f * ls2))) by Def1;

        reconsider a1 = ((f " ) * (f * ls1)), a2 = ((f " ) * (f * ls2)) as Loop of s by A4, A3, A6, Th26;

        assume (h . x1) = (h . x2);

        then ((f * ls1),(f * ls2)) are_homotopic by A15, A17, TOPALG_1: 46;

        then

         A18: (a1,a2) are_homotopic by A4, A3, A6, Th27;

        

         A19: ((f " ) * f) = ( id ( dom f)) by A5, A2, TOPS_2: 52;

        

         A20: ((f " ) * (f * ls1)) = (((f " ) * f) * ls1) by RELAT_1: 36

        .= ls1 by A19, FUNCT_2: 17;

        ((f " ) * (f * ls2)) = (((f " ) * f) * ls2) by RELAT_1: 36

        .= ls2 by A19, FUNCT_2: 17;

        hence thesis by A14, A16, A20, A18, TOPALG_1: 46;

      end;

      hence thesis by A8, GROUP_6: 60;

    end;

    theorem :: TOPALG_3:32

    for S,T be non empty TopSpace, s be Point of S, t be Point of T, f be continuous Function of S, T, P be Path of t, (f . s), h be Homomorphism of ( pi_1 (S,s)), ( pi_1 (T,t)) st f is being_homeomorphism & ((f . s),t) are_connected & h = (( pi_1-iso P) * ( FundGrIso (f,s))) holds h is bijective

    proof

      let S,T be non empty TopSpace;

      let s be Point of S;

      let t be Point of T;

      let f be continuous Function of S, T;

      let P be Path of t, (f . s);

      let h be Homomorphism of ( pi_1 (S,s)), ( pi_1 (T,t));

      assume f is being_homeomorphism;

      then

       A1: ( FundGrIso (f,s)) is bijective by Th31;

      assume that

       A2: ((f . s),t) are_connected and

       A3: h = (( pi_1-iso P) * ( FundGrIso (f,s)));

      reconsider G = ( pi_1-iso P) as Homomorphism of ( pi_1 (T,(f . s))), ( pi_1 (T,t)) by A2, TOPALG_1: 50;

      G is bijective by A2, TOPALG_1: 55;

      hence thesis by A1, A3, GROUP_6: 64;

    end;

    theorem :: TOPALG_3:33

    for S be non empty TopSpace, T be non empty pathwise_connected TopSpace, s be Point of S, t be Point of T st (S,T) are_homeomorphic holds (( pi_1 (S,s)),( pi_1 (T,t))) are_isomorphic

    proof

      let S be non empty TopSpace;

      let T be non empty pathwise_connected TopSpace;

      let s be Point of S;

      let t be Point of T;

      given f be Function of S, T such that

       A1: f is being_homeomorphism;

      reconsider f as continuous Function of S, T by A1;

      take (( pi_1-iso the Path of t, (f . s)) * ( FundGrIso (f,s)));

      ( FundGrIso (f,s)) is bijective by A1, Th31;

      hence thesis by GROUP_6: 64;

    end;