defpred S1[ object , object ] means [\$2,1] = \$1;
let n be non zero Nat; :: thesis: ex h being Function of (FTSL2 (n,1)),() 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 () & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (FTSL2 (n,1)) implies ex y being object st
( y in the carrier of () & S1[x,y] ) )

A2: FTSL1 n = RelStr(# (Seg n),() #) by FINTOPO4:def 4;
assume x in the carrier of (FTSL2 (n,1)) ; :: thesis: ex y being object st
( y in the carrier of () & 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 ;
then S1[x,nu] by A5, XXREAL_0:1;
hence ex y being object st
( y in the carrier of () & S1[x,y] ) by A3, A2; :: thesis: verum
end;
ex f being Function of (FTSL2 (n,1)),() st
for x being object st x in the carrier of (FTSL2 (n,1)) holds
S1[x,f . x] from then consider f being Function of (FTSL2 (n,1)),() 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),() #) by FINTOPO4:def 4;
A8: the carrier of () c= rng f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of () or x in rng f )
set z = [x,1];
A9: 1 in Seg 1 ;
assume x in the carrier of () ; :: thesis: x in rng f
then A10: [x,1] in the carrier of (FTSL2 (n,1)) by ;
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 ;
hence x in rng f by ; :: thesis: verum
end;
A12: for x being Element of (FTSL2 (n,1)) holds f .: (U_FT x) = Im ( the InternalRel of (),(f . x))
proof
let x be Element of (FTSL2 (n,1)); :: thesis: f .: (U_FT x) = Im ( the InternalRel of (),(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 (),(f . x)) c= f .: (U_FT x)
proof
reconsider nv = v as Nat by A14;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Im ( the InternalRel of (),(f . x)) or y in f .: (U_FT x) )
assume A17: y in Im ( the InternalRel of (),(f . x)) ; :: thesis: y in f .: (U_FT x)
( 1 <= nv & nv <= 1 ) by ;
then A18: nv = 1 by XXREAL_0:1;
Im ((),(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 ;
set u2 = f . x3;
set v2 = 1;
Im ((),v) = {nv,(max ((nv -' 1),1)),(min ((nv + 1),1))} by
.= {1,(max (0,1)),(min (2,1))} by
.= {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 ((),v) by ZFMISC_1:31;
A22: Im ((Nbdl2 (n,1)),x) = [:(Im ((),u)),(Im ((),v)):] by ;
x = [(f . x),1] by A6;
then f . x3 in Im ((),u) by ;
then A23: [(f . x3),1] in [:(Im ((),u)),(Im ((),v)):] by ;
x3 = [(f . x3),1] by ;
hence y in f .: (U_FT x) by ; :: thesis: verum
end;
f .: (U_FT x) c= Im ( the InternalRel of (),(f . x))
proof
x = [(f . x),1] by A6;
then A24: u = f . x by ;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (U_FT x) or y in Im ( the InternalRel of (),(f . x)) )
assume y in f .: (U_FT x) ; :: thesis: y in Im ( the InternalRel of (),(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 ((),u)),(Im ((),v)):] by ;
x2 = [(f . x2),1] by ;
hence y in Im ( the InternalRel of (),(f . x)) by ; :: thesis: verum
end;
hence f .: (U_FT x) = Im ( the InternalRel of (),(f . x)) by ; :: thesis: verum
end;
for x1, x2 being object st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume that
A28: x1 in dom f and
A29: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
[(f . x1),1] = x1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
then A30: f is one-to-one by FUNCT_1:def 4;
rng f = the carrier of () by ;
then f is onto by FUNCT_2:def 3;
then f is being_homeomorphism by ;
hence ex h being Function of (FTSL2 (n,1)),() st h is being_homeomorphism ; :: thesis: verum