:: TOPGRP_1 semantic presentation

begin


registration
let X be set ;
cluster Relation-like X -defined X -valued Function-like one-to-one V14(X) quasi_total onto for Element of bool [:X,X:];
existence
 ex b1 being Function of X,X st
( b1 is one-to-one & b1 is onto )
proof
take  id X ; ::_thesis: ( id X is one-to-one & id X is onto )
thus  id X is one-to-one ; ::_thesis: id X is onto
thus  rng (id X) = X by RELAT_1:45; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;

theorem :: TOPGRP_1:1
for S being 1-sorted holds rng (id S) = [#] S by RELAT_1:45;

registration
let R be 1-sorted ;
cluster(id R) /"  ->  one-to-one ;
coherence
 (id R) /" is one-to-one
proof
 rng (id R) = [#] R by RELAT_1:45;
hence  (id R) /" is one-to-one by TOPS_2:50; ::_thesis: verum
end;
end;

theorem Th2: :: TOPGRP_1:2
for R being 1-sorted holds (id R) /" = id R
proof
let R be 1-sorted ; ::_thesis: (id R) /" = id R
 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 ;
::_thesis: verum
end;

theorem :: TOPGRP_1:3
for R being 1-sorted
for X being Subset of R holds (id R) " X = X
proof
let R be 1-sorted ; ::_thesis: for X being Subset of R holds (id R) " X = X
let X be Subset of R; ::_thesis: (id R) " X = X
 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  (id R) " X = X by A1, FUNCT_1:92; ::_thesis: verum
end;

begin


theorem Th4: :: TOPGRP_1:4
for H being non empty multMagma
for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1
proof
let H be non empty multMagma ; ::_thesis: for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1
let P, P1, Q, Q1 be Subset of H; ::_thesis: ( P c= P1 & Q c= Q1 implies P * Q c= P1 * Q1 )
assume A1: ( P c= P1 & Q c= Q1 ) ; ::_thesis: P * Q c= P1 * Q1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P * Q or x in P1 * Q1 )
assume  x in P * Q ; ::_thesis: x in P1 * Q1
then  ex g, t being Element of H st
( x = g * t & g in P & t in Q ) ;
hence  x in P1 * Q1 by A1; ::_thesis: verum
end;

theorem Th5: :: TOPGRP_1:5
for H being non empty multMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
P * h c= Q * h
proof
let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H
for h being Element of H st P c= Q holds
P * h c= Q * h
let P, Q be Subset of H; ::_thesis: for h being Element of H st P c= Q holds
P * h c= Q * h
let h be Element of H; ::_thesis: ( P c= Q implies P * h c= Q * h )
assume A1: P c= Q ; ::_thesis: P * h c= Q * h
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in P * h or x in Q * h )
assume  x in P * h ; ::_thesis: x in Q * h
then  ex g being Element of H st
( x = g * h & g in P ) by GROUP_2:28;
hence  x in Q * h by A1, GROUP_2:28; ::_thesis: verum
end;

theorem :: TOPGRP_1:6
for H being non empty multMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
h * P c= h * Q
proof
let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H
for h being Element of H st P c= Q holds
h * P c= h * Q
let P, Q be Subset of H; ::_thesis: for h being Element of H st P c= Q holds
h * P c= h * Q
let h be Element of H; ::_thesis: ( P c= Q implies h * P c= h * Q )
assume A1: P c= Q ; ::_thesis: h * P c= h * Q
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in h * P or x in h * Q )
assume  x in h * P ; ::_thesis: x in h * Q
then  ex g being Element of H st
( x = h * g & g in P ) by GROUP_2:27;
hence  x in h * Q by A1, GROUP_2:27; ::_thesis: verum
end;


