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


begin

registration
let X be set ;
cluster Relation-like X -defined X -valued Function-like one-to-one quasi_total onto Element of bool [:X,X:];
existence
ex b1 being Function of X,X st
( b1 is one-to-one & b1 is onto )
proof end;
end;

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

registration
let R be 1-sorted ;
cluster (id R) /" -> one-to-one ;
coherence
(id R) /" is one-to-one
proof end;
end;

theorem Th2: :: TOPGRP_1:2
for R being 1-sorted holds (id R) /" = id R
proof end;

theorem :: TOPGRP_1:3
for R being 1-sorted
for X being Subset of R holds (id R) " X = X
proof end;

begin

theorem Th4: :: TOPGRP_1:4
for H being non empty multMagma
for P, P1, Q, Q1 being Subset of H st P c= P1 & Q c= Q1 holds
P * Q c= P1 * Q1
proof end;

theorem Th5: :: TOPGRP_1:5
for H being non empty multMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
P * h c= Q * h
proof end;

theorem :: TOPGRP_1:6
for H being non empty multMagma
for P, Q being Subset of H
for h being Element of H st P c= Q holds
h * P c= h * Q
proof end;

theorem Th7: :: TOPGRP_1:7
for G being Group
for A being Subset of G
for a being Element of G holds
( a in A " iff a " in A )
proof end;

theorem :: TOPGRP_1:8
for G being Group
for A being Subset of G holds (A ") " = A ;

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

theorem Th9: :: TOPGRP_1:9
for G being Group
for A, B being Subset of G holds
( A c= B iff A " c= B " )
proof end;

theorem Th10: :: TOPGRP_1:10
for G being Group
for A being Subset of G holds (inverse_op G) .: A = A "
proof end;

theorem Th11: :: TOPGRP_1:11
for G being Group
for A being Subset of G holds (inverse_op G) " A = A "
proof end;

theorem Th12: :: TOPGRP_1:12
for G being Group holds inverse_op G is one-to-one
proof end;

theorem Th13: :: TOPGRP_1:13
for G being Group holds rng (inverse_op G) = the carrier of G
proof end;

registration
let G be Group;
cluster inverse_op G -> one-to-one onto ;
coherence
( inverse_op G is one-to-one & inverse_op G is onto )
proof end;
end;

theorem Th14: :: TOPGRP_1:14
for G being Group holds (inverse_op G) " = inverse_op G
proof end;

theorem Th15: :: TOPGRP_1:15
for H being non empty multMagma
for P, Q being Subset of H holds the multF of H .: [:P,Q:] = P * Q
proof end;

definition
let G be non empty multMagma ;
let a be Element of G;
func a * -> Function of G,G means :Def1: :: TOPGRP_1:def 1
 for x being Element of G holds it . x = a * x;
existence
ex b1 being Function of G,G st
for x being Element of G holds b1 . x = a * x
proof end;
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = a * x ) & ( for x being Element of G holds b2 . x = a * x ) holds
b1 = b2
proof end;
func * a -> Function of G,G means :Def2: :: TOPGRP_1:def 2
 for x being Element of G holds it . x = x * a;
existence
ex b1 being Function of G,G st
for x being Element of G holds b1 . x = x * a
proof end;
uniqueness
for b1, b2 being Function of G,G st ( for x being Element of G holds b1 . x = x * a ) & ( for x being Element of G holds b2 . x = x * a ) holds
b1 = b2
proof end;
end;

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

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

registration
let G be Group;
let a be Element of G;
cluster a * -> one-to-one onto ;
coherence
( a * is one-to-one & a * is onto )
proof end;
cluster * a -> one-to-one onto ;
coherence
( * a is one-to-one & * a is onto )
proof end;
end;

theorem Th16: :: TOPGRP_1:16
for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (h *) .: P = h * P
proof end;

theorem Th17: :: TOPGRP_1:17
for H being non empty multMagma
for P being Subset of H
for h being Element of H holds (* h) .: P = P * h
proof end;

theorem Th18: :: TOPGRP_1:18
for G being Group
for a being Element of G holds (a *) /" = (a ") *
proof end;

theorem Th19: :: TOPGRP_1:19
for G being Group
for a being Element of G holds (* a) /" = * (a ")
proof end;

begin

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

