defpred S_{1}[ object , object ] means [$2,1] = $1;

let n be non zero Nat; :: thesis: 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 object st x in the carrier of (FTSS2 (n,1)) holds

ex y being object st

( y in the carrier of (FTSL1 n) & S_{1}[x,y] )

for x being object st x in the carrier of (FTSS2 (n,1)) holds

S_{1}[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 object st x in the carrier of (FTSS2 (n,1)) holds

S_{1}[x,f . x]
;

A7: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

A8: the carrier of (FTSL1 n) c= rng f

x1 = x2

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;

hence ex h being Function of (FTSS2 (n,1)),(FTSL1 n) st h is being_homeomorphism ; :: thesis: verum

let n be non zero Nat; :: thesis: 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 object st x in the carrier of (FTSS2 (n,1)) holds

ex y being object st

( y in the carrier of (FTSL1 n) & S

proof

ex f being Function of (FTSS2 (n,1)),(FTSL1 n) st
let x be object ; :: thesis: ( x in the carrier of (FTSS2 (n,1)) implies ex y being object st

( y in the carrier of (FTSL1 n) & S_{1}[x,y] ) )

A2: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

assume x in the carrier of (FTSS2 (n,1)) ; :: thesis: ex y being object st

( y in the carrier of (FTSL1 n) & S_{1}[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 S_{1}[x,nu]
by A5, XXREAL_0:1;

hence ex y being object st

( y in the carrier of (FTSL1 n) & S_{1}[x,y] )
by A3, A2; :: thesis: verum

end;( y in the carrier of (FTSL1 n) & S

A2: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

assume x in the carrier of (FTSS2 (n,1)) ; :: thesis: ex y being object st

( y in the carrier of (FTSL1 n) & S

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 S

hence ex y being object st

( y in the carrier of (FTSL1 n) & S

for x being object st x in the carrier of (FTSS2 (n,1)) holds

S

then consider f being Function of (FTSS2 (n,1)),(FTSL1 n) such that

A6: for x being object st x in the carrier of (FTSS2 (n,1)) holds

S

A7: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def 4;

A8: the carrier of (FTSL1 n) c= rng f

proof

A12:
for x being Element of (FTSS2 (n,1)) holds f .: (U_FT x) = Im ( the InternalRel of (FTSL1 n),(f . x))
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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 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; :: thesis: verum

end;set z = [x,1];

A9: 1 in Seg 1 ;

assume x in the carrier of (FTSL1 n) ; :: thesis: 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 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; :: thesis: verum

proof

for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
let x be Element of (FTSS2 (n,1)); :: thesis: 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: f .: (U_FT x) c= Im ( the InternalRel of (FTSL1 n),(f . x))

end;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: f .: (U_FT x) c= Im ( the InternalRel of (FTSL1 n),(f . x))

proof

Im ( the InternalRel of (FTSL1 n),(f . x)) c= f .: (U_FT x)
let y be object ; :: 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 object 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 6;

consider u2, v2 being object 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, XTUPLE_0:1;

A22: Im ((Nbds2 (n,1)),x) = [:{u},(Im ((Nbdl1 1),v)):] \/ [:(Im ((Nbdl1 n),u)),{v}:] by A13, A14, A15, Def4;

hence y in Im ( the InternalRel of (FTSL1 n),(f . x)) by A7, A15, A19, A21, A23, XTUPLE_0:1; :: thesis: verum

end;assume y in f .: (U_FT x) ; :: thesis: y in Im ( the InternalRel of (FTSL1 n),(f . x))

then consider x2 being object 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 6;

consider u2, v2 being object 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, XTUPLE_0:1;

A22: Im ((Nbds2 (n,1)),x) = [:{u},(Im ((Nbdl1 1),v)):] \/ [:(Im ((Nbdl1 n),u)),{v}:] by A13, A14, A15, Def4;

A23: now :: thesis: u2 in Class ((Nbdl1 n),u)end;

x = [(f . x),1]
by A6;per cases
( [u2,v2] in [:{u},(Im ((Nbdl1 1),v)):] or [u2,v2] in [:(Im ((Nbdl1 n),u)),{v}:] )
by A18, A22, A20, XBOOLE_0:def 3;

end;

suppose A24:
[u2,v2] in [:{u},(Im ((Nbdl1 1),v)):]
; :: thesis: u2 in Class ((Nbdl1 n),u)

reconsider pu = u as Element of (FTSL1 n) by A7, A13;

FTSL1 n is filled by FINTOPO4:18;

then A25: u in U_FT pu ;

u2 in {u} by A24, ZFMISC_1:87;

hence u2 in Class ((Nbdl1 n),u) by A7, A25, TARSKI:def 1; :: thesis: verum

end;FTSL1 n is filled by FINTOPO4:18;

then A25: u in U_FT pu ;

u2 in {u} by A24, ZFMISC_1:87;

hence u2 in Class ((Nbdl1 n),u) by A7, A25, TARSKI:def 1; :: thesis: verum

hence y in Im ( the InternalRel of (FTSL1 n),(f . x)) by A7, A15, A19, A21, A23, XTUPLE_0:1; :: thesis: verum

proof

hence
f .: (U_FT x) = Im ( the InternalRel of (FTSL1 n),(f . x))
by A16, XBOOLE_0:def 10; :: thesis: verum
set X = Im ((Nbdl1 n),u);

set Y = Im ((Nbdl1 1),v);

reconsider nv = v as Nat by A14;

let y be object ; :: 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 A26: 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 A7, A8;

then consider x3 being object such that

A27: x3 in dom f and

A28: y = f . x3 by A7, A26, FUNCT_1:def 3;

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, XTUPLE_0:1;

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:1;

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: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 1 in Im ((Nbdl1 1),v) by ZFMISC_1:31;

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 6; :: thesis: verum

end;set Y = Im ((Nbdl1 1),v);

reconsider nv = v as Nat by A14;

let y be object ; :: 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 A26: 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 A7, A8;

then consider x3 being object such that

A27: x3 in dom f and

A28: y = f . x3 by A7, A26, FUNCT_1:def 3;

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, XTUPLE_0:1;

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:1;

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: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 1 in Im ((Nbdl1 1),v) by ZFMISC_1:31;

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 6; :: thesis: verum

x1 = x2

proof

then A36:
f is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )

assume that

A34: x1 in dom f and

A35: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

[(f . x1),1] = x1 by A6, A34;

hence x1 = x2 by A6, A35; :: thesis: verum

end;assume that

A34: x1 in dom f and

A35: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2

[(f . x1),1] = x1 by A6, A34;

hence x1 = x2 by A6, A35; :: thesis: verum

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;

hence ex h being Function of (FTSS2 (n,1)),(FTSL1 n) st h is being_homeomorphism ; :: thesis: verum