theorem Th7: :: TOPGRP_1:7
for G being Group
for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )
proof
let G be Group; ::_thesis: for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )
let A be Subset of G; ::_thesis: for a being Element of G holds
( a in A " iff a " in A )
let a be Element of G; ::_thesis: ( a in A " iff a " in A )
 ( (a ") " = a & (A ") " = A ) ;
hence  ( a in A " iff a " in A ) ; ::_thesis: verum
end;

Lm1:  for G being Group
for A, B being Subset of G st A c= B holds
A " c= B "
proof
let G be Group; ::_thesis: for A, B being Subset of G st A c= B holds
A " c= B "
let A, B be Subset of G; ::_thesis: ( A c= B implies A " c= B " )
assume A1: A c= B ; ::_thesis: A " c= B "
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in A " or a in B " )
assume  a in A " ; ::_thesis: a in B "
then  ex g being Element of G st
( a = g " & g in A ) ;
hence  a in B " by A1; ::_thesis: verum
end;

theorem :: TOPGRP_1:8
canceled;

theorem Th9: :: TOPGRP_1:9
for G being Group
for A, B being Subset of G holds
( A c= B iff A " c= B " )
proof
let G be Group; ::_thesis: for A, B being Subset of G holds
( A c= B iff A " c= B " )
let A, B be Subset of G; ::_thesis: ( A c= B iff A " c= B " )
 ( (A ") " = A & (B ") " = B ) ;
hence  ( A c= B iff A " c= B " ) by Lm1; ::_thesis: verum
end;

theorem Th10: :: TOPGRP_1:10
for G being Group
for A being Subset of G holds (inverse_op G) .: A = A "
proof
let G be Group; ::_thesis: for A being Subset of G holds (inverse_op G) .: A = A "
let A be Subset of G; ::_thesis: (inverse_op G) .: A = A "
set f = inverse_op G;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A " c= (inverse_op G) .: A
let y be set ; ::_thesis: ( y in (inverse_op G) .: A implies y in A " )
assume  y in (inverse_op G) .: A ; ::_thesis: y in A "
then consider x being set  such that
A1: x in the carrier of G and
A2: x in A and
A3: y = (inverse_op G) . x by FUNCT_2:64;
reconsider x = x as Element of G by A1;
 y = x " by A3, GROUP_1:def_6;
hence  y in A " by A2; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in A " or y in (inverse_op G) .: A )
assume  y in A " ; ::_thesis: y in (inverse_op G) .: A
then consider g being Element of G such that
A4: ( y = g " & g in A ) ;
 (inverse_op G) . g = g " by GROUP_1:def_6;
hence  y in (inverse_op G) .: A by A4, FUNCT_2:35; ::_thesis: verum
end;

theorem Th11: :: TOPGRP_1:11
for G being Group
for A being Subset of G holds (inverse_op G) " A = A "
proof
let G be Group; ::_thesis: for A being Subset of G holds (inverse_op G) " A = A "
let A be Subset of G; ::_thesis: (inverse_op G) " A = A "
set f = inverse_op G;
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: A " c= (inverse_op G) " A
let x be set ; ::_thesis: ( x in (inverse_op G) " A implies x in A " )
assume A2: x in (inverse_op G) " A ; ::_thesis: x in A "
then reconsider g = x as Element of G ;
 (inverse_op G) . x in A by A2, FUNCT_1:def_7;
then  ((inverse_op G) . g) " in A " ;
then  (g ") " in A " by GROUP_1:def_6;
hence  x in A " ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in (inverse_op G) " A )
assume  x in A " ; ::_thesis: x in (inverse_op G) " A
then consider g being Element of G such that
A3: ( x = g " & g in A ) ;
(inverse_op G) . (g ") = (g ") " by GROUP_1:def_6
.= g ;
hence  x in (inverse_op G) " A by A1, A3, FUNCT_1:def_7; ::_thesis: verum
end;

theorem Th12: :: TOPGRP_1:12
for G being Group holds inverse_op G is one-to-one
proof
let G be Group; ::_thesis: inverse_op G is one-to-one
set f = inverse_op G;
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom (inverse_op G) or not x2 in dom (inverse_op G) or not (inverse_op G) . x1 = (inverse_op G) . x2 or x1 = x2 )
assume that
A1: ( x1 in dom (inverse_op G) & x2 in dom (inverse_op G) ) and
A2: (inverse_op G) . x1 = (inverse_op G) . x2 ; ::_thesis: x1 = x2
reconsider a = x1, b = x2 as Element of G by A1;
 ( (inverse_op G) . a = a " & (inverse_op G) . b = b " ) by GROUP_1:def_6;
hence  x1 = x2 by A2, GROUP_1:9; ::_thesis: verum
end;

theorem Th13: :: TOPGRP_1:13
for G being Group holds rng (inverse_op G) = the carrier of G
proof
let G be Group; ::_thesis: rng (inverse_op G) = the carrier of G
set f = inverse_op G;
thus  rng (inverse_op G) c= the carrier of G ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (inverse_op G)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of G or x in rng (inverse_op G) )
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1;
assume  x in the carrier of G ; ::_thesis: x in rng (inverse_op G)
then reconsider a = x as Element of G ;
(inverse_op G) . (a ") = (a ") " by GROUP_1:def_6
.= a ;
hence  x in rng (inverse_op G) by A1, FUNCT_1:def_3; ::_thesis: verum
end;

registration
let G be Group;
cluster inverse_op G ->  one-to-one onto ;
coherence
 ( inverse_op G is one-to-one & inverse_op G is onto )
proof
thus  inverse_op G is one-to-one by Th12; ::_thesis: inverse_op G is onto
thus  rng (inverse_op G) = the carrier of G by Th13; :: according to FUNCT_2:def_3 ::_thesis: verum
end;
end;

theorem Th14: :: TOPGRP_1:14
for G being Group holds (inverse_op G) " = inverse_op G
proof
let G be Group; ::_thesis: (inverse_op G) " = inverse_op G
set f = inverse_op G;
A1: dom (inverse_op G) = the carrier of G by FUNCT_2:def_1;
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(inverse_op_G)_holds_
(inverse_op_G)_._x_=_((inverse_op_G)_")_._x
let x be set ; ::_thesis: ( x in dom (inverse_op G) implies (inverse_op G) . x = ((inverse_op G) ") . x )
assume  x in dom (inverse_op G) ; ::_thesis: (inverse_op G) . x = ((inverse_op G) ") . x
then reconsider g = x as Element of G ;
A3: (inverse_op G) . (g ") = (g ") " by GROUP_1:def_6
.= g ;
thus (inverse_op G) . x = g " by GROUP_1:def_6
.= ((inverse_op G) ") . x by A1, A3, FUNCT_1:32 ; ::_thesis: verum
end;
 dom ((inverse_op G) ") = the carrier of G by FUNCT_2:def_1;
hence  (inverse_op G) " = inverse_op G by A1, A2, FUNCT_1:2; ::_thesis: verum
end;

theorem Th15: :: TOPGRP_1:15
for H being non empty multMagma
for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q
proof
let H be non empty multMagma ; ::_thesis: for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q
let P, Q be Subset of H; ::_thesis: the multF of H .: [:P,Q:] = P * Q
set f = the multF of H;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P * Q c= the multF of H .: [:P,Q:]
let y be set ; ::_thesis: ( y in the multF of H .: [:P,Q:] implies y in P * Q )
assume  y in the multF of H .: [:P,Q:] ; ::_thesis: y in 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 = the multF of H . 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 = a, b = b as Element of H by A3;
 y = a * b by A2, A4;
hence  y in P * Q by A3; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P * Q or y in the multF of H .: [:P,Q:] )
assume  y in P * Q ; ::_thesis: y in the multF of H .: [: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  y in the multF of H .: [:P,Q:] by A5, FUNCT_2:35; ::_thesis: verum
end;

definition
let G be non empty multMagma ;
let a be Element of G;
funca *  ->  Function of G,G means :Def1: :: TOPGRP_1:def 1
 for x being Element of G holds it . x = a * x;
existence
 ex b1 being Function of G,G st
for x being Element of G holds b1 . x = a * x
proof
deffunc H1( Element of G) ->  Element of the carrier 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 = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of G,G ;
take  f ; ::_thesis: for x being Element of G holds f . x = a * x
thus  for x being Element of G holds f . x = a * x by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = a * x ) & ( for x being Element of G holds b2 . x = a * x ) holds
b1 = b2
proof
let f, g be Function of G,G; ::_thesis: ( ( for x being Element of G holds f . x = a * x ) & ( for x being Element of G holds g . x = a * x ) implies f = g )
assume 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 ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of G implies f . x = g . x )
assume  x in the carrier of G ; ::_thesis: f . x = g . x
then reconsider y = x as Element of G ;
thus f . x = a * y by A2
.= g . x by A3 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
func * a ->  Function of G,G means :Def2: :: TOPGRP_1:def 2
 for x being Element of G holds it . x = x * a;
existence
 ex b1 being Function of G,G st
for x being Element of G holds b1 . x = x * a
proof
deffunc H1( Element of G) ->  Element of the carrier 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 = H1(x) from FUNCT_2:sch_4();
reconsider f = f as Function of G,G ;
take  f ; ::_thesis: for x being Element of G holds f . x = x * a
thus  for x being Element of G holds f . x = x * a by A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = x * a ) & ( for x being Element of G holds b2 . x = x * a ) holds
b1 = b2
proof
let f, g be Function of G,G; ::_thesis: ( ( for x being Element of G holds f . x = x * a ) & ( for x being Element of G holds g . x = x * a ) implies f = g )
assume 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 ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_G_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in the carrier of G implies f . x = g . x )
assume  x in the carrier of G ; ::_thesis: f . x = g . x
then reconsider y = x as Element of G ;
thus f . x = y * a by A5
.= g . x by A6 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines * TOPGRP_1:def_1_:_
 for G being non empty multMagma
for a being Element of G
for b3 being Function of G,G holds
( b3 = a * iff for x being Element of G holds b3 . x = a * x );

:: deftheorem Def2 defines * TOPGRP_1:def_2_:_
 for G being non empty multMagma
for a being Element of G
for b3 being Function of G,G holds
( b3 = * a iff for x being Element of G holds b3 . x = x * a );

registration
let G be Group;
let a be Element of G;
clustera *  ->  one-to-one onto ;
coherence
 ( a * is one-to-one & a * is onto )
proof
set f = a * ;
A1: dom (a *) = the carrier of G by FUNCT_2:def_1;
hereby  :: according to FUNCT_1:def_4 ::_thesis: a * is onto
let x1, x2 be set ; ::_thesis: ( x1 in dom (a *) & x2 in dom (a *) & (a *) . x1 = (a *) . x2 implies x1 = x2 )
assume that
A2: ( x1 in dom (a *) & x2 in dom (a *) ) and
A3: (a *) . x1 = (a *) . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of G by A2;
A4: ( (a *) . y1 = a * y1 & (a *) . 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 ; ::_thesis: verum
end;
thus  rng (a *) c= the carrier of G ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (a *)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng (a *) )
assume  y in the carrier of G ; ::_thesis: y in rng (a *)
then reconsider y1 = y as Element of G ;
(a *) . ((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  y in rng (a *) by A1, FUNCT_1:def_3; ::_thesis: verum
end;
cluster * a ->  one-to-one onto ;
coherence
 ( * a is one-to-one & * a is onto )
proof
set f = * a;
A5: dom (* a) = the carrier of G by FUNCT_2:def_1;
hereby  :: according to FUNCT_1:def_4 ::_thesis: * a is onto
let x1, x2 be set ; ::_thesis: ( x1 in dom (* a) & x2 in dom (* a) & (* a) . x1 = (* a) . x2 implies x1 = x2 )
assume that
A6: ( x1 in dom (* a) & x2 in dom (* a) ) and
A7: (* a) . x1 = (* a) . x2 ; ::_thesis: x1 = x2
reconsider y1 = x1, y2 = x2 as Element of G by A6;
A8: ( (* a) . y1 = y1 * a & (* a) . 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 ; ::_thesis: verum
end;
thus  rng (* a) c= the carrier of G ; :: according to FUNCT_2:def_3,XBOOLE_0:def_10 ::_thesis: the carrier of G c= rng (* a)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of G or y in rng (* a) )
assume  y in the carrier of G ; ::_thesis: y in rng (* a)
then reconsider y1 = y as Element of G ;
(* a) . (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  y in rng (* a) by A5, FUNCT_1:def_3; ::_thesis: verum
end;
end;

theorem Th16: :: TOPGRP_1:16
for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (h *) .: P = h * P
proof
let H be non empty multMagma ; ::_thesis: for P being Subset of H
for h being Element of H holds (h *) .: P = h * P
let P be Subset of H; ::_thesis: for h being Element of H holds (h *) .: P = h * P
let h be Element of H; ::_thesis: (h *) .: P = h * P
set f = h * ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: h * P c= (h *) .: P
let y be set ; ::_thesis: ( y in (h *) .: P implies y in h * P )
assume  y in (h *) .: P ; ::_thesis: y in h * P
then consider x being set  such that
A1: x in dom (h *) and
A2: ( x in P & y = (h *) . x ) by FUNCT_1:def_6;
reconsider x = x as Element of H by A1;
 (h *) . x = h * x by Def1;
hence  y in h * P by A2, GROUP_2:27; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in h * P or y in (h *) .: P )
assume  y in h * P ; ::_thesis: 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 (h *) = the carrier of H & (h *) . s = h * s ) by Def1, FUNCT_2:def_1;
hence  y in (h *) .: P by A3, FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th17: :: TOPGRP_1:17
for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (* h) .: P = P * h
proof
let H be non empty multMagma ; ::_thesis: for P being Subset of H
for h being Element of H holds (* h) .: P = P * h
let P be Subset of H; ::_thesis: for h being Element of H holds (* h) .: P = P * h
let h be Element of H; ::_thesis: (* h) .: P = P * h
set f = * h;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: P * h c= (* h) .: P
let y be set ; ::_thesis: ( y in (* h) .: P implies y in P * h )
assume  y in (* h) .: P ; ::_thesis: y in P * h
then consider x being set  such that
A1: x in dom (* h) and
A2: ( x in P & y = (* h) . x ) by FUNCT_1:def_6;
reconsider x = x as Element of H by A1;
 (* h) . x = x * h by Def2;
hence  y in P * h by A2, GROUP_2:28; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in P * h or y in (* h) .: P )
assume  y in P * h ; ::_thesis: y in (* h) .: P
then consider s being Element of H such that
A3: ( y = s * h & s in P ) by GROUP_2:28;
 ( dom (* h) = the carrier of H & (* h) . s = s * h ) by Def2, FUNCT_2:def_1;
hence  y in (* h) .: P by A3, FUNCT_1:def_6; ::_thesis: verum
end;

theorem Th18: :: TOPGRP_1:18
for G being Group
for a being Element of G holds (a *) /" = (a ") *
proof
let G be Group; ::_thesis: for a being Element of G holds (a *) /" = (a ") *
let a be Element of G; ::_thesis: (a *) /" = (a ") *
set f = a * ;
set g = (a ") * ;
A1: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_
((a_*)_/")_._y_=_((a_")_*)_._y
reconsider h = a * as Function ;
let y be set ; ::_thesis: ( y in the carrier of G implies ((a *) /") . y = ((a ") *) . y )
assume  y in the carrier of G ; ::_thesis: ((a *) /") . y = ((a ") *) . y
then reconsider y1 = y as Element of G ;
 rng (a *) = the carrier of G by FUNCT_2:def_3;
then A2: y1 in rng (a *) ;
 dom (a *) = the carrier of G by FUNCT_2:def_1;
then A3: ( ((a ") *) . y1 in dom (a *) & ((a *) /") . y1 in dom (a *) ) ;
(a *) . (((a ") *) . y) = a * (((a ") *) . 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
.= (a *) . (((a *) /") . y) by TOPS_2:def_4 ;
hence  ((a *) /") . y = ((a ") *) . y by A3, FUNCT_1:def_4; ::_thesis: verum
end;
 ( dom ((a *) /") = the carrier of G & dom ((a ") *) = the carrier of G ) by FUNCT_2:def_1;
hence  (a *) /" = (a ") * by A1, FUNCT_1:2; ::_thesis: verum
end;

theorem Th19: :: TOPGRP_1:19
for G being Group
for a being Element of G holds (* a) /" = * (a ")
proof
let G be Group; ::_thesis: for a being Element of G holds (* a) /" = * (a ")
let a be Element of G; ::_thesis: (* a) /" = * (a ")
set f = * a;
set g = * (a ");
A1: now__::_thesis:_for_y_being_set_st_y_in_the_carrier_of_G_holds_
((*_a)_/")_._y_=_(*_(a_"))_._y
reconsider h = * a as Function ;
let y be set ; ::_thesis: ( y in the carrier of G implies ((* a) /") . y = (* (a ")) . y )
assume  y in the carrier of G ; ::_thesis: ((* a) /") . y = (* (a ")) . y
then reconsider y1 = y as Element of G ;
 rng (* a) = the carrier of G by FUNCT_2:def_3;