theorem Th20: :: TOPGRP_1:20
for T being TopStruct holds id T is being_homeomorphism
proof end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster -> non empty a_neighborhood of p;
coherence
for b1 being a_neighborhood of p holds not b1 is empty
proof end;
end;

theorem Th21: :: TOPGRP_1:21
for T being non empty TopSpace
for p being Point of T holds [#] T is a_neighborhood of p
proof end;

registration
let T be non empty TopSpace;
let p be Point of T;
cluster non empty open a_neighborhood of p;
existence
ex b1 being a_neighborhood of p st
( not b1 is empty & b1 is open )
proof end;
end;

theorem :: TOPGRP_1:22
for S, T being non empty TopSpace
for f being Function of S,T st f is open holds
for p being Point of S
for P being a_neighborhood of p ex R being open a_neighborhood of f . p st R c= f .: P
proof end;

theorem :: TOPGRP_1:23
for S, T being non empty TopSpace
for f being Function of S,T st ( for p being Point of S
for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P ) holds
f is open
proof end;

theorem :: TOPGRP_1:24
for S, T being non empty TopStruct
for f being Function of S,T holds
( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f " P is closed ) ) ) )
proof end;

theorem Th25: :: TOPGRP_1:25
for S, T being non empty TopStruct
for f being Function of S,T holds
( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of S holds
( P is open iff f .: P is open ) ) ) )
proof end;

