defpred S1[ set , set ] means [$2,1] = $1;
let n be non zero Element of NAT ; ex h being Function of (FTSS2 n,1),(FTSL1 n) st h is being_homeomorphism
set FT1 = FTSS2 n,1;
set FT2 = FTSL1 n;
A1:
for x being set st x in the carrier of (FTSS2 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 (FTSS2 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
(FTSS2 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 (FTSS2 n,1),(FTSL1 n) st
for x being set st x in the carrier of (FTSS2 n,1) holds
S1[x,f . x]
from FUNCT_2:sch 1(A1);
then consider f being Function of (FTSS2 n,1),(FTSL1 n) such that
A6:
for x being set st x in the carrier of (FTSS2 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
(FTSS2 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 (FTSS2 n,1) holds f .: (U_FT x) = Im the InternalRel of (FTSL1 n),(f . x)
proof
let x be
Element of
(FTSS2 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:
f .: (U_FT x) c= Im the
InternalRel of
(FTSL1 n),
(f . x)
proof
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 A17:
x2 in dom f
and A18:
x2 in Im (Nbds2 n,1),
x
and A19:
y = f . x2
by FUNCT_1:def 12;
consider u2,
v2 being
set such that
u2 in Seg n
and
v2 in Seg 1
and A20:
x2 = [u2,v2]
by A17, ZFMISC_1:def 2;
x2 = [(f . x2),1]
by A6, A17;
then A21:
u2 = f . x2
by A20, ZFMISC_1:33;
A22:
Im (Nbds2 n,1),
x = [:{u},(Im (Nbdl1 1),v):] \/ [:(Im (Nbdl1 n),u),{v}:]
by A13, A14, A15, Def4;
x = [(f . x),1]
by A6;
hence
y in Im the
InternalRel of
(FTSL1 n),
(f . x)
by A7, A15, A19, A21, A23, ZFMISC_1:33;
verum
end;
Im the
InternalRel of
(FTSL1 n),
(f . x) c= f .: (U_FT x)
proof
set X =
Im (Nbdl1 n),
u;
set Y =
Im (Nbdl1 1),
v;
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 A26:
y in Im the
InternalRel of
(FTSL1 n),
(f . x)
;
y in f .: (U_FT x)
Im (Nbdl1 n),
(f . x) c= rng f
by A7, A8, XBOOLE_1:1;
then consider x3 being
set such that A27:
x3 in dom f
and A28:
y = f . x3
by A7, A26, FUNCT_1:def 5;
set u2 =
f . x3;
set v2 = 1;
x = [(f . x),1]
by A6;
then A29:
f . x3 in Im (Nbdl1 n),
u
by A7, A15, A26, A28, ZFMISC_1:33;
A30:
Im (Nbds2 n,1),
x = [:{u},(Im (Nbdl1 1),v):] \/ [:(Im (Nbdl1 n),u),{v}:]
by A13, A14, A15, Def4;
( 1
<= nv &
nv <= 1 )
by A14, FINSEQ_1:3;
then A31:
nv = 1
by XXREAL_0:1;
A32:
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 A31, 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
1
in Im (Nbdl1 1),
v
by ZFMISC_1:37;
then
[(f . x3),1] in [:(Im (Nbdl1 n),u),(Im (Nbdl1 1),v):]
by A29, ZFMISC_1:def 2;
then A33:
[(f . x3),1] in [:(Im (Nbdl1 n),u),{v}:] \/ [:{u},(Im (Nbdl1 1),v):]
by A31, A32, XBOOLE_0:def 3;
x3 = [(f . x3),1]
by A6, A27;
hence
y in f .: (U_FT x)
by A27, A28, A33, A30, FUNCT_1:def 12;
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 A36:
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 A36, A12, Def1;
hence
ex h being Function of (FTSS2 n,1),(FTSL1 n) st h is being_homeomorphism
; verum