FINTOPO6

:: Connectedness and Continuous Sequences in Finite Topological Spaces
::  by Yatsuka Nakamura
::
:: Received August 18, 2006
:: Copyright (c) 2006-2026 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, RELAT_2, FIN_TOPO, TARSKI,
      CONNSP_1, PRE_TOPC, STRUCT_0, RELAT_1, RCOMP_1, FINSEQ_1, ORDINAL2,
      XXREAL_0, NAT_1, ARYTM_3, FUNCT_1, ORDINAL4, PARTFUN1, CARD_1, ARYTM_1,
      BORSUK_2, RFINSEQ, FINTOPO3, FINTOPO6;
 notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, ORDINAL1, NUMBERS, XXREAL_0,
      NAT_1, DOMAIN_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FINSEQ_1,
      STRUCT_0, ORDERS_2, FIN_TOPO, FINTOPO3, NAT_D, ENUMSET1, FINTOPO4,
      PRE_TOPC, RFINSEQ;
 constructors DOMAIN_1, EQREL_1, RFINSEQ, RFUNCT_3, NAT_D, FIN_TOPO, FINTOPO3,
      FINTOPO4, REAL_1, RELSET_1;
 registrations XBOOLE_0, RELAT_1, FUNCT_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0,
      FIN_TOPO, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, FIN_TOPO;
 equalities STRUCT_0, SUBSET_1, FIN_TOPO, FINSEQ_1;
 expansions TARSKI, XBOOLE_0, FIN_TOPO;
 theorems NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, RELSET_1, XBOOLE_0, XBOOLE_1,
      FIN_TOPO, FINTOPO3, ENUMSET1, FINTOPO4, FINSEQ_6, TARSKI, XREAL_1,
      SUBSET_1, PRE_TOPC, RFINSEQ, FINSEQ_3, FINSEQ_5, REVROT_1, ORDINAL1,
      XXREAL_0, PARTFUN1, XREAL_0, NAT_D;
 schemes NAT_1, RELSET_1;

begin :: Connectedness and Subspaces

reserve FT for non empty RelStr,
  A,B,C for Subset of FT;

registration
  let FT;
  cluster empty -> connected for Subset of FT;
  coherence;
end;

::$CT

theorem Th1:
  ({}FT)^b={}
proof
  assume not thesis;
  then consider x being object such that
A1: x in ({}FT)^b by XBOOLE_0:def 1;
  ex y being Element of FT st x=y & U_FT y meets {}FT by A1;
  hence contradiction;
end;

registration
  let FT;
  cluster ({}FT)^b -> empty;
  coherence by Th1;
end;

theorem
  for A being Subset of FT st for B,C being Subset of FT st A = B
  \/ C & B <> {} & C <> {} & B misses C holds B^b meets C & B meets C^b holds A
  is connected;

