:: The Definition and Basic Properties of Topological Groups
::  by Artur Korni{\l}owicz
::
:: Received September 7, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, SUBSET_1, PRE_TOPC, FUNCT_1, FUNCT_2, RELAT_1,
      VALUED_1, XBOOLE_0, ALGSTR_0, TARSKI, GROUP_1, ZFMISC_1, ORDINAL2,
      TOPS_2, CONNSP_2, TOPS_1, RCOMP_1, T_0TOPSP, BINOP_1, UNIALG_1, CARD_5,
      SETFAM_1, COMPTS_1, RLVECT_3, TOPGRP_1, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, CARD_1, TOPS_2,
      FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, SETFAM_1, GROUP_2,
      DOMAIN_1, STRUCT_0, ALGSTR_0, PRE_TOPC, GROUP_1, CONNSP_2, TOPS_1,
      COMPTS_1, BORSUK_1, T_0TOPSP, CANTOR_1, YELLOW_8;
 constructors TOPS_1, TOPS_2, COMPTS_1, GROUP_2, BORSUK_1, GRCAT_1, URYSOHN1,
      T_0TOPSP, CANTOR_1, YELLOW_8, TEX_1;
 registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, PRE_TOPC,
      TOPS_1, GROUP_1, COMPTS_1, BORSUK_1, TEX_1, BORSUK_2, RELSET_1, CARD_1,
      ORDINAL1, ALGSTR_0;
 requirements SUBSET, BOOLE, NUMERALS;
 definitions TARSKI, FUNCT_1, PRE_TOPC, GROUP_1, STRUCT_0, TOPS_1, TOPS_2,
      CONNSP_2, FUNCT_2, T_0TOPSP, XBOOLE_0, BINOP_1, SUBSET_1, COMPTS_1,
      RELAT_1, ALGSTR_0, GROUP_2;
 theorems PRE_TOPC, RELAT_1, TOPS_1, TOPS_2, BINOP_1, FUNCT_2, GROUP_1,
      GROUP_2, TARSKI, FUNCT_1, BORSUK_1, TEX_2, ZFMISC_1, CONNSP_2, URYSOHN1,
      T_0TOPSP, YELLOW_8, YELLOW_9, XBOOLE_0, XBOOLE_1, STRUCT_0, RELSET_1;
 schemes BINOP_1, FUNCT_2, XBOOLE_0;

begin  :: Preliminaries

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
  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 Th2:
  (id R)/" = id R