then A2: y1 in rng (* a) ;
 dom (* a) = the carrier of G by FUNCT_2:def_1;
then A3: ( (* (a ")) . y1 in dom (* a) & ((* a) /") . y1 in dom (* a) ) ;
(* a) . ((* (a ")) . y) = ((* (a ")) . 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
.= (* a) . (((* a) /") . y) by TOPS_2:def_4 ;
hence  ((* a) /") . y = (* (a ")) . y by A3, FUNCT_1:def_4; ::_thesis: verum
end;
 ( dom ((* a) /") = the carrier of G & dom (* (a ")) = the carrier of G ) by FUNCT_2:def_1;
hence  (* a) /" = * (a ") by A1, FUNCT_1:2; ::_thesis: verum
end;

begin

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

theorem Th20: :: TOPGRP_1:20
for T being TopStruct holds id T is being_homeomorphism
proof
let T be TopStruct ; ::_thesis: id T is being_homeomorphism
thus  ( dom (id T) = [#] T & rng (id T) = [#] T ) by RELAT_1:45; :: according to TOPS_2:def_5 ::_thesis: ( id T is one-to-one & id T is continuous & (id T) /" is continuous )
thus  ( id T is one-to-one & id T is continuous & (id T) /" is continuous ) ; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster  ->  non empty for a_neighborhood of p;
coherence
 for b1 being a_neighborhood of p holds not b1 is empty
proof
let N be a_neighborhood of p; ::_thesis: not N is empty
 p in Int N by CONNSP_2:def_1;
hence  not N is empty ; ::_thesis: verum
end;
end;

theorem Th21: :: TOPGRP_1:21
for T being non empty TopSpace
for p being Point of T holds [#] T is a_neighborhood of p
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds [#] T is a_neighborhood of p
let p be Point of T; ::_thesis: [#] T is a_neighborhood of p
 Int ([#] T) = the carrier of T by TOPS_1:15;
hence  p in Int ([#] T) ; :: according to CONNSP_2:def_1 ::_thesis: verum
end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster non empty open for a_neighborhood of p;
existence
 ex b1 being a_neighborhood of p st
( not b1 is empty & b1 is open )
proof
reconsider B = [#] T as a_neighborhood of p by Th21;
take  B ; ::_thesis: ( not B is empty & B is open )
thus  ( not B is empty & B is open ) ; ::_thesis: verum
end;
end;

theorem :: TOPGRP_1:22
for S, T being non empty TopSpace
for f being Function of S,T st f is open holds
for p being Point of S
for 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; ::_thesis: for f being Function of S,T st f is open holds
for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let f be Function of S,T; ::_thesis: ( f is open implies for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P )
assume A1: for A being Subset of S st A is open holds
f .: A is open ; :: according to T_0TOPSP:def_2 ::_thesis: for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let p be Point of S; ::_thesis: for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
let P be a_neighborhood of p; ::_thesis: ex R being open a_neighborhood of f . p st R c= f .: 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 ; ::_thesis: R c= f .: P
thus  R c= f .: P by RELAT_1:123, TOPS_1:16; ::_thesis: verum
end;

theorem :: TOPGRP_1:23
for S, T being non empty TopSpace
for f being Function of S,T st ( for p being Point of S
for 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; ::_thesis: for f being Function of S,T st ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) holds
f is open
let f be Function of S,T; ::_thesis: ( ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) implies f is open )
assume A1: for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ; ::_thesis: f is open
let A be Subset of S; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open )
assume A2: A is open ; ::_thesis: f .: 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 ; ::_thesis: ( x in f .: A iff ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) )
hereby  ::_thesis: ( ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A )
assume  x in f .: A ; ::_thesis: ex K being Element of bool the carrier of T st
( K is open & K c= f .: A & x in K )
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; ::_thesis: ( K is open & K c= f .: A & x in K )
 Int R c= R by TOPS_1:16;
then A10: K c= f .: V by A9, XBOOLE_1:1;
thus  K is open ; ::_thesis: ( K c= f .: A & x in K )
 f .: V c= f .: A by A7, RELAT_1:123;
hence  K c= f .: A by A10, XBOOLE_1:1; ::_thesis: x in K
thus  x in K by A5, CONNSP_2:def_1; ::_thesis: verum
end;
thus  ( ex Q being Subset of T st
( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; ::_thesis: verum
end;
hence  f .: A is open by TOPS_1:25; ::_thesis: verum
end;

theorem :: TOPGRP_1:24
for S, T being non empty TopStruct
for 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 ; ::_thesis: for 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 ) ) ) )
let f be Function of S,T; ::_thesis: ( 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 ) ) ) )
hereby  ::_thesis: ( 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 ) ) implies f is being_homeomorphism )
assume A1: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) ) ) )
hence A2: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of T holds
( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) )
let P be Subset of T; ::_thesis: ( ( P is closed implies f " P is closed ) & ( f " P is closed implies P is closed ) )
hereby  ::_thesis: ( f " P is closed implies P is closed )
assume A3: P is closed ; ::_thesis: f " P is closed
 f is continuous by A1, TOPS_2:def_5;
hence  f " P is closed by A3, PRE_TOPC:def_6; ::_thesis: verum
end;
assume  f " P is closed ; ::_thesis: P is closed
then  f .: (f " P) is closed by A1, TOPS_2:58;
hence  P is closed by A2, FUNCT_1:77; ::_thesis: verum
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 ) ; ::_thesis: f is being_homeomorphism
thus  ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A4, A5, A6; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f /" is continuous )
thus  f is continuous ::_thesis: f /" is continuous
proof
let P be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P is closed or f " P is closed )
thus  ( not P is closed or f " P is closed ) by A7; ::_thesis: verum
end;
let R be Subset of S; :: according to PRE_TOPC:def_6 ::_thesis: ( not R is closed or (f /") " R is closed )
assume A8: R is closed ; ::_thesis: (f /") " 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  (f /") " R is closed by A7, A8, A9; ::_thesis: verum
end;

theorem Th25: :: TOPGRP_1:25
for S, T being non empty TopStruct
for 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 ; ::_thesis: for 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 ) ) ) )
let f be Function of S,T; ::_thesis: ( 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 ) ) ) )
A1: [#] T <> {} ;
A2: [#] S <> {} ;
hereby  ::_thesis: ( 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 ) ) implies f is being_homeomorphism )
assume A3: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of S holds
( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) ) ) )
hence A4: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of S holds
( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) )
let P be Subset of S; ::_thesis: ( ( P is open implies f .: P is open ) & ( f .: P is open implies P is open ) )
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, TOPS_2:def_5;
hereby  ::_thesis: ( f .: P is open implies P is open )
assume A7: P is open ; ::_thesis: f .: P is open
 f is onto by A4, FUNCT_2:def_3;
