defpred S1[ object , object ] means [$2,1] = $1;
let n be non zero 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 object st x in the carrier of (FTSL2 (n,1)) holds
ex y being object st
( y in the carrier of (FTSL1 n) & S1[x,y] )
proof
let x be
object ;
( x in the carrier of (FTSL2 (n,1)) implies ex y being object 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 object st
( y in the carrier of (FTSL1 n) & S1[x,y] )
then consider u,
v being
object 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
Nat by A3, A4;
( 1
<= nv &
nv <= 1 )
by A4, FINSEQ_1:1;
then
S1[
x,
nu]
by A5, XXREAL_0:1;
hence
ex
y being
object 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 object 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 object 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
object ;
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 XTUPLE_0:1;
[x,1] in dom f
by A10, FUNCT_2:def 1;
hence
x in rng f
by A11, FUNCT_1:def 3;
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
object 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
Nat by A14;
let y be
object ;
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:1;
then A18:
nv = 1
by XXREAL_0:1;
Im (
(Nbdl1 n),
(f . x))
c= rng f
by A7, A8;
then consider x3 being
object such that A19:
x3 in dom f
and A20:
y = f . x3
by A7, A17, FUNCT_1:def 3;
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:8
.=
{1,1,(min (2,1))}
by XXREAL_0:def 10
.=
{1,(min (2,1))}
by ENUMSET1:30
.=
{1,1}
by XXREAL_0:def 9
.=
{1}
by ENUMSET1:29
;
then A21:
1
in Im (
(Nbdl1 1),
v)
by ZFMISC_1:31;
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, XTUPLE_0:1;
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 6;
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, XTUPLE_0:1;
let y be
object ;
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
object such that A25:
x2 in dom f
and A26:
(
x2 in Im (
(Nbdl2 (n,1)),
x) &
y = f . x2 )
by FUNCT_1:def 6;
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:87;
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 object 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 4;
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;
hence
ex h being Function of (FTSL2 (n,1)),(FTSL1 n) st h is being_homeomorphism
; verum