:: TOPGRP_1 semantic presentation
begin
registration
let
X
be ( ( ) ( )
set
) ;
cluster
Relation-like
X
: ( ( ) ( )
set
)
-defined
X
: ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
(
X
: ( ( ) ( )
set
) )
quasi_total
onto
for ( ( ) ( )
Element
of
bool
[:
X
: ( ( ) ( )
set
) ,
X
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGRP_1:1
for
S
being ( ( ) ( )
1-sorted
) holds
rng
(
id
S
: ( ( ) ( )
1-sorted
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
S
: ( ( ) ( )
1-sorted
) : ( ( ) ( non
proper
)
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
registration
let
R
be ( ( ) ( )
1-sorted
) ;
cluster
(
id
R
: ( ( ) ( )
1-sorted
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
/"
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
R
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
->
Function-like
one-to-one
quasi_total
;
end;
theorem
:: TOPGRP_1:2
for
R
being ( ( ) ( )
1-sorted
) holds
(
id
R
: ( ( ) ( )
1-sorted
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
/"
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
=
id
R
: ( ( ) ( )
1-sorted
) : ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:3
for
R
being ( ( ) ( )
1-sorted
)
for
X
being ( ( ) ( )
Subset
of ) holds
(
id
R
: ( ( ) ( )
1-sorted
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
"
X
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( ) ( )
1-sorted
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
=
X
: ( ( ) ( )
Subset
of ) ;
begin
theorem
:: TOPGRP_1:4
for
H
being ( ( non
empty
) ( non
empty
)
multMagma
)
for
P
,
P1
,
Q
,
Q1
being ( ( ) ( )
Subset
of ) st
P
: ( ( ) ( )
Subset
of )
c=
P1
: ( ( ) ( )
Subset
of ) &
Q
: ( ( ) ( )
Subset
of )
c=
Q1
: ( ( ) ( )
Subset
of ) holds
P
: ( ( ) ( )
Subset
of )
*
Q
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
P1
: ( ( ) ( )
Subset
of )
*
Q1
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:5
for
H
being ( ( non
empty
) ( non
empty
)
multMagma
)
for
P
,
Q
being ( ( ) ( )
Subset
of )
for
h
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
P
: ( ( ) ( )
Subset
of )
c=
Q
: ( ( ) ( )
Subset
of ) holds
P
: ( ( ) ( )
Subset
of )
*
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
Q
: ( ( ) ( )
Subset
of )
*
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:6
for
H
being ( ( non
empty
) ( non
empty
)
multMagma
)
for
P
,
Q
being ( ( ) ( )
Subset
of )
for
h
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
P
: ( ( ) ( )
Subset
of )
c=
Q
: ( ( ) ( )
Subset
of ) holds
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
Q
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:7
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
for
A
being ( ( ) ( )
Subset
of )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) iff
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) ) ;
theorem
:: TOPGRP_1:8
canceled;
theorem
:: TOPGRP_1:9
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
for
A
,
B
being ( ( ) ( )
Subset
of ) holds
(
A
: ( ( ) ( )
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) iff
A
: ( ( ) ( )
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
B
: ( ( ) ( )
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPGRP_1:10
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
.:
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
A
: ( ( ) ( )
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:11
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
for
A
being ( ( ) ( )
Subset
of ) holds
(
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
"
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
A
: ( ( ) ( )
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:12
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) holds
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
one-to-one
;
theorem
:: TOPGRP_1:13
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) holds
rng
(
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) ;
registration
let
G
be ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) ;
cluster
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
Function-like
one-to-one
quasi_total
onto
;
end;
theorem
:: TOPGRP_1:14
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) holds
(
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
"
: ( (
Function-like
quasi_total
bijective
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
inverse_op
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:15
for
H
being ( ( non
empty
) ( non
empty
)
multMagma
)
for
P
,
Q
being ( ( ) ( )
Subset
of ) holds the
multF
of
H
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
[:
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
[:
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
.:
[:
P
: ( ( ) ( )
Subset
of ) ,
Q
: ( ( ) ( )
Subset
of )
:]
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
P
: ( ( ) ( )
Subset
of )
*
Q
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
G
be ( ( non
empty
) ( non
empty
)
multMagma
) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
func
a
*
->
( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) )
means
:: TOPGRP_1:def 1
for
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
it
: ( (
Function-like
quasi_total
) (
Relation-like
[:
G
: ( ( ) ( )
set
) ,
G
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
G
: ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
G
: ( ( ) ( )
set
) ,
G
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
G
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
.
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
a
: ( ( ) ( )
set
)
*
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
func
*
a
->
( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) )
means
:: TOPGRP_1:def 2
for
x
being ( ( ) ( )
Element
of ( ( ) ( )
set
) ) holds
it
: ( (
Function-like
quasi_total
) (
Relation-like
[:
G
: ( ( ) ( )
set
) ,
G
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
G
: ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
G
: ( ( ) ( )
set
) ,
G
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) ,
G
: ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
.
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
) )
=
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of the
carrier
of
G
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ) ;
end;
registration
let
G
be ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
*
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
one-to-one
quasi_total
onto
;
cluster
*
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
one-to-one
quasi_total
onto
;
end;
theorem
:: TOPGRP_1:16
for
H
being ( ( non
empty
) ( non
empty
)
multMagma
)
for
P
being ( ( ) ( )
Subset
of )
for
h
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.:
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:17
for
H
being ( ( non
empty
) ( non
empty
)
multMagma
)
for
P
being ( ( ) ( )
Subset
of )
for
h
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
*
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.:
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
P
: ( ( ) ( )
Subset
of )
*
h
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
multMagma
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:18
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
/"
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
*
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:19
for
G
being ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
/"
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
*
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
Group
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) ;
begin
registration
let
T
be ( ( ) ( )
TopStruct
) ;
cluster
(
id
T
: ( ( ) ( )
TopStruct
)
)
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
continuous
open
)
Element
of
bool
[:
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
/"
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
continuous
;
end;
theorem
:: TOPGRP_1:20
for
T
being ( ( ) ( )
TopStruct
) holds
id
T
: ( ( ) ( )
TopStruct
) : ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
continuous
open
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
p
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
->
non
empty
for ( ( ) ( )
a_neighborhood
of
p
: ( ( ) ( )
set
) ) ;
end;
theorem
:: TOPGRP_1:21
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
[#]
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
non
proper
open
closed
dense
non
boundary
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( non
empty
)
a_neighborhood
of
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
let
p
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
non
empty
open
for ( ( ) ( )
a_neighborhood
of
p
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) ) ;
end;
theorem
:: TOPGRP_1:22
for
S
,
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) st
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
open
holds
for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
P
being ( ( ) ( non
empty
)
a_neighborhood
of
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ex
R
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ) st
R
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
3
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.
b
4
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) )
c=
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.:
P
: ( ( ) ( non
empty
)
a_neighborhood
of
b
4
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:23
for
S
,
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) st ( for
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
P
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) ex
R
being ( ( ) ( non
empty
)
a_neighborhood
of
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) ) st
R
: ( ( ) ( non
empty
)
a_neighborhood
of
b
3
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.
b
4
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) ) )
c=
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.:
P
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
4
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
open
;
theorem
:: TOPGRP_1:24
for
S
,
T
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) holds
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
iff (
dom
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
S
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
non
proper
dense
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
rng
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
non
proper
dense
)
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
one-to-one
& ( for
P
being ( ( ) ( )
Subset
of ) holds
(
P
: ( ( ) ( )
Subset
of ) is
closed
iff
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
"
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
closed
) ) ) ) ;
theorem
:: TOPGRP_1:25
for
S
,
T
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) holds
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
iff (
dom
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
S
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
non
proper
dense
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
rng
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
non
proper
dense
)
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
one-to-one
& ( for
P
being ( ( ) ( )
Subset
of ) holds
(
P
: ( ( ) ( )
Subset
of ) is
open
iff
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.:
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
) ) ) ) ;
theorem
:: TOPGRP_1:26
for
S
,
T
being ( ( non
empty
) ( non
empty
)
TopStruct
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) holds
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
iff (
dom
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
S
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
non
proper
dense
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
rng
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[#]
T
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
non
proper
dense
)
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
one-to-one
& ( for
P
being ( ( ) ( )
Subset
of ) holds
(
P
: ( ( ) ( )
Subset
of ) is
open
iff
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
"
P
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
) ( non
empty
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
) ) ) ) ;
theorem
:: TOPGRP_1:27
for
S
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) ) holds
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) ) is
continuous
iff for
P
being ( ( ) ( )
Subset
of ) holds
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) )
"
(
Int
P
: ( ( ) ( )
Subset
of )
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
c=
Int
(
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) )
"
P
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
registration
let
T
be ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ;
cluster
non
empty
dense
for ( ( ) ( )
Element
of
bool
the
carrier
of
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: TOPGRP_1:28
for
S
,
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
for
A
being ( (
dense
) (
dense
)
Subset
of ) st
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
holds
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.:
A
: ( (
dense
) (
dense
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
dense
;
theorem
:: TOPGRP_1:29
for
S
,
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
f
being ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
for
A
being ( (
dense
) (
dense
)
Subset
of ) st
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
holds
f
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
"
A
: ( (
dense
) (
dense
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
dense
;
registration
let
S
,
T
be ( ( ) ( )
TopStruct
) ;
cluster
Function-like
quasi_total
being_homeomorphism
->
Function-like
one-to-one
quasi_total
onto
continuous
for ( ( ) ( )
Element
of
bool
[:
the
carrier
of
S
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
T
: ( ( ) ( )
Element
of the
carrier
of
S
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
S
,
T
be ( ( non
empty
) ( non
empty
)
TopStruct
) ;
cluster
Function-like
quasi_total
being_homeomorphism
->
Function-like
quasi_total
open
for ( ( ) ( )
Element
of
bool
[:
the
carrier
of
S
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
T
: ( ( ) ( )
Element
of the
carrier
of
S
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopStruct
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( ( ) ( )
TopStruct
) ;
cluster
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
being_homeomorphism
for ( ( ) ( )
Element
of
bool
[:
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
let
T
be ( ( ) ( )
TopStruct
) ;
let
f
be ( (
Function-like
quasi_total
being_homeomorphism
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) ;
cluster
f
: ( (
Function-like
quasi_total
being_homeomorphism
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Element
of
bool
[:
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
/"
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
being_homeomorphism
;
end;
begin
definition
let
S
,
T
be ( ( ) ( )
TopStruct
) ;
assume
S
: ( ( ) ( )
TopStruct
) ,
T
: ( ( ) ( )
TopStruct
)
are_homeomorphic
;
mode
Homeomorphism
of
S
,
T
->
( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
S
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
Element
of the
carrier
of
S
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) )
means
:: TOPGRP_1:def 3
it
: ( (
Function-like
quasi_total
) (
Relation-like
[:
S
: ( ( ) ( )
TopStruct
) ,
S
: ( ( ) ( )
TopStruct
)
:]
: ( ( ) ( )
set
)
-defined
S
: ( ( ) ( )
TopStruct
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
S
: ( ( ) ( )
TopStruct
) ,
S
: ( ( ) ( )
TopStruct
)
:]
: ( ( ) ( )
set
) ,
S
: ( ( ) ( )
TopStruct
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
;
end;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
mode
Homeomorphism
of
T
->
( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) )
means
:: TOPGRP_1:def 4
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) is
being_homeomorphism
;
end;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
:: original:
Homeomorphism
redefine
mode
Homeomorphism
of
T
->
( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ,
T
: ( ( ) ( )
TopStruct
) ) ;
end;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
:: original:
id
redefine
func
id
T
->
( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ,
T
: ( ( ) ( )
TopStruct
) ) ;
end;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
:: original:
id
redefine
func
id
T
->
( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ;
end;
registration
let
T
be ( ( ) ( )
TopStruct
) ;
cluster
->
being_homeomorphism
for ( ( ) ( )
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ;
end;
theorem
:: TOPGRP_1:30
for
T
being ( ( ) ( )
TopStruct
)
for
f
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) holds
f
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
/"
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ;
theorem
:: TOPGRP_1:31
for
T
being ( ( ) ( )
TopStruct
)
for
f
,
g
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) holds
f
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
*
g
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) ) : ( (
Function-like
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
func
HomeoGroup
T
->
( (
strict
) (
strict
)
multMagma
)
means
:: TOPGRP_1:def 5
for
x
being ( ( ) ( )
set
) holds
( (
x
: ( ( ) ( )
set
)
in
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) implies
x
: ( ( ) ( )
set
) is ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ) & (
x
: ( ( ) ( )
set
) is ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) implies
x
: ( ( ) ( )
set
)
in
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) ) & ( for
f
,
g
being ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) holds the
multF
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( (
Function-like
quasi_total
) (
Relation-like
[:
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) , the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) , the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
it
: ( ( ) ( )
Element
of the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) )
.
(
f
: ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ,
g
: ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) ) : ( ( ) ( )
set
)
=
g
: ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) )
*
f
: ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) : ( (
Function-like
) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
)
Element
of
bool
[:
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ) );
end;
registration
let
T
be ( ( ) ( )
TopStruct
) ;
cluster
HomeoGroup
T
: ( ( ) ( )
TopStruct
) : ( (
strict
) (
strict
)
multMagma
)
->
non
empty
strict
;
end;
theorem
:: TOPGRP_1:32
for
T
being ( ( ) ( )
TopStruct
)
for
f
,
g
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) )
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
f
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) &
g
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
=
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
(
HomeoGroup
b
1
: ( ( ) ( )
TopStruct
)
)
: ( (
strict
) ( non
empty
strict
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
=
g
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
*
f
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) ) : ( (
Function-like
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
registration
let
T
be ( ( ) ( )
TopStruct
) ;
cluster
HomeoGroup
T
: ( ( ) ( )
TopStruct
) : ( (
strict
) ( non
empty
strict
)
multMagma
)
->
strict
Group-like
associative
;
end;
theorem
:: TOPGRP_1:33
for
T
being ( ( ) ( )
TopStruct
) holds
id
T
: ( ( ) ( )
TopStruct
) : ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
=
1_
(
HomeoGroup
T
: ( ( ) ( )
TopStruct
)
)
: ( (
strict
) ( non
empty
strict
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
(
HomeoGroup
b
1
: ( ( ) ( )
TopStruct
)
)
: ( (
strict
) ( non
empty
strict
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: TOPGRP_1:34
for
T
being ( ( ) ( )
TopStruct
)
for
f
being ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
f
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
(
HomeoGroup
b
1
: ( ( ) ( )
TopStruct
)
)
: ( (
strict
) ( non
empty
strict
unital
Group-like
associative
)
multMagma
) : ( ( ) ( non
empty
)
set
) )
=
f
: ( ( ) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
b
1
: ( ( ) ( )
TopStruct
) )
/"
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) ;
definition
let
T
be ( ( ) ( )
TopStruct
) ;
attr
T
is
homogeneous
means
:: TOPGRP_1:def 6
for
p
,
q
being ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ex
f
being ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) ) st
f
: ( ( ) (
Relation-like
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
T
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
)
Homeomorphism
of
T
: ( ( ) ( )
TopStruct
) )
.
p
: ( ( ) ( )
Point
of ( ( ) ( )
set
) ) : ( ( ) ( )
set
)
=
q
: ( ( ) ( )
Point
of ( ( ) ( )
set
) ) ;
end;
registration
cluster
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
->
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
homogeneous
for ( ( ) ( )
TopStruct
) ;
end;
theorem
:: TOPGRP_1:35
for
T
being ( ( non
empty
TopSpace-like
homogeneous
) ( non
empty
TopSpace-like
homogeneous
)
TopSpace
) st ex
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
{
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
compact
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
homogeneous
) ( non
empty
TopSpace-like
homogeneous
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
closed
holds
T
: ( ( non
empty
TopSpace-like
homogeneous
) ( non
empty
TopSpace-like
homogeneous
)
TopSpace
) is
T_1
;
theorem
:: TOPGRP_1:36
for
T
being ( ( non
empty
TopSpace-like
homogeneous
) ( non
empty
TopSpace-like
homogeneous
)
TopSpace
) st ex
p
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) st
for
A
being ( ( ) ( )
Subset
of ) st
A
: ( ( ) ( )
Subset
of ) is
open
&
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
A
: ( ( ) ( )
Subset
of ) holds
ex
B
being ( ( ) ( )
Subset
of ) st
(
p
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
B
: ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of ) is
open
&
Cl
B
: ( ( ) ( )
Subset
of ) : ( ( ) (
closed
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
homogeneous
) ( non
empty
TopSpace-like
homogeneous
)
TopSpace
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
A
: ( ( ) ( )
Subset
of ) ) holds
T
: ( ( non
empty
TopSpace-like
homogeneous
) ( non
empty
TopSpace-like
homogeneous
)
TopSpace
) is
regular
;
begin
definition
attr
c
1
is
strict
;
struct
TopGrStr
->
( ( ) ( )
multMagma
) , ( ( ) ( )
TopStruct
) ;
aggr
TopGrStr
(#
carrier
,
multF
,
topology
#)
->
( (
strict
) (
strict
)
TopGrStr
) ;
end;
registration
let
A
be ( ( non
empty
) ( non
empty
)
set
) ;
let
R
be ( (
Function-like
quasi_total
) ( non
empty
Relation-like
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
A
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) )
quasi_total
)
BinOp
of
A
: ( ( non
empty
) ( non
empty
)
set
) ) ;
let
T
be ( ( ) ( )
Subset-Family
of ) ;
cluster
TopGrStr
(#
A
: ( ( non
empty
) ( non
empty
)
set
) ,
R
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
A
: ( ( non
empty
) ( non
empty
)
set
)
-valued
Function-like
V14
(
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
[:
A
: ( ( non
empty
) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
A
: ( ( non
empty
) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
T
: ( ( ) ( )
Element
of
bool
(
bool
A
: ( ( non
empty
) ( non
empty
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) (
strict
)
TopGrStr
)
->
non
empty
strict
;
end;
registration
let
x
be ( ( ) ( )
set
) ;
let
R
be ( (
Function-like
quasi_total
) ( non
empty
Relation-like
[:
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
-valued
Function-like
V14
(
[:
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
:]
: ( ( ) ( non
empty
)
set
) )
quasi_total
)
BinOp
of
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ) ;
let
T
be ( ( ) ( )
Subset-Family
of ) ;
cluster
TopGrStr
(#
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ,
R
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
[:
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
:]
: ( ( ) ( non
empty
)
set
)
-defined
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
-valued
Function-like
V14
(
[:
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
:]
: ( ( ) ( non
empty
)
set
) )
quasi_total
)
Element
of
bool
[:
[:
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
:]
: ( ( ) ( non
empty
)
set
) ,
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ,
T
: ( ( ) ( )
Element
of
bool
(
bool
{
x
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
)
)
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) #) : ( (
strict
) ( non
empty
strict
)
TopGrStr
)
->
trivial
strict
;
end;
registration
cluster
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
->
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
Group-like
associative
commutative
for ( ( ) ( )
multMagma
) ;
end;
registration
let
a
be ( ( ) ( )
set
) ;
cluster
1TopSp
{
a
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
)
set
) : ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
TopStruct
)
->
trivial
;
end;
registration
cluster
non
empty
strict
for ( ( ) ( )
TopGrStr
) ;
end;
registration
cluster
1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
TopSpace-like
strict
for ( ( ) ( )
TopGrStr
) ;
end;
definition
let
G
be ( ( non
empty
Group-like
associative
) ( non
empty
unital
Group-like
associative
)
TopGrStr
) ;
attr
G
is
UnContinuous
means
:: TOPGRP_1:def 7
inverse_op
G
: ( ( ) ( )
TopStruct
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Element
of
bool
[:
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) is
continuous
;
end;
definition
let
G
be ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
) ;
attr
G
is
BinContinuous
means
:: TOPGRP_1:def 8
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
[:
G
: ( ( ) ( )
TopStruct
) ,
G
: ( ( ) ( )
TopStruct
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) st
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
[:
G
: ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
) ,
G
: ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) )
=
the
multF
of
G
: ( ( ) ( )
TopStruct
) : ( (
Function-like
quasi_total
) (
Relation-like
[:
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Element
of
bool
[:
[:
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) , the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) , the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) holds
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
[:
G
: ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
) ,
G
: ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
)
:]
: ( (
strict
TopSpace-like
) (
strict
TopSpace-like
)
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( (
TopSpace-like
) (
TopSpace-like
)
TopGrStr
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) is
continuous
;
end;
registration
cluster
non
empty
trivial
V43
() 1 : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V27
()
V28
()
cardinal
)
Element
of
K114
() : ( ( ) ( non
empty
V21
()
V22
()
V23
()
V28
()
cardinal
limit_cardinal
)
Element
of
bool
K110
() : ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) )
-element
TopSpace-like
compact
unital
Group-like
associative
commutative
homogeneous
strict
UnContinuous
BinContinuous
for ( ( ) ( )
TopGrStr
) ;
end;
definition
mode
TopGroup
is
( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGrStr
) ;
end;
definition
mode
TopologicalGroup
is
( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopGroup
) ;
end;
theorem
:: TOPGRP_1:37
for
T
being ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
W
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) ) ex
A
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ex
B
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) st
A
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
*
B
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
W
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPGRP_1:38
for
T
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopGrStr
) st ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
W
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) ) ex
A
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ex
B
being ( ( ) ( non
empty
)
a_neighborhood
of
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) st
A
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
*
B
: ( ( ) ( non
empty
)
a_neighborhood
of
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
W
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) ) ) holds
T
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopGrStr
) is
BinContinuous
;
theorem
:: TOPGRP_1:39
for
T
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
W
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ex
A
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) st
A
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
W
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPGRP_1:40
for
T
being ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) st ( for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
W
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ex
A
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) st
A
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
W
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ) holds
T
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) is
UnContinuous
;
theorem
:: TOPGRP_1:41
for
T
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
)
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
W
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) ex
A
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ex
B
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) st
A
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
*
(
B
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
"
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
W
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPGRP_1:42
for
T
being ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) st ( for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
W
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ex
A
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) ex
B
being ( ( ) ( non
empty
)
a_neighborhood
of
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ) st
A
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
*
(
B
: ( ( ) ( non
empty
)
a_neighborhood
of
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) )
"
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
W
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
(
b
3
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ) holds
T
: ( ( non
empty
TopSpace-like
Group-like
associative
) ( non
empty
TopSpace-like
unital
Group-like
associative
)
TopGroup
) is ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
BinContinuous
)
TopologicalGroup
) ;
registration
let
G
be ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) )
*
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
continuous
;
cluster
*
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
V14
( the
carrier
of
G
: ( ( non
empty
TopSpace-like
BinContinuous
) ( non
empty
TopSpace-like
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) )
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
->
Function-like
quasi_total
continuous
;
end;
theorem
:: TOPGRP_1:43
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
: ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
continuous
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) ) ;
theorem
:: TOPGRP_1:44
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
)
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
continuous
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) ) ;
definition
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
BinContinuous
)
TopGroup
) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
:: original:
*
redefine
func
a
*
->
( ( ) ( non
empty
Relation-like
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
G
: ( ( ) ( )
TopStruct
) ) ;
:: original:
*
redefine
func
*
a
->
( ( ) ( non
empty
Relation-like
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
G
: ( ( ) ( )
TopStruct
) ) ;
end;
theorem
:: TOPGRP_1:45
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) holds
inverse_op
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( (
Function-like
quasi_total
) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
)
Element
of
bool
[:
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) , the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( non
empty
Relation-like
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) ) ;
definition
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) ;
:: original:
inverse_op
redefine
func
inverse_op
G
->
( ( ) ( non
empty
Relation-like
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
one-to-one
V14
( the
carrier
of
G
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
onto
bijective
continuous
being_homeomorphism
open
)
Homeomorphism
of
G
: ( ( ) ( )
TopStruct
) ) ;
end;
registration
cluster
non
empty
TopSpace-like
Group-like
associative
BinContinuous
->
non
empty
TopSpace-like
Group-like
associative
homogeneous
for ( ( ) ( )
TopGrStr
) ;
end;
theorem
:: TOPGRP_1:46
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
F
being ( (
closed
) (
closed
)
Subset
of )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
F
: ( (
closed
) (
closed
)
Subset
of )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
closed
;
theorem
:: TOPGRP_1:47
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
F
being ( (
closed
) (
closed
)
Subset
of )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
F
: ( (
closed
) (
closed
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
closed
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) ;
let
F
be ( (
closed
) (
closed
)
Subset
of ) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
F
: ( (
closed
) (
closed
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
closed
;
cluster
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) )
*
F
: ( (
closed
) (
closed
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
closed
;
end;
theorem
:: TOPGRP_1:48
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
)
for
F
being ( (
closed
) (
closed
)
Subset
of ) holds
F
: ( (
closed
) (
closed
)
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
closed
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) ;
let
F
be ( (
closed
) (
closed
)
Subset
of ) ;
cluster
F
: ( (
closed
) (
closed
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
closed
;
end;
theorem
:: TOPGRP_1:49
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
O
being ( (
open
) (
open
)
Subset
of )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
O
: ( (
open
) (
open
)
Subset
of )
*
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
;
theorem
:: TOPGRP_1:50
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
O
being ( (
open
) (
open
)
Subset
of )
for
a
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
O
: ( (
open
) (
open
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) ;
let
A
be ( (
open
) (
open
)
Subset
of ) ;
let
a
be ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) ;
cluster
A
: ( (
open
) (
open
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
open
;
cluster
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) )
*
A
: ( (
open
) (
open
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
open
;
end;
theorem
:: TOPGRP_1:51
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
)
for
O
being ( (
open
) (
open
)
Subset
of ) holds
O
: ( (
open
) (
open
)
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) ;
let
A
be ( (
open
) (
open
)
Subset
of ) ;
cluster
A
: ( (
open
) (
open
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
open
;
end;
theorem
:: TOPGRP_1:52
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
A
,
O
being ( ( ) ( )
Subset
of ) st
O
: ( ( ) ( )
Subset
of ) is
open
holds
O
: ( ( ) ( )
Subset
of )
*
A
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
;
theorem
:: TOPGRP_1:53
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
A
,
O
being ( ( ) ( )
Subset
of ) st
O
: ( ( ) ( )
Subset
of ) is
open
holds
A
: ( ( ) ( )
Subset
of )
*
O
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
open
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) ;
let
A
be ( (
open
) (
open
)
Subset
of ) ;
let
B
be ( ( ) ( )
Subset
of ) ;
cluster
A
: ( (
open
) (
open
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*
B
: ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
open
;
cluster
B
: ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*
A
: ( (
open
) (
open
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
open
;
end;
theorem
:: TOPGRP_1:54
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
)
for
a
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) holds
A
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPGRP_1:55
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
)
for
a
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
for
A
being ( ( ) ( non
empty
)
a_neighborhood
of
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
*
(
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) ex
B
being ( (
open
) ( non
empty
open
)
a_neighborhood
of
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ) st
B
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
*
(
B
: ( (
open
) ( non
empty
open
)
a_neighborhood
of
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) )
"
)
: ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
open
)
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
A
: ( ( ) ( non
empty
)
a_neighborhood
of
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
*
(
b
2
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: TOPGRP_1:56
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
)
for
A
being ( (
dense
) (
dense
)
Subset
of ) holds
A
: ( (
dense
) (
dense
)
Subset
of )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
dense
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGroup
) ;
let
A
be ( (
dense
) (
dense
)
Subset
of ) ;
cluster
A
: ( (
dense
) (
dense
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
"
: ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
UnContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
dense
;
end;
theorem
:: TOPGRP_1:57
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
A
being ( (
dense
) (
dense
)
Subset
of )
for
a
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
*
A
: ( (
dense
) (
dense
)
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
dense
;
theorem
:: TOPGRP_1:58
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
)
for
A
being ( (
dense
) (
dense
)
Subset
of )
for
a
being ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) holds
A
: ( (
dense
) (
dense
)
Subset
of )
*
a
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
dense
;
registration
let
G
be ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGroup
) ;
let
A
be ( (
dense
) (
dense
)
Subset
of ) ;
let
a
be ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) ;
cluster
A
: ( (
dense
) (
dense
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
*
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
dense
;
cluster
a
: ( ( ) ( )
Element
of the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) )
*
A
: ( (
dense
) (
dense
)
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
BinContinuous
)
TopGrStr
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
->
dense
;
end;
theorem
:: TOPGRP_1:59
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
)
for
B
being ( (
open
V182
(
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ,
1_
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) ) (
open
V182
(
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ,
1_
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) )
Basis
of
1_
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) )
for
M
being ( (
dense
) (
dense
)
Subset
of ) holds
{
(
V
: ( ( ) ( )
Subset
of )
*
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) where
V
is ( ( ) ( )
Subset
of ) ,
x
is ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) ) : (
V
: ( ( ) ( )
Subset
of )
in
B
: ( (
open
V182
(
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ,
1_
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) ) (
open
V182
(
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ,
1_
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) )
Basis
of
1_
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
being_of_order_0
)
Element
of the
carrier
of
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) : ( ( ) ( non
empty
)
set
) ) ) &
x
: ( ( ) ( )
Point
of ( ( ) ( non
empty
)
set
) )
in
M
: ( (
dense
) (
dense
)
Subset
of ) )
}
is ( (
open
V180
(
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ) ) (
open
V180
(
b
1
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ) )
Basis
of
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) ) ;
theorem
:: TOPGRP_1:60
for
G
being ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) holds
G
: ( ( non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
) ( non
empty
TopSpace-like
unital
Group-like
associative
homogeneous
UnContinuous
BinContinuous
)
TopologicalGroup
) is
regular
;
registration
cluster
non
empty
TopSpace-like
Group-like
associative
UnContinuous
BinContinuous
->
non
empty
TopSpace-like
regular
Group-like
associative
UnContinuous
BinContinuous
for ( ( ) ( )
TopGrStr
) ;
end;
theorem
:: TOPGRP_1:61
for
T
being ( ( ) ( )
TopStruct
)
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) st
T
: ( ( ) ( )
TopStruct
) is
empty
holds
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
)
-valued
Function-like
V14
( the
carrier
of
b
1
: ( ( ) ( )
TopStruct
) : ( ( ) ( )
set
) )
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) is
being_homeomorphism
;