:: The Definition and Basic Properties of Topological Groups
:: by Artur Korni{\l}owicz
::
:: Received September 7, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

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 b₁ being Function of X,X st
( b₁ is one-to-one & b₁ is onto )

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

end;

theorem Th2: :: TOPGRP_1:2

for R being 1-sorted holds (id R) /" = id R

proof end;

theorem :: TOPGRP_1:3

for R being 1-sorted
for X being Subset of R holds (id R) " X = X

proof 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

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

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

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

Lm1: for G being Group
for A, B being Subset of G st A c= B holds
A " c= B "

proof end;

theorem :: TOPGRP_1:8

canceled;

::$CT

theorem Th8: :: TOPGRP_1:9

for G being Group
for A, B being Subset of G holds
( A c= B iff A " c= B " )

proof end;

theorem Th9: :: TOPGRP_1:10

for G being Group
for A being Subset of G holds (inverse_op G) .: A = A "

proof end;

theorem Th10: :: TOPGRP_1:11

for G being Group
for A being Subset of G holds (inverse_op G) " A = A "

proof end;

theorem Th11: :: TOPGRP_1:12

for G being Group holds inverse_op G is one-to-one

proof end;

theorem Th12: :: TOPGRP_1:13

for G being Group holds rng (inverse_op G) = the carrier of G

proof 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 ) by Th11, Th12;

end;

theorem Th13: :: TOPGRP_1:14

for G being Group holds (inverse_op G) " = inverse_op G

proof end;

theorem Th14: :: 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 end;

definition

let G be non empty multMagma ;
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
ex b₁ being Function of G,G st
for x being Element of G holds b₁ . x = a * x

proof end;

uniqueness
for b₁, b₂ being Function of G,G st ( for x being Element of G holds b₁ . x = a * x ) & ( for x being Element of G holds b₂ . x = a * x ) holds
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
ex b₁ being Function of G,G st
for x being Element of G holds b₁ . x = x * a

proof end;

uniqueness
for b₁, b₂ being Function of G,G st ( for x being Element of G holds b₁ . x = x * a ) & ( for x being Element of G holds b₂ . x = x * a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines * TOPGRP_1:def 1 :
for G being non empty multMagma
for a being Element of G
for b₃ being Function of G,G holds
( b₃ = a * iff for x being Element of G holds b₃ . x = a * x );

:: deftheorem Def2 defines * TOPGRP_1:def 2 :
for G being non empty multMagma
for a being Element of G
for b₃ being Function of G,G holds
( b₃ = * a iff for x being Element of G holds b₃ . x = x * a );

registration

let G be Group;
let a be Element of G;

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

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

proof end;

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

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

proof end;

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

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

proof end;

theorem Th17: :: TOPGRP_1:18

for G being Group
for a being Element of G holds (a *) /" = (a ") *

proof end;

theorem Th18: :: TOPGRP_1:19

for G being Group
for a being Element of G holds (* a) /" = * (a ")

proof end;

registration

let T be TopStruct ;

cluster (id T) /" -> continuous ;

coherence
(id T) /" is continuous by Th2;

end;

theorem Th19: :: TOPGRP_1:20

for T being TopStruct holds id T is being_homeomorphism by RELAT_1:45;

registration

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

cluster -> non empty for a_neighborhood of p;

coherence
for b₁ being a_neighborhood of p holds not b₁ is empty

proof end;

end;

theorem Th20: :: TOPGRP_1:21

for T being non empty TopSpace
for p being Point of T holds [#] T is a_neighborhood of p

proof 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 b₁ being a_neighborhood of p st
( not b₁ is empty & b₁ is open )

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

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

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

proof end;

registration

let T be non empty TopSpace;

cluster non empty dense for Element of bool the carrier of T;

existence
ex b₁ being Subset of T st
( not b₁ is empty & b₁ is dense )

proof end;

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

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

proof 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 b₁ being Function of S,T st b₁ is being_homeomorphism holds
( b₁ is onto & b₁ is one-to-one & b₁ is continuous ) ;

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 b₁ being Function of S,T st b₁ is being_homeomorphism holds
b₁ is open by Th24;

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 b₁ being Function of T,T st b₁ is being_homeomorphism

proof end;

end;

registration

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

cluster f /" -> being_homeomorphism ;

coherence
f /" is being_homeomorphism

proof end;

end;

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 b₁ being Function of S,T st b₁ is being_homeomorphism by A1;

end;

:: deftheorem Def3 defines Homeomorphism TOPGRP_1:def 3 :
for S, T being TopStruct st S,T are_homeomorphic holds
for b₃ being Function of S,T holds
( b₃ is Homeomorphism of S,T iff b₃ 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 b₁ being Function of T,T st b₁ is being_homeomorphism

proof end;

end;

:: deftheorem Def4 defines Homeomorphism TOPGRP_1:def 4 :
for T being TopStruct
for b₂ being Function of T,T holds
( b₂ is Homeomorphism of T iff b₂ is being_homeomorphism );

definition

let T be TopStruct ;
:: original: Homeomorphism
redefine mode Homeomorphism of T -> Homeomorphism of T,T;
coherence
for b₁ being Homeomorphism of T holds b₁ is Homeomorphism of T,T

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

end;

definition

let T be TopStruct ;
:: original: id
redefine func id T -> Homeomorphism of T;
coherence
id T is Homeomorphism of T

proof end;

end;

registration

let T be TopStruct ;

cluster -> being_homeomorphism for Homeomorphism of T;

coherence
for b₁ being Homeomorphism of T holds b₁ is being_homeomorphism by Def4;

end;

theorem Th29: :: TOPGRP_1:30

for T being TopStruct
for f being Homeomorphism of T holds f /" is Homeomorphism of T

proof end;

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

proof end;

theorem Th30: :: TOPGRP_1:31

for T being TopStruct
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T

proof 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 b₁ being strict multMagma st
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 ) )