then (f /") " P = (f ") " 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; ::_thesis: verum
end;
assume A8: f .: P is open ; ::_thesis: 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; ::_thesis: verum
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 ) ; ::_thesis: f is being_homeomorphism
now__::_thesis:_for_B_being_Subset_of_T_st_B_is_open_holds_
f_"_B_is_open
let B be Subset of T; ::_thesis: ( B is open implies f " B is open )
assume A13: B is open ; ::_thesis: f " B is open
 B = f .: (f " B) by A10, FUNCT_1:77;
hence  f " B is open by A12, A13; ::_thesis: verum
end;
then A14: f is continuous by A1, TOPS_2:43;
now__::_thesis:_for_B_being_Subset_of_S_st_B_is_open_holds_
(f_/")_"_B_is_open
let B be Subset of S; ::_thesis: ( B is open implies (f /") " B is open )
assume A15: B is open ; ::_thesis: (f /") " B is open
 f is onto by A10, FUNCT_2:def_3;
then (f /") " B = (f ") " B by A11, TOPS_2:def_4
.= f .: B by A11, FUNCT_1:84 ;
hence  (f /") " B is open by A12, A15; ::_thesis: verum
end;
then  f /" is continuous by A2, TOPS_2:43;
hence  f is being_homeomorphism by A9, A10, A11, A14, TOPS_2:def_5; ::_thesis: verum
end;

theorem :: TOPGRP_1:26
for S, T being non empty TopStruct
for 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 ; ::_thesis: for 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 ) ) ) )
let f be Function of S,T; ::_thesis: ( 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 ) ) ) )
A1: [#] T <> {} ;
hereby  ::_thesis: ( 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 ) ) implies f is being_homeomorphism )
assume A2: f is being_homeomorphism ; ::_thesis: ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) ) ) )
hence A3: ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by TOPS_2:def_5; ::_thesis: for P being Subset of T holds
( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) )
let P be Subset of T; ::_thesis: ( ( P is open implies f " P is open ) & ( f " P is open implies P is open ) )
hereby  ::_thesis: ( f " P is open implies P is open )
assume A4: P is open ; ::_thesis: f " P is open
 f is continuous by A2, TOPS_2:def_5;
hence  f " P is open by A1, A4, TOPS_2:43; ::_thesis: verum
end;
assume  f " P is open ; ::_thesis: P is open
then  f .: (f " P) is open by A2, Th25;
hence  P is open by A3, FUNCT_1:77; ::_thesis: verum
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 ) ; ::_thesis: f is being_homeomorphism
A9: now__::_thesis:_for_R_being_Subset_of_S_st_R_is_open_holds_
(f_/")_"_R_is_open
let R be Subset of S; ::_thesis: ( R is open implies (f /") " R is open )
assume A10: R is open ; ::_thesis: (f /") " 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; ::_thesis: verum
end;
thus  ( dom f = [#] S & rng f = [#] T & f is one-to-one ) by A5, A6, A7; :: according to TOPS_2:def_5 ::_thesis: ( f is continuous & f /" is continuous )
thus  f is continuous by A1, A8, TOPS_2:43; ::_thesis: f /" is continuous
 [#] S <> {} ;
hence  f /" is continuous by A9, TOPS_2:43; ::_thesis: verum
end;

theorem :: TOPGRP_1:27
for S being TopSpace
for T being non empty TopSpace
for 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; ::_thesis: for T being non empty TopSpace
for 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) )
let T be non empty TopSpace; ::_thesis: for 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) )
let f be Function of S,T; ::_thesis: ( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) )
A1: [#] T <> {} ;
hereby  ::_thesis: ( ( for P being Subset of T holds f " (Int P) c= Int (f " P) ) implies f is continuous )
assume A2: f is continuous ; ::_thesis: for P being Subset of T holds f " (Int P) c= Int (f " P)
let P be Subset of T; ::_thesis: f " (Int P) c= Int (f " P)
 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; ::_thesis: verum
