:: FINTOPO5 semantic presentation

begin

theorem Th1: :: FINTOPO5:1
for X being set
for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
(f ") .: (f .: A) = A
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
(f ") .: (f .: A) = A
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for A being Subset of X st f is one-to-one holds
(f ") .: (f .: A) = A
let f be Function of X,Y; ::_thesis: for A being Subset of X st f is one-to-one holds
(f ") .: (f .: A) = A
let A be Subset of X; ::_thesis: ( f is one-to-one implies (f ") .: (f .: A) = A )
A1: dom f = X by FUNCT_2:def_1;
assume  f is one-to-one ; ::_thesis: (f ") .: (f .: A) = A
hence  (f ") .: (f .: A) = A by A1, FUNCT_1:107; ::_thesis: verum
end;

theorem :: FINTOPO5:2
for n being Element of NAT holds
( n > 0 iff Seg n <> {} ) ;

definition
let FT1, FT2 be RelStr ;
let h be Function of FT1,FT2;
attrh is being_homeomorphism  means :Def1: :: FINTOPO5:def 1
( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) );
end;

:: deftheorem Def1 defines being_homeomorphism FINTOPO5:def_1_:_
 for FT1, FT2 being RelStr
for h being Function of FT1,FT2 holds
( h is being_homeomorphism iff ( h is one-to-one & h is onto & ( for x being Element of FT1 holds h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) ) );

theorem Th3: :: FINTOPO5:3
for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2 st h is being_homeomorphism holds
ex g being Function of FT2,FT1 st
( g = h " & g is being_homeomorphism )
proof
let FT1, FT2 be non empty RelStr ; ::_thesis: for h being Function of FT1,FT2 st h is being_homeomorphism holds
ex g being Function of FT2,FT1 st
( g = h " & g is being_homeomorphism )
let h be Function of FT1,FT2; ::_thesis: ( h is being_homeomorphism implies ex g being Function of FT2,FT1 st
( g = h " & g is being_homeomorphism ) )
assume A1: h is being_homeomorphism ; ::_thesis: ex g being Function of FT2,FT1 st
( g = h " & g is being_homeomorphism )
then A2: ( h is one-to-one & h is onto ) by Def1;
then A3: rng h = the carrier of FT2 by FUNCT_2:def_3;
then reconsider g2 = h " as Function of FT2,FT1 by A2, FUNCT_2:25;
A4: for y being Element of FT2 holds g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y))
proof
let y be Element of FT2; ::_thesis: g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y))
reconsider x = g2 . y as Element of FT1 ;
 ( y = h . x & h .: (U_FT x) = Im ( the InternalRel of FT2,(h . x)) ) by A1, A2, A3, Def1, FUNCT_1:35;
hence  g2 .: (U_FT y) = Im ( the InternalRel of FT1,(g2 . y)) by A2, Th1; ::_thesis: verum
end;
rng g2 = dom h by A2, FUNCT_1:33
.= the carrier of FT1 by FUNCT_2:def_1 ;
then A5: g2 is onto by FUNCT_2:def_3;
 g2 is one-to-one by A2, FUNCT_1:40;
then  g2 is being_homeomorphism by A5, A4, Def1;
hence  ex g being Function of FT2,FT1 st
( g = h " & g is being_homeomorphism ) ; ::_thesis: verum
end;

theorem Th4: :: FINTOPO5:4
for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
proof
let FT1, FT2 be non empty RelStr ; ::_thesis: for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
let h be Function of FT1,FT2; ::_thesis: for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
let n be Element of NAT ; ::_thesis: for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
let x be Element of FT1; ::_thesis: for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
let y be Element of FT2; ::_thesis: ( h is being_homeomorphism & y = h . x implies for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) ) )
assume that
A1: h is being_homeomorphism and
A2: y = h . x ; ::_thesis: for z being Element of FT1 holds
( z in U_FT (x,n) iff h . z in U_FT (y,n) )
A3: ( h is one-to-one & h is onto ) by A1, Def1;
let z be Element of FT1; ::_thesis: ( z in U_FT (x,n) iff h . z in U_FT (y,n) )
 x in the carrier of FT1 ;
then A4: x in dom h by FUNCT_2:def_1;
 z in the carrier of FT1 ;
then A5: z in dom h by FUNCT_2:def_1;
A6: now__::_thesis:_(_h_._z_in_U_FT_(y,n)_implies_z_in_U_FT_(x,n)_)
defpred S1[ Element of NAT ] means  for w being Element of FT2 st w in U_FT (y,$1) holds
(h ") . w in U_FT (x,$1);
assume A7: h . z in U_FT (y,n) ; ::_thesis: z in U_FT (x,n)
consider g being Function of FT2,FT1 such that
A8: g = h " and
A9: g is being_homeomorphism by A1, Th3;
A10: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; ::_thesis: S1[k + 1]
 for w being Element of FT2 st w in U_FT (y,(k + 1)) holds
(h ") . w in U_FT (x,(k + 1))
proof
let w be Element of FT2; ::_thesis: ( w in U_FT (y,(k + 1)) implies (h ") . w in U_FT (x,(k + 1)) )
A12: U_FT (y,(k + 1)) = (U_FT (y,k)) ^f by FINTOPO3:48;
assume  w in U_FT (y,(k + 1)) ; ::_thesis: (h ") . w in U_FT (x,(k + 1))
then consider x3 being Element of FT2 such that
A13: x3 = w and
A14: ex y3 being Element of FT2 st
( y3 in U_FT (y,k) & x3 in U_FT y3 ) by A12;
consider y2 being Element of FT2 such that
A15: y2 in U_FT (y,k) and
A16: x3 in U_FT y2 by A14;
reconsider q = g . y2, p = g . x3 as Element of FT1 ;
A17: for w2 being Element of FT2 st w2 in U_FT (y2,0) holds
(h ") . w2 in U_FT (q,0)
proof
let w2 be Element of FT2; ::_thesis: ( w2 in U_FT (y2,0) implies (h ") . w2 in U_FT (q,0) )
 w2 in the carrier of FT2 ;
then A18: w2 in dom g by FUNCT_2:def_1;
A19: (h ") .: (U_FT y2) = Class ( the InternalRel of FT1,((h ") . y2)) by A8, A9, Def1;
hereby  ::_thesis: verum
assume  w2 in U_FT (y2,0) ; ::_thesis: (h ") . w2 in U_FT (q,0)
then  w2 in U_FT y2 by FINTOPO3:47;
then  (h ") . w2 in U_FT q by A8, A19, A18, FUNCT_1:def_6;
hence  (h ") . w2 in U_FT (q,0) by FINTOPO3:47; ::_thesis: verum
end;
end;
 x3 in U_FT (y2,0) by A16, FINTOPO3:47;
then  p in U_FT (q,0) by A8, A17;
then A20: p in U_FT q by FINTOPO3:47;
 q in U_FT (x,k) by A8, A11, A15;
then  p in (U_FT (x,k)) ^f by A20;
hence  (h ") . w in U_FT (x,(k + 1)) by A8, A13, FINTOPO3:48; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
A21: g . y = x by A2, A4, A3, A8, FUNCT_1:34;
 for w being Element of FT2 st w in U_FT (y,0) holds
(h ") . w in U_FT (x,0)
proof
let w be Element of FT2; ::_thesis: ( w in U_FT (y,0) implies (h ") . w in U_FT (x,0) )
 w in the carrier of FT2 ;
then A22: w in dom g by FUNCT_2:def_1;
A23: g .: (U_FT y) = Class ( the InternalRel of FT1,(g . y)) by A9, Def1;
hereby  ::_thesis: verum
assume  w in U_FT (y,0) ; ::_thesis: (h ") . w in U_FT (x,0)
then  w in U_FT y by FINTOPO3:47;
then  g . w in U_FT x by A21, A23, A22, FUNCT_1:def_6;
hence  (h ") . w in U_FT (x,0) by A8, FINTOPO3:47; ::_thesis: verum
end;
end;
then A24: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A24, A10);
then  (h ") . (h . z) in U_FT (x,n) by A7;
hence  z in U_FT (x,n) by A3, A5, FUNCT_1:34; ::_thesis: verum
end;
now__::_thesis:_(_z_in_U_FT_(x,n)_implies_h_._z_in_U_FT_(y,n)_)
defpred S1[ Element of NAT ] means  for w being Element of FT1 st w in U_FT (x,$1) holds
h . w in U_FT (y,$1);
assume A25: z in U_FT (x,n) ; ::_thesis: h . z in U_FT (y,n)
A26: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A27: S1[k] ; ::_thesis: S1[k + 1]
 for w being Element of FT1 st w in U_FT (x,(k + 1)) holds
h . w in U_FT (y,(k + 1))
proof
let w be Element of FT1; ::_thesis: ( w in U_FT (x,(k + 1)) implies h . w in U_FT (y,(k + 1)) )
A28: U_FT (x,(k + 1)) = (U_FT (x,k)) ^f by FINTOPO3:48;
assume  w in U_FT (x,(k + 1)) ; ::_thesis: h . w in U_FT (y,(k + 1))
then consider x3 being Element of FT1 such that
A29: x3 = w and
A30: ex y3 being Element of FT1 st
( y3 in U_FT (x,k) & x3 in U_FT y3 ) by A28;
consider y2 being Element of FT1 such that
A31: y2 in U_FT (x,k) and
A32: x3 in U_FT y2 by A30;
reconsider q = h . y2, p = h . x3 as Element of FT2 ;
A33: for w2 being Element of FT1 st w2 in U_FT (y2,0) holds
h . w2 in U_FT (q,0)
proof
let w2 be Element of FT1; ::_thesis: ( w2 in U_FT (y2,0) implies h . w2 in U_FT (q,0) )
 w2 in the carrier of FT1 ;
then A34: w2 in dom h by FUNCT_2:def_1;
A35: h .: (U_FT y2) = Class ( the InternalRel of FT2,(h . y2)) by A1, Def1;
hereby  ::_thesis: verum
assume  w2 in U_FT (y2,0) ; ::_thesis: h . w2 in U_FT (q,0)
then  w2 in U_FT y2 by FINTOPO3:47;
then  h . w2 in U_FT q by A35, A34, FUNCT_1:def_6;
hence  h . w2 in U_FT (q,0) by FINTOPO3:47; ::_thesis: verum
end;
end;
 x3 in U_FT (y2,0) by A32, FINTOPO3:47;
then  p in U_FT (q,0) by A33;
then A36: p in U_FT q by FINTOPO3:47;
 q in U_FT (y,k) by A27, A31;
then  p in (U_FT (y,k)) ^f by A36;
hence  h . w in U_FT (y,(k + 1)) by A29, FINTOPO3:48; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for w being Element of FT1 st w in U_FT (x,0) holds
h . w in U_FT (y,0)
proof
let w be Element of FT1; ::_thesis: ( w in U_FT (x,0) implies h . w in U_FT (y,0) )
 w in the carrier of FT1 ;
then A37: w in dom h by FUNCT_2:def_1;
A38: h .: (U_FT x) = Class ( the InternalRel of FT2,(h . x)) by A1, Def1;
hereby  ::_thesis: verum
assume  w in U_FT (x,0) ; ::_thesis: h . w in U_FT (y,0)
then  w in U_FT x by FINTOPO3:47;
then  h . w in U_FT y by A2, A38, A37, FUNCT_1:def_6;
hence  h . w in U_FT (y,0) by FINTOPO3:47; ::_thesis: verum
end;
end;
then A39: S1[ 0 ] ;
 for k being Element of NAT holds S1[k] from NAT_1:sch_1(A39, A26);
hence  h . z in U_FT (y,n) by A25; ::_thesis: verum
end;
hence  ( z in U_FT (x,n) iff h . z in U_FT (y,n) ) by A6; ::_thesis: verum
end;

theorem :: FINTOPO5:5
for FT1, FT2 being non empty RelStr
for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )
proof
let FT1, FT2 be non empty RelStr ; ::_thesis: for h being Function of FT1,FT2
for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )
let h be Function of FT1,FT2; ::_thesis: for n being Element of NAT
for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )
let n be Element of NAT ; ::_thesis: for x being Element of FT1
for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )
let x be Element of FT1; ::_thesis: for y being Element of FT2 st h is being_homeomorphism & y = h . x holds
for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )
let y be Element of FT2; ::_thesis: ( h is being_homeomorphism & y = h . x implies for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) ) )
assume that
A1: h is being_homeomorphism and
A2: y = h . x ; ::_thesis: for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) )
 x in the carrier of FT1 ;
then A3: x in dom h by FUNCT_2:def_1;
consider g being Function of FT2,FT1 such that
A4: g = h " and
A5: g is being_homeomorphism by A1, Th3;
 ( h is one-to-one & h is onto ) by A1, Def1;
then  x = g . y by A2, A4, A3, FUNCT_1:34;
hence  for v being Element of FT2 holds
( (h ") . v in U_FT (x,n) iff v in U_FT (y,n) ) by A4, A5, Th4; ::_thesis: verum
end;

theorem :: FINTOPO5:6
for n being non zero Element of NAT
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous 0 holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)
proof
let n be non zero Element of NAT ; ::_thesis: for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous 0 holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)
let f be Function of (FTSL1 n),(FTSL1 n); ::_thesis: ( f is_continuous 0 implies ex p being Element of (FTSL1 n) st f . p in U_FT (p,0) )
assume A1: f is_continuous 0 ; ::_thesis: ex p being Element of (FTSL1 n) st f . p in U_FT (p,0)
assume A2: for p being Element of (FTSL1 n) holds not f . p in U_FT (p,0) ; ::_thesis: contradiction
defpred S1[ Nat] means ( $1 > 0 & ( for j being Nat st $1 <= n & j = f . $1 holds
$1 > j ) );
A3: n >= 0 + 1 by NAT_1:13;
A4: RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n by FINTOPO4:def_4;
A5: FTSL1 n is filled by FINTOPO4:18;
now__::_thesis:_for_j_being_Nat_holds_
(_not_j_=_f_._n_or_not_n_<=_j_)
A6: n in the carrier of (FTSL1 n) by A3, A4;
then reconsider p2 = n as Element of (FTSL1 n) ;
 p2 in U_FT p2 by A5, FIN_TOPO:def_4;
then A7: p2 in U_FT (p2,0) by FINTOPO3:47;
given j being Nat such that A8: j = f . n and
A9: n <= j ; ::_thesis: contradiction
 f . n in the carrier of (FTSL1 n) by A6, FUNCT_2:5;
then  j <= n by A4, A8, FINSEQ_1:1;
then  n = j by A9, XXREAL_0:1;
hence  contradiction by A2, A8, A7; ::_thesis: verum
end;
then A10: for j being Nat st n <= n & j = f . n holds
n > j ;
then A11: ex k being Nat st S1[k] ;
 ex k being Nat st
( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from NAT_1:sch_5(A11);
then consider k being Nat such that
A12: S1[k] and
A13: for m being Nat st S1[m] holds
k <= m ;
A14: 0 + 1 <= k by A12, NAT_1:13;
then A15: k - 1 >= 0 by XREAL_1:48;
then A16: k - 1 = k -' 1 by XREAL_0:def_2;
A17: k <= n by A10, A13;
then reconsider pk = k as Element of (FTSL1 n) by A4, A14, FINSEQ_1:1;
 k < k + 1 by NAT_1:13;
then A18: k - 1 < (k + 1) - 1 by XREAL_1:9;
now__::_thesis:_(_(_k_-'_1_<=_0_&_contradiction_)_or_(_k_-'_1_>_0_&_ex_j_being_Nat_st_
(_k_-'_1_<=_n_&_j_=_f_._(k_-'_1)_&_k_-'_1_<=_j_)_&_contradiction_)_)
percases ( k -' 1 <= 0 or ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ) by A13, A16, A18;
caseA19: k -' 1 <= 0 ; ::_thesis: contradiction
 1 in the carrier of (FTSL1 n) by A3, A4;
then A20: f . 1 in Seg n by A4, FUNCT_2:5;
then reconsider j0 = f . 1 as Element of NAT ;
 k - 1 = 0 by A15, A19, XREAL_0:def_2;
then  1 > j0 by A3, A12;
hence  contradiction by A20, FINSEQ_1:1; ::_thesis: verum
end;
caseA21: ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ; ::_thesis: contradiction
 k in NAT by ORDINAL1:def_12;
then A22: k in the carrier of (FTSL1 n) by A4, A17, A14;
then A23: f . k in Seg n by A4, FUNCT_2:5;
then reconsider jn = f . k as Element of NAT ;
 jn < jn + 1 by NAT_1:13;
then A24: jn - 1 < (jn + 1) - 1 by XREAL_1:9;
A25: k -' 1 >= 0 + 1 by A21, NAT_1:13;
then A26: ( k -' 1 = k or k -' 1 = max ((k -' 1),1) or k -' 1 = min ((k + 1),n) ) by XXREAL_0:def_10;
consider j being Nat such that
A27: k -' 1 <= n and
A28: j = f . (k -' 1) and
A29: k -' 1 <= j by A21;
reconsider pkm = k -' 1 as Element of (FTSL1 n) by A4, A27, A25, FINSEQ_1:1;
 k -' 1 in Seg n by A27, A25;
then A30: Im ((Nbdl1 n),pkm) = {(k -' 1),(max (((k -' 1) -' 1),1)),(min (((k -' 1) + 1),n))} by FINTOPO4:def_3;
 Im ((Nbdl1 n),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by A4, A22, FINTOPO4:def_3;
then  k -' 1 in U_FT pk by A4, A26, ENUMSET1:def_1;
then A31: k -' 1 in U_FT (pk,0) by FINTOPO3:47;
reconsider pfk = jn as Element of (FTSL1 n) by A22, FUNCT_2:5;
A32: f .: (U_FT (pk,0)) c= U_FT (pfk,0) by A1, FINTOPO4:def_2;
A33: jn < k by A12, A17;
then A34: jn + 1 <= k by NAT_1:13;
A35: k -' 1 in the carrier of (FTSL1 n) by A4, A27, A25;
now__::_thesis:_not_k_-'_1_=_j
assume A36: k -' 1 = j ; ::_thesis: contradiction
then reconsider pj = j as Element of (FTSL1 n) by A35;
 pj in U_FT pj by A5, FIN_TOPO:def_4;
then  f . j in U_FT (pj,0) by A28, A36, FINTOPO3:47;
hence  contradiction by A2; ::_thesis: verum
end;
then  k -' 1 < j by A29, XXREAL_0:1;
then A37: (k -' 1) + 1 <= j by NAT_1:13;
then A38: jn < j by A16, A33, XXREAL_0:2;
 j in the carrier of (FTSL1 n) by A28, A35, FUNCT_2:5;
then A39: j <= n by A4, FINSEQ_1:1;
now__::_thesis:_not_k_=_j
assume A40: k = j ; ::_thesis: contradiction
then  min (((k -' 1) + 1),n) = (k -' 1) + 1 by A16, A39, XXREAL_0:def_9;
then  k in U_FT pkm by A4, A16, A30, ENUMSET1:def_1;
then  f . (k -' 1) in U_FT (pkm,0) by A28, A40, FINTOPO3:47;
hence  contradiction by A2; ::_thesis: verum
end;
then A41: k < j by A16, A37, XXREAL_0:1;
A42: now__::_thesis:_(_(_jn_+_1_<=_n_&_j_<>_min_((jn_+_1),n)_)_or_(_jn_+_1_>_n_&_j_<>_min_((jn_+_1),n)_)_)
percases ( jn + 1 <= n or jn + 1 > n ) ;
case jn + 1 <= n ; ::_thesis: j <> min ((jn + 1),n)
hence  j <> min ((jn + 1),n) by A41, A34, XXREAL_0:def_9; ::_thesis: verum
end;
caseA43: jn + 1 > n ; ::_thesis: j <> min ((jn + 1),n)
then  jn >= n by NAT_1:13;
hence  j <> min ((jn + 1),n) by A38, A43, XXREAL_0:def_9; ::_thesis: verum
end;
end;
end;
A44: 1 <= jn by A23, FINSEQ_1:1;
then  jn - 1 >= 0 by XREAL_1:48;
then A45: jn - 1 = jn -' 1 by XREAL_0:def_2;
A46: now__::_thesis:_j_<>_max_((jn_-'_1),1)
percases ( jn -' 1 >= 1 or jn -' 1 < 1 ) ;
suppose jn -' 1 >= 1 ; ::_thesis: j <> max ((jn -' 1),1)
hence  j <> max ((jn -' 1),1) by A38, A45, A24, XXREAL_0:def_10; ::_thesis: verum
end;
suppose jn -' 1 < 1 ; ::_thesis: j <> max ((jn -' 1),1)
hence  j <> max ((jn -' 1),1) by A44, A38, XXREAL_0:def_10; ::_thesis: verum
end;
end;
end;
 k -' 1 in dom f by A35, FUNCT_2:def_1;
then  f . (k -' 1) in f .: (U_FT (pk,0)) by A31, FUNCT_1:def_6;
then A47: j in U_FT (pfk,0) by A28, A32;
 Im ((Nbdl1 n),jn) = {jn,(max ((jn -' 1),1)),(min ((jn + 1),n))} by A23, FINTOPO4:def_3;
then  not j in U_FT pfk by A4, A16, A37, A33, A46, A42, ENUMSET1:def_1;
hence  contradiction by A47, FINTOPO3:47; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

theorem Th7: :: FINTOPO5:7
for T being non empty RelStr
for p being Element of T
for k being Element of NAT st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))
proof
let T be non empty RelStr ; ::_thesis: for p being Element of T
for k being Element of NAT st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))
let p be Element of T; ::_thesis: for k being Element of NAT st T is filled holds
U_FT (p,k) c= U_FT (p,(k + 1))
let k be Element of NAT ; ::_thesis: ( T is filled implies U_FT (p,k) c= U_FT (p,(k + 1)) )
A1: U_FT (p,(k + 1)) = (U_FT (p,k)) ^f by FINTOPO3:48;
assume  T is filled ; ::_thesis: U_FT (p,k) c= U_FT (p,(k + 1))
hence  U_FT (p,k) c= U_FT (p,(k + 1)) by A1, FINTOPO3:1; ::_thesis: verum
end;

theorem Th8: :: FINTOPO5:8
for T being non empty RelStr
for p being Element of T
for k being Element of NAT st T is filled holds
U_FT (p,0) c= U_FT (p,k)
proof
let T be non empty RelStr ; ::_thesis: for p being Element of T
for k being Element of NAT st T is filled holds
U_FT (p,0) c= U_FT (p,k)
let p be Element of T; ::_thesis: for k being Element of NAT st T is filled holds
U_FT (p,0) c= U_FT (p,k)
let k be Element of NAT ; ::_thesis: ( T is filled implies U_FT (p,0) c= U_FT (p,k) )
defpred S1[ Element of NAT ] means  U_FT (p,0) c= U_FT (p,$1);
assume A1: T is filled ; ::_thesis: U_FT (p,0) c= U_FT (p,k)
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
 U_FT (p,k) c= U_FT (p,(k + 1)) by A1, Th7;
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
A4: S1[ 0 ] ;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A4, A2);
hence  U_FT (p,0) c= U_FT (p,k) ; ::_thesis: verum
end;

theorem Th9: :: FINTOPO5:9
for n being non zero Nat
for jn, j, k being Nat
for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n & abs (jn - j) <= k + 1 ) )
proof
let n be non zero Nat; ::_thesis: for jn, j, k being Nat
for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n & abs (jn - j) <= k + 1 ) )
let jn, j, k be Nat; ::_thesis: for p being Element of (FTSL1 n) st p = jn holds
( j in U_FT (p,k) iff ( j in Seg n & abs (jn - j) <= k + 1 ) )
let p be Element of (FTSL1 n); ::_thesis: ( p = jn implies ( j in U_FT (p,k) iff ( j in Seg n & abs (jn - j) <= k + 1 ) ) )
A1: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def_4;
assume A2: p = jn ; ::_thesis: ( j in U_FT (p,k) iff ( j in Seg n & abs (jn - j) <= k + 1 ) )
A3: now__::_thesis:_(_j_in_Seg_n_&_abs_(jn_-_j)_<=_k_+_1_implies_j_in_U_FT_(p,k)_)
defpred S1[ Nat] means  for j2, jn2 being Nat
for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= $1 + 1 holds
j2 in U_FT (p2,$1);
A4: S1[ 0 ]
proof
let j2, jn2 be Nat; ::_thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= 0 + 1 holds
j2 in U_FT (p2,0)
let p2 be Element of (FTSL1 n); ::_thesis: ( jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= 0 + 1 implies j2 in U_FT (p2,0) )
assume that
A5: jn2 = p2 and
A6: j2 in Seg n and
A7: abs (jn2 - j2) <= 0 + 1 ; ::_thesis: j2 in U_FT (p2,0)
A8: j2 <= n by A6, FINSEQ_1:1;
A9: 1 <= j2 by A6, FINSEQ_1:1;
now__::_thesis:_(_(_jn2_-_j2_>=_0_&_(_j2_=_jn2_or_j2_=_max_((jn2_-'_1),1)_or_j2_=_min_((jn2_+_1),n)_)_)_or_(_jn2_-_j2_<_0_&_(_j2_=_jn2_or_j2_=_max_((jn2_-'_1),1)_or_j2_=_min_((jn2_+_1),n)_)_)_)
percases ( jn2 - j2 >= 0 or jn2 - j2 < 0 ) ;
case jn2 - j2 >= 0 ; ::_thesis: verum
then A10: jn2 - j2 = jn2 -' j2 by XREAL_0:def_2;
A11: ( jn2 -' j2 >= 0 + 1 or jn2 -' j2 = 0 ) by NAT_1:13;
 jn2 - j2 <= 1 by A7, ABSVALUE:def_1;
then A12: ( jn2 - j2 = 1 or jn2 -' j2 = 0 ) by A10, A11, XXREAL_0:1;
percases ( jn2 - 1 = j2 or jn2 = j2 ) by A10, A12;
supposeA13: jn2 - 1 = j2 ; ::_thesis: ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) )
then  jn2 - 1 = jn2 -' 1 by XREAL_0:def_2;
hence  ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) by A9, A13, XXREAL_0:def_10; ::_thesis: verum
end;
suppose jn2 = j2 ; ::_thesis: ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) )
hence  ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) ; ::_thesis: verum
end;
end;
end;
caseA14: jn2 - j2 < 0 ; ::_thesis: ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) )
then  (jn2 - j2) + j2 < 0 + j2 by XREAL_1:8;
then A15: jn2 + 1 <= j2 by NAT_1:13;
 - (jn2 - j2) <= 1 by A7, A14, ABSVALUE:def_1;
then  (j2 - jn2) + jn2 <= 1 + jn2 by XREAL_1:7;
then  jn2 + 1 = j2 by A15, XXREAL_0:1;
hence  ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) by A8, XXREAL_0:def_9; ::_thesis: verum
end;
end;
end;
then  ( jn2 in NAT & j2 in {jn2,(max ((jn2 -' 1),1)),(min ((jn2 + 1),n))} ) by ENUMSET1:def_1, ORDINAL1:def_12;
then  j2 in U_FT p2 by A1, A5, FINTOPO4:def_3;
hence  j2 in U_FT (p2,0) by FINTOPO3:47; ::_thesis: verum
end;
A16: for jj being Nat st S1[jj] holds
S1[jj + 1]
proof
let jj be Nat; ::_thesis: ( S1[jj] implies S1[jj + 1] )
assume A17: S1[jj] ; ::_thesis: S1[jj + 1]
let j2, jn2 be Nat; ::_thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= (jj + 1) + 1 holds
j2 in U_FT (p2,(jj + 1))
let p2 be Element of (FTSL1 n); ::_thesis: ( jn2 = p2 & j2 in Seg n & abs (jn2 - j2) <= (jj + 1) + 1 implies j2 in U_FT (p2,(jj + 1)) )
assume that
A18: jn2 = p2 and
A19: j2 in Seg n and
A20: abs (jn2 - j2) <= (jj + 1) + 1 ; ::_thesis: j2 in U_FT (p2,(jj + 1))
A21: j2 <= n by A19, FINSEQ_1:1;
reconsider x0 = j2 as Element of (FTSL1 n) by A1, A19;
A22: 1 <= j2 by A19, FINSEQ_1:1;
A23: jn2 <= n by A1, A18, FINSEQ_1:1;
A24: 1 <= jn2 by A1, A18, FINSEQ_1:1;
A25: now__::_thesis:_ex_y_being_Element_of_(FTSL1_n)_st_
(_y_in_U_FT_(p2,jj)_&_x0_in_U_FT_y_)
percases ( jn2 - j2 >= 0 or jn2 - j2 < 0 ) ;
supposeA26: jn2 - j2 >= 0 ; ::_thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )
percases ( jn2 - j2 = 0 or jn2 - j2 > 0 ) by A26;
supposeA27: jn2 - j2 = 0 ; ::_thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )
 FTSL1 n is filled by FINTOPO4:18;
then A28: x0 in U_FT p2 by A18, A27, FIN_TOPO:def_4;
 abs (jn2 - j2) <= jj + 1 by A27, ABSVALUE:def_1;
hence  ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y ) by A17, A18, A19, A27, A28; ::_thesis: verum
end;
supposeA29: jn2 - j2 > 0 ; ::_thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )
then  jn2 - j2 = jn2 -' j2 by XREAL_0:def_2;
then A30: jn2 - j2 >= 0 + 1 by A29, NAT_1:13;
then  (jn2 - j2) + j2 >= 1 + j2 by XREAL_1:7;
then A31: n >= j2 + 1 by A23, XXREAL_0:2;
 j2 < j2 + 1 by NAT_1:13;
then A32: jn2 - (j2 + 1) < jn2 - j2 by XREAL_1:15;
 abs (jn2 - j2) = jn2 - j2 by A29, ABSVALUE:def_1;
then A33: jn2 - (j2 + 1) < (jj + 1) + 1 by A20, A32, XXREAL_0:2;
A34: (jn2 - j2) - 1 >= 1 - 1 by A30, XREAL_1:9;
then  jn2 -' (j2 + 1) = jn2 - (j2 + 1) by XREAL_0:def_2;
then  jn2 - (j2 + 1) <= jj + 1 by A33, NAT_1:13;
then A35: abs (jn2 - (j2 + 1)) <= jj + 1 by A34, ABSVALUE:def_1;
 1 <= j2 + 1 by A22, NAT_1:13;
then A36: j2 + 1 in Seg n by A31;
then reconsider yj2 = j2 + 1 as Element of (FTSL1 n) by A1;
 abs ((j2 + 1) - j2) = 1 by ABSVALUE:def_1;
then  x0 in U_FT (yj2,0) by A4, A19;
then  x0 in U_FT yj2 by FINTOPO3:47;
hence  ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y ) by A17, A18, A36, A35; ::_thesis: verum
end;
end;
end;
suppose jn2 - j2 < 0 ; ::_thesis: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y )
then A37: (jn2 - j2) + j2 < 0 + j2 by XREAL_1:6;
then A38: j2 - jn2 > 0 by XREAL_1:50;
 j2 - 1 >= 0 by A22, XREAL_1:48;
then A39: j2 - 1 = j2 -' 1 by XREAL_0:def_2;
 jn2 + 1 <= j2 by A37, NAT_1:13;
then A40: (jn2 + 1) - 1 <= j2 - 1 by XREAL_1:9;
then  (j2 - 1) - jn2 >= 0 by XREAL_1:48;
then A41: abs ((j2 -' 1) - jn2) = (j2 -' 1) - jn2 by A39, ABSVALUE:def_1;
 j2 < j2 + 1 by NAT_1:13;
then  j2 - 1 < (j2 + 1) - 1 by XREAL_1:9;
then A42: j2 -' 1 < n by A21, A39, XXREAL_0:2;
abs (jn2 - j2) = abs (j2 - jn2) by UNIFORM1:11
.= 1 + ((j2 -' 1) - jn2) by A39, A38, ABSVALUE:def_1
.= 1 + (abs (jn2 - (j2 -' 1))) by A41, UNIFORM1:11 ;
then A43: abs (jn2 - (j2 -' 1)) <= jj + 1 by A20, XREAL_1:6;
 j2 -' 1 >= 1 by A24, A40, A39, XXREAL_0:2;
then A44: j2 -' 1 in Seg n by A42;
then reconsider pj21 = j2 -' 1 as Element of (FTSL1 n) by A1;
abs ((j2 -' 1) - j2) = abs (j2 - (j2 -' 1)) by UNIFORM1:11
.= 1 by A39, ABSVALUE:def_1 ;
then  x0 in U_FT (pj21,0) by A4, A19;
then  x0 in U_FT pj21 by FINTOPO3:47;
hence  ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x0 in U_FT y ) by A17, A18, A44, A43; ::_thesis: verum
end;
end;
end;
 jj in NAT by ORDINAL1:def_12;
then  U_FT (p2,(jj + 1)) = (U_FT (p2,jj)) ^f by FINTOPO3:48
.=  {  x where x is Element of (FTSL1 n) : ex y being Element of (FTSL1 n) st
( y in U_FT (p2,jj) & x in U_FT y )  }  ;
hence  j2 in U_FT (p2,(jj + 1)) by A25; ::_thesis: verum
end;
A45: for ii being Nat holds S1[ii] from NAT_1:sch_2(A4, A16);
assume  ( j in Seg n & abs (jn - j) <= k + 1 ) ; ::_thesis: j in U_FT (p,k)
hence  j in U_FT (p,k) by A2, A45; ::_thesis: verum
end;
now__::_thesis:_(_j_in_U_FT_(p,k)_implies_(_j_in_Seg_n_&_abs_(jn_-_j)_<=_k_+_1_)_)
defpred S1[ Nat] means  for j2, jn2 being Nat
for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in U_FT (p2,$1) holds
abs (jn2 - j2) <= $1 + 1;
A46: S1[ 0 ]
proof
let j2, jn2 be Nat; ::_thesis: for p2 being Element of (FTSL1 n) st jn2 = p2 & j2 in U_FT (p2,0) holds
abs (jn2 - j2) <= 0 + 1
let p2 be Element of (FTSL1 n); ::_thesis: ( jn2 = p2 & j2 in U_FT (p2,0) implies abs (jn2 - j2) <= 0 + 1 )
assume that
A47: jn2 = p2 and
A48: j2 in U_FT (p2,0) ; ::_thesis: abs (jn2 - j2) <= 0 + 1
A49: j2 in U_FT p2 by A48, FINTOPO3:47;
 jn2 in NAT by ORDINAL1:def_12;
then A50: Im ((Nbdl1 n),jn2) = {jn2,(max ((jn2 -' 1),1)),(min ((jn2 + 1),n))} by A1, A47, FINTOPO4:def_3;
A51: jn2 <= n by A1, A47, FINSEQ_1:1;
percases ( j2 = jn2 or j2 = max ((jn2 -' 1),1) or j2 = min ((jn2 + 1),n) ) by A1, A47, A49, A50, ENUMSET1:def_1;
suppose j2 = jn2 ; ::_thesis: abs (jn2 - j2) <= 0 + 1
hence  abs (jn2 - j2) <= 0 + 1 by ABSVALUE:2; ::_thesis: verum
end;
supposeA52: j2 = max ((jn2 -' 1),1) ; ::_thesis: abs (jn2 - j2) <= 0 + 1
percases ( jn2 -' 1 >= 1 or jn2 -' 1 < 1 ) ;
supposeA53: jn2 -' 1 >= 1 ; ::_thesis: abs (jn2 - j2) <= 0 + 1
then  j2 = jn2 -' 1 by A52, XXREAL_0:def_10;
then  j2 = jn2 - 1 by A53, NAT_D:39;
hence  abs (jn2 - j2) <= 0 + 1 by ABSVALUE:def_1; ::_thesis: verum
end;
supposeA54: jn2 -' 1 < 1 ; ::_thesis: abs (jn2 - j2) <= 0 + 1
then  jn2 -' 1 < 0 + 1 ;
then  jn2 -' 1 = 0 by NAT_1:13;
then A55: 1 - jn2 >= 0 by NAT_D:36, XREAL_1:48;
 1 <= 1 + jn2 by NAT_1:12;
then A56: 1 - jn2 <= (1 + jn2) - jn2 by XREAL_1:9;
 j2 = 1 by A52, A54, XXREAL_0:def_10;
then  abs (j2 - jn2) = 1 - jn2 by A55, ABSVALUE:def_1;
hence  abs (jn2 - j2) <= 0 + 1 by A56, UNIFORM1:11; ::_thesis: verum
end;
end;
end;
supposeA57: j2 = min ((jn2 + 1),n) ; ::_thesis: abs (jn2 - j2) <= 0 + 1
percases ( jn2 + 1 <= n or jn2 + 1 > n ) ;
suppose jn2 + 1 <= n ; ::_thesis: abs (jn2 - j2) <= 0 + 1
then  j2 = jn2 + 1 by A57, XXREAL_0:def_9;
then  abs (j2 - jn2) = 1 by ABSVALUE:def_1;
hence  abs (jn2 - j2) <= 0 + 1 by UNIFORM1:11; ::_thesis: verum
end;
supposeA58: jn2 + 1 > n ; ::_thesis: abs (jn2 - j2) <= 0 + 1
then  jn2 >= n by NAT_1:13;
then A59: jn2 = n by A51, XXREAL_0:1;
 j2 = n by A57, A58, XXREAL_0:def_9;
hence  abs (jn2 - j2) <= 0 + 1 by A59, ABSVALUE:2; ::_thesis: verum
end;
end;
end;
end;
end;
A60: for i2 being Nat st S1[i2] holds
S1[i2 + 1]
proof
let i2 be Nat; ::_thesis: ( S1[i2] implies S1[i2 + 1] )
assume A61: S1[i2] ; ::_thesis: S1[i2 + 1]
let j3, jn3 be Nat; ::_thesis: for p2 being Element of (FTSL1 n) st jn3 = p2 & j3 in U_FT (p2,(i2 + 1)) holds
abs (jn3 - j3) <= (i2 + 1) + 1
let p2 be Element of (FTSL1 n); ::_thesis: ( jn3 = p2 & j3 in U_FT (p2,(i2 + 1)) implies abs (jn3 - j3) <= (i2 + 1) + 1 )
assume that
A62: jn3 = p2 and
A63: j3 in U_FT (p2,(i2 + 1)) ; ::_thesis: abs (jn3 - j3) <= (i2 + 1) + 1
 i2 in NAT by ORDINAL1:def_12;
then  U_FT (p2,(i2 + 1)) = (U_FT (p2,i2)) ^f by FINTOPO3:48
.=  {  x where x is Element of (FTSL1 n) : ex y being Element of (FTSL1 n) st
( y in U_FT (p2,i2) & x in U_FT y )  }  ;
then consider x being Element of (FTSL1 n) such that
A64: x = j3 and
A65: ex y being Element of (FTSL1 n) st
( y in U_FT (p2,i2) & x in U_FT y ) by A63;
consider y being Element of (FTSL1 n) such that
A66: y in U_FT (p2,i2) and
A67: x in U_FT y by A65;
 y in Seg n by A1;
then reconsider iy = y as Element of NAT ;
 x in U_FT (y,0) by A67, FINTOPO3:47;
then A68: abs (iy - j3) <= 1 by A46, A64;
 abs (jn3 - iy) <= i2 + 1 by A61, A62, A66;
then A69: (abs (jn3 - iy)) + (abs (iy - j3)) <= (i2 + 1) + 1 by A68, XREAL_1:7;
 abs ((jn3 - iy) + (iy - j3)) <= (abs (jn3 - iy)) + (abs (iy - j3)) by COMPLEX1:56;
hence  abs (jn3 - j3) <= (i2 + 1) + 1 by A69, XXREAL_0:2; ::_thesis: verum
end;
A70: for i3 being Nat holds S1[i3] from NAT_1:sch_2(A46, A60);
assume  j in U_FT (p,k) ; ::_thesis: ( j in Seg n & abs (jn - j) <= k + 1 )
hence  ( j in Seg n & abs (jn - j) <= k + 1 ) by A2, A1, A70; ::_thesis: verum
end;
hence  ( j in U_FT (p,k) iff ( j in Seg n & abs (jn - j) <= k + 1 ) ) by A3; ::_thesis: verum
end;

theorem :: FINTOPO5:10
for kc, km being Element of NAT
for n being non zero Element of NAT
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
proof
let kc, km be Element of NAT ; ::_thesis: for n being non zero Element of NAT
for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
let n be non zero Element of NAT ; ::_thesis: for f being Function of (FTSL1 n),(FTSL1 n) st f is_continuous kc & km = [/(kc / 2)\] holds
ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
let f be Function of (FTSL1 n),(FTSL1 n); ::_thesis: ( f is_continuous kc & km = [/(kc / 2)\] implies ex p being Element of (FTSL1 n) st f . p in U_FT (p,km) )
assume that
A1: f is_continuous kc and
A2: km = [/(kc / 2)\] ; ::_thesis: ex p being Element of (FTSL1 n) st f . p in U_FT (p,km)
assume A3: for p being Element of (FTSL1 n) holds not f . p in U_FT (p,km) ; ::_thesis: contradiction
defpred S1[ Nat] means ( $1 > 0 & ( for j being Nat st $1 <= n & j = f . $1 holds
$1 > j ) );
A4: n >= 0 + 1 by NAT_1:13;
A5: RelStr(# (Seg n),(Nbdl1 n) #) = FTSL1 n by FINTOPO4:def_4;
A6: FTSL1 n is filled by FINTOPO4:18;
now__::_thesis:_for_j_being_Nat_holds_
(_not_j_=_f_._n_or_not_n_<=_j_)
A7: n in the carrier of (FTSL1 n) by A4, A5;
then reconsider p2 = n as Element of (FTSL1 n) ;
given j being Nat such that A8: j = f . n and
A9: n <= j ; ::_thesis: contradiction
 f . n in the carrier of (FTSL1 n) by A7, FUNCT_2:5;
then  j <= n by A5, A8, FINSEQ_1:1;
then A10: n = j by A9, XXREAL_0:1;
 p2 in U_FT p2 by A6, FIN_TOPO:def_4;
then A11: p2 in U_FT (p2,0) by FINTOPO3:47;
 U_FT (p2,0) c= U_FT (p2,km) by Th8, FINTOPO4:18;
hence  contradiction by A3, A8, A10, A11; ::_thesis: verum
end;
then A12: for j being Nat st n <= n & j = f . n holds
n > j ;
then A13: ex k being Nat st S1[k] ;
 ex k being Nat st
( S1[k] & ( for m being Nat st S1[m] holds
k <= m ) ) from NAT_1:sch_5(A13);
then consider k being Nat such that
A14: S1[k] and
A15: for m being Nat st S1[m] holds
k <= m ;
A16: 0 + 1 <= k by A14, NAT_1:13;
then A17: k - 1 >= 0 by XREAL_1:48;
then A18: k - 1 = k -' 1 by XREAL_0:def_2;
 k < k + 1 by NAT_1:13;
then A19: k - 1 < (k + 1) - 1 by XREAL_1:9;
A20: k <= n by A12, A15;
then reconsider pk = k as Element of (FTSL1 n) by A5, A16, FINSEQ_1:1;
percases ( k -' 1 <= 0 or ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ) by A15, A18, A19;
supposeA21: k -' 1 <= 0 ; ::_thesis: contradiction
 1 in the carrier of (FTSL1 n) by A4, A5;
then A22: f . 1 in Seg n by A5, FUNCT_2:5;
then reconsider j0 = f . 1 as Element of NAT ;
 k - 1 = 0 by A17, A21, XREAL_0:def_2;
then  1 > j0 by A4, A14;
hence  contradiction by A22, FINSEQ_1:1; ::_thesis: verum
end;
supposeA23: ( k -' 1 > 0 & ex j being Nat st
( k -' 1 <= n & j = f . (k -' 1) & k -' 1 <= j ) ) ; ::_thesis: contradiction
 k in NAT by ORDINAL1:def_12;
then A24: k in the carrier of (FTSL1 n) by A5, A20, A16;
then  f . k in Seg n by A5, FUNCT_2:5;
then reconsider jn = f . k as Element of NAT ;
A25: not jn in U_FT (pk,km) by A3;
A26: jn < k by A14, A20;
then A27: k - jn > 0 by XREAL_1:50;
 jn in Seg n by A5, A24, FUNCT_2:5;
then  not abs (k - jn) <= km + 1 by A25, Th9;
then A28: k - jn > km + 1 by A27, ABSVALUE:def_1;
 k - jn = k -' jn by A27, XREAL_0:def_2;
then A29: k - jn >= (km + 1) + 1 by A28, NAT_1:13;
reconsider pfk = jn as Element of (FTSL1 n) by A24, FUNCT_2:5;
A30: kc < kc + 2 by XREAL_1:29;
A31: k -' 1 >= 0 + 1 by A23, NAT_1:13;
then A32: k -' 1 = max ((k -' 1),1) by XXREAL_0:def_10;
 Im ((Nbdl1 n),k) = {k,(max ((k -' 1),1)),(min ((k + 1),n))} by A5, A24, FINTOPO4:def_3;
then  k -' 1 in U_FT pk by A5, A32, ENUMSET1:def_1;
then A33: k -' 1 in U_FT (pk,0) by FINTOPO3:47;
consider j being Nat such that
A34: k -' 1 <= n and
A35: j = f . (k -' 1) and
A36: k -' 1 <= j by A23;
reconsider pkm = k -' 1 as Element of (FTSL1 n) by A5, A34, A31, FINSEQ_1:1;
A37: not j in U_FT (pkm,km) by A3, A35;
A38: k -' 1 in the carrier of (FTSL1 n) by A5, A34, A31;
then  k -' 1 in dom f by FUNCT_2:def_1;
then A39: f . (k -' 1) in f .: (U_FT (pk,0)) by A33, FUNCT_1:def_6;
now__::_thesis:_not_k_-'_1_=_j
assume A40: k -' 1 = j ; ::_thesis: contradiction
then reconsider pj = j as Element of (FTSL1 n) by A38;
 pj in U_FT pj by A6, FIN_TOPO:def_4;
then A41: pj in U_FT (pj,0) by FINTOPO3:47;
 U_FT (pj,0) c= U_FT (pj,km) by Th8, FINTOPO4:18;
hence  contradiction by A3, A35, A40, A41; ::_thesis: verum
end;
then  k -' 1 < j by A36, XXREAL_0:1;
then A42: (k -' 1) + 1 <= j by NAT_1:13;
then  j - k >= 0 by A18, XREAL_1:48;
then A43: j - k = j -' k by XREAL_0:def_2;
 j in the carrier of (FTSL1 n) by A35, A38, FUNCT_2:5;
then  not abs ((k -' 1) - j) <= km + 1 by A5, A37, Th9;
then  abs (j - (k -' 1)) > km + 1 by UNIFORM1:11;
then  (j -' k) + 1 > km + 1 by A18, A43, ABSVALUE:def_1;
then  (j - k) + 1 >= (km + 1) + 1 by A43, NAT_1:13;
then  (k - jn) + ((j - k) + 1) >= ((km + 1) + 1) + ((km + 1) + 1) by A29, XREAL_1:7;
then  (j - jn) + 1 >= (((km + 1) + 1) + (km + 1)) + 1 ;
then  j - jn >= ((km + 1) + 1) + (km + 1) by XREAL_1:6;
then  (j - jn) - 1 >= ((((km + 1) + 1) + km) + 1) - 1 by XREAL_1:9;
then A44: ((j - jn) - 1) / 2 >= ((2 * km) + 2) / 2 by XREAL_1:72;
 [/(kc / 2)\] >= kc / 2 by INT_1:def_7;
then  [/(kc / 2)\] + (2 / 2) >= (kc / 2) + (2 / 2) by XREAL_1:7;
then  ((j - jn) - 1) / 2 >= (kc / 2) + (2 / 2) by A2, A44, XXREAL_0:2;
then  (((j - jn) - 1) / 2) * 2 >= ((kc / 2) + (2 / 2)) * 2 by XREAL_1:64;
then  (j - jn) - 1 > kc by A30, XXREAL_0:2;
then A45: ((j - jn) - 1) + 1 > kc + 1 by XREAL_1:6;
 jn < j by A18, A42, A26, XXREAL_0:2;
then  j - jn >= 0 by XREAL_1:48;
then A46: abs (j - jn) = j - jn by ABSVALUE:def_1;
 ( f .: (U_FT (pk,0)) c= U_FT (pfk,kc) & abs (jn - j) = abs (j - jn) ) by A1, FINTOPO4:def_2, UNIFORM1:11;
hence  contradiction by A35, A39, A46, A45, Th9; ::_thesis: verum
end;
end;
end;

definition
let A, B be set ;
let R be Relation of A,B;
let x be set ;
:: original: Im
redefine func Im (R,x) ->  Subset of B;
coherence
 Im (R,x) is Subset of B
proof
 Im (R,x) = R .: {x} ;
hence  Im (R,x) is Subset of B ; ::_thesis: verum
end;
end;

definition
let n, m be Element of NAT ;
func Nbdl2 (n,m) ->  Relation of [:(Seg n),(Seg m):] means :Def2: :: FINTOPO5:def 2
 for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (it,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):];
existence
 ex b1 being Relation of [:(Seg n),(Seg m):] st
for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
proof
defpred S1[ set , set ] means  for i, j being Element of NAT st $1 = [i,j] holds
$2 = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):];
A1: for x being set st x in [:(Seg n),(Seg m):] holds
ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [:(Seg n),(Seg m):] implies ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] ) )
assume  x in [:(Seg n),(Seg m):] ; ::_thesis: ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] )
then consider u, y being set  such that
A2: ( u in Seg n & y in Seg m ) and
A3: x = [u,y] by ZFMISC_1:def_2;
reconsider i = u, j = y as Element of NAT by A2;
set y3 = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):];
A4: [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] c= [:(Seg n),(Seg m):]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] or z in [:(Seg n),(Seg m):] )
assume  z in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ; ::_thesis: z in [:(Seg n),(Seg m):]
then  ex x4, y4 being set st
( x4 in Im ((Nbdl1 n),i) & y4 in Im ((Nbdl1 m),j) & z = [x4,y4] ) by ZFMISC_1:def_2;
hence  z in [:(Seg n),(Seg m):] by ZFMISC_1:def_2; ::_thesis: verum
end;
 for i4, j4 being Element of NAT st x = [i4,j4] holds
[:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):]
proof
let i4, j4 be Element of NAT ; ::_thesis: ( x = [i4,j4] implies [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):] )
assume A5: x = [i4,j4] ; ::_thesis: [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):]
then  i4 = u by A3, XTUPLE_0:1;
hence  [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] = [:(Im ((Nbdl1 n),i4)),(Im ((Nbdl1 m),j4)):] by A3, A5, XTUPLE_0:1; ::_thesis: verum
end;
hence  ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] ) by A4; ::_thesis: verum
end;
consider f being Function of [:(Seg n),(Seg m):],(bool [:(Seg n),(Seg m):]) such that
A6: for x being set st x in [:(Seg n),(Seg m):] holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
consider R being Relation of [:(Seg n),(Seg m):] such that
A7: for i being set st i in [:(Seg n),(Seg m):] holds
Im (R,i) = f . i by FUNCT_2:93;
take  R ; ::_thesis: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
let x be set ; ::_thesis: ( x in [:(Seg n),(Seg m):] implies for i, j being Element of NAT st x = [i,j] holds
Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] )
assume A8: x in [:(Seg n),(Seg m):] ; ::_thesis: for i, j being Element of NAT st x = [i,j] holds
Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
let i, j be Element of NAT ; ::_thesis: ( x = [i,j] implies Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] )
assume A9: x = [i,j] ; ::_thesis: Im (R,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):]
thus  Im (R,x) = f . x by A7, A8
.= [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] by A6, A8, A9 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b2,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) holds
b1 = b2
proof
let f1, f2 be Relation of [:(Seg n),(Seg m):]; ::_thesis: ( ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f2,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ) implies f1 = f2 )
assume that
A10: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] and
A11: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f2,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] ; ::_thesis: f1 = f2
 for x being set st x in [:(Seg n),(Seg m):] holds
Im (f1,x) = Im (f2,x)
proof
let x be set ; ::_thesis: ( x in [:(Seg n),(Seg m):] implies Im (f1,x) = Im (f2,x) )
assume A12: x in [:(Seg n),(Seg m):] ; ::_thesis: Im (f1,x) = Im (f2,x)
then consider u, y being set  such that
A13: ( u in Seg n & y in Seg m ) and
A14: x = [u,y] by ZFMISC_1:def_2;
reconsider i = u, j = y as Element of NAT by A13;
 Im (f1,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] by A10, A12, A14;
hence  Im (f1,x) = Im (f2,x) by A11, A12, A14; ::_thesis: verum
end;
hence  f1 = f2 by RELSET_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Nbdl2 FINTOPO5:def_2_:_
 for n, m being Element of NAT
for b3 being Relation of [:(Seg n),(Seg m):] holds
( b3 = Nbdl2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b3,x) = [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] );

definition
let n, m be Element of NAT ;
func FTSL2 (n,m) ->  strict RelStr  equals :: FINTOPO5:def 3
 RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);
coherence
 RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #) is strict RelStr ;
end;

:: deftheorem  defines FTSL2 FINTOPO5:def_3_:_
 for n, m being Element of NAT holds FTSL2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbdl2 (n,m)) #);

registration
let n, m be non zero Element of NAT ;
cluster FTSL2 (n,m) ->  non empty strict ;
coherence
 not FTSL2 (n,m) is empty ;
end;

theorem :: FINTOPO5:11
for n, m being non zero Element of NAT holds FTSL2 (n,m) is filled
proof
let n, m be non zero Element of NAT ; ::_thesis: FTSL2 (n,m) is filled
 for x being Element of (FTSL2 (n,m)) holds x in U_FT x
proof
let x be Element of (FTSL2 (n,m)); ::_thesis: x in U_FT x
consider u, y being set  such that
A1: u in Seg n and
A2: y in Seg m and
A3: x = [u,y] by ZFMISC_1:def_2;
reconsider i = u, j = y as Element of NAT by A1, A2;
A4: FTSL1 m = RelStr(# (Seg m),(Nbdl1 m) #) by FINTOPO4:def_4;
then reconsider pj = j as Element of (FTSL1 m) by A2;
A5: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def_4;
then reconsider pi = i as Element of (FTSL1 n) by A1;
 FTSL1 m is filled by FINTOPO4:18;
then A6: j in U_FT pj by FIN_TOPO:def_4;
 FTSL1 n is filled by FINTOPO4:18;
then  i in U_FT pi by FIN_TOPO:def_4;
then  x in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] by A3, A4, A5, A6, ZFMISC_1:def_2;
hence  x in U_FT x by A3, Def2; ::_thesis: verum
end;
hence  FTSL2 (n,m) is filled by FIN_TOPO:def_4; ::_thesis: verum
end;

theorem :: FINTOPO5:12
for n, m being non zero Element of NAT holds FTSL2 (n,m) is symmetric
proof
let n, m be non zero Element of NAT ; ::_thesis: FTSL2 (n,m) is symmetric
 for x, y being Element of (FTSL2 (n,m)) st y in U_FT x holds
x in U_FT y
proof
A1: FTSL1 m is symmetric by FINTOPO4:19;
let x, y be Element of (FTSL2 (n,m)); ::_thesis: ( y in U_FT x implies x in U_FT y )
consider xu, xv being set  such that
A2: xu in Seg n and
A3: xv in Seg m and
A4: x = [xu,xv] by ZFMISC_1:def_2;
reconsider i = xu, j = xv as Element of NAT by A2, A3;
consider yu, yv being set  such that
A5: yu in Seg n and
A6: yv in Seg m and
A7: y = [yu,yv] by ZFMISC_1:def_2;
reconsider i2 = yu, j2 = yv as Element of NAT by A5, A6;
A8: FTSL1 m = RelStr(# (Seg m),(Nbdl1 m) #) by FINTOPO4:def_4;
then reconsider pj = j as Element of (FTSL1 m) by A3;
reconsider pj2 = j2 as Element of (FTSL1 m) by A8, A6;
assume  y in U_FT x ; ::_thesis: x in U_FT y
then  y in [:(Im ((Nbdl1 n),i)),(Im ((Nbdl1 m),j)):] by A4, Def2;
then A9: ex y1, y2 being set st
( y1 in Class ((Nbdl1 n),i) & y2 in Class ((Nbdl1 m),j) & y = [y1,y2] ) by ZFMISC_1:def_2;
then  j2 in U_FT pj by A8, A7, XTUPLE_0:1;
then A10: j in U_FT pj2 by A1, FIN_TOPO:def_13;
A11: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def_4;
then reconsider pi = i as Element of (FTSL1 n) by A2;
A12: FTSL1 n is symmetric by FINTOPO4:19;
reconsider pi2 = i2 as Element of (FTSL1 n) by A11, A5;
 pi2 in U_FT pi by A11, A7, A9, XTUPLE_0:1;
then  pi in U_FT pi2 by A12, FIN_TOPO:def_13;
then  x in [:(Im ((Nbdl1 n),i2)),(Im ((Nbdl1 m),j2)):] by A4, A8, A11, A10, ZFMISC_1:def_2;
hence  x in U_FT y by A7, Def2; ::_thesis: verum
end;
hence  FTSL2 (n,m) is symmetric by FIN_TOPO:def_13; ::_thesis: verum
end;

theorem :: FINTOPO5:13
for n being non zero Element of NAT ex h being Function of (FTSL2 (n,1)),(FTSL1 n) st h is being_homeomorphism
proof
defpred S1[ set , set ] means [$2,1] = $1;
let n be non zero Element of NAT ; ::_thesis: ex h being Function of (FTSL2 (n,1)),(FTSL1 n) st h is being_homeomorphism
set FT1 = FTSL2 (n,1);
set FT2 = FTSL1 n;
A1: 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] ) )
A2: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def_4;
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 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:1;
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; ::_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(A1);
then consider f being Function of (FTSL2 (n,1)),(FTSL1 n) such that
A6: for x being set st x in the carrier of (FTSL2 (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 ; :: 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 (FTSL2 (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;
A12: 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 and
A14: v in Seg 1 and
A15: x = [u,v] by ZFMISC_1:def_2;
A16: Im ( the InternalRel of (FTSL1 n),(f . x)) c= f .: (U_FT x)
proof
reconsider nv = v as Element of NAT by A14;
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 A17: y in Im ( the InternalRel of (FTSL1 n),(f . x)) ; ::_thesis: y in f .: (U_FT x)
 ( 1 <= nv & nv <= 1 ) by A14, FINSEQ_1:1;
then A18: nv = 1 by XXREAL_0:1;
 Im ((Nbdl1 n),(f . x)) c= rng f by A7, A8, XBOOLE_1:1;
then consider x3 being set  such that
A19: x3 in dom f and
A20: y = f . x3 by A7, A17, FUNCT_1:def_3;
set u2 = f . x3;
set v2 = 1;
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 A18, 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 A21: 1 in Im ((Nbdl1 1),v) by ZFMISC_1:31;
A22: Im ((Nbdl2 (n,1)),x) = [:(Im ((Nbdl1 n),u)),(Im ((Nbdl1 1),v)):] by A13, A14, A15, Def2;
 x = [(f . x),1] by A6;
then  f . x3 in Im ((Nbdl1 n),u) by A7, A15, A17, A20, XTUPLE_0:1;
then A23: [(f . x3),1] in [:(Im ((Nbdl1 n),u)),(Im ((Nbdl1 1),v)):] by A21, ZFMISC_1:def_2;
 x3 = [(f . x3),1] by A6, A19;
hence  y in f .: (U_FT x) by A19, A20, A23, A22, FUNCT_1:def_6; ::_thesis: verum
end;
 f .: (U_FT x) c= Im ( the InternalRel of (FTSL1 n),(f . x))
proof
 x = [(f . x),1] by A6;
then A24: u = f . x by A15, XTUPLE_0:1;
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
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 ((Nbdl1 n),u)),(Im ((Nbdl1 1),v)):] by A13, A14, A15, Def2;
 x2 = [(f . x2),1] by A6, A25;
hence  y in Im ( the InternalRel of (FTSL1 n),(f . x)) by A7, A26, A27, A24, ZFMISC_1:87; ::_thesis: verum
end;
hence  f .: (U_FT x) = Im ( the InternalRel of (FTSL1 n),(f . x)) by A16, XBOOLE_0:def_10; ::_thesis: verum
end;
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_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 A6, A28;
hence  x1 = x2 by A6, A29; ::_thesis: verum
end;
then A30: f is one-to-one by FUNCT_1:def_4;
 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 A30, A12, Def1;
hence  ex h being Function of (FTSL2 (n,1)),(FTSL1 n) st h is being_homeomorphism ; ::_thesis: verum
end;

definition
let n, m be Element of NAT ;
func Nbds2 (n,m) ->  Relation of [:(Seg n),(Seg m):] means :Def4: :: FINTOPO5:def 4
 for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (it,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:];
existence
 ex b1 being Relation of [:(Seg n),(Seg m):] st
for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
proof
defpred S1[ set , set ] means  for i, j being Element of NAT st $1 = [i,j] holds
$2 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:];
A1: for x being set st x in [:(Seg n),(Seg m):] holds
ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in [:(Seg n),(Seg m):] implies ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] ) )
assume  x in [:(Seg n),(Seg m):] ; ::_thesis: ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] )
then consider u, y being set  such that
A2: u in Seg n and
A3: y in Seg m and
A4: x = [u,y] by ZFMISC_1:def_2;
reconsider i = u, j = y as Element of NAT by A2, A3;
set y3 = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:];
A5: [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] c= [:(Seg n),(Seg m):]
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] or z in [:(Seg n),(Seg m):] )
assume A6: z in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] ; ::_thesis: z in [:(Seg n),(Seg m):]
percases ( z in [:{i},(Im ((Nbdl1 m),j)):] or z in [:(Im ((Nbdl1 n),u)),{j}:] ) by A6, XBOOLE_0:def_3;
suppose z in [:{i},(Im ((Nbdl1 m),j)):] ; ::_thesis: z in [:(Seg n),(Seg m):]
then consider x4, y4 being set  such that
A7: x4 in {i} and
A8: ( y4 in Im ((Nbdl1 m),j) & z = [x4,y4] ) by ZFMISC_1:def_2;
 x4 = i by A7, TARSKI:def_1;
hence  z in [:(Seg n),(Seg m):] by A2, A8, ZFMISC_1:def_2; ::_thesis: verum
end;
suppose z in [:(Im ((Nbdl1 n),u)),{j}:] ; ::_thesis: z in [:(Seg n),(Seg m):]
then consider x4, y4 being set  such that
A9: x4 in Im ((Nbdl1 n),u) and
A10: y4 in {j} and
A11: z = [x4,y4] by ZFMISC_1:def_2;
 y4 in Seg m by A3, A10, TARSKI:def_1;
hence  z in [:(Seg n),(Seg m):] by A9, A11, ZFMISC_1:def_2; ::_thesis: verum
end;
end;
end;
 for i4, j4 being Element of NAT st x = [i4,j4] holds
[:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]
proof
let i4, j4 be Element of NAT ; ::_thesis: ( x = [i4,j4] implies [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:] )
assume  x = [i4,j4] ; ::_thesis: [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:]
then  ( i4 = u & j4 = y ) by A4, XTUPLE_0:1;
hence  [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] = [:{i4},(Im ((Nbdl1 m),j4)):] \/ [:(Im ((Nbdl1 n),i4)),{j4}:] ; ::_thesis: verum
end;
hence  ex y being set st
( y in bool [:(Seg n),(Seg m):] & S1[x,y] ) by A5; ::_thesis: verum
end;
consider f being Function of [:(Seg n),(Seg m):],(bool [:(Seg n),(Seg m):]) such that
A12: for x being set st x in [:(Seg n),(Seg m):] holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
consider R being Relation of [:(Seg n),(Seg m):] such that
A13: for i being set st i in [:(Seg n),(Seg m):] holds
Im (R,i) = f . i by FUNCT_2:93;
take  R ; ::_thesis: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
let x be set ; ::_thesis: ( x in [:(Seg n),(Seg m):] implies for i, j being Element of NAT st x = [i,j] holds
Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )
assume A14: x in [:(Seg n),(Seg m):] ; ::_thesis: for i, j being Element of NAT st x = [i,j] holds
Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
let i, j be Element of NAT ; ::_thesis: ( x = [i,j] implies Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] )
assume A15: x = [i,j] ; ::_thesis: Im (R,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:]
thus  Im (R,x) = f . x by A13, A14
.= [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] by A12, A14, A15 ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation of [:(Seg n),(Seg m):] st ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b2,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) holds
b1 = b2
proof
let f1, f2 be Relation of [:(Seg n),(Seg m):]; ::_thesis: ( ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) & ( for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f2,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ) implies f1 = f2 )
assume that
A16: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] and
A17: for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (f2,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] ; ::_thesis: f1 = f2
 for x being set st x in [:(Seg n),(Seg m):] holds