definition
  let FT be non empty RelStr;
  attr FT is connected means

  [#]FT is connected;
end;

theorem Th3:
  for A being Subset of FT holds A is connected implies for A2, B2
  being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated holds
  A2 = {}FT or B2 = {}FT
proof
  let A be Subset of FT;
  assume
A1: A is connected;
  let A2, B2 be Subset of FT;
  assume that
A2: A = A2 \/ B2 & A2 misses B2 and
A3: A2,B2 are_separated;
  A2^b misses B2 by A3,FINTOPO4:def 1;
  hence thesis by A1,A2;
end;

theorem Th4:
  FT is connected implies for A, B being Subset of FT st [#]FT = A
  \/ B & A misses B & A,B are_separated holds A = {}FT or B = {}FT
proof
  assume FT is connected;
  then
A1: [#]FT is connected;
  let A, B be Subset of FT;
  assume that
A2: [#]FT = A \/ B & A misses B and
A3: A,B are_separated;
  A^b misses B by A3,FINTOPO4:def 1;
  hence thesis by A1,A2;
end;

theorem Th5:
  for A,B being Subset of FT st FT is symmetric & A^b misses B
  holds A misses B^b
proof
  let A,B be Subset of FT;
  assume that
A1: FT is symmetric and
A2: A^b misses B;
  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 y being Element of FT such that
A5: x=y and
A6: U_FT y meets B by A4;
  consider z being object such that
A7: z in U_FT y and
A8: z in B by A6,XBOOLE_0:3;
  reconsider z2=z as Element of FT by A7;
  y in U_FT z2 by A1,A7;
  then U_FT z2 meets A by A3,A5,XBOOLE_0:3;
  then
A9: z in A^b;
  A^b /\ B={} by A2;
  hence contradiction by A8,A9,XBOOLE_0:def 4;
end;

theorem Th6:
  for A being Subset of FT st FT is symmetric & for A2, B2 being
Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2 are_separated holds A2 = {}
  FT or B2 = {}FT holds A is connected
proof
  let A be Subset of FT;
  assume
A1: FT is symmetric;
  assume
A2: for A2, B2 being Subset of FT st A = A2 \/ B2 & A2 misses B2 & A2,B2
  are_separated holds A2 = {}FT or B2 = {}FT;
  for B,C being Subset of FT st A = B \/ C & B <> {} & C <> {} & B misses
  C holds B^b meets C & B meets C^b
  proof
    let B,C be Subset of FT;
    assume A = B \/ C & B <> {} & C <> {} & B misses C;
    then not B,C are_separated by A2;
    then not(B^b misses C & B misses (C^b)) by FINTOPO4:def 1;
    hence thesis by A1,Th5;
  end;
  hence thesis;
end;

definition
  let T be RelStr;
  mode SubSpace of T -> RelStr means
    :Def2:
    the carrier of it c= the carrier
of T & for x being Element of it st x in the carrier of it holds U_FT x =Im(the
    InternalRel of T,x) /\ the carrier of it;
  existence
  proof
    for x being Element of T st x in the carrier of T holds U_FT x =Im(the
    InternalRel of T,x)/\ the carrier of T by XBOOLE_1:28;
    hence thesis;
  end;
end;

Lm1: for T being RelStr holds the RelStr of T is SubSpace of T
proof
  let T be RelStr;
  set S = the RelStr of T;
  for x being Element of S st x in the carrier of S holds U_FT x =Im(the
  InternalRel of T,x)/\ (the carrier of T) by XBOOLE_1:28;
  hence thesis by Def2;
end;

registration
  let T be RelStr;
  cluster strict for SubSpace of T;
  existence
  proof
    the RelStr of T is SubSpace of T by Lm1;
    hence thesis;
  end;
end;

registration
  let T be non empty RelStr;
  cluster strict non empty for SubSpace of T;
  existence
  proof
    the RelStr of T is SubSpace of T & the RelStr of T is non empty by Lm1;
    hence thesis;
  end;
end;

definition
  let T be non empty RelStr, P be non empty Subset of T;
  func T|P -> strict non empty SubSpace of T means
  :Def3:
  [#]it = P;
  existence
  proof
    deffunc F(set) = Im(the InternalRel of T,$1) /\ P;
A1: for x being Element of T st x in P holds F(x) c= P by XBOOLE_1:17;
    consider G being Relation of P such that
A2: for y being Element of T st y in P holds Im(G,y)=F(y) from
    RELSET_1:sch 3(A1);
    set FS=RelStr(# P,G #);
    for x being Element of FS st x in the carrier of FS holds U_FT x =Im(
    the InternalRel of T,x)/\ (the carrier of FS) by A2;
    then
    [#]FS = the carrier of FS & FS is strict non empty SubSpace of T by Def2;
    hence thesis;
  end;
  uniqueness
  proof
    let Z1,Z2 be strict non empty SubSpace of T;
    assume that
A3: [#] Z1 = P and
A4: [#] Z2 = P;
    reconsider R1 = the InternalRel of Z1, R2 = the InternalRel of Z2 as
    Relation of P by A3,A4;
    for z being set st z in P holds Im(R1,z) = Im(R2,z)
    proof
      let z be set;
      assume
A5:   z in P;
      then reconsider z1=z as Element of Z1 by A3;
      reconsider z2=z as Element of Z2 by A4,A5;
      thus Im(R1,z) = U_FT z1
        .= Im(the InternalRel of T,z1)/\ (the carrier of Z1) by Def2
        .= U_FT z2 by A3,A4,Def2
        .= Im(R2,z);
    end;
    hence thesis by A3,A4,RELSET_1:31;
  end;
end;

theorem Th7:
  for X being non empty SubSpace of FT st FT is filled holds X is filled
proof
  let X be non empty SubSpace of FT;
  assume
A1: FT is filled;
  let x be Element of X;
  the carrier of X c= the carrier of FT by Def2;
  then reconsider x2=x as Element of FT;
A2: U_FT x= (U_FT x2) /\ ([#]X) by Def2;
  x2 in U_FT x2 by A1;
  hence thesis by A2,XBOOLE_0:def 4;
end;

registration
  let FT be filled non empty RelStr;
  cluster -> filled for non empty SubSpace of FT;
  coherence by Th7;
end;

theorem
  for X being non empty SubSpace of FT st FT is symmetric holds X is symmetric
proof
  let X be non empty SubSpace of FT;
  assume
A1: FT is symmetric;
  for x, y being Element of X holds y in U_FT x implies x in U_FT y
  proof
    let x, y be Element of X;
    assume
A2: y in U_FT x;
    the carrier of X c= the carrier of FT by Def2;
    then reconsider x2=x, y2=y as Element of FT;
A3: U_FT x=U_FT x2 /\ ([#]X) & U_FT y=U_FT y2 /\ ([#]X) by Def2;
    y2 in U_FT x2 implies x2 in U_FT y2 by A1;
    hence thesis by A2,A3,XBOOLE_0:def 4;
  end;
  hence thesis;
end;

theorem Th9:
  for X9 being SubSpace of FT, A being Subset of X9 holds A is Subset of FT
proof
  let X9 be SubSpace of FT, A be Subset of X9;
  the carrier of X9 c= the carrier of FT by Def2;
  hence thesis by XBOOLE_1:1;
end;

theorem
  for P being Subset of FT holds P is closed iff P` is open
proof
  let P be Subset of FT;
  P` is open implies P`` is closed by FIN_TOPO:23;
  hence thesis by FIN_TOPO:24;
end;

theorem
  for A being Subset of FT holds A is open iff (for z being Element of
FT st U_FT z c= A holds z in A)& for x being Element of FT st x in A holds U_FT
  x c= A
proof
  let A be Subset of FT;
  hereby
    assume A is open;
    then
A1: A = A^i;
    hence for z being Element of FT st U_FT z c= A holds z in A;
    for x being Element of FT st x in A holds U_FT x c= A
    proof
      let x be Element of FT;
      assume x in A;
      then ex y being Element of FT st x=y & U_FT y c= A by A1;
      hence thesis;
    end;
    hence for x being Element of FT st x in A holds U_FT x c= A;
  end;
  assume that
A2: for z being Element of FT st U_FT z c= A holds z in A and
A3: for x being Element of FT st x in A holds U_FT x c= A;
A4: A c= { y where y is Element of FT: U_FT y c= A}
  proof
    let u be object;
    assume
A5: u in A;
    then reconsider y2=u as Element of FT;
    U_FT y2 c= A by A3,A5;
    hence thesis;
  end;
  { y where y is Element of FT: U_FT y c= A} c= A
  proof
    let u be object;
    assume u in { y where y is Element of FT: U_FT y c= A};
    then ex y being Element of FT st y=u & U_FT y c= A;
    hence thesis by A2;
  end;
  then A = A^i by A4;
  hence thesis;
end;

theorem Th12:
  for X9 being non empty SubSpace of FT, A being Subset of FT, A1
  being Subset of X9 st A = A1 holds A1^b = (A^b) /\ ([#]X9)
proof
  let X9 be non empty SubSpace of FT, A be Subset of FT, A1 be Subset of X9
  such that
A1: A = A1;
A2: (A^b) /\ ([#]X9) c= A1^b
  proof
    let u be object;
    assume
A3: u in (A^b) /\ ([#]X9);
    then u in A^b by XBOOLE_0:def 4;
    then consider y2 being Element of FT such that
A4: u=y2 and
A5: (U_FT y2) meets A;
    reconsider y3=y2 as Element of X9 by A3,A4;
    consider z being object such that
A6: z in (U_FT y2) and
A7: z in A by A5,XBOOLE_0:3;
    U_FT y3=(U_FT y2) /\ [#]X9 by Def2;
    then z in U_FT y3 by A1,A6,A7,XBOOLE_0:def 4;
    then (U_FT y3) meets A1 by A1,A7,XBOOLE_0:3;
    hence thesis by A4;
  end;
  A1^b c= (A^b) /\ ([#]X9)
  proof
    reconsider Y=X9 as non empty RelStr;
    let x be object;
    assume x in A1^b;
    then consider y being Element of Y such that
A8: y=x and
A9: U_FT y meets A1;
    y in the carrier of X9 & the carrier of Y c= the carrier of FT by Def2;
    then reconsider z=y as Element of FT;
    U_FT y =Im(the InternalRel of FT,y)/\ (the carrier of X9) by Def2;
    then U_FT z meets A by A1,A9,XBOOLE_1:74;
    then z in {u where u is Element of FT: U_FT u meets A};
    hence thesis by A8,XBOOLE_0:def 4;
  end;
  hence thesis by A2;
end;

theorem
  for X9 being non empty SubSpace of FT, P1,Q1 being Subset of FT, P,Q
  being Subset of X9 st P=P1 & Q=Q1 holds P,Q are_separated implies P1,Q1
  are_separated
proof
  let X9 be non empty SubSpace of FT, P1,Q1 be Subset of FT, P,Q be Subset of
  X9 such that
A1: P = P1 & Q = Q1;
  reconsider P2 = P, Q2 = Q as Subset of FT by Th9;
  assume
A2: P,Q are_separated;
  then P^b misses Q by FINTOPO4:def 1;
  then
A3: (P^b) /\ Q = {};
  P misses (Q^b) by A2,FINTOPO4:def 1;
  then
A4: P /\ (Q^b) = {};
  P /\ (Q^b) = P /\ (([#] X9) /\ (Q2^b)) by Th12
    .= P /\ [#] X9 /\ (Q2^b) by XBOOLE_1:16
    .= P2 /\ (Q2^b) by XBOOLE_1:28;
  then
A5: P2 misses Q2^b by A4;
  (P^b) /\ Q = ((P2^b) /\ ([#](X9))) /\ Q by Th12
    .= (P2^b) /\ (Q /\ [#] X9) by XBOOLE_1:16
    .= (P2^b) /\ Q2 by XBOOLE_1:28;
  then (P2^b) misses Q2 by A3;
  hence thesis by A1,A5,FINTOPO4:def 1;
end;

theorem
  for X9 being non empty SubSpace of FT, P,Q being Subset of FT, P1,Q1
  being Subset of X9 st P=P1 & Q=Q1 & P \/ Q c= [#](X9) holds P,Q are_separated
  implies P1,Q1 are_separated
proof
  let X9 be non empty SubSpace of FT, P,Q be Subset of FT, P1,Q1 be Subset of
  X9 such that
A1: P = P1 & Q = Q1 and
A2: P \/ Q c= [#](X9);
  P c= P \/ Q & Q c= P \/ Q by XBOOLE_1:7;
  then reconsider P2 = P, Q2 = Q as Subset of X9 by A2,XBOOLE_1:1;
  assume
A3: P,Q are_separated;
  then P misses (Q^b) by FINTOPO4:def 1;
  then
A4: P /\ (Q^b) = {};
  P2 /\ (Q2^b) = P2 /\ (([#] X9) /\ (Q^b)) by Th12
    .= (P2 /\ [#] X9) /\ (Q^b) by XBOOLE_1:16
    .= P /\ (Q^b) by XBOOLE_1:28;
  then
A5: P2 misses (Q2^b) by A4;
  P2^b = (P^b) /\ [#] X9 by Th12;
  then
A6: (P2^b) /\ Q2 = (P^b) /\ (Q2 /\ [#] X9) by XBOOLE_1:16
    .= (P^b) /\ Q by XBOOLE_1:28;
  P^b misses Q by A3,FINTOPO4:def 1;
  then (P^b) /\ Q = {};
  then (P2^b) misses Q2 by A6;
  hence thesis by A1,A5,FINTOPO4:def 1;
end;

theorem Th15:
  for A being non empty Subset of FT holds A is connected iff FT|A is connected
proof
  let A be non empty Subset of FT;
A1: [#](FT|A)=A by Def3;
  thus A is connected implies (FT|A) is connected
  proof
    assume
A2: A is connected;
    for B2,C2 being Subset of (FT|A) st [#](FT|A) = B2 \/ C2 & B2 <> {} &
    C2 <> {} & B2 misses C2 holds B2^b meets C2
    proof
      let B2,C2 be Subset of (FT|A);
A3:   ([#](FT|A))/\ C2=C2 by XBOOLE_1:28;
      the carrier of (FT|A)=[#](FT|A) .=A by Def3;
      then reconsider B3=B2, C3=C2 as Subset of FT by XBOOLE_1:1;
      assume [#](FT|A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2;
      then
A4:   B3^b meets C3 by A1,A2;
      B2^b /\ C2= B3^b /\ [#](FT|A)/\ C2 by Th12
        .= B3^b /\ C3 by A3,XBOOLE_1:16;
      then B2^b /\ C2 <> {} by A4;
      hence thesis;
    end;
    then [#](FT|A) is connected;
    hence thesis;
  end;
  assume (FT|A) is connected;
  then
A5: [#](FT|A) is connected;
  let B,C be Subset of FT;
  assume that
A6: A = B \/ C and
A7: B <> {} & C <> {} & B misses C;
A8: [#](FT|A) =A by Def3;
  then reconsider B2=B as Subset of (FT|A) by A6,XBOOLE_1:7;
  reconsider C2=C as Subset of (FT|A) by A6,A8,XBOOLE_1:7;
  ([#](FT|A))/\ C2=C2 & B2^b=B^b /\ [#](FT|A) by Th12,XBOOLE_1:28;
  then
A9: B^b /\ C = B2^b /\ C2 by XBOOLE_1:16;
  B2^b meets C2 by A5,A6,A7,A8;
  hence B^b /\ C <> {} by A9;
end;

theorem
  for FT being filled non empty RelStr, A being non empty Subset of FT
st FT is symmetric holds A is connected iff for P,Q being Subset of FT st A = P
  \/ Q & P misses Q & P,Q are_separated holds P = {}FT or Q = {}FT
proof
  let FT be filled non empty RelStr, A be non empty Subset of FT;
  assume
A1: FT is symmetric;
  now
    assume not A is connected;
    then not FT|A is connected by Th15;
    then not [#](FT|A) is connected;
    then consider P,Q being Subset of FT|A such that
A2: [#](FT|A) = P \/ Q and
A3: P <> {} & Q <> {} and
A4: P misses Q and
A5: P^b misses Q;
    reconsider P1 = P, Q1 = Q as Subset of FT by Th9;
    take P1,Q1;
    thus A = P1 \/ Q1 & P1 misses Q1 by A2,A4,Def3;
A6: P^b=P1^b /\ [#](FT|A) by Th12;
    ([#](FT|A))/\ Q1=Q1 by XBOOLE_1:28;
    then P1^b /\ Q1=P1^b /\ ([#](FT|A))/\ Q by XBOOLE_1:16
      .={} by A5,A6;
    then P1^b misses Q1;
    hence P1,Q1 are_separated & P1 <> {}FT & Q1 <> {}FT by A1,A3,FINTOPO4:10;
  end;
  hence thesis by Th3;
end;

theorem
  for A being Subset of FT st FT is filled connected & A <> {} & A` <>
  {} holds A^delta <>{}
proof
  let A be Subset of FT;
  assume that
A1: FT is filled connected and
A2: A <> {} & A` <>{};
A3: now
    assume A^b meets A`;
    then consider x being object such that
A4: x in A^b and
A5: x in A` by XBOOLE_0:3;
    reconsider x as Element of FT by A4;
    x in U_FT x by A1;
    then
A6: U_FT x meets A` by A5,XBOOLE_0:3;
    U_FT x meets A by A4,FIN_TOPO:8;
    hence ex z being Element of FT st U_FT z meets A & U_FT z meets A` by A6;
  end;
A7: now
    assume A meets (A`)^b;
    then consider x being object such that
A8: x in (A`)^b and
A9: x in A by XBOOLE_0:3;
    reconsider x as Element of FT by A8;
    x in U_FT x by A1;
    then
A10: U_FT x meets A by A9,XBOOLE_0:3;
    U_FT x meets A` by A8,FIN_TOPO:8;
    hence ex z being Element of FT st U_FT z meets A & U_FT z meets A` by A10;
  end;
  {}={}FT & A \/ A` = [#]FT by XBOOLE_1:45;
  then not A,A` are_separated by A1,A2,Th4,XBOOLE_1:79;
  hence thesis by A3,A7,FINTOPO4:def 1,FIN_TOPO:5;
end;

theorem
  for A being Subset of FT st FT is filled symmetric & FT is connected &
  A <> {} & A` <> {} holds A^deltai <>{}
proof
  let A be Subset of FT;
  assume that
A1: FT is filled symmetric and
A2: FT is connected & A <> {} & A` <>{};
A3: now
    assume A^b meets A`;
    then consider x being object such that
A4: x in A^b and
A5: x in A` by XBOOLE_0:3;
    reconsider x as Element of FT by A4;
    U_FT x meets A by A4,FIN_TOPO:8;
    then consider y being object such that
A6: y in U_FT x and
A7: y in A by XBOOLE_0:3;
    reconsider y as Element of FT by A6;
    y in U_FT y by A1;
    then
A8: U_FT y meets A by A7,XBOOLE_0:3;
    x in U_FT y by A1,A6;
    then U_FT y meets A` by A5,XBOOLE_0:3;
    then y in A^delta by A8;
    hence thesis by A7,XBOOLE_0:def 4;
  end;
A9: now
    assume A meets (A`)^b;
    then consider x being object such that
A10: x in (A`)^b and
A11: x in A by XBOOLE_0:3;
    reconsider x as Element of FT by A10;
    x in U_FT x by A1;
    then
A12: U_FT x meets A by A11,XBOOLE_0:3;
    U_FT x meets A` by A10,FIN_TOPO:8;
    then x in A^delta by A12;
    hence thesis by A11,XBOOLE_0:def 4;
  end;
  {}={}FT & A \/ A` = [#]FT by XBOOLE_1:45;
  then not A,A` are_separated by A2,Th4,XBOOLE_1:79;
  hence thesis by A3,A9,FINTOPO4:def 1;
end;

theorem
  for A being Subset of FT st FT is filled symmetric & FT is connected &
  A <> {} & A` <>{} holds A^deltao <>{}
proof
  let A be Subset of FT;
  assume that
A1: FT is filled symmetric and
A2: FT is connected & A <> {} & A` <>{};
A3: now
    assume A meets (A`)^b;
    then consider x being object such that
A4: x in (A`)^b and
A5: x in A by XBOOLE_0:3;
    reconsider x as Element of FT by A4;
    U_FT x meets A` by A4,FIN_TOPO:8;
    then consider y being object such that
A6: y in U_FT x and
A7: y in A` by XBOOLE_0:3;
    reconsider y as Element of FT by A6;
    y in U_FT y by A1;
    then
A8: U_FT y meets A` by A7,XBOOLE_0:3;
    x in U_FT y by A1,A6;
    then U_FT y meets A by A5,XBOOLE_0:3;
    then y in A^delta by A8;
    hence thesis by A7,XBOOLE_0:def 4;
  end;
A9: now
    assume A^b meets A`;
    then consider x being object such that
A10: x in A^b and
A11: x in A` by XBOOLE_0:3;
    reconsider x as Element of FT by A10;
    x in U_FT x by A1;
    then
A12: U_FT x meets A` by A11,XBOOLE_0:3;
    U_FT x meets A by A10,FIN_TOPO:8;
    then x in A^delta by A12;
    hence thesis by A11,XBOOLE_0:def 4;
  end;
  {}={}FT & A \/ A` = [#]FT by XBOOLE_1:45;
  then not A,A` are_separated by A2,Th4,XBOOLE_1:79;
  hence thesis by A9,A3,FINTOPO4:def 1;
end;

theorem
  for A being Subset of FT holds A^deltai misses A^deltao
proof
  let A be Subset of FT;
  A misses A` by XBOOLE_1:79;
  then
A1: A /\ A` = {};
  thus A^deltai /\ (A^deltao) = A /\ ((A^delta) /\ A`) /\ (A^delta) by
XBOOLE_1:16
    .= A /\ A` /\ (A^delta) /\ (A^delta) by XBOOLE_1:16
    .= {} by A1;
end;

theorem
  for FT being filled non empty RelStr, A being Subset of FT holds A
  ^deltao=(A^b) \ A
proof
  let FT be filled non empty RelStr,A be Subset of FT;
A1: A` /\ ((A`)^b)=A` by FIN_TOPO:13,XBOOLE_1:28;
  thus A^deltao=A` /\ ((A^b) /\ ((A`)^b)) by FIN_TOPO:18
    .= (A^b) /\ (A` /\ ((A`)^b)) by XBOOLE_1:16
    .= A^b \ A by A1,SUBSET_1:13;
end;

theorem
  for A, B being Subset of FT st A,B are_separated holds A^deltao misses B
proof
  let A,B be Subset of FT;
  assume A,B are_separated;
  then
A1: A^b misses B by FINTOPO4:def 1;
  thus (A^deltao)/\ B = A` /\ ((A^delta) /\ B) by XBOOLE_1:16
    .= A` /\ ((A^b) /\ ((A`)^b)/\ B) by FIN_TOPO:18
    .= A` /\ (((A`)^b) /\ ((A^b)/\ B)) by XBOOLE_1:16
    .= A` /\ (((A`)^b) /\ ({})) by A1
    .= {};
end;

theorem
  for A, B being Subset of FT st FT is filled & A misses B & A^deltao
  misses B & B^deltao misses A holds A,B are_separated
proof
  let A, B be Subset of FT;
  assume that
A1: FT is filled and
A2: A /\ B = {} and
A3: (A^deltao)/\ B = {} and
A4: (B^deltao)/\ A = {};
  B` /\ ((B^delta) /\ A) = {} by A4,XBOOLE_1:16;
  then B` /\ ((B^b) /\ ((B`)^b)/\ A) = {} by FIN_TOPO:18;
  then B` /\ (((B`)^b) /\ ((B^b)/\ A)) = {} by XBOOLE_1:16;
  then
A5: B` /\ ((B`)^b) /\ ((B^b)/\ A) = {} by XBOOLE_1:16;
  B` /\ ((B`)^b)=B` by A1,FIN_TOPO:13,XBOOLE_1:28;
  then B` misses ((B^b)/\ A) by A5;
  then ((B^b)/\ A) c= B by SUBSET_1:24;
  then ((B^b)/\ A)/\ A c= B /\ A by XBOOLE_1:26;
  then (B^b)/\ (A/\ A) c= B /\ A by XBOOLE_1:16;
  then B^b /\ A ={} by A2,XBOOLE_1:3;
  then
A6: A misses B^b;
  A` /\ ((A^delta) /\ B) = {} by A3,XBOOLE_1:16;
  then A` /\ ((A^b) /\ ((A`)^b)/\ B) = {} by FIN_TOPO:18;
  then A` /\ (((A`)^b) /\ ((A^b)/\ B)) = {} by XBOOLE_1:16;
  then
A7: A` /\ ((A`)^b) /\ ((A^b)/\ B) = {} by XBOOLE_1:16;
  A` /\ ((A`)^b)=A` by A1,FIN_TOPO:13,XBOOLE_1:28;
  then A` misses ((A^b)/\ B) by A7;
  then ((A^b)/\ B) c= A by SUBSET_1:24;
  then ((A^b)/\ B)/\ B c= A /\ B by XBOOLE_1:26;
  then (A^b)/\ (B/\ B) c= A /\ B by XBOOLE_1:16;
  then A^b /\ B ={} by A2,XBOOLE_1:3;
  then A^b misses B;
  hence thesis by A6,FINTOPO4:def 1;
end;

theorem Th24:
  for x being Point of FT holds {x} is connected
proof
  let x be Point of FT;
  assume not {x} is connected;
  then consider P,Q being Subset of FT such that
A1: {x} = P \/ Q and
A2: P <> {} and
A3: Q <> {} and
A4: P misses Q and
  not(P^b meets Q & P meets Q^b);
  P <> Q
  by A2,A4;
  hence contradiction by A1,A2,A3,ZFMISC_1:38;
end;

registration
  let FT;
  let x be Point of FT;
  cluster {x} -> connected for Subset of FT;
  coherence by Th24;
end;

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

  A is connected & for B being Subset
  of FT st B is connected holds A c= B implies A = B;
end;

theorem
  for A being Subset of FT st A is_a_component_of FT holds A <> {}FT
proof
  let A be Subset of FT;
  set x = the Point of FT;
  {} c= {x};
  hence thesis;
end;

theorem
  A is closed & B is closed & A misses B implies A,B are_separated
by FINTOPO4:def 1;

theorem Th27:
  FT is filled & [#]FT = A \/ B & A,B are_separated implies A is open closed
proof
  assume that
A1: FT is filled and
A2: [#]FT = A \/ B and
A3: A,B are_separated;
    B c= B^b by A1,FIN_TOPO:13;
   then A misses (B^b) implies B^b = B by A2,XBOOLE_1:73;
  then
A4: B is closed by A3,FINTOPO4:def 1;
    A c= A^b by A1,FIN_TOPO:13;
  then
A5: A^b misses B implies A^b = A by A2,XBOOLE_1:73;
  B`= A by A1,A2,A3,FINTOPO4:6,PRE_TOPC:5;
  hence thesis by A3,A5,A4,FINTOPO4:def 1,FIN_TOPO:24;
end;

theorem Th28:
  for A,B,A1,B1 being Subset of FT holds A,B are_separated & A1 c=
  A & B1 c= B implies A1,B1 are_separated
proof
  let A,B,A1,B1 be Subset of FT;
  assume that
A1: A,B are_separated and
A2: A1 c= A and
A3: B1 c= B;
  A misses (B^b) by A1,FINTOPO4:def 1;
  then
A4: A/\(B^b)={};
  B1^b c= B^b by A3,FIN_TOPO:14;
  then A1 /\ (B1^b) = {}FT by A2,A4,XBOOLE_1:3,27;
  then
A5: A1 misses (B1^b);
  A^b misses B by A1,FINTOPO4:def 1;
  then
A6: A^b /\ B={};
  A1^b c= A^b by A2,FIN_TOPO:14;
  then (A1^b) /\ B1 = {}FT by A3,A6,XBOOLE_1:3,27;
  then (A1^b) misses B1;
  hence thesis by A5,FINTOPO4:def 1;
end;

theorem Th29:
  A,B are_separated & A,C are_separated implies A,B \/ C are_separated
proof
  assume that
A1: A,B are_separated and
A2: A,C are_separated;
A3: (A^b) misses C by A2,FINTOPO4:def 1;
  (A^b) misses B by A1,FINTOPO4:def 1;
  then
A4: (A^b) /\ B = {};
  (A^b) /\ (B \/ C) = ((A^b) /\ B) \/ ((A^b) /\ C) by XBOOLE_1:23
    .= {} by A3,A4;
  then
A5: (A^b) misses (B \/ C);
  A misses (B^b) by A1,FINTOPO4:def 1;
  then
A6: A /\ (B^b) = {};
A7: A misses (C^b) by A2,FINTOPO4:def 1;
  A /\ ((B \/ C)^b) = A /\ ((B^b) \/ (C^b)) by FINTOPO3:8
    .= (A /\ (B^b)) \/ (A /\ (C^b)) by XBOOLE_1:23
    .= {} by A7,A6;
  then A misses ((B \/ C)^b);
  hence thesis by A5,FINTOPO4:def 1;
end;

theorem
  FT is filled symmetric & ( for A, B being Subset of FT st [#]FT = A \/
B & A <> {}FT & B <> {}FT & A is closed & B is closed holds A meets B) implies
  FT is connected
proof
  assume
A1: FT is filled symmetric;
  assume
A2: for A, B being Subset of FT st [#]FT = A \/ B & A <> {}FT & B <> {}
  FT & A is closed & B is closed holds A meets B;
  assume not FT is connected;
  then not [#]FT is connected;
  then consider P, Q being Subset of FT such that
A3: [#]FT = P \/ Q and
A4: P misses Q and
A5: P,Q are_separated and
A6: P <> {}FT & Q <> {}FT by A1,Th6;
  P is closed & Q is closed by A1,A3,A5,Th27;
  hence contradiction by A2,A3,A4,A6;
end;

theorem
  FT is connected implies for A, B being Subset of FT st [#]FT = A \/ B
  & A <> {}FT & B <> {}FT & A is closed & B is closed holds A meets B
proof
  assume
A1: [#]FT is connected;
  given A, B being Subset of FT such that
A2: [#]FT = A \/ B & A <> {}FT & B <> {}FT & A is closed & B is closed &
  A misses B;
  thus contradiction by A1,A2;
end;

theorem Th32:
  FT is filled & A is connected & A c= B \/ C & B,C are_separated
  implies A c= B or A c= C
proof
  assume that
A1: FT is filled and
A2: A is connected and
A3: A c= B \/ C and
A4: B,C are_separated;
A5: (A /\ B) \/ (A /\ C) = A /\ (B \/ C) by XBOOLE_1:23
    .= A by A3,XBOOLE_1:28;
  assume that
A6: not A c= B and
A7: not A c= C;
  A meets B by A3,A7,XBOOLE_1:73;
  then
A8: A /\ B <> {};
  A meets C by A3,A6,XBOOLE_1:73;
  then
A9: A /\ C <> {};
A10: A /\ B c= B & A /\ C c= C by XBOOLE_1:17;
  then {}FT={} & (A /\ B) misses (A /\ C) by A1,A4,Th28,FINTOPO4:6;
  hence contradiction by A2,A4,A8,A9,A10,A5,Th3,Th28;
end;

theorem Th33:
  for A,B being Subset of FT st FT is symmetric & A is connected &
  B is connected & not A,B are_separated holds A \/ B is connected
proof
  let A,B be Subset of FT;
  assume that
A1: FT is symmetric and
A2: A is connected and
A3: B is connected and
A4: not A,B are_separated;
  given P,Q being Subset of FT such that
A5: A \/ B = P \/ Q and
A6: P <> {} and
A7: Q <> {} and
A8: P misses Q and
A9: P^b misses Q;
  set P2=A/\P,Q2=A/\Q;
A10: P2 misses Q2 by A8,XBOOLE_1:76;
A11: Q^b misses P by A1,A9,Th5;
A12: now
    assume that
A13: A c= Q and
A14: B c= P;
    per cases by A4,FINTOPO4:def 1;
    suppose
      A^b meets B;
      then Q^b meets B by A13,FIN_TOPO:14,XBOOLE_1:63;
      hence contradiction by A11,A14,XBOOLE_1:63;
    end;
    suppose
      A meets (B^b);
      then not A^b misses B by A1,Th5;
      then Q^b meets B by A13,FIN_TOPO:14,XBOOLE_1:63;
      hence contradiction by A11,A14,XBOOLE_1:63;
    end;
  end;
A15: now
    assume
A16: A/\P={};
    then
A17: A/\Q=A/\P \/ A/\Q .=A/\(P\/Q) by XBOOLE_1:23
      .=A by A5,XBOOLE_1:21;
A18: now
      assume B/\Q={};
      then B/\P=B/\Q \/ B/\P .=B/\(Q\/P) by XBOOLE_1:23
        .=B by A5,XBOOLE_1:21;
      hence contradiction by A12,A17,XBOOLE_1:18;
    end;
    set P3=B/\P,Q3=B/\Q;
A19: P3\/Q3=B/\(P\/Q) by XBOOLE_1:23
      .=B by A5,XBOOLE_1:21;
A20: P3 misses Q3 by A8,XBOOLE_1:76;
    P3^b c= P^b & Q3 c= Q by FIN_TOPO:14,XBOOLE_1:17;
    then
A21: P3^b misses Q3 by A9,XBOOLE_1:64;
    B/\P=A/\P \/ B/\P by A16
      .=(A\/B)/\P by XBOOLE_1:23
      .=P by A5,XBOOLE_1:21;
    hence contradiction by A3,A6,A18,A19,A20,A21;
  end;
A22: now
    assume that
A23: A c= P and
A24: B c= Q;
A25: A^b c= P^b by A23,FIN_TOPO:14;
    per cases by A4,FINTOPO4:def 1;
    suppose
      A^b meets B;
      hence contradiction by A9,A24,A25,XBOOLE_1:64;
    end;
    suppose
      A meets (B^b);
      then not A^b misses B by A1,Th5;
      hence contradiction by A9,A24,A25,XBOOLE_1:64;
    end;
  end;
A26: now
    assume
A27: A/\Q={};
    then
A28: A/\P=A/\Q \/ A/\P .=A/\(Q\/P) by XBOOLE_1:23
      .=A by A5,XBOOLE_1:21;
A29: now
      assume B/\P={};
      then B/\Q=B/\P \/ B/\Q .=B/\(P\/Q) by XBOOLE_1:23
        .=B by A5,XBOOLE_1:21;
      hence contradiction by A22,A28,XBOOLE_1:18;
    end;
    set P3=B/\Q,Q3=B/\P;
A30: Q3\/P3=B/\(P\/Q) by XBOOLE_1:23
      .=B by A5,XBOOLE_1:21;
A31: P3 misses Q3 by A8,XBOOLE_1:76;
    P3^b c= Q^b & Q3 c= P by FIN_TOPO:14,XBOOLE_1:17;
    then
A32: P3^b misses Q3 by A11,XBOOLE_1:64;
    B/\Q=A/\Q \/ B/\Q by A27
      .=(A\/B)/\Q by XBOOLE_1:23
      .=Q by A5,XBOOLE_1:21;
    hence contradiction by A3,A7,A29,A30,A31,A32;
  end;
  P2^b c= P^b & Q2 c= Q by FIN_TOPO:14,XBOOLE_1:17;
  then
A33: P2^b misses Q2 by A9,XBOOLE_1:64;
  P2\/Q2=A/\(P\/Q) by XBOOLE_1:23
    .=A by A5,XBOOLE_1:21;
  hence contradiction by A2,A15,A26,A10,A33;
end;

theorem Th34:
  for A,C being Subset of FT st FT is symmetric & C is connected &
  C c= A & A c=C^b holds A is connected
proof
  let A,C be Subset of FT;
  assume that
A1: FT is symmetric and
A2: C is connected and
A3: C c= A and
A4: A c= C^b;
  let P2,Q2 be Subset of FT;
  assume that
A5: A=P2\/Q2 and
A6: P2<>{} and
A7: Q2<>{} and
A8: P2 misses Q2;
  assume
A9: not thesis;
  set x2 = the Element of Q2;
A10: x2 in Q2 by A7;
  Q2 c= Q2 \/P2 by XBOOLE_1:7;
  then Q2 c= C^b by A4,A5;
  then x2 in C^b by A10;
  then consider z2 being Element of FT such that
A11: z2=x2 and
A12: U_FT z2 meets C;
  set y3 = the Element of U_FT z2 /\ C;
A13: U_FT z2 /\ C <> {} by A12;
  then y3 in U_FT z2 /\ C;
  then reconsider y4=y3 as Element of FT;
  y3 in U_FT z2 by A13,XBOOLE_0:def 4;
  then z2 in U_FT y4 by A1;
  then z2 in U_FT y4 /\ Q2 by A7,A11,XBOOLE_0:def 4;
  then
A14: U_FT y4 meets Q2;
  set P3=P2/\C,Q3=Q2/\C;
A15: C = A /\ C by A3,XBOOLE_1:28
    .=P3 \/ Q3 by A5,XBOOLE_1:23;
  set x = the Element of P2;
A16: x in P2 by A6;
  P2 c= P2\/Q2 by XBOOLE_1:7;
  then P2 c= C^b by A4,A5;
  then x in C^b by A16;
  then consider z being Element of FT such that
A17: z=x and
A18: U_FT z meets C;
  set y = the Element of U_FT z /\ C;
A19: U_FT z /\ C <> {} by A18;
  then y in U_FT z /\ C;
  then reconsider y2=y as Element of FT;
  y in U_FT z by A19,XBOOLE_0:def 4;
  then z in U_FT y2 by A1;
  then z in (U_FT y2)/\P2 by A6,A17,XBOOLE_0:def 4;
  then (U_FT y2) meets P2;
  then
A20: y2 in P2^b;
A21: y4 in C by A13,XBOOLE_0:def 4;
A22: now
    assume Q3={};
    then
A23: y4 in P2 by A21,A15,XBOOLE_0:def 4;
    consider w being Element of FT such that
A24: w=y4 and
A25: U_FT w meets Q2 by A14;
    consider s being object such that
A26: s in U_FT w and
A27: s in Q2 by A25,XBOOLE_0:3;
    reconsider s2=s as Element of FT by A26;
    w in U_FT s2 by A1,A26;
    then U_FT s2 meets P2 by A23,A24,XBOOLE_0:3;
    then s2 in P2^b;
    hence contradiction by A9,A27,XBOOLE_0:3;
  end;
A28: P3 c= P2 by XBOOLE_1:17;
A29: y2 in C by A19,XBOOLE_0:def 4;
A30: now
    assume P3={};
    then y2 in Q2 by A29,A15,XBOOLE_0:def 4;
    then y2 in P2^b /\ Q2 by A20,XBOOLE_0:def 4;
    hence contradiction by A9;
  end;
  P3 misses Q2 by A8,XBOOLE_1:17,63;
  then P3 misses Q3 by XBOOLE_1:17,63;
  then P3^b meets Q3 by A2,A15,A30,A22;
  then P2^b meets Q3 by A28,FIN_TOPO:14,XBOOLE_1:63;
  hence contradiction by A9,XBOOLE_1:17,63;
end;

theorem Th35:
  for C being Subset of FT st FT is filled symmetric & C is
  connected holds C^b is connected
proof
  let C be Subset of FT;
  assume that
A1: FT is filled symmetric and
A2: C is connected;
  C c= C^b by A1,FIN_TOPO:13;
  hence thesis by A1,A2,Th34;
end;

theorem Th36:
  FT is filled symmetric connected & A is connected & [#]FT \ A =
  B \/ C & B,C are_separated implies A \/ B is connected
proof
  assume that
A1: FT is filled symmetric and
A2: FT is connected and
A3: A is connected and
A4: [#]FT \ A = B \/ C and
A5: B,C are_separated;
A6: [#]FT is connected by A2;
  now
    let P,Q be Subset of FT such that
A7: A \/ B = P \/ Q and
    P misses Q and
A8: P,Q are_separated;
A9: [#]FT = A \/ (B \/ C) by A4,XBOOLE_1:45
      .= P \/ Q \/ C by A7,XBOOLE_1:4;
A10: now
A11:  [#]FT = P \/ (Q \/ C) by A9,XBOOLE_1:4;
      assume A c= Q;
      then P misses A by A1,A8,Th28,FINTOPO4:6;
      then P c= B by A7,XBOOLE_1:7,73;
      then
A12:  P,C are_separated by A5,Th28;
      then P misses Q \/ C by A1,A8,Th29,FINTOPO4:6;
      hence P = {}FT or Q = {}FT by A6,A8,A12,A11,Th3,Th29;
    end;
    now
A13:  [#]FT = Q \/ (P \/ C) by A9,XBOOLE_1:4;
      assume A c= P;
      then Q misses A by A1,A8,Th28,FINTOPO4:6;
      then Q c= B by A7,XBOOLE_1:7,73;
      then
A14:  Q,C are_separated by A5,Th28;
      then Q misses P\/C by A1,A8,Th29,FINTOPO4:6;
      hence P = {}FT or Q = {}FT by A6,A8,A14,A13,Th3,Th29;
    end;
    hence P = {}FT or Q = {}FT by A1,A3,A7,A8,A10,Th32,XBOOLE_1:7;
  end;
  hence thesis by A1,Th6;
end;

theorem Th37:
  for X9 being non empty SubSpace of FT, A being Subset of FT, B
  being Subset of X9 st A = B holds A is connected iff B is connected
proof
  let X9 be non empty SubSpace of FT, A8 be Subset of FT, B8 be Subset of X9;
  assume
A1: A8 = B8;
  per cases;
  suppose
    A8={};
    hence thesis by A1;
  end;
  suppose
A2: A8<>{};
    then reconsider A=A8 as non empty Subset of FT;
    reconsider B=B8 as non empty Subset of X9 by A1,A2;
    reconsider X = X9 as non empty RelStr;
A3: now
      assume not A8 is connected;
      then consider P,Q being Subset of FT such that
A4:   A8 = P \/ Q and
A5:   P <> {} & Q <> {} & P misses Q and
A6:   P^b misses Q;
      Q c= A8 by A4,XBOOLE_1:7;
      then reconsider Q9=Q as Subset of X by A1,XBOOLE_1:1;
      P c= A8 by A4,XBOOLE_1:7;
      then reconsider P9=P as Subset of X by A1,XBOOLE_1:1;
A7:   Q9 c= the carrier of X;
      P9^b=P^b /\ [#]X by Th12;
      then P9^b /\ Q9 =P^b /\ ([#]X /\ Q) by XBOOLE_1:16
        .=P^b /\ Q by A7,XBOOLE_1:28
        .={} by A6;
      then (P9^b) misses Q9;
      hence not B8 is connected by A1,A4,A5;
    end;
    now
      assume not B is connected;
      then consider P,Q being Subset of X9 such that
A8:   B8 = P \/ Q & P <> {} & Q <> {} & P misses Q and
A9:   P^b misses Q;
      the carrier of X c= the carrier of FT by Def2;
      then reconsider Q9=Q as Subset of FT by XBOOLE_1:1;
      the carrier of X c= the carrier of FT by Def2;
      then reconsider P9=P as Subset of FT by XBOOLE_1:1;
A10:  P^b=P9^b /\ [#]X by Th12;
      P9^b /\ Q9 =P9^b /\ ([#]X /\ Q) by XBOOLE_1:28
        .=P^b /\ Q by A10,XBOOLE_1:16
        .={} by A9;
      then (P9^b) misses Q9;
      hence not A is connected by A1,A8;
    end;
    hence thesis by A3;
  end;
end;

theorem
  for A being Subset of FT st FT is filled symmetric & A
  is_a_component_of FT holds A is closed
proof
  let A be Subset of FT;
  assume that
A1: FT is filled symmetric and
A2: A is_a_component_of FT;
  A is connected by A2;
  then
A3: A^b is connected by A1,Th35;
  A c= A^b by A1,FIN_TOPO:13;
  hence A = A^b by A2,A3;
end;

theorem Th39:
  for A,B being Subset of FT st FT is symmetric & A
is_a_component_of FT & B is_a_component_of FT holds A = B or A,B are_separated
proof
  let A,B be Subset of FT;
  assume that
A1: FT is symmetric and
A2: A is_a_component_of FT and
A3: B is_a_component_of FT;
A4: A is connected by A2;
  assume that
A5: A <> B and
A6: not A,B are_separated;
  B is connected by A3;
  then A \/ B is connected by A1,A6,A4,Th33;
  then B c= A \/ B & A = A \/ B by A2,XBOOLE_1:7;
  hence contradiction by A3,A5,A4;
end;

theorem
  for A,B being Subset of FT st FT is filled symmetric & A
is_a_component_of FT & B is_a_component_of FT holds A = B or A misses B by Th39
,FINTOPO4:6;

theorem
  for C being Subset of FT st FT is filled symmetric & C is connected
holds for S being Subset of FT st S is_a_component_of FT holds C misses S or C
  c= S
proof
  let C be Subset of FT;
  assume
A1: FT is filled symmetric & C is connected;
  let S be Subset of FT;
  assume
A2: S is_a_component_of FT;
A3: S c= C \/ S by XBOOLE_1:7;
  assume
A4: C meets S;
  S is connected by A2;
  then C \/ S is connected by A1,A4,Th33,FINTOPO4:6;
  then S = C \/ S by A2,A3;
  hence thesis by XBOOLE_1:7;
end;

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

  ex B1 being Subset of FT|A st B1 = B & B1 is_a_component_of FT|A;
end;

theorem
  for D being non empty Subset of FT st FT is filled symmetric & D=[#]FT
\ A holds FT is connected & A is connected & C is_a_component_of D implies [#]
  FT \ C is connected
proof
  let D be non empty Subset of FT;
  assume that
A1: FT is filled symmetric and
A2: D=[#]FT \ A and
A3: FT is connected and
A4: A is connected and
A5: C is_a_component_of D;
  consider C1 being Subset of FT|D such that
A6: C1 = C and
A7: C1 is_a_component_of FT|D by A5;
  reconsider C2 = C1 as Subset of FT by A6;
  C1 c= [#](FT|D);
  then C1 c= [#]FT \ A by A2,Def3;
  then
A8: ([#]FT \ A)` c= C2` by SUBSET_1:12;
  then
A9: A c= C2` by PRE_TOPC:3;
A10: A c= [#]FT \ C2 by A8,PRE_TOPC:3;
A11: C1 is connected by A7;
  now
    A misses C1 by A9,SUBSET_1:23;
    then
A12: A /\ C1 = {};
    let P,Q be Subset of FT such that
A13: [#]FT \ C = P \/ Q and
A14: P misses Q and
A15: P,Q are_separated;
A16: C is connected by A6,A11,Th37;
A17: now
      assume
A18:  A c= Q;
      P c= Q` by A14,SUBSET_1:23;
      then Q misses Q` & A /\ P c= Q /\ Q` by A18,XBOOLE_1:27,79;
      then
A19:  A /\ P c= {};
      (C \/ P ) /\ A = (A /\ C) \/ (A /\ P) by XBOOLE_1:23
        .= {} by A6,A12,A19,XBOOLE_1:3;
      then C \/ P misses A;
      then C \/ P c= A` by SUBSET_1:23;
      then C \/ P c= [#](FT|D) by A2,Def3;
      then reconsider C1P1 = C \/ P as Subset of FT|D;
      C \/ P is connected by A1,A3,A13,A15,A16,Th36;
      then
A20:  C1P1 is connected by Th37;
      C c= C1 \/ P by A6,XBOOLE_1:7;
      then C1P1 = C1 by A6,A7,A20;
      then
A21:  P c= C by A6,XBOOLE_1:7;
      P c= [#]FT \ C by A13,XBOOLE_1:7;
      then C misses C` & P c= C /\ ([#]FT \ C) by A21,XBOOLE_1:19,79;
      then P c= {};
      hence P = {}FT by XBOOLE_1:3;
    end;
A22: P misses P` by XBOOLE_1:79;
A23: Q c= [#]FT \ C by A13,XBOOLE_1:7;
    now
      assume
A24:  A c= P;
      Q c= P` by A14,SUBSET_1:23;
      then A /\ Q c= P /\ P` by A24,XBOOLE_1:27;
      then
A25:  A /\ Q c= {} by A22;
      (C \/ Q) /\ A = (A /\ C) \/ (A /\ Q) by XBOOLE_1:23
        .= {} by A6,A12,A25,XBOOLE_1:3;
      then (C \/ Q) misses A;
      then C \/ Q c= A` by SUBSET_1:23;
      then C \/ Q c= [#](FT|D) by A2,Def3;
      then reconsider C1Q1 = C \/ Q as Subset of FT|D;
      C \/ Q is connected by A1,A3,A13,A15,A16,Th36;
      then
A26:  C1Q1 is connected by Th37;
      C1 c= C1 \/ Q by XBOOLE_1:7;
      then C1Q1 = C1 by A6,A7,A26;
      then Q c= C by A6,XBOOLE_1:7;
      then C misses C` & Q c= C /\ ([#]FT \ C) by A23,XBOOLE_1:19,79;
      then Q c= {};
      hence Q = {}FT by XBOOLE_1:3;
    end;
    hence P = {}FT or Q = {}FT by A1,A4,A6,A10,A13,A15,A17,Th32;
  end;
  hence thesis by A1,Th6;
end;

begin ::Continuous Finite Sequences and Minimum Path

definition
  let FT;
  let f be FinSequence of FT;
  attr f is continuous means

  1<=len f & for i being Nat,x1 being
  Element of FT st 1<=i & i<len f & x1=f.i holds f.(i+1) in U_FT x1;
end;

Lm2: for x being Element of FT holds <*x*> is continuous
by FINSEQ_1:39;

registration
  let FT;
  let x be Element of FT;
  cluster <*x*> -> continuous for FinSequence of FT;
  coherence by Lm2;
end;

theorem Th43:
  for f being FinSequence of FT,x,y being Element of FT st f is
  continuous & y=f.(len f) & x in U_FT y holds f^(<*x*>) is continuous
proof
  let f be FinSequence of FT,x,y be Element of FT;
  assume that
A1: f is continuous and
A2: y=f.(len f) and
A3: x in U_FT y;
  reconsider g=f^(<*x*>) as FinSequence of FT;
A4: dom f=Seg len f by FINSEQ_1:def 3;
A5: len (<*x*>)=1 by FINSEQ_1:39;
A6: for i being Nat,x1 being Element of FT st 1<=i & i<len g & x1=g.i holds
  g.(i+1) in U_FT x1
  proof
    let i be Nat,x1 be Element of FT;
    assume that
A7: 1<=i and
A8: i<len g and
A9: x1=g.i;
    i+1 <=len g & 1<i+1 by A7,A8,NAT_1:13;
    then i+1 in dom g by FINSEQ_3:25;
    then g.(i+1)=g/.(i+1) by PARTFUN1:def 6;
    then reconsider x2=g.(i+1) as Element of FT;
    now
      per cases;
      suppose
A10:    i<len f;
A11:    1<=i+1 by NAT_1:11;
        i+1<=len f by A10,NAT_1:13;
        then i+1 in dom f by A11,FINSEQ_3:25;
        then
A12:    g.(i+1)=f.(i+1) by FINSEQ_1:def 7;
        i in dom f by A4,A7,A10;
        then g.i=f.i by FINSEQ_1:def 7;
        hence x2 in U_FT x1 by A1,A7,A9,A10,A12;
      end;
      suppose
A13:    i>=len f;
        len g=len f+1 by A5,FINSEQ_1:22;
        then
A14:    i<=len f by A8,NAT_1:13;
        then
A15:    i=len f by A13,XXREAL_0:1;
        i in dom f by A4,A7,A14;
        then x1=y by A2,A9,A15,FINSEQ_1:def 7;
        hence x2 in U_FT x1 by A3,A15,FINSEQ_1:42;
      end;
    end;
    hence thesis;
  end;
  len (f^<*x*>)=len f+len (<*x*>) by FINSEQ_1:22
    .=len f+1 by FINSEQ_1:39;
  then len (f^<*x*>)>=1 by NAT_1:11;
  hence thesis by A6;
end;

theorem Th44:
  for f,g being FinSequence of FT st f is continuous & g is
  continuous & g.1 in U_FT (f/.(len f)) holds f^g is continuous
proof
  let f,g be FinSequence of FT;
  assume that
A1: f is continuous and
A2: g is continuous and
A3: g.1 in U_FT (f/.(len f));
A4: len (f^g)=len f+len g by FINSEQ_1:22;
  len g>=1 by A2;
  then len (f^g)>=0+1 by A4,XREAL_1:7;
  hence len (f^g)>=1;
  let i be Nat,x1 be Element of FT;
  set g2=f^g;
A5: dom f=Seg len f by FINSEQ_1:def 3;
A6: len f>=1 by A1;
  assume that
A7: 1<=i and
A8: i<len(f^g) and
A9: x1=(f^g).i;
  i+1 <=len g2 & 1<i+1 by A7,A8,NAT_1:13;
  then i+1 in dom g2 by FINSEQ_3:25;
  then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
  then reconsider x2=g2.(i+1) as Element of FT;
  per cases;
  suppose
A10: i<len f;
A11: 1<=i+1 by NAT_1:11;
    i+1<=len f by A10,NAT_1:13;
    then i+1 in dom f by A11,FINSEQ_3:25;
    then
A12: g2.(i+1)=f.(i+1) by FINSEQ_1:def 7;
    i in dom f by A5,A7,A10;
    then g2.i=f.i by FINSEQ_1:def 7;
    hence thesis by A1,A7,A9,A10,A12;
  end;
  suppose
A13: i>=len f;
    then
A14: i+1>len f by NAT_1:13;
A15: i<len f+len g by A8,FINSEQ_1:22;
A16: len g2=len f+len g by FINSEQ_1:22;
    then
A17: i+1<=len f+len g by A8,NAT_1:13;
    per cases by A13,XXREAL_0:1;
    suppose
A18:  i=len f;
A19:  len f in dom f by A6,FINSEQ_3:25;
      then
A20:  x1=f.(len f) by A9,A18,FINSEQ_1:def 7
        .=f/.(len f) by A19,PARTFUN1:def 6;
      x2=g.(i+1-len f) by A14,A16,A17,FINSEQ_1:24
        .= g.1 by A18;
      hence thesis by A3,A20;
    end;
    suppose
A21:  i>len f;
      set j=i-'len f;
A22:  i-len f>0 by A21,XREAL_1:50;
      then
A23:  i-'len f=i-len f by XREAL_0:def 2;
      then j+1=i+1-len f;
      then
A24:  x2=g.(j+1) by A14,A16,A17,FINSEQ_1:24;
A25:  i-len f<len g by A15,XREAL_1:19;
      i>=len f+1 by A21,NAT_1:13;
      then
A26:  x1=g.j by A9,A15,A23,FINSEQ_1:23;
      i-'len f>=0+1 by A22,A23,NAT_1:13;
      hence thesis by A2,A23,A24,A26,A25;
    end;
  end;
end;

definition
  let FT;
  let A be Subset of FT;
  attr A is arcwise_connected means

  for x1,x2 being Element of FT st x1
in A & x2 in A ex f being FinSequence of FT st f is continuous & rng f c=A & f.
  1=x1 & f.(len f)=x2;
end;

registration
  let FT;
  cluster empty -> arcwise_connected for Subset of FT;
  coherence;
end;

Lm3: for x being Element of FT holds {x} is arcwise_connected
proof
  let x be Element of FT;
  set A={x};
A1: rng (<*x*>) c= A by FINSEQ_1:39;
A2: <*x*>.1=x;
  then
A3: <*x*>.(len <*x*>)=x by FINSEQ_1:40;
  for x1,x2 being Element of FT st x1 in A & x2 in A ex f being
  FinSequence of FT st f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2
  proof
    let x1,x2 be Element of FT;
    assume x1 in A & x2 in A;
    then x1=x & x2=x by TARSKI:def 1;
    hence thesis by A2,A3,A1;
  end;
  hence thesis;
end;

registration
  let FT;
  let x be Element of FT;
  cluster {x} -> arcwise_connected for Subset of FT;
  coherence by Lm3;
end;

theorem
  for A being Subset of FT st FT is symmetric holds A is connected iff A
  is arcwise_connected
proof
  let A be Subset of FT;
  assume
A1: FT is symmetric;
  now
    assume not A is arcwise_connected;
    then consider x1,x2 being Element of FT such that
A2: x1 in A and
A3: x2 in A and
A4: not(ex f being FinSequence of FT st f is continuous & rng f c=A &
    f. 1=x1 & f.(len f)=x2);
A5: {z where z is Element of FT: z in A & ex f being FinSequence of FT st
    f is continuous & rng f c= A & f.1=x1 & f.(len f)=z} c= A
    proof
      let x be object;
      assume x in {z where z is Element of FT: z in A & ex f being
FinSequence of FT st f is continuous & rng f c= A & f.1=x1 & f.(len f)=z};
      then
      ex z being Element of FT st x=z & z in A & ex f being FinSequence of
      FT st f is continuous & rng f c= A & f.1= x1 & f.(len f)=z;
      hence thesis;
    end;
    then reconsider
    G={z where z is Element of FT: z in A & ex f being FinSequence
of FT st f is continuous & rng f c= A & f.1=x1 & f.(len f)=z} as Subset of FT
    by XBOOLE_1:1;
A6: G misses (A\G) by XBOOLE_1:79;
A7: now
      assume G^b meets (A\G);
      then consider u being object such that
A8:   u in G^b and
A9:   u in (A\G) by XBOOLE_0:3;
A10:  not u in G by A9,XBOOLE_0:def 5;
      consider x being Element of FT such that
A11:  u=x and
A12:  U_FT x meets G by A8;
      consider y being object such that
A13:  y in U_FT x and
A14:  y in G by A12,XBOOLE_0:3;
      consider z2 being Element of FT such that
A15:  y=z2 and
      z2 in A and
A16:  ex f being FinSequence of FT st f is continuous & rng f c= A &
      f.1= x1 & f.(len f)=z2 by A14;
      consider f being FinSequence of FT such that
A17:  f is continuous and
A18:  rng f c= A and
A19:  f.1=x1 and
A20:  f.(len f)=z2 by A16;
      reconsider g=f^(<*x*>) as FinSequence of FT;
A21:  rng g =rng f \/ rng (<*x*>) by FINSEQ_1:31
        .=rng f \/ {x} by FINSEQ_1:38;
A22:  u in A by A9,XBOOLE_0:def 5;
      then {x} c= A by A11,ZFMISC_1:31;
      then
A23:  rng g c= A by A18,A21,XBOOLE_1:8;
      1<=len f by A17;
      then 1 in dom f by FINSEQ_3:25;
      then
A24:  g.(len f+1)=x & g.1=x1 by A19,FINSEQ_1:42,def 7;
      x in U_FT z2 by A1,A13,A15;
      then
A25:  g is continuous by A17,A20,Th43;
      len g=len f+len (<*x*>) by FINSEQ_1:22
        .=len f+1 by FINSEQ_1:39;
      hence contradiction by A22,A10,A11,A25,A24,A23;
    end;
A26: now
      {x1} c= A by A2,ZFMISC_1:31;
      then
A27:  rng (<*x1*>) c= A by FINSEQ_1:38;
      assume
A28:  G={};
A29:  (<*x1*>).1=x1;
      then (<*x1*>).(len (<*x1*>))=x1 by FINSEQ_1:39;
      then x1 in G by A2,A27,A29;
      hence contradiction by A28;
    end;
A30: now
      assume A\G={};
      then A c= G by XBOOLE_1:37;
      then G=A by A5;
      then ex z being Element of FT st z=x2 & z in A & ex f being FinSequence
      of FT st f is continuous & rng f c= A & f.1= x1 & f.(len f)=z by A3;
      hence contradiction by A4;
    end;
    A= G \/ (A\G) by A5,XBOOLE_1:45;
    hence not A is connected by A30,A26,A6,A7;
  end;
  hence A is connected implies A is arcwise_connected;
  now
    assume not A is connected;
    then consider P,Q being Subset of FT such that
A31: A=P\/Q and
A32: P<>{} and
A33: Q<>{} and
A34: P misses Q and
A35: P^b misses Q;
    set q0 = the Element of Q;
    q0 in Q by A33;
    then reconsider q1=q0 as Element of FT;
    set p0 = the Element of P;
    p0 in P by A32;
    then reconsider p1=p0 as Element of FT;
A36: p1 in A & q1 in A by A31,A32,A33,XBOOLE_0:def 3;
    thus now
      assume A is arcwise_connected;
      then consider f being FinSequence of FT such that
A37:  f is continuous and
A38:  rng f c=A and
A39:  f.1=p1 and
A40:  f.(len f)=q1 by A36;
      defpred P[Nat] means 1<=$1 & $1<=len f & f.$1 in P;
      len f>=1 by A37;
      then
A41:  ex k being Nat st P[k] by A32,A39;
A42:  for k being Nat st P[k] holds k <= len f;
      consider i0 being Nat such that
A43:  P[i0] & for n being Nat st P[n] holds n <= i0 from NAT_1:sch 6(
      A42,A41 );
      i0<>len f by A33,A34,A40,A43,XBOOLE_0:3;
      then
A44:  i0<len f by A43,XXREAL_0:1;
      then
A45:  i0+1 <=len f by NAT_1:13;
      reconsider u0=f.i0 as Element of FT by A43;
A46:  1<i0+1 by A43,NAT_1:13;
      then i0+1 in dom f by A45,FINSEQ_3:25;
      then
A47:  f.(i0+1) in rng f by FUNCT_1:def 3;
      then reconsider z0=f.(i0+1) as Element of FT;
      z0 in U_FT u0 by A37,A43,A44;
      then f.i0 in U_FT z0 by A1;
      then U_FT z0 meets P by A43,XBOOLE_0:3;
      then
A48:  z0 in P^b;
      now
        assume f.(i0+1) in P;
        then i0+1<=i0 by A43,A45,A46;
        hence contradiction by NAT_1:13;
      end;
      then f.(i0+1) in Q by A31,A38,A47,XBOOLE_0:def 3;
      hence contradiction by A35,A48,XBOOLE_0:3;
    end;
    hence not A is arcwise_connected;
  end;
  hence thesis;
end;

theorem Th46:
  for g being FinSequence of FT, k being Nat st g is continuous &
  1<=k holds g|k is continuous
proof
  let g be FinSequence of FT, k be Nat;
  assume that
A1: g is continuous and
A2: 1<=k;
  per cases;
  suppose
    len g <= k;
    hence thesis by A1,FINSEQ_1:58;
  end;
  suppose
A3: k<=len g;
    hence len(g|k) >= 1 by A2,FINSEQ_1:59;
    let i be Nat,x11 be Element of FT;
    assume that
A4: 1<=i and
A5: i<len (g|k) and
A6: x11=(g|k).i;
A7: len (g|k)=k by A3,FINSEQ_1:59;
    then
A8: (g|k).i=g.i by A5,FINSEQ_3:112;
    i+1<=k by A7,A5,NAT_1:13;
    then
A9: (g|k).(i+1)=g.(i+1) by FINSEQ_3:112;
    i<len g by A3,A7,A5,XXREAL_0:2;
    hence thesis by A1,A4,A6,A8,A9;
  end;
end;

theorem Th47:
  for g being FinSequence of FT, k being Element of NAT st g is
  continuous & k<len g holds g/^k is continuous
proof
  let g be FinSequence of FT, k be Element of NAT;
  assume that
A1: g is continuous and
A2: k<len g;
A3: len g-k>0 by A2,XREAL_1:50;
  then
A4: len g-k=len g -'k by XREAL_0:def 2;
A5: len (g/^k)=len g-k by A2,RFINSEQ:def 1;
A6: for i being Nat,x11 being Element of FT st 1<=i & i<len (g/^k) & x11=(g
  /^k).i holds (g/^k).(i+1) in U_FT x11
  proof
    let i be Nat,x11 be Element of FT;
    assume that
A7: 1<=i and
A8: i<len (g/^k) and
A9: x11=(g/^k).i;
A10: 1<=1+i by NAT_1:11;
    i in dom (g/^k) by A7,A8,FINSEQ_3:25;
    then
A11: (g/^k).(i)=g.(i+k) by A2,RFINSEQ:def 1;
    i<=i+k by NAT_1:11;
    then
A12: i+1+k=i+k+1 & 1<=i+k by A7,XXREAL_0:2;
    i+1<=len g -'k by A5,A4,A8,NAT_1:13;
    then i+1 in dom (g/^k) by A5,A4,A10,FINSEQ_3:25;
    then
A13: (g/^k).(i+1)=g.(i+1+k) by A2,RFINSEQ:def 1;
    i+k<len g-k+k by A5,A8,XREAL_1:6;
    hence thesis by A1,A9,A11,A13,A12;
  end;
  len g -'k>=0+1 by A3,A4,NAT_1:13;
  hence thesis by A5,A4,A6;
end;

definition
  let FT;
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
  pred g is_minimum_path_in A,x1,x2 means

  g is continuous & rng g c=A &
g.1=x1 & g.len g=x2 & for h being FinSequence of FT st h is continuous & rng h
  c=A & h.1=x1 & h.len h=x2 holds len g <= len h;
end;

theorem
  for A being Subset of FT, x being Element of FT st x in A holds <*x*>
  is_minimum_path_in A,x,x
proof
  let A be Subset of FT, x be Element of FT;
  assume
A1: x in A;
  thus <*x*> is continuous;
  {x} c= A by A1,ZFMISC_1:31;
  hence rng <*x*> c= A by FINSEQ_1:38;
  len <*x*> =1 by FINSEQ_1:40;
  hence thesis;
end;

Lm4: for f being FinSequence of FT,A being Subset of FT, x1,x2 being Element
of FT st f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2 ex g being
FinSequence of FT st g is continuous & rng g c=A & g.1=x1 & g.(len g)=x2 & for
h being FinSequence of FT st h is continuous & rng h c=A & h.1=x1 & h.(len h)=
x2 holds len g <= len h
proof
  let f be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
  defpred P[Nat] means ex g being FinSequence of FT st g is continuous & rng g
  c=A & g.1=x1 & g.(len g)=x2 & $1=len g;
  assume f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2;
  then
A1: ex k being Nat st P[k];
  ex k being Nat st P[k] & for n being Nat st P[n] holds k <= n from NAT_1
  :sch 5(A1);
  then consider k0 being Nat such that
A2: P[k0] and
A3: for n being Nat st P[n] holds k0 <= n;
  consider g0 being FinSequence of FT such that
A4: g0 is continuous & rng g0 c=A & g0.1=x1 & g0.(len g0)=x2 and
A5: k0=len g0 by A2;
  for h being FinSequence of FT st h is continuous & rng h c=A & h.1=x1 &
  h.(len h)=x2 holds len g0 <= len h by A3,A5;
  hence thesis by A4;
end;

theorem
  for A being Subset of FT holds A is arcwise_connected iff for x1,x2
  being Element of FT st x1 in A & x2 in A ex g being FinSequence of FT st g
  is_minimum_path_in A,x1,x2
proof
  let A be Subset of FT;
  thus A is arcwise_connected implies for x1,x2 being Element of FT st x1 in A
  & x2 in A ex g being FinSequence of FT st g is_minimum_path_in A,x1,x2
  proof
    assume
A1: A is arcwise_connected;
    thus for x1,x2 being Element of FT st x1 in A & x2 in A ex g being
    FinSequence of FT st g is_minimum_path_in A,x1,x2
    proof
      let x1,x2 be Element of FT;
      assume x1 in A & x2 in A;
      then
      ex f being FinSequence of FT st f is continuous & rng f c= A & f.1=x1
      & f.(len f)=x2 by A1;
      then consider g2 being FinSequence of FT such that
A2:   g2 is continuous & rng g2 c=A & g2.1=x1 & g2.(len g2)=x2 & for h
being FinSequence of FT st h is continuous & rng h c=A & h.1= x1 & h.(len h)=x2
      holds len g2 <= len h by Lm4;
      g2 is_minimum_path_in A,x1,x2 by A2;
      hence thesis;
    end;
  end;
  assume
A3: for x1,x2 being Element of FT st x1 in A & x2 in A ex g being
  FinSequence of FT st g is_minimum_path_in A,x1,x2;
  for x1,x2 being Element of FT st x1 in A & x2 in A ex f being
  FinSequence of FT st f is continuous & rng f c=A & f.1=x1 & f.len f=x2
  proof
    let x1,x2 be Element of FT;
    assume x1 in A & x2 in A;
    then consider g being FinSequence of FT such that
A4: g is_minimum_path_in A,x1,x2 by A3;
A5: g.1=x1 & g.(len g)=x2 by A4;
    g is continuous & rng g c=A by A4;
    hence thesis by A5;
  end;
  hence thesis;
end;

theorem
  for A being Subset of FT,x1,x2 being Element of FT st ex f being
  FinSequence of FT st f is continuous & rng f c=A & f.1=x1 & f.len f=x2 ex g
  being FinSequence of FT st g is_minimum_path_in A,x1,x2
proof
  let A be Subset of FT,x1,x2 be Element of FT;
  given f being FinSequence of FT such that
A1: f is continuous & rng f c=A & f.1=x1 & f.(len f)=x2;
  consider g2 being FinSequence of FT such that
A2: g2 is continuous & rng g2 c=A & g2.1=x1 & g2.(len g2)=x2 & for h
being FinSequence of FT st h is continuous & rng h c=A & h.1= x1 & h.(len h)=x2
  holds len g2 <= len h by A1,Lm4;
  g2 is_minimum_path_in A,x1,x2 by A2;
  hence thesis;
end;

theorem Th51:
  for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT, k being Element of NAT st g is_minimum_path_in A,x1,x2 & 1<=k &
k<=len g holds g|k is continuous & rng (g|k) c=A & (g|k).1=x1 & (g|k).(len (g|k
  ))=g/.k
proof
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT, k be
  Element of NAT;
  assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: 1<=k and
A3: k<=len g;
A4: k in dom g by A2,A3,FINSEQ_3:25;
  g is continuous by A1;
  hence g|k is continuous by A2,Th46;
A5: rng (g|k) c= rng g by FINSEQ_5:19;
  rng g c=A by A1;
  hence rng (g|k) c=A by A5;
  g.1=x1 by A1;
  hence (g|k).1=x1 by A2,FINSEQ_3:112;
  len (g|k)=k by A3,FINSEQ_1:59;
  hence (g|k).(len (g|k))=g.k by FINSEQ_3:112
    .=g/.k by A4,PARTFUN1:def 6;
end;

theorem Th52:
  for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT, k being Element of NAT st g is_minimum_path_in A,x1,x2 & k<len g
holds g/^k is continuous & rng (g/^k) c=A & (g/^k).1=g/.(1+k) & (g/^k).(len (g
  /^k))=x2
proof
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT, k be
  Element of NAT;
  assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: k<len g;
A3: len (g/^k)=len g-k by A2,RFINSEQ:def 1;
  g is continuous by A1;
  hence g/^k is continuous by A2,Th47;
A4: rng (g/^k) c= rng g by FINSEQ_5:33;
  rng g c=A by A1;
  hence rng (g/^k) c=A by A4;
A5: len (g/^k)=len g-k by A2,RFINSEQ:def 1;
  1<=1+k & k+1<=len g by A2,NAT_1:11,13;
  then
A6: 1+k in dom g by FINSEQ_3:25;
A7: len g-k>0 by A2,XREAL_1:50;
  then len g-'k=len g -k by XREAL_0:def 2;
  then len g-k>=0+1 by A7,NAT_1:13;
  then 1 in dom (g/^k) by A5,FINSEQ_3:25;
  hence (g/^k).1=g.(1+k) by A2,RFINSEQ:def 1
    .=g/.(1+k) by A6,PARTFUN1:def 6;
A8: len g-k>0 by A2,XREAL_1:50;
  then
A9: len g-k=len g-'k by XREAL_0:def 2;
  then len g-'k>=0+1 by A8,NAT_1:13;
  then len g-'k in dom (g/^k) by A5,A9,FINSEQ_3:25;
  hence (g/^k).(len (g/^k))=g.(len g-'k+k) by A2,A9,A3,RFINSEQ:def 1
    .=x2 by A1,A9;
end;

theorem
  for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT st g is_minimum_path_in A,x1,x2 holds for k being Nat st 1<=k & k
  <=len g holds g|k is_minimum_path_in A,x1,g/.k
proof
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
  assume
A1: g is_minimum_path_in A,x1,x2;
  then
A2: rng g c=A;
A3: g is continuous by A1;
  then
A4: 1<=len g;
A5: g.(len g)=x2 by A1;
  let k be Nat;
  assume that
A6: 1<=k and
A7: k<=len g;
  reconsider k as Element of NAT by ORDINAL1:def 12;
A8: (g|k).1=x1 & (g|k).(len (g|k))=g/.k by A1,A6,A7,Th51;
A9: g|k is continuous & rng (g|k) c=A by A1,A6,A7,Th51;
  now
    per cases by A7,XXREAL_0:1;
    suppose
A10:  k<len g;
      now
        k in dom g by A6,A7,FINSEQ_3:25;
        then
A11:    g/.k=g.k by PARTFUN1:def 6;
        k+1<=len g by A10,NAT_1:13;
        then
A12:    (g/^k).1=g.(k+1) by FINSEQ_6:114;
        rng (g/^k) c= rng g by FINSEQ_5:33;
        then
A13:    rng (g/^k) c= A by A2;
        assume not g|k is_minimum_path_in A,x1,g/.k;
        then consider h being FinSequence of FT such that
A14:    h is continuous and
A15:    rng h c=A and
A16:    h.1=x1 and
A17:    h.(len h)=g/.k and
A18:    len (g|k) > len h by A9,A8;
        reconsider s=h^(g/^k) as FinSequence of FT;
A19:    len s=len h +len(g/^k) by FINSEQ_1:22;
        rng s = rng h \/ rng (g/^k) by FINSEQ_1:31;
        then
A20:    rng s c= A by A15,A13,XBOOLE_1:8;
A21:    g/^k is continuous by A1,A10,Th52;
        then 1<= len (g/^k);
        then len (g/^k) in dom (g/^k) by FINSEQ_3:25;
        then
A22:    s.(len s)=(g/^k).(len (g/^k)) by A19,FINSEQ_1:def 7
          .=x2 by A5,A10,FINSEQ_6:185;
A23:    1<=len h by A14;
        then 1 in dom h by FINSEQ_3:25;
        then
A24:    s.1=x1 by A16,FINSEQ_1:def 7;
        len h in dom h by A23,FINSEQ_3:25;
        then h.len h=h/.len h by PARTFUN1:def 6;
        then (g/^k).1 in U_FT (h/.(len h)) by A3,A6,A10,A17,A12,A11;
        then
A25:    s is continuous by A14,A21,Th44;
        g=(g|k)^(g/^k) by RFINSEQ:8;
        then len g=len (g|k) + len (g/^k) by FINSEQ_1:22;
        then len s<len g by A18,A19,XREAL_1:8;
        hence contradiction by A1,A25,A20,A24,A22;
      end;
      hence g|k is_minimum_path_in A,x1,g/.k;
    end;
    suppose
A26:  k=len g;
A27:  len g in dom g by A4,FINSEQ_3:25;
      g|k=g by A26,FINSEQ_1:58;
      hence g|k is_minimum_path_in A,x1,g/.k by A1,A26,A27,PARTFUN1:def 6;
    end;
  end;
  hence thesis;
end;

theorem
  for g being FinSequence of FT,A being Subset of FT, x1,x2 being
  Element of FT st g is_minimum_path_in A,x1,x2 holds g is one-to-one
proof
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
  assume
A1: g is_minimum_path_in A,x1,x2;
  then
A2: g is continuous;
A3: for h being FinSequence of FT st h is continuous & rng h c=A & h.1=x1 &
  h.(len h)=x2 holds len g <= len h by A1;
A4: rng g c=A by A1;
A5: g.1=x1 by A1;
A6: g.(len g)=x2 by A1;
  assume not g is one-to-one;
  then consider y1,y2 being object such that
A7: y1 in dom g and
A8: y2 in dom g and
A9: g.y1=g.y2 and
A10: y1<>y2 by FUNCT_1:def 4;
  reconsider n1=y1,n2=y2 as Element of NAT by A7,A8;
A11: dom g=Seg len g by FINSEQ_1:def 3;
  then
A12: 1<=n1 by A7,FINSEQ_1:1;
A13: n2 <=len g by A8,A11,FINSEQ_1:1;
A14: 1<=n2 by A8,A11,FINSEQ_1:1;
A15: n1 <=len g by A7,A11,FINSEQ_1:1;
  per cases by A10,XXREAL_0:1;
  suppose
A16: n1>n2;
    set k=len g-'n1;
    set g2=(g|n2)^(g/^n1);
A17: len (g/^n1)=len g-n1 by A15,RFINSEQ:def 1;
A18: len g-n1>=0 by A15,XREAL_1:48;
    then
A19: len g-'n1=len g-n1 by XREAL_0:def 2;
A20: len (g|n2)=n2 by A13,FINSEQ_1:59;
    then
A21: g2.1=(g|n2).1 by A14,FINSEQ_1:64
      .=g.1 by A14,FINSEQ_3:112;
A22: len g2=len (g|n2)+len (g/^n1) by FINSEQ_1:22
      .=n2+(len g-n1) by A15,A20,RFINSEQ:def 1;
    per cases by A15,XXREAL_0:1;
    suppose
      n1<len g;
      then n1+1<=len g by NAT_1:13;
      then
A23:  n1+1-n1<=len g-n1 by XREAL_1:13;
      then
A24:  0+1<=n2+(len g-n1) by XREAL_1:7;
A25:  g2 is continuous
      proof
        thus len g2 >= 1 by A22,A24;
        let i be Nat,z1 be Element of FT;
        assume that
A26:    1<=i and
A27:    i<len g2 and
A28:    z1=g2.i;
A29:    i+1 <=len g2 by A27,NAT_1:13;
        reconsider i as Element of NAT by ORDINAL1:def 12;
        1<i+1 by A26,NAT_1:13;
        then i+1 in dom g2 by A29,FINSEQ_3:25;
        then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
        then reconsider z2=g2.(i+1) as Element of FT;
        now
          per cases;
          suppose
A30:        i<n2;
            then
A31:        i+1<=n2 by NAT_1:13;
            i+1<=len (g|n2) by A20,A30,NAT_1:13;
            then
A32:        z2=(g|n2).(i+1) by FINSEQ_1:64,NAT_1:12
              .=g.(i+1) by A31,FINSEQ_3:112;
A33:        i<len g by A13,A30,XXREAL_0:2;
            z1=(g|n2).i by A20,A26,A28,A30,FINSEQ_1:64
              .=g.i by A30,FINSEQ_3:112;
            hence z2 in U_FT z1 by A2,A26,A33,A32;
          end;
          suppose
A34:        i>=n2;
            i-n2<n2+(len g-n1)-n2 by A22,A27,XREAL_1:9;
            then
A35:        i-'n2<len g - n1 by A34,XREAL_1:233;
            then
A36:        i-'n2+n1<len g-n1+n1 by XREAL_1:6;
A37:        len (g|n2) +(i-'n2)=n2+(i-n2) by A20,A34,XREAL_1:233
              .=i;
A38:        now
              per cases by A34,XXREAL_0:1;
              suppose
                i>n2;
                then
A39:            i-n2>0 by XREAL_1:50;
                then i-'n2=i-n2 by XREAL_0:def 2;
                then
A40:            0+1<=i-'n2 by A39,NAT_1:13;
                then
A41:            i-'n2 in dom (g/^n1) by A17,A35,FINSEQ_3:25;
                thus z1=(g/^n1).(i-'n2) by A17,A28,A35,A37,A40,FINSEQ_1:65
                  .=g.(i-'n2+n1) by A15,A41,RFINSEQ:def 1;
              end;
              suppose
A42:            i=n2;
                hence z1=(g|n2).n2 by A20,A26,A28,FINSEQ_1:64
                  .=g.(0+n1) by A9,FINSEQ_3:112
                  .=g.(i-'n2+n1) by A42,XREAL_1:232;
              end;
            end;
            i-'n2<len g-'n1 by A15,A35,XREAL_1:233;
            then i-'n2+1<=len g-'n1 by NAT_1:13;
            then
A43:        i-'n2+1<=len (g/^n1) by A15,A17,XREAL_1:233;
            1<=i-'n2+1 by NAT_1:12;
            then
A44:        i-'n2+1 in dom (g/^n1) by A43,FINSEQ_3:25;
            len (g|n2)+(i-'n2+1)=i-n2+1+n2 by A20,A34,XREAL_1:233
              .=i+1;
            then
A45:        z2=(g/^n1).(i-'n2+1) by A43,FINSEQ_1:65,NAT_1:12
              .=g.(i-'n2+1+n1) by A15,A44,RFINSEQ:def 1
              .=g.(i-'n2+n1+1);
            1<=i-'n2+n1 by A12,NAT_1:12;
            hence z2 in U_FT z1 by A2,A38,A45,A36;
          end;
        end;
        hence thesis;
      end;
A46:  rng (g/^n1) c= rng g by FINSEQ_5:33;
      rng g2=rng (g|n2) \/ rng (g/^n1) & rng (g|n2) c= rng g by FINSEQ_1:31
,FINSEQ_5:19;
      then
A47:  rng g2 c= rng g by A46,XBOOLE_1:8;
A48:  k+n1=len g by A19;
A49:  k in dom ((g/^n1)) by A19,A17,A23,FINSEQ_3:25;
      then g2.(len (g|n2) + k) = (g/^n1).k by FINSEQ_1:def 7
        .= x2 by A6,A15,A49,A48,RFINSEQ:def 1;
      then g2.(len g2)=x2 by A20,A22,A18,XREAL_0:def 2;
      then len g<=len g2 by A4,A5,A3,A21,A47,A25,XBOOLE_1:1;
      then len g-n2<= n2+(len g-n1)-n2 by A22,XREAL_1:13;
      hence contradiction by A16,XREAL_1:10;
    end;
    suppose
A50:  n1=len g;
A51:  len (g/^n1)=len g-n1 by A15,RFINSEQ:def 1;
A52:  g2 is continuous
      proof
        thus 1<=len g2 by A8,A11,A22,A50,FINSEQ_1:1;
        let i be Nat,z1 be Element of FT;
        assume that
A53:    1<=i and
A54:    i<len g2 and
A55:    z1=g2.i;
A56:    i+1 <=len g2 by A54,NAT_1:13;
        reconsider i as Element of NAT by ORDINAL1:def 12;
        1<i+1 by A53,NAT_1:13;
        then i+1 in dom g2 by A56,FINSEQ_3:25;
        then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
        then reconsider z2=g2.(i+1) as Element of FT;
        per cases;
        suppose
A57:      i<n2;
          then
A58:      i+1<=n2 by NAT_1:13;
          i+1<=len (g|n2) by A20,A57,NAT_1:13;
          then
A59:      z2=(g|n2).(i+1) by FINSEQ_1:64,NAT_1:12
            .=g.(i+1) by A58,FINSEQ_3:112;
A60:      i<len g by A13,A57,XXREAL_0:2;
          z1=(g|n2).i by A20,A53,A55,A57,FINSEQ_1:64
            .=g.i by A57,FINSEQ_3:112;
          hence thesis by A2,A53,A60,A59;
        end;
        suppose
A61:      i>=n2;
          i-n2<n2+(len g-n1)-n2 by A22,A54,XREAL_1:9;
          then
A62:      i-'n2<len g - n1 by A61,XREAL_1:233;
          then
A63:      i-'n2+n1<len g-n1+n1 by XREAL_1:6;
A64:      len (g|n2) +(i-'n2)=n2+(i-n2) by A20,A61,XREAL_1:233
            .=i;
A65:      now
            per cases by A61,XXREAL_0:1;
            suppose
              i>n2;
              then
A66:          i-n2>0 by XREAL_1:50;
              then i-'n2=i-n2 by XREAL_0:def 2;
              then
A67:          0+1<=i-'n2 by A66,NAT_1:13;
              then
A68:          i-'n2 in dom (g/^n1) by A51,A62,FINSEQ_3:25;
              thus z1=(g/^n1).(i-'n2) by A51,A55,A62,A64,A67,FINSEQ_1:65
                .=g.(i-'n2+n1) by A15,A68,RFINSEQ:def 1;
            end;
            suppose
A69:          i=n2;
              hence z1=(g|n2).n2 by A20,A53,A55,FINSEQ_1:64
                .=g.(0+n1) by A9,FINSEQ_3:112
                .=g.(i-'n2+n1) by A69,XREAL_1:232;
            end;
          end;
          i-'n2<len g-'n1 by A15,A62,XREAL_1:233;
          then i-'n2+1<=len g-'n1 by NAT_1:13;
          then
A70:      i-'n2+1<=len (g/^n1) by A15,A51,XREAL_1:233;
          1<=i-'n2+1 by NAT_1:12;
          then
A71:      i-'n2+1 in dom (g/^n1) by A70,FINSEQ_3:25;
          len (g|n2)+(i-'n2+1)=i-n2+1+n2 by A20,A61,XREAL_1:233
            .=i+1;
          then
A72:      z2=(g/^n1).(i-'n2+1) by A70,FINSEQ_1:65,NAT_1:12
            .=g.(i-'n2+1+n1) by A15,A71,RFINSEQ:def 1
            .=g.(i-'n2+n1+1);
          1<=i-'n2+n1 by A12,NAT_1:12;
          hence thesis by A2,A65,A72,A63;
        end;
      end;
A73:  rng (g|n2) c= rng g by FINSEQ_5:19;
A74:  g2=(g|n2)^({}) by A50,FINSEQ_6:167
        .= (g|n2) by FINSEQ_1:34;
      then g2.len g2=x2 by A6,A9,A20,A50,FINSEQ_3:112;
      then len g<=len g2 by A4,A5,A3,A21,A74,A73,A52,XBOOLE_1:1;
      then len g-n2<= n2+(len g-n1)-n2 by A22,XREAL_1:13;
      hence contradiction by A16,XREAL_1:10;
    end;
  end;
  suppose
A75: n2>n1;
    set k=len g-'n2;
    set g2=(g|n1)^(g/^n2);
A76: len (g/^n2)=len g-n2 by A13,RFINSEQ:def 1;
    len g-n2>=0 by A13,XREAL_1:48;
    then
A77: len g-'n2=len g-n2 by XREAL_0:def 2;
A78: len (g|n1)=n1 by A15,FINSEQ_1:59;
    then
A79: g2.1=(g|n1).1 by A12,FINSEQ_1:64
      .=x1 by A5,A12,FINSEQ_3:112;
A80: len g2=len (g|n1)+len (g/^n2) by FINSEQ_1:22
      .=n1+(len g-n2) by A13,A78,RFINSEQ:def 1;
    per cases by A13,XXREAL_0:1;
    suppose
      n2<len g;
      then n2+1<=len g by NAT_1:13;
      then
A81:  n2+1-n2<=len g-n2 by XREAL_1:13;
      then
A82:  0+1<=n1+(len g-n2) by XREAL_1:7;
A83:  g2 is continuous
      proof
        thus len g2 >= 1 by A80,A82;
        let i be Nat,z1 be Element of FT;
        assume that
A84:    1<=i and
A85:    i<len g2 and
A86:    z1=g2.i;
A87:    i+1 <=len g2 by A85,NAT_1:13;
        reconsider i as Element of NAT by ORDINAL1:def 12;
        1<i+1 by A84,NAT_1:13;
        then i+1 in dom g2 by A87,FINSEQ_3:25;
        then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
        then reconsider z2=g2.(i+1) as Element of FT;
        per cases;
        suppose
A88:      i<n1;
          then
A89:      i+1<=n1 by NAT_1:13;
          i+1<=len (g|n1) by A78,A88,NAT_1:13;
          then
A90:      z2=(g|n1).(i+1) by FINSEQ_1:64,NAT_1:12
            .=g.(i+1) by A89,FINSEQ_3:112;
A91:      i<len g by A15,A88,XXREAL_0:2;
          z1=(g|n1).i by A78,A84,A86,A88,FINSEQ_1:64
            .=g.i by A88,FINSEQ_3:112;
          hence thesis by A2,A84,A91,A90;
        end;
        suppose
A92:      i>=n1;
          i-n1<n1+(len g-n2)-n1 by A80,A85,XREAL_1:9;
          then
A93:      i-'n1<len g - n2 by A92,XREAL_1:233;
          then
A94:      i-'n1+n2<len g-n2+n2 by XREAL_1:6;
A95:      len (g|n1) +(i-'n1)=n1+(i-n1) by A78,A92,XREAL_1:233
            .=i;
A96:      now
            per cases by A92,XXREAL_0:1;
            suppose
              i>n1;
              then
A97:          i-n1>0 by XREAL_1:50;
              then i-'n1=i-n1 by XREAL_0:def 2;
              then
A98:          0+1<=i-'n1 by A97,NAT_1:13;
              then
A99:          i-'n1 in dom (g/^n2) by A76,A93,FINSEQ_3:25;
              thus z1=(g/^n2).(i-'n1) by A76,A86,A93,A95,A98,FINSEQ_1:65
                .=g.(i-'n1+n2) by A13,A99,RFINSEQ:def 1;
            end;
            suppose
A100:         i=n1;
              hence z1=(g|n1).n1 by A78,A84,A86,FINSEQ_1:64
                .=g.(0+n2) by A9,FINSEQ_3:112
                .=g.(i-'n1+n2) by A100,XREAL_1:232;
            end;
          end;
          i-'n1<len g-'n2 by A13,A93,XREAL_1:233;
          then i-'n1+1<=len g-'n2 by NAT_1:13;
          then
A101:     i-'n1+1<=len (g/^n2) by A13,A76,XREAL_1:233;
          1<=i-'n1+1 by NAT_1:12;
          then
A102:     i-'n1+1 in dom (g/^n2) by A101,FINSEQ_3:25;
          len (g|n1)+(i-'n1+1)=i-n1+1+n1 by A78,A92,XREAL_1:233
            .=i+1;
          then
A103:     z2=(g/^n2).(i-'n1+1) by A101,FINSEQ_1:65,NAT_1:12
            .=g.(i-'n1+1+n2) by A13,A102,RFINSEQ:def 1
            .=g.(i-'n1+n2+1);
          1<=i-'n1+n2 by A14,NAT_1:12;
          hence thesis by A2,A96,A103,A94;
        end;
      end;
A104: rng (g/^n2) c= rng g by FINSEQ_5:33;
      rng g2=rng (g|n1) \/ rng (g/^n2) & rng (g|n1) c= rng g by FINSEQ_1:31
,FINSEQ_5:19;
      then rng g2 c= rng g by A104,XBOOLE_1:8;
      then
A105: rng g2 c= A by A4;
A106: k+n2=len g by A77;
A107: k in dom ((g/^n2)) by A77,A76,A81,FINSEQ_3:25;
      then g2.(len (g|n1) + k) = (g/^n2).k by FINSEQ_1:def 7
        .= x2 by A6,A13,A107,A106,RFINSEQ:def 1;
      then g2.(len g2)=x2 by A15,A80,A77,FINSEQ_1:59;
      then len g<=len g2 by A1,A79,A105,A83;
      then len g-n1<= n1+(len g-n2)-n1 by A80,XREAL_1:13;
      hence contradiction by A75,XREAL_1:10;
    end;
    suppose
A108: n2=len g;
A109: len (g/^n2)=len g-n2 by A13,RFINSEQ:def 1;
A110: g2 is continuous
      proof
        thus len g2 >= 1 by A7,A11,A80,A108,FINSEQ_1:1;
        let i be Nat,z1 be Element of FT;
        assume that
A111:   1<=i and
A112:   i<len g2 and
A113:   z1=g2.i;
A114:   i+1 <=len g2 by A112,NAT_1:13;
        reconsider i as Element of NAT by ORDINAL1:def 12;
        1<i+1 by A111,NAT_1:13;
        then i+1 in dom g2 by A114,FINSEQ_3:25;
        then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
        then reconsider z2=g2.(i+1) as Element of FT;
        per cases;
        suppose
A115:     i<n1;
          then
A116:     i+1<=n1 by NAT_1:13;
          i+1<=len (g|n1) by A78,A115,NAT_1:13;
          then
A117:     z2=(g|n1).(i+1) by FINSEQ_1:64,NAT_1:12
            .=g.(i+1) by A116,FINSEQ_3:112;
A118:     i<len g by A15,A115,XXREAL_0:2;
          z1=(g|n1).i by A78,A111,A113,A115,FINSEQ_1:64
            .=g.i by A115,FINSEQ_3:112;
          hence thesis by A2,A111,A118,A117;
        end;
        suppose
A119:     i>=n1;
          i-n1<n1+(len g-n2)-n1 by A80,A112,XREAL_1:9;
          then
A120:     i-'n1<len g - n2 by A119,XREAL_1:233;
          then
A121:     i-'n1+n2<len g-n2+n2 by XREAL_1:6;
A122:     len (g|n1) +(i-'n1)=n1+(i-n1) by A78,A119,XREAL_1:233
            .=i;
A123:     now
            per cases by A119,XXREAL_0:1;
            suppose
              i>n1;
              then
A124:         i-n1>0 by XREAL_1:50;
              then i-'n1=i-n1 by XREAL_0:def 2;
              then
A125:         0+1<=i-'n1 by A124,NAT_1:13;
              then
A126:         i-'n1 in dom (g/^n2) by A109,A120,FINSEQ_3:25;
              thus z1=(g/^n2).(i-'n1) by A109,A113,A120,A122,A125,FINSEQ_1:65
                .=g.(i-'n1+n2) by A13,A126,RFINSEQ:def 1;
            end;
            suppose
A127:         i=n1;
              hence z1=(g|n1).n1 by A78,A111,A113,FINSEQ_1:64
                .=g.(0+n2) by A9,FINSEQ_3:112
                .=g.(i-'n1+n2) by A127,XREAL_1:232;
            end;
          end;
          i-'n1<len g-'n2 by A13,A120,XREAL_1:233;
          then i-'n1+1<=len g-'n2 by NAT_1:13;
          then
A128:     i-'n1+1<=len (g/^n2) by A13,A109,XREAL_1:233;
          1<=i-'n1+1 by NAT_1:12;
          then
A129:     i-'n1+1 in dom (g/^n2) by A128,FINSEQ_3:25;
          len (g|n1)+(i-'n1+1)=i-n1+1+n1 by A78,A119,XREAL_1:233
            .=i+1;
          then
A130:     z2=(g/^n2).(i-'n1+1) by A128,FINSEQ_1:65,NAT_1:12
            .=g.(i-'n1+1+n2) by A13,A129,RFINSEQ:def 1
            .=g.(i-'n1+n2+1);
          1<=i-'n1+n2 by A14,NAT_1:12;
          hence thesis by A2,A123,A130,A121;
        end;
      end;
A131: g2=(g|n1)^({}) by A108,FINSEQ_6:167
        .= (g|n1) by FINSEQ_1:34;
      rng (g|n1) c= rng g by FINSEQ_5:19;
      then
A132: rng g2 c= A by A4,A131;
      g2.(len g2)=x2 by A6,A9,A78,A108,A131,FINSEQ_3:112;
      then len g<=len g2 by A1,A79,A132,A110;
      then len g-n1<= n1+(len g-n2)-n1 by A80,XREAL_1:13;
      hence contradiction by A75,XREAL_1:10;
    end;
  end;
end;

definition
  let FT;
  let f be FinSequence of FT;
  attr f is inv_continuous means

  1<=len f & for i,j being Nat,y being
  Element of FT st 1<=i & i<=len f & 1<=j & j<= len f & y=f.i & i<>j & f.j in
  U_FT y holds i=j+1 or j=i+1;
end;

theorem Th55:
  for g being FinSequence of FT,A being Subset of FT, x1,x2 being
  Element of FT st g is_minimum_path_in A,x1,x2 & FT is symmetric holds g is
  inv_continuous
proof
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
  assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is symmetric;
A3: g.1=x1 by A1;
A4: g.(len g)=x2 by A1;
A5: g is continuous by A1;
  hence 1<=len g;
  let i2,j2 be Nat,y be Element of FT;
  assume that
A6: 1<=i2 and
A7: i2<=len g and
A8: 1<=j2 and
A9: j2<= len g and
A10: y=g.i2 and
A11: i2<>j2 and
A12: g.j2 in U_FT y;
A13: rng g c=A by A1;
  hereby
    assume that
A14: i2<>j2+1 and
A15: j2<>i2+1;
    per cases by A11,XXREAL_0:1;
    suppose
A16:  i2<j2;
      set n1=j2-'1,n2=i2;
      reconsider n1,n2 as Element of NAT by ORDINAL1:def 12;
      i2+1<=j2 by A16,NAT_1:13;
      then i2+1<j2 by A15,XXREAL_0:1;
      then i2 <j2-1 by XREAL_1:20;
      then
A17:  n1>n2 by A8,XREAL_1:233;
      1<j2 by A6,A16,XXREAL_0:2;
      then 1+1<=j2 by NAT_1:13;
      then 1<=j2-1 by XREAL_1:19;
      then
A18:  1<=n1 by A8,XREAL_1:233;
      set k=len g-'n1;
      reconsider g2=(g|n2)^(g/^n1) as FinSequence of FT;
A19:  len (g|n2)=n2 by A7,FINSEQ_1:59;
A20:  j2-'1<=j2 by NAT_D:35;
      then
A21:  n1 <=len g by A9,XXREAL_0:2;
      then
A22:  len (g/^n1)=len g-n1 by RFINSEQ:def 1;
A23:  len g-n1>=0 by A21,XREAL_1:48;
      then
A24:  len g-'n1=len g-n1 by XREAL_0:def 2;
A25:  len g2=len (g|n2)+len (g/^n1) by FINSEQ_1:22
        .=n2+(len g-n1) by A21,A19,RFINSEQ:def 1;
A26:  g2.1=(g|n2).1 by A6,A19,FINSEQ_1:64
        .=x1 by A3,A6,FINSEQ_3:112;
      now
        per cases by A21,XXREAL_0:1;
        suppose
          n1<len g;
          then n1+1<=len g by NAT_1:13;
          then
A27:      n1+1-n1<=len g-n1 by XREAL_1:13;
          then
A28:      0+1<=n2+(len g-n1) by XREAL_1:7;
A29:      g2 is continuous
          proof
            thus len g2 >= 1 by A25,A28;
            let i be Nat,z1 be Element of FT;
            assume that
A30:        1<=i and
A31:        i<len g2 and
A32:        z1=g2.i;
A33:        i+1 <=len g2 by A31,NAT_1:13;
            reconsider i as Element of NAT by ORDINAL1:def 12;
            1<i+1 by A30,NAT_1:13;
            then i+1 in dom g2 by A33,FINSEQ_3:25;
            then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
            then reconsider z2=g2.(i+1) as Element of FT;
            per cases;
            suppose
A34:          i<n2;
              then
A35:          i+1<=n2 by NAT_1:13;
              i+1<=len (g|n2) by A19,A34,NAT_1:13;
              then
A36:          z2=(g|n2).(i+1) by FINSEQ_1:64,NAT_1:12
                .=g.(i+1) by A35,FINSEQ_3:112;
A37:          i<len g by A7,A34,XXREAL_0:2;
              z1=(g|n2).i by A19,A30,A32,A34,FINSEQ_1:64
                .=g.i by A34,FINSEQ_3:112;
              hence thesis by A5,A30,A37,A36;
            end;
            suppose
A38:          i>=n2;
              i-n2<n2+(len g-n1)-n2 by A25,A31,XREAL_1:9;
              then
A39:          i-'n2<len g - n1 by A38,XREAL_1:233;
              then i-'n2<len g-'n1 by A9,A20,XREAL_1:233,XXREAL_0:2;
              then i-'n2+1<=len g-'n1 by NAT_1:13;
              then
A40:          i-'n2+1<=len (g/^n1) by A9,A20,A22,XREAL_1:233,XXREAL_0:2;
A41:          len (g|n2) +(i-'n2)=n2+(i-n2) by A19,A38,XREAL_1:233
                .=i;
A42:          len (g|n2)+(i-'n2+1)=i-n2+1+n2 by A19,A38,XREAL_1:233
                .=i+1;
              1<=i-'n2+1 by NAT_1:12;
              then
A43:          i-'n2+1 in dom (g/^n1) by A40,FINSEQ_3:25;
              per cases by A38,XXREAL_0:1;
              suppose
                i>n2;
                then
A44:            i-n2>0 by XREAL_1:50;
                then i-'n2=i-n2 by XREAL_0:def 2;
                then
A45:            0+1<=i-'n2 by A44,NAT_1:13;
                then
A46:            i-'n2 in dom (g/^n1) by A22,A39,FINSEQ_3:25;
A47:            z2=(g/^n1).(i-'n2+1) by A40,A42,FINSEQ_1:65,NAT_1:12
                  .=g.(i-'n2+1+n1) by A21,A43,RFINSEQ:def 1
                  .=g.(i-'n2+n1+1);
A48:            1<=i-'n2+n1 & i-'n2+n1<len g-n1+n1 by A18,A39,NAT_1:12
,XREAL_1:6;
                z1=(g/^n1).(i-'n2) by A22,A32,A39,A41,A45,FINSEQ_1:65
                  .=g.(i-'n2+n1) by A21,A46,RFINSEQ:def 1;
                hence thesis by A5,A47,A48;
              end;
              suppose
A49:            i=n2;
                then
A50:            z1=(g|n2).n2 by A19,A30,A32,FINSEQ_1:64
                  .=y by A10,FINSEQ_3:112;
                z2=(g/^n1).(i-'n2+1) by A40,A42,FINSEQ_1:65,NAT_1:12
                  .=g.(i-'n2+1+n1) by A21,A43,RFINSEQ:def 1
                  .=g.(i-'n2+n1+1)
                  .=g.(0+(j2-'1)+1) by A49,XREAL_1:232
                  .=g.(j2-1+1) by A8,XREAL_1:233;
                hence thesis by A12,A50;
              end;
            end;
          end;
A51:      rng (g/^n1) c= rng g by FINSEQ_5:33;
          rng g2=rng (g|n2) \/ rng (g/^n1) & rng (g|n2) c= rng g by FINSEQ_1:31
,FINSEQ_5:19;
          then rng g2 c= rng g by A51,XBOOLE_1:8;
          then
A52:      rng g2 c= A by A13;
A53:      k+n1=len g by A24;
A54:      k in dom (g/^n1) by A24,A22,A27,FINSEQ_3:25;
          then g2.(len (g|n2) + k) = (g/^n1).k by FINSEQ_1:def 7
            .= x2 by A4,A21,A54,A53,RFINSEQ:def 1;
          then g2.(len g2)=x2 by A19,A25,A23,XREAL_0:def 2;
          then len g<=len g2 by A1,A26,A52,A29;
          then len g-n2<= n2+(len g-n1)-n2 by A25,XREAL_1:13;
          hence contradiction by A17,XREAL_1:10;
        end;
        suppose
          n1=len g;
          then j2-1=len g by A8,XREAL_1:233;
          then j2=len g+1;
          hence contradiction by A9,NAT_1:13;
        end;
      end;
      hence contradiction;
    end;
    suppose
A55:  j2<i2;
      reconsider n1=i2-'1,n2=j2 as Element of NAT by ORDINAL1:def 12;
      j2+1<=i2 by A55,NAT_1:13;
      then j2+1<i2 by A14,XXREAL_0:1;
      then j2 <i2-1 by XREAL_1:20;
      then
A56:  n1>n2 by A6,XREAL_1:233;
      1<i2 by A8,A55,XXREAL_0:2;
      then 1+1<=i2 by NAT_1:13;
      then 1<=i2-1 by XREAL_1:19;
      then
A57:  1<=n1 by A6,XREAL_1:233;
      set k=len g-'n1;
      reconsider g2=(g|n2)^(g/^n1) as FinSequence of FT;
A58:  len (g|n2)=n2 by A9,FINSEQ_1:59;
A59:  i2-'1<=i2 by NAT_D:35;
      then
A60:  n1 <=len g by A7,XXREAL_0:2;
      then
A61:  len (g/^n1)=len g-n1 by RFINSEQ:def 1;
A62:  len g-n1>=0 by A60,XREAL_1:48;
      then
A63:  len g-'n1=len g-n1 by XREAL_0:def 2;
A64:  len g2=len (g|n2)+len (g/^n1) by FINSEQ_1:22
        .=n2+(len g-n1) by A60,A58,RFINSEQ:def 1;
A65:  g2.1=(g|n2).1 by A8,A58,FINSEQ_1:64
        .=x1 by A3,A8,FINSEQ_3:112;
      now
        per cases by A60,XXREAL_0:1;
        suppose
          n1<len g;
          then n1+1<=len g by NAT_1:13;
          then
A66:      n1+1-n1<=len g-n1 by XREAL_1:13;
          then
A67:      0+1<=n2+(len g-n1) by XREAL_1:7;
A68:      g2 is continuous
          proof
            thus len g2 >= 1 by A64,A67;
            let i be Nat,z1 be Element of FT;
            assume that
A69:        1<=i and
A70:        i<len g2 and
A71:        z1=g2.i;
A72:        i+1 <=len g2 by A70,NAT_1:13;
            reconsider i as Element of NAT by ORDINAL1:def 12;
            1<i+1 by A69,NAT_1:13;
            then i+1 in dom g2 by A72,FINSEQ_3:25;
            then g2.(i+1)=g2/.(i+1) by PARTFUN1:def 6;
            then reconsider z2=g2.(i+1) as Element of FT;
            per cases;
            suppose
A73:          i<n2;
              then
A74:          i+1<=n2 by NAT_1:13;
              i+1<=len (g|n2) by A58,A73,NAT_1:13;
              then
A75:          z2=(g|n2).(i+1) by FINSEQ_1:64,NAT_1:12
                .=g.(i+1) by A74,FINSEQ_3:112;
A76:          i<len g by A9,A73,XXREAL_0:2;
              z1=(g|n2).i by A58,A69,A71,A73,FINSEQ_1:64
                .=g.i by A73,FINSEQ_3:112;
              hence thesis by A5,A69,A76,A75;
            end;
            suppose
A77:          i>=n2;
              i-n2<n2+(len g-n1)-n2 by A64,A70,XREAL_1:9;
              then
A78:          i-'n2<len g - n1 by A77,XREAL_1:233;
              then i-'n2<len g-'n1 by A7,A59,XREAL_1:233,XXREAL_0:2;
              then i-'n2+1<=len g-'n1 by NAT_1:13;
              then
A79:          i-'n2+1<=len (g/^n1) by A7,A59,A61,XREAL_1:233,XXREAL_0:2;
A80:          len (g|n2) +(i-'n2)=n2+(i-n2) by A58,A77,XREAL_1:233
                .=i;
A81:          len (g|n2)+(i-'n2+1)=i-n2+1+n2 by A58,A77,XREAL_1:233
                .=i+1;
              1<=i-'n2+1 by NAT_1:12;
              then
A82:          i-'n2+1 in dom (g/^n1) by A79,FINSEQ_3:25;
              per cases by A77,XXREAL_0:1;
              suppose
                i>n2;
                then
A83:            i-n2>0 by XREAL_1:50;
                then i-'n2=i-n2 by XREAL_0:def 2;
                then
A84:            0+1<=i-'n2 by A83,NAT_1:13;
                then
A85:            i-'n2 in dom (g/^n1) by A61,A78,FINSEQ_3:25;
A86:            z2=(g/^n1).(i-'n2+1) by A79,A81,FINSEQ_1:65,NAT_1:12
                  .=g.(i-'n2+1+n1) by A60,A82,RFINSEQ:def 1
                  .=g.(i-'n2+n1+1);
A87:            1<=i-'n2+n1 & i-'n2+n1<len g-n1+n1 by A57,A78,NAT_1:12
,XREAL_1:6;
                z1=(g/^n1).(i-'n2) by A61,A71,A78,A80,A84,FINSEQ_1:65
                  .=g.(i-'n2+n1) by A60,A85,RFINSEQ:def 1;
                hence thesis by A5,A86,A87;
              end;
              suppose
A88:            i=n2;
                then
A89:            z1=(g|n2).n2 by A58,A69,A71,FINSEQ_1:64
                  .=g.j2 by FINSEQ_3:112;
                z2=(g/^n1).(i-'n2+1) by A79,A81,FINSEQ_1:65,NAT_1:12
                  .=g.(i-'n2+1+n1) by A60,A82,RFINSEQ:def 1
                  .=g.(i-'n2+n1+1)
                  .=g.(0+(i2-'1)+1) by A88,XREAL_1:232
                  .=g.(i2-1+1) by A6,XREAL_1:233
                  .=y by A10;
                hence thesis by A2,A12,A89;
              end;
            end;
          end;
A90:      rng (g/^n1) c= rng g by FINSEQ_5:33;
          rng g2=rng (g|n2) \/ rng (g/^n1) & rng (g|n2) c= rng g by FINSEQ_1:31
,FINSEQ_5:19;
          then rng g2 c= rng g by A90,XBOOLE_1:8;
          then
A91:      rng g2 c= A by A13;
A92:      k+n1=len g by A63;
A93:      k in dom (g/^n1) by A63,A61,A66,FINSEQ_3:25;
          then g2.(len (g|n2) + k) = (g/^n1).k by FINSEQ_1:def 7
            .= x2 by A4,A60,A93,A92,RFINSEQ:def 1;
          then g2.(len g2)=x2 by A58,A64,A62,XREAL_0:def 2;
          then len g<=len g2 by A1,A65,A91,A68;
          then len g-n2<= n2+(len g-n1)-n2 by A64,XREAL_1:13;
          hence contradiction by A56,XREAL_1:10;
        end;
        suppose
          n1=len g;
          then i2-1=len g by A6,XREAL_1:233;
          then i2=len g+1;
          hence contradiction by A7,NAT_1:13;
        end;
      end;
      hence contradiction;
    end;
  end;
end;

theorem
  for g being FinSequence of FT,A being Subset of FT, x1,x2 being
Element of FT st g is_minimum_path_in A,x1,x2 & FT is filled symmetric & x1<>x2
holds (for i being Nat st 1<i & i<len g holds (rng g)/\ U_FT (g/.i)={g.(i-'1),g
.i,g.(i+1)}) & (rng g)/\ U_FT (g/.1)={g.1,g.2} & (rng g)/\ U_FT (g/.len g)={g.(
  len g -'1),g.len g}
proof
  let g be FinSequence of FT,A be Subset of FT, x1,x2 be Element of FT;
  assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is filled symmetric and
A3: x1<>x2;
A4: dom g=Seg len g by FINSEQ_1:def 3;
A5: g is continuous by A1;
  then
A6: 1<=len g;
  then
A7: len g in dom g by A4;
  then
A8: g.len g=g/.len g by PARTFUN1:def 6;
A9: g is inv_continuous by A1,A2,Th55;
  then
A10: 1<=len g;
  thus for i being Nat st 1<i & i<len g holds (rng g) /\ U_FT (g/.i)={g.(i-'1)
  ,g.i,g.(i+1)}
  proof
    let i be Nat;
    assume that
A11: 1<i and
A12: i<len g;
A13: i in Seg len g by A11,A12;
    1<i+1 & i+1<=len g by A11,A12,NAT_1:13;
    then
A14: i+1 in Seg len g;
    i-'1<=i by NAT_D:35;
    then
A15: i-'1< len g by A12,XXREAL_0:2;
    1+1<=i by A11,NAT_1:13;
    then
A16: 1<= i-1 by XREAL_1:19;
    then 1<=i-'1 by A11,XREAL_1:233;
    then
A17: i-'1 in Seg len g by A15;
A18: i-'1+1=i-1+1 by A11,XREAL_1:233
      .=i;
    thus (rng g) /\ U_FT (g/.i)={g.(i-'1),g.i,g.(i+1)}
    proof
      thus (rng g) /\ U_FT (g/.i) c={g.(i-'1),g.i,g.(i+1)}
      proof
        let x be object;
        assume
A19:    x in (rng g) /\ U_FT (g/.i);
        then
A20:    x in U_FT (g/.i) by XBOOLE_0:def 4;
        x in rng g by A19,XBOOLE_0:def 4;
        then consider nx being object such that
A21:    nx in dom g and
A22:    x=g.nx by FUNCT_1:def 3;
        reconsider j=nx as Element of NAT by A21;
        i=j+1 implies i-1=j;
        then
A23:    i=j+1 implies i-'1=j by A11,XREAL_1:233;
A24:    g/.i=g.i by A4,A13,PARTFUN1:def 6;
        1<=j & j<=len g by A4,A21,FINSEQ_1:1;
        then j=i or i=j+1 or j=i+1 by A9,A11,A12,A20,A22,A24;
        hence thesis by A22,A23,ENUMSET1:def 1;
      end;
      let x be object;
A25:  g.i=g/.i by A4,A13,PARTFUN1:def 6;
A26:  g.(i-'1)=g/.(i-'1) by A4,A17,PARTFUN1:def 6;
      assume
A27:  x in {g.(i-'1),g.i,g.(i+1)};
      per cases by A27,ENUMSET1:def 1;
      suppose
A28:    x=g.(i-'1);
        g.i in U_FT (g/.(i-'1)) by A5,A16,A15,A18,A26;
        then
A29:    x in U_FT (g/.i) by A2,A25,A26,A28;
        x in rng g by A4,A17,A28,FUNCT_1:def 3;
        hence thesis by A29,XBOOLE_0:def 4;
      end;
      suppose
        x=g.i;
        then x in rng g & x in U_FT (g/.i) by A2,A4,A13,A25,FUNCT_1:def 3;
        hence thesis by XBOOLE_0:def 4;
      end;
      suppose
        x=g.(i+1);
        then x in rng g & x in U_FT (g/.i) by A5,A4,A11,A12,A14,A25,
FUNCT_1:def 3;
        hence thesis by XBOOLE_0:def 4;
      end;
    end;
  end;
  g.1=x1 & g.(len g)=x2 by A1;
  then
A30: 1< len g by A3,A6,XXREAL_0:1;
  then
A31: 1+1<=len g by NAT_1:13;
  then
A32: 1+1-1<=len g-1 by XREAL_1:13;
A33: 1 in dom g by A10,FINSEQ_3:25;
  then
A34: g.1=g/.1 by PARTFUN1:def 6;
  thus (rng g) /\ U_FT (g/.1)={g.1,g.2}
  proof
    thus (rng g) /\ U_FT (g/.1) c= {g.1,g.2}
    proof
      let x be object;
      assume
A35:  x in (rng g) /\ U_FT (g/.1);
      then
A36:  x in U_FT (g/.1) by XBOOLE_0:def 4;
      x in (rng g) by A35,XBOOLE_0:def 4;
      then consider y being object such that
A37:  y in dom g and
A38:  x=g.y by FUNCT_1:def 3;
      reconsider j=y as Element of NAT by A37;
A39:  1<=j by A4,A37,FINSEQ_1:1;
      j<=len g by A4,A37,FINSEQ_1:1;
      then 1+1=j or 1=j or j+1=1 by A9,A34,A36,A38,A39;
      then 1+1=j or 1=j by A39,XREAL_1:7;
      hence thesis by A38,TARSKI:def 2;
    end;
    let x be object;
    2 in dom g by A31,A4;
    then
A40: x=g.2 implies x in rng g by FUNCT_1:def 3;
    assume
A41: x in {g.1,g.2};
A42: now
      per cases by A41,TARSKI:def 2;
      case
        x=g.1;
        hence x in U_FT (g/.1) by A2,A34;
      end;
      case
A43:    x=g.2;
        then reconsider xx=x as Element of FT by A40;
        xx=g.(1+1) by A43;
        hence x in U_FT (g/.1) by A5,A30,A34;
      end;
    end;
    x=g.1 implies x in rng g by A33,FUNCT_1:def 3;
    hence thesis by A40,A42,XBOOLE_0:def 4;
  end;
  len g<len g+1 by NAT_1:13;
  then
A44: len g-1<len g+1-1 by XREAL_1:14;
  then
A45: len g-'1<len g by A10,XREAL_1:233;
A46: len g-'1=len g -1 by A10,XREAL_1:233;
  then
A47: len g-'1 in dom g by A32,A44,FINSEQ_3:25;
  then
A48: g.(len g-'1)=g/.(len g-'1) by PARTFUN1:def 6;
A49: 1<=len g-'1 by A10,A32,XREAL_1:233;
  thus (rng g) /\ U_FT (g/.len g)={g.(len g -'1),g.len g}
  proof
    thus (rng g) /\ U_FT (g/.len g) c= {g.(len g -'1),g.len g}
    proof
      let x be object;
      assume
A50:  x in (rng g) /\ U_FT (g/.len g);
      then
A51:  x in U_FT (g/.len g) by XBOOLE_0:def 4;
      x in rng g by A50,XBOOLE_0:def 4;
      then consider y being object such that
A52:  y in dom g and
A53:  x=g.y by FUNCT_1:def 3;
      reconsider ny=y as Element of NAT by A52;
A54:  ny<=len g by A4,A52,FINSEQ_1:1;
      1<=ny by A4,A52,FINSEQ_1:1;
      then ny+1=len g or len g +1=ny or len g=ny by A9,A8,A51,A53,A54;
      then ny=len g-1 or len g=ny by A54,NAT_1:13;
      then x=g.(len g -'1) or x=g.len g by A6,A53,XREAL_1:233;
      hence thesis by TARSKI:def 2;
    end;
    let x be object;
A55: g.len g in U_FT (g/.len g) by A2,A8;
    g.(len g-'1+1) in U_FT (g/.(len g-'1)) by A5,A49,A45,A48;
    then
A56: g.(len g-'1) in U_FT (g/.len g) by A2,A8,A46,A48;
    assume x in {g.(len g -'1),g.len g};
    then
A57: x=g.(len g -'1) or x=g.len g by TARSKI:def 2;
    then x in rng g by A7,A47,FUNCT_1:def 3;
    hence thesis by A57,A55,A56,XBOOLE_0:def 4;
  end;
end;

theorem
  for g being FinSequence of FT,A being non empty Subset of FT, x1,x2
  being Element of FT,B0 being Subset of FT|A st g is_minimum_path_in A,x1,x2 &
  FT is filled symmetric & B0={x1} holds for i being Element of NAT st i< len g
  holds g.(i+1) in Finf(B0,i) & (i>=1 implies not g.(i+1) in Finf(B0,i-'1))
proof
  let g be FinSequence of FT,A be non empty Subset of FT, x1,x2 be Element of
  FT, B0 be Subset of FT|A;
  assume that
A1: g is_minimum_path_in A,x1,x2 and
A2: FT is filled symmetric and
A3: B0={x1};
A4: rng g c=A by A1;
  defpred P[Nat] means $1+1 <=len g implies g.($1+1) in Finf(B0,$1) & ($1>=1
  implies not g.($1+1) in Finf(B0,$1-'1));
  defpred Q[Nat] means for y being Element of FT st y in Finf(B0,$1
) holds ex h being FinSequence of FT st h is continuous & rng h c= A & h.1=x1 &
  h.len h=y & len h <= $1+1;
A5: [#](FT|A)=A by Def3;
A6: for k being Nat st Q[k] holds Q[k+1]
  proof
    let k be Nat;
    assume
A7: Q[k];
    for y being Element of FT st y in Finf(B0,k+1) holds ex h being
FinSequence of FT st h is continuous & rng h c= A & h.1=x1 & h.len h=y & len h
    <= k+1+1
    proof
      let y be Element of FT;
A8:   Finf(B0,k+1)=(Finf(B0,k))^f by FINTOPO3:31;
      assume y in Finf(B0,k+1);
      then consider x being Element of FT|A such that
A9:   x=y and
A10:  ex y2 being Element of FT|A st y2 in Finf(B0,k) & x in U_FT y2 by A8;
A11:  [#](FT|A)=A by Def3;
      then
A12:  {y} c= A by A9,ZFMISC_1:31;
      consider y2 being Element of FT|A such that
A13:  y2 in Finf(B0,k) and
A14:  x in U_FT y2 by A10;
      y2 in the carrier of (FT|A);
      then reconsider y3=y2 as Element of FT by A11;
      consider h2 being FinSequence of FT such that
A15:  h2 is continuous and
A16:  rng h2 c= A and
A17:  h2.1=x1 and
A18:  h2.len h2=y3 and
A19:  len h2 <= k+1 by A7,A13;
      U_FT y2=(U_FT y3)/\ A by A11,Def2;
      then
A20:  y in U_FT y3 by A9,A14,XBOOLE_0:def 4;
      reconsider h3=h2^(<*y*>) as FinSequence of FT;
      rng(h2^(<*y*>)) = rng h2 \/ rng (<*y*>) & rng (<*y*>)={y} by FINSEQ_1:31
,39;
      then
A21:  rng h3 c= A by A16,A12,XBOOLE_1:8;
      1<= len h2 by A15;
      then 1 in dom h2 by FINSEQ_3:25;
      then
A22:  h3.1=x1 by A17,FINSEQ_1:def 7;
      len (<*y*>)=1 by FINSEQ_1:40;
      then
A23:  len h3=len h2 +1 by FINSEQ_1:22;
      then
A24:  h3.len h3=y by FINSEQ_1:42;
      len h3<=k+1+1 by A19,A23,XREAL_1:6;
      hence thesis by A15,A18,A20,A21,A22,A24,Th43;
    end;
    hence thesis;
  end;
A25: g.1=x1 by A1;
  then
A26: g.1 in {x1} by TARSKI:def 1;
A27: g.(len g)=x2 by A1;
A28: g is continuous by A1;
  then 1<=len g;
  then 1 in dom g by FINSEQ_3:25;
  then x1 in rng g by A25,FUNCT_1:def 3;
  then
A29: {x1} c= A by A4,ZFMISC_1:31;
  for y being Element of FT st y in Finf(B0,0) holds ex h being
FinSequence of FT st h is continuous & rng h c= A & h.1=x1 & h.len h=y & len h
  <= 0+1
  proof
    let y be Element of FT;
A30: len (<*x1*>)=1 by FINSEQ_1:40;
    assume y in Finf(B0,0);
    then y in {x1} by A3,FINTOPO3:32;
    then
A31: y=x1 by TARSKI:def 1;
    rng (<*x1*>)={x1} & (<*x1*>).1=x1 by FINSEQ_1:39;
    hence thesis by A29,A31,A30;
  end;
  then
A32: Q[0];
A33: for k being Nat holds Q[k] from NAT_1:sch 2(A32,A6);
A34: for k being Nat st P[k] holds P[k+1]
  proof
    let k be Nat;
    assume
A35: P[k];
    per cases;
    suppose
      k+1+1>len g;
      hence thesis;
    end;
    suppose
A36:  k+1+1<=len g;
A37:  1<=k+1 by NAT_1:12;
      then 1<k+1+1 by NAT_1:13;
      then k+1+1 in dom g by A36,FINSEQ_3:25;
      then
A38:  g.(k+1+1) in rng g by FUNCT_1:def 3;
      reconsider y0=g.(k+1) as Element of FT|A by A35,A36,NAT_1:13;
A39:  k+1<len g by A36,NAT_1:13;
      then k+1 in dom g by A37,FINSEQ_3:25;
      then
A40:  g.(k+1)=g/.(k+1) by PARTFUN1:def 6;
      1<k+1+1 by A37,NAT_1:13;
      then
A41:  k+1+1 in dom g by A36,FINSEQ_3:25;
A42:  now
        assume
A43:    g.(k+1+1) in Finf(B0,k);
        now
          per cases;
          suppose
A44:        k=0;
            then k-1<0;
            then k-'1=0 by XREAL_0:def 2;
            then Finf(B0,k) c= (Finf(B0,k-'1))^f by A2,A44,FINTOPO3:1;
            hence g.(k+1+1) in Finf(B0,k-'1)^f by A43;
          end;
          suppose
            k>0;
            then k>=0+1 by NAT_1:13;
            then k=k-'1+1 by XREAL_1:235;
            hence g.(k+1+1) in Finf(B0,k-'1)^f by A43,FINTOPO3:31;
          end;
        end;
        then consider x being Element of FT|A such that
A45:    g.(k+1+1)=x and
        ex y being Element of FT|A st y in Finf(B0,k-'1) & x in U_FT y;
        x in A by A5;
        then reconsider x3=x as Element of FT;
        consider h being FinSequence of FT such that
A46:    h is continuous and
A47:    rng h c= A and
A48:    h.1=x1 and
A49:    h.len h=x3 and
A50:    len h <= k+1 by A33,A43,A45;
        reconsider s=h^(g/^(k+1+1)) as FinSequence of FT;
A51:    len s=len h +len(g/^(k+1+1)) by FINSEQ_1:22;
        g=(g|(k+1+1))^(g/^(k+1+1)) by RFINSEQ:8;
        then
A52:    len g=len (g|(k+1+1)) + len (g/^(k+1+1)) by FINSEQ_1:22;
A53:    1<=len h by A46;
        then len h in dom h by FINSEQ_3:25;
        then
A54:    h.(len h)=h/.(len h) by PARTFUN1:def 6;
        len (g|(k+1+1))=k+1+1 by A36,FINSEQ_1:59;
        then
A55:    len (g|(k+1+1))>len h by A50,NAT_1:13;
        then
A56:    len s<len g by A51,A52,XREAL_1:8;
        per cases;
        suppose
A57:      k+1+1<len g;
          then len g>=1+(k+1+1) by NAT_1:13;
          then 1<=len g -(k+1+1) by XREAL_1:19;
          then 1<=len (g/^(k+1+1)) by A57,RFINSEQ:def 1;
          then
A58:      1 in dom (g/^(k+1+1)) by FINSEQ_3:25;
A59:      g.(k+1+1)=g/.(k+1+1) by A41,PARTFUN1:def 6;
A60:      g/^(k+1+1) is continuous by A28,A57,Th47;
          then 1<= len (g/^(k+1+1));
          then len (g/^(k+1+1)) in dom (g/^(k+1+1)) by FINSEQ_3:25;
          then
A61:      s.(len s)=(g/^(k+1+1)).(len (g/^(k+1+1))) by A51,FINSEQ_1:def 7
            .=x2 by A27,A57,FINSEQ_6:185;
          1<=k+1+1 by NAT_1:12;
          then g.(k+1+1+1) in U_FT (g/.(k+1+1)) by A28,A57,A59;
          then (g/^(k+1+1)).1 in U_FT (h/.(len h)) by A45,A49,A54,A57,A59,A58,
RFINSEQ:def 1;
          then
A62:      s is continuous by A46,A60,Th44;
          1 in dom h by A53,FINSEQ_3:25;
          then
A63:      s.1=x1 by A48,FINSEQ_1:def 7;
          rng (g/^(k+1+1)) c= rng g by FINSEQ_5:33;
          then
A64:      rng (g/^(k+1+1)) c= A by A4;
          rng s = rng h \/ rng (g/^(k+1+1)) by FINSEQ_1:31;
          then rng s c= A by A47,A64,XBOOLE_1:8;
          hence contradiction by A1,A56,A62,A63,A61;
        end;
        suppose
A65:      k+1+1>=len g;
          then g/^(k+1+1)=<*>the carrier of FT by FINSEQ_5:32;
          then
A66:      s=h by FINSEQ_1:34;
          k+1+1=len g by A36,A65,XXREAL_0:1;
          hence contradiction by A1,A45,A46,A47,A48,A49,A55,A51,A52,A66;
        end;
      end;
      [#](FT|A)=A by Def3;
      then
A67:  U_FT y0 = U_FT(g/.(k+1))/\ A by A40,Def2;
      g.(k+1+1) in U_FT (g/.(k+1)) by A28,A39,A37,A40;
      then g.(k+1+1) in U_FT y0 by A4,A67,A38,XBOOLE_0:def 4;
      then
A68:  g.(k+1+1) in (Finf(B0,k))^f by A35,A36,NAT_1:13;
      k+1-'1=k+1-1 by NAT_D:37
        .=k;
      hence thesis by A68,A42,FINTOPO3:31;
    end;
  end;
  let i be Element of NAT;
  assume i < len g;
  then
A69: i+1<=len g by NAT_1:13;
  Finf({x1},0)={x1} by FINTOPO3:32
    .=Finf(B0,0) by A3,FINTOPO3:32;
  then
A70: P[0] by A26,FINTOPO3:32;
  for j being Nat holds P[j] from NAT_1:sch 2(A70,A34);
  hence thesis by A69;
end;