defpred S1[ object , object ] means [\$2,1] = \$1;
let n be non zero Nat; :: thesis: ex h being Function of (FTSS2 (n,1)),() 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 () & S1[x,y] )
proof
let x be object ; :: thesis: ( x in the carrier of (FTSS2 (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 (FTSS2 (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 (FTSS2 (n,1)),() st
for x being object st x in the carrier of (FTSS2 (n,1)) holds
S1[x,f . x] from then consider f being Function of (FTSS2 (n,1)),() such that
A6: for x being object st x in the carrier of (FTSS2 (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 (FTSS2 (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 (FTSS2 (n,1)) holds f .: (U_FT x) = Im ( the InternalRel of (),(f . x))
proof
let x be Element of (FTSS2 (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: f .: (U_FT x) c= Im ( the InternalRel of (),(f . x))
proof
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
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 ;
x2 = [(f . x2),1] by ;
then A21: u2 = f . x2 by ;
A22: Im ((Nbds2 (n,1)),x) = [:{u},(Im ((),v)):] \/ [:(Im ((),u)),{v}:] by ;
A23: now :: thesis: u2 in Class ((),u)
per cases ( [u2,v2] in [:{u},(Im ((),v)):] or [u2,v2] in [:(Im ((),u)),{v}:] ) by ;
suppose A24: [u2,v2] in [:{u},(Im ((),v)):] ; :: thesis: u2 in Class ((),u)
reconsider pu = u as Element of () by ;
FTSL1 n is filled by FINTOPO4:18;
then A25: u in U_FT pu ;
u2 in {u} by ;
hence u2 in Class ((),u) by ; :: thesis: verum
end;
suppose [u2,v2] in [:(Im ((),u)),{v}:] ; :: thesis: u2 in Class ((),u)
hence u2 in Class ((),u) by ZFMISC_1:87; :: thesis: verum
end;
end;
end;
x = [(f . x),1] by A6;
hence y in Im ( the InternalRel of (),(f . x)) by ; :: thesis: verum
end;
Im ( the InternalRel of (),(f . x)) c= f .: (U_FT x)
proof
set X = Im ((),u);
set Y = Im ((),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 (),(f . x)) or y in f .: (U_FT x) )
assume A26: y in Im ( the InternalRel of (),(f . x)) ; :: thesis: y in f .: (U_FT x)
Im ((),(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 ;
set u2 = f . x3;
set v2 = 1;
x = [(f . x),1] by A6;
then A29: f . x3 in Im ((),u) by ;
A30: Im ((Nbds2 (n,1)),x) = [:{u},(Im ((),v)):] \/ [:(Im ((),u)),{v}:] by ;
( 1 <= nv & nv <= 1 ) by ;
then A31: nv = 1 by XXREAL_0:1;
A32: 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 1 in Im ((),v) by ZFMISC_1:31;
then [(f . x3),1] in [:(Im ((),u)),(Im ((),v)):] by ;
then A33: [(f . x3),1] in [:(Im ((),u)),{v}:] \/ [:{u},(Im ((),v)):] by ;
x3 = [(f . x3),1] by ;
hence y in f .: (U_FT 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
A34: x1 in dom f and
A35: ( x2 in dom f & f . x1 = f . x2 ) ; :: thesis: x1 = x2
[(f . x1),1] = x1 by ;
hence x1 = x2 by ; :: thesis: verum
end;
then A36: 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 (FTSS2 (n,1)),() st h is being_homeomorphism ; :: thesis: verum