Im (f1,x) = Im (f2,x)
proof
let x be set ; ::_thesis: ( x in [:(Seg n),(Seg m):] implies Im (f1,x) = Im (f2,x) )
assume A18: x in [:(Seg n),(Seg m):] ; ::_thesis: Im (f1,x) = Im (f2,x)
then consider u, y being set  such that
A19: ( u in Seg n & y in Seg m ) and
A20: x = [u,y] by ZFMISC_1:def_2;
reconsider i = u, j = y as Element of NAT by A19;
 Im (f1,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] by A16, A18, A20;
hence  Im (f1,x) = Im (f2,x) by A17, A18, A20; ::_thesis: verum
end;
hence  f1 = f2 by RELSET_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Nbds2 FINTOPO5:def_4_:_
 for n, m being Element of NAT
for b3 being Relation of [:(Seg n),(Seg m):] holds
( b3 = Nbds2 (n,m) iff for x being set st x in [:(Seg n),(Seg m):] holds
for i, j being Element of NAT st x = [i,j] holds
Im (b3,x) = [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] );

definition
let n, m be Element of NAT ;
func FTSS2 (n,m) ->  strict RelStr  equals :: FINTOPO5:def 5
 RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);
coherence
 RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #) is strict RelStr ;
end;

:: deftheorem  defines FTSS2 FINTOPO5:def_5_:_
 for n, m being Element of NAT holds FTSS2 (n,m) = RelStr(# [:(Seg n),(Seg m):],(Nbds2 (n,m)) #);

registration
let n, m be non zero Element of NAT ;
cluster FTSS2 (n,m) ->  non empty strict ;
coherence
 not FTSS2 (n,m) is empty ;
end;

theorem :: FINTOPO5:14
for n, m being non zero Element of NAT holds FTSS2 (n,m) is filled
proof
let n, m be non zero Element of NAT ; ::_thesis: FTSS2 (n,m) is filled
 for x being Element of (FTSS2 (n,m)) holds x in U_FT x
proof
let x be Element of (FTSS2 (n,m)); ::_thesis: x in U_FT x
consider u, y being set  such that
A1: u in Seg n and
A2: y in Seg m and
A3: x = [u,y] by ZFMISC_1:def_2;
reconsider i = u, j = y as Element of NAT by A1, A2;
A4: FTSL1 m = RelStr(# (Seg m),(Nbdl1 m) #) by FINTOPO4:def_4;
then reconsider pj = j as Element of (FTSL1 m) by A2;
A5: i in {i} by ZFMISC_1:31;
 FTSL1 m is filled by FINTOPO4:18;
then  j in U_FT pj by FIN_TOPO:def_4;
then  x in [:{i},(Im ((Nbdl1 m),j)):] by A3, A4, A5, ZFMISC_1:def_2;
then  x in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),u)),{j}:] by XBOOLE_0:def_3;
hence  x in U_FT x by A3, Def4; ::_thesis: verum
end;
hence  FTSS2 (n,m) is filled by FIN_TOPO:def_4; ::_thesis: verum
end;

