:: by Artur Korni{\l}owicz

::

:: Received September 7, 1998

:: Copyright (c) 1998-2018 Association of Mizar Users

registration

let X be set ;

ex b_{1} being Function of X,X st

( b_{1} is one-to-one & b_{1} is onto )

end;
cluster Relation-like X -defined X -valued Function-like one-to-one V14(X) quasi_total onto for Function of ,;

existence ex b

( b

proof end;

registration
end;

theorem Th4: :: TOPGRP_1:4

for H being non empty multMagma

for P, Q, P1, Q1 being Subset of H st P c= P1 & Q c= Q1 holds

P * Q c= P1 * Q1

for P, Q, P1, Q1 being Subset of H st P c= P1 & Q c= Q1 holds

P * Q c= P1 * Q1

proof 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

for P, Q being Subset of H

for h being Element of H st P c= Q holds

P * h c= Q * h

proof 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

for P, Q being Subset of H

for h being Element of H st P c= Q holds

h * P c= h * Q

proof end;

Lm1: for G being Group

for A, B being Subset of G st A c= B holds

A " c= B "

proof end;

::$CT

registration
end;

definition

let G be non empty multMagma ;

let a be Element of G;

ex b_{1} being Function of G,G st

for x being Element of G holds b_{1} . x = a * x

for b_{1}, b_{2} being Function of G,G st ( for x being Element of G holds b_{1} . x = a * x ) & ( for x being Element of G holds b_{2} . x = a * x ) holds

b_{1} = b_{2}

ex b_{1} being Function of G,G st

for x being Element of G holds b_{1} . x = x * a

for b_{1}, b_{2} being Function of G,G st ( for x being Element of G holds b_{1} . x = x * a ) & ( for x being Element of G holds b_{2} . x = x * a ) holds

b_{1} = b_{2}

end;
let a be Element of G;

func a * -> Function of G,G means :Def1: :: TOPGRP_1:def 1

for x being Element of G holds it . x = a * x;

existence for x being Element of G holds it . x = a * x;

ex b

for x being Element of G holds b

proof end;

uniqueness for b

b

proof 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 for x being Element of G holds it . x = x * a;

ex b

for x being Element of G holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def1 defines * TOPGRP_1:def 1 :

for G being non empty multMagma

for a being Element of G

for b_{3} being Function of G,G holds

( b_{3} = a * iff for x being Element of G holds b_{3} . x = a * x );

for G being non empty multMagma

for a being Element of G

for b

( b

:: deftheorem Def2 defines * TOPGRP_1:def 2 :

for G being non empty multMagma

for a being Element of G

for b_{3} being Function of G,G holds

( b_{3} = * a iff for x being Element of G holds b_{3} . x = x * a );

for G being non empty multMagma

for a being Element of G

for b

( b

registration

let G be Group;

let a be Element of G;

coherence

( a * is one-to-one & a * is onto )

( * a is one-to-one & * a is onto )

end;
let a be Element of G;

coherence

( a * is one-to-one & a * is onto )

proof end;

coherence ( * a is one-to-one & * a is onto )

proof end;

theorem Th15: :: 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

for P being Subset of H

for h being Element of H holds (h *) .: P = h * P

proof end;

theorem Th16: :: 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

for P being Subset of H

for h being Element of H holds (* h) .: P = P * h

proof end;

registration
end;

registration

let T be non empty TopSpace;

let p be Point of T;

coherence

for b_{1} being a_neighborhood of p holds not b_{1} is empty

end;
let p be Point of T;

coherence

for b

proof end;

registration

let T be non empty TopSpace;

let p be Point of T;

existence

ex b_{1} being a_neighborhood of p st

( not b_{1} is empty & b_{1} is open )

end;
let p be Point of T;

existence

ex b

( not b

proof 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

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 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

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 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 ) ) ) )

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 end;

theorem Th24: :: 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 ) ) ) )

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 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 ) ) ) )

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 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) )

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 end;

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset of T st

( not b_{1} is empty & b_{1} is dense )

end;
existence

ex b

