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