defpred S1[ set , set ] means [$2,1] = $1;
let n be non zero Element of NAT ; ex h being Function of (FTSL2 n,1),(FTSL1 n) st h is being_homeomorphism
set FT1 = FTSL2 n,1;
set FT2 = FTSL1 n;
A1:
for x being set st x in the carrier of (FTSL2 n,1) holds
ex y being set st
( y in the carrier of (FTSL1 n) & S1[x,y] )
proof
let x be
set ;
( x in the carrier of (FTSL2 n,1) implies ex y being set st
( y in the carrier of (FTSL1 n) & S1[x,y] ) )
A2:
FTSL1 n = RelStr(#
(Seg n),
(Nbdl1 n) #)
by FINTOPO4:def 4;
assume
x in the
carrier of
(FTSL2 n,1)
;
ex y being set st
( y in the carrier of (FTSL1 n) & S1[x,y] )
then consider u,
v being
set such that A3:
u in Seg n
and A4:
v in Seg 1
and A5:
x = [u,v]
by ZFMISC_1:def 2;
reconsider nu =
u,
nv =
v as
Element of
NAT by A3, A4;
( 1
<= nv &
nv <= 1 )
by A4, FINSEQ_1:3;
then
S1[
x,
nu]
by A5, XXREAL_0:1;
hence
ex
y being
set st
(
y in the
carrier of
(FTSL1 n) &
S1[
x,
y] )
by A3, A2;
verum
end;
ex f being Function of (FTSL2 n,1),(FTSL1 n) st
for x being set st x in the carrier of (FTSL2 n,1) holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
then consider f being Function of (FTSL2 n,1),(FTSL1 n) such that
A6:
for x being set st x in the carrier of (FTSL2 n,1) holds
S1[x,f . x]
;
A7:
FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #)
by FINTOPO4:def 4;
A8:
the carrier of (FTSL1 n) c= rng f
proof
let x be
set ;
TARSKI:def 3 ( not x in the carrier of (FTSL1 n) or x in rng f )
set z =
[x,1];
A9:
1
in Seg 1
;
assume
x in the
carrier of
(FTSL1 n)
;
x in rng f
then A10:
[x,1] in the
carrier of
(FTSL2 n,1)
by A7, A9, ZFMISC_1:def 2;
then
[(f . [x,1]),1] = [x,1]
by A6;
then A11:
f . [x,1] = x
by ZFMISC_1:33;
[x,1] in dom f
by A10, FUNCT_2:def 1;
hence
x in rng f
by A11, FUNCT_1:def 5;
verum
end;
A12:
for x being Element of (FTSL2 n,1) holds f .: (U_FT x) = Im the InternalRel of (FTSL1 n),(f . x)
proof
let x be
Element of
(FTSL2 n,1);
f .: (U_FT x) = Im the InternalRel of (FTSL1 n),(f . x)
consider u,
v being
set such that A13:
u in Seg n
and A14:
v in Seg 1
and A15:
x = [u,v]
by ZFMISC_1:def 2;
A16:
Im the
InternalRel of
(FTSL1 n),
(f . x) c= f .: (U_FT x)
proof
reconsider nv =
v as
Element of
NAT by A14;
let y be
set ;
TARSKI:def 3 ( not y in Im the InternalRel of (FTSL1 n),(f . x) or y in f .: (U_FT x) )
assume A17:
y in Im the
InternalRel of
(FTSL1 n),
(f . x)
;
y in f .: (U_FT x)
( 1
<= nv &
nv <= 1 )
by A14, FINSEQ_1:3;
then A18:
nv = 1
by XXREAL_0:1;
Im (Nbdl1 n),
(f . x) c= rng f
by A7, A8, XBOOLE_1:1;
then consider x3 being
set such that A19:
x3 in dom f
and A20:
y = f . x3
by A7, A17, FUNCT_1:def 5;
set u2 =
f . x3;
set v2 = 1;
Im (Nbdl1 1),
v =
{nv,(max (nv -' 1),1),(min (nv + 1),1)}
by A14, FINTOPO4:def 3
.=
{1,(max 0 ,1),(min 2,1)}
by A18, NAT_2:10
.=
{1,1,(min 2,1)}
by XXREAL_0:def 10
.=
{1,(min 2,1)}
by ENUMSET1:70
.=
{1,1}
by XXREAL_0:def 9
.=
{1}
by ENUMSET1:69
;
then A21:
1
in Im (Nbdl1 1),
v
by ZFMISC_1:37;
A22:
Im (Nbdl2 n,1),
x = [:(Im (Nbdl1 n),u),(Im (Nbdl1 1),v):]
by A13, A14, A15, Def2;
x = [(f . x),1]
by A6;
then
f . x3 in Im (Nbdl1 n),
u
by A7, A15, A17, A20, ZFMISC_1:33;
then A23:
[(f . x3),1] in [:(Im (Nbdl1 n),u),(Im (Nbdl1 1),v):]
by A21, ZFMISC_1:def 2;
x3 = [(f . x3),1]
by A6, A19;
hence
y in f .: (U_FT x)
by A19, A20, A23, A22, FUNCT_1:def 12;
verum
end;
f .: (U_FT x) c= Im the
InternalRel of
(FTSL1 n),
(f . x)
proof
x = [(f . x),1]
by A6;
then A24:
u = f . x
by A15, ZFMISC_1:33;
let y be
set ;
TARSKI:def 3 ( not y in f .: (U_FT x) or y in Im the InternalRel of (FTSL1 n),(f . x) )
assume
y in f .: (U_FT x)
;
y in Im the InternalRel of (FTSL1 n),(f . x)
then consider x2 being
set such that A25:
x2 in dom f
and A26:
(
x2 in Im (Nbdl2 n,1),
x &
y = f . x2 )
by FUNCT_1:def 12;
A27:
Im (Nbdl2 n,1),
x = [:(Im (Nbdl1 n),u),(Im (Nbdl1 1),v):]
by A13, A14, A15, Def2;
x2 = [(f . x2),1]
by A6, A25;
hence
y in Im the
InternalRel of
(FTSL1 n),
(f . x)
by A7, A26, A27, A24, ZFMISC_1:106;
verum
end;
hence
f .: (U_FT x) = Im the
InternalRel of
(FTSL1 n),
(f . x)
by A16, XBOOLE_0:def 10;
verum
end;
for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
then A30:
f is one-to-one
by FUNCT_1:def 8;
rng f = the carrier of (FTSL1 n)
by A8, XBOOLE_0:def 10;
then
f is onto
by FUNCT_2:def 3;
then
f is being_homeomorphism
by A30, A12, Def1;
hence
ex h being Function of (FTSL2 n,1),(FTSL1 n) st h is being_homeomorphism
; verum