( not b

proof end;

theorem Th27: :: 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

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 end;

theorem Th28: :: 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

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 end;

registration

let S, T be TopStruct ;

for b_{1} being Function of S,T st b_{1} is being_homeomorphism holds

( b_{1} is onto & b_{1} is one-to-one & b_{1} is continuous )
;

end;
cluster Function-like quasi_total being_homeomorphism -> one-to-one onto continuous for Function of ,;

coherence for b

( b

registration

let S, T be non empty TopStruct ;

coherence

for b_{1} being Function of S,T st b_{1} is being_homeomorphism holds

b_{1} is open
by Th24;

end;
coherence

for b

b

registration

let T be TopStruct ;

ex b_{1} being Function of T,T st b_{1} is being_homeomorphism

end;
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 Function of ,;

existence ex b

proof end;

registration

let T be TopStruct ;

let f be being_homeomorphism Function of T,T;

coherence

f /" is being_homeomorphism

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

coherence

f /" is being_homeomorphism

proof end;

definition

let S, T be TopStruct ;

assume A1: S,T are_homeomorphic ;

ex b_{1} being Function of S,T st b_{1} is being_homeomorphism
by A1;

end;
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 it is being_homeomorphism ;

ex b

:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :

for S, T being TopStruct st S,T are_homeomorphic holds

for b_{3} being Function of S,T holds

( b_{3} is Homeomorphism of S,T iff b_{3} is being_homeomorphism );

for S, T being TopStruct st S,T are_homeomorphic holds

for b

( b

definition

let T be TopStruct ;

ex b_{1} being Function of T,T st b_{1} is being_homeomorphism

end;
mode Homeomorphism of T -> Function of T,T means :Def4: :: TOPGRP_1:def 4

it is being_homeomorphism ;

existence it is being_homeomorphism ;

ex b

proof end;

:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def 4 :

for T being TopStruct

for b_{2} being Function of T,T holds

( b_{2} is Homeomorphism of T iff b_{2} is being_homeomorphism );

for T being TopStruct

for b

( b

definition

let T be TopStruct ;

:: original: Homeomorphism

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

coherence

for b_{1} being Homeomorphism of T holds b_{1} is Homeomorphism of T,T

end;
:: original: Homeomorphism

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

coherence

for b

proof end;

definition

let T be TopStruct ;

:: original: id

redefine func id T -> Homeomorphism of T,T;

coherence

id T is Homeomorphism of T,T

end;
:: original: id

redefine func id T -> Homeomorphism of T,T;

coherence

id T is Homeomorphism of T,T

proof end;

definition

let T be TopStruct ;

:: original: id

redefine func id T -> Homeomorphism of T;

coherence

id T is Homeomorphism of T

end;
:: original: id

redefine func id T -> Homeomorphism of T;

coherence

id T is Homeomorphism of T

proof end;

registration

let T be TopStruct ;

coherence

for b_{1} being Homeomorphism of T holds b_{1} is being_homeomorphism
by Def4;

end;
coherence

for b

Lm2: for T being TopStruct

for f being Function of T,T st T is empty holds

f is being_homeomorphism

proof end;

definition

let T be TopStruct ;

ex b_{1} being strict multMagma st

for x being set holds

( ( x in the carrier of b_{1} implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b_{1} ) & ( for f, g being Homeomorphism of T holds the multF of b_{1} . (f,g) = g * f ) )

for b_{1}, b_{2} being strict multMagma st ( for x being set holds

( ( x in the carrier of b_{1} implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b_{1} ) & ( for f, g being Homeomorphism of T holds the multF of b_{1} . (f,g) = g * f ) ) ) & ( for x being set holds

( ( x in the carrier of b_{2} implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b_{2} ) & ( for f, g being Homeomorphism of T holds the multF of b_{2} . (f,g) = g * f ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) );

ex b

for x being set holds

( ( x in the carrier of b

proof end;

uniqueness for b

( ( x in the carrier of b

( ( x in the carrier of b

b

proof end;

:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def 5 :

for T being TopStruct

for b_{2} being strict multMagma holds

( b_{2} = HomeoGroup T iff for x being set holds

( ( x in the carrier of b_{2} implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b_{2} ) & ( for f, g being Homeomorphism of T holds the multF of b_{2} . (f,g) = g * f ) ) );

for T being TopStruct

for b

( b

( ( x in the carrier of b

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;

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 ;

coherence

( HomeoGroup T is Group-like & HomeoGroup T is associative )

end;
coherence

( HomeoGroup T is Group-like & HomeoGroup T is associative )

proof 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 /"

for f being Homeomorphism of T

for a being Element of (HomeoGroup T) st f = a holds

a " = f /"

proof end;

definition

let T be TopStruct ;

end;
attr T 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;

for p, q being Point of T ex f being Homeomorphism of T st f . p = q;

:: 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 );

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
end;

theorem Th35: :: 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

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 end;

definition

attr c_{1} is strict ;

struct TopGrStr -> multMagma , TopStruct ;

aggr TopGrStr(# carrier, multF, topology #) -> TopGrStr ;

end;
struct TopGrStr -> multMagma , TopStruct ;

aggr TopGrStr(# carrier, multF, topology #) -> TopGrStr ;

registration

let A be non empty set ;

let R be BinOp of A;

let T be Subset-Family of A;

coherence

not TopGrStr(# A,R,T #) is empty ;

end;
let R be BinOp of A;

let T be Subset-Family of A;

coherence

not TopGrStr(# A,R,T #) is empty ;

registration

let x be set ;

let R be BinOp of {x};

let T be Subset-Family of {x};

coherence

TopGrStr(# {x},R,T #) is trivial ;

end;
let R be BinOp of {x};

let T be Subset-Family of {x};

coherence

TopGrStr(# {x},R,T #) is trivial ;

registration

coherence

for b_{1} being 1 -element multMagma holds

( b_{1} is Group-like & b_{1} is associative & b_{1} is commutative )

end;
for b

( b

proof end;

registration
end;

registration

existence

ex b_{1} being TopGrStr st

( b_{1} is strict & b_{1} is TopSpace-like & b_{1} is 1 -element )

end;
ex b

( b

proof end;

:: definition

:: let G be Group;

:: redefine func inverse_op G -> Function of G, G;

:: coherence;

:: end;

:: let G be Group;

:: redefine func inverse_op G -> Function of G, G;

:: coherence;

:: 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 );

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 ;

end;
attr G 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 ;

for f being Function of [:G,G:],G st f = the multF of G holds

f is continuous ;

:: 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 );

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

ex b_{1} being 1 -element TopSpace-like Group-like associative TopGrStr st

( b_{1} is strict & b_{1} is commutative & b_{1} is UnContinuous & b_{1} is BinContinuous )
end;

cluster non empty trivial V46() 1 -element TopSpace-like compact unital Group-like associative commutative homogeneous strict UnContinuous BinContinuous for TopGrStr ;

existence ex b

( b

proof end;

theorem Th36: :: 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

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 end;

theorem Th37: :: 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

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 end;

theorem Th38: :: 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

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 end;

theorem Th39: :: 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

for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ) holds

T is UnContinuous

proof end;

theorem Th40: :: 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

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 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

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 end;

registration

let G be non empty TopSpace-like BinContinuous TopGrStr ;

let a be Element of G;

coherence

a * is continuous

* a is continuous

end;
let a be Element of G;

coherence

a * is continuous

proof end;

coherence * a is continuous

proof end;

definition

let G be BinContinuous TopGroup;

let a be Element of G;

:: original: *

redefine func a * -> Homeomorphism of G;

coherence

a * is Homeomorphism of G by Th42;

:: original: *

redefine func * a -> Homeomorphism of G;

coherence

* a is Homeomorphism of G by Th43;

end;
let a be Element of G;

:: original: *

redefine func a * -> Homeomorphism of G;

coherence

a * is Homeomorphism of G by Th42;

:: original: *

redefine func * a -> Homeomorphism of G;

coherence

* a is Homeomorphism of G by Th43;

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 Th44;

end;
:: original: inverse_op

redefine func inverse_op G -> Homeomorphism of G;

coherence

inverse_op G is Homeomorphism of G by Th44;

registration
end;

theorem Th45: :: 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

for F being closed Subset of G

for a being Element of G holds F * a is closed

proof end;

theorem Th46: :: 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

for F being closed Subset of G

for a being Element of G holds a * F is closed

proof end;

registration

let G be BinContinuous TopGroup;

let F be closed Subset of G;

let a be Element of G;

coherence

F * a is closed by Th45;

coherence

a * F is closed by Th46;

end;
let F be closed Subset of G;

let a be Element of G;

coherence

F * a is closed by Th45;

coherence

a * F is closed by Th46;

registration
end;

theorem Th48: :: 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

for O being open Subset of G

for a being Element of G holds O * a is open

proof end;

theorem Th49: :: 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

for O being open Subset of G

for a being Element of G holds a * O is open

proof end;

registration

let G be BinContinuous TopGroup;

let A be open Subset of G;

let a be Element of G;

coherence

A * a is open by Th48;

coherence

a * A is open by Th49;

end;
let A be open Subset of G;

let a be Element of G;

coherence

A * a is open by Th48;

coherence

a * A is open by Th49;

registration
end;

registration

let G be BinContinuous TopGroup;

let A be open Subset of G;

let B be Subset of G;

coherence

A * B is open by Th51;

coherence

B * A is open by Th52;

end;
let A be open Subset of G;

let B be Subset of G;

coherence

A * B is open by Th51;

coherence

B * A is open by Th52;

theorem Th53: :: 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 "

for a being Point of G

for A being a_neighborhood of a holds A " is a_neighborhood of a "

proof end;

theorem Th54: :: 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

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 end;

registration
end;

theorem Th56: :: 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

for A being dense Subset of G

for a being Point of G holds a * A is dense

proof end;

theorem Th57: :: 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

for A being dense Subset of G

for a being Point of G holds A * a is dense

proof end;

registration

let G be BinContinuous TopGroup;

let A be dense Subset of G;

let a be Point of G;

coherence

A * a is dense by Th57;

coherence

a * A is dense by Th56;

end;
let A be dense Subset of G;

let a be Point of G;

coherence

A * a is dense by Th57;

coherence

a * A is dense by Th56;

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

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 end;

registration

for b_{1} being TopologicalGroup holds b_{1} is regular
by Th59;

end;

cluster non empty TopSpace-like Group-like associative UnContinuous BinContinuous -> regular for TopologicalGroup;

coherence for b

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;

for f being Function of T,T st T is empty holds

f is being_homeomorphism by Lm2;