proof end;

uniqueness
for b₁, b₂ being strict multMagma st ( 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 ) ) ) & ( 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 ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines HomeoGroup TOPGRP_1:def 5 :
for T being TopStruct
for b₂ being strict multMagma holds
( b₂ = HomeoGroup T iff 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 ) ) );

registration

let T be TopStruct ;

cluster HomeoGroup T -> non empty strict ;

coherence
not HomeoGroup T is empty

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

end;

theorem Th32: :: TOPGRP_1:33

for T being TopStruct holds id T = 1_ (HomeoGroup T)

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

proof end;

definition

let T be TopStruct ;

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;

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

cluster 1 -element -> 1 -element homogeneous for TopStruct ;

coherence
for b₁ being 1 -element TopStruct holds b₁ is homogeneous

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

proof end;

definition

attr c₁ is strict ;
struct TopGrStr -> multMagma , TopStruct ;
aggr TopGrStr(# 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

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

coherence
for b₁ being 1 -element multMagma holds
( b₁ is Group-like & b₁ is associative & b₁ is commutative )

proof 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 b₁ being TopGrStr st
( b₁ is strict & not b₁ is empty )

proof end;

end;

registration

cluster 1 -element TopSpace-like strict for TopGrStr ;

existence
ex b₁ being TopGrStr st
( b₁ is strict & b₁ is TopSpace-like & b₁ is 1 -element )

proof end;

end;

:: definition
:: let G be Group;
:: redefine func inverse_op G -> Function of G, G;
:: coherence;
:: end;

definition

let G be non empty Group-like associative TopGrStr ;

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

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 ;

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 V46() 1 -element TopSpace-like compact unital Group-like associative commutative homogeneous strict UnContinuous BinContinuous for TopGrStr ;

existence
ex b₁ being 1 -element TopSpace-like Group-like associative TopGrStr st
( b₁ is strict & b₁ is commutative & b₁ is UnContinuous & b₁ is BinContinuous )

proof end;

end;

definition

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

end;

definition

mode TopologicalGroup is UnContinuous BinContinuous TopGroup;

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

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

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

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

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

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

proof end;

registration

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

cluster a * -> continuous ;

coherence
a * is continuous

proof end;

cluster * a -> continuous ;

coherence
* a is continuous

proof end;

end;

theorem Th42: :: TOPGRP_1:43

for G being BinContinuous TopGroup
for a being Element of G holds a * is Homeomorphism of G

proof end;

theorem Th43: :: TOPGRP_1:44

for G being BinContinuous TopGroup
for a being Element of G holds * a is Homeomorphism of G

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;

theorem Th44: :: TOPGRP_1:45

for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G

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

end;

registration

cluster non empty TopSpace-like Group-like associative BinContinuous -> homogeneous for TopGrStr ;

coherence
for b₁ being TopGroup st b₁ is BinContinuous holds
b₁ is homogeneous

proof end;

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

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

proof end;

registration

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

cluster F * a -> closed ;

coherence
F * a is closed by Th45;

cluster a * F -> closed ;

coherence
a * F is closed by Th46;

end;

theorem Th47: :: TOPGRP_1:48

for G being UnContinuous TopGroup
for F being closed Subset of G holds F " is closed

proof end;

registration

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

cluster F " -> closed ;

coherence
F " is closed by Th47;

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

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

proof end;

registration

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

cluster A * a -> open ;

coherence
A * a is open by Th48;

cluster a * A -> open ;

coherence
a * A is open by Th49;

end;

theorem Th50: :: TOPGRP_1:51

for G being UnContinuous TopGroup
for O being open Subset of G holds O " is open

proof end;

registration

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

cluster A " -> open ;

coherence
A " is open by Th50;

end;

theorem Th51: :: 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 end;

theorem Th52: :: 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 end;

registration

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

cluster A * B -> open ;

coherence
A * B is open by Th51;

cluster B * A -> open ;

coherence
B * A is open by Th52;

end;

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 "

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

proof end;

theorem Th55: :: TOPGRP_1:56

for G being UnContinuous TopGroup
for A being dense Subset of G holds A " is dense

proof end;

registration

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

cluster A " -> dense ;

coherence
A " is dense by Th55;

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

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

proof end;

registration

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

cluster A * a -> dense ;

coherence
A * a is dense by Th57;

cluster a * A -> dense ;

coherence
a * A is dense by Th56;

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

theorem Th59: :: TOPGRP_1:60

for G being TopologicalGroup holds G is regular

proof end;

registration

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

coherence
for b₁ being TopologicalGroup holds b₁ is regular by Th59;

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;