theorem :: TOPGRP_1:26
for S, T being non empty TopStruct
for f being Function of S,T holds
( f is being_homeomorphism iff ( dom f = [#] S & rng f = [#] T & f is one-to-one & ( for P being Subset of T holds
( P is open iff f " P is open ) ) ) )
proof end;

theorem :: TOPGRP_1:27
for S being TopSpace
for T being non empty TopSpace
for f being Function of S,T holds
( f is continuous iff for P being Subset of T holds f " (Int P) c= Int (f " P) )
proof end;

registration
let T be non empty TopSpace;
cluster non empty dense Element of bool the carrier of T;
existence
ex b1 being Subset of T st
( not b1 is empty & b1 is dense )
proof end;
end;

theorem Th28: :: TOPGRP_1:28
for S, T being non empty TopSpace
for f being Function of S,T
for A being dense Subset of S st f is being_homeomorphism holds
f .: A is dense
proof end;

theorem Th29: :: TOPGRP_1:29
for S, T being non empty TopSpace
for f being Function of S,T
for A being dense Subset of T st f is being_homeomorphism holds
f " A is dense
proof end;

registration
let S, T be TopStruct ;
cluster Function-like quasi_total being_homeomorphism -> one-to-one onto continuous Element of bool [: the carrier of S, the carrier of T:];
coherence
for b1 being Function of S,T st b1 is being_homeomorphism holds
( b1 is onto & b1 is one-to-one & b1 is continuous )
proof end;
end;

registration
let S, T be non empty TopStruct ;
cluster Function-like quasi_total being_homeomorphism -> open Element of bool [: the carrier of S, the carrier of T:];
coherence
for b1 being Function of S,T st b1 is being_homeomorphism holds
b1 is open
proof end;
end;

registration
let T be TopStruct ;
cluster Relation-like the carrier of T -defined the carrier of T -valued Function-like quasi_total being_homeomorphism Element of bool [: the carrier of T, the carrier of T:];
existence
ex b1 being Function of T,T st b1 is being_homeomorphism
proof end;
end;

registration
let T be TopStruct ;
let f be being_homeomorphism Function of T,T;
cluster f /" -> being_homeomorphism ;
coherence
f /" is being_homeomorphism
proof end;
end;

begin

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

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

definition
let T be TopStruct ;
mode Homeomorphism of T -> Function of T,T means :Def4: :: TOPGRP_1:def 4
it is being_homeomorphism ;
existence
ex b1 being Function of T,T st b1 is being_homeomorphism
proof end;
end;

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

definition
let T be TopStruct ;
:: original: Homeomorphism
redefine mode Homeomorphism of T -> Homeomorphism of T,T;
coherence
for b1 being Homeomorphism of T holds b1 is Homeomorphism of T,T
proof end;
end;

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

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

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

theorem Th30: :: TOPGRP_1:30
for T being TopStruct
for f being Homeomorphism of T holds f /" is Homeomorphism of T
proof end;

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

theorem Th31: :: TOPGRP_1:31
for T being TopStruct
for f, g being Homeomorphism of T holds f * g is Homeomorphism of T
proof end;

definition
let T be TopStruct ;
func HomeoGroup T -> strict multMagma means :Def5: :: TOPGRP_1:def 5
 for x being set holds
( ( x in the carrier of it implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of it ) & ( for f, g being Homeomorphism of T holds the multF of it . (f,g) = g * f ) );
existence
ex b1 being strict multMagma st
for x being set holds
( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) )
proof end;
uniqueness
for b1, b2 being strict multMagma st ( for x being set holds
( ( x in the carrier of b1 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b1 ) & ( for f, g being Homeomorphism of T holds the multF of b1 . (f,g) = g * f ) ) ) & ( for x being set holds
( ( x in the carrier of b2 implies x is Homeomorphism of T ) & ( x is Homeomorphism of T implies x in the carrier of b2 ) & ( for f, g being Homeomorphism of T holds the multF of b2 . (f,g) = g * f ) ) ) holds
b1 = b2
proof end;
end;

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

registration
let T be TopStruct ;
cluster HomeoGroup T -> non empty strict ;
coherence
not HomeoGroup T is empty
proof end;
end;

theorem :: TOPGRP_1:32
for T being TopStruct
for f, g being Homeomorphism of T
for a, b being Element of (HomeoGroup T) st f = a & g = b holds
a * b = g * f by Def5;

registration
let T be TopStruct ;
cluster HomeoGroup T -> strict Group-like associative ;
coherence
( HomeoGroup T is Group-like & HomeoGroup T is associative )
proof end;
end;

theorem Th33: :: TOPGRP_1:33
for T being TopStruct holds id T = 1_ (HomeoGroup T)
proof end;

theorem :: TOPGRP_1:34
for T being TopStruct
for f being Homeomorphism of T
for a being Element of (HomeoGroup T) st f = a holds
a " = f /"
proof end;

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

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

registration
cluster non empty trivial -> non empty homogeneous TopStruct ;
coherence
for b1 being non empty TopStruct st b1 is trivial holds
b1 is homogeneous
proof end;
end;

registration
cluster non empty trivial strict TopSpace-like TopStruct ;
existence
ex b1 being TopSpace st
( b1 is strict & b1 is trivial & not b1 is empty )
proof end;
end;

theorem :: TOPGRP_1:35
for T being non empty homogeneous TopSpace st ex p being Point of T st {p} is closed holds
T is T_1
proof end;

theorem Th36: :: TOPGRP_1:36
for T being non empty homogeneous TopSpace st ex p being Point of T st
for A being Subset of T st A is open & p in A holds
ex B being Subset of T st
( p in B & B is open & Cl B c= A ) holds
T is regular
proof end;

begin

definition
attr c1 is strict ;
struct TopGrStr -> multMagma , TopStruct ;
aggr TopGrStr(# carrier, multF, topology #) -> TopGrStr ;
end;

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

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

registration
cluster non empty trivial -> non empty Group-like associative commutative multMagma ;
coherence
for b1 being non empty multMagma st b1 is trivial holds
( b1 is Group-like & b1 is associative & b1 is commutative )
proof end;
end;

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

registration
cluster non empty strict TopGrStr ;
existence
ex b1 being TopGrStr st
( b1 is strict & not b1 is empty )
proof end;
end;

registration
cluster non empty trivial TopSpace-like strict TopGrStr ;
existence
ex b1 being TopGrStr st
( b1 is strict & b1 is TopSpace-like & b1 is trivial & not b1 is empty )
proof end;
end;

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

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

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

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

registration
cluster non empty trivial TopSpace-like unital Group-like associative commutative strict UnContinuous BinContinuous TopGrStr ;
existence
ex b1 being non empty TopSpace-like Group-like associative TopGrStr st
( b1 is strict & b1 is commutative & b1 is trivial & b1 is UnContinuous & b1 is BinContinuous )
proof end;
end;

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

definition
mode TopologicalGroup is UnContinuous BinContinuous TopGroup;
end;

theorem Th37: :: TOPGRP_1:37
for T being non empty TopSpace-like BinContinuous TopGrStr
for a, b being Element of T
for W being a_neighborhood of a * b ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * B c= W
proof end;

theorem Th38: :: TOPGRP_1:38
for T being non empty TopSpace-like TopGrStr st ( for a, b being Element of T
for W being a_neighborhood of a * b ex A being a_neighborhood of a ex B being a_neighborhood of b st A * B c= W ) holds
T is BinContinuous
proof end;

theorem Th39: :: TOPGRP_1:39
for T being UnContinuous TopGroup
for a being Element of T
for W being a_neighborhood of a " ex A being open a_neighborhood of a st A " c= W
proof end;

theorem Th40: :: TOPGRP_1:40
for T being TopGroup st ( for a being Element of T
for W being a_neighborhood of a " ex A being a_neighborhood of a st A " c= W ) holds
T is UnContinuous
proof end;

theorem Th41: :: TOPGRP_1:41
for T being TopologicalGroup
for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being open a_neighborhood of a ex B being open a_neighborhood of b st A * (B ") c= W
proof end;

theorem :: TOPGRP_1:42
for T being TopGroup st ( for a, b being Element of T
for W being a_neighborhood of a * (b ") ex A being a_neighborhood of a ex B being a_neighborhood of b st A * (B ") c= W ) holds
T is TopologicalGroup
proof end;

registration
let G be non empty TopSpace-like BinContinuous TopGrStr ;
let a be Element of G;
cluster a * -> continuous ;
coherence
a * is continuous
proof end;
cluster * a -> continuous ;
coherence
* a is continuous
proof end;
end;

theorem Th43: :: TOPGRP_1:43
for G being BinContinuous TopGroup
for a being Element of G holds a * is Homeomorphism of G
proof end;

theorem Th44: :: TOPGRP_1:44
for G being BinContinuous TopGroup
for a being Element of G holds * a is Homeomorphism of G
proof end;

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

theorem Th45: :: TOPGRP_1:45
for G being UnContinuous TopGroup holds inverse_op G is Homeomorphism of G
proof end;

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

registration
cluster non empty TopSpace-like Group-like associative BinContinuous -> homogeneous TopGrStr ;
coherence
for b1 being TopGroup st b1 is BinContinuous holds
b1 is homogeneous
proof end;
end;

theorem Th46: :: TOPGRP_1:46
for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds F * a is closed
proof end;

theorem Th47: :: TOPGRP_1:47
for G being BinContinuous TopGroup
for F being closed Subset of G
for a being Element of G holds a * F is closed
proof end;

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

theorem Th48: :: TOPGRP_1:48
for G being UnContinuous TopGroup
for F being closed Subset of G holds F " is closed
proof end;

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

theorem Th49: :: TOPGRP_1:49
for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds O * a is open
proof end;

theorem Th50: :: TOPGRP_1:50
for G being BinContinuous TopGroup
for O being open Subset of G
for a being Element of G holds a * O is open
proof end;

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

theorem Th51: :: TOPGRP_1:51
for G being UnContinuous TopGroup
for O being open Subset of G holds O " is open
proof end;

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

theorem Th52: :: TOPGRP_1:52
for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
O * A is open
proof end;

theorem Th53: :: TOPGRP_1:53
for G being BinContinuous TopGroup
for A, O being Subset of G st O is open holds
A * O is open
proof end;

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

theorem Th54: :: TOPGRP_1:54
for G being UnContinuous TopGroup
for a being Point of G
for A being a_neighborhood of a holds A " is a_neighborhood of a "
proof end;

theorem Th55: :: TOPGRP_1:55
for G being TopologicalGroup
for a being Point of G
for A being a_neighborhood of a * (a ") ex B being open a_neighborhood of a st B * (B ") c= A
proof end;

theorem Th56: :: TOPGRP_1:56
for G being UnContinuous TopGroup
for A being dense Subset of G holds A " is dense
proof end;

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

theorem Th57: :: TOPGRP_1:57
for G being BinContinuous TopGroup
for A being dense Subset of G
for a being Point of G holds a * A is dense
proof end;

theorem Th58: :: TOPGRP_1:58
for G being BinContinuous TopGroup
for A being dense Subset of G
for a being Point of G holds A * a is dense
proof end;

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

theorem :: TOPGRP_1:59
for G being TopologicalGroup
for B being Basis of 1_ G
for M being dense Subset of G holds { (V * x) where V is Subset of G, x is Point of G : ( V in B & x in M ) } is Basis of G
proof end;

theorem Th60: :: TOPGRP_1:60
for G being TopologicalGroup holds G is regular
proof end;

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

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