proof
  rng (id R) = [#]R by RELAT_1:45;
  then id R is onto by FUNCT_2:def 3;
  hence (id R)/" = (id the carrier of R)" by TOPS_2:def 4
    .= id R by FUNCT_1:45;
end;

theorem
  (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  :: On the groups

reserve H for non empty multMagma,
  P, Q, P1, Q1 for Subset of H,
  h for Element of H;

theorem 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 set;
  assume x in P * Q;
  then ex g, t being Element of H st x = g * t & g in P & t in Q;
  hence thesis by A1;
end;

theorem Th5:
  P c= Q implies P * h c= Q * h
proof
  assume
A1: P c= Q;
  let x be set;
  assume x in P * h;
  then ex g being Element of H st x = g * h & g in P by GROUP_2:28;
  hence thesis by A1,GROUP_2:28;
end;

theorem
  P c= Q implies h * P c= h * Q
proof
  assume
A1: P c= Q;
  let x be set;
  assume x in h * P;
  then ex g being 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 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 set;
  assume a in A";
  then ex g being Element of G st a = g" & g in A;
  hence thesis by A1;
end;

canceled;

theorem Th9:
  A c= B iff A" c= B"
proof
  A"" = A & B"" = B;
  hence thesis by Lm1;
end;

theorem Th10:
  (inverse_op G).:A = A"
proof
  set f = inverse_op G;
  hereby
    let y be set;
    assume y in f.:A;
    then consider x being set 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 set;
  assume y in A";
  then consider g being 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 Th11:
  (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 set;
    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 set;
  assume x in A";
  then consider g being 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 Th12:
  inverse_op G is one-to-one
proof
  set f = inverse_op G;
  let x1, x2 be set;
  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 Th13:
  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 set;
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
  proof
    thus inverse_op G is one-to-one by Th12;
    thus rng inverse_op G = the carrier of G by Th13;
  end;
end;

theorem Th14:
  (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 set;
    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;
  dom (f") = the carrier of G by FUNCT_2:def 1;
  hence thesis by A1,A2,FUNCT_1:2;
end;

theorem Th15:
  (the multF of H).:[:P,Q:] = P*Q
proof
  set f = the multF of H;
  hereby
    let y be set;
    assume y in f.:[:P,Q:];
    then consider x being set 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 being set 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 set;
  assume y in P*Q;
  then consider g, h being 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;
  func a* -> Function of G, G means
  :Def1:
  for x being Element of G holds it.x = a * x;
  existence
  proof
    deffunc U(Element of G) = a * $1;
    consider f being Function of the carrier of G, the carrier of G such that
A1: for x being 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 being Element of G holds f.x = a * x and
A3: for x being Element of G holds g.x = a * x;
    now
      let x be set;
      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 by FUNCT_2:12;
  end;
  func *a -> Function of G, G means
  :Def2:
  for x being Element of G holds it.x = x * a;
  existence
  proof
    deffunc U(Element of G) = $1 *a;
    consider f being Function of the carrier of G, the carrier of G such that
A4: for x being 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 being Element of G holds f.x = x * a and
A6: for x being Element of G holds g.x = x * a;
    now
      let x be set;
      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 by FUNCT_2:12;
  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 set;
      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 set;
    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 set;
      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 set;
    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 Th16:
  h*.:P = h * P
proof
  set f = h*;
  hereby
    let y be set;
    assume y in f.:P;
    then consider x being set 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 set;
  assume y in h * P;
  then consider s being 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 Th17:
  (*h).:P = P * h
proof
  set f = *h;
  hereby
    let y be set;
    assume y in f.:P;
    then consider x being set 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 set;
  assume y in P * h;
  then consider s being 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 Th18:
  a*/" = a"*
proof
  set f = a*, g = a"*;
A1: now
    reconsider h = f as Function;
    let y be set;
    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;
  dom (f/") = the carrier of G & dom g = the carrier of G by FUNCT_2:def 1;
  hence thesis by A1,FUNCT_1:2;
end;

theorem Th19:
  (*a)/" = *(a")
proof
  set f = *a, g = *(a");
A1: now
    reconsider h = f as Function;
    let y be set;
    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;
  dom (f/") = the carrier of G & dom g = the carrier of G by FUNCT_2:def 1;
  hence thesis by A1,FUNCT_1:2;
end;

begin  :: On the topological spaces

registration
  let T be TopStruct;
  cluster (id T)/" -> continuous;
  coherence by Th2;
end;

theorem Th20:
  id T is being_homeomorphism
proof
  thus dom id T = [#]T & rng id T = [#]T by RELAT_1:45;
  thus thesis;
end;

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 Th21:
  for T being non empty TopSpace, p being 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 Th21;
    take B;
    thus thesis;
  end;
end;

theorem
  for S, T being non empty TopSpace, f being Function of S, T st f is
open holds for p being Point of S, P being a_neighborhood of p ex R being 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 being 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
  for S, T being non empty TopSpace, f being Function of S, T st for p
being Point of S, P being open a_neighborhood of p ex R being 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 being Point of S, P being open a_neighborhood of p ex R being
  a_neighborhood of f.p st R c= f.:P;
  let A be Subset of S such that
A2: A is open;
  for x being set holds x in f.:A iff ex Q being 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 being set 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 being 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 being 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,XBOOLE_1:1;
      thus K is open;
      f.:V c= f.:A by A7,RELAT_1:123;
      hence K c= f.:A by A10,XBOOLE_1:1;
      thus x in K by A5,CONNSP_2:def 1;
    end;
    thus thesis;
  end;
  hence thesis by TOPS_1:25;
end;

theorem
  for S, T being non empty TopStruct, f being Function of S, T holds f
is being_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one & for
  P being 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 by TOPS_2:def 5;
    let P be Subset of T;
    hereby
      assume
A3:   P is closed;
      f is continuous by A1,TOPS_2:def 5;
      hence f"P is closed by A3,PRE_TOPC:def 6;
    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 being 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
  proof
    let P be Subset of T;
    thus thesis by A7;
  end;
  let R be Subset of S such that
A8: R is closed;
  for x1, x2 being Element of S st x1 in R & f.x1 = f.x2 holds x2 in R by A4,A6
,FUNCT_1:def 4;
  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 Th25:
  for S, T being non empty TopStruct, f being Function of S, T
  holds f is being_homeomorphism iff dom f = [#]S & rng f = [#]T & f is
  one-to-one & for P being 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 by TOPS_2:def 5;
    let P be Subset of S;
A5: f"(f.:P) c= P & P c= f"(f.:P) by A4,FUNCT_1:76,82;
A6: f/" is continuous by A3,TOPS_2:def 5;
    hereby
      assume
A7:   P is open;
      f is onto by A4,FUNCT_2:def 3;
      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,TOPS_2:def 5;
    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 being 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,FUNCT_2:def 3;
     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,TOPS_2:def 5;
end;

theorem
  for S, T being non empty TopStruct, f being Function of S, T holds f
is being_homeomorphism iff dom f = [#]S & rng f = [#]T & f is one-to-one & for
  P being 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 by TOPS_2:def 5;
    let P be Subset of T;
    hereby
      assume
A4:   P is open;
      f is continuous by A2,TOPS_2:def 5;
      hence f"P is open by A1,A4,TOPS_2:43;
    end;
    assume f"P is open;
    then f.:(f"P) is open by A2,Th25;
    hence P is open by A3,FUNCT_1:77;
  end;
  assume that
A5: dom f = [#]S and
A6: rng f = [#]T and
A7: f is one-to-one and
A8: for P being Subset of T holds P is open iff f"P is open;
A9: now
    let R be Subset of S such that
A10: R is open;
    for x1, x2 being Element of S st x1 in R & f.x1 = f.x2 holds x2 in R
    by A5,A7,FUNCT_1:def 4;
    then
A11: f"(f.:R) = R by T_0TOPSP:1;
    (f/")"R = f.:R by A6,A7,TOPS_2:54;
    hence (f/")"R is open by A8,A10,A11;
  end;
  thus dom f = [#]S & rng f = [#]T & f is one-to-one by A5,A6,A7;
  thus f is continuous by A1,A8,TOPS_2:43;
  [#]S <> {};
  hence thesis by A9,TOPS_2:43;
end;

theorem
  for S being TopSpace, T being non empty TopSpace, f being Function of
S, T holds f is continuous iff for P being 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 being 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 Th28:
  for S, T being non empty TopSpace, f being Function of S, T, A
  being 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,TOPS_2:def 5;
  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 Th29:
  for S, T being non empty TopSpace, f being Function of S, T, A
  being 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
  proof
    let f be Function of S, T;
    assume
A1: f is being_homeomorphism;
    then rng f = [#]T by TOPS_2:def 5;
    hence rng f = the carrier of T;
    thus thesis by A1,TOPS_2:def 5;
  end;
end;

registration
  let S, T be non empty TopStruct;
  cluster being_homeomorphism -> open for Function of S, T;
  coherence
  proof
    let f be Function of S, T;
    assume
A1: f is being_homeomorphism;
    let A be Subset of S;
    thus thesis by A1,Th25;
  end;
end;

registration
  let T be TopStruct;
  cluster being_homeomorphism for Function of T, T;
  existence
  proof
    take id T;
    thus thesis by Th20;
  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,RELAT_1:55;
      hence thesis by Th20;
    end;
  end;
end;

begin  :: The group of homoemorphisms

definition
  let S,T be TopStruct;
  assume
A1: S,T are_homeomorphic;
  mode Homeomorphism of S,T -> Function of S,T means
    :Def3:
    it is being_homeomorphism;
  existence by A1,T_0TOPSP:def 1;
end;

definition
  let T be TopStruct;
  mode Homeomorphism of T -> Function of T,T means
    :Def4:
    it is being_homeomorphism;
  existence
  proof
A1: id T is being_homeomorphism by Th20;
    then T,T are_homeomorphic by T_0TOPSP:def 1;
    then reconsider f = id T as Homeomorphism of T,T by A1,Def3;
    f is being_homeomorphism by Th20;
    hence thesis;
  end;
end;

definition
  let T be TopStruct;
  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 by T_0TOPSP:def 1;
    hence thesis by A1,Def3;
  end;
end;

definition
  let T be TopStruct;
  redefine func id T -> Homeomorphism of T,T;
  coherence
  proof
    id T is being_homeomorphism by Th20;
    hence T,T are_homeomorphic by T_0TOPSP:def 1;
    thus thesis by Th20;
  end;
end;

definition
  let T be TopStruct;
  redefine func id T -> Homeomorphism of T;
  coherence
  proof
    thus id T is being_homeomorphism by Th20;
  end;
end;

registration
  let T be TopStruct;
  cluster -> being_homeomorphism for Homeomorphism of T;
  coherence by Def4;
end;

theorem Th30:
  for f being 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 being 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 Th31:
  for f, g being 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;
  func HomeoGroup T -> strict multMagma means
  :Def5:
  (x in the carrier of it
  iff x is Homeomorphism of T) & for f, g being Homeomorphism of T holds (the
  multF of it).(f,g) = g * f;
  existence
  proof
    defpred X[set] means $1 is Homeomorphism of T;
    consider A being set such that
A1: for q being set holds q in A iff q in Funcs(the carrier of T,the
    carrier of T) & X[q] from XBOOLE_0:sch 1;
A2: now
      let f be Homeomorphism of T;
      f in Funcs(the carrier of T, the carrier of T) by FUNCT_2:9;
      hence f in A by A1;
    end;
    then reconsider A as non empty set;
    defpred P[Element of A, Element of A, Element of A] means ex f, g being
    Homeomorphism of T st $1 = f & $2 = g & $3 = g * f;
A3: for x, y being Element of A ex z being 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 Th31;
      then reconsider z = y1 * x1 as Element of A by A2;
      take z, x1, y1;
      thus thesis;
    end;
    consider o being BinOp of A such that
A4: for a, b being 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 being Homeomorphism of T st f1 = m & g1 = n & o.(f1,g1) = n *
    m by A4;
    hence thesis;
  end;
  uniqueness
  proof
    defpred X[set] 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
    being 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
    being Homeomorphism of T holds (the multF of B).(f,g) = g * f;
A7: for x being set holds x in the carrier of B iff X[x] by A6;
A8: for c, d being 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 being set 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
  for f, g being Homeomorphism of T for a, b being 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 Th30;
      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,Th31;
    reconsider a = r*g as Homeomorphism of T by Th31;
    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 Th33:
  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
  for f being Homeomorphism of T for a being 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 Th33;
  a * g = f/" * f by A4,A2,Def5
    .= id T by A1,A3,TOPS_2:52
    .= 1_G by Th33;
  hence thesis by A5,GROUP_1:5;
end;

definition
  let T be TopStruct;
  attr T is homogeneous means
  :Def6:
  for p, q being Point of T ex f being 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
  for T being homogeneous non empty TopSpace st ex p being Point of T st
  {p} is closed holds T is T_1
proof
  let T be homogeneous non empty TopSpace;
  given p being Point of T such that
A1: {p} is closed;
  now
    let q be Point of T;
    consider f being 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 Th36:
  for T being homogeneous non empty TopSpace st ex p being Point
  of T st for A being Subset of T st A is open & p in A holds ex B being 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 being Point of T such that
A1: for A being Subset of T st A is open & p in A holds ex B being
  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 being 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 being 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,Th25;
    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  :: On the topological groups

definition
  struct (multMagma, TopStruct) TopGrStr (# carrier -> set, multF -> BinOp of
    the carrier, topology -> Subset-Family of the carrier #);
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 being 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-like 1-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;
::   redefine func inverse_op G -> Function of G, G;
::   coherence;
:: end;

definition
  let G be Group-like associative non empty TopGrStr;
  attr G is UnContinuous means
  :Def7:
  inverse_op G is continuous;
end;

definition
  let G be TopSpace-like TopGrStr;
  attr G is BinContinuous means
  :Def8:
  for f being 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 associative 1-element TopGrStr;
  existence
  proof
    set R = the BinOp of {{}};
    1TopSp {{}} is 1-element;
    then reconsider
    T = TopGrStr (#{{}}, R, bool {{}}#) as strict TopSpace-like
            1-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 Th37:
  for T being BinContinuous non empty TopSpace-like TopGrStr, a,
  b being Element of T, W being a_neighborhood of a*b ex A being open
  a_neighborhood of a, B being 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 being a_neighborhood of [a,b] such that
A1: f.:H c= W by BORSUK_1:def 1;
  consider F being Subset-Family of [:T,T:] such that
A2: Int H = union F and
A3: for e being set st e in F ex X1, Y1 being 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 being set such that
A4: [a,b] in M and
A5: M in F by A2,TARSKI:def 4;
  consider A, B being 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 set;
  assume x in A*B;
  then consider g, h being 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 Th38:
  for T being TopSpace-like non empty TopGrStr st (for a, b being
  Element of T, W being a_neighborhood of a*b ex A being a_neighborhood of a, B
  being 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 being Element of T, W being a_neighborhood of a*b ex A
  being a_neighborhood of a, B being 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 being Point of [:T,T:], G being a_neighborhood of f.W ex H being
  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 being Point of T such that
A3: W = [a,b] by BORSUK_1:10;
    f.W = a*b by A2,A3;
    then consider
    A being a_neighborhood of a, B being 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,Th15;
  end;
  hence thesis by BORSUK_1:def 1;
end;

theorem Th39:
  for T being UnContinuous TopGroup, a being Element of T, W being
  a_neighborhood of a" ex A being 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 being 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 set;
  assume x in A";
  then consider g being 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 Th40:
  for T being TopGroup st for a being Element of T, W being
  a_neighborhood of a" ex A being a_neighborhood of a st A" c= W holds T is
  UnContinuous
proof
  let T be TopGroup such that
A1: for a being Element of T, W being a_neighborhood of a" ex A being
  a_neighborhood of a st A" c= W;
  set f = inverse_op T;
  for W being Point of T, G being a_neighborhood of f.W ex H being
  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 being a_neighborhood of a such that
A2: A" c= G by A1;
    take A;
    thus thesis by A2,Th10;
  end;
  hence f is continuous by BORSUK_1:def 1;
end;

theorem Th41:
  for T being TopologicalGroup, a, b being Element of T for W
  being a_neighborhood of a*(b") ex A being open a_neighborhood of a, B being
  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 being open a_neighborhood of a, B being open a_neighborhood of b"
  such that
A1: A*B c= W by Th37;
  consider C being open a_neighborhood of b such that
A2: C" c= B by Th39;
  take A, C;
  let x be set;
  assume x in A*(C");
  then consider g, h being Element of T such that
A3: x = g*h and
A4: g in A and
A5: h in C";
  consider k being 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
  for T being TopGroup st for a, b being Element of T, W being
a_neighborhood of a*(b") ex A being a_neighborhood of a, B being a_neighborhood
  of b st A*(B") c= W holds T is TopologicalGroup
proof
  let T be TopGroup such that
A1: for a, b being Element of T, W being a_neighborhood of a*(b") ex A
  being a_neighborhood of a, B being a_neighborhood of b st A*(B") c= W;
A2: for a being Element of T, W being a_neighborhood of a" ex A being
  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 being a_neighborhood of 1_T, B being a_neighborhood of a such
    that
A3: A*(B") c= W by A1;
    take B;
    let x be set;
    assume
A4: x in B";
    then consider g being 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 being Element of T, W being a_neighborhood of a*b ex A being
  a_neighborhood of a, B being 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 being a_neighborhood of a, B being a_neighborhood of b" such
    that
A6: A*(B") c= W by A1;
    consider B1 being a_neighborhood of b such that
A7: B1" c= B by A2;
    take A, B1;
    let x be set;
    assume x in A * B1;
    then consider g, h being 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,Th38,Th40;
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 being Point of G, A being a_neighborhood of f.w ex W being
    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 being open a_neighborhood of a, W being open a_neighborhood
      of w such that
A1:   B*W c= A by Th37;
      take W;
      let k be set;
      assume k in f.:W;
      then k in a * W by Th16;
      then
A2:   ex h being 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 being Point of G, A being a_neighborhood of f.w ex W being
    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 being open a_neighborhood of w, B being open a_neighborhood
      of a such that
A3:   W*B c= A by Th37;
      take W;
      let k be set;
      assume k in f.:W;
      then k in W * a by Th17;
      then
A4:   ex h being 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 Th43:
  for G being BinContinuous TopGroup, a being 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,def 3;
  thus f is continuous;
  f/" = (a"*) by Th18;
  hence thesis;
end;

theorem Th44:
  for G being BinContinuous TopGroup, a being 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,def 3;
  thus f is continuous;
  f/" = *(a") by Th19;
  hence thesis;
end;

definition
  let G be BinContinuous TopGroup, a be Element of G;
  redefine func a* -> Homeomorphism of G;
  coherence by Th43;
  redefine func *a -> Homeomorphism of G;
  coherence by Th44;
end;

theorem Th45:
  for G being 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,def 3;
  thus f is continuous by Def7;
  f = (f qua Function)" by Th14
    .= f/" by TOPS_2:def 4;
  hence thesis by Def7;
end;

definition
  let G be UnContinuous TopGroup;
  redefine func inverse_op G -> Homeomorphism of G;
  coherence by Th45;
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 Th46:
  for G being BinContinuous TopGroup, F being closed Subset of G,
  a being 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 Th17;
  hence thesis by TOPS_2:58;
end;

theorem Th47:
  for G being BinContinuous TopGroup, F being closed Subset of G,
  a being 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 Th16;
  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 Th46;
  cluster a * F -> closed;
  coherence by Th47;
end;

theorem Th48:
  for G being UnContinuous TopGroup, F being 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 Th10;
  hence thesis by TOPS_2:58;
end;

registration
  let G be UnContinuous TopGroup, F be closed Subset of G;
  cluster F" -> closed;
  coherence by Th48;
end;

theorem Th49:
  for G being BinContinuous TopGroup, O being open Subset of G, a
  being 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 Th17;
  hence thesis by Th25;
end;

theorem Th50:
  for G being BinContinuous TopGroup, O being open Subset of G, a
  being 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 Th16;
  hence thesis by Th25;
end;

registration
  let G be BinContinuous TopGroup, A be open Subset of G, a be Element of G;
  cluster A * a -> open;
  coherence by Th49;
  cluster a * A -> open;
  coherence by Th50;
end;

theorem Th51:
  for G being UnContinuous TopGroup, O being 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 Th10;
  hence thesis by Th25;
end;

registration
  let G be UnContinuous TopGroup, A be open Subset of G;
  cluster A" -> open;
  coherence by Th51;
end;

theorem Th52:
  for G being BinContinuous TopGroup, A, O being 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 set;
    assume x in O * A;
    then consider o, a being 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 set;
      assume q in Q;
      then ex h being 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 Th53:
  for G being BinContinuous TopGroup, A, O being 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 set;
    assume x in A * O;
    then consider a, o being 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 set;
      assume q in Q;
      then ex h being 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 Th52;
  cluster B * A -> open;
  coherence by Th53;
end;

theorem Th54:
  for G being UnContinuous TopGroup, a being Point of G, A being
  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 being 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,Th9;
  hence a" in Int (A") by A1,TOPS_1:22;
end;

theorem Th55:
  for G being TopologicalGroup, a being Point of G, A being
  a_neighborhood of a*a" ex B being 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 being open a_neighborhood of a such that
A1: X*Y" c= A by Th41;
  reconsider B = X /\ Y as open a_neighborhood of a by CONNSP_2:2;
  take B;
  let x be set;
  assume x in B*B";
  then consider g, h being 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 Th56:
  for G being UnContinuous TopGroup, A being 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 Th11;
  hence thesis by Th29;
end;

registration
  let G be UnContinuous TopGroup, A be dense Subset of G;
  cluster A" -> dense;
  coherence by Th56;
end;

theorem Th57:
  for G being BinContinuous TopGroup, A being dense Subset of G, a
  being 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 Th28;
end;

theorem Th58:
  for G being BinContinuous TopGroup, A being dense Subset of G, a
  being 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 Th17;
  hence thesis by Th28;
end;

registration
  let G be BinContinuous TopGroup, A be dense Subset of G, a be Point of G;
  cluster A * a -> dense;
  coherence by Th58;
  cluster a * A -> dense;
  coherence by Th57;
end;

theorem
  for G being TopologicalGroup, B being Basis of 1_G, M being dense
  Subset of G holds { V * x where V is Subset of G, x is 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 is Subset of G, x is Point of G: V in B & x in M };
A1: Z c= the topology of G
  proof
    let a be set;
    assume a in Z;
    then consider V being Subset of G, x being 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 being Subset of G st W is open for a being Point of G st a in W ex
  V being 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 being open a_neighborhood of 1_G such that
A8: V*V" c= W*a" by Th55;
    consider E being 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 being set 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 being 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 set;
      assume q in E*d";
      then
A16:  ex v being 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,XBOOLE_1:1;
    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 set;
    assume a in Z;
    then
    ex V being Subset of G, x being 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 Th60:
  for G being TopologicalGroup holds G is regular
proof
  let G be TopologicalGroup;
  ex p being Point of G st for A being Subset of G st A is open & p in A
  holds ex B being 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 being open a_neighborhood of e, B being open a_neighborhood of
    e" such that
A2: C*B c= A by A1,Th37;
    e"" = e;
    then B" is a_neighborhood of e by Th54;
    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 Th9;
    then C*W" c= C*B by Th4;
    then
A3: C*W" c= A by A2,XBOOLE_1:1;
    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 set;
    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 being set 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 being 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 Th36;
end;

registration
  cluster -> regular for TopologicalGroup;
  coherence by Th60;
end;

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