end;
assume A4: for P being Subset of T holds f " (Int P) c= Int (f " P) ; ::_thesis: f is continuous
now__::_thesis:_for_P_being_Subset_of_T_st_P_is_open_holds_
f_"_P_is_open
let P be Subset of T; ::_thesis: ( P is open implies f " P is open )
assume  P is open ; ::_thesis: f " 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; ::_thesis: verum
end;
hence  f is continuous by A1, TOPS_2:43; ::_thesis: verum
end;

registration
let T be non empty TopSpace;
cluster non empty dense for Element of bool the carrier of T;
existence
 ex b1 being Subset of T st
( not b1 is empty & b1 is dense )
proof
take  [#] T ; ::_thesis: ( not [#] T is empty & [#] T is dense )
thus  ( not [#] T is empty & [#] T is dense ) ; ::_thesis: verum
end;
end;

theorem Th28: :: TOPGRP_1:28
for S, T being non empty TopSpace
for f being Function of S,T
for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T
for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
let f be Function of S,T; ::_thesis: for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
let A be dense Subset of S; ::_thesis: ( f is being_homeomorphism implies f .: A is dense )
assume A1: f is being_homeomorphism ; ::_thesis: f .: A is dense
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 ;
:: according to TOPS_1:def_3 ::_thesis: verum
end;

theorem Th29: :: TOPGRP_1:29
for S, T being non empty TopSpace
for f being Function of S,T
for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
proof
let S, T be non empty TopSpace; ::_thesis: for f being Function of S,T
for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
let f be Function of S,T; ::_thesis: for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
let A be dense Subset of T; ::_thesis: ( f is being_homeomorphism implies f " A is dense )
assume A1: f is being_homeomorphism ; ::_thesis: f " A is dense
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 ; :: according to TOPS_1:def_3 ::_thesis: verum
end;

registration
let S, T be TopStruct ;
cluster Function-like quasi_total being_homeomorphism  ->  one-to-one onto continuous for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is being_homeomorphism holds
( b1 is onto & b1 is one-to-one & b1 is continuous )
proof
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies ( f is onto & f is one-to-one & f is continuous ) )
assume A1: f is being_homeomorphism ; ::_thesis: ( f is onto & f is one-to-one & f is continuous )
then  rng f = [#] T by TOPS_2:def_5;
hence  rng f = the carrier of T ; :: according to FUNCT_2:def_3 ::_thesis: ( f is one-to-one & f is continuous )
thus  ( f is one-to-one & f is continuous ) by A1, TOPS_2:def_5; ::_thesis: verum
end;
end;

registration
let S, T be non empty TopStruct ;
cluster Function-like quasi_total being_homeomorphism  ->  open for Element of bool [: the carrier of S, the carrier of T:];
coherence
 for b1 being Function of S,T st b1 is being_homeomorphism holds
b1 is open
proof
let f be Function of S,T; ::_thesis: ( f is being_homeomorphism implies f is open )
assume A1: f is being_homeomorphism ; ::_thesis: f is open
let A be Subset of S; :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open )
thus  ( not A is open or f .: A is open ) by A1, Th25; ::_thesis: verum
end;
end;

registration
let T be TopStruct ;
cluster Relation-like the carrier of T -defined the carrier of T -valued Function-like V14( the carrier of T) quasi_total being_homeomorphism for Element of bool [: the carrier of T, the carrier of T:];
existence
 ex b1 being Function of T,T st b1 is being_homeomorphism
proof
take  id T ; ::_thesis: id T is being_homeomorphism
thus  id T is being_homeomorphism by Th20; ::_thesis: verum
end;
end;

registration
let T be TopStruct ;
let f be being_homeomorphism Function of T,T;
clusterf /"  ->  being_homeomorphism ;
coherence
 f /" is being_homeomorphism
proof
percases ( not T is empty or T is empty ) ;
suppose not T is empty ; ::_thesis: f /" is being_homeomorphism
hence  f /" is being_homeomorphism by TOPS_2:56; ::_thesis: verum
end;
suppose T is empty ; ::_thesis: f /" is being_homeomorphism
then A1: the carrier of T is empty ;
f /" = f " by TOPS_2:def_4
.= id T by A1, RELAT_1:55 ;
hence  f /" is being_homeomorphism by Th20; ::_thesis: verum
end;
end;
end;
end;

begin

definition
let S, T be TopStruct ;
assume A1: S,T are_homeomorphic ;
mode Homeomorphism of S,T ->  Function of S,T means :Def3: :: TOPGRP_1:def 3
it is being_homeomorphism ;
existence
 ex b1 being Function of S,T st b1 is being_homeomorphism by A1, T_0TOPSP:def_1;
end;

:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def_3_:_
 for S, T being TopStruct st S,T are_homeomorphic holds
for b3 being Function of S,T holds
( b3 is Homeomorphism of S,T iff b3 is being_homeomorphism );

definition
let T be TopStruct ;
mode Homeomorphism of T ->  Function of T,T means :Def4: :: TOPGRP_1:def 4
it is being_homeomorphism ;
existence
 ex b1 being Function of T,T st b1 is being_homeomorphism
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  ex b1 being Function of T,T st b1 is being_homeomorphism ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def_4_:_
 for T being TopStruct
for b2 being Function of T,T holds
( b2 is Homeomorphism of T iff b2 is being_homeomorphism );

definition
let T be TopStruct ;
:: original: Homeomorphism
redefine mode Homeomorphism of T ->  Homeomorphism of T,T;
coherence
 for b1 being Homeomorphism of T holds b1 is Homeomorphism of T,T
proof
let f be Homeomorphism of T; ::_thesis: f is Homeomorphism of T,T
A1: f is being_homeomorphism by Def4;
then  T,T are_homeomorphic by T_0TOPSP:def_1;
hence  f is Homeomorphism of T,T by A1, Def3; ::_thesis: verum
end;
end;

definition
let T be TopStruct ;
:: original: id
redefine func id T ->  Homeomorphism of T,T;
coherence
 id T is Homeomorphism of T,T
proof
 id T is being_homeomorphism by Th20;
hence  T,T are_homeomorphic by T_0TOPSP:def_1; :: according to TOPGRP_1:def_3 ::_thesis: id T is being_homeomorphism
thus  id T is being_homeomorphism by Th20; ::_thesis: verum
end;
end;

definition
let T be TopStruct ;
:: original: id
redefine func id T ->  Homeomorphism of T;
coherence
 id T is Homeomorphism of T
proof
thus  id T is being_homeomorphism by Th20; :: according to TOPGRP_1:def_4 ::_thesis: verum
end;
end;

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

theorem Th30: :: TOPGRP_1:30
for T being TopStruct
for f being Homeomorphism of T holds f /" is Homeomorphism of T
proof
let T be TopStruct ; ::_thesis: for f being Homeomorphism of T holds f /" is Homeomorphism of T
let f be Homeomorphism of T; ::_thesis: f /" is Homeomorphism of T
thus  f /" is being_homeomorphism ; :: according to TOPGRP_1:def_4 ::_thesis: verum
end;

Lm2:  for T being TopStruct
for f being Function of T,T st T is empty holds
f is being_homeomorphism
proof
let T be TopStruct ; ::_thesis: for f being Function of T,T st T is empty holds
f is being_homeomorphism
let f be Function of T,T; ::_thesis: ( T is empty implies f is being_homeomorphism )
assume A1: T is empty ; ::_thesis: f is being_homeomorphism
then f = {}
.= id T by A1 ;
hence  f is being_homeomorphism ; ::_thesis: verum
end;

theorem Th31: :: TOPGRP_1:31
for T being TopStruct
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
proof
let T be TopStruct ; ::_thesis: for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
let f, g be Homeomorphism of T; ::_thesis: f * g is Homeomorphism of T
 ( not T is empty or T is empty ) ;
hence  f * g is being_homeomorphism by TOPS_2:57; :: according to TOPGRP_1:def_4 ::_thesis: verum
end;

definition
let T be TopStruct ;
func HomeoGroup T ->  strict multMagma  means :Def5: :: TOPGRP_1:def 5
 for x being set holds
( ( x in the carrier of it implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of it ) & ( for f, g being Homeomorphism of T holds the multF of it . (f,g) = g * f ) );
existence
 ex b1 being strict multMagma st
for x being set holds
( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) )
proof
defpred S1[ 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) & S1[q] ) ) from XBOOLE_0:sch_1();
A2: now__::_thesis:_for_f_being_Homeomorphism_of_T_holds_f_in_A
let f be Homeomorphism of T; ::_thesis: f in A
 f in Funcs ( the carrier of T, the carrier of T) by FUNCT_2:9;
hence  f in A by A1; ::_thesis: verum
end;
then reconsider A = A as non empty set ;
defpred S2[ 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 S2[x,y,z]
proof
let x, y be Element of A; ::_thesis: ex z being Element of A st S2[x,y,z]
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 ; ::_thesis: S2[x,y,z]
take  x1 ; ::_thesis: ex g being Homeomorphism of T st
( x = x1 & y = g & z = g * x1 )
take  y1 ; ::_thesis: ( x = x1 & y = y1 & z = y1 * x1 )
thus  ( x = x1 & y = y1 & z = y1 * x1 ) ; ::_thesis: verum
end;
consider o being BinOp of A such that
A4: for a, b being Element of A holds S2[a,b,o . (a,b)] from BINOP_1:sch_3(A3);
take G = multMagma(# A,o #); ::_thesis: for x being set holds
( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) )
let x be set ; ::_thesis: ( ( x in the carrier of G implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of G ) & ( for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f ) )
thus  ( x in the carrier of G iff x is Homeomorphism of T ) by A1, A2; ::_thesis: for f, g being Homeomorphism of T holds the multF of G . (f,g) = g * f
let f, g be Homeomorphism of T; ::_thesis: the multF of G . (f,g) = g * f
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  the multF of G . (f,g) = g * f ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being strict multMagma st ( for x being set holds
( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) ) ) & ( for x being set holds
( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) ) holds
b1 = b2
proof
defpred S1[ set ] means $1 is Homeomorphism of T;
let A, B be strict multMagma ; ::_thesis: ( ( for x being set holds
( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . (f,g) = g * f ) ) ) & ( for x being set holds
( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . (f,g) = g * f ) ) ) implies A = B )
assume that
A5: for x being set holds
( ( x in the carrier of A implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of A ) & ( for f, g being Homeomorphism of T holds the multF of A . (f,g) = g * f ) ) and
A6: for x being set holds
( ( x in the carrier of B implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of B ) & ( for f, g being Homeomorphism of T holds the multF of B . (f,g) = g * f ) ) ; ::_thesis: A = B
A7: for x being set holds
( x in the carrier of B iff S1[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 ; ::_thesis: ( c in the carrier of A & d in the carrier of A implies the multF of A . (c,d) = the multF of B . (c,d) )
assume  ( c in the carrier of A & d in the carrier of A ) ; ::_thesis: the multF of A . (c,d) = the multF of B . (c,d)
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 ; ::_thesis: verum
end;
A9: for x being set holds
( x in the carrier of A iff S1[x] ) by A5;
 the carrier of A = the carrier of B from XBOOLE_0:sch_2(A9, A7);
hence  A = B by A8, BINOP_1:1; ::_thesis: verum
end;
end;

:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def_5_:_
 for T being TopStruct
for b2 being strict multMagma holds
( b2 = HomeoGroup T iff for x being set holds
( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) );

registration
let T be TopStruct ;
cluster HomeoGroup T ->  non empty strict ;
coherence
 not HomeoGroup T is empty
proof
 id T is Homeomorphism of T ;
hence  not the carrier of (HomeoGroup T) is empty by Def5; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

theorem :: TOPGRP_1:32
for T being TopStruct
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 ->  strict Group-like associative ;
coherence
 ( HomeoGroup T is Group-like & HomeoGroup T is associative )
proof
set G = HomeoGroup T;
set o = the multF of (HomeoGroup T);
thus  HomeoGroup T is Group-like ::_thesis: HomeoGroup T is associative
proof
reconsider e = id T as Element of (HomeoGroup T) by Def5;
take  e ; :: according to GROUP_1:def_2 ::_thesis: for b1 being Element of the carrier of (HomeoGroup T) holds
( b1 * e = b1 & e * b1 = b1 & ex b2 being Element of the carrier of (HomeoGroup T) st
( b1 * b2 = e & b2 * b1 = e ) )
let h be Element of (HomeoGroup T); ::_thesis: ( h * e = h & e * h = h & ex b1 being Element of the carrier of (HomeoGroup T) st
( h * b1 = e & b1 * h = e ) )
reconsider h1 = h, e1 = e as Homeomorphism of T by Def5;
thus h * e = e1 * h1 by Def5
.= h by FUNCT_2:17 ; ::_thesis: ( e * h = h & ex b1 being Element of the carrier of (HomeoGroup T) st
( h * b1 = e & b1 * h = e ) )
thus e * h = h1 * e1 by Def5
.= h by FUNCT_2:17 ; ::_thesis: ex b1 being Element of the carrier of (HomeoGroup T) st
( h * b1 = e & b1 * h = e )
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 (HomeoGroup T) by Def5;
reconsider g1 = g as Homeomorphism of T by Def5;
take  g ; ::_thesis: ( h * g = e & g * h = e )
A2: rng h1 = [#] T by TOPS_2:def_5;
thus h * g = g1 * h1 by Def5
.= e by A1, A2, TOPS_2:52 ; ::_thesis: g * h = e
thus g * h = h1 * g1 by Def5
.= e by A2, TOPS_2:52 ; ::_thesis: verum
end;
let x, y, z be Element of (HomeoGroup T); :: according to GROUP_1:def_3 ::_thesis: (x * y) * z = x * (y * z)
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 = the multF of (HomeoGroup T) . ((g * f),z) by Def5
.= r * p by Def5
.= (r * g) * f by RELAT_1:36
.= the multF of (HomeoGroup T) . (f,a) by Def5
.= x * (y * z) by Def5 ; ::_thesis: verum
end;
end;

theorem Th33: :: TOPGRP_1:33
for T being TopStruct holds id T = 1_ (HomeoGroup T)
proof
let T be TopStruct ; ::_thesis: id T = 1_ (HomeoGroup T)
set G = HomeoGroup T;
reconsider e = id T as Element of (HomeoGroup T) by Def5;
now__::_thesis:_for_h_being_Element_of_(HomeoGroup_T)_holds_
(_h_*_e_=_h_&_e_*_h_=_h_)
let h be Element of (HomeoGroup T); ::_thesis: ( h * e = h & e * h = h )
reconsider h1 = h as Homeomorphism of T by Def5;
thus h * e = (id T) * h1 by Def5
.= h by FUNCT_2:17 ; ::_thesis: e * h = h
thus e * h = h1 * (id T) by Def5
.= h by FUNCT_2:17 ; ::_thesis: verum
end;
hence  id T = 1_ (HomeoGroup T) by GROUP_1:4; ::_thesis: verum
end;

theorem :: TOPGRP_1:34
for T being TopStruct
for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
proof
let T be TopStruct ; ::_thesis: for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
let f be Homeomorphism of T; ::_thesis: for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
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 (HomeoGroup T) by Def5;
A3: rng f = [#] T by TOPS_2:def_5;
let a be Element of (HomeoGroup T); ::_thesis: ( f = a implies a " = f /" )
assume A4: f = a ; ::_thesis: a " = f /"
A5: g * a = f * (f /") by A4, A2, Def5
.= id T by A3, TOPS_2:52
.= 1_ (HomeoGroup T) by Th33 ;
a * g = (f /") * f by A4, A2, Def5
.= id T by A1, A3, TOPS_2:52
.= 1_ (HomeoGroup T) by Th33 ;
hence  a " = f /" by A5, GROUP_1:5; ::_thesis: verum
end;

definition
let T be TopStruct ;
attrT is homogeneous  means :Def6: :: TOPGRP_1:def 6
 for p, q being Point of T ex f being Homeomorphism of T st f . p = q;
end;

:: deftheorem Def6 defines homogeneous TOPGRP_1:def_6_:_
 for T being TopStruct holds
( T is homogeneous iff for p, q being Point of T ex f being Homeomorphism of T st f . p = q );

registration
cluster1 -element  -> 1 -element homogeneous for TopStruct ;
coherence
 for b1 being 1 -element TopStruct holds b1 is homogeneous
proof
let T be 1 -element TopStruct ; ::_thesis: T is homogeneous
let p, q be Point of T; :: according to TOPGRP_1:def_6 ::_thesis: ex f being Homeomorphism of T st f . p = q
take  id T ; ::_thesis: (id T) . p = q
thus  (id T) . p = q by STRUCT_0:def_10; ::_thesis: verum
end;
end;

theorem :: TOPGRP_1:35
for T being non empty homogeneous TopSpace st ex p being Point of T st {p} is closed holds
T is T_1
proof
let T be non empty homogeneous TopSpace; ::_thesis: ( ex p being Point of T st {p} is closed implies T is T_1 )
given p being Point of T such that A1: {p} is closed ; ::_thesis: T is T_1
now__::_thesis:_for_q_being_Point_of_T_holds_{q}_is_closed
let q be Point of T; ::_thesis: {q} is closed
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; ::_thesis: verum
end;
hence  T is T_1 by URYSOHN1:19; ::_thesis: verum
end;

theorem Th36: :: TOPGRP_1:36
for T being non empty homogeneous 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 non empty homogeneous TopSpace; ::_thesis: ( 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 ) implies T is regular )
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 ) ; ::_thesis: T is regular
A2: [#] T <> {} ;
now__::_thesis:_for_A_being_open_Subset_of_T
for_q_being_Point_of_T_st_q_in_A_holds_
ex_fB_being_open_Subset_of_T_st_
(_q_in_fB_&_Cl_fB_c=_A_)
let A be open Subset of T; ::_thesis: for q being Point of T st q in A holds
ex fB being open Subset of T st
( q in fB & Cl fB c= A )
let q be Point of T; ::_thesis: ( q in A implies ex fB being open Subset of T st
( q in fB & Cl fB c= A ) )
assume A3: q in A ; ::_thesis: ex fB being open Subset of T st
( q in fB & Cl fB c= 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 = fB; ::_thesis: ( q in fB & Cl fB c= A )
thus  q in fB by A4, A6, A9, FUNCT_1:def_6; ::_thesis: Cl fB c= A
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; ::_thesis: verum
end;
hence  T is regular by URYSOHN1:21; ::_thesis: verum
end;

begin

definition
attrc1 is strict ;
struct TopGrStr  ->  multMagma , TopStruct ;
aggrTopGrStr(# carrier, multF, topology #) ->  TopGrStr ;
end;

registration
let A be non empty set ;
let R be BinOp of A;
let T be Subset-Family of A;
cluster TopGrStr(# A,R,T #) ->  non empty ;
coherence
 not TopGrStr(# A,R,T #) is empty ;
end;

registration
let x be set ;
let R be BinOp of {x};
let T be Subset-Family of {x};
cluster TopGrStr(# {x},R,T #) ->  trivial ;
coherence
 TopGrStr(# {x},R,T #) is trivial ;
end;

registration
cluster1 -element  -> 1 -element Group-like associative commutative for multMagma ;
coherence
 for b1 being 1 -element multMagma holds
( b1 is Group-like & b1 is associative & b1 is commutative )
proof
let H be 1 -element multMagma ; ::_thesis: ( H is Group-like & H is associative & H is commutative )
hereby  :: according to GROUP_1:def_2 ::_thesis: ( H is associative & H is commutative )
set e = the Element of H;
take e = the Element of H; ::_thesis: for h being Element of H holds
( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
let h be Element of H; ::_thesis: ( h * e = h & e * h = h & ex g being Element of H st
( h * g = e & g * h = e ) )
thus  ( h * e = h & e * h = h ) by STRUCT_0:def_10; ::_thesis: ex g being Element of H st
( h * g = e & g * h = e )
take g = e; ::_thesis: ( h * g = e & g * h = e )
thus  ( h * g = e & g * h = e ) by STRUCT_0:def_10; ::_thesis: verum
end;
thus  for x, y, z being Element of H holds (x * y) * z = x * (y * z) by STRUCT_0:def_10; :: according to GROUP_1:def_3 ::_thesis: H is commutative
let x, y be Element of H; :: according to GROUP_1:def_12 ::_thesis: x * y = y * x
thus  x * y = y * x by STRUCT_0:def_10; ::_thesis: verum
end;
end;

registration
let a be set ;
cluster 1TopSp {a} ->  trivial ;
coherence
 1TopSp {a} is trivial ;
end;

registration
cluster non empty strict for TopGrStr ;
existence
 ex b1 being TopGrStr st
( b1 is strict & not b1 is empty )
proof
set R = the BinOp of {{}};
set T = the Subset-Family of {{}};
take  TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) ; ::_thesis: ( TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty )
thus  ( TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is strict & not TopGrStr(# {{}}, the BinOp of {{}}, the Subset-Family of {{}} #) is empty ) ; ::_thesis: verum
end;
end;

registration
cluster1 -element TopSpace-like strict for TopGrStr ;
existence
 ex b1 being TopGrStr st
( b1 is strict & b1 is TopSpace-like & b1 is 1 -element )
proof
set R = the BinOp of {{}};
take  TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) ; ::_thesis: ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element )
 the carrier of (1TopSp {{}}) is 1 -element ;
hence  ( TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is strict & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is TopSpace-like & TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) is 1 -element ) by TEX_2:7; ::_thesis: verum
end;
end;

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

:: deftheorem Def7 defines UnContinuous TOPGRP_1:def_7_:_
 for G being non empty Group-like associative TopGrStr holds
( G is UnContinuous iff inverse_op G is continuous );

definition
let G be TopSpace-like TopGrStr ;
attrG is BinContinuous  means :Def8: :: TOPGRP_1:def 8
 for f being Function of [:G,G:],G st f = the multF of G holds
f is continuous ;
end;

:: deftheorem Def8 defines BinContinuous TOPGRP_1:def_8_:_
 for G being TopSpace-like TopGrStr holds
( G is BinContinuous iff for f being Function of [:G,G:],G st f = the multF of G holds
f is continuous );

registration
cluster non empty trivial V43() 1 -element TopSpace-like compact unital Group-like associative commutative homogeneous strict UnContinuous BinContinuous for TopGrStr ;
existence
 ex b1 being 1 -element TopSpace-like Group-like associative TopGrStr st
( b1 is strict & b1 is commutative & b1 is UnContinuous & b1 is BinContinuous )
proof
set R = the BinOp of {{}};
 1TopSp {{}} is 1 -element ;
then reconsider T = TopGrStr(# {{}}, the BinOp of {{}},(bool {{}}) #) as 1 -element TopSpace-like strict TopGrStr by TEX_2:7;
take  T ; ::_thesis: ( T is strict & T is commutative & T is UnContinuous & T is BinContinuous )
thus  ( T is strict & T is commutative ) ; ::_thesis: ( T is UnContinuous & T is BinContinuous )
hereby  :: according to TOPGRP_1:def_7 ::_thesis: T is BinContinuous
set f = inverse_op T;
thus  inverse_op T is continuous ::_thesis: verum
proof
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or (inverse_op T) " P1 is closed )
assume  P1 is closed ; ::_thesis: (inverse_op T) " P1 is closed
percases ( (inverse_op T) " P1 = {} or (inverse_op T) " P1 = {{}} ) by ZFMISC_1:33;
suppose (inverse_op T) " P1 = {} ; ::_thesis: (inverse_op T) " P1 is closed
hence  (inverse_op T) " P1 is closed ; ::_thesis: verum
end;
suppose (inverse_op T) " P1 = {{}} ; ::_thesis: (inverse_op T) " P1 is closed
then  (inverse_op T) " P1 = [#] T ;
hence  (inverse_op T) " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;
let f be Function of [:T,T:],T; :: according to TOPGRP_1:def_8 ::_thesis: ( f = the multF of T implies f is continuous )
assume  f = the multF of T ; ::_thesis: f is continuous
A1: the carrier of [:T,T:] = [:{{}},{{}}:] by BORSUK_1:def_2
.= {[{},{}]} by ZFMISC_1:29 ;
let P1 be Subset of T; :: according to PRE_TOPC:def_6 ::_thesis: ( not P1 is closed or f " P1 is closed )
assume  P1 is closed ; ::_thesis: f " P1 is closed
percases ( f " P1 = {} or f " P1 = {[{},{}]} ) by A1, ZFMISC_1:33;
suppose f " P1 = {} ; ::_thesis: f " P1 is closed
hence  f " P1 is closed ; ::_thesis: verum
end;
suppose f " P1 = {[{},{}]} ; ::_thesis: f " P1 is closed
then  f " P1 = [#] [:T,T:] by A1;
hence  f " P1 is closed ; ::_thesis: verum
end;
end;
end;
end;

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

definition
mode TopologicalGroup is UnContinuous BinContinuous TopGroup;
end;

theorem Th37: :: TOPGRP_1:37
for T being non empty TopSpace-like BinContinuous TopGrStr
for a, b being Element of T
for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
proof
let T be non empty TopSpace-like BinContinuous TopGrStr ; ::_thesis: for a, b being Element of T
for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
let W be a_neighborhood of a * b; ::_thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
 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 holds
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 = B as open a_neighborhood of b by A8, CONNSP_2:def_1;
reconsider A = A as open a_neighborhood of a by A7, A9, CONNSP_2:def_1;
take  A ; ::_thesis: ex B being open a_neighborhood of b st A * B c= W
take  B ; ::_thesis: A * B c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B or x in W )
assume  x in A * B ; ::_thesis: x in W
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  x in W by A1; ::_thesis: verum
end;

theorem Th38: :: TOPGRP_1:38
for T being non empty TopSpace-like TopGrStr st ( for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) holds
T is BinContinuous
proof
let T be non empty TopSpace-like TopGrStr ; ::_thesis: ( ( for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) implies T is BinContinuous )
assume A1: for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ; ::_thesis: T is BinContinuous
let f be Function of [:T,T:],T; :: according to TOPGRP_1:def_8 ::_thesis: ( f = the multF of T implies f is continuous )
assume A2: f = the multF of T ; ::_thesis: f is continuous
 for W being Point of [:T,T:]
for 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:]; ::_thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; ::_thesis: ex H being a_neighborhood of W st f .: H c= G
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 ; ::_thesis: f .: H c= G
thus  f .: H c= G by A2, A4, Th15; ::_thesis: verum
end;
hence  f is continuous by BORSUK_1:def_1; ::_thesis: verum
end;

theorem Th39: :: TOPGRP_1:39
for T being UnContinuous TopGroup
for a being Element of T
for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
proof
let T be UnContinuous TopGroup; ::_thesis: for a being Element of T
for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
let a be Element of T; ::_thesis: for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
let W be a_neighborhood of a " ; ::_thesis: ex A being open a_neighborhood of a st A " c= W
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 ; ::_thesis: A " c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A " or x in W )
assume  x in A " ; ::_thesis: x in W
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  x in W by A1, A2; ::_thesis: verum
end;

theorem Th40: :: TOPGRP_1:40
for T being TopGroup st ( for a being Element of T
for 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; ::_thesis: ( ( for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ) implies T is UnContinuous )
assume A1: for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ; ::_thesis: T is UnContinuous
set f = inverse_op T;
 for W being Point of T
for G being a_neighborhood of (inverse_op T) . W ex H being a_neighborhood of W st (inverse_op T) .: H c= G
proof
let a be Point of T; ::_thesis: for G being a_neighborhood of (inverse_op T) . a ex H being a_neighborhood of a st (inverse_op T) .: H c= G
let G be a_neighborhood of (inverse_op T) . a; ::_thesis: ex H being a_neighborhood of a st (inverse_op T) .: H c= G
 (inverse_op T) . 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 ; ::_thesis: (inverse_op T) .: A c= G
thus  (inverse_op T) .: A c= G by A2, Th10; ::_thesis: verum
end;
hence  inverse_op T is continuous by BORSUK_1:def_1; :: according to TOPGRP_1:def_7 ::_thesis: verum
end;

theorem Th41: :: TOPGRP_1:41
for T being TopologicalGroup
for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
proof
let T be TopologicalGroup; ::_thesis: for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
let W be a_neighborhood of a * (b "); ::_thesis: ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
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 ; ::_thesis: ex B being open a_neighborhood of b st A * (B ") c= W
take  C ; ::_thesis: A * (C ") c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * (C ") or x in W )
assume  x in A * (C ") ; ::_thesis: x in W
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  x in W by A1, A3, A6; ::_thesis: verum
end;

theorem :: TOPGRP_1:42
for T being TopGroup st ( for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) holds
T is TopologicalGroup
proof
let T be TopGroup; ::_thesis: ( ( for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) implies T is TopologicalGroup )
assume A1: for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ; ::_thesis: T is TopologicalGroup
A2: for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W
proof
let a be Element of T; ::_thesis: for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W
let W be a_neighborhood of a " ; ::_thesis: ex A being a_neighborhood of a st A " c= W
 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 ; ::_thesis: B " c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B " or x in W )
assume A4: x in B " ; ::_thesis: x in W
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  x in W by A3, A5; ::_thesis: verum
end;
 for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
proof
let a, b be Element of T; ::_thesis: for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
let W be a_neighborhood of a * b; ::_thesis: ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W
 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 ; ::_thesis: ex B being a_neighborhood of b st A * B c= W
take  B1 ; ::_thesis: A * B1 c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * B1 or x in W )
assume  x in A * B1 ; ::_thesis: x in W
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  x in W by A6; ::_thesis: verum
end;
hence  T is TopologicalGroup by A2, Th38, Th40; ::_thesis: verum
end;

registration
let G be non empty TopSpace-like BinContinuous TopGrStr ;
let a be Element of G;
clustera *  ->  continuous ;
coherence
 a * is continuous
proof
set f = a * ;
 for w being Point of G
for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A
proof
let w be Point of G; ::_thesis: for A being a_neighborhood of (a *) . w ex W being a_neighborhood of w st (a *) .: W c= A
let A be a_neighborhood of (a *) . w; ::_thesis: ex W being a_neighborhood of w st (a *) .: W c= A
 (a *) . 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 ; ::_thesis: (a *) .: W c= A
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in (a *) .: W or k in A )
assume  k in (a *) .: W ; ::_thesis: k in A
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  k in A by A1; ::_thesis: verum
end;
hence  a * is continuous by BORSUK_1:def_1; ::_thesis: verum
end;
cluster * a ->  continuous ;
coherence
 * a is continuous
proof
set f = * a;
 for w being Point of G
for A being a_neighborhood of (* a) . w ex W being a_neighborhood of w st (* a) .: W c= A
proof
let w be Point of G; ::_thesis: for A being a_neighborhood of (* a) . w ex W being a_neighborhood of w st (* a) .: W c= A
let A be a_neighborhood of (* a) . w; ::_thesis: ex W being a_neighborhood of w st (* a) .: W c= A
 (* a) . 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 ; ::_thesis: (* a) .: W c= A
let k be set ; :: according to TARSKI:def_3 ::_thesis: ( not k in (* a) .: W or k in A )
assume  k in (* a) .: W ; ::_thesis: k in A
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  k in A by A3; ::_thesis: verum
end;
hence  * a is continuous by BORSUK_1:def_1; ::_thesis: verum
end;
end;

theorem Th43: :: TOPGRP_1:43
for G being BinContinuous TopGroup
for a being Element of G holds a * is Homeomorphism of G
proof
let G be BinContinuous TopGroup; ::_thesis: for a being Element of G holds a * is Homeomorphism of G
let a be Element of G; ::_thesis: a * is Homeomorphism of G
set f = a * ;
thus  ( dom (a *) = [#] G & rng (a *) = [#] G & a * is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( a * is continuous & (a *) /" is continuous )
thus  a * is continuous ; ::_thesis: (a *) /" is continuous
 (a *) /" = (a ") * by Th18;
hence  (a *) /" is continuous ; ::_thesis: verum
end;

theorem Th44: :: TOPGRP_1:44
for G being BinContinuous TopGroup
for a being Element of G holds * a is Homeomorphism of G
proof
let G be BinContinuous TopGroup; ::_thesis: for a being Element of G holds * a is Homeomorphism of G
let a be Element of G; ::_thesis: * a is Homeomorphism of G
set f = * a;
thus  ( dom (* a) = [#] G & rng (* a) = [#] G & * a is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( * a is continuous & (* a) /" is continuous )
thus  * a is continuous ; ::_thesis: (* a) /" is continuous
 (* a) /" = * (a ") by Th19;
hence  (* a) /" is continuous ; ::_thesis: verum
end;

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

theorem Th45: :: TOPGRP_1:45
for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G
proof
let G be UnContinuous TopGroup; ::_thesis: inverse_op G is Homeomorphism of G
set f = inverse_op G;
thus  ( dom (inverse_op G) = [#] G & rng (inverse_op G) = [#] G & inverse_op G is one-to-one ) by FUNCT_2:def_1, FUNCT_2:def_3; :: according to TOPS_2:def_5,TOPGRP_1:def_4 ::_thesis: ( inverse_op G is continuous & (inverse_op G) /" is continuous )
thus  inverse_op G is continuous by Def7; ::_thesis: (inverse_op G) /" is continuous
inverse_op G = (inverse_op G) " by Th14
.= (inverse_op G) /" by TOPS_2:def_4 ;
hence  (inverse_op G) /" is continuous by Def7; ::_thesis: verum
end;

definition
let G be UnContinuous TopGroup;
:: original: inverse_op
redefine func inverse_op G ->  Homeomorphism of G;
coherence
 inverse_op G is Homeomorphism of G by Th45;
end;

registration
cluster non empty TopSpace-like Group-like associative BinContinuous  ->  homogeneous for TopGrStr ;
coherence
 for b1 being TopGroup st b1 is BinContinuous holds
b1 is homogeneous
proof
let T be TopGroup; ::_thesis: ( T is BinContinuous implies T is homogeneous )
assume  T is BinContinuous ; ::_thesis: T is homogeneous
then reconsider G = T as BinContinuous TopGroup ;
 G is homogeneous
proof
let p, q be Point of G; :: according to TOPGRP_1:def_6 ::_thesis: ex f being Homeomorphism of G st f . p = q
take  * ((p ") * q) ; ::_thesis: (* ((p ") * q)) . 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 ; ::_thesis: verum
end;
hence  T is homogeneous ; ::_thesis: verum
end;
end;

theorem Th46: :: TOPGRP_1:46
for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds F * a is closed
proof
let G be BinContinuous TopGroup; ::_thesis: for F being closed Subset of G
for a being Element of G holds F * a is closed
let F be closed Subset of G; ::_thesis: for a being Element of G holds F * a is closed
let a be Element of G; ::_thesis: F * a is closed
 F * a = (* a) .: F by Th17;
hence  F * a is closed by TOPS_2:58; ::_thesis: verum
end;

theorem Th47: :: TOPGRP_1:47
for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds a * F is closed
proof
let G be BinContinuous TopGroup; ::_thesis: for F being closed Subset of G
for a being Element of G holds a * F is closed
let F be closed Subset of G; ::_thesis: for a being Element of G holds a * F is closed
let a be Element of G; ::_thesis: a * F is closed
 a * F = (a *) .: F by Th16;
hence  a * F is closed by TOPS_2:58; ::_thesis: verum
end;

registration
let G be BinContinuous TopGroup;
let F be closed Subset of G;
let a be Element of G;
clusterF * a ->  closed ;
coherence
 F * a is closed by Th46;
clustera * F ->  closed ;
coherence
 a * F is closed by Th47;
end;

theorem Th48: :: TOPGRP_1:48
for G being UnContinuous TopGroup
for F being closed Subset of G holds F " is closed
proof
let G be UnContinuous TopGroup; ::_thesis: for F being closed Subset of G holds F " is closed
let F be closed Subset of G; ::_thesis: F " is closed
 F " = (inverse_op G) .: F by Th10;
hence  F " is closed by TOPS_2:58; ::_thesis: verum
end;

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

theorem Th49: :: TOPGRP_1:49
for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds O * a is open
proof
let G be BinContinuous TopGroup; ::_thesis: for O being open Subset of G
for a being Element of G holds O * a is open
let O be open Subset of G; ::_thesis: for a being Element of G holds O * a is open
let a be Element of G; ::_thesis: O * a is open
 O * a = (* a) .: O by Th17;
hence  O * a is open by Th25; ::_thesis: verum
end;

theorem Th50: :: TOPGRP_1:50
for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds a * O is open
proof
let G be BinContinuous TopGroup; ::_thesis: for O being open Subset of G
for a being Element of G holds a * O is open
let O be open Subset of G; ::_thesis: for a being Element of G holds a * O is open
let a be Element of G; ::_thesis: a * O is open
 a * O = (a *) .: O by Th16;
hence  a * O is open by Th25; ::_thesis: verum
end;

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

theorem Th51: :: TOPGRP_1:51
for G being UnContinuous TopGroup
for O being open Subset of G holds O " is open
proof
let G be UnContinuous TopGroup; ::_thesis: for O being open Subset of G holds O " is open
let O be open Subset of G; ::_thesis: O " is open
 O " = (inverse_op G) .: O by Th10;
hence  O " is open by Th25; ::_thesis: verum
end;

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

theorem Th52: :: TOPGRP_1:52
for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
O * A is open
proof
let G be BinContinuous TopGroup; ::_thesis: for A, O being Subset of G st O is open holds
O * A is open
let A, O be Subset of G; ::_thesis: ( O is open implies O * A is open )
assume A1: O is open ; ::_thesis: O * A is open
 Int (O * A) = O * A
proof
thus  Int (O * A) c= O * A by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: O * A c= Int (O * A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O * A or x in Int (O * A) )
assume  x in O * A ; ::_thesis: x in Int (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: O * a c= O * A
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in O * a or q in O * A )
assume  q in O * a ; ::_thesis: q in O * A
then  ex h being Element of G st
( q = h * a & h in O ) by GROUP_2:28;
hence  q in O * A by A3; ::_thesis: verum
end;
 x in O * a by A2, GROUP_2:28;
hence  x in Int (O * A) by A1, A4, TOPS_1:22; ::_thesis: verum
end;
hence  O * A is open ; ::_thesis: verum
end;

theorem Th53: :: TOPGRP_1:53
for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
A * O is open
proof
let G be BinContinuous TopGroup; ::_thesis: for A, O being Subset of G st O is open holds
A * O is open
let A, O be Subset of G; ::_thesis: ( O is open implies A * O is open )
assume A1: O is open ; ::_thesis: A * O is open
 Int (A * O) = A * O
proof
thus  Int (A * O) c= A * O by TOPS_1:16; :: according to XBOOLE_0:def_10 ::_thesis: A * O c= Int (A * O)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A * O or x in Int (A * O) )
assume  x in A * O ; ::_thesis: x in Int (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: a * O c= A * O
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in a * O or q in A * O )
assume  q in a * O ; ::_thesis: q in A * O
then  ex h being Element of G st
( q = a * h & h in O ) by GROUP_2:27;
hence  q in A * O by A3; ::_thesis: verum
end;
 x in a * O by A2, A4, GROUP_2:27;
hence  x in Int (A * O) by A1, A5, TOPS_1:22; ::_thesis: verum
end;
hence  A * O is open ; ::_thesis: verum
end;

registration
let G be BinContinuous TopGroup;
let A be open Subset of G;
let B be Subset of G;
clusterA * B ->  open ;
coherence
 A * B is open by Th52;
clusterB * A ->  open ;
coherence
 B * A is open by Th53;
end;

theorem Th54: :: TOPGRP_1:54
for G being UnContinuous TopGroup
for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "
proof
let G be UnContinuous TopGroup; ::_thesis: for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "
let a be Point of G; ::_thesis: for A being a_neighborhood of a holds A " is a_neighborhood of a "
let A be a_neighborhood of a; ::_thesis: A " is 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; :: according to CONNSP_2:def_1 ::_thesis: verum
end;

theorem Th55: :: TOPGRP_1:55
for G being TopologicalGroup
for a being Point of G
for 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; ::_thesis: for a being Point of G
for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A
let a be Point of G; ::_thesis: for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A
let A be a_neighborhood of a * (a "); ::_thesis: ex B being open a_neighborhood of a st B * (B ") c= 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 ; ::_thesis: B * (B ") c= A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B * (B ") or x in A )
assume  x in B * (B ") ; ::_thesis: x in A
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  x in A by A1; ::_thesis: verum
end;

theorem Th56: :: TOPGRP_1:56
for G being UnContinuous TopGroup
for A being dense Subset of G holds A " is dense
proof
let G be UnContinuous TopGroup; ::_thesis: for A being dense Subset of G holds A " is dense
let A be dense Subset of G; ::_thesis: A " is dense
 (inverse_op G) " A = A " by Th11;
hence  A " is dense by Th29; ::_thesis: verum
end;

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

theorem Th57: :: TOPGRP_1:57
for G being BinContinuous TopGroup
for A being dense Subset of G
for a being Point of G holds a * A is dense
proof
let G be BinContinuous TopGroup; ::_thesis: for A being dense Subset of G
for a being Point of G holds a * A is dense
let A be dense Subset of G; ::_thesis: for a being Point of G holds a * A is dense
let a be Point of G; ::_thesis: a * A is dense
 (a *) .: A = a * A by Th16;
hence  a * A is dense by Th28; ::_thesis: verum
end;

theorem Th58: :: TOPGRP_1:58
for G being BinContinuous TopGroup
for A being dense Subset of G
for a being Point of G holds A * a is dense
proof
let G be BinContinuous TopGroup; ::_thesis: for A being dense Subset of G
for a being Point of G holds A * a is dense
let A be dense Subset of G; ::_thesis: for a being Point of G holds A * a is dense
let a be Point of G; ::_thesis: A * a is dense
 (* a) .: A = A * a by Th17;
hence  A * a is dense by Th28; ::_thesis: verum
end;

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

theorem :: TOPGRP_1:59
for G being TopologicalGroup
for B being Basis of 1_ G
for 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; ::_thesis: for B being Basis of 1_ G
for 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
let B be Basis of 1_ G; ::_thesis: for 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
let M be dense Subset of G; ::_thesis:  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  is Basis of G
set Z =  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  ;
A1:  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  c= the topology of G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  or a in the topology of G )
assume  a in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  ; ::_thesis: a in the topology of G
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 = V as Subset of G ;
 V is open by A3, YELLOW_8:12;
hence  a in the topology of G by A2, PRE_TOPC:def_2; ::_thesis: verum
end;
A4: for W being Subset of G st W is open holds
for a being Point of G st a in W holds
ex V being Subset of G st
( V in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  & 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; ::_thesis: ( W is open implies for a being Point of G st a in W holds
ex V being Subset of G st
( V in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  & a in V & V c= W ) )
assume A6: W is open ; ::_thesis: for a being Point of G st a in W holds
ex V being Subset of G st
( V in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  & a in V & V c= W )
let a be Point of G; ::_thesis: ( a in W implies ex V being Subset of G st
( V in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  & a in V & V c= W ) )
assume A7: a in W ; ::_thesis: ex V being Subset of G st
( V in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  & a in V & V c= 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 = d as Point of G by A11;
take I = E * ((d ") * a); ::_thesis: ( I in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  & a in I & I c= W )
 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  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  by A9; ::_thesis: ( a in I & I c= W )
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 ; :: according to TARSKI:def_3 ::_thesis: ( not q in E * (d ") or q in V * (V ") )
assume  q in E * (d ") ; ::_thesis: q in V * (V ")
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  q in V * (V ") by A10, A16; ::_thesis: verum
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; ::_thesis: I c= W
(W * (a ")) * a = W * ((a ") * a) by GROUP_2:34
.= W * (1_ G) by GROUP_1:def_5
.= W by GROUP_2:37 ;
hence  I c= W by A17, GROUP_2:34; ::_thesis: verum
end;
  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  c= bool the carrier of G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  or a in bool the carrier of G )
assume  a in  {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  ; ::_thesis: a in bool the carrier of G
then  ex V being Subset of G ex x being Point of G st
( a = V * x & V in B & x in M ) ;
hence  a in bool the carrier of G ; ::_thesis: verum
end;
hence   {  (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M )  }  is Basis of G by A1, A4, YELLOW_9:32; ::_thesis: verum
end;

theorem Th60: :: TOPGRP_1:60
for G being TopologicalGroup holds G is regular
proof
let G be TopologicalGroup; ::_thesis: G is regular
 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  1_ G ; ::_thesis: for A being Subset of G st A is open & 1_ G in A holds
ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A )
let A be Subset of G; ::_thesis: ( A is open & 1_ G in A implies ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A ) )
assume  ( A is open & 1_ G in A ) ; ::_thesis: ex B being Subset of G st
( 1_ G in B & B is open & Cl B c= A )
then  1_ G in Int A by TOPS_1:23;
then A1: A is a_neighborhood of 1_ G by CONNSP_2:def_1;
 1_ G = (1_ G) * ((1_ G) ") by GROUP_1:def_5;
then consider C being open a_neighborhood of 1_ G, B being open a_neighborhood of (1_ G) "  such that
A2: C * B c= A by A1, Th37;
 ((1_ G) ") " = 1_ G ;
then  B " is a_neighborhood of 1_ G by Th54;
then reconsider W = C /\ (B ") as a_neighborhood of 1_ G 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 ; ::_thesis: ( 1_ G in W & W is open & Cl W c= A )
 Int W = W by TOPS_1:23;
hence A4: ( 1_ G in W & W is open ) by CONNSP_2:def_1; ::_thesis: Cl W c= A
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in Cl W or p in A )
assume A5: p in Cl W ; ::_thesis: p in A
then reconsider r = p as Point of G ;
 r = r * (1_ G) 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 = 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 * (1_ G) 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  p in A by A3; ::_thesis: verum
end;
hence  G is regular by Th36; ::_thesis: verum
end;

registration
cluster non empty TopSpace-like Group-like associative UnContinuous BinContinuous  ->  regular for TopGrStr ;
coherence
 for b1 being TopologicalGroup holds b1 is regular by Th60;
end;

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