topgrp_1.miz



    begin

    reserve S,R for 1-sorted,

X for Subset of R,

T for TopStruct,

x for set;

    registration

      let X be set;

      cluster one-to-one onto for Function of X, X;

      existence

      proof

        take ( id X);

        thus ( id X) is one-to-one;

        thus ( rng ( id X)) = X by RELAT_1: 45;

      end;

    end

    theorem :: TOPGRP_1:1

    ( rng ( id S)) = ( [#] S) by RELAT_1: 45;

    registration

      let R be 1-sorted;

      cluster (( id R) /" ) -> one-to-one;

      coherence

      proof

        ( rng ( id R)) = ( [#] R) by RELAT_1: 45;

        hence thesis by TOPS_2: 50;

      end;

    end

    theorem :: TOPGRP_1:2

    

     Th2: (( id R) /" ) = ( id R)

    proof

      ( rng ( id R)) = ( [#] R) by RELAT_1: 45;

      then ( id R) is onto;

      

      hence (( id R) /" ) = (( id the carrier of R) " ) by TOPS_2:def 4

      .= ( id R) by FUNCT_1: 45;

    end;

    theorem :: TOPGRP_1:3

    (( id R) " X) = X

    proof

      ( rng ( id R)) = ( [#] R) by RELAT_1: 45;

      then

       A1: (( id R) .: X) = ((( id R) /" ) " X) by TOPS_2: 54;

      (( id R) /" ) = ( id R) by Th2;

      hence thesis by A1, FUNCT_1: 92;

    end;

    begin

    reserve H for non empty multMagma,

P,Q,P1,Q1 for Subset of H,

h for Element of H;

    theorem :: TOPGRP_1:4

    

     Th4: P c= P1 & Q c= Q1 implies (P * Q) c= (P1 * Q1)

    proof

      assume

       A1: P c= P1 & Q c= Q1;

      let x be object;

      assume x in (P * Q);

      then ex g,t be Element of H st x = (g * t) & g in P & t in Q;

      hence thesis by A1;

    end;

    theorem :: TOPGRP_1:5

    

     Th5: P c= Q implies (P * h) c= (Q * h)

    proof

      assume

       A1: P c= Q;

      let x be object;

      assume x in (P * h);

      then ex g be Element of H st x = (g * h) & g in P by GROUP_2: 28;

      hence thesis by A1, GROUP_2: 28;

    end;

    theorem :: TOPGRP_1:6

    P c= Q implies (h * P) c= (h * Q)

    proof

      assume

       A1: P c= Q;

      let x be object;

      assume x in (h * P);

      then ex g be Element of H st x = (h * g) & g in P by GROUP_2: 27;

      hence thesis by A1, GROUP_2: 27;

    end;

    reserve G for Group,

A,B for Subset of G,

a for Element of G;

    theorem :: TOPGRP_1:7

    

     Th7: a in (A " ) iff (a " ) in A

    proof

      ((a " ) " ) = a & ((A " ) " ) = A;

      hence thesis;

    end;

    

     Lm1: A c= B implies (A " ) c= (B " )

    proof

      assume

       A1: A c= B;

      let a be object;

      assume a in (A " );

      then ex g be Element of G st a = (g " ) & g in A;

      hence thesis by A1;

    end;

    ::$Canceled

    theorem :: TOPGRP_1:9

    

     Th8: A c= B iff (A " ) c= (B " )

    proof

      ((A " ) " ) = A & ((B " ) " ) = B;

      hence thesis by Lm1;

    end;

    theorem :: TOPGRP_1:10

    

     Th9: (( inverse_op G) .: A) = (A " )

    proof

      set f = ( inverse_op G);

      hereby

        let y be object;

        assume y in (f .: A);

        then

        consider x be object such that

         A1: x in the carrier of G and

         A2: x in A and

         A3: y = (f . x) by FUNCT_2: 64;

        reconsider x as Element of G by A1;

        y = (x " ) by A3, GROUP_1:def 6;

        hence y in (A " ) by A2;

      end;

      let y be object;

      assume y in (A " );

      then

      consider g be Element of G such that

       A4: y = (g " ) & g in A;

      (f . g) = (g " ) by GROUP_1:def 6;

      hence thesis by A4, FUNCT_2: 35;

    end;

    theorem :: TOPGRP_1:11

    

     Th10: (( inverse_op G) " A) = (A " )

    proof

      set f = ( inverse_op G);

      

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

      hereby

        let x be object;

        assume

         A2: x in (f " A);

        then

        reconsider g = x as Element of G;

        (f . x) in A by A2, FUNCT_1:def 7;

        then ((f . g) " ) in (A " );

        then ((g " ) " ) in (A " ) by GROUP_1:def 6;

        hence x in (A " );

      end;

      let x be object;

      assume x in (A " );

      then

      consider g be Element of G such that

       A3: x = (g " ) & g in A;

      (f . (g " )) = ((g " ) " ) by GROUP_1:def 6

      .= g;

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

    end;

    theorem :: TOPGRP_1:12

    

     Th11: ( inverse_op G) is one-to-one

    proof

      set f = ( inverse_op G);

      let x1,x2 be object;

      assume that

       A1: x1 in ( dom f) & x2 in ( dom f) and

       A2: (f . x1) = (f . x2);

      reconsider a = x1, b = x2 as Element of G by A1;

      (f . a) = (a " ) & (f . b) = (b " ) by GROUP_1:def 6;

      hence thesis by A2, GROUP_1: 9;

    end;

    theorem :: TOPGRP_1:13

    

     Th12: ( rng ( inverse_op G)) = the carrier of G

    proof

      set f = ( inverse_op G);

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

      let x be object;

      

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

      assume x in the carrier of G;

      then

      reconsider a = x as Element of G;

      (f . (a " )) = ((a " ) " ) by GROUP_1:def 6

      .= a;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    registration

      let G be Group;

      cluster ( inverse_op G) -> one-to-one onto;

      coherence by Th11, Th12;

    end

    theorem :: TOPGRP_1:14

    

     Th13: (( inverse_op G) " ) = ( inverse_op G)

    proof

      set f = ( inverse_op G);

      

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

       A2:

      now

        let x be object;

        assume x in ( dom f);

        then

        reconsider g = x as Element of G;

        

         A3: (f . (g " )) = ((g " ) " ) by GROUP_1:def 6

        .= g;

        

        thus (f . x) = (g " ) by GROUP_1:def 6

        .= ((f " ) . x) by A1, A3, FUNCT_1: 32;

      end;

      thus thesis by A1, A2;

    end;

    theorem :: TOPGRP_1:15

    

     Th14: (the multF of H .: [:P, Q:]) = (P * Q)

    proof

      set f = the multF of H;

      hereby

        let y be object;

        assume y in (f .: [:P, Q:]);

        then

        consider x be object such that x in [:the carrier of H, the carrier of H:] and

         A1: x in [:P, Q:] and

         A2: y = (f . x) by FUNCT_2: 64;

        consider a,b be object such that

         A3: a in P & b in Q and

         A4: x = [a, b] by A1, ZFMISC_1:def 2;

        reconsider a, b as Element of H by A3;

        y = (a * b) by A2, A4;

        hence y in (P * Q) by A3;

      end;

      let y be object;

      assume y in (P * Q);

      then

      consider g,h be Element of H such that

       A5: y = (g * h) and

       A6: g in P & h in Q;

       [g, h] in [:P, Q:] by A6, ZFMISC_1: 87;

      hence thesis by A5, FUNCT_2: 35;

    end;

    definition

      let G be non empty multMagma, a be Element of G;

      :: TOPGRP_1:def1

      func a * -> Function of G, G means

      : Def1: for x be Element of G holds (it . x) = (a * x);

      existence

      proof

        deffunc U( Element of G) = (a * $1);

        consider f be Function of the carrier of G, the carrier of G such that

         A1: for x be Element of G holds (f . x) = U(x) from FUNCT_2:sch 4;

        reconsider f as Function of G, G;

        take f;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let f,g be Function of G, G such that

         A2: for x be Element of G holds (f . x) = (a * x) and

         A3: for x be Element of G holds (g . x) = (a * x);

        now

          let x be object;

          assume x in the carrier of G;

          then

          reconsider y = x as Element of G;

          

          thus (f . x) = (a * y) by A2

          .= (g . x) by A3;

        end;

        hence thesis;

      end;

      :: TOPGRP_1:def2

      func * a -> Function of G, G means

      : Def2: for x be Element of G holds (it . x) = (x * a);

      existence

      proof

        deffunc U( Element of G) = ($1 * a);

        consider f be Function of the carrier of G, the carrier of G such that

         A4: for x be Element of G holds (f . x) = U(x) from FUNCT_2:sch 4;

        reconsider f as Function of G, G;

        take f;

        thus thesis by A4;

      end;

      uniqueness

      proof

        let f,g be Function of G, G such that

         A5: for x be Element of G holds (f . x) = (x * a) and

         A6: for x be Element of G holds (g . x) = (x * a);

        now

          let x be object;

          assume x in the carrier of G;

          then

          reconsider y = x as Element of G;

          

          thus (f . x) = (y * a) by A5

          .= (g . x) by A6;

        end;

        hence thesis;

      end;

    end

    registration

      let G be Group, a be Element of G;

      cluster (a * ) -> one-to-one onto;

      coherence

      proof

        set f = (a * );

        

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

        hereby

          let x1,x2 be object;

          assume that

           A2: x1 in ( dom f) & x2 in ( dom f) and

           A3: (f . x1) = (f . x2);

          reconsider y1 = x1, y2 = x2 as Element of G by A2;

          

           A4: (f . y1) = (a * y1) & (f . y2) = (a * y2) by Def1;

          

          thus x1 = (( 1_ G) * y1) by GROUP_1:def 4

          .= (((a " ) * a) * y1) by GROUP_1:def 5

          .= ((a " ) * (a * y1)) by GROUP_1:def 3

          .= (((a " ) * a) * y2) by A3, A4, GROUP_1:def 3

          .= (( 1_ G) * y2) by GROUP_1:def 5

          .= x2 by GROUP_1:def 4;

        end;

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

        let y be object;

        assume y in the carrier of G;

        then

        reconsider y1 = y as Element of G;

        (f . ((a " ) * y1)) = (a * ((a " ) * y1)) by Def1

        .= ((a * (a " )) * y1) by GROUP_1:def 3

        .= (( 1_ G) * y1) by GROUP_1:def 5

        .= y by GROUP_1:def 4;

        hence thesis by A1, FUNCT_1:def 3;

      end;

      cluster ( * a) -> one-to-one onto;

      coherence

      proof

        set f = ( * a);

        

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

        hereby

          let x1,x2 be object;

          assume that

           A6: x1 in ( dom f) & x2 in ( dom f) and

           A7: (f . x1) = (f . x2);

          reconsider y1 = x1, y2 = x2 as Element of G by A6;

          

           A8: (f . y1) = (y1 * a) & (f . y2) = (y2 * a) by Def2;

          

          thus x1 = (y1 * ( 1_ G)) by GROUP_1:def 4

          .= (y1 * (a * (a " ))) by GROUP_1:def 5

          .= ((y1 * a) * (a " )) by GROUP_1:def 3

          .= (y2 * (a * (a " ))) by A7, A8, GROUP_1:def 3

          .= (y2 * ( 1_ G)) by GROUP_1:def 5

          .= x2 by GROUP_1:def 4;

        end;

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

        let y be object;

        assume y in the carrier of G;

        then

        reconsider y1 = y as Element of G;

        (f . (y1 * (a " ))) = ((y1 * (a " )) * a) by Def2

        .= (y1 * ((a " ) * a)) by GROUP_1:def 3

        .= (y1 * ( 1_ G)) by GROUP_1:def 5

        .= y by GROUP_1:def 4;

        hence thesis by A5, FUNCT_1:def 3;

      end;

    end

    theorem :: TOPGRP_1:16

    

     Th15: ((h * ) .: P) = (h * P)

    proof

      set f = (h * );

      hereby

        let y be object;

        assume y in (f .: P);

        then

        consider x be object such that

         A1: x in ( dom f) and

         A2: x in P & y = (f . x) by FUNCT_1:def 6;

        reconsider x as Element of H by A1;

        (f . x) = (h * x) by Def1;

        hence y in (h * P) by A2, GROUP_2: 27;

      end;

      let y be object;

      assume y in (h * P);

      then

      consider s be Element of H such that

       A3: y = (h * s) & s in P by GROUP_2: 27;

      ( dom f) = the carrier of H & (f . s) = (h * s) by Def1, FUNCT_2:def 1;

      hence thesis by A3, FUNCT_1:def 6;

    end;

    theorem :: TOPGRP_1:17

    

     Th16: (( * h) .: P) = (P * h)

    proof

      set f = ( * h);

      hereby

        let y be object;

        assume y in (f .: P);

        then

        consider x be object such that

         A1: x in ( dom f) and

         A2: x in P & y = (f . x) by FUNCT_1:def 6;

        reconsider x as Element of H by A1;

        (f . x) = (x * h) by Def2;

        hence y in (P * h) by A2, GROUP_2: 28;

      end;

      let y be object;

      assume y in (P * h);

      then

      consider s be Element of H such that

       A3: y = (s * h) & s in P by GROUP_2: 28;

      ( dom f) = the carrier of H & (f . s) = (s * h) by Def2, FUNCT_2:def 1;

      hence thesis by A3, FUNCT_1:def 6;

    end;

    theorem :: TOPGRP_1:18

    

     Th17: ((a * ) /" ) = ((a " ) * )

    proof

      set f = (a * ), g = ((a " ) * );

       A1:

      now

        reconsider h = f as Function;

        let y be object;

        assume y in the carrier of G;

        then

        reconsider y1 = y as Element of G;

        ( rng f) = the carrier of G by FUNCT_2:def 3;

        then

         A2: y1 in ( rng f);

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

        then

         A3: (g . y1) in ( dom f) & ((f /" ) . y1) in ( dom f);

        (f . (g . y)) = (a * (g . y1)) by Def1

        .= (a * ((a " ) * y1)) by Def1

        .= ((a * (a " )) * y1) by GROUP_1:def 3

        .= (( 1_ G) * y1) by GROUP_1:def 5

        .= y by GROUP_1:def 4

        .= (h . ((h " ) . y)) by A2, FUNCT_1: 35

        .= (f . ((f /" ) . y)) by TOPS_2:def 4;

        hence ((f /" ) . y) = (g . y) by A3, FUNCT_1:def 4;

      end;

      thus thesis by A1;

    end;

    theorem :: TOPGRP_1:19

    

     Th18: (( * a) /" ) = ( * (a " ))

    proof

      set f = ( * a), g = ( * (a " ));

       A1:

      now

        reconsider h = f as Function;

        let y be object;

        assume y in the carrier of G;

        then

        reconsider y1 = y as Element of G;

        ( rng f) = the carrier of G by FUNCT_2:def 3;

        then

         A2: y1 in ( rng f);

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

        then

         A3: (g . y1) in ( dom f) & ((f /" ) . y1) in ( dom f);

        (f . (g . y)) = ((g . y1) * a) by Def2

        .= ((y1 * (a " )) * a) by Def2

        .= (y1 * ((a " ) * a)) by GROUP_1:def 3

        .= (y1 * ( 1_ G)) by GROUP_1:def 5

        .= y by GROUP_1:def 4

        .= (h . ((h " ) . y)) by A2, FUNCT_1: 35

        .= (f . ((f /" ) . y)) by TOPS_2:def 4;

        hence ((f /" ) . y) = (g . y) by A3, FUNCT_1:def 4;

      end;

      thus thesis by A1;

    end;

    begin

    registration

      let T be TopStruct;

      cluster (( id T) /" ) -> continuous;

      coherence by Th2;

    end

    theorem :: TOPGRP_1:20

    

     Th19: ( id T) is being_homeomorphism by RELAT_1: 45;

    registration

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

      cluster -> non empty for a_neighborhood of p;

      coherence

      proof

        let N be a_neighborhood of p;

        p in ( Int N) by CONNSP_2:def 1;

        hence thesis;

      end;

    end

    theorem :: TOPGRP_1:21

    

     Th20: for T be non empty TopSpace, p be Point of T holds ( [#] T) is a_neighborhood of p

    proof

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

      ( Int ( [#] T)) = the carrier of T by TOPS_1: 15;

      hence p in ( Int ( [#] T));

    end;

    registration

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

      cluster non empty open for a_neighborhood of p;

      existence

      proof

        reconsider B = ( [#] T) as a_neighborhood of p by Th20;

        take B;

        thus thesis;

      end;

    end

    theorem :: TOPGRP_1:22

    for S,T be non empty TopSpace, f be Function of S, T st f is open holds for p be Point of S, P be a_neighborhood of p holds ex R be open a_neighborhood of (f . p) st R c= (f .: P)

    proof

      let S,T be non empty TopSpace, f be Function of S, T such that

       A1: for A be Subset of S st A is open holds (f .: A) is open;

      let p be Point of S, P be a_neighborhood of p;

      

       A2: p in ( Int P) by CONNSP_2:def 1;

      (f .: ( Int P)) is open by A1;

      then

      reconsider R = (f .: ( Int P)) as open a_neighborhood of (f . p) by A2, CONNSP_2: 3, FUNCT_2: 35;

      take R;

      thus thesis by RELAT_1: 123, TOPS_1: 16;

    end;

    theorem :: TOPGRP_1:23

    for S,T be non empty TopSpace, f be Function of S, T st for p be Point of S, P be open a_neighborhood of p holds ex R be a_neighborhood of (f . p) st R c= (f .: P) holds f is open

    proof

      let S,T be non empty TopSpace, f be Function of S, T such that

       A1: for p be Point of S, P be open a_neighborhood of p holds ex R be a_neighborhood of (f . p) st R c= (f .: P);

      let A be Subset of S such that

       A2: A is open;

      for x be set holds x in (f .: A) iff ex Q be Subset of T st Q is open & Q c= (f .: A) & x in Q

      proof

        let x be set;

        hereby

          assume x in (f .: A);

          then

          consider a be object such that

           A3: a in ( dom f) and

           A4: a in A and

           A5: x = (f . a) by FUNCT_1:def 6;

          reconsider p = a as Point of S by A3;

          consider V be Subset of S such that

           A6: V is open and

           A7: V c= A and

           A8: a in V by A2, A4;

          V is a_neighborhood of p by A6, A8, CONNSP_2: 3;

          then

          consider R be a_neighborhood of (f . p) such that

           A9: R c= (f .: V) by A1, A6;

          take K = ( Int R);

          ( Int R) c= R by TOPS_1: 16;

          then

           A10: K c= (f .: V) by A9;

          thus K is open;

          (f .: V) c= (f .: A) by A7, RELAT_1: 123;

          hence K c= (f .: A) by A10;

          thus x in K by A5, CONNSP_2:def 1;

        end;

        thus thesis;

      end;

      hence thesis by TOPS_1: 25;

    end;

    theorem :: TOPGRP_1:24

    for S,T be non empty TopStruct, f be Function of S, T holds f is being_homeomorphism iff ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one & for P be Subset of T holds P is closed iff (f " P) is closed

    proof

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

      hereby

        assume

         A1: f is being_homeomorphism;

        hence

         A2: ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one;

        let P be Subset of T;

        hereby

          assume

           A3: P is closed;

          f is continuous by A1;

          hence (f " P) is closed by A3;

        end;

        assume (f " P) is closed;

        then (f .: (f " P)) is closed by A1, TOPS_2: 58;

        hence P is closed by A2, FUNCT_1: 77;

      end;

      assume that

       A4: ( dom f) = ( [#] S) and

       A5: ( rng f) = ( [#] T) and

       A6: f is one-to-one and

       A7: for P be Subset of T holds P is closed iff (f " P) is closed;

      thus ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one by A4, A5, A6;

      thus f is continuous by A7;

      let R be Subset of S such that

       A8: R is closed;

      for x1,x2 be Element of S st x1 in R & (f . x1) = (f . x2) holds x2 in R by A4, A6;

      then

       A9: (f " (f .: R)) = R by T_0TOPSP: 1;

      ((f /" ) " R) = (f .: R) by A5, A6, TOPS_2: 54;

      hence thesis by A7, A8, A9;

    end;

    theorem :: TOPGRP_1:25

    

     Th24: for S,T be non empty TopStruct, f be Function of S, T holds f is being_homeomorphism iff ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one & for P be Subset of S holds P is open iff (f .: P) is open

    proof

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

      

       A1: ( [#] T) <> {} ;

      

       A2: ( [#] S) <> {} ;

      hereby

        assume

         A3: f is being_homeomorphism;

        hence

         A4: ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one;

        let P be Subset of S;

        

         A5: (f " (f .: P)) c= P & P c= (f " (f .: P)) by A4, FUNCT_1: 76, FUNCT_1: 82;

        

         A6: (f /" ) is continuous by A3;

        hereby

          assume

           A7: P is open;

          f is onto by A4;

          

          then ((f /" ) " P) = ((f qua Function " ) " P) by A4, TOPS_2:def 4

          .= (f .: P) by A4, FUNCT_1: 84;

          hence (f .: P) is open by A2, A6, A7, TOPS_2: 43;

        end;

        assume

         A8: (f .: P) is open;

        f is continuous by A3;

        then (f " (f .: P)) is open by A1, A8, TOPS_2: 43;

        hence P is open by A5, XBOOLE_0:def 10;

      end;

      assume that

       A9: ( dom f) = ( [#] S) and

       A10: ( rng f) = ( [#] T) and

       A11: f is one-to-one and

       A12: for P be Subset of S holds P is open iff (f .: P) is open;

      now

        let B be Subset of T such that

         A13: B is open;

        B = (f .: (f " B)) by A10, FUNCT_1: 77;

        hence (f " B) is open by A12, A13;

      end;

      then

       A14: f is continuous by A1, TOPS_2: 43;

      now

        let B be Subset of S such that

         A15: B is open;

        f is onto by A10;

        

        then ((f /" ) " B) = ((f qua Function " ) " B) by A11, TOPS_2:def 4

        .= (f .: B) by A11, FUNCT_1: 84;

        hence ((f /" ) " B) is open by A12, A15;

      end;

      then (f /" ) is continuous by A2, TOPS_2: 43;

      hence thesis by A9, A10, A11, A14;

    end;

    theorem :: TOPGRP_1:26

    for S,T be non empty TopStruct, f be Function of S, T holds f is being_homeomorphism iff ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one & for P be Subset of T holds P is open iff (f " P) is open

    proof

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

      

       A1: ( [#] T) <> {} ;

      hereby

        assume

         A2: f is being_homeomorphism;

        hence

         A3: ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one;

        let P be Subset of T;

        thus P is open implies (f " P) is open by A2, TOPS_2: 43;

        assume (f " P) is open;

        then (f .: (f " P)) is open by A2, Th24;

        hence P is open by A3, FUNCT_1: 77;

      end;

      assume that

       A4: ( dom f) = ( [#] S) and

       A5: ( rng f) = ( [#] T) and

       A6: f is one-to-one and

       A7: for P be Subset of T holds P is open iff (f " P) is open;

       A8:

      now

        let R be Subset of S such that

         A9: R is open;

        for x1,x2 be Element of S st x1 in R & (f . x1) = (f . x2) holds x2 in R by A4, A6;

        then

         A10: (f " (f .: R)) = R by T_0TOPSP: 1;

        ((f /" ) " R) = (f .: R) by A5, A6, TOPS_2: 54;

        hence ((f /" ) " R) is open by A7, A9, A10;

      end;

      thus ( dom f) = ( [#] S) & ( rng f) = ( [#] T) & f is one-to-one by A4, A5, A6;

      thus f is continuous by A1, A7, TOPS_2: 43;

      ( [#] S) <> {} ;

      hence thesis by A8, TOPS_2: 43;

    end;

    theorem :: TOPGRP_1:27

    for S be TopSpace, T be non empty TopSpace, f be Function of S, T holds f is continuous iff for P be Subset of T holds (f " ( Int P)) c= ( Int (f " P))

    proof

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

      

       A1: ( [#] T) <> {} ;

      hereby

        assume

         A2: f is continuous;

        let P be Subset of T;

        (f " ( Int P)) c= (f " P) by RELAT_1: 143, TOPS_1: 16;

        then

         A3: ( Int (f " ( Int P))) c= ( Int (f " P)) by TOPS_1: 19;

        (f " ( Int P)) is open by A1, A2, TOPS_2: 43;

        hence (f " ( Int P)) c= ( Int (f " P)) by A3, TOPS_1: 23;

      end;

      assume

       A4: for P be Subset of T holds (f " ( Int P)) c= ( Int (f " P));

      now

        let P be Subset of T;

        assume P is open;

        then ( Int P) = P by TOPS_1: 23;

        then

         A5: (f " P) c= ( Int (f " P)) by A4;

        ( Int (f " P)) c= (f " P) by TOPS_1: 16;

        hence (f " P) is open by A5, XBOOLE_0:def 10;

      end;

      hence thesis by A1, TOPS_2: 43;

    end;

    registration

      let T be non empty TopSpace;

      cluster non empty dense for Subset of T;

      existence

      proof

        take ( [#] T);

        thus thesis;

      end;

    end

    theorem :: TOPGRP_1:28

    

     Th27: for S,T be non empty TopSpace, f be Function of S, T, A be dense Subset of S st f is being_homeomorphism holds (f .: A) is dense

    proof

      let S,T be non empty TopSpace, f be Function of S, T, A be dense Subset of S such that

       A1: f is being_homeomorphism;

      

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

      ( Cl A) = ( [#] S) by TOPS_1:def 3;

      

      hence ( Cl (f .: A)) = (f .: the carrier of S) by A1, TOPS_2: 60

      .= ( [#] T) by A2, RELSET_1: 22;

    end;

    theorem :: TOPGRP_1:29

    

     Th28: for S,T be non empty TopSpace, f be Function of S, T, A be dense Subset of T st f is being_homeomorphism holds (f " A) is dense

    proof

      let S,T be non empty TopSpace, f be Function of S, T, A be dense Subset of T such that

       A1: f is being_homeomorphism;

      

       A2: ( Cl A) = ( [#] T) by TOPS_1:def 3;

      

      thus ( Cl (f " A)) = (f " ( Cl A)) by A1, TOPS_2: 59

      .= ( [#] S) by A2, TOPS_2: 41;

    end;

    registration

      let S,T be TopStruct;

      cluster being_homeomorphism -> onto one-to-one continuous for Function of S, T;

      coherence ;

    end

    registration

      let S,T be non empty TopStruct;

      cluster being_homeomorphism -> open for Function of S, T;

      coherence by Th24;

    end

    registration

      let T be TopStruct;

      cluster being_homeomorphism for Function of T, T;

      existence

      proof

        take ( id T);

        thus thesis by Th19;

      end;

    end

    registration

      let T be TopStruct, f be being_homeomorphism Function of T, T;

      cluster (f /" ) -> being_homeomorphism;

      coherence

      proof

        per cases ;

          suppose T is non empty;

          hence thesis by TOPS_2: 56;

        end;

          suppose T is empty;

          then

           A1: the carrier of T is empty;

          (f /" ) = (f " ) by TOPS_2:def 4

          .= ( id T) by A1;

          hence thesis by Th19;

        end;

      end;

    end

    begin

    definition

      let S,T be TopStruct;

      assume

       A1: (S,T) are_homeomorphic ;

      :: TOPGRP_1:def3

      mode Homeomorphism of S,T -> Function of S, T means

      : Def3: it is being_homeomorphism;

      existence by A1;

    end

    definition

      let T be TopStruct;

      :: TOPGRP_1:def4

      mode Homeomorphism of T -> Function of T, T means

      : Def4: it is being_homeomorphism;

      existence

      proof

        

         A1: ( id T) is being_homeomorphism by Th19;

        then (T,T) are_homeomorphic ;

        then

        reconsider f = ( id T) as Homeomorphism of T, T by A1, Def3;

        f is being_homeomorphism by Th19;

        hence thesis;

      end;

    end

    definition

      let T be TopStruct;

      :: original: Homeomorphism

      redefine

      mode Homeomorphism of T -> Homeomorphism of T, T ;

      coherence

      proof

        let f be Homeomorphism of T;

        

         A1: f is being_homeomorphism by Def4;

        then (T,T) are_homeomorphic ;

        hence thesis by A1, Def3;

      end;

    end

    definition

      let T be TopStruct;

      :: original: id

      redefine

      func id T -> Homeomorphism of T, T ;

      coherence

      proof

        ( id T) is being_homeomorphism by Th19;

        hence (T,T) are_homeomorphic ;

        thus thesis by Th19;

      end;

    end

    definition

      let T be TopStruct;

      :: original: id

      redefine

      func id T -> Homeomorphism of T ;

      coherence

      proof

        thus ( id T) is being_homeomorphism by Th19;

      end;

    end

    registration

      let T be TopStruct;

      cluster -> being_homeomorphism for Homeomorphism of T;

      coherence by Def4;

    end

    theorem :: TOPGRP_1:30

    

     Th29: for f be Homeomorphism of T holds (f /" ) is Homeomorphism of T

    proof

      let f be Homeomorphism of T;

      thus (f /" ) is being_homeomorphism;

    end;

    

     Lm2: for T be TopStruct, f be Function of T, T st T is empty holds f is being_homeomorphism

    proof

      let T be TopStruct;

      let f be Function of T, T;

      assume

       A1: T is empty;

      

      then f = {}

      .= ( id T) by A1;

      hence thesis;

    end;

    theorem :: TOPGRP_1:31

    

     Th30: for f,g be Homeomorphism of T holds (f * g) is Homeomorphism of T

    proof

      let f,g be Homeomorphism of T;

      T is non empty or T is empty;

      hence (f * g) is being_homeomorphism by TOPS_2: 57;

    end;

    definition

      let T be TopStruct;

      :: TOPGRP_1:def5

      func HomeoGroup T -> strict multMagma means

      : Def5: (x in the carrier of it iff x is Homeomorphism of T) & for f,g be Homeomorphism of T holds (the multF of it . (f,g)) = (g * f);

      existence

      proof

        defpred X[ object] means $1 is Homeomorphism of T;

        consider A be set such that

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

        

         A2: for f be Homeomorphism of T holds f in A by A1, FUNCT_2: 9;

        then

        reconsider A as non empty set;

        defpred P[ Element of A, Element of A, Element of A] means ex f,g be Homeomorphism of T st $1 = f & $2 = g & $3 = (g * f);

        

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

        proof

          let x,y be Element of A;

          reconsider x1 = x, y1 = y as Homeomorphism of T by A1;

          (y1 * x1) is Homeomorphism of T by Th30;

          then

          reconsider z = (y1 * x1) as Element of A by A2;

          take z, x1, y1;

          thus thesis;

        end;

        consider o be BinOp of A such that

         A4: for a,b be Element of A holds P[a, b, (o . (a,b))] from BINOP_1:sch 3( A3);

        take G = multMagma (# A, o #);

        let x;

        thus x in the carrier of G iff x is Homeomorphism of T by A1, A2;

        let f,g be Homeomorphism of T;

        reconsider f1 = f, g1 = g as Element of A by A2;

        ex m,n be Homeomorphism of T st f1 = m & g1 = n & (o . (f1,g1)) = (n * m) by A4;

        hence thesis;

      end;

      uniqueness

      proof

        defpred X[ object] means $1 is Homeomorphism of T;

        let A,B be strict multMagma;

        assume that

         A5: (x in the carrier of A iff x is Homeomorphism of T) & for f,g be Homeomorphism of T holds (the multF of A . (f,g)) = (g * f) and

         A6: (x in the carrier of B iff x is Homeomorphism of T) & for f,g be Homeomorphism of T holds (the multF of B . (f,g)) = (g * f);

        

         A7: for x be object holds x in the carrier of B iff X[x] by A6;

        

         A8: for c,d be set st c in the carrier of A & d in the carrier of A holds (the multF of A . (c,d)) = (the multF of B . (c,d))

        proof

          let c,d be set;

          assume c in the carrier of A & d in the carrier of A;

          then

          reconsider f = c, g = d as Homeomorphism of T by A5;

          

          thus (the multF of A . (c,d)) = (g * f) by A5

          .= (the multF of B . (c,d)) by A6;

        end;

        

         A9: for x be object holds x in the carrier of A iff X[x] by A5;

        the carrier of A = the carrier of B from XBOOLE_0:sch 2( A9, A7);

        hence thesis by A8, BINOP_1: 1;

      end;

    end

    registration

      let T be TopStruct;

      cluster ( HomeoGroup T) -> non empty;

      coherence

      proof

        ( id T) is Homeomorphism of T;

        hence the carrier of ( HomeoGroup T) is non empty by Def5;

      end;

    end

    theorem :: TOPGRP_1:32

    for f,g be Homeomorphism of T holds for a,b be Element of ( HomeoGroup T) st f = a & g = b holds (a * b) = (g * f) by Def5;

    registration

      let T be TopStruct;

      cluster ( HomeoGroup T) -> Group-like associative;

      coherence

      proof

        set G = ( HomeoGroup T), o = the multF of G;

        thus G is Group-like

        proof

          reconsider e = ( id T) as Element of G by Def5;

          take e;

          let h be Element of G;

          reconsider h1 = h, e1 = e as Homeomorphism of T by Def5;

          

          thus (h * e) = (e1 * h1) by Def5

          .= h by FUNCT_2: 17;

          

          thus (e * h) = (h1 * e1) by Def5

          .= h by FUNCT_2: 17;

          reconsider h1 = h as Homeomorphism of T by Def5;

          

           A1: ( dom h1) = ( [#] T) by TOPS_2:def 5;

          (h1 /" ) is Homeomorphism of T by Th29;

          then

          reconsider g = (h1 /" ) as Element of G by Def5;

          reconsider g1 = g as Homeomorphism of T by Def5;

          take g;

          

           A2: ( rng h1) = ( [#] T) by TOPS_2:def 5;

          

          thus (h * g) = (g1 * h1) by Def5

          .= e by A1, A2, TOPS_2: 52;

          

          thus (g * h) = (h1 * g1) by Def5

          .= e by A2, TOPS_2: 52;

        end;

        let x,y,z be Element of G;

        reconsider f = x, g = y as Homeomorphism of T by Def5;

        reconsider p = (g * f), r = z as Homeomorphism of T by Def5, Th30;

        reconsider a = (r * g) as Homeomorphism of T by Th30;

        

        thus ((x * y) * z) = (o . ((g * f),z)) by Def5

        .= (r * p) by Def5

        .= ((r * g) * f) by RELAT_1: 36

        .= (o . (f,a)) by Def5

        .= (x * (y * z)) by Def5;

      end;

    end

    theorem :: TOPGRP_1:33

    

     Th32: ( id T) = ( 1_ ( HomeoGroup T))

    proof

      set G = ( HomeoGroup T);

      reconsider e = ( id T) as Element of G by Def5;

      now

        let h be Element of G;

        reconsider h1 = h as Homeomorphism of T by Def5;

        

        thus (h * e) = (( id T) * h1) by Def5

        .= h by FUNCT_2: 17;

        

        thus (e * h) = (h1 * ( id T)) by Def5

        .= h by FUNCT_2: 17;

      end;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: TOPGRP_1:34

    for f be Homeomorphism of T holds for a be Element of ( HomeoGroup T) st f = a holds (a " ) = (f /" )

    proof

      let f be Homeomorphism of T;

      set G = ( HomeoGroup T);

      

       A1: ( dom f) = ( [#] T) by TOPS_2:def 5;

      

       A2: (f /" ) is Homeomorphism of T by Def4;

      then

      reconsider g = (f /" ) as Element of G by Def5;

      

       A3: ( rng f) = ( [#] T) by TOPS_2:def 5;

      let a be Element of ( HomeoGroup T) such that

       A4: f = a;

      

       A5: (g * a) = (f * (f /" )) by A4, A2, Def5

      .= ( id T) by A3, TOPS_2: 52

      .= ( 1_ G) by Th32;

      (a * g) = ((f /" ) * f) by A4, A2, Def5

      .= ( id T) by A1, A3, TOPS_2: 52

      .= ( 1_ G) by Th32;

      hence thesis by A5, GROUP_1: 5;

    end;

    definition

      let T be TopStruct;

      :: TOPGRP_1:def6

      attr T is homogeneous means

      : Def6: for p,q be Point of T holds ex f be Homeomorphism of T st (f . p) = q;

    end

    registration

      cluster -> homogeneous for 1 -element TopStruct;

      coherence

      proof

        let T be 1 -element TopStruct;

        let p,q be Point of T;

        take ( id T);

        thus (( id T) . p) = q by STRUCT_0:def 10;

      end;

    end

    theorem :: TOPGRP_1:35

    for T be homogeneous non empty TopSpace st ex p be Point of T st {p} is closed holds T is T_1

    proof

      let T be homogeneous non empty TopSpace;

      given p be Point of T such that

       A1: {p} is closed;

      now

        let q be Point of T;

        consider f be Homeomorphism of T such that

         A2: (f . p) = q by Def6;

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

        then ( Im (f,p)) = {(f . p)} by FUNCT_1: 59;

        hence {q} is closed by A1, A2, TOPS_2: 58;

      end;

      hence thesis by URYSOHN1: 19;

    end;

    theorem :: TOPGRP_1:36

    

     Th35: for T be homogeneous non empty TopSpace st ex p be Point of T st for A be Subset of T st A is open & p in A holds ex B be Subset of T st p in B & B is open & ( Cl B) c= A holds T is regular

    proof

      let T be homogeneous non empty TopSpace;

      given p be Point of T such that

       A1: for A be Subset of T st A is open & p in A holds ex B be Subset of T st p in B & B is open & ( Cl B) c= A;

      

       A2: ( [#] T) <> {} ;

      now

        let A be open Subset of T, q be Point of T such that

         A3: q in A;

        consider f be Homeomorphism of T such that

         A4: (f . p) = q by Def6;

        

         A5: (f " A) is open by A2, TOPS_2: 43;

        reconsider g = f as Function;

        

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

        

         A7: ( rng f) = ( [#] T) by TOPS_2:def 5;

        then ((g " ) . q) = ((f " ) . q) & (g . ((g " ) . q)) in A by A3, FUNCT_1: 32;

        then

         A8: ((g " ) . q) in (g " A) by A6, FUNCT_1:def 7;

        p = ((g " ) . q) by A4, A6, FUNCT_1: 32;

        then

        consider B be Subset of T such that

         A9: p in B and

         A10: B is open and

         A11: ( Cl B) c= (f " A) by A1, A8, A5;

        reconsider fB = (f .: B) as open Subset of T by A10, Th24;

        take fB;

        thus q in fB by A4, A6, A9, FUNCT_1:def 6;

        

         A12: (f .: ( Cl B)) = ( Cl fB) by TOPS_2: 60;

        (f .: ( Cl B)) c= (f .: (f " A)) by A11, RELAT_1: 123;

        hence ( Cl fB) c= A by A7, A12, FUNCT_1: 77;

      end;

      hence thesis by URYSOHN1: 21;

    end;

    begin

    definition

      struct ( multMagma, TopStruct) TopGrStr (# the carrier -> set,

the multF -> BinOp of the carrier,

the topology -> Subset-Family of the carrier #)

       attr strict strict;

    end

    registration

      let A be non empty set, R be BinOp of A, T be Subset-Family of A;

      cluster TopGrStr (# A, R, T #) -> non empty;

      coherence ;

    end

    registration

      let x be set, R be BinOp of {x}, T be Subset-Family of {x};

      cluster TopGrStr (# {x}, R, T #) -> trivial;

      coherence ;

    end

    registration

      cluster -> Group-like associative commutative for 1 -element multMagma;

      coherence

      proof

        let H be 1 -element multMagma;

        hereby

          set e = the Element of H;

          take e;

          let h be Element of H;

          thus (h * e) = h & (e * h) = h by STRUCT_0:def 10;

          take g = e;

          thus (h * g) = e & (g * h) = e by STRUCT_0:def 10;

        end;

        thus for x,y,z be Element of H holds ((x * y) * z) = (x * (y * z)) by STRUCT_0:def 10;

        let x,y be Element of H;

        thus thesis by STRUCT_0:def 10;

      end;

    end

    registration

      let a be set;

      cluster ( 1TopSp {a}) -> trivial;

      coherence ;

    end

    registration

      cluster strict non empty for TopGrStr;

      existence

      proof

        set R = the BinOp of { {} }, T = the Subset-Family of { {} };

        take TopGrStr (# { {} }, R, T #);

        thus thesis;

      end;

    end

    registration

      cluster strict TopSpace-like1 -element for TopGrStr;

      existence

      proof

        set R = the BinOp of { {} };

        take TopGrStr (# { {} }, R, ( bool { {} }) #);

        the carrier of ( 1TopSp { {} }) is 1 -element;

        hence thesis by TEX_2: 7;

      end;

    end

    definition

      let G be Group-like associative non empty TopGrStr;

      :: TOPGRP_1:def7

      attr G is UnContinuous means

      : Def7: ( inverse_op G) is continuous;

    end

    definition

      let G be TopSpace-like TopGrStr;

      :: TOPGRP_1:def8

      attr G is BinContinuous means

      : Def8: for f be Function of [:G, G:], G st f = the multF of G holds f is continuous;

    end

    registration

      cluster strict commutative UnContinuous BinContinuous for TopSpace-like Group-like associative1 -element TopGrStr;

      existence

      proof

        set R = the BinOp of { {} };

        ( 1TopSp { {} }) is 1 -element;

        then

        reconsider T = TopGrStr (# { {} }, R, ( bool { {} }) #) as strict TopSpace-like1 -element TopGrStr by TEX_2: 7;

        take T;

        thus T is strict commutative;

        hereby

          set f = ( inverse_op T);

          thus f is continuous

          proof

            let P1 be Subset of T such that P1 is closed;

            per cases by ZFMISC_1: 33;

              suppose (f " P1) = {} ;

              hence thesis;

            end;

              suppose (f " P1) = { {} };

              then (f " P1) = ( [#] T);

              hence thesis;

            end;

          end;

        end;

        let f be Function of [:T, T:], T such that f = the multF of T;

        

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

        .= { [ {} , {} ]} by ZFMISC_1: 29;

        let P1 be Subset of T such that P1 is closed;

        per cases by A1, ZFMISC_1: 33;

          suppose (f " P1) = {} ;

          hence thesis;

        end;

          suppose (f " P1) = { [ {} , {} ]};

          then (f " P1) = ( [#] [:T, T:]) by A1;

          hence thesis;

        end;

      end;

    end

    definition

      mode TopGroup is TopSpace-like Group-like associative non empty TopGrStr;

    end

    definition

      mode TopologicalGroup is UnContinuous BinContinuous TopGroup;

    end

    theorem :: TOPGRP_1:37

    

     Th36: for T be BinContinuous non empty TopSpace-like TopGrStr, a,b be Element of T, W be a_neighborhood of (a * b) holds ex A be open a_neighborhood of a, B be open a_neighborhood of b st (A * B) c= W

    proof

      let T be BinContinuous non empty TopSpace-like TopGrStr, a,b be Element of T, W be a_neighborhood of (a * b);

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

      then

      reconsider f = the multF of T as Function of [:T, T:], T;

      f is continuous by Def8;

      then

      consider H be a_neighborhood of [a, b] such that

       A1: (f .: H) c= W by BORSUK_1:def 1;

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

       A2: ( Int H) = ( union F) and

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

       [a, b] in ( Int H) by CONNSP_2:def 1;

      then

      consider M be set such that

       A4: [a, b] in M and

       A5: M in F by A2, TARSKI:def 4;

      consider A,B be Subset of T such that

       A6: M = [:A, B:] and

       A7: A is open and

       A8: B is open by A3, A5;

      a in A by A4, A6, ZFMISC_1: 87;

      then

       A9: a in ( Int A) by A7, TOPS_1: 23;

      b in B by A4, A6, ZFMISC_1: 87;

      then b in ( Int B) by A8, TOPS_1: 23;

      then

      reconsider B as open a_neighborhood of b by A8, CONNSP_2:def 1;

      reconsider A as open a_neighborhood of a by A7, A9, CONNSP_2:def 1;

      take A, B;

      let x be object;

      assume x in (A * B);

      then

      consider g,h be Element of T such that

       A10: x = (g * h) and

       A11: g in A & h in B;

      

       A12: ( Int H) c= H by TOPS_1: 16;

       [g, h] in M by A6, A11, ZFMISC_1: 87;

      then [g, h] in ( Int H) by A2, A5, TARSKI:def 4;

      then x in (f .: H) by A10, A12, FUNCT_2: 35;

      hence thesis by A1;

    end;

    theorem :: TOPGRP_1:38

    

     Th37: for T be TopSpace-like non empty TopGrStr st (for a,b be Element of T, W be a_neighborhood of (a * b) holds ex A be a_neighborhood of a, B be a_neighborhood of b st (A * B) c= W) holds T is BinContinuous

    proof

      let T be TopSpace-like non empty TopGrStr such that

       A1: for a,b be Element of T, W be a_neighborhood of (a * b) holds ex A be a_neighborhood of a, B be a_neighborhood of b st (A * B) c= W;

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

       A2: f = the multF of T;

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

      proof

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

        consider a,b be Point of T such that

         A3: W = [a, b] by BORSUK_1: 10;

        (f . W) = (a * b) by A2, A3;

        then

        consider A be a_neighborhood of a, B be a_neighborhood of b such that

         A4: (A * B) c= G by A1;

        reconsider H = [:A, B:] as a_neighborhood of W by A3;

        take H;

        thus thesis by A2, A4, Th14;

      end;

      hence thesis by BORSUK_1:def 1;

    end;

    theorem :: TOPGRP_1:39

    

     Th38: for T be UnContinuous TopGroup, a be Element of T, W be a_neighborhood of (a " ) holds ex A be open a_neighborhood of a st (A " ) c= W

    proof

      let T be UnContinuous TopGroup, a be Element of T, W be a_neighborhood of (a " );

      reconsider f = ( inverse_op T) as Function of T, T;

      (f . a) = (a " ) & f is continuous by Def7, GROUP_1:def 6;

      then

      consider H be a_neighborhood of a such that

       A1: (f .: H) c= W by BORSUK_1:def 1;

      a in ( Int ( Int H)) by CONNSP_2:def 1;

      then

      reconsider A = ( Int H) as open a_neighborhood of a by CONNSP_2:def 1;

      take A;

      let x be object;

      assume x in (A " );

      then

      consider g be Element of T such that

       A2: x = (g " ) and

       A3: g in A;

      ( Int H) c= H & (f . g) = (g " ) by GROUP_1:def 6, TOPS_1: 16;

      then (g " ) in (f .: H) by A3, FUNCT_2: 35;

      hence thesis by A1, A2;

    end;

    theorem :: TOPGRP_1:40

    

     Th39: for T be TopGroup st for a be Element of T, W be a_neighborhood of (a " ) holds ex A be a_neighborhood of a st (A " ) c= W holds T is UnContinuous

    proof

      let T be TopGroup such that

       A1: for a be Element of T, W be a_neighborhood of (a " ) holds ex A be a_neighborhood of a st (A " ) c= W;

      set f = ( inverse_op T);

      for W be Point of T, G be a_neighborhood of (f . W) holds ex H be a_neighborhood of W st (f .: H) c= G

      proof

        let a be Point of T, G be a_neighborhood of (f . a);

        (f . a) = (a " ) by GROUP_1:def 6;

        then

        consider A be a_neighborhood of a such that

         A2: (A " ) c= G by A1;

        take A;

        thus thesis by A2, Th9;

      end;

      hence f is continuous by BORSUK_1:def 1;

    end;

    theorem :: TOPGRP_1:41

    

     Th40: for T be TopologicalGroup, a,b be Element of T holds for W be a_neighborhood of (a * (b " )) holds ex A be open a_neighborhood of a, B be open a_neighborhood of b st (A * (B " )) c= W

    proof

      let T be TopologicalGroup, a,b be Element of T, W be a_neighborhood of (a * (b " ));

      consider A be open a_neighborhood of a, B be open a_neighborhood of (b " ) such that

       A1: (A * B) c= W by Th36;

      consider C be open a_neighborhood of b such that

       A2: (C " ) c= B by Th38;

      take A, C;

      let x be object;

      assume x in (A * (C " ));

      then

      consider g,h be Element of T such that

       A3: x = (g * h) and

       A4: g in A and

       A5: h in (C " );

      consider k be Element of T such that

       A6: h = (k " ) and k in C by A5;

      (g * (k " )) in (A * B) by A2, A4, A5, A6;

      hence thesis by A1, A3, A6;

    end;

    theorem :: TOPGRP_1:42

    for T be TopGroup st for a,b be Element of T, W be a_neighborhood of (a * (b " )) holds ex A be a_neighborhood of a, B be a_neighborhood of b st (A * (B " )) c= W holds T is TopologicalGroup

    proof

      let T be TopGroup such that

       A1: for a,b be Element of T, W be a_neighborhood of (a * (b " )) holds ex A be a_neighborhood of a, B be a_neighborhood of b st (A * (B " )) c= W;

      

       A2: for a be Element of T, W be a_neighborhood of (a " ) holds ex A be a_neighborhood of a st (A " ) c= W

      proof

        let a be Element of T, W be a_neighborhood of (a " );

        W is a_neighborhood of (( 1_ T) * (a " )) by GROUP_1:def 4;

        then

        consider A be a_neighborhood of ( 1_ T), B be a_neighborhood of a such that

         A3: (A * (B " )) c= W by A1;

        take B;

        let x be object;

        assume

         A4: x in (B " );

        then

        consider g be Element of T such that

         A5: x = (g " ) and g in B;

        ( 1_ T) in A by CONNSP_2: 4;

        then (( 1_ T) * (g " )) in (A * (B " )) by A4, A5;

        then (g " ) in (A * (B " )) by GROUP_1:def 4;

        hence thesis by A3, A5;

      end;

      for a,b be Element of T, W be a_neighborhood of (a * b) holds ex A be a_neighborhood of a, B be a_neighborhood of b st (A * B) c= W

      proof

        let a,b be Element of T, W be a_neighborhood of (a * b);

        W is a_neighborhood of (a * ((b " ) " ));

        then

        consider A be a_neighborhood of a, B be a_neighborhood of (b " ) such that

         A6: (A * (B " )) c= W by A1;

        consider B1 be a_neighborhood of b such that

         A7: (B1 " ) c= B by A2;

        take A, B1;

        let x be object;

        assume x in (A * B1);

        then

        consider g,h be Element of T such that

         A8: x = (g * h) & g in A and

         A9: h in B1;

        (h " ) in (B1 " ) by A9;

        then h in (B " ) by A7, Th7;

        then x in (A * (B " )) by A8;

        hence thesis by A6;

      end;

      hence thesis by A2, Th37, Th39;

    end;

    registration

      let G be BinContinuous non empty TopSpace-like TopGrStr, a be Element of G;

      cluster (a * ) -> continuous;

      coherence

      proof

        set f = (a * );

        for w be Point of G, A be a_neighborhood of (f . w) holds ex W be a_neighborhood of w st (f .: W) c= A

        proof

          let w be Point of G, A be a_neighborhood of (f . w);

          (f . w) = (a * w) by Def1;

          then

          consider B be open a_neighborhood of a, W be open a_neighborhood of w such that

           A1: (B * W) c= A by Th36;

          take W;

          let k be object;

          assume k in (f .: W);

          then k in (a * W) by Th15;

          then

           A2: ex h be Element of G st k = (a * h) & h in W by GROUP_2: 27;

          a in B by CONNSP_2: 4;

          then k in (B * W) by A2;

          hence thesis by A1;

        end;

        hence thesis by BORSUK_1:def 1;

      end;

      cluster ( * a) -> continuous;

      coherence

      proof

        set f = ( * a);

        for w be Point of G, A be a_neighborhood of (f . w) holds ex W be a_neighborhood of w st (f .: W) c= A

        proof

          let w be Point of G, A be a_neighborhood of (f . w);

          (f . w) = (w * a) by Def2;

          then

          consider W be open a_neighborhood of w, B be open a_neighborhood of a such that

           A3: (W * B) c= A by Th36;

          take W;

          let k be object;

          assume k in (f .: W);

          then k in (W * a) by Th16;

          then

           A4: ex h be Element of G st k = (h * a) & h in W by GROUP_2: 28;

          a in B by CONNSP_2: 4;

          then k in (W * B) by A4;

          hence thesis by A3;

        end;

        hence thesis by BORSUK_1:def 1;

      end;

    end

    theorem :: TOPGRP_1:43

    

     Th42: for G be BinContinuous TopGroup, a be Element of G holds (a * ) is Homeomorphism of G

    proof

      let G be BinContinuous TopGroup, a be Element of G;

      set f = (a * );

      thus ( dom f) = ( [#] G) & ( rng f) = ( [#] G) & f is one-to-one by FUNCT_2:def 1, FUNCT_2:def 3;

      thus f is continuous;

      (f /" ) = ((a " ) * ) by Th17;

      hence thesis;

    end;

    theorem :: TOPGRP_1:44

    

     Th43: for G be BinContinuous TopGroup, a be Element of G holds ( * a) is Homeomorphism of G

    proof

      let G be BinContinuous TopGroup, a be Element of G;

      set f = ( * a);

      thus ( dom f) = ( [#] G) & ( rng f) = ( [#] G) & f is one-to-one by FUNCT_2:def 1, FUNCT_2:def 3;

      thus f is continuous;

      (f /" ) = ( * (a " )) by Th18;

      hence thesis;

    end;

    definition

      let G be BinContinuous TopGroup, a be Element of G;

      :: original: *

      redefine

      func a * -> Homeomorphism of G ;

      coherence by Th42;

      :: original: *

      redefine

      func * a -> Homeomorphism of G ;

      coherence by Th43;

    end

    theorem :: TOPGRP_1:45

    

     Th44: for G be UnContinuous TopGroup holds ( inverse_op G) is Homeomorphism of G

    proof

      let G be UnContinuous TopGroup;

      set f = ( inverse_op G);

      thus ( dom f) = ( [#] G) & ( rng f) = ( [#] G) & f is one-to-one by FUNCT_2:def 1, FUNCT_2:def 3;

      thus f is continuous by Def7;

      f = (f qua Function " ) by Th13

      .= (f /" ) by TOPS_2:def 4;

      hence thesis by Def7;

    end;

    definition

      let G be UnContinuous TopGroup;

      :: original: inverse_op

      redefine

      func inverse_op G -> Homeomorphism of G ;

      coherence by Th44;

    end

    registration

      cluster BinContinuous -> homogeneous for TopGroup;

      coherence

      proof

        let T be TopGroup;

        assume T is BinContinuous;

        then

        reconsider G = T as BinContinuous TopGroup;

        G is homogeneous

        proof

          let p,q be Point of G;

          take ( * ((p " ) * q));

          

          thus (( * ((p " ) * q)) . p) = (p * ((p " ) * q)) by Def2

          .= ((p * (p " )) * q) by GROUP_1:def 3

          .= (( 1_ G) * q) by GROUP_1:def 5

          .= q by GROUP_1:def 4;

        end;

        hence thesis;

      end;

    end

    theorem :: TOPGRP_1:46

    

     Th45: for G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G holds (F * a) is closed

    proof

      let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G;

      (F * a) = (( * a) .: F) by Th16;

      hence thesis by TOPS_2: 58;

    end;

    theorem :: TOPGRP_1:47

    

     Th46: for G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G holds (a * F) is closed

    proof

      let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G;

      (a * F) = ((a * ) .: F) by Th15;

      hence thesis by TOPS_2: 58;

    end;

    registration

      let G be BinContinuous TopGroup, F be closed Subset of G, a be Element of G;

      cluster (F * a) -> closed;

      coherence by Th45;

      cluster (a * F) -> closed;

      coherence by Th46;

    end

    theorem :: TOPGRP_1:48

    

     Th47: for G be UnContinuous TopGroup, F be closed Subset of G holds (F " ) is closed

    proof

      let G be UnContinuous TopGroup, F be closed Subset of G;

      (F " ) = (( inverse_op G) .: F) by Th9;

      hence thesis by TOPS_2: 58;

    end;

    registration

      let G be UnContinuous TopGroup, F be closed Subset of G;

      cluster (F " ) -> closed;

      coherence by Th47;

    end

    theorem :: TOPGRP_1:49

    

     Th48: for G be BinContinuous TopGroup, O be open Subset of G, a be Element of G holds (O * a) is open

    proof

      let G be BinContinuous TopGroup, O be open Subset of G, a be Element of G;

      (O * a) = (( * a) .: O) by Th16;

      hence thesis by Th24;

    end;

    theorem :: TOPGRP_1:50

    

     Th49: for G be BinContinuous TopGroup, O be open Subset of G, a be Element of G holds (a * O) is open

    proof

      let G be BinContinuous TopGroup, O be open Subset of G, a be Element of G;

      (a * O) = ((a * ) .: O) by Th15;

      hence thesis by Th24;

    end;

    registration

      let G be BinContinuous TopGroup, A be open Subset of G, a be Element of G;

      cluster (A * a) -> open;

      coherence by Th48;

      cluster (a * A) -> open;

      coherence by Th49;

    end

    theorem :: TOPGRP_1:51

    

     Th50: for G be UnContinuous TopGroup, O be open Subset of G holds (O " ) is open

    proof

      let G be UnContinuous TopGroup, O be open Subset of G;

      (O " ) = (( inverse_op G) .: O) by Th9;

      hence thesis by Th24;

    end;

    registration

      let G be UnContinuous TopGroup, A be open Subset of G;

      cluster (A " ) -> open;

      coherence by Th50;

    end

    theorem :: TOPGRP_1:52

    

     Th51: for G be BinContinuous TopGroup, A,O be Subset of G st O is open holds (O * A) is open

    proof

      let G be BinContinuous TopGroup, A,O be Subset of G such that

       A1: O is open;

      ( Int (O * A)) = (O * A)

      proof

        thus ( Int (O * A)) c= (O * A) by TOPS_1: 16;

        let x be object;

        assume x in (O * A);

        then

        consider o,a be Element of G such that

         A2: x = (o * a) & o in O and

         A3: a in A;

        set Q = (O * a);

        

         A4: Q c= (O * A)

        proof

          let q be object;

          assume q in Q;

          then ex h be Element of G st q = (h * a) & h in O by GROUP_2: 28;

          hence thesis by A3;

        end;

        x in Q by A2, GROUP_2: 28;

        hence thesis by A1, A4, TOPS_1: 22;

      end;

      hence thesis;

    end;

    theorem :: TOPGRP_1:53

    

     Th52: for G be BinContinuous TopGroup, A,O be Subset of G st O is open holds (A * O) is open

    proof

      let G be BinContinuous TopGroup, A,O be Subset of G such that

       A1: O is open;

      ( Int (A * O)) = (A * O)

      proof

        thus ( Int (A * O)) c= (A * O) by TOPS_1: 16;

        let x be object;

        assume x in (A * O);

        then

        consider a,o be Element of G such that

         A2: x = (a * o) and

         A3: a in A and

         A4: o in O;

        set Q = (a * O);

        

         A5: Q c= (A * O)

        proof

          let q be object;

          assume q in Q;

          then ex h be Element of G st q = (a * h) & h in O by GROUP_2: 27;

          hence thesis by A3;

        end;

        x in Q by A2, A4, GROUP_2: 27;

        hence thesis by A1, A5, TOPS_1: 22;

      end;

      hence thesis;

    end;

    registration

      let G be BinContinuous TopGroup, A be open Subset of G, B be Subset of G;

      cluster (A * B) -> open;

      coherence by Th51;

      cluster (B * A) -> open;

      coherence by Th52;

    end

    theorem :: TOPGRP_1:54

    

     Th53: for G be UnContinuous TopGroup, a be Point of G, A be a_neighborhood of a holds (A " ) is a_neighborhood of (a " )

    proof

      let G be UnContinuous TopGroup, a be Point of G, A be a_neighborhood of a;

      a in ( Int A) by CONNSP_2:def 1;

      then

      consider Q be Subset of G such that

       A1: Q is open and

       A2: Q c= A & a in Q by TOPS_1: 22;

      (Q " ) c= (A " ) & (a " ) in (Q " ) by A2, Th8;

      hence (a " ) in ( Int (A " )) by A1, TOPS_1: 22;

    end;

    theorem :: TOPGRP_1:55

    

     Th54: for G be TopologicalGroup, a be Point of G, A be a_neighborhood of (a * (a " )) holds ex B be open a_neighborhood of a st (B * (B " )) c= A

    proof

      let G be TopologicalGroup, a be Point of G, A be a_neighborhood of (a * (a " ));

      consider X,Y be open a_neighborhood of a such that

       A1: (X * (Y " )) c= A by Th40;

      reconsider B = (X /\ Y) as open a_neighborhood of a by CONNSP_2: 2;

      take B;

      let x be object;

      assume x in (B * (B " ));

      then

      consider g,h be Point of G such that

       A2: x = (g * h) and

       A3: g in B and

       A4: h in (B " );

      (h " ) in B by A4, Th7;

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

      then

       A5: h in (Y " ) by Th7;

      g in X by A3, XBOOLE_0:def 4;

      then x in (X * (Y " )) by A2, A5;

      hence thesis by A1;

    end;

    theorem :: TOPGRP_1:56

    

     Th55: for G be UnContinuous TopGroup, A be dense Subset of G holds (A " ) is dense

    proof

      let G be UnContinuous TopGroup, A be dense Subset of G;

      (( inverse_op G) " A) = (A " ) by Th10;

      hence thesis by Th28;

    end;

    registration

      let G be UnContinuous TopGroup, A be dense Subset of G;

      cluster (A " ) -> dense;

      coherence by Th55;

    end

    theorem :: TOPGRP_1:57

    

     Th56: for G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G holds (a * A) is dense

    proof

      let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;

      ((a * ) .: A) = (a * A) by Th15;

      hence thesis by Th27;

    end;

    theorem :: TOPGRP_1:58

    

     Th57: for G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G holds (A * a) is dense

    proof

      let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;

      (( * a) .: A) = (A * a) by Th16;

      hence thesis by Th27;

    end;

    registration

      let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;

      cluster (A * a) -> dense;

      coherence by Th57;

      cluster (a * A) -> dense;

      coherence by Th56;

    end

    theorem :: TOPGRP_1:59

    for G be TopologicalGroup, B be Basis of ( 1_ G), M be dense Subset of G holds { (V * x) where V be Subset of G, x be Point of G : V in B & x in M } is Basis of G

    proof

      let G be TopologicalGroup, B be Basis of ( 1_ G), M be dense Subset of G;

      set Z = { (V * x) where V be Subset of G, x be Point of G : V in B & x in M };

      

       A1: Z c= the topology of G

      proof

        let a be object;

        assume a in Z;

        then

        consider V be Subset of G, x be Point of G such that

         A2: a = (V * x) and

         A3: V in B and x in M;

        reconsider V as Subset of G;

        V is open by A3, YELLOW_8: 12;

        hence thesis by A2, PRE_TOPC:def 2;

      end;

      

       A4: for W be Subset of G st W is open holds for a be Point of G st a in W holds ex V be Subset of G st V in Z & a in V & V c= W

      proof

        

         A5: (( 1_ G) * (( 1_ G) " )) = (( 1_ G) * ( 1_ G)) by GROUP_1: 8

        .= ( 1_ G) by GROUP_1:def 4;

        let W be Subset of G such that

         A6: W is open;

        let a be Point of G such that

         A7: a in W;

        ( 1_ G) = (a * (a " )) by GROUP_1:def 5;

        then ( 1_ G) in (W * (a " )) by A7, GROUP_2: 28;

        then (W * (a " )) is a_neighborhood of (( 1_ G) * (( 1_ G) " )) by A6, A5, CONNSP_2: 3;

        then

        consider V be open a_neighborhood of ( 1_ G) such that

         A8: (V * (V " )) c= (W * (a " )) by Th54;

        consider E be Subset of G such that

         A9: E in B and

         A10: E c= V by CONNSP_2: 4, YELLOW_8: 13;

        E is open & E <> {} by A9, YELLOW_8: 12;

        then (a * (M " )) meets E by TOPS_1: 45;

        then

        consider d be object such that

         A11: d in ((a * (M " )) /\ E) by XBOOLE_0: 4;

        reconsider d as Point of G by A11;

        take I = (E * ((d " ) * a));

        d in (a * (M " )) by A11, XBOOLE_0:def 4;

        then

        consider m be Point of G such that

         A12: d = (a * m) and

         A13: m in (M " ) by GROUP_2: 27;

        ((d " ) * a) = (((d " ) * a) * ( 1_ G)) by GROUP_1:def 4

        .= (((d " ) * a) * (m * (m " ))) by GROUP_1:def 5

        .= ((((d " ) * a) * m) * (m " )) by GROUP_1:def 3

        .= (((d " ) * d) * (m " )) by A12, GROUP_1:def 3

        .= (( 1_ G) * (m " )) by GROUP_1:def 5

        .= (m " ) by GROUP_1:def 4;

        then ((d " ) * a) in M by A13, Th7;

        hence I in Z by A9;

        

         A14: (( 1_ G) * a) = a by GROUP_1:def 4;

        

         A15: d in E by A11, XBOOLE_0:def 4;

        (E * (d " )) c= (V * (V " ))

        proof

          let q be object;

          assume q in (E * (d " ));

          then

           A16: ex v be Point of G st q = (v * (d " )) & v in E by GROUP_2: 28;

          (d " ) in (V " ) by A10, A15;

          hence thesis by A10, A16;

        end;

        then (E * (d " )) c= (W * (a " )) by A8;

        then

         A17: ((E * (d " )) * a) c= ((W * (a " )) * a) by Th5;

        (d * (d " )) = ( 1_ G) by GROUP_1:def 5;

        then ( 1_ G) in (E * (d " )) by A15, GROUP_2: 28;

        then a in ((E * (d " )) * a) by A14, GROUP_2: 28;

        hence a in I by GROUP_2: 34;

        ((W * (a " )) * a) = (W * ((a " ) * a)) by GROUP_2: 34

        .= (W * ( 1_ G)) by GROUP_1:def 5

        .= W by GROUP_2: 37;

        hence thesis by A17, GROUP_2: 34;

      end;

      Z c= ( bool the carrier of G)

      proof

        let a be object;

        assume a in Z;

        then ex V be Subset of G, x be Point of G st a = (V * x) & V in B & x in M;

        hence thesis;

      end;

      hence thesis by A1, A4, YELLOW_9: 32;

    end;

    theorem :: TOPGRP_1:60

    

     Th59: for G be TopologicalGroup holds G is regular

    proof

      let G be TopologicalGroup;

      ex p be Point of G st for A be Subset of G st A is open & p in A holds ex B be Subset of G st p in B & B is open & ( Cl B) c= A

      proof

        set e = ( 1_ G);

        take e;

        let A be Subset of G;

        assume A is open & e in A;

        then e in ( Int A) by TOPS_1: 23;

        then

         A1: A is a_neighborhood of e by CONNSP_2:def 1;

        e = (e * (e " )) by GROUP_1:def 5;

        then

        consider C be open a_neighborhood of e, B be open a_neighborhood of (e " ) such that

         A2: (C * B) c= A by A1, Th36;

        ((e " ) " ) = e;

        then (B " ) is a_neighborhood of e by Th53;

        then

        reconsider W = (C /\ (B " )) as a_neighborhood of e by CONNSP_2: 2;

        W c= (B " ) by XBOOLE_1: 17;

        then (W " ) c= ((B " ) " ) by Th8;

        then (C * (W " )) c= (C * B) by Th4;

        then

         A3: (C * (W " )) c= A by A2;

        take W;

        ( Int W) = W by TOPS_1: 23;

        hence

         A4: e in W & W is open by CONNSP_2:def 1;

        let p be object;

        assume

         A5: p in ( Cl W);

        then

        reconsider r = p as Point of G;

        r = (r * e) by GROUP_1:def 4;

        then p in (r * W) by A4, GROUP_2: 27;

        then (r * W) meets W by A5, PRE_TOPC:def 7;

        then

        consider a be object such that

         A6: a in ((r * W) /\ W) by XBOOLE_0: 4;

        

         A7: a in W by A6, XBOOLE_0:def 4;

        

         A8: a in (r * W) by A6, XBOOLE_0:def 4;

        reconsider a as Point of G by A6;

        consider b be Element of G such that

         A9: a = (r * b) and

         A10: b in W by A8, GROUP_2: 27;

        

         A11: W c= C & (b " ) in (W " ) by A10, XBOOLE_1: 17;

        r = (r * e) by GROUP_1:def 4

        .= (r * (b * (b " ))) by GROUP_1:def 5

        .= (a * (b " )) by A9, GROUP_1:def 3;

        then p in (C * (W " )) by A7, A11;

        hence thesis by A3;

      end;

      hence thesis by Th35;

    end;

    registration

      cluster -> regular for TopologicalGroup;

      coherence by Th59;

    end

    theorem :: TOPGRP_1:61

    for T be TopStruct, f be Function of T, T st T is empty holds f is being_homeomorphism by Lm2;