:: Continuous Mappings between Finite and One-Dimensional Finite Topological
:: Spaces
::  by Hiroshi Imura , Masami Tanaka and Yatsuka Nakamura
::
:: Received July 13, 2004
:: Copyright (c) 2004-2019 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XBOOLE_0, ORDERS_2, SUBSET_1, CONNSP_1, FIN_TOPO,
      XXREAL_0, FINTOPO3, TARSKI, ARYTM_3, ARYTM_1, CARD_1, RELAT_2, FUNCT_1,
      STRUCT_0, RELAT_1, NAT_1, FINSEQ_1, ZFMISC_1, FINTOPO4;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, ORDINAL1, NUMBERS,
      XCMPLX_0, XXREAL_0, NAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1,
      STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1;
 constructors ENUMSET1, NAT_1, EQREL_1, NAT_D, FIN_TOPO, FINTOPO3, FINSEQ_1,
      RELSET_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, XXREAL_0, XREAL_0, NAT_1,
      STRUCT_0, FIN_TOPO, ORDINAL1, FINSEQ_1, RELAT_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, FIN_TOPO;
 equalities FIN_TOPO, FINSEQ_1;
 expansions TARSKI, FIN_TOPO;
 theorems TARSKI, FINSEQ_1, NAT_1, FUNCT_1, FUNCT_2, XBOOLE_0, XBOOLE_1,
      FIN_TOPO, FINTOPO3, RELAT_1, ENUMSET1, XREAL_1, XXREAL_0, ORDINAL1,
      RELSET_1, XREAL_0, NAT_D;
 schemes NAT_1, FUNCT_2, RELSET_1;

begin

definition
  let FT be non empty RelStr, A,B be Subset of FT;
  pred A,B are_separated means

  A^b misses B & A misses B^b;
  symmetry;
end;

theorem Th1:
  for FT being filled non empty RelStr, A being Subset of FT, n,m
  being Element of NAT st n<=m holds Finf(A,n) c= Finf(A,m)
proof
  let FT be filled non empty RelStr, A be Subset of FT, n,m be Element of
  NAT;
  defpred P[Nat] means Finf(A,n) c= Finf(A,n+$1);
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
A2: Finf(A,n+k) c= Finf(A,n+k+1) by FINTOPO3:37;
    assume P[k];
    hence thesis by A2,XBOOLE_1:1;
  end;
  assume n<=m;
  then m-n>=0 by XREAL_1:48;
  then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
    .=m;
A4: P[0];
  for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
  hence thesis by A3;
end;

theorem
  for FT being filled non empty RelStr, A being Subset of FT, n,m
  being Element of NAT st n<=m holds Fcl(A,n) c= Fcl(A,m)
proof
  let FT be filled non empty RelStr,A be Subset of FT, n,m be Element of NAT;
  defpred P[Nat] means Fcl(A,n) c= Fcl(A,n+$1);
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
A2: Fcl(A,n+k) c= Fcl(A,n+k+1) by FINTOPO3:25;
    assume P[k];
    hence thesis by A2,XBOOLE_1:1;
  end;
  assume n<=m;
  then m-n>=0 by XREAL_1:48;
  then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
    .=m;
A4: P[0];
  for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
  hence thesis by A3;
end;

theorem
  for FT being filled non empty RelStr, A being Subset of FT, n,m
  being Element of NAT st n<=m holds Fdfl(A,m) c= Fdfl(A,n)
proof
  let FT be filled non empty RelStr,A be Subset of FT, n,m be Element of NAT;
  defpred P[Nat] means Fdfl(A,n+$1) c= Fdfl(A,n);
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
A2: Fdfl(A,n+k+1) c= Fdfl(A,n+k) by FINTOPO3:44;
    assume P[k];
    hence thesis by A2,XBOOLE_1:1;
  end;
  assume n<=m;
  then m-n>=0 by XREAL_1:48;
  then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
    .=m;
A4: P[0];
  for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
  hence thesis by A3;
end;

theorem
  for FT being filled non empty RelStr, A being Subset of FT, n,m
  being Element of NAT st n<=m holds Fint(A,m) c= Fint(A,n)
proof
  let FT be filled non empty RelStr,A be Subset of FT, n,m be Element of NAT;
  defpred P[Nat] means Fint(A,n+$1) c= Fint(A,n);
A1: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
A2: Fint(A,n+k+1) c= Fint(A,n+k) by FINTOPO3:26;
    assume P[k];
    hence thesis by A2,XBOOLE_1:1;
  end;
  assume n<=m;
  then m-n>=0 by XREAL_1:48;
  then