theorem :: FINTOPO5:15
for n, m being non zero Element of NAT holds FTSS2 (n,m) is symmetric
proof
let n, m be non zero Element of NAT ; ::_thesis: FTSS2 (n,m) is symmetric
 for x, y being Element of (FTSS2 (n,m)) st y in U_FT x holds
x in U_FT y
proof
let x, y be Element of (FTSS2 (n,m)); ::_thesis: ( y in U_FT x implies x in U_FT y )
consider xu, xv being set  such that
A1: xu in Seg n and
A2: xv in Seg m and
A3: x = [xu,xv] by ZFMISC_1:def_2;
reconsider i = xu, j = xv as Element of NAT by A1, A2;
consider yu, yv being set  such that
A4: yu in Seg n and
A5: yv in Seg m and
A6: y = [yu,yv] by ZFMISC_1:def_2;
reconsider i2 = yu, j2 = yv as Element of NAT by A4, A5;
A7: FTSL1 m = RelStr(# (Seg m),(Nbdl1 m) #) by FINTOPO4:def_4;
then reconsider pj = j as Element of (FTSL1 m) by A2;
A8: FTSL1 n = RelStr(# (Seg n),(Nbdl1 n) #) by FINTOPO4:def_4;
then reconsider pi = i as Element of (FTSL1 n) by A1;
reconsider pj2 = j2 as Element of (FTSL1 m) by A7, A5;
reconsider pi2 = i2 as Element of (FTSL1 n) by A8, A4;
assume  y in U_FT x ; ::_thesis: x in U_FT y
then A9: y in [:{i},(Im ((Nbdl1 m),j)):] \/ [:(Im ((Nbdl1 n),i)),{j}:] by A3, Def4;
now__::_thesis:_(_(_y_in_[:{i},(Im_((Nbdl1_m),j)):]_&_x_in_[:{i2},(Im_((Nbdl1_m),j2)):]_)_or_(_y_in_[:(Im_((Nbdl1_n),i)),{j}:]_&_x_in_[:(Im_((Nbdl1_n),i2)),{j2}:]_)_)
percases ( y in [:{i},(Im ((Nbdl1 m),j)):] or y in [:(Im ((Nbdl1 n),i)),{j}:] ) by A9, XBOOLE_0:def_3;
case y in [:{i},(Im ((Nbdl1 m),j)):] ; ::_thesis: x in [:{i2},(Im ((Nbdl1 m),j2)):]
then consider y1, y2 being set  such that
A10: y1 in {i} and
A11: y2 in Class ((Nbdl1 m),j) and
A12: y = [y1,y2] by ZFMISC_1:def_2;
 y1 = i by A10, TARSKI:def_1;
then A13: i in {i2} by A6, A10, A12, XTUPLE_0:1;
A14: FTSL1 m is symmetric by FINTOPO4:19;
 pj2 in U_FT pj by A7, A6, A11, A12, XTUPLE_0:1;
then  pj in U_FT pj2 by A14, FIN_TOPO:def_13;
hence  x in [:{i2},(Im ((Nbdl1 m),j2)):] by A3, A7, A13, ZFMISC_1:def_2; ::_thesis: verum
end;
case y in [:(Im ((Nbdl1 n),i)),{j}:] ; ::_thesis: x in [:(Im ((Nbdl1 n),i2)),{j2}:]
then consider y1, y2 being set  such that
A15: y1 in Class ((Nbdl1 n),i) and
A16: y2 in {j} and
A17: y = [y1,y2] by ZFMISC_1:def_2;
 y2 = j by A16, TARSKI:def_1;
then A18: j in {j2} by A6, A16, A17, XTUPLE_0:1;
A19: FTSL1 n is symmetric by FINTOPO4:19;
 pi2 in U_FT pi by A8, A6, A15, A17, XTUPLE_0:1;
then  pi in U_FT pi2 by A19, FIN_TOPO:def_13;
hence  x in [:(Im ((Nbdl1 n),i2)),{j2}:] by A3, A8, A18, ZFMISC_1:def_2; ::_thesis: verum
end;
end;
end;
then  x in [:{i2},(Im ((Nbdl1 m),j2)):] \/ [:(Im ((Nbdl1 n),i2)),{j2}:] by XBOOLE_0:def_3;
hence  x in U_FT y by A6, Def4; ::_thesis: verum
end;
hence  FTSS2 (n,m) is symmetric by FIN_TOPO:def_13; ::_thesis: verum
end;

theorem :: FINTOPO5:16
for n being non zero Element of NAT ex h being Function of (FTSS2 (n,1)),(FTSL1 n) st h is being_homeomorphism
proof
defpred S1[ set , set ] means [$2,1] = $1;
let n be non zero Element of 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 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 ; ::_thesis: ( 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)) ; ::_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 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:1;
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; ::_thesis: 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 ; :: 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;
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)); ::_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 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 ; :: 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
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 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, 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)
percases ( [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;
supposeA24: [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 by FIN_TOPO:def_4;
 u2 in {u} by A24, ZFMISC_1:87;
hence  u2 in Class ((Nbdl1 n),u) by A7, A25, TARSKI:def_1; ::_thesis: verum
end;
suppose [u2,v2] in [:(Im ((Nbdl1 n),u)),{v}:] ; ::_thesis: u2 in Class ((Nbdl1 n),u)
hence  u2 in Class ((Nbdl1 n),u) by ZFMISC_1:87; ::_thesis: verum
end;
end;
end;
 x = [(f . x),1] by A6;
hence  y in Im ( the InternalRel of (FTSL1 n),(f . x)) by A7, A15, A19, A21, A23, XTUPLE_0:1; ::_thesis: 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 ; :: 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, 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_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;
hence  f .: (U_FT x) = Im ( the InternalRel of (FTSL1 n),(f . x)) by A16, XBOOLE_0:def_10; ::_thesis: verum
end;
 for x1, x2 being set st x1 in dom f & x2 in dom f & f . x1 = f . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_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;
then A36: f is one-to-one by FUNCT_1:def_4;
 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 ; ::_thesis: verum
end;