A3: n+(m-'n)=n+(m-n) by XREAL_0:def 2
    .=m;
A4: P[0];
  for m2 being Nat holds P[m2] from NAT_1:sch 2(A4,A1);
  hence thesis by A3;
end;

theorem
  for FT being non empty RelStr,A,B being Subset of FT st A,B
  are_separated holds B,A are_separated;

theorem Th6:
  for FT being filled non empty RelStr, A,B being Subset of FT st
  A,B are_separated holds A misses B
by FIN_TOPO:13,XBOOLE_1:63;

theorem
  for FT being non empty RelStr, A,B being Subset of FT st FT is
  symmetric holds A,B are_separated iff A^f misses B & A misses (B^f)
by FIN_TOPO:12;

theorem Th8:
  for FT being filled non empty RelStr, A,B being Subset of FT st
  FT is symmetric & A^b misses B holds A misses (B^b)
proof
  let FT be filled non empty RelStr, A,B be Subset of FT;
  assume that
A1: FT is symmetric and
A2: A^b misses B;
  now
    assume A meets (B^b);
    then consider x being object such that
A3: x in A and
A4: x in B^b by XBOOLE_0:3;
    consider x2 being Element of FT such that
A5: x2=x and
A6: U_FT x2 meets B by A4;
    set y = the Element of U_FT x2 /\ B;
A7: U_FT x2 /\ B <>{} by A6,XBOOLE_0:def 7;
    then
A8: y in U_FT x2 by XBOOLE_0:def 4;
    then reconsider y2=y as Element of FT;
    x2 in U_FT y2 by A1,A8;
    then x2 in U_FT y2 /\ A by A3,A5,XBOOLE_0:def 4;
    then U_FT y2 meets A by XBOOLE_0:def 7;
    then
A9: y2 in A^b;
    y in B by A7,XBOOLE_0:def 4;
    hence contradiction by A2,A9,XBOOLE_0:3;
  end;
  hence thesis;
end;

theorem
  for FT being filled non empty RelStr, A,B being Subset of FT st FT
  is symmetric & A misses (B^b) holds A^b misses B by Th8;

theorem
  for FT being filled non empty RelStr, A,B being Subset of FT st FT
  is symmetric holds A,B are_separated iff A^b misses B
by Th8;

theorem
  for FT being filled non empty RelStr, A,B being Subset of FT st FT
  is symmetric holds A,B are_separated iff A misses (B^b)
by Th8;

theorem Th12:
  for FT being filled non empty RelStr, IT being Subset of FT st
FT is symmetric holds IT is connected iff (for A, B being Subset of FT st IT =
  A \/ B & A,B are_separated holds A = IT or B = IT)
proof
  let FT be filled non empty RelStr,IT be Subset of FT;
  assume
A1: FT is symmetric;
A2: now
    assume
A3: for A, B being Subset of FT st IT = A \/ B & A,B are_separated
    holds A = IT or B = IT;
    for A,B being Subset of FT st IT = A \/ B & A <> {} & B <> {} & A
    misses B holds A^b meets B
    proof
      let A,B be Subset of FT;
      assume that
A4:   IT = A \/ B and
A5:   A <> {} & B <> {} and
      A misses B;
      now
        assume
A6:     A^b misses B;
        now
          assume A meets (B^b);
          then consider x being object such that
A7:       x in A and
A8:       x in B^b by XBOOLE_0:3;
          consider x2 being Element of FT such that
A9:       x2=x and
A10:      U_FT x2 meets B by A8;
          set y = the Element of U_FT x2 /\ B;
A11:      U_FT x2 /\ B <>{} by A10,XBOOLE_0:def 7;
          then
A12:      y in U_FT x2 by XBOOLE_0:def 4;
          then reconsider y2=y as Element of FT;
          x2 in U_FT y2 by A1,A12;
          then x2 in U_FT y2 /\ A by A7,A9,XBOOLE_0:def 4;
          then U_FT y2 meets A by XBOOLE_0:def 7;
          then
A13:      y2 in A^b;
          y in B by A11,XBOOLE_0:def 4;
          hence contradiction by A6,A13,XBOOLE_0:3;
        end;
        then A,B are_separated by A6;
        then
A14:    A=IT or B=IT by A3,A4;
A15:    A c= A^b by FIN_TOPO:13;
        A^b /\ B={} by A6,XBOOLE_0:def 7;
        then A /\ B ={} by A15,XBOOLE_1:3,26;
        hence contradiction by A4,A5,A14,XBOOLE_1:21;
      end;
      hence thesis;
    end;
    hence IT is connected;
  end;
  now
    assume
A16: IT is connected;
    thus for A, B being Subset of FT st IT = A \/ B & A,B are_separated holds
    A = IT or B = IT
    proof
      let A, B be Subset of FT;
      assume that
A17:  IT = A \/ B and
A18:  A,B are_separated;
A19:  A misses B by A18,Th6;
      now
        assume A<>{};
        then B={} by A18,A16,A17,A19;
        hence thesis by A17;
      end;
      hence thesis by A17;
    end;
  end;
  hence thesis by A2;
end;

theorem
  for FT being filled non empty RelStr, B being Subset of FT st FT is
symmetric holds B is connected iff not (ex C being Subset of FT st C<>{} & B\C
  <>{} & C c= B & (C^b) misses (B\C))
proof
  let FT be filled non empty RelStr, B be Subset of FT;
  assume
A1: FT is symmetric;
  thus B is connected implies not (ex C being Subset of FT st C<>{} & B\C <>{}
  & C c= B & (C^b) misses (B\C))
  proof
    assume
A2: B is connected;
    for C being Subset of FT st C c= B & (C^b) misses (B\C) holds C={} or
    B\C={}
    proof
      let C be Subset of FT;
      assume that
A3:   C c= B and
A4:   (C^b) misses (B\C);
      C misses ((B\C)^b) by A1,A4,Th8;
      then
A5:   C,B\C are_separated by A4;
      C \/ (B\C)=C \/ B by XBOOLE_1:39
        .=B by A3,XBOOLE_1:12;
      then C = B or B\C = B by A1,A2,A5,Th12;
      hence thesis by A3,XBOOLE_1:37,38;
    end;
    hence thesis;
  end;
  thus not (ex C being Subset of FT st C<>{} & B\C <>{} & C c= B & (C^b)
  misses (B\C)) implies B is connected
  proof
    assume
A6: not (ex C being Subset of FT st C<>{} & B\C <>{} & C c= B & (C^b)
    misses (B\C));
    for A, B2 being Subset of FT st B = A \/ B2 & A,B2 are_separated
    holds A = B or B2 = B
    proof
      let A, B2 be Subset of FT;
      assume that
A7:   B = A \/ B2 and
A8:   A,B2 are_separated;
A9:   (A \/ B2) \A =B2\A by XBOOLE_1:40;
      A^b misses B2 by A8;
      then A^b misses (B\A) by A7,A9,XBOOLE_1:36,63;
      then A={} or B\A={} by A6,A7,XBOOLE_1:7;
      then
A10:  B=B2 or B c= A by A7,XBOOLE_1:37;
      A c= B by A7,XBOOLE_1:7;
      hence thesis by A10,XBOOLE_0:def 10;
    end;
    hence thesis by A1,Th12;
  end;
end;

definition
  let FT1,FT2 be non empty RelStr, f be Function of FT1, FT2, n be Nat;
  pred f is_continuous n means

  for x being Element of FT1,y being
Element of FT2 st x in the carrier of FT1 & y=f.x holds f.:(U_FT(x,0)) c= U_FT(
  y,n);
end;

theorem
  for FT1 being non empty RelStr, FT2 being filled non empty RelStr, n
being Element of NAT, f being Function of FT1, FT2 st f is_continuous 0 holds f
  is_continuous n
proof
  let FT1 be non empty RelStr, FT2 be filled non empty RelStr,n be Element
  of NAT, f be Function of FT1, FT2;
  assume
A1: f is_continuous 0;
  for x being Element of FT1,y being Element of FT2 st x in the carrier of
  FT1 & y=f.x holds f.:( U_FT(x,0)) c= U_FT(y,n)
  proof
    let x be Element of FT1,y be Element of FT2;
    assume that
    x in the carrier of FT1 and
A2: y=f.x;
    U_FT y =U_FT(y,0) & U_FT(y,n)=Finf((U_FT y),n) by FINTOPO3:47,def 10;
    then
A3: U_FT(y,0) c= U_FT(y,n) by FINTOPO3:36;
    f.:( U_FT(x,0)) c= U_FT(y,0) by A1,A2;
    hence thesis by A3;
  end;
  hence thesis;
end;

theorem
  for FT1 being non empty RelStr, FT2 being filled non empty RelStr,
n0,n being Element of NAT, f being Function of FT1, FT2 st f is_continuous n0 &
  n0<=n holds f is_continuous n
proof
  let FT1 be non empty RelStr, FT2 be filled non empty RelStr,n0,n be
  Element of NAT, f be Function of FT1, FT2;
  assume that
A1: f is_continuous n0 and
A2: n0<=n;
  for x being Element of FT1,y being Element of FT2 st x in the carrier of
  FT1 & y=f.x holds f.:( U_FT(x,0)) c= U_FT(y,n)
  proof
    let x be Element of FT1,y be Element of FT2;
    assume that
    x in the carrier of FT1 and
A3: y=f.x;
    U_FT(y,n0)=Finf((U_FT y),n0) & U_FT(y,n)=Finf((U_FT y),n) by
FINTOPO3:def 10;
    then
A4: U_FT(y,n0) c= U_FT(y,n) by A2,Th1;
    f.:( U_FT(x,0)) c= U_FT(y,n0) by A1,A3;
    hence thesis by A4;
  end;
  hence thesis;
end;

theorem Th16:
  for FT1,FT2 being non empty RelStr, A being Subset of FT1,B
being Subset of FT2, f being Function of FT1, FT2 st f is_continuous 0 & B=f.:A
  holds f.:(A^b) c= B^b
proof
  let FT1,FT2 be non empty RelStr,A be Subset of FT1, B be Subset of FT2, f be
  Function of FT1, FT2;
  assume that
A1: f is_continuous 0 and
A2: B=f.:A;
  thus f.:(A^b) c= B^b
  proof
    let y be object;
    assume y in f.:(A^b);
    then consider x being object such that
A3: x in dom f and
A4: x in A^b and
A5: y=f.x by FUNCT_1:def 6;
    reconsider x0=x as Element of FT1 by A3;
    reconsider y0=y as Element of FT2 by A3,A5,FUNCT_2:5;
    f.:( U_FT(x0,0)) c= U_FT(y0,0) by A1,A5;
    then f.:(U_FT x0) c= U_FT(y0,0) by FINTOPO3:47;
    then f.:(U_FT x0) c= U_FT y0 by FINTOPO3:47;
    then
A6: f.:((U_FT x0) /\ A) c= (f.:((U_FT x0)))/\ (f.:A) & (f.:((U_FT x0)))/\
    (f.:A) c= (U_FT y0) /\ (f.:A) by RELAT_1:121,XBOOLE_1:26;
    ex z being Element of FT1 st z=x & U_FT z meets A by A4;
    then
A7: U_FT x0 /\ A<>{} by XBOOLE_0:def 7;
    dom f=the carrier of FT1 by FUNCT_2:def 1;
    then f.:((U_FT x0) /\ A)<>{} by A7,RELAT_1:119;
    then (U_FT y0) /\ (f.:A)<>{} by A6;
    then U_FT y0 meets B by A2,XBOOLE_0:def 7;
    hence thesis;
  end;
end;

theorem
  for FT1,FT2 being non empty RelStr,A being Subset of FT1, B being
Subset of FT2, f being Function of FT1, FT2 st A is connected & f is_continuous
  0 & B=f.:A holds B is connected
proof
  let FT1,FT2 be non empty RelStr,A be Subset of FT1, B be Subset of FT2, f be
  Function of FT1, FT2;
  assume that
A1: A is connected and
A2: f is_continuous 0 and
A3: B=f.:A;
  for B2,C2 being Subset of FT2 st B = B2 \/ C2 & B2 <> {} & C2 <> {} & B2
  misses C2 holds B2^b meets C2
  proof
    let B2,C2 be Subset of FT2;
    assume that
A4: B = B2 \/ C2 and
A5: B2 <> {} and
A6: C2 <> {} and
A7: B2 misses C2;
    reconsider C1=f"C2 as Subset of FT1;
    reconsider C10=C1 /\ A as Subset of FT1;
    reconsider B1 = f"B2 as Subset of FT1;
    reconsider B10=B1/\A as Subset of FT1;
A8: C10 c= C1 by XBOOLE_1:17;
    set x6 = the Element of C2;
    x6 in B by A4,A6,XBOOLE_0:def 3;
    then consider z6 being object such that
A9: z6 in dom f and
A10: z6 in A and
A11: x6=f.z6 by A3,FUNCT_1:def 6;
    z6 in f"C2 by A6,A9,A11,FUNCT_1:def 7;
    then
A12: C10<>{} by A10,XBOOLE_0:def 4;
    set x5 = the Element of B2;
    x5 in B by A4,A5,XBOOLE_0:def 3;
    then consider z5 being object such that
A13: z5 in dom f and
A14: z5 in A and
A15: x5=f.z5 by A3,FUNCT_1:def 6;
    A c= the carrier of FT1;
    then
A16: A c= dom f by FUNCT_2:def 1;
    B2 /\ C2 = {} by A7,XBOOLE_0:def 7;
    then f"(B2 /\ C2) = {};
    then B10 c= B1 & (f"B2) /\ (f"C2) = {} by FUNCT_1:68,XBOOLE_1:17;
    then B10 /\ C10= {} by A8,XBOOLE_1:3,27;
    then
A17: B10 misses C10 by XBOOLE_0:def 7;
    (f"B2) \/ (f"C2)=f"(f.:A) by A3,A4,RELAT_1:140;
    then A c= B1 \/ C1 by A16,FUNCT_1:76;
    then A c= A/\(B1\/C1) by XBOOLE_1:19;
    then
A18: A c= B10 \/ C10 by XBOOLE_1:23;
    B10 c= A & C10 c= A by XBOOLE_1:17;
    then B10 \/ C10 c= A by XBOOLE_1:8;
    then
A19: A=B10 \/ C10 by A18,XBOOLE_0:def 10;
    z5 in f"B2 by A5,A13,A15,FUNCT_1:def 7;
    then B10<>{} by A14,XBOOLE_0:def 4;
    then B10^b meets C10 by A1,A19,A12,A17;
    then
A20: B10^b /\ C10 <> {} by XBOOLE_0:def 7;
    reconsider B20 = f.:B1 as Subset of FT2;
A21: dom f=the carrier of FT1 by FUNCT_2:def 1;
    f.:B1 c= B2
    proof
      let y be object;
      assume y in f.:B1;
      then ex x2 being object st x2 in dom f & x2 in B1 & y=f.x2
by FUNCT_1:def 6;
      hence thesis by FUNCT_1:def 7;
    end;
    then
A22: B20^b c= B2^b by FIN_TOPO:14;
    f.:(B1^b) c= B20^b by A2,Th16;
    then f.:(B1^b) c= B2^b by A22;
    then
A23: (f.:(B1^b)) /\ (f.:C1) c= (f.:(B1^b)) /\ C2 & (f.:(B1^b)) /\ C2 c= B2
    ^b /\ C2 by FUNCT_1:75,XBOOLE_1:26;
    B10^b c= B1^b by FIN_TOPO:14,XBOOLE_1:17;
    then B1^b /\ C1 <> {} by A8,A20,XBOOLE_1:3,27;
    then f.:(B1^b /\ C1) <> {} by A21,RELAT_1:119;
    then (f.:(B1^b)) /\ (f.:C1) <> {} by RELAT_1:121,XBOOLE_1:3;
    then B2^b /\ C2 <>{} by A23;
    hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis;
end;

::1 dimensional linear FT_Str

definition
  let n be Nat;
  func Nbdl1 n -> Relation of Seg n means
  :Def3:
  for i being Element of NAT st
  i in Seg n holds Im(it,i)={i,max(i-'1,1),min(i+1,n)};
  existence
  proof
    deffunc F(Nat) = {$1,max($1-'1,1),min($1+1,n)};
A1: for x being Element of NAT st x in Seg n holds F(x) c= Seg n
    proof
      let i be Element of NAT;
      set y0={i,max(i-'1,1),min(i+1,n)};
      assume
A2:   i in Seg n;
      then Seg n <> {};
      then n>0;
      then
A3:   0+1<=n by NAT_1:13;
      thus y0 c=Seg n
      proof
        let z1 be object;
        assume
A4:     z1 in y0;
        then z1=i or z1=max(i-'1,1) or z1=min(i+1,n) by ENUMSET1:def 1;
        then reconsider z2=z1 as Element of NAT by ORDINAL1:def 12;
A5:     now
          i-'1<=i & i<=n by A2,FINSEQ_1:1,NAT_D:35;
          then i-'1<=n by XXREAL_0:2;
          then
A6:       1<= max(i-'1,1) & max(i-'1,1)<=n by A3,XXREAL_0:28,30;
          assume z1=max(i-'1,1);
          hence thesis by A6;
        end;
        now
          1<=i+1 by NAT_1:12;
          then
A7:       1<=min(i+1,n) by A3,XXREAL_0:20;
A8:       min(i+1,n)<=n by XXREAL_0:17;
          assume z1=min(i+1,n);
          hence z2 in Seg n by A7,A8;
        end;
        hence thesis by A2,A4,A5,ENUMSET1:def 1;
      end;
    end;
    consider f being Relation of Seg n such that
A9: for x3 being Element of NAT st x3 in Seg n holds Im(f,x3) = F(x3)
    from RELSET_1:sch 3(A1);
    take f;
    thus thesis by A9;
  end;
  uniqueness
  proof
    thus for f1,f2 being Relation of Seg n st (for i being Element of NAT st i
in Seg n holds Im(f1,i)={i,max(i-'1,1),min(i+1,n)})& (for i being Element of
    NAT st i in Seg n holds Im(f2,i)={i,max(i-'1,1),min(i+1,n)}) holds f1=f2
    proof
      let f1,f2 be Relation of Seg n;
      assume that
A10:  for i being Element of NAT st i in Seg n holds Im(f1,i)={i,max(
      i-'1,1) ,min(i+1,n)} and
A11:  for i being Element of NAT st i in Seg n holds Im(f2,i)={i,max(
      i-' 1,1),min(i+1,n)};
      for x being set st x in Seg n holds Im(f1,x)=Im(f2,x)
      proof
        let x be set;
        assume
A12:    x in Seg n;
        then reconsider i2=x as Element of NAT;
        Im(f1,i2)={i2,max(i2-'1,1),min(i2+1,n)} by A10,A12;
        hence thesis by A11,A12;
      end;
      hence thesis by RELSET_1:31;
    end;
  end;
end;

definition
  let n be Nat;
  assume
A1: n>0;
  func FTSL1 n -> non empty RelStr equals
  :Def4:
  RelStr(# Seg n,Nbdl1 n #);
  correctness by A1;
end;

theorem
  for n being Nat st n>0 holds FTSL1 n is filled
proof
  let n be Nat;
  assume n>0;
  then
A1: FTSL1 n=RelStr(# Seg n,Nbdl1 n #) by Def4;
  let x be Element of FTSL1 n;
  x in Seg n by A1;
  then reconsider i=x as Element of NAT;
  U_FT x= {i,max(i-'1,1),min(i+1,n)} by A1,Def3;
  hence thesis by ENUMSET1:def 1;
end;

theorem
  for n being Nat st n>0 holds FTSL1 n is symmetric
proof
  let n be Nat;
  assume n>0;
  then
A1: FTSL1 n=RelStr(# Seg n,Nbdl1 n #) by Def4;
  let x, y be Element of FTSL1 n;
  x in Seg n by A1;
  then reconsider i=x as Element of NAT;
A2: 1<=i by A1,FINSEQ_1:1;
A3: i<=n by A1,FINSEQ_1:1;
  y in Seg n by A1;
  then reconsider j=y as Element of NAT;
A4: U_FT y= {j,max(j-'1,1),min(j+1,n)} by A1,Def3;
A5: U_FT x= {i,max(i-'1,1),min(i+1,n)} by A1,Def3;
  now
A6: now
      assume
A7:   y=max(i-'1,1);
      now
        per cases;
        case
A8:       i-'1>=1;
          then
A9:       y=i-'1 by A7,XXREAL_0:def 10;
          now
            per cases;
            case
              i-1>=0;
              then j=i-1 by A9,XREAL_0:def 2;
              hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A3,XXREAL_0:def 9
;
            end;
            case
              i-1<0;
              hence contradiction by A8,XREAL_0:def 2;
            end;
          end;
          hence x =j or x=max(j-'1,1) or x= min(j+1,n);
        end;
        case
A10:      i-'1<1;
A11:      now
            assume i>1;
            then
A12:        i-1>0 by XREAL_1:50;
            then i-'1=i-1 by XREAL_0:def 2;
            then i-'1>=0+1 by A12,NAT_1:13;
            hence contradiction by A10;
          end;
          y=1 by A7,A10,XXREAL_0:def 10;
          hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A2,A11,XXREAL_0:1;
        end;
      end;
      hence x in U_FT y by A4,ENUMSET1:def 1;
    end;
    assume
A13: y in U_FT x;
A14: now
      assume y=min(i+1,n);
      now
        per cases by A5,A13,ENUMSET1:def 1;
        case
          y=i;
          hence x =j or x=max(j-'1,1) or x= min(j+1,n);
        end;
        case
A15:      y=max(i-'1,1);
          now
            per cases;
            case
A16:          i-'1>=1;
              then
A17:          y=i-'1 by A15,XXREAL_0:def 10;
              now
                per cases;
                case
                  i-1>=0;
                  then j=i-1 by A17,XREAL_0:def 2;
                  hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A3,
XXREAL_0:def 9;
                end;
                case
                  i-1<0;
                  hence contradiction by A16,XREAL_0:def 2;
                end;
              end;
              hence x =j or x=max(j-'1,1) or x= min(j+1,n);
            end;
            case
A18:          i-'1<1;
A19:          now
                assume i>1;
                then
A20:            i-1>0 by XREAL_1:50;
                then i-'1=i-1 by XREAL_0:def 2;
                then i-'1>=0+1 by A20,NAT_1:13;
                hence contradiction by A18;
              end;
              y=1 by A15,A18,XXREAL_0:def 10;
              hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A2,A19,XXREAL_0:1
;
            end;
          end;
          hence x =j or x=max(j-'1,1) or x= min(j+1,n);
        end;
        case
A21:      y=min(i+1,n);
          now
            per cases;
            case
              i+1<=n;
              then
A22:          y=i+1 by A21,XXREAL_0:def 9;
              then
A23:          j-1=j-'1 by XREAL_0:def 2;
              now
                per cases;
                case
                  j-1>=1;
                  hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A22,A23,
XXREAL_0:def 10;
                end;
                case
                  j-1<1;
                  hence contradiction by A1,A22,FINSEQ_1:1;
                end;
              end;
              hence x =j or x=max(j-'1,1) or x= min(j+1,n);
            end;
            case
A24:          i+1>n;
              then y=n by A21,XXREAL_0:def 9;
              then j+1>n by NAT_1:13;
              then
A25:          min(j+1,n)=n by XXREAL_0:def 9;
              i>=n by A24,NAT_1:13;
              hence x =j or x=max(j-'1,1) or x= min(j+1,n) by A3,A25,XXREAL_0:1
;
            end;
          end;
          hence x =j or x=max(j-'1,1) or x= min(j+1,n);
        end;
      end;
      hence x in U_FT y by A4,ENUMSET1:def 1;
    end;
    y=i or y=max(i-'1,1) or y=min(i+1,n) by A5,A13,ENUMSET1:def 1;
    hence x in U_FT y by A13,A6,A14;
  end;
  hence thesis;
end;

::1 dimensional cyclic FT_Str

definition
  let n be Nat;
  func Nbdc1 n -> Relation of Seg n means
  :Def5:
  for i being Element of NAT st
i in Seg n holds (1<i & i<n implies Im(it,i)={i,i-'1,i+1})& (i=1 & i<n implies
  Im(it,i)={i,n,i+1}) & (1<i & i=n implies Im(it,i)={i,i-'1,1}) & (i=1 & i=n
  implies Im(it,i)={i});
  existence
  proof
    defpred P[object,object] means
for i being Element of NAT st i=$1 holds (1<i & i
    <n implies $2={i,i-'1,i+1})& (i=1 & i<n implies $2={i,n,i+1}) & (1<i & i=n
    implies $2={i,i-'1,1}) & (i=1 & i=n implies $2={i});
A1: for x being object st x in Seg n
   ex y being object st y in bool Seg n & P[x, y]
    proof
      let x be object;
      assume
A2:   x in Seg n;
      then reconsider i2=x as Element of NAT;
A3:   1<=i2 & i2<=n by A2,FINSEQ_1:1;
      now
        per cases by A3,XXREAL_0:1;
        case
A4:       1<i2 & i2<n;
          i2<=i2+1 by NAT_1:12;
          then
A5:       1<i2+1 by A4,XXREAL_0:2;
          i2+1<=n by A4,NAT_1:13;
          then
A6:       i2+1 in Seg n by A5;
          set y0={i2,i2-'1,i2+1};
          i2-1>0 by A4,XREAL_1:50;
          then i2-'1>0 by XREAL_0:def 2;
          then
A7:       i2-'1>=0+1 by NAT_1:13;
          i2-'1<=i2 by NAT_D:35;
          then i2-'1<n by A4,XXREAL_0:2;
          then
A8:       i2-'1 in Seg n by A7;
A9:       y0 c= Seg n
          by A2,A8,A6,ENUMSET1:def 1;
          P[x,y0] by A4;
          hence thesis by A9;
        end;
        case
A10:      i2=1 & i2<n;
          then i2+1<=n by NAT_1:13;
          then
A11:      i2+1 in Seg n by A10;
          set y0={i2,n,i2+1};
A12:      n in Seg n by A10;
A13:      y0 c= Seg n
          by A2,A12,A11,ENUMSET1:def 1;
          P[x,y0] by A10;
          hence thesis by A13;
        end;
        case
A14:      1<i2 & i2=n;
          then i2-1>0 by XREAL_1:50;
          then i2-'1>0 by XREAL_0:def 2;
          then
A15:      i2-'1>=0+1 by NAT_1:13;
          set y0={i2,i2-'1,1};
A16:      1 in Seg n by A14;
          i2-'1<=n by A14,NAT_D:35;
          then
A17:      i2-'1 in Seg n by A15;
A18:      y0 c= Seg n
          by A2,A17,A16,ENUMSET1:def 1;
          P[x,y0] by A14;
          hence thesis by A18;
        end;
        case
A19:      i2=1 & i2=n;
          set y0={i2};
A20:      y0 c= Seg n
          by A2,TARSKI:def 1;
          P[x,y0] by A19;
          hence thesis by A20;
        end;
      end;
      hence thesis;
    end;
    consider f2 being Function of Seg n,bool Seg n such that
A21: for x3 being object st x3 in Seg n holds P[x3,f2.x3] from FUNCT_2:
    sch 1(A1 );
    consider R being Relation of Seg n such that
A22: for i being set st i in Seg n holds Im(R,i) = f2.i by FUNCT_2:93;
    take R;
    let i being Element of NAT;
    assume
A23: i in Seg n;
    then Im(R,i) = f2.i by A22;
    hence thesis by A21,A23;
  end;
  uniqueness
  proof
    let f1,f2 be Relation of Seg n;
    assume that
A24: for i being Element of NAT st i in Seg n holds (1<i & i<n implies
Im( f1,i)={i,i-'1,i+1})& (i=1 & i<n implies Im(f1,i)={i,n,i+1}) & (1<i & i=n
    implies Im(f1,i)={i,i-'1,1}) & (i=1 & i=n implies Im(f1,i)={i}) and
A25: for i being Element of NAT st i in Seg n holds (1<i & i<n implies
    Im(f2,i)={i,i-'1,i+1})& (i=1 & i<n implies Im(f2,i)={i,n,i+1}) & (1<i & i=n
    implies Im(f2,i)={i,i-'1,1}) & (i=1 & i=n implies Im(f2,i)={i});
    for x being set st x in Seg n holds Im(f1,x)=Im(f2,x)
    proof
      let x be set;
      assume
A26:  x in Seg n;
      then reconsider i2=x as Element of NAT;
A27:  1<=i2 & i2<=n by A26,FINSEQ_1:1;
      per cases by A27,XXREAL_0:1;
      suppose
A28:    1<i2 & i2<n;
        set y0={i2,i2-'1,i2+1};
        Im(f1,x)=y0 by A24,A26,A28;
        hence thesis by A25,A26,A28;
      end;
      suppose
A29:    i2=1 & i2<n;
        set y0={i2,n,i2+1};
        Im(f1,x)=y0 by A24,A26,A29;
        hence thesis by A25,A26,A29;
      end;
      suppose
A30:    1<i2 & i2=n;
        set y0={i2,i2-'1,1};
        Im(f1,x)=y0 by A24,A26,A30;
        hence thesis by A25,A26,A30;
      end;
      suppose
A31:    i2=1 & i2=n;
        set y0={i2};
        Im(f1,x)=y0 by A24,A26,A31;
        hence thesis by A25,A26,A31;
      end;
    end;
    hence f1=f2 by RELSET_1:31;
  end;
end;

definition
  let n be Nat;
  assume
A1: n>0;
  func FTSC1 n -> non empty RelStr equals
  :Def6:
  RelStr(# Seg n,Nbdc1 n #);
  correctness by A1;
end;

theorem
  for n being Element of NAT st n>0 holds FTSC1 n is filled
proof
  let n be Element of NAT;
  set f=Nbdc1 n;
  assume n>0;
  then
A1: FTSC1 n=RelStr(# Seg n,Nbdc1 n #) by Def6;
  let x be Element of FTSC1 n;
  x in Seg n by A1;
  then reconsider i=x as Element of NAT;
A2: 1<=i & i<=n by A1,FINSEQ_1:1;
A3: i=1 & i<n implies Im(f,i)={i,n,i+1} by A1,Def5;
A4: 1<i & i<n implies Im(f,i)={i,i-'1,i+1} by A1,Def5;
A5: i=1 & i=n implies Im(f,i)={i} by A1,Def5;
A6: 1<i & i=n implies Im(f,i)={i,i-'1,1} by A1,Def5;
  per cases by A2,XXREAL_0:1;
  suppose
    1<i & i<n;
    hence thesis by A1,A4,ENUMSET1:def 1;
  end;
  suppose
    i=1 & i<n;
    hence thesis by A1,A3,ENUMSET1:def 1;
  end;
  suppose
    1<i & i=n;
    hence thesis by A1,A6,ENUMSET1:def 1;
  end;
  suppose
    i=1 & i=n;
    hence thesis by A1,A5,TARSKI:def 1;
  end;
end;

theorem
  for n being Element of NAT st n>0 holds FTSC1 n is symmetric
proof
  let n be Element of NAT;
  set f=Nbdc1 n;
  assume n>0;
  then
A1: FTSC1 n=RelStr(# Seg n,Nbdc1 n #) by Def6;
  let x, y be Element of FTSC1 n;
  x in Seg n by A1;
  then reconsider i=x as Element of NAT;
A2: 1<=i by A1,FINSEQ_1:1;
A3: i=1 & i<n implies Im(f,i)={i,n,i+1} by A1,Def5;
A4: i=1 & i=n implies Im(f,i)={i} by A1,Def5;
A5: i<=n by A1,FINSEQ_1:1;
  y in Seg n by A1;
  then reconsider j=y as Element of NAT;
A6: 1<=j by A1,FINSEQ_1:1;
A7: 1<i & i=n implies Im(f,i)={i,i-'1,1} by A1,Def5;
A8: 1<i & i<n implies Im(f,i)={i,i-'1,i+1} by A1,Def5;
  assume
A9: y in U_FT x;
A10: j<=n by A1,FINSEQ_1:1;
  per cases by A2,A5,XXREAL_0:1;
  suppose
A11: 1<i & i<n;
A12: now
      i-1>0 by A11,XREAL_1:50;
      then
A13:  i-'1=i-1 by XREAL_0:def 2;
      assume
A14:  y=i-'1;
      per cases by A14,A13;
      suppose
A15:    x=j;
        then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A11,Def5;
        hence thesis by A15,ENUMSET1:def 1;
      end;
      suppose
A16:    x=j-'1;
        then
A17:    i=(i-'1)-'1 by A14;
        now
          assume i<>0;
          then
A18:      i>=0+1 by NAT_1:13;
          then i-1>=1-1 by XREAL_1:9;
          then
A19:      i-1=i-'1 by XREAL_0:def 2;
          now
            assume
A20:        i=1;
            then i-'1-1<0 by A19;
            hence contradiction by A14,A16,A20,XREAL_0:def 2;
          end;
          then i>1 by A18,XXREAL_0:1;
          then i-1>1-1 by XREAL_1:9;
          then i-'1>=0+1 by A19,NAT_1:13;
          then i-'1-1>=0 by XREAL_1:48;
          then i-'1-'1=i-'1-1 by XREAL_0:def 2;
          hence contradiction by A17,A19;
        end;
        hence thesis by A11;
      end;
      suppose
A21:    x=j+1;
        then
A22:    j<n by A5,NAT_1:13;
A23:    now
          assume j<>1;
          then j>1 by A6,XXREAL_0:1;
          then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A22,Def5;
          hence thesis by A21,ENUMSET1:def 1;
        end;
        now
          assume j=1;
          then Im(the InternalRel of FTSC1 n,y)={j,n,j+1} by A1,A22,Def5;
          hence thesis by A21,ENUMSET1:def 1;
        end;
        hence thesis by A23;
      end;
    end;
A24: now
      assume
A25:  y=i+1;
      then
A26:  j-1=x;
      now
        per cases by A11,A26,XREAL_0:def 2;
        case
A27:      x=j;
          then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A11,Def5;
          hence thesis by A27,ENUMSET1:def 1;
        end;
        case
A28:      x=j-'1;
          now
            assume j=1;
            then j-1=0;
            hence contradiction by A11,A28,XREAL_0:def 2;
          end;
          then
A29:      j>1 by A6,XXREAL_0:1;
A30:      now
            assume j<>n;
            then j<n by A10,XXREAL_0:1;
            then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A29,Def5;
            hence thesis by A28,ENUMSET1:def 1;
          end;
          now
            assume j=n;
            then Im(the InternalRel of FTSC1 n,y)={j,j-'1,1} by A1,A29,Def5;
            hence thesis by A28,ENUMSET1:def 1;
          end;
          hence thesis by A30;
        end;
        case
          x=j+1;
          hence contradiction by A25;
        end;
      end;
      hence thesis;
    end;
    y=i or y=i-'1 or y=i+1 by A1,A8,A9,A11,ENUMSET1:def 1;
    hence thesis by A9,A12,A24;
  end;
  suppose
A31: i=1 & i<n;
    per cases by A1,A3,A9,A31,ENUMSET1:def 1;
    suppose
      y=i & y<>n;
      hence thesis by A1,A3,A31,ENUMSET1:def 1;
    end;
    suppose
      y=n;
      then Im(the InternalRel of FTSC1 n,y)={j,j-'1,1} by A1,A31,Def5;
      hence thesis by A31,ENUMSET1:def 1;
    end;
    suppose
A32:  y=i+1 & y<>n;
      then j-1=i;
      then
A33:  j-'1=i by XREAL_0:def 2;
      j<n by A10,A32,XXREAL_0:1;
      then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A31,A32,Def5;
      hence thesis by A33,ENUMSET1:def 1;
    end;
  end;
  suppose
A34: 1<i & i=n;
    per cases by A1,A7,A9,A34,ENUMSET1:def 1;
    suppose
      y=i & y<>1;
      hence thesis by A1,A7,A34,ENUMSET1:def 1;
    end;
    suppose
      y=1;
      then Im(the InternalRel of FTSC1 n,y)={j,n,j+1} by A1,A34,Def5;
      hence thesis by A34,ENUMSET1:def 1;
    end;
    suppose
A35:  y=i-'1 & y<>1;
      then
A36:  1<j by A6,XXREAL_0:1;
      n-1>0 by A34,XREAL_1:50;
      then
A37:  n-1=n-'1 by XREAL_0:def 2;
      n-1+1=n;
      then j<n by A34,A35,A37,NAT_1:13;
      then Im(the InternalRel of FTSC1 n,y)={j,j-'1,j+1} by A1,A36,Def5;
      hence thesis by A34,A35,A37,ENUMSET1:def 1;
    end;
  end;
  suppose
    i=1 & i=n;
    then j=i by A1,A4,A9,TARSKI:def 1;
    hence thesis by A9;
  end;
end;