The Mizar article:

Graph Theoretical Properties of Arcs in the Plane and Fashoda Meet Theorem

by
Yatsuka Nakamura

Received August 21, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: JGRAPH_1
[ MML identifier index ]


environ

 vocabulary GRAPH_1, FINSEQ_1, ORDERS_1, SQUARE_1, ABSVALUE, ARYTM_1, GRAPH_4,
      FUNCT_1, FINSEQ_4, BOOLE, FUNCT_3, RELAT_1, FINSET_1, CARD_1, EUCLID,
      TOPREAL1, GOBOARD5, PRE_TOPC, TARSKI, MCART_1, GOBOARD1, GOBOARD4,
      COMPLEX1, METRIC_1, RLVECT_1, RVSUM_1, PCOMPS_1, COMPTS_1, WEIERSTR,
      NAT_1, ARYTM_3, BORSUK_1, TOPS_2, ORDINAL2, RCOMP_1, TBSP_1, SUBSET_1,
      PSCOMP_1, LATTICES, JGRAPH_1, ARYTM;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0,
      REAL_1, RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSET_1, CARD_1,
      NAT_1, GRAPH_1, STRUCT_0, BINARITH, GRAPH_2, FINSEQ_4, GRAPH_4, TOPREAL1,
      GOBOARD5, PRE_TOPC, GOBOARD1, GOBOARD4, TOPMETR, PCOMPS_1, COMPTS_1,
      WEIERSTR, TOPS_2, METRIC_1, TBSP_1, RCOMP_1, ABSVALUE, SQUARE_1,
      PSCOMP_1, RVSUM_1, TOPRNS_1, EUCLID, FUNCT_3;
 constructors REAL_1, BINARITH, GRAPH_2, GRAPH_4, GOBOARD5, GOBOARD4, WEIERSTR,
      TOPS_2, TBSP_1, RCOMP_1, ABSVALUE, SQUARE_1, PSCOMP_1, FUNCT_3, FINSEQ_4,
      TOPRNS_1, GOBOARD1, JORDAN7;
 clusters STRUCT_0, RELSET_1, GRAPH_4, EUCLID, PRE_TOPC, BORSUK_1, XREAL_0,
      FINSEQ_1, METRIC_1, ARYTM_3, MEMBERED;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, XBOOLE_0;
 theorems AXIOMS, TARSKI, FUNCT_1, FINSEQ_1, NAT_1, JORDAN3, ZFMISC_1, REAL_1,
      REAL_2, SPPOL_1, FINSEQ_4, CARD_1, FINSET_1, GRAPH_1, GRAPH_2, BINARITH,
      FUNCT_3, RELAT_1, GRAPH_4, FINSEQ_3, TOPREAL1, GOBOARD1, GOBOARD5,
      GOBOARD4, TOPREAL3, SQUARE_1, EUCLID, JORDAN7, UNIFORM1, WEIERSTR,
      JORDAN5A, TOPS_2, PRE_TOPC, TBSP_1, HEINE, COMPTS_1, TOPMETR, PSCOMP_1,
      TOPREAL5, BORSUK_1, RCOMP_1, ABSVALUE, METRIC_1, RVSUM_1, FINSEQ_2,
      FUNCT_2, GROUP_4, SCMFSA_7, JORDAN6, XBOOLE_0, XBOOLE_1, TOPRNS_1,
      JORDAN1, XCMPLX_0, XCMPLX_1;
 schemes FINSEQ_1;

begin :: GRAPHS BY CARTESIAN PRODUCT

reserve x,y for set;
reserve G for Graph;
reserve vs,vs' for FinSequence of the Vertices of G;
reserve IT for oriented Chain of G;
reserve n,m,k,i,j for Nat;
reserve r,r1,r2 for Real;

canceled;

theorem Th2: sqrt(r1^2+r2^2)<=abs(r1)+abs(r2)
proof
  A1: r1^2>=0 by SQUARE_1:72;
    r2^2>=0 by SQUARE_1:72;
  then r1^2+r2^2>=0+0 by A1,REAL_1:55;
  then A2:(sqrt(r1^2+r2^2))^2=r1^2+r2^2 by SQUARE_1:def 4;
A3:(abs(r1)+abs(r2))^2=(abs(r1))^2+2*(abs(r1))*(abs(r2))+(abs(r2))^2
  by SQUARE_1:63;
    (abs(r1))^2=r1^2 by SQUARE_1:62;
then A4:(abs(r1)+abs(r2))^2 - (sqrt(r1^2+r2^2))^2=
  r1^2+2*(abs(r1))*(abs(r2))+r2^2-(r1^2+r2^2) by A2,A3,SQUARE_1:62
  .=2*(abs(r1))*(abs(r2))+r1^2+r2^2-r1^2-r2^2 by XCMPLX_1:36
  .=2*(abs(r1))*(abs(r2))+r2^2+r1^2-r1^2-r2^2 by XCMPLX_1:1
  .=2*(abs(r1))*(abs(r2))+r2^2-r2^2 by XCMPLX_1:26
  .=2*(abs(r1))*(abs(r2)) by XCMPLX_1:26;
  A5:abs(r1)>=0 by ABSVALUE:5;
  then A6: 2*abs(r1)>=0 by SQUARE_1:19;
  A7:abs(r2)>=0 by ABSVALUE:5;
  then 2*abs(r1)*abs(r2)>=0 by A6,SQUARE_1:19;
  then A8:(abs(r1)+abs(r2))^2>= (sqrt(r1^2+r2^2))^2 by A4,REAL_2:105;
    (sqrt(r1^2+r2^2))^2>=0 by SQUARE_1:72;
  then A9:sqrt((abs(r1)+abs(r2))^2)>=sqrt((sqrt(r1^2+r2^2))^2) by A8,SQUARE_1:
94;
    abs(r1)+abs(r2)>=0+0 by A5,A7,REAL_1:55;
 hence thesis by A2,A9,SQUARE_1:89;
end;

theorem Th3: abs(r1)<=sqrt(r1^2+r2^2) & abs(r2)<=sqrt(r1^2+r2^2)
 proof
   A1: r1^2>=0 by SQUARE_1:72;
   A2:r2^2>=0 by SQUARE_1:72;
   then r1^2+0<= r1^2+r2^2 by AXIOMS:24;
   then sqrt(r1^2)<= sqrt(r1^2+r2^2) by A1,SQUARE_1:94;
  hence abs(r1)<= sqrt(r1^2+r2^2) by SQUARE_1:91;
     0+r2^2<= r1^2+r2^2 by A1,REAL_1:55;
   then sqrt(r2^2)<= sqrt(r1^2+r2^2) by A2,SQUARE_1:94;
  hence thesis by SQUARE_1:91;
 end;

theorem Th4: for vs st IT is Simple & vs is_oriented_vertex_seq_of IT
  holds for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs
 proof let vs;assume A1:IT is Simple & vs is_oriented_vertex_seq_of IT;
   then consider vs' such that A2: vs' is_oriented_vertex_seq_of IT &
     (for n,m st 1<=n & n<m & m<=len vs' & vs'.n=vs'.m holds n=1 & m=len vs')
                                           by GRAPH_4:def 7;
   A3:len vs = len IT + 1 &
   for n st 1<=n & n<=len IT holds IT.n orientedly_joins vs/.n, vs/.(n+1)
                            by A1,GRAPH_4:def 5;
   per cases;
   suppose IT<> {};
     then vs=vs' by A1,A2,GRAPH_4:11;
    hence thesis by A2;
   suppose IT= {}; then len IT=0 by FINSEQ_1:25;
    hence thesis by A3,AXIOMS:22;
 end;

definition let X be set;
 func PGraph(X) -> MultiGraphStruct equals
:Def1: MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#);
coherence;
end;

theorem Th5:for X being non empty set holds PGraph(X) is Graph
 proof let X be non empty set;
    PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
 hence thesis by GRAPH_1:def 1;
end;

theorem Th6:for X being set holds the Vertices of PGraph(X)=X
proof let X be set;
    PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
  hence thesis;
end;

definition let f be FinSequence;
 func PairF(f) -> FinSequence means
 :Def2: len it=len f-'1 &
   for i being Nat st 1<=i & i<len f holds it.i=[f.i,f.(i+1)];
 existence
  proof
    deffunc F(Nat)=[f.$1,f.($1+1)];
     ex p being FinSequence st len p = len f-'1
   & for k being Nat st k in Seg (len f-'1) holds p.k=F(k)
                                from SeqLambda;
   then consider p being FinSequence such that A1: len p = len f-'1
   & for k being Nat st k in Seg (len f-'1) holds p.k=[f.k,f.(k+1)];
     for i being Nat st 1<=i & i<len f holds p.i=[f.i,f.(i+1)]
   proof let i be Nat;assume A2:1<=i & i<len f;
     then len f>1 by AXIOMS:22;
     then A3:len f-1=len f-'1 by SCMFSA_7:3;
       i+1<=len f by A2,NAT_1:38;
     then i+1-1<=len f-1 by REAL_1:49;
     then i<=len f-'1 by A3,XCMPLX_1:26;
     then i in Seg (len f-'1) by A2,FINSEQ_1:3;
    hence thesis by A1;
   end;
   hence thesis by A1;
  end;
 uniqueness
 proof let g1,g2 be FinSequence;
   assume A4:(len g1=len f-'1 &
   for i being Nat st 1<=i & i<len f holds g1.i=[f.i,f.(i+1)])&
    (len g2=len f-'1 &
   for i being Nat st 1<=i & i<len f holds g2.i=[f.i,f.(i+1)]);
   per cases;
   suppose A5:len f>=1;
       for j being Nat st 1<=j & j<=len g1 holds g1.j=g2.j
     proof let j be Nat;assume A6:1<=j & j<=len g1;
         len f<len f+1 by NAT_1:38;
       then len f-1<len f by REAL_1:84;
       then len g1<len f by A4,A5,SCMFSA_7:3;
       then A7:j<len f by A6,AXIOMS:22;
       then g1.j=[f.j,f.(j+1)] by A4,A6;
      hence thesis by A4,A6,A7;
     end;
     hence thesis by A4,FINSEQ_1:18;
   suppose len f<1; then len f+1<=1 by NAT_1:38;
     then len f+1-1<=1-1 by REAL_1:49;
     then len f<=0 by XCMPLX_1:26; then A8:len f=0 by NAT_1:18; 0-1<0;
     then A9:len g1=0 & len g2=0 by A4,A8,BINARITH:def 3;
     then g1= {} by FINSEQ_1:25;
    hence thesis by A9,FINSEQ_1:25;
 end;
end;

reserve X for non empty set;

definition let X be non empty set;
 cluster PGraph(X) -> Graph-like;
 coherence by Th5;
end;

theorem Th7:for f being FinSequence of X
  holds f is FinSequence of the Vertices of PGraph(X)
proof let f be FinSequence of X;
    PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
  hence thesis;
end;

theorem Th8:for f being FinSequence of X
  holds PairF(f) is FinSequence of the Edges of PGraph(X)
proof let f be FinSequence of X;
   A1:rng PairF(f) c= [:X,X:]
   proof let y be set;assume y in rng PairF(f);
     then consider x being set such that
          A2:x in dom PairF(f) & y=(PairF(f)).x by FUNCT_1:def 5;
     A3:x in Seg len PairF(f) by A2,FINSEQ_1:def 3;
     reconsider n=x as Nat by A2;
     A4:1<=n & n<=len PairF(f) by A3,FINSEQ_1:3;
     A5:len PairF(f)=len f-'1 by Def2;
     then 1<=len f-'1 by A4,AXIOMS:22;
     then A6:len f-'1=len f-1 by JORDAN3:1;
       len f-'1<len f-'1+1 by NAT_1:38;
     then len f-'1<len f by A6,XCMPLX_1:27;
     then A7:n<len f by A4,A5,AXIOMS:22;
     then A8:(PairF(f)).n =[f.n,f.(n+1)] by A4,Def2;
     A9:rng f c= X by FINSEQ_1:def 4;
       n in dom f by A4,A7,FINSEQ_3:27;
then A10: f.n in rng f by FUNCT_1:def 5;
     A11:1<n+1 by A4,NAT_1:38;
       n+1<=len f by A7,NAT_1:38;
     then n+1 in dom f by A11,FINSEQ_3:27;
     then f.(n+1) in rng f by FUNCT_1:def 5;
    hence y in [:X,X:] by A2,A8,A9,A10,ZFMISC_1:def 2;
   end;
    PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
 hence thesis by A1,FINSEQ_1:def 4;
end;

definition let X be non empty set,f be FinSequence of X;
 redefine func PairF(f) -> FinSequence of the Edges of PGraph(X);
 coherence by Th8;
end;

theorem Th9:for n being Nat,f being FinSequence of X
  st 1 <= n & n <= len PairF(f) holds
  (PairF(f)).n in the Edges of PGraph(X)
proof let n be Nat,f be FinSequence of X;
 assume A1:1 <= n & n <= len PairF(f);
  A2:len PairF(f)=len f-'1 by Def2;
  then 1<=len f-'1 by A1,AXIOMS:22;
  then A3:len f-'1=len f-1 by JORDAN3:1;
    len f-'1<len f-'1+1 by NAT_1:38;
  then len f-'1<len f by A3,XCMPLX_1:27;
  then A4:n<len f by A1,A2,AXIOMS:22;
  then A5:(PairF(f)).n =[f.n,f.(n+1)] by A1,Def2;
  A6:rng f c= X by FINSEQ_1:def 4;
    n in dom f by A1,A4,FINSEQ_3:27;
then A7:f.n in rng f by FUNCT_1:def 5;
  A8:1<n+1 by A1,NAT_1:38;
    n+1<=len f by A4,NAT_1:38;
  then n+1 in dom f by A8,FINSEQ_3:27;
then A9:f.(n+1) in rng f by FUNCT_1:def 5;
    PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
 hence thesis by A5,A6,A7,A9,ZFMISC_1:def 2;
end;

theorem Th10:for f being FinSequence of X holds
 PairF(f) is oriented Chain of PGraph(X)
proof let f be FinSequence of X;
A1: now per cases;
  case len f>=1;
       then len f-1+1=len f-'1+1 by SCMFSA_7:3;
       then len f=len f-'1+1 by XCMPLX_1:27;
       then A2:len f = len PairF(f) + 1 by Def2;
       A3:for n st 1 <= n & n <= len f holds f.n in the Vertices of PGraph(X)
        proof let n;assume
          A4:1 <= n & n <= len f;
           A5:rng f c= X by FINSEQ_1:def 4;
             n in dom f by A4,FINSEQ_3:27;
then A6:        f.n in rng f by FUNCT_1:def 5;
             PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
           hence thesis by A5,A6;
        end;
         for n st 1 <= n & n <= len PairF(f)
         ex x', y' being Element of the Vertices of PGraph(X) st
           x' = f.n & y' = f.(n+1) & (PairF(f)).n joins x', y'
        proof let n;assume A7:1 <= n & n <= len PairF(f);
         A8:len PairF(f)=len f-'1 by Def2;
         then 1<=len f-'1 by A7,AXIOMS:22;
         then A9:len f-'1=len f-1 by JORDAN3:1;
           len f-'1<len f-'1+1 by NAT_1:38;
         then len f-'1<len f by A9,XCMPLX_1:27;
         then A10:n<len f by A7,A8,AXIOMS:22;
         A11:rng f c= X by FINSEQ_1:def 4;
           n in dom f by A7,A10,FINSEQ_3:27;
then A12:     f.n in rng f by FUNCT_1:def 5;
         A13:1<n+1 by A7,NAT_1:38;
           n+1<=len f by A10,NAT_1:38;
         then n+1 in dom f by A13,FINSEQ_3:27;
then A14:     f.(n+1) in rng f by FUNCT_1:def 5;
     A15:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
         then reconsider a=f.n,b=f.(n+1) as Element of the Vertices of PGraph(X
)
                                     by A11,A12,A14;
         A16:(pr1(X,X)).([f.n,f.(n+1)])=f.n by A11,A12,A14,FUNCT_3:def 5;
           (pr2(X,X)).([f.n,f.(n+1)])=f.(n+1)
                           by A11,A12,A14,FUNCT_3:def 6;
         then ((the Source of PGraph(X)).((PairF(f)).n) = a
         & (the Target of PGraph(X)).((PairF(f)).n) = b)
                              by A7,A10,A15,A16,Def2;
          then (PairF(f)).n joins a, b by GRAPH_1:def 9;
         hence thesis;
        end;
     then (for n st 1 <= n & n <= len PairF(f) holds
            (PairF(f)).n in the Edges of PGraph(X)) &
     ex p being FinSequence st
       len p = len PairF(f) + 1 &
       (for n st 1 <= n & n <= len p holds p.n in the Vertices of PGraph(X)) &
       for n st 1 <= n & n <= len PairF(f)
         ex x', y' being Element of the Vertices of PGraph(X) st
           x' = p.n & y' = p.(n+1) & (PairF(f)).n joins x', y' by A2,A3,Th9;
  hence PairF(f) is Chain of PGraph(X) by GRAPH_1:def 11;
 case len f<1;
   then len f+1<=1 by NAT_1:38;
     then len f+1-1<=1-1 by REAL_1:49;
     then len f<=0 by XCMPLX_1:26; then A17:len f=0 by NAT_1:18; 0-1<0;
     then len f-'1=0 by A17,BINARITH:def 3;
     then len PairF(f)=0 by Def2;
     then PairF(f)= {} by FINSEQ_1:25;
  hence PairF(f) is oriented Chain of PGraph(X) by GRAPH_1:14;
 end;
   for n st 1 <= n & n < len PairF(f) holds
       (the Source of PGraph(X)).((PairF(f)).(n+1))
       = (the Target of PGraph(X)).((PairF(f)).n)
 proof let n;assume A18:1 <= n & n < len PairF(f);
         then A19:n+1<=len PairF(f) by NAT_1:38;
         A20:len PairF(f)=len f-'1 by Def2;
         then 1<=len f-'1 by A18,AXIOMS:22;
         then A21:len f-'1=len f-1 by JORDAN3:1;
           len f-'1<len f-'1+1 by NAT_1:38;
         then A22:len f-'1<len f by A21,XCMPLX_1:27;
         then A23:n<len f by A18,A20,AXIOMS:22;
         A24:n+1<len f by A19,A20,A22,AXIOMS:22;
         A25:rng f c= X by FINSEQ_1:def 4;
           n in dom f by A18,A23,FINSEQ_3:27;
then A26:     f.n in rng f by FUNCT_1:def 5;
         A27:1<n+1 by A18,NAT_1:38;
           n+1<=len f by A23,NAT_1:38;
         then n+1 in dom f by A27,FINSEQ_3:27;
then A28:     f.(n+1) in rng f by FUNCT_1:def 5;
         A29:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
                                  by Def1;
then reconsider a=f.n,b=f.(n+1) as Element of the Vertices of PGraph(X)
                                     by A25,A26,A28;
         A30:(pr1(X,X)).([f.n,f.(n+1)])=f.n by A25,A26,A28,FUNCT_3:def 5;
           (pr2(X,X)).([f.n,f.(n+1)])=f.(n+1) by A25,A26,A28,FUNCT_3:def 6;
         then A31:((the Source of PGraph(X)).((PairF(f)).n) = a
         & (the Target of PGraph(X)).((PairF(f)).n) = b)
                              by A18,A23,A29,A30,Def2;
         A32:rng f c= X by FINSEQ_1:def 4;
           n+1 in dom f by A24,A27,FINSEQ_3:27;
then A33:     f.(n+1) in rng f by FUNCT_1:def 5;
         A34:1<n+1+1 by A27,NAT_1:38;
           n+1+1<=len f by A24,NAT_1:38;
         then n+1+1 in dom f by A34,FINSEQ_3:27;
then A35:     f.(n+1+1) in rng f by FUNCT_1:def 5;
     A36:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#) by Def1;
           (pr1(X,X)).([f.(n+1),f.((n+1)+1)])=f.(n+1)
                            by A32,A33,A35,FUNCT_3:def 5;
  hence thesis by A24,A27,A31,A36,Def2;
 end;
 hence thesis by A1,GRAPH_1:def 12;
end;

definition let X be non empty set,f be FinSequence of X;
 redefine func PairF(f) -> oriented Chain of PGraph(X);
 coherence by Th10;
end;

theorem Th11:for f being FinSequence of X,
  f1 being FinSequence of the Vertices of PGraph(X) st len f>=1 & f=f1 holds
  f1 is_oriented_vertex_seq_of PairF(f)
 proof let f be FinSequence of X,
   f1 be FinSequence of the Vertices of PGraph(X);
  assume A1:len f>=1 & f=f1;
         then len f-'1=len f-1 by SCMFSA_7:3;
         then len f-1+1=len PairF(f)+1 by Def2;
         then A2:len f1=len PairF(f)+1 by A1,XCMPLX_1:27;
      for n st 1<=n & n<=len PairF(f) holds
      ((PairF(f)).n) orientedly_joins f1/.n, f1/.(n+1)
     proof let n;assume A3: 1<=n & n<=len PairF(f);
         A4:len PairF(f)=len f-'1 by Def2;
         then 1<=len f-'1 by A3,AXIOMS:22;
         then A5:len f-'1=len f-1 by JORDAN3:1;
           len f-'1<len f-'1+1 by NAT_1:38;
         then len f-'1<len f by A5,XCMPLX_1:27;
         then A6:n<len f by A3,A4,AXIOMS:22;
         A7:rng f c= X by FINSEQ_1:def 4;
         A8:n in dom f by A3,A6,FINSEQ_3:27;
then A9:      f.n in rng f by FUNCT_1:def 5;
         A10:1<n+1 by A3,NAT_1:38;
           n+1<=len f by A6,NAT_1:38;
         then A11:n+1 in dom f by A10,FINSEQ_3:27;
then A12:     f.(n+1) in rng f by FUNCT_1:def 5;
         A13:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
                                  by Def1;
         A14:f1/.n=f1.n by A1,A8,FINSEQ_4:def 4;
         A15:f1/.(n+1)=f1.(n+1) by A1,A11,FINSEQ_4:def 4;
         A16:(pr1(X,X)).([f.n,f.(n+1)])=f.n by A7,A9,A12,FUNCT_3:def 5;
           (pr2(X,X)).([f.n,f.(n+1)])=f.(n+1) by A7,A9,A12,FUNCT_3:def 6;
         then (the Source of PGraph(X)).((PairF(f)).n) = f1/.n
         & (the Target of PGraph(X)).((PairF(f)).n) = f1/.(n+1)
                         by A1,A3,A6,A13,A14,A15,A16,Def2;
      hence thesis by GRAPH_4:def 1;
     end;
  hence thesis by A2,GRAPH_4:def 5;
 end;

begin ::  SHORTCUTS OF FINITE SEQUENCES IN PLANE

definition let X be non empty set,f,g be FinSequence of X;
pred g is_Shortcut_of f means
:Def3: f.1=g.1 & f.len f=g.len g &
 ex fc being FinSubsequence of PairF(f),fvs being FinSubsequence of f,
 sc being oriented simple Chain of PGraph(X),
 g1 being FinSequence of the Vertices of PGraph(X)
 st Seq fc = sc & Seq fvs = g & g1=g
 & g1 is_oriented_vertex_seq_of sc;
end;

theorem Th12:for f,g being FinSequence of X st g is_Shortcut_of f holds
 1<=len g & len g <= len f
proof let f,g be FinSequence of X;assume
    g is_Shortcut_of f;
  then consider fc being FinSubsequence of PairF(f),fvs being FinSubsequence of
f,
  sc being oriented simple Chain of PGraph(X),
  g1 being FinSequence of the Vertices of PGraph(X)
  such that A1:Seq fc = sc & Seq fvs = g & g1=g
  & g1 is_oriented_vertex_seq_of sc by Def3;
   A2:len g1 = len sc + 1 by A1,GRAPH_4:def 5;
    fvs c= f by GRAPH_2:def 5;
  then A3:dom fvs c= dom f by RELAT_1:25;
  A4:g=fvs*Sgm(dom fvs) by A1,FINSEQ_1:def 14;
    rng Sgm(dom fvs) c= dom fvs by FINSEQ_1:71;
  then A5:dom g=dom (Sgm(dom fvs)) by A4,RELAT_1:46;
A6:Seg len f is finite set;
  then dom f is finite set by FINSEQ_1:def 3;
  then reconsider dfvs=dom fvs as finite set by A3,FINSET_1:13;
  reconsider df=dom f as finite set by A6,FINSEQ_1:def 3;
  A7:dom fvs c=Seg len f by A3,FINSEQ_1:def 3;
  A8:len g=len Sgm(dom fvs) by A5,FINSEQ_3:31
  .=card dfvs by A7,FINSEQ_3:44;
    card df=card (Seg len f) by FINSEQ_1:def 3 .=len f by FINSEQ_1:78;
 hence thesis by A1,A2,A3,A8,CARD_1:80,NAT_1:37;
end;

theorem Th13:for f being FinSequence of X st len f>=1 holds
 ex g being FinSequence of X st g is_Shortcut_of f
proof let f be FinSequence of X;assume A1: len f>=1;
  reconsider f1=f as FinSequence of the Vertices of PGraph(X) by Th7;
    f1 is_oriented_vertex_seq_of PairF(f) by A1,Th11;
  then consider fc being FinSubsequence of PairF(f),
  fvs being FinSubsequence of f1, sc being oriented simple Chain of PGraph(X),
  vs1 being FinSequence of the Vertices of PGraph(X)
   such that A2: Seq fc = sc & Seq fvs = vs1
   & vs1 is_oriented_vertex_seq_of sc &
     f1.1 = vs1.1 & f1.len f1 = vs1.len vs1 by GRAPH_4:23;
   A3:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
                                  by Def1;
   then reconsider g1=vs1 as FinSequence of X;
     g1 is_Shortcut_of f by A2,A3,Def3;
 hence thesis;
end;

theorem Th14:for f,g being FinSequence of X st
 g is_Shortcut_of f holds rng PairF(g) c= rng PairF(f)
proof let f,g be FinSequence of X;assume
    g is_Shortcut_of f;
  then consider fc being FinSubsequence of PairF(f),
  fvs being FinSubsequence of f,
  sc being oriented simple Chain of PGraph(X),
  g1 being FinSequence of the Vertices of PGraph(X)
   such that
  A1:Seq fc = sc & Seq fvs = g & g1=g & g1 is_oriented_vertex_seq_of sc
                                     by Def3;
  let y be set;assume y in rng PairF(g);
    then consider x being set such that
    A2: x in dom PairF(g) & y=(PairF(g)).x by FUNCT_1:def 5;
    A3:x in Seg len PairF(g) by A2,FINSEQ_1:def 3;
    reconsider n=x as Nat by A2;
    A4:1<=n & n<=len PairF(g) by A3,FINSEQ_1:3;
    A5:len PairF(g)=len g-'1 by Def2;
      1<=len PairF(g) by A4,AXIOMS:22;
    then A6:len g-'1=len g-1 by A5,JORDAN3:1;
      len g<len g+1 by NAT_1:38;
    then len g-1<len g by REAL_1:84;
    then A7:n<len g by A4,A5,A6,AXIOMS:22;
    then A8:(PairF(g)).x=[g.n,g.(n+1)] by A4,Def2;
    A9:n+1<=len g by A7,NAT_1:38;
    A10:fc* Sgm(dom fc)=sc by A1,FINSEQ_1:def 14;
      rng Sgm(dom fc) = dom fc by FINSEQ_1:71;
    then A11:rng fc = rng sc by A10,RELAT_1:47;
      fc c= PairF(f) by GRAPH_2:def 5;
    then A12:rng sc c= rng PairF(f) by A11,RELAT_1:25;
      n+1<=len sc+1 by A1,A9,GRAPH_4:def 5;
    then A13:n<=len sc by REAL_1:53;
then A14: (sc.n) orientedly_joins g1/.n, g1/.(n+1) by A1,A4,GRAPH_4:def 5;
      n in dom sc by A4,A13,FINSEQ_3:27;
    then sc.n in rng sc by FUNCT_1:def 5;
    then consider z being set such that
    A15: z in dom PairF(f) & (PairF(f)).z=sc.n by A12,FUNCT_1:def 5;
    A16:z in Seg len PairF(f) by A15,FINSEQ_1:def 3;
    reconsider m=z as Nat by A15;
A17: 1<=m & m<=len PairF(f) by A16,FINSEQ_1:3;
    then A18:1<=m & m<=len f -'1 by Def2;
    then 1<=len f-'1 by AXIOMS:22;
    then A19:len f-'1=len f-1 by JORDAN3:1;
      len f<len f+1 by NAT_1:38;
    then len f-1<len f by REAL_1:84;
    then A20:1<=m & m<len f by A18,A19,AXIOMS:22;
    then A21:[f.m,f.(m+1)]=sc.n by A15,Def2;
      m in dom f by A20,FINSEQ_3:27;
    then A22:f.m in rng f by FUNCT_1:def 5;
    A23:1<m+1 by A17,NAT_1:38;
      m+1<=len f by A20,NAT_1:38;
    then m+1 in dom f by A23,FINSEQ_3:27;
    then A24:f.(m+1) in rng f by FUNCT_1:def 5;
A25:  rng f c= X by FINSEQ_1:def 4;
    A26:PGraph(X)=MultiGraphStruct(#X,[:X,X:],pr1(X,X),pr2(X,X)#)
                                  by Def1;
    then A27:(the Source of PGraph(X)).(sc.n)= f.m by A21,A22,A24,A25,FUNCT_3:
def 5;
      (the Target of PGraph(X)).(sc.n)= f.(m+1) by A21,A22,A24,A25,A26,FUNCT_3:
def 6;
    then A28:g1/.n=f.m & g1/.(n+1)=f.(m+1) by A14,A27,GRAPH_4:def 1;
      1<=n+1 & n+1<=len g1 by A1,A4,A7,NAT_1:38;
    then g.n=f.m & g.(n+1)=f.(m+1) by A1,A4,A7,A28,FINSEQ_4:24;
   hence thesis by A2,A8,A15,A21,FUNCT_1:def 5;
end;

theorem Th15:for f,g being FinSequence of X st f.1<>f.len f &
g is_Shortcut_of f holds g is one-to-one & rng PairF(g) c= rng PairF(f)
& g.1=f.1 & g.len g=f.len f
proof let f,g be FinSequence of X;
 assume A1:f.1<>f.len f & g is_Shortcut_of f;
 then A2: f.1=g.1 & f.len f=g.len g &
  ex fc being FinSubsequence of PairF(f),fvs being FinSubsequence of f,
  sc being oriented simple Chain of PGraph(X),
  g1 being FinSequence of the Vertices of PGraph(X)
  st Seq fc = sc & Seq fvs = g & g1=g
  & g1 is_oriented_vertex_seq_of sc by Def3;
  consider fc being FinSubsequence of PairF(f),
  fvs being FinSubsequence of f,
  sc being oriented simple Chain of PGraph(X),
  g1 being FinSequence of the Vertices of PGraph(X)
   such that
  A3:Seq fc = sc & Seq fvs = g & g1=g & g1 is_oriented_vertex_seq_of sc
                                        by A1,Def3;
    sc is Simple by GRAPH_4:20;
  then consider vs being FinSequence of the Vertices of PGraph(X)
   such that A4: vs is_oriented_vertex_seq_of sc &
     (for n,m being Nat st 1<=n & n<m & m<=len vs & vs.n=vs.m
     holds n=1 & m=len vs) by GRAPH_4:def 7;
     A5:len g1 = len sc + 1 &
     for n st 1<=n & n<=len sc holds sc.n orientedly_joins g1/.n,g1/.(n+1)
                                  by A3,GRAPH_4:def 5;
     then 1<=len g1 by NAT_1:29;
     then 1<len g1 by A1,A2,A3,REAL_1:def 5;
     then len sc>=1 by A5,NAT_1:38;
     then len sc>0 by AXIOMS:22;
     then sc<> {} by FINSEQ_1:25;
     then A6:g1=vs by A3,A4,GRAPH_4:11;
   for x,y being set st x in dom g & y in dom g & g.x=g.y holds x=y
  proof let x,y be set;assume
A7: x in dom g & y in dom g & g.x=g.y;
    then A8:x in Seg len g by FINSEQ_1:def 3;
    reconsider i1=x as Nat by A7;
    A9:y in Seg len g by A7,FINSEQ_1:def 3;
    reconsider i2=y as Nat by A7;
    A10:1<=i1 & i1<=len g by A8,FINSEQ_1:3;
    A11:1<=i2 & i2<=len g by A9,FINSEQ_1:3;
      now assume A12:x<>y;
     per cases;
     suppose i1<=i2;
       then i1<i2 by A12,REAL_1:def 5;
       then i1=1 & i2=len g by A3,A4,A6,A7,A10,A11;
      hence contradiction by A1,A2,A7;
     suppose i1>i2;
       then i2=1 & i1=len g by A3,A4,A6,A7,A10,A11;
      hence contradiction by A1,A2,A7;
    end;
   hence x=y;
  end;
 hence g is one-to-one by FUNCT_1:def 8;
 thus rng PairF(g) c= rng PairF(f) by A1,Th14;
 thus thesis by A1,Def3;
end;

definition let n; let IT be FinSequence of TOP-REAL n;
   attr IT is nodic means
   :Def4: for i,j st LSeg(IT,i) meets LSeg(IT,j)
         holds LSeg(IT,i) /\ LSeg(IT,j)={IT.i}
               &(IT.i=IT.j or IT.i=IT.(j+1)) or
               LSeg(IT,i) /\ LSeg(IT,j)={IT.(i+1)}
               &(IT.(i+1)=IT.j or IT.(i+1)=IT.(j+1)) or
               LSeg(IT,i)=LSeg(IT,j);
end;

theorem for f being FinSequence of TOP-REAL 2 st f is s.n.c.
  holds f is s.c.c.
proof let f be FinSequence of TOP-REAL 2;
  assume f is s.n.c.;
  then for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f)
    holds LSeg(f,i) misses LSeg(f,j) by TOPREAL1:def 9;
  hence thesis by GOBOARD5:def 4;
end;

theorem Th17:for f being FinSequence of TOP-REAL 2 st f is s.c.c. &
 LSeg(f,1) misses LSeg(f,len f -'1) holds f is s.n.c.
proof let f be FinSequence of TOP-REAL 2;
  assume A1:f is s.c.c. & LSeg(f,1) misses LSeg(f,len f -'1);
     for i,j st i+1 < j holds LSeg(f,i) misses LSeg(f,j)
    proof let i,j;assume A2:i+1 < j;
      per cases;
      suppose len f<>0; then len f>0 by NAT_1:19;
then A3:      len f>=0+1 by NAT_1:38;
          now per cases;
        case A4:1<=i & j+1<=len f;
          then A5:j<len f by NAT_1:38;
            now per cases;
          case A6:i=1 & j+1=len f;
            then j=len f-1 by XCMPLX_1:26;
           then LSeg(f,i) misses LSeg(f,j) by A1,A3,A6,SCMFSA_7:3;
           hence LSeg(f,i) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
          case not(i=1 & j+1=len f);
           then i>1 or j+1<len f by A4,REAL_1:def 5;
           then LSeg(f,i) misses LSeg(f,j) by A1,A2,A5,GOBOARD5:def 4;
           hence LSeg(f,i) /\ LSeg(f,j) = {} by XBOOLE_0:def 7;
          end;
         hence LSeg(f,i) /\ LSeg(f,j) = {};
        case A7:not (1<=i & j+1<=len f);
            now per cases by A7;
          case 1>i;
            then LSeg(f,i)={} by TOPREAL1:def 5;
           hence LSeg(f,i) /\ LSeg(f,j) = {};
          case j+1>len f;
            then LSeg(f,j)={} by TOPREAL1:def 5;
           hence LSeg(f,i) /\ LSeg(f,j) = {};
          end;
         hence LSeg(f,i) /\ LSeg(f,j) = {};
        end;
       hence thesis by XBOOLE_0:def 7;
      suppose A8:len f=0;
          now per cases;
        case i>=1; then i>len f by A8,AXIOMS:22;
          then i+1>len f by NAT_1:38;
          then LSeg(f,i)={} by TOPREAL1:def 5;
         hence LSeg(f,i) /\ LSeg(f,j) = {};
        case i<1;
          then LSeg(f,i)={} by TOPREAL1:def 5;
         hence LSeg(f,i) /\ LSeg(f,j) = {};
        end;
       hence thesis by XBOOLE_0:def 7;
    end;
  hence thesis by TOPREAL1:def 9;
end;

theorem Th18: for f being FinSequence of TOP-REAL 2 st
  f is nodic & PairF(f) is Simple holds f is s.c.c.
proof let f be FinSequence of TOP-REAL 2;
 assume A1:f is nodic & PairF(f) is Simple;
   reconsider f1=f as
     FinSequence of the Vertices of PGraph(the carrier of TOP-REAL 2) by Th6;
   per cases;
   suppose len f>=1;
then A2:f1 is_oriented_vertex_seq_of PairF(f) by Th11;
    for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f)
    holds LSeg(f,i) misses LSeg(f,j)
  proof let i,j;assume A3:i+1 < j & (i > 1 & j < len f or j+1 < len f);
    per cases;
    suppose A4:i>=1;
      A5:i<j by A3,NAT_1:38;
      A6:i+1<j+1 by A3,NAT_1:38;
      A7:1<=j by A4,A5,AXIOMS:22;
      A8:j<len f by A3,NAT_1:38;
       then A9: i+1<len f by A3,AXIOMS:22;
       A10:i<j+1 by A5,NAT_1:38;
       A11: j+1<=len f by A3,NAT_1:38;
       then A12:i<len f by A10,AXIOMS:22;
       A13:1<i+1 by A4,NAT_1:38;
       A14:1<j+1 by A7,NAT_1:38;
      now assume A15:LSeg(f,i) meets LSeg(f,j);
        now per cases by A1,A15,Def4;
      case A16:LSeg(f,i) /\ LSeg(f,j)={f.i}
        &(f.i=f.j or f.i=f.(j+1))& LSeg(f,i)<>LSeg(f,j);
          now per cases by A16;
        case f.i=f.j;
         hence contradiction by A1,A2,A4,A5,A8,Th4;
        case f.i=f.(j+1);
         hence contradiction by A1,A2,A3,A4,A10,A11,Th4;
        end;
       hence contradiction;
      case A17:LSeg(f,i) /\ LSeg(f,j)={f.(i+1)}
        &(f.(i+1)=f.j or f.(i+1)=f.(j+1))&LSeg(f,i)<>LSeg(f,j);
          now per cases by A17;
        case f.(i+1)=f.j;
         hence contradiction by A1,A2,A3,A8,A13,Th4;
        case f.(i+1)=f.(j+1);
         hence contradiction by A1,A2,A6,A11,A13,Th4;
        end;
       hence contradiction;
      case LSeg(f,i)=LSeg(f,j);
        then LSeg(f/.i,f/.(i+1))=LSeg(f,j) by A4,A9,TOPREAL1:def 5;
then A18:     LSeg(f/.i,f/.(i+1))=LSeg(f/.j,f/.(j+1))
                         by A7,A11,TOPREAL1:def 5;
        A19:f/.i=f.i by A4,A12,FINSEQ_4:24;
        A20:f/.(i+1)=f.(i+1) by A9,A13,FINSEQ_4:24;
        A21:f/.j=f.j by A7,A8,FINSEQ_4:24;
        A22:f/.(j+1)=f.(j+1) by A11,A14,FINSEQ_4:24;
          now per cases by A18,A19,A20,A21,A22,SPPOL_1:25;
        case f.i=f.j & f.(i+1)=f.(j+1);
         hence contradiction by A1,A2,A6,A11,A13,Th4;
        case f.i=f.(j+1) & f.(i+1)=f.j;
         hence contradiction by A1,A2,A3,A8,A13,Th4;
        end;
       hence contradiction;
      end;
     hence contradiction;
    end;
   hence thesis;
   suppose i<1;
     then LSeg(f,i)={} by TOPREAL1:def 5;
     then LSeg(f,i) /\ LSeg(f,j) = {};
    hence thesis by XBOOLE_0:def 7;
  end;
  hence thesis by GOBOARD5:def 4;
 suppose A23:len f<1;
    for i,j st i+1 < j & (i > 1 & j < len f or j+1 < len f)
    holds LSeg(f,i) misses LSeg(f,j)
   proof let i,j;assume i+1 < j & (i > 1 & j < len f or j+1 < len f);
     per cases;
     suppose i>=1; then i>len f by A23,AXIOMS:22;
       then i+1>len f by NAT_1:38;
       then LSeg(f,i)={} by TOPREAL1:def 5;
       then LSeg(f,i) /\ LSeg(f,j) = {};
      hence thesis by XBOOLE_0:def 7;
     suppose i<1;
       then LSeg(f,i)={} by TOPREAL1:def 5;
       then LSeg(f,i) /\ LSeg(f,j) = {};
      hence thesis by XBOOLE_0:def 7;
   end;
  hence thesis by GOBOARD5:def 4;
end;

theorem Th19:for f being FinSequence of TOP-REAL 2 st
  f is nodic & PairF(f) is Simple & f.1<>f.len f holds f is s.n.c.
proof let f be FinSequence of TOP-REAL 2;
  assume A1:f is nodic & PairF(f) is Simple & f.1<>f.len f;
   then A2:f is s.c.c. by Th18;
   reconsider f1=f as
     FinSequence of the Vertices of PGraph(the carrier of TOP-REAL 2) by Th6;
   A3:len f-'1<=len f by JORDAN3:7;
  per cases;
  suppose A4:len f-'1>2;
   then A5:len f-'1>1 by AXIOMS:22;
   then A6:1<len f by JORDAN3:7;
     len f>=1 by A5,JORDAN3:7;
then A7:f1 is_oriented_vertex_seq_of PairF(f) by Th11;
   A8:1+1<len f by A4,JORDAN3:7;
A9:len f-'1=len f-1 by A5,JORDAN3:1;
   then A10:(len f-'1)+1=len f by XCMPLX_1:27;
     now assume
A11:  LSeg(f,1) meets LSeg(f,len f-'1);
       now per cases by A1,A11,Def4;
     case LSeg(f,1) /\ LSeg(f,(len f-'1))={f.1}
               &(f.1=f.(len f-'1) or f.1=f.((len f-'1)+1));
      hence contradiction by A1,A3,A5,A7,A9,Th4,XCMPLX_1:27;
     case A12:LSeg(f,1) /\ LSeg(f,(len f-'1))={f.(1+1)}
               &(f.(1+1)=f.(len f-'1) or f.(1+1)=f.((len f-'1)+1));
         now per cases by A12;
       case f.(1+1)=f.(len f-'1);
        hence contradiction by A1,A3,A4,A7,Th4;
       case f.(1+1)=f.((len f-'1)+1);
        hence contradiction by A1,A7,A8,A10,Th4;
       end;
      hence contradiction;
     case A13:LSeg(f,1)=LSeg(f,(len f-'1));
      A14:1+1<(len f-'1)+1 by A5,REAL_1:53;
      A15:(len f-'1)<len f by A10,NAT_1:38;
       A16:1<(len f-'1)+1 by A6,A9,XCMPLX_1:27;
       A17: (len f-'1)+1<=len f by A9,XCMPLX_1:27;
       A18:1<len f by A5,JORDAN3:7;
          LSeg(f/.1,f/.(1+1))=LSeg(f,(len f-'1))
                         by A8,A13,TOPREAL1:def 5;
then A19:     LSeg(f/.1,f/.(1+1))=LSeg(f/.(len f-'1),f/.((len f-'1)+1))
                         by A5,A17,TOPREAL1:def 5;
        A20:f/.1=f.1 by A18,FINSEQ_4:24;
        A21:f/.(1+1)=f.(1+1) by A8,FINSEQ_4:24;
        A22:f/.(len f-'1)=f.(len f-'1) by A5,A15,FINSEQ_4:24;
        A23:f/.((len f-'1)+1)=f.((len f-'1)+1) by A16,A17,FINSEQ_4:24;
          now per cases by A19,A20,A21,A22,A23,SPPOL_1:25;
        case f.1=f.(len f-'1) & f.(1+1)=f.((len f-'1)+1);
         hence contradiction by A1,A7,A14,A17,Th4;
        case f.1=f.((len f-'1)+1) & f.(1+1)=f.(len f-'1);
         hence contradiction by A1,A9,XCMPLX_1:27;
        end;
       hence contradiction;
     end;
    hence contradiction;
   end;
   hence thesis by A2,Th17;
  suppose A24:len f-'1<=2;
        for i,j st i+1 < j holds LSeg(f,i) misses LSeg(f,j)
      proof let i,j;assume A25:i+1 < j;
        per cases;
        suppose A26:1<=i & j+1<=len f;
            i+1+1<j+1 by A25,REAL_1:53;
          then A27:i+1+1<len f by A26,AXIOMS:22;
            1<i+1 by A26,NAT_1:38;
          then 1+1<i+1+1 by REAL_1:67;
          then 1+1+1<=i+1+1 by NAT_1:38;
          then 1+1+1<len f by A27,AXIOMS:22;
then A28:      1+1+1-1<len f-1 by REAL_1:54;
          then 1<len f-1 by AXIOMS:22;
         hence thesis by A24,A28,JORDAN3:1;
        suppose A29:1>i or j+1>len f;
            now per cases by A29;
          case 1>i;
            then LSeg(f,i)={} by TOPREAL1:def 5;
           hence LSeg(f,i) /\ LSeg(f,j) = {};
          case j+1>len f;
            then LSeg(f,j)={} by TOPREAL1:def 5;
           hence LSeg(f,i) /\ LSeg(f,j) = {};
        end;
        hence thesis by XBOOLE_0:def 7;
     end;
     hence thesis by TOPREAL1:def 9;
end;

theorem Th20:for p1,p2,p3 being Point of TOP-REAL n st
 (ex x being set st x<>p2 & x in LSeg(p1,p2)/\ LSeg(p2,p3)) holds
 p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2)
proof let p1,p2,p3 be Point of TOP-REAL n;
 given x being set such that
   A1:x<>p2 & x in LSeg(p1,p2)/\ LSeg(p2,p3);
   A2:x in LSeg(p1,p2) & x in LSeg(p2,p3) by A1,XBOOLE_0:def 3;
   reconsider p=x as Point of TOP-REAL n by A1;
     p in { (1-r1)*p1 + r1*p2 : 0 <= r1 & r1 <= 1 } by A2,TOPREAL1:def 4;
   then consider r1 such that
   A3:p=(1-r1)*p1 + r1*p2 &( 0 <= r1 & r1 <= 1 );
     p in { (1-r2)*p2 + r2*p3 : 0 <= r2 & r2 <= 1 } by A2,TOPREAL1:def 4;
   then consider r2 such that
   A4:p=(1-r2)*p2 + r2*p3 &( 0 <= r2 & r2 <= 1 );
   per cases;
   suppose A5:r1>=1-r2;
       now per cases;
     case A6:r2<>0;
        r2*p3=(1-r1)*p1 + r1*p2-(1-r2)*p2 by A3,A4,EUCLID:52;
      then r2*p3=(1-r1)*p1 + (r1*p2-(1-r2)*p2) by EUCLID:49;
      then r2"*(r2*p3)=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by EUCLID:54;
      then (r2"*r2)*p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by EUCLID:34;
      then 1*p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by A6,XCMPLX_0:def 7;
then A7:   p3=r2"*((1-r1)*p1 + (r1-(1-r2))*p2) by EUCLID:33
      .=r2"*((1-r1)*p1) +r2"*((r1-(1-r2))*p2) by EUCLID:36
      .=(r2"*(1-r1))*p1 +r2"*((r1-(1-r2))*p2) by EUCLID:34
      .=(r2"*(1-r1))*p1 +(r2"*(r1-(1-r2)))*p2 by EUCLID:34;
        r2"*(1-r1) +r2"*(r1-(1-r2))=r2"*(1-r1+(r1-(1-r2))) by XCMPLX_1:8
      .=r2"*(1-r1+r1-(1-r2)) by XCMPLX_1:29 .=r2"*(1-(1-r2)) by XCMPLX_1:27
      .=r2"*(1-1+r2) by XCMPLX_1:37 .=1 by A6,XCMPLX_0:def 7;
      then A8:r2"*(1-r1)=1-r2"*(r1-(1-r2)) by XCMPLX_1:26;
      A9:(r1-(1-r2))>=0 by A5,SQUARE_1:12;
      A10:r2">0 by A4,A6,REAL_1:72;
      then A11:0<=r2"*(r1-(1-r2)) by A9,REAL_2:121;
        r1<=1+0 by A3;
      then r1-1<=0 by REAL_1:86;
      then r1-1+r2<=0+r2 by AXIOMS:24;
      then (r1-(1-r2))<=r2 by XCMPLX_1:37;
      then r2"*(r1-(1-r2))<=r2"*r2 by A10,AXIOMS:25;
      then r2"*(r1-(1-r2))<=1 by A6,XCMPLX_0:def 7;
      then p3 in {(1-r)*p1+r*p2:0<=r & r<=1} by A7,A8,A11;
     hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by TOPREAL1:def 4;
     case r2=0; then p=1*p2+0.REAL n by A4,EUCLID:33;
      then p=p2+0.REAL n by EUCLID:33;
     hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by A1,EUCLID:31;
     end;
     hence thesis;
   suppose A12:r1<1-r2;
     set s1=1-r2;
     set s2=1-r1;
     A13:1-s1=1-1+r2 by XCMPLX_1:37 .=r2;
     A14:1-s2=1-1+r1 by XCMPLX_1:37 .=r1;
A15:  0+s1<=1-s1+s1 by A4,A13,AXIOMS:24;
       1-s2+s2<=1+s2 by A3,A14,AXIOMS:24;
     then 1<=1+s2 by XCMPLX_1:27;
then A16:  1-1<=s2 by REAL_1:86;
       now per cases;
     case A17:s2<>0;
        s2*p1=(1-s1)*p3 + s1*p2-(1-s2)*p2 by A3,A4,A13,A14,EUCLID:52
      .=(1-s1)*p3 + (s1*p2-(1-s2)*p2) by EUCLID:49
      .=(1-s1)*p3 + (s1-(1-s2))*p2 by EUCLID:54;
      then (s2"*s2)*p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by EUCLID:34;
      then 1*p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by A17,XCMPLX_0:def 7;
      then p1=s2"*((1-s1)*p3 + (s1-(1-s2))*p2) by EUCLID:33
      .=s2"*((1-s1)*p3) +s2"*((s1-(1-s2))*p2) by EUCLID:36
      .=(s2"*(1-s1))*p3 +s2"*((s1-(1-s2))*p2) by EUCLID:34;
      then A18:p1=(s2"*(1-s1))*p3 +(s2"*(s1-(1-s2)))*p2 by EUCLID:34;
        s2"*(1-s1) +s2"*(s1-(1-s2))=s2"*(1-s1+(s1-(1-s2))) by XCMPLX_1:8
      .=s2"*(1-s1+s1-(1-s2)) by XCMPLX_1:29 .=s2"*(1-(1-s2)) by XCMPLX_1:27
      .=s2"*(1-1+s2) by XCMPLX_1:37 .=1 by A17,XCMPLX_0:def 7;
      then A19:s2"*(1-s1)=1-s2"*(s1-(1-s2)) by XCMPLX_1:26;
      A20:(s1-(1-s2))>=0 by A12,A14,SQUARE_1:12;
      A21:s2">0 by A16,A17,REAL_1:72;
      then A22:0<=s2"*(s1-(1-s2)) by A20,REAL_2:121;
        s1<=1+0 by A15,XCMPLX_1:27;
      then s1-1<=0 by REAL_1:86;
      then s1-1+s2<=0+s2 by AXIOMS:24;
      then (s1-(1-s2))<=s2 by XCMPLX_1:37;
      then s2"*(s1-(1-s2))<=s2"*s2 by A21,AXIOMS:25;
      then s2"*(s1-(1-s2))<=1 by A17,XCMPLX_0:def 7;
      then p1 in {(1-r)*p3+r*p2:0<=r & r<=1} by A18,A19,A22;
     hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by TOPREAL1:def 4;
     case s2=0; then p=1*p2+0.REAL n by A3,A14,EUCLID:33;
      then p=p2+0.REAL n by EUCLID:33;
      hence p1 in LSeg(p2,p3) or p3 in LSeg(p1,p2) by A1,EUCLID:31;
     end;
   hence thesis;
end;

theorem Th21:for f being FinSequence of TOP-REAL 2 st f is s.n.c. &
LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} &
LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)} holds
f is unfolded
proof let f be FinSequence of TOP-REAL 2;
  assume A1: f is s.n.c. &
   LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)} &
   LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)};
     for i st 1 <= i & i + 2 <= len f
    holds LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)}
    proof let i;assume A2:1 <= i & i + 2 <= len f;
      A3:i+1+1=i+(1+1) by XCMPLX_1:1 .=i+2;
      A4: 1<i+1 by A2,NAT_1:38;
      A5:i+1<len f by A2,A3,NAT_1:38;
      then A6:i<len f by NAT_1:38;
      A7:1<i+1+1 by A4,NAT_1:38;
      A8:LSeg(f,i)=LSeg(f/.i,f/.(i+1)) by A2,A5,TOPREAL1:def 5;
      A9:LSeg(f,i+1)=LSeg(f/.(i+1),f/.(i+1+1))
                               by A2,A3,A4,TOPREAL1:def 5;
      A10:f/.(i+1) in LSeg(f/.i,f/.(i+1)) by TOPREAL1:6;
        f/.(i+1) in LSeg(f/.(i+1),f/.(i+1+1)) by TOPREAL1:6;
      then f/.(i+1) in LSeg(f,i) /\ LSeg(f,i+1) by A8,A9,A10,XBOOLE_0:def 3;
      then A11:{f/.(i+1)} c= LSeg(f,i) /\ LSeg(f,i+1) by ZFMISC_1:37;
      per cases;
      suppose i=1;
       hence thesis by A1,A11,XBOOLE_0:def 10;
      suppose A12:i<>1;
         now per cases;
       case A13:i+2=len f;
         then A14:i=len f-2 by XCMPLX_1:26;
         then A15:len f-2=len f-'2 by A2,JORDAN3:1;
         A16:i+1=len f-1 by A3,A13,XCMPLX_1:26;
         then len f-1=len f-'1 by A4,JORDAN3:1;
        hence LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)}
                              by A1,A11,A14,A15,A16,XBOOLE_0:def 10;
       case i+2<>len f;
         then i+2<len f by A2,REAL_1:def 5;
         then A17:i+1+1+1<=len f by A3,NAT_1:38;
           1<i by A2,A12,REAL_1:def 5;
         then 1+1<=i by NAT_1:38;
then A18:     1+1-1<=i-1 by REAL_1:49;
           now assume A19:LSeg(f,i) /\ LSeg(f,i+1)<>{f/.(i+1)};
            A20:f/.(i+1) in LSeg(f,i+1) by A9,TOPREAL1:6;
              f/.(i+1) in LSeg(f,i) by A8,TOPREAL1:6;
            then f/.(i+1) in LSeg(f,i) /\ LSeg(f,i+1) by A20,XBOOLE_0:def 3;
            then {f/.(i+1)} c= LSeg(f,i) /\ LSeg(f,i+1) by ZFMISC_1:37;
            then not LSeg(f,i) /\ LSeg(f,i+1) c= {f/.(i+1)}
                       by A19,XBOOLE_0:def 10;
           then consider x being set such that
A21: x in LSeg(f,i) /\ LSeg(f,i+1) & not x in {f/.(i+1)} by TARSKI:def 3;
             A22:x<>f/.(i+1) by A21,TARSKI:def 1;
            A23:LSeg(f,i+1+1)=LSeg(f/.(i+1+1),f/.(i+1+1+1))
                               by A7,A17,TOPREAL1:def 5;
              now per cases by A8,A9,A21,A22,Th20;
            case A24: f/.i in LSeg(f/.(i+1),f/.(i+1+1));
              A25:i-'1=i-1 by A2,SCMFSA_7:3;
              then A26:i-'1+1=i by XCMPLX_1:27;
              then i-'1+1<i+1 by NAT_1:38;
              then LSeg(f,i-'1) misses LSeg(f,i+1) by A1,TOPREAL1:def 9;
              then A27:LSeg(f,i-'1)/\ LSeg(f,i+1)={} by XBOOLE_0:def 7;
                LSeg(f,i-'1)=LSeg(f/.(i-'1),f/.(i-'1+1))
                            by A6,A18,A25,A26,TOPREAL1:def 5;
              then f/.i in LSeg(f,i-'1) by A26,TOPREAL1:6;
             hence contradiction by A9,A24,A27,XBOOLE_0:def 3;
            case A28: f/.(i+1+1) in LSeg(f/.i,f/.(i+1));
                i+1<i+1+1 by NAT_1:38;
              then LSeg(f,i) misses LSeg(f,i+1+1) by A1,TOPREAL1:def 9;
              then A29:LSeg(f,i)/\ LSeg(f,i+1+1)={} by XBOOLE_0:def 7;
                f/.(i+1+1) in LSeg(f,i+1+1) by A23,TOPREAL1:6;
             hence contradiction by A8,A28,A29,XBOOLE_0:def 3;
            end;
          hence contradiction;
         end;
        hence LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)};
       end;
       hence thesis;
    end;
  hence thesis by TOPREAL1:def 8;
end;

theorem Th22:for f being FinSequence of X holds
  PairF(f) is Simple & f.1<>f.len f implies f is one-to-one & len f<>1
proof let f be FinSequence of X;
  thus PairF(f) is Simple & f.1<>f.len f implies f is one-to-one & len f<>1
   proof assume A1:PairF(f) is Simple & f.1<>f.len f;
     then consider vs being FinSequence of the Vertices of PGraph(X) such that
     A2:vs is_oriented_vertex_seq_of PairF(f) &
     (for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
                                              by GRAPH_4:def 7;
     reconsider f1=f as FinSequence of the Vertices of PGraph(X) by Th7;
       now per cases;
     case A3:len f>=1;
        now per cases by A3,REAL_1:def 5;
      case A4: len f>1;
     A5: f1 is_oriented_vertex_seq_of PairF(f) by A3,Th11;
      then len f1=len PairF(f)+1 by GRAPH_4:def 5;
      then 1-1<len PairF(f)+1-1 by A4,REAL_1:54;
      then 1-1<len PairF(f) by XCMPLX_1:26;
      then PairF(f) <> {} by FINSEQ_1:25;
     then A6:vs = f1 by A2,A5,GRAPH_4:11;
       for x,y st x in dom f & y in dom f & f.x=f.y holds x=y
      proof let x,y;assume A7:x in dom f & y in dom f & f.x=f.y;
        A8:dom f=Seg len f by FINSEQ_1:def 3;
        reconsider i=x,j=y as Nat by A7;
        A9:1<=i & i<=len f by A7,A8,FINSEQ_1:3;
        A10:1<=j & j<=len f by A7,A8,FINSEQ_1:3;
          now assume A11:i<>j;
            now per cases by A11,REAL_1:def 5;
          case i<j; then i=1 & j=len f by A2,A6,A7,A9,A10;
           hence contradiction by A1,A7;
          case j<i; then j=1 & i=len f by A2,A6,A7,A9,A10;
           hence contradiction by A1,A7;
          end;
          hence contradiction;
         end;
       hence thesis;
      end;
    hence f is one-to-one by FUNCT_1:def 8;
     case len f=1;
    hence f is one-to-one by A1;
     end;
    hence f is one-to-one;
    case len f<1; then len f+1<=1 by NAT_1:38;
      then len f+1-1<=1-1 by REAL_1:49; then len f<=1-1 by XCMPLX_1:26;
   then len f=0 by NAT_1:18;
     then for x,y st x in dom f & y in dom f & f.x=f.y holds x=y by FINSEQ_1:4,
def 3;
    hence f is one-to-one by FUNCT_1:def 8;
    end;
    hence thesis by A1;
   end;
end;

theorem for f being FinSequence of X holds
  f is one-to-one & len f>1 implies PairF(f) is Simple & f.1<>f.len f
proof let f be FinSequence of X;
   assume A1:f is one-to-one & len f>1;
    then A2:1 in dom f by FINSEQ_3:27;
A3: len f in dom f by A1,FINSEQ_3:27;
     reconsider f1=f as FinSequence of the Vertices of PGraph(X) by Th7;
     A4: f1 is_oriented_vertex_seq_of PairF(f) by A1,Th11;
       for i,j st 1<=i & i<j & j<=len f1 & f1.i=f1.j holds i=1 & j=len f1
      proof let i,j;assume A5:1<=i & i<j & j<=len f1 & f1.i=f1.j;
        then A6:i<len f by AXIOMS:22;
          1<j by A5,AXIOMS:22;
then A7:     j in Seg len f by A5,FINSEQ_1:3;
          i in Seg len f by A5,A6,FINSEQ_1:3;
        then i in dom f & j in dom f by A7,FINSEQ_1:def 3;
       hence thesis by A1,A5,FUNCT_1:def 8;
      end;
    hence thesis by A1,A2,A3,A4,FUNCT_1:def 8,GRAPH_4:def 7;
end;

theorem for f being FinSequence of TOP-REAL 2 st
  f is nodic & PairF(f) is Simple & f.1<>f.len f holds f is unfolded
proof let f be FinSequence of TOP-REAL 2;
  assume A1:f is nodic & PairF(f) is Simple & f.1<>f.len f;
  then A2:f is s.n.c. by Th19;
  per cases;
  suppose A3:2<len f;
   then A4:2+1<=len f by NAT_1:38;
   A5:1+1<=len f by A3;
   A6:LSeg(f,1)=LSeg(f/.1,f/.(1+1)) by A3,TOPREAL1:def 5;
   A7:LSeg(f,2)=LSeg(f/.2,f/.(2+1)) by A4,TOPREAL1:def 5;
   A8:f is one-to-one by A1,Th22;
  A9:1<len f by A3,AXIOMS:22;
  then A10:1 in dom f by FINSEQ_3:27;
  A11:2 in dom f by A3,FINSEQ_3:27;
  A12:f.1=f/.1 by A9,FINSEQ_4:24;
  A13:2+1 in dom f by A4,FINSEQ_3:27;
  A14:f.2=f/.2 by A3,FINSEQ_4:24;
  then A15:f.2 in LSeg(f,1) by A5,TOPREAL1:27;
   A16:now assume A17:LSeg(f,1)=LSeg(f,2);
        now per cases by A6,A7,A17,SPPOL_1:25;
      case A18:f/.1=f/.2 & f/.(1+1)=f/.(2+1);
        A19:f.1=f/.1 by A9,FINSEQ_4:24;
          f.2=f/.2 by A3,FINSEQ_4:24;
       hence contradiction by A8,A10,A11,A18,A19,FUNCT_1:def 8;
      case A20:f/.1=f/.(2+1) & f/.(1+1)=f/.2;
          f.(2+1)=f/.(2+1) by A4,FINSEQ_4:24;
       hence contradiction by A8,A10,A12,A13,A20,FUNCT_1:def 8;
      end;
     hence contradiction;
   end;
     f.2 in LSeg(f,2) by A4,A14,TOPREAL1:27;
   then LSeg(f,1)/\ LSeg(f,2)<>{} by A15,XBOOLE_0:def 3;
   then LSeg(f,1) meets LSeg(f,2) by XBOOLE_0:def 7;
   then LSeg(f,1) /\ LSeg(f,2)={f.1} &(f.1=f.2 or f.1=f.(2+1)) or
   LSeg(f,1) /\ LSeg(f,2)={f.(1+1)} &(f.(1+1)=f.2 or f.(1+1)=f.(2+1))
     by A1,A16,Def4;
  then A21:LSeg(f,1) /\ LSeg(f,1+1) c= {f/.(1+1)}
    by A3,A8,A10,A13,FINSEQ_4:24,FUNCT_1:def 8;
A22:1+1-1<=len f-1 by A3,REAL_1:49;
A23:2+1-2<=len f-2 by A4,REAL_1:49;
   A24:len f-1=len f-'1 by A9,SCMFSA_7:3;
   then A25:len f-'1+1=len f by XCMPLX_1:27;
   A26:len f-'2=len f-2 by A3,SCMFSA_7:3;
then A27:len f-'2+1=len f-(1+1-1) by XCMPLX_1:37;
     len f<len f+1 by NAT_1:38;
   then A28:len f-1<len f by REAL_1:84;
   then len f-1-1<len f-1 by REAL_1:54;
   then A29:len f-(1+1)<len f-1 by XCMPLX_1:36;
   then A30:len f-2<len f by A28,AXIOMS:22;
   A31:len f-'2<len f by A26,A28,A29,AXIOMS:22;
   then A32:(len f-'2)+1<=len f by NAT_1:38;
   then A33:LSeg(f,(len f-'2))=LSeg(f/.(len f-'2),f/.((len f-'2)+1))
                           by A23,A26,TOPREAL1:def 5;
   A34:LSeg(f,(len f-'1))=LSeg(f/.(len f-'1),f/.((len f-'1)+1))
                           by A22,A24,A25,TOPREAL1:def 5;
   A35:f.(len f-'2)=f/.(len f-'2) by A23,A26,A31,FINSEQ_4:24;
   A36:f.(len f-'2)=f/.(len f-'2) by A23,A26,A30,FINSEQ_4:24;
   A37:now assume A38:LSeg(f,(len f-'2))=LSeg(f,(len f-'1));
      A39:(len f-'2) in dom f by A23,A26,A31,FINSEQ_3:27;
      A40:(len f-'1) in dom f by A22,A24,A28,FINSEQ_3:27;
        now per cases by A33,A34,A38,SPPOL_1:25;
      case A41:f/.(len f-'2)=f/.(len f-'1)
                   & f/.((len f-'2)+1)=f/.((len f-'1)+1);
          f.(len f-'1)=f/.(len f-'1) by A22,A24,A28,FINSEQ_4:24;
       hence contradiction by A8,A24,A26,A29,A35,A39,A40,A41,FUNCT_1:def 8;
      case A42:f/.(len f-'2)=f/.((len f-'1)+1)
            & f/.((len f-'2)+1)=f/.(len f-'1);
          (len f-'1)+1 in Seg len f by A9,A25,FINSEQ_1:3;
        then A43:(len f-'1)+1 in dom f by FINSEQ_1:def 3;
          f.((len f-'1)+1)=f/.((len f-'1)+1) by A9,A25,FINSEQ_4:24;
       hence contradiction
         by A8,A25,A26,A28,A29,A36,A39,A42,A43,FUNCT_1:def 8;
      end;
     hence contradiction;
   end;
   A44:f.(len f-'1)=f/.(len f-'1) by A22,A24,A28,FINSEQ_4:24;
   then A45:f.(len f-'1) in LSeg(f,(len f-'2))
                  by A23,A24,A26,A27,A32,TOPREAL1:27;
     f.(len f-'1) in LSeg(f,(len f-'1)) by A22,A24,A25,A44,TOPREAL1:27;
   then LSeg(f,(len f-'2))/\ LSeg(f,(len f-'1))<>{} by A45,XBOOLE_0:def 3;
   then LSeg(f,(len f-'2)) meets LSeg(f,(len f-'1)) by XBOOLE_0:def 7;
   then A46:LSeg(f,(len f-'2)) /\ LSeg(f,(len f-'1))={f.(len f-'2)}
     &(f.(len f-'2)=f.(len f-'1) or f.(len f-'2)=f.((len f-'1)+1)) or
     LSeg(f,(len f-'2)) /\ LSeg(f,(len f-'1))={f.((len f-'2)+1)}
     &(f.((len f-'2)+1)=f.(len f-'1) or f.((len f-'2)+1)=f.((len f-'1)+1))
                                    by A1,A37,Def4;
   A47:len f-'2 in dom f by A23,A26,A31,FINSEQ_3:27;
     len f-'1+1 in dom f by A9,A25,FINSEQ_3:27;
  then LSeg(f,len f-'2) /\ LSeg(f,len f-'1) c= {f/.(len f-'1)}
    by A8,A22,A24,A25,A26,A27,A28,A29,A46,A47,FINSEQ_4:24,FUNCT_1:def 8;
 hence thesis by A2,A21,Th21;
 suppose A48:len f<=2;
    for i st 1 <= i & i + 2 <= len f
       holds LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)}
  proof let i;assume A49:1 <= i & i + 2 <= len f;
    then i+2<=2 by A48,AXIOMS:22;
    then i<=2-2 by REAL_1:84;
   hence thesis by A49,AXIOMS:22;
  end;
 hence thesis by TOPREAL1:def 8;
end;

theorem Th25: for f,g being FinSequence of TOP-REAL 2,i st
 g is_Shortcut_of f & 1 <= i & i+1 <= len g holds
 ex k1 being Nat st 1<=k1 & k1+1<=len f & f/.k1=g/.i &
   f/.(k1+1)=g/.(i+1)
    & f.k1=g.i & f.(k1+1)=g.(i+1)
   proof let f,g be FinSequence of TOP-REAL 2,i;assume that
     A1:g is_Shortcut_of f and
     A2:1 <= i & i+1 <= len g;
     A3:i<=len g by A2,NAT_1:38;
     A4:1<=i+1 by A2,NAT_1:38;
     A5: rng PairF(g) c= rng PairF(f) by A1,Th14;
     A6:i<len g by A2,NAT_1:38;
     then A7:(PairF(g)).i=[g.i,g.(i+1)] by A2,Def2;
     A8:len PairF(g)=len g -'1 by Def2;
     A9:i<=len g-1 by A2,REAL_1:84;
     then 1<=len g-1 by A2,AXIOMS:22;
     then len g-'1=len g-1 by JORDAN3:1;
     then i in dom (PairF(g)) by A2,A8,A9,FINSEQ_3:27;
     then [ g.i,g.(i+1) ] in rng PairF(g) by A7,FUNCT_1:def 5;
     then consider x such that
     A10:x in dom PairF(f) & (PairF(f)).x=[g.i,g.(i+1)] by A5,FUNCT_1:def 5;
     A11:x in Seg len PairF(f) by A10,FINSEQ_1:def 3;
     reconsider k=x as Nat by A10;
     A12:1<=k & k<=len PairF(f) by A11,FINSEQ_1:3;
     A13:len PairF(f)=len f-'1 by Def2;
     A14:1<len g by A2,A6,AXIOMS:22;
       len g<=len f by A1,Th12;
     then 1<=len f by A14,AXIOMS:22;
     then len f-'1=len f-1 by SCMFSA_7:3;
     then k+1<=len f-1+1 by A12,A13,AXIOMS:24;
     then A15:k+1<=len f by XCMPLX_1:27;
     then A16:k<len f by NAT_1:38;
     then [ g.i,g.(i+1)]=[ f.k,f.(k+1) ] by A10,A12,Def2;
     then A17:g.i=f.k & g.(i+1)=f.(k+1) by ZFMISC_1:33;
     A18:1<k+1 by A12,NAT_1:38;
     A19:g/.i=g.i by A2,A3,FINSEQ_4:24;
     A20:g/.(i+1)=g.(i+1) by A2,A4,FINSEQ_4:24;
     A21:f/.k=f.k by A12,A16,FINSEQ_4:24;
       f/.(k+1)=f.(k+1) by A15,A18,FINSEQ_4:24;
   hence thesis by A12,A15,A17,A19,A20,A21;
   end;

theorem Th26: for f,g being FinSequence of TOP-REAL 2 st
 g is_Shortcut_of f holds rng g c= rng f
proof let f,g be FinSequence of TOP-REAL 2;
  assume A1: g is_Shortcut_of f;
 let x;assume x in rng g;
   then consider z being set such that
   A2:z in dom g & x=g.z by FUNCT_1:def 5;
   A3:z in Seg len g by A2,FINSEQ_1:def 3;
   reconsider i=z as Nat by A2;
   A4:1<=i & i<=len g by A3,FINSEQ_1:3;
   per cases;
   suppose i<len g; then i+1<=len g by NAT_1:38;
     then consider k1 being Nat such that
     A5:1<=k1 & k1+1<=len f & f/.k1=g/.i
     & f/.(k1+1)=g/.(i+1) & f.k1=g.i & f.(k1+1)=g.(i+1) by A1,A4,Th25;
       k1<len f by A5,NAT_1:38;
     then k1 in dom f by A5,FINSEQ_3:27;
    hence x in rng f by A2,A5,FUNCT_1:def 5;
   suppose i>=len g; then A6:i=len g by A4,AXIOMS:21;
       now per cases;
     case A7:1<i; then 1-1<i-1 by REAL_1:54;
       then 0<i-'1 by A7,SCMFSA_7:3;
       then A8:0+1<=i-'1 by NAT_1:38;
         i-'1=i-1 by A7,SCMFSA_7:3;
       then A9:i-'1+1=len g by A6,XCMPLX_1:27;
       then consider k1 being Nat such that
       A10:1<=k1 & k1+1<=len f & f/.k1=g/.(i-'1)
         & f/.(k1+1)=g/.(i-'1+1) & f.k1=g.(i-'1)
         & f.(k1+1)=g.(i-'1+1) by A1,A8,Th25;
           1<k1+1 by A10,NAT_1:38;
         then k1+1 in dom f by A10,FINSEQ_3:27;
      hence x in rng f by A2,A6,A9,A10,FUNCT_1:def 5;
     case 1>=i;
       then A11:i=1 by A4,AXIOMS:21;
       A12:f.1=g.1 by A1,Def3;
         len g<=len f by A1,Th12;
       then 1 in dom f by A6,A11,FINSEQ_3:27;
      hence x in rng f by A2,A11,A12,FUNCT_1:def 5;
     end;
    hence thesis;
end;

theorem Th27: for f,g being FinSequence of TOP-REAL 2 st
 g is_Shortcut_of f holds L~g c= L~f
proof let f,g be FinSequence of TOP-REAL 2;
  assume A1: g is_Shortcut_of f;
  let x be set;assume x in L~g;
    then x in union { LSeg(g,i) : 1 <= i & i+1 <= len g } by TOPREAL1:def 6;
    then consider y such that A2:x in y & y in
      { LSeg(g,i) : 1 <= i & i+1 <= len g }
                    by TARSKI:def 4;
    consider i such that A3: y=LSeg(g,i) &(1<=i & i+1<=len g) by A2;
    A4:x in LSeg(g/.i,g/.(i+1)) by A2,A3,TOPREAL1:def 5;
    consider k1 being Nat such that
        A5:  1<=k1 & k1+1<=len f & f/.k1=g/.i & f/.(k1+1)=g/.(i+1)
        & f.k1=g.i & f.(k1+1)=g.(i+1) by A1,A3,Th25;
    A6:x in LSeg(f,k1) by A4,A5,TOPREAL1:def 5;
      LSeg(f,k1) in {LSeg(f,k):1<=k & k+1<=len f} by A5;
    then x in union { LSeg(f,k) : 1 <= k & k+1 <= len f } by A6,TARSKI:def 4;
   hence thesis by TOPREAL1:def 6;
end;

theorem Th28: for f,g being FinSequence of TOP-REAL 2 st f is special
 & g is_Shortcut_of f holds g is special
proof let f,g be FinSequence of TOP-REAL 2;assume
  A1:f is special & g is_Shortcut_of f;
    for i st 1 <= i & i+1 <= len g holds
    (g/.i)`1 = (g/.(i+1))`1 or (g/.i)`2 = (g/.(i+1))`2
   proof let i;assume
     A2:1 <= i & i+1 <= len g;
     then A3:i<=len g by NAT_1:38;
     A4:1<=i+1 by A2,NAT_1:38;
     A5: rng PairF(g) c= rng PairF(f) by A1,Th14;
     A6:i<len g by A2,NAT_1:38;
     then A7:(PairF(g)).i=[g.i,g.(i+1)] by A2,Def2;
     A8:len PairF(g)=len g -'1 by Def2;
     A9:i<=len g-1 by A2,REAL_1:84;
     then 1<=len g-1 by A2,AXIOMS:22;
     then len g-'1=len g-1 by JORDAN3:1;
     then i in dom PairF(g) by A2,A8,A9,FINSEQ_3:27;
     then [ (g.i),(g.(i+1)) ] in rng PairF(g) by A7,FUNCT_1:def 5;
     then consider x such that
     A10:x in dom PairF(f) & (PairF(f)).x=[g.i,g.(i+1)] by A5,FUNCT_1:def 5;
     A11:x in Seg len PairF(f) by A10,FINSEQ_1:def 3;
     reconsider k=x as Nat by A10;
     A12:1<=k & k<=len PairF(f) by A11,FINSEQ_1:3;
     A13:len PairF(f)=len f-'1 by Def2;
     A14:1<len g by A2,A6,AXIOMS:22;
       len g<=len f by A1,Th12;
     then 1<=len f by A14,AXIOMS:22;
     then len f-'1=len f-1 by SCMFSA_7:3;
     then k+1<=len f-1+1 by A12,A13,AXIOMS:24;
     then A15:k+1<=len f by XCMPLX_1:27;
     then A16:k<len f by NAT_1:38;
     then (PairF(f)).k=[f.k,f.(k+1)] by A12,Def2;
     then A17:g.i=f.k & g.(i+1)=f.(k+1) by A10,ZFMISC_1:33;
     A18:1<k+1 by A12,NAT_1:38;
     A19:g/.i=g.i by A2,A3,FINSEQ_4:24;
     A20:g/.(i+1)=g.(i+1) by A2,A4,FINSEQ_4:24;
     A21:f/.k=f.k by A12,A16,FINSEQ_4:24;
       f/.(k+1)=f.(k+1) by A15,A18,FINSEQ_4:24;
    hence thesis by A1,A12,A15,A17,A19,A20,A21,TOPREAL1:def 7;
   end;
  hence thesis by TOPREAL1:def 7;
end;

theorem Th29:for f being FinSequence of TOP-REAL 2 st f is special & 2<=len f
 & f.1 <> f.len f holds ex g being FinSequence of TOP-REAL 2 st
 2<=len g & g is special & g is one-to-one & L~g c= L~f & f.1=g.1
 & f.len f=g.len g & rng g c= rng f
proof let f be FinSequence of TOP-REAL 2;assume
  A1:f is special & 2<=len f & f.1 <> f.len f; then 1<=len f by AXIOMS:22;
  then consider g being FinSequence of TOP-REAL 2 such that
  A2:g is_Shortcut_of f by Th13;
  A3:g is one-to-one & rng PairF(g) c= rng PairF(f)
   & g.1=f.1 & g.len g=f.len f by A1,A2,Th15;
  A4:g is special by A1,A2,Th28;
  A5:L~g c= L~f by A2,Th27;
  A6: rng g c= rng f by A2,Th26;
    1<=len g by A2,Th12;
  then 1<len g by A1,A3,REAL_1:def 5;
  then 1+1<=len g by NAT_1:38;
 hence thesis by A3,A4,A5,A6;
end;

::  Goboard Theorem for general special sequences
theorem Th30:for f1,f2 being FinSequence of TOP-REAL 2 st
 f1 is special & f2 is special & 2<=len f1 & 2<=len f2 & f1.1<>f1.len f1
 & f2.1<>f2.len f2 &
 X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
 Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds
  L~f1 meets L~f2
proof let f1,f2 be FinSequence of TOP-REAL 2;
 assume A1:f1 is special & f2 is special & 2<=len f1
 & 2<=len f2 & f1.1<>f1.len f1
 & f2.1<>f2.len f2 &
 X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
 Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) &
 Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2);
 then consider g1 being FinSequence of TOP-REAL 2 such that
 A2: 2<=len g1 & g1 is special & g1 is one-to-one & L~g1 c= L~f1 & f1.1=g1.1
 & f1.len f1=g1.len g1 & rng g1 c= rng f1 by Th29;
  consider g2 being FinSequence of TOP-REAL 2 such that
 A3: 2<=len g2 & g2 is special & g2 is one-to-one & L~g2 c= L~f2 & f2.1=g2.1
 & f2.len f2=g2.len g2 & rng g2 c= rng f2 by A1,Th29;
    for i st i in dom X_axis(g1) holds (X_axis(g1)).1 <= X_axis(g1).i
    & X_axis(g1).i <= (X_axis(g1)).(len g1)
   proof let i;assume A4:i in dom X_axis(g1);
    A5:len (X_axis(f1)) = len f1 &
    for j st j in dom X_axis(f1) holds (X_axis(f1)).j = (f1/.j)`1
                               by GOBOARD1:def 3;
    A6:len (X_axis(g1)) = len g1 &
    for j st j in dom X_axis(g1) holds (X_axis(g1)).j = (g1/.j)`1
                               by GOBOARD1:def 3;
    A7:1<=len g1 by A2,AXIOMS:22;
    then A8:1 in dom X_axis(g1) by A6,FINSEQ_3:27;
    A9:g1/.1=g1.1 by A7,FINSEQ_4:24;
    A10:1<=len f1 by A1,AXIOMS:22;
    then A11:g1/.1=f1/.1 by A2,A9,FINSEQ_4:24;
      g1/.len g1=g1.(len g1) by A7,FINSEQ_4:24;
    then A12:g1/.len g1=f1/.len f1 by A2,A10,FINSEQ_4:24;
    A13:1 in dom X_axis(f1) by A5,A10,FINSEQ_3:27;
      i in Seg len g1 by A4,A6,FINSEQ_1:def 3;
    then A14:i in dom g1 by FINSEQ_1:def 3; then g1.i in rng g1 by FUNCT_1:def
5;
    then consider y being set such that
    A15:y in dom f1 & g1.i=f1.y by A2,FUNCT_1:def 5;
    reconsider j=y as Nat by A15;
      f1.j=f1/.j by A15,FINSEQ_4:def 4;
    then A16:j in dom f1 & g1/.i=f1/.j by A14,A15,FINSEQ_4:def 4;
      j in Seg len f1 by A15,FINSEQ_1:def 3;
    then A17:j in dom (X_axis(f1)) by A5,FINSEQ_1:def 3;
    then A18:(X_axis(f1)).1 <= X_axis(f1).j
    & X_axis(f1).j <= (X_axis(f1)).(len f1) by A1,GOBOARD4:def 1;
    A19:X_axis(f1).j =(f1/.j)`1 by A17,GOBOARD1:def 3;
      len f1 in Seg len f1 by A10,FINSEQ_1:3;
    then len f1 in dom (X_axis(f1)) by A5,FINSEQ_1:def 3;
    then A20:(g1/.1)`1<=(g1/.i)`1 & (g1/.i)`1<=(g1/.len g1)`1
                   by A11,A12,A13,A16,A18,A19,GOBOARD1:def 3;
    A21:X_axis(g1).i = (g1/.i)`1 by A4,GOBOARD1:def 3;
      len g1 in Seg len g1 by A7,FINSEQ_1:3;
    then len g1 in dom (X_axis(g1)) by A6,FINSEQ_1:def 3;
    hence thesis by A8,A20,A21,GOBOARD1:def 3;
   end;
   then A22:X_axis(g1) lies_between (X_axis(g1)).1, (X_axis(g1)).(len g1)
                                  by GOBOARD4:def 1;
    for i st i in dom X_axis(g2) holds (X_axis(g1)).1 <= X_axis(g2).i
    & X_axis(g2).i <= (X_axis(g1)).(len g1)
   proof let i;assume A23:i in dom X_axis(g2);
    A24:len (X_axis(f2)) = len f2 &
    for j st j in dom X_axis(f2) holds (X_axis(f2)).j = (f2/.j)`1
                               by GOBOARD1:def 3;
    A25:len (X_axis(f1)) = len f1 &
    for j st j in dom X_axis(f1) holds (X_axis(f1)).j = (f1/.j)`1
                               by GOBOARD1:def 3;
    A26:len (X_axis(g2)) = len g2 &
    for j st j in dom X_axis(g2) holds (X_axis(g2)).j = (g2/.j)`1
                               by GOBOARD1:def 3;
    A27:len (X_axis(g1)) = len g1 &
    for j st j in dom X_axis(g1) holds (X_axis(g1)).j = (g1/.j)`1
                               by GOBOARD1:def 3;
    A28:1<=len g1 by A2,AXIOMS:22; then 1 in Seg len g1 by FINSEQ_1:3;
    then A29:1 in dom (X_axis(g1)) by A27,FINSEQ_1:def 3;
    A30:g1/.1=g1.1 by A28,FINSEQ_4:24;
    A31:1<=len f1 by A1,AXIOMS:22;
    then A32:g1/.1=f1/.1 by A2,A30,FINSEQ_4:24;
      g1/.len g1=g1.(len g1) by A28,FINSEQ_4:24;
    then A33:g1/.len g1=f1/.len f1 by A2,A31,FINSEQ_4:24;
      1 in Seg len f1 by A31,FINSEQ_1:3;
    then A34:1 in dom (X_axis(f1)) by A25,FINSEQ_1:def 3;
      i in Seg len g2 by A23,A26,FINSEQ_1:def 3;
    then A35:i in dom g2 by FINSEQ_1:def 3; then g2.i in rng g2 by FUNCT_1:def
5;
    then consider y being set such that
    A36:y in dom f2 & g2.i=f2.y by A3,FUNCT_1:def 5;
    reconsider j=y as Nat by A36;
      f2.j=f2/.j by A36,FINSEQ_4:def 4;
    then A37:j in dom f2 & g2/.i=f2/.j by A35,A36,FINSEQ_4:def 4;
      j in Seg len f2 by A36,FINSEQ_1:def 3;
    then A38:j in dom (X_axis(f2)) by A24,FINSEQ_1:def 3;
    then A39:(X_axis(f1)).1 <= X_axis(f2).j
    & X_axis(f2).j <= (X_axis(f1)).(len f1) by A1,GOBOARD4:def 1;
    A40:X_axis(f2).j =(f2/.j)`1 by A38,GOBOARD1:def 3;
      len f1 in Seg len f1 by A31,FINSEQ_1:3;
    then len f1 in dom (X_axis(f1)) by A25,FINSEQ_1:def 3;
    then A41:(g1/.1)`1<=(g2/.i)`1 & (g2/.i)`1<=(g1/.len g1)`1
                   by A32,A33,A34,A37,A39,A40,GOBOARD1:def 3;
    A42:X_axis(g2).i =(g2/.i)`1 by A23,GOBOARD1:def 3;
      len g1 in Seg len g1 by A28,FINSEQ_1:3;
    then len g1 in dom (X_axis(g1)) by A27,FINSEQ_1:def 3;
    hence thesis by A29,A41,A42,GOBOARD1:def 3;
   end;
   then A43:X_axis(g2) lies_between (X_axis(g1)).1, (X_axis(g1)).(len g1)
                                  by GOBOARD4:def 1;
    for i st i in dom Y_axis(g1) holds (Y_axis(g2)).1 <= Y_axis(g1).i
    & Y_axis(g1).i <= (Y_axis(g2)).(len g2)
   proof let i;assume A44:i in dom Y_axis(g1);
    A45:len (Y_axis(f1)) = len f1 &
    for j st j in dom Y_axis(f1) holds (Y_axis(f1)).j = (f1/.j)`2
                               by GOBOARD1:def 4;
    A46:len (Y_axis(f2)) = len f2 &
    for j st j in dom Y_axis(f2) holds (Y_axis(f2)).j = (f2/.j)`2
                               by GOBOARD1:def 4;
    A47:len (Y_axis(g1)) = len g1 &
    for j st j in dom Y_axis(g1) holds (Y_axis(g1)).j = (g1/.j)`2
                               by GOBOARD1:def 4;
    A48:len (Y_axis(g2)) = len g2 &
    for j st j in dom Y_axis(g2) holds (Y_axis(g2)).j = (g2/.j)`2
                               by GOBOARD1:def 4;
    A49:1<=len g2 by A3,AXIOMS:22; then 1 in Seg len g2 by FINSEQ_1:3;
    then A50:1 in dom (Y_axis(g2)) by A48,FINSEQ_1:def 3;
    A51:g2/.1=g2.1 by A49,FINSEQ_4:24;
    A52:1<=len f2 by A1,AXIOMS:22;
    then A53:g2/.1=f2/.1 by A3,A51,FINSEQ_4:24;
      g2/.len g2=g2.(len g2) by A49,FINSEQ_4:24;
    then A54:g2/.len g2=f2/.len f2 by A3,A52,FINSEQ_4:24;
      1 in Seg len f2 by A52,FINSEQ_1:3;
    then A55:1 in dom (Y_axis(f2)) by A46,FINSEQ_1:def 3;
      i in Seg len g1 by A44,A47,FINSEQ_1:def 3;
    then A56:i in dom g1 by FINSEQ_1:def 3; then g1.i in rng g1 by FUNCT_1:def
5;
    then consider y being set such that
    A57:y in dom f1 & g1.i=f1.y by A2,FUNCT_1:def 5;
    reconsider j=y as Nat by A57;
      f1.j=f1/.j by A57,FINSEQ_4:def 4;
    then A58:j in dom f1 & g1/.i=f1/.j by A56,A57,FINSEQ_4:def 4;
      j in Seg len f1 by A57,FINSEQ_1:def 3;
    then A59:j in dom (Y_axis(f1)) by A45,FINSEQ_1:def 3;
    then A60:(Y_axis(f2)).1 <= Y_axis(f1).j
    & Y_axis(f1).j <= (Y_axis(f2)).(len f2) by A1,GOBOARD4:def 1;
    A61:Y_axis(f1).j =(f1/.j)`2 by A59,GOBOARD1:def 4;
      len f2 in Seg len f2 by A52,FINSEQ_1:3;
    then len f2 in dom (Y_axis(f2)) by A46,FINSEQ_1:def 3;
    then A62:(g2/.1)`2<=(g1/.i)`2 & (g1/.i)`2<=(g2/.len g2)`2
                   by A53,A54,A55,A58,A60,A61,GOBOARD1:def 4;
    A63:Y_axis(g1).i = (g1/.i)`2 by A44,GOBOARD1:def 4;
      len g2 in Seg len g2 by A49,FINSEQ_1:3;
    then len g2 in dom (Y_axis(g2)) by A48,FINSEQ_1:def 3;
    hence thesis by A50,A62,A63,GOBOARD1:def 4;
   end;
   then A64:Y_axis(g1) lies_between (Y_axis(g2)).1, (Y_axis(g2)).(len g2)
                                  by GOBOARD4:def 1;
    for i st i in dom Y_axis(g2) holds (Y_axis(g2)).1 <= Y_axis(g2).i
    & Y_axis(g2).i <= (Y_axis(g2)).(len g2)
   proof let i;assume A65:i in dom Y_axis(g2);
    A66:len (Y_axis(f2)) = len f2 &
    for j st j in dom Y_axis(f2) holds (Y_axis(f2)).j = (f2/.j)`2
                               by GOBOARD1:def 4;
    A67:len (Y_axis(g2)) = len g2 &
    for j st j in dom Y_axis(g2) holds (Y_axis(g2)).j = (g2/.j)`2
                               by GOBOARD1:def 4;
    A68:1<=len g2 by A3,AXIOMS:22; then 1 in Seg len g2 by FINSEQ_1:3;
    then A69:1 in dom (Y_axis(g2)) by A67,FINSEQ_1:def 3;
    A70:g2/.1=g2.1 by A68,FINSEQ_4:24;
    A71:1<=len f2 by A1,AXIOMS:22;
    then A72:g2/.1=f2/.1 by A3,A70,FINSEQ_4:24;
      g2/.len g2=g2.(len g2) by A68,FINSEQ_4:24;
    then A73:g2/.len g2=f2/.len f2 by A3,A71,FINSEQ_4:24;
      1 in Seg len f2 by A71,FINSEQ_1:3;
    then A74:1 in dom (Y_axis(f2)) by A66,FINSEQ_1:def 3;
      i in Seg len g2 by A65,A67,FINSEQ_1:def 3;
    then A75:i in dom g2 by FINSEQ_1:def 3; then g2.i in rng g2 by FUNCT_1:def
5;
    then consider y being set such that
    A76:y in dom f2 & g2.i=f2.y by A3,FUNCT_1:def 5;
    reconsider j=y as Nat by A76;
      f2.j=f2/.j by A76,FINSEQ_4:def 4;
    then A77:j in dom f2 & g2/.i=f2/.j by A75,A76,FINSEQ_4:def 4;
      j in Seg len f2 by A76,FINSEQ_1:def 3;
    then A78:j in dom (Y_axis(f2)) by A66,FINSEQ_1:def 3;
    then A79:(Y_axis(f2)).1 <= Y_axis(f2).j
    & Y_axis(f2).j <= (Y_axis(f2)).(len f2) by A1,GOBOARD4:def 1;
    A80:Y_axis(f2).j =(f2/.j)`2 by A78,GOBOARD1:def 4;
      len f2 in Seg len f2 by A71,FINSEQ_1:3;
    then len f2 in dom (Y_axis(f2)) by A66,FINSEQ_1:def 3;
    then A81:(g2/.1)`2<=(g2/.i)`2 & (g2/.i)`2<=(g2/.len g2)`2
                   by A72,A73,A74,A77,A79,A80,GOBOARD1:def 4;
    A82:Y_axis(g2).i =(g2/.i)`2 by A65,GOBOARD1:def 4;
      len g2 in Seg len (Y_axis(g2)) by A67,A68,FINSEQ_1:3;
    then len g2 in dom (Y_axis(g2)) by FINSEQ_1:def 3;
    hence thesis by A69,A81,A82,GOBOARD1:def 4;
   end;
   then A83:Y_axis(g2) lies_between (Y_axis(g2)).1, (Y_axis(g2)).(len g2)
                                  by GOBOARD4:def 1;
A84:for k being Nat st k in dom g1 & k+1 in dom g1 holds g1/.k <> g1/.(k+1)
    proof let k be Nat;assume A85:k in dom g1 & k+1 in dom g1;
        k<k+1 by NAT_1:38;
      then A86:g1.k<>g1.(k+1) by A2,A85,FUNCT_1:def 8;
        g1.k=g1/.k by A85,FINSEQ_4:def 4;
     hence thesis by A85,A86,FINSEQ_4:def 4;
    end;
     for k being Nat st k in dom g2 & k+1 in dom g2 holds g2/.k <> g2/.(k+1)
    proof let k be Nat;assume A87:k in dom g2 & k+1 in dom g2;
        k<k+1 by NAT_1:38;
      then A88:g2.k<>g2.(k+1) by A3,A87,FUNCT_1:def 8;
        g2.k=g2/.k by A87,FINSEQ_4:def 4;
     hence thesis by A87,A88,FINSEQ_4:def 4;
    end;
   then L~g1 meets L~g2 by A2,A3,A22,A43,A64,A83,A84,GOBOARD4:4;
then A89: L~g1 /\ L~g2 <> {} by XBOOLE_0:def 7;
     L~g1 /\ L~g2 c= L~f1 /\ L~f2 by A2,A3,XBOOLE_1:27;
   then L~f1 /\ L~f2 <> {} by A89,XBOOLE_1:3;
 hence thesis by XBOOLE_0:def 7;
end;

begin  :: NORM OF POINTS IN TOPREAL n

theorem Th31: for a,b,r1,r2 being Real
  st a<=r1 & r1<=b & a<=r2 & r2<=b holds
  abs(r1-r2)<=b-a
 proof let a,b,r1,r2 be Real;
  assume A1:a<=r1 & r1<=b & a<=r2 & r2<=b;
   per cases;
   suppose r1-r2>=0;
     then A2:abs(r1-r2)=r1-r2 by ABSVALUE:def 1;
     A3:r1-r2<=b-r2 by A1,REAL_1:49;
       b-r2<=b-a by A1,REAL_2:106;
    hence thesis by A2,A3,AXIOMS:22;
   suppose r1-r2<0;
     then A4:abs(r1-r2)=-(r1-r2) by ABSVALUE:def 1 .=r2-r1 by XCMPLX_1:143;
     A5:r2-r1<=b-r1 by A1,REAL_1:49;
       b-r1<=b-a by A1,REAL_2:106;
    hence thesis by A4,A5,AXIOMS:22;
 end;

definition let n;let p be Point of TOP-REAL n;
 redefine func |. p .| means
:Def5: for w being Element of REAL n st p=w holds it=|.w.|;
 compatibility
  proof let r be Real;
   thus r = |. p .| implies for w being Element of REAL n st p=w holds r=|.w.|
    by TOPRNS_1:def 6;
    reconsider y = p as Element of REAL n by EUCLID:25;
   assume for w being Element of REAL n st p=w holds r=|.w.|;
    then r=|.y.|;
   hence r = |. p .| by TOPRNS_1:def 6;
  end;
end;

reserve p,p1,p2 for Point of TOP-REAL n;

canceled 13;

theorem Th45: for x1,x2 being Point of Euclid n st x1=p1 & x2=p2 holds
 |.p1 - p2.| = dist(x1,x2)
 proof let x1,x2 be Point of Euclid n;
   assume A1:x1=p1 & x2=p2;
     Euclid n= MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
   then reconsider x1'=x1,x2'=x2 as Element of REAL n;
     p1-p2=x1'-x2' by A1,EUCLID:def 13;
   then |.p1-p2.|=|.x1'-x2'.| by Def5;
   then A2:(Pitag_dist n).(x1',x2')=|.p1-p2.| by EUCLID:def 6;
     Euclid n = MetrStruct(#REAL n,Pitag_dist n#) by EUCLID:def 7;
  hence thesis by A2,METRIC_1:def 1;
 end;

theorem Th46: for p being Point of TOP-REAL 2 holds
 (|.p.|)^2 = (p`1)^2+(p`2)^2
 proof let p be Point of TOP-REAL 2;
    reconsider w=p as Element of REAL 2 by EUCLID:25;
    A1:|.p.|=|.w.| by Def5;
    A2:|.w.| = sqrt Sum sqr w by EUCLID:def 5;
      0 <= Sum sqr w by RVSUM_1:116;
    then A3: (|.p.|)^2=Sum sqr w by A1,A2,SQUARE_1:def 4;
    A4: p`1=w.1 by EUCLID:def 14;
    A5: p`2=w.2 by EUCLID:def 15;
    A6:len sqr w =2 by FINSEQ_2:109;
    A7:(sqr w).1=(p`1)^2 by A4,RVSUM_1:78;
      (sqr w).2=(p`2)^2 by A5,RVSUM_1:78;
    then sqr w=<*(p`1)^2,(p`2)^2*> by A6,A7,FINSEQ_1:61;
  hence thesis by A3,RVSUM_1:107;
 end;

theorem Th47: for p being Point of TOP-REAL 2 holds
 |.p.| = sqrt((p`1)^2+(p`2)^2)
 proof let p be Point of TOP-REAL 2;
   A1:(|.p.|)^2= (p`1)^2+(p`2)^2 by Th46;
     |.p.| >=0 by TOPRNS_1:26;
  hence thesis by A1,SQUARE_1:89;
 end;

theorem Th48: for p being Point of TOP-REAL 2 holds |.p.|<=abs(p`1)+abs(p`2)
 proof let p be Point of TOP-REAL 2;
   A1:(|.p.|)^2= (p`1)^2+(p`2)^2 by Th46;
     |.p.| >=0 by TOPRNS_1:26;
   then sqrt((p`1)^2+(p`2)^2)=|.p.| by A1,SQUARE_1:89;
  hence thesis by Th2;
 end;

theorem Th49: for p1,p2 being Point of TOP-REAL 2 holds
       |.p1-p2.|<=abs(p1`1-p2`1)+abs(p1`2-p2`2)
proof let p1,p2 be Point of TOP-REAL 2;
    p1`1-p2`1=(p1-p2)`1 & p1`2-p2`2=(p1-p2)`2 by TOPREAL3:8;
 hence thesis by Th48;
end;

theorem Th50: for p being Point of TOP-REAL 2 holds
      abs(p`1)<=|.p.| & abs(p`2)<=|.p.|
 proof let p be Point of TOP-REAL 2;
     |.p.| = sqrt((p`1)^2+(p`2)^2) by Th47;
  hence thesis by Th3;
 end;

theorem Th51: for p1,p2 being Point of TOP-REAL 2 holds
      abs(p1`1-p2`1)<=|.p1-p2.| & abs(p1`2-p2`2)<=|.p1-p2.|
proof let p1,p2 be Point of TOP-REAL 2;
    p1`1-p2`1=(p1-p2)`1 & p1`2-p2`2=(p1-p2)`2 by TOPREAL3:8;
 hence thesis by Th50;
end;

theorem Th52:  p in LSeg(p1,p2) implies ex r st
  0<=r & r<=1 & p=(1-r)*p1+r*p2
 proof assume p in LSeg(p1,p2);
   then p in { (1-r)*p1 + r*p2 : 0 <= r & r <= 1 } by TOPREAL1:def 4;
  then consider r1 such that
  A1: p=(1-r1)*p1 + r1*p2 &( 0 <= r1 & r1 <= 1);
  thus thesis by A1;
 end;

theorem Th53:  p in LSeg(p1,p2) implies
 |.p-p1.|<=|.p1-p2.| & |.p-p2.|<=|.p1-p2.|
 proof assume A1:p in LSeg(p1,p2);
   then consider r such that
   A2: 0<=r & r<=1 & p=(1-r)*p1+r*p2 by Th52;
     p-p1= (1-r)*p1+r*p2+-p1 by A2,EUCLID:45
   .= (1-r)*p1+-p1+r*p2 by EUCLID:30
   .=(1-r)*p1-p1+r*p2 by EUCLID:45
   .=(1-r)*p1-1*p1+r*p2 by EUCLID:33
   .=(1-r-1)*p1+r*p2 by EUCLID:54
   .=(1+-r-1)*p1+r*p2 by XCMPLX_0:def 8
   .=(-r)*p1+r*p2 by XCMPLX_1:26
   .=r*p2+-r*p1 by EUCLID:44
   .=r*p2+r*(-p1) by EUCLID:44
   .=r*(p2+(-p1)) by EUCLID:36
   .=r*(p2-p1) by EUCLID:45;
   then |.p-p1.|=abs(r)*|.p2-p1.| by TOPRNS_1:8
   .=abs(r)*|.p1-p2.| by TOPRNS_1:28 .=r*|.p1-p2.| by A2,ABSVALUE:def 1;
   then A3:|.p1-p2.|- |.p-p1.|=1*|.p1-p2.|-r*|.p1-p2.|.=(1-r)*|.p1-p2.|
                          by XCMPLX_1:40;
   A4:0<=1-r by A2,SQUARE_1:12;
     |.p1-p2.|>=0 by TOPRNS_1:26;
then A5:|.p1-p2.|- |.p-p1.|>=0 by A3,A4,SQUARE_1:19;
   consider r such that
   A6: 0<=r & r<=1 & p=(1-r)*p2+r*p1 by A1,Th52;
     p-p2= (1-r)*p2+r*p1+-p2 by A6,EUCLID:45
   .= (1-r)*p2+-p2+r*p1 by EUCLID:30
   .=(1-r)*p2-p2+r*p1 by EUCLID:45
   .=(1-r)*p2-1*p2+r*p1 by EUCLID:33
   .=(1-r-1)*p2+r*p1 by EUCLID:54
   .=(1+-r-1)*p2+r*p1 by XCMPLX_0:def 8
   .=(-r)*p2+r*p1 by XCMPLX_1:26
   .=r*p1+-r*p2 by EUCLID:44
   .=r*p1+r*(-p2) by EUCLID:44
   .=r*(p1+(-p2)) by EUCLID:36
   .=r*(p1-p2) by EUCLID:45;
   then |.p-p2.|=abs(r)*|.p1-p2.| by TOPRNS_1:8
   .=r*|.p1-p2.| by A6,ABSVALUE:def 1;
   then A7:|.p1-p2.|- |.p-p2.|=1*|.p1-p2.|-r*|.p1-p2.|.=(1-r)*|.p1-p2.|
                          by XCMPLX_1:40;
   A8:0<=1-r by A6,SQUARE_1:12;
     |.p1-p2.|>=0 by TOPRNS_1:26;
   then |.p1-p2.|- |.p-p2.|>=0 by A7,A8,SQUARE_1:19;
  hence thesis by A5,REAL_2:105;
 end;

begin ::  EXTENDED GOBOARD THEOREM AND FASHODA MEET THEOREM

reserve M for non empty MetrSpace;

theorem Th54: for P,Q being Subset of TopSpaceMetr(M) st
   P <> {} & P is compact & Q <> {} & Q is compact holds
   min_dist_min(P,Q)>=0
 proof let P,Q be Subset of TopSpaceMetr(M);
   assume P <> {} & P is compact & Q <> {} & Q is compact;
   then consider x1,x2 being Point of M such that
   A1:x1 in P & x2 in Q &
    dist(x1,x2) = min_dist_min(P,Q) by WEIERSTR:36;
  thus thesis by A1,METRIC_1:5;
 end;

theorem Th55: for P,Q being Subset of TopSpaceMetr(M) st
   P <> {} & P is compact & Q <> {} & Q is compact holds
   P misses Q iff min_dist_min(P,Q)>0
 proof let P,Q be Subset of TopSpaceMetr(M);
  assume A1:P <> {} & P is compact & Q <> {} & Q is compact;
   then consider x1,x2 being Point of M such that
   A2:x1 in P & x2 in Q &
    dist(x1,x2) = min_dist_min(P,Q) by WEIERSTR:36;
A3: the distance of M is discerning by METRIC_1:def 8;
A4: now assume not min_dist_min(P,Q)>0;
      then dist(x1,x2)=0 by A1,A2,Th54;
      then (the distance of M).(x1,x2)=0 by METRIC_1:def 1;
      then x1=x2 by A3,METRIC_1:def 4;
     hence P /\ Q <> {} by A2,XBOOLE_0:def 3;
    end;
      now assume A5:P /\ Q <>{};
      consider p being Element of P /\ Q;
      A6:p in P & p in Q by A5,XBOOLE_0:def 3;
      then reconsider p'=p as Element of TopSpaceMetr(M);
      reconsider q=p' as Point of M by TOPMETR:16;
        the distance of M is Reflexive by METRIC_1:def 7;
      then (the distance of M).(q,q)=0 by METRIC_1:def 3;
      then dist(q,q)=0 by METRIC_1:def 1;
     hence not min_dist_min(P,Q)>0 by A1,A6,WEIERSTR:40;
    end;
  hence thesis by A4,XBOOLE_0:def 7;
 end;

::  Approximation of finite sequence by special finite sequence
theorem Th56: for f being FinSequence of TOP-REAL 2,a,c,d being Real st
 1<=len f & X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) &
 Y_axis(f) lies_between c, d & a>0 &
 (for i st 1<=i & i+1<=len f holds
 |. f/.i-f/.(i+1) .|<a)
 holds
 ex g being FinSequence of TOP-REAL 2 st g is special &
 g.1=f.1 & g.len g=f.len f & len g>=len f &
 X_axis(g) lies_between (X_axis(f)).1, (X_axis(f)).(len f) &
 Y_axis(g) lies_between c, d &
 (for j st j in dom g holds ex k st k in dom f & |. g/.j - f/.k .|<a)&
 (for j st 1<=j & j+1<=len g holds |. g/.j - g/.(j+1) .|<a)
 proof let f be FinSequence of TOP-REAL 2,a,c,d be Real;
  assume A1:1<=len f &
    X_axis(f) lies_between (X_axis(f)).1, (X_axis(f)).(len f) &
   Y_axis(f) lies_between c, d & a>0 &
   (for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|<a);
   defpred P[set,set] means
   (for j st $1=2*j or $1=2*j -'1 holds
   ($1 =2*j implies $2=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &($1 =2*j-'1 implies $2=f/.j));
   A2: for k st k in Seg (2*(len f)-'1)
     ex x st P[k,x]
    proof let k;assume
A3:   k in Seg (2*(len f)-'1);
      then A4:1<=k & k<=(2*(len f)-'1) by FINSEQ_1:3;
      per cases by GROUP_4:100;
      suppose A5:k mod 2=0;
       consider i such that
       A6: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
         for j st k=2*j or k=2*j -'1 holds
        (k =2*j implies |[(f/.i)`1,(f/.(i+1))`2]|
             =|[(f/.j)`1,(f/.(j+1))`2]|)
          &(k =2*j-'1 implies |[(f/.i)`1,(f/.(i+1))`2]|=f/.j)
       proof let j;assume A7:k=2*j or k=2*j -'1;
         per cases by A7;
         suppose k=2*j;
          then i=2*j/2 by A5,A6,XCMPLX_1:90;
then A8:       i=j by XCMPLX_1:90;
            now assume
            A9:k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
             then A10:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by
XCMPLX_1:40
             .=2*(j-1)+1+1-1 by XCMPLX_1:1
             .=2*(j-1)+1 by XCMPLX_1:26;
               now assume A11:j=0;
                0-1<0; then 0-'1=0 by BINARITH:def 3;
              hence contradiction by A3,A9,A11,FINSEQ_1:3;
             end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
             then k= 2*(j-'1)+1 & 1<=2 by A10,SCMFSA_7:3;
            hence contradiction by A5,NAT_1:def 2;
           end;
          hence thesis by A8;
         suppose A12:k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
          then A13:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:
40
          .=2*(j-1)+1+1-1 by XCMPLX_1:1
          .=2*(j-1)+1 by XCMPLX_1:26;
            now assume A14:j=0;
              0-1<0; then 0-'1=0 by BINARITH:def 3;
           hence contradiction by A3,A12,A14,FINSEQ_1:3;
          end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
          then k= 2*(j-'1)+1 & 1<=2 by A13,SCMFSA_7:3;
          hence thesis by A5,NAT_1:def 2;
       end;
       hence thesis;
      suppose A15:k mod 2=1;
       consider i such that
       A16: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
         for j st k=2*j or k=2*j -'1 holds
        (k =2*j implies f/.(i+1)=|[(f/.j)`1,(f/.(j+1))`2]|)
          &(k =2*j-'1 implies f/.(i+1)=f/.j)
       proof let j;assume A17:k=2*j or k=2*j -'1;
         per cases by A17;
         suppose k=2*j-'1;
          then A18:k=2*j-1 by A4,JORDAN3:1;
          A19:now assume
              k=2*j-'1;
            then k=2*j-1 by A4,JORDAN3:1;
            then k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:40
            .=2*(j-1)+1+1-1 by XCMPLX_1:1
            .=2*(j-1)+1 by XCMPLX_1:26;
            then 2*(j-1)=2*i+1-1 by A15,A16,XCMPLX_1:26;
            then 2*(j-1)/2=2*i/2 by XCMPLX_1:26;
            then (j-1)=2*i/2 by XCMPLX_1:90;
            then j-1+1=i+1 by XCMPLX_1:90;
           hence f/.(i+1)=f/.j by XCMPLX_1:27;
          end;
            now assume k=2*j;
            then k-k=1 by A18,XCMPLX_1:18;
           hence contradiction by XCMPLX_1:14;
          end;
          hence thesis by A19;
         suppose k=2*j;
           then 2*j-2*i=1 by A15,A16,XCMPLX_1:26;
           then A20:2*(j-i)=1 by XCMPLX_1:40;
           then j-i>=0 by SQUARE_1:24;
           then A21:j-i=j-'i by BINARITH:def 3;
             j-i=0 or j-i>0 by A20,SQUARE_1:24;
           then j-i>=0+1 by A20,A21,NAT_1:38;
          then 2*(j-i)>=2*1 by AXIOMS:25;
          hence thesis by A20;
      end;
     hence thesis;
    end;
   A22:for k being Nat,y1,y2 being set st k in Seg (2*(len f)-'1) &
   P[k,y1] & P[k,y2] holds y1=y2
    proof let k be Nat,y1,y2 be set;
      assume A23: k in Seg (2*(len f)-'1) &
       (for j st k=2*j or k=2*j -'1 holds
        (k =2*j implies y1=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &(k =2*j-'1 implies y1=f/.j))&
       (for j st k=2*j or k=2*j -'1 holds
         (k =2*j implies y2=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &(k =2*j-'1 implies y2=f/.j));
      per cases by GROUP_4:100;
      suppose A24:k mod 2=0;
       consider i such that
       A25: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
        y1=|[(f/.i)`1,(f/.(i+1))`2]| by A23,A24,A25;
      hence thesis by A23,A24,A25;
     suppose A26:k mod 2=1;
       consider i such that
       A27: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
         k=2*i+2*1-(1+1)+1 by A26,A27,XCMPLX_1:26
       .=2*(i+1)-(1+1)+1 by XCMPLX_1:8
       .=2*(i+1)+1-(1+1) by XCMPLX_1:29
       .=2*(i+1)+1-1-1 by XCMPLX_1:36;
       then A28:k=2*(i+1)-1 by XCMPLX_1:26;
         1<=1+i by NAT_1:37;
       then 2*1<=2*(i+1) by AXIOMS:25;
       then 1<=2*(i+1) by AXIOMS:22;
       then A29:2*(i+1)-'1= 2*(i+1)-1 by SCMFSA_7:3;
       then y1=f/.(i+1) by A23,A28;
      hence thesis by A23,A28,A29;
    end;
     ex p being FinSequence st dom p = Seg (2*(len f)-'1)
      & for k st k in Seg (2*(len f)-'1) holds
   P[k,p.k] from SeqEx(A22,A2);
   then consider p being FinSequence such that
   A30: dom p = Seg (2*(len f)-'1)
      & for k st k in Seg (2*(len f)-'1) holds
   (for j st k=2*j or k=2*j -'1 holds
   (k =2*j implies p.k=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &(k =2*j-'1 implies p.k=f/.j));
    A31:len p=(2*(len f)-'1) by A30,FINSEQ_1:def 3;
     rng p c= the carrier of TOP-REAL 2
    proof let y;assume y in rng p;
      then consider x such that
      A32:x in dom p & y=p.x by FUNCT_1:def 5;
      A33:x in Seg len p by A32,FINSEQ_1:def 3;
      reconsider i=x as Nat by A32;
      A34:1 <= i & i <= len p by A33,FINSEQ_1:3;
      per cases by GROUP_4:100;
      suppose A35:i mod 2=0;
        consider j such that
        A36: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          p.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A32,A35,A36;
       hence thesis by A32;
      suppose A37:i mod 2=1;
        consider j such that
        A38: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A37,A38,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A39:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A34,JORDAN3:1;
        then p.i=f/.(j+1) by A30,A32,A39;
       hence thesis by A32;
    end;
   then reconsider g1=p as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
     for i st 1 <= i & i+1 <= len g1 holds
    (g1/.i)`1 = (g1/.(i+1))`1 or (g1/.i)`2 = (g1/.(i+1))`2
    proof let i;assume A40:1 <= i & i+1 <= len g1;
      then A41:i<len g1 by NAT_1:38;
      A42:1<i+1 by A40,NAT_1:38;
      then A43:i+1 in Seg len g1 by A40,FINSEQ_1:3;
A44:    i in Seg (2*(len f)-'1) by A31,A40,A41,FINSEQ_1:3;
      A45:g1.i=g1/.i by A40,A41,FINSEQ_4:24;
      A46:g1.(i+1)=g1/.(i+1) by A40,A42,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A47:i mod 2=0;
        consider j such that
        A48: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
        A49:g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A44,A47,A48;
          i+1=2*j+1+1-1 by A47,A48,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A50:i+1=2*(j+1)-1 by XCMPLX_1:8;
          1<=1+i by NAT_1:29;
        then 2*(j+1)-'1 =2*(j+1)-1 by A50,JORDAN3:1;
        then g1.(i+1)=f/.(j+1) by A30,A31,A43,A50;
       hence thesis by A45,A46,A49,EUCLID:56;
      suppose A51:i mod 2=1;
        consider j such that
        A52: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A51,A52,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A53:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A40,JORDAN3:1;
        then A54: g1.i=f/.(j+1) by A30,A44,A53;
          i+1=2*j+(1+1) by A51,A52,XCMPLX_1:1
        .=2*j+2*1
        .=2*(j+1) by XCMPLX_1:8;
        then g1.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A31,A43;
       hence thesis by A45,A46,A54,EUCLID:56;
    end;
   then A55:g1 is special by TOPREAL1:def 7;
    A56:f.len f=f/.len f by A1,FINSEQ_4:24;
A57: 2*(len f)>=2*1 by A1,AXIOMS:25;
    then 2*(len f)>=1 by AXIOMS:22;
    then A58:2*(len f)-'1= 2*(len f)-1 by SCMFSA_7:3;
A59:2*(len f)-1>= 1+1-1 by A57,REAL_1:49;
then A60: 1 in Seg (2*(len f)-'1) by A58,FINSEQ_1:3;
      2*1-'1=1+1-'1 .=1 by BINARITH:39;
    then p.1=f/.1 by A30,A60;
   then A61:g1.1=f.1 by A1,FINSEQ_4:24;
  (2*(len f)-'1) in Seg (2*(len f)-'1) by A58,A59,FINSEQ_1:3;
   then A62:g1.len g1=f.len f by A30,A31,A56;
      len f + len f>=len f+1 by A1,AXIOMS:24;
    then 2*(len f)>=len f +1 by XCMPLX_1:11;
    then 2*(len f)-1>=len f +1-1 by REAL_1:49;
   then A63:len g1>=len f by A31,A58,XCMPLX_1:26;
     for i st i in dom (X_axis(g1)) holds (X_axis(f)).1 <= (X_axis(g1)).i
         & (X_axis(g1)).i <= (X_axis(f)).(len f)
    proof let i;assume
      A64:i in dom (X_axis(g1));
then A65:   i in Seg len (X_axis(g1)) by FINSEQ_1:def 3;
      then i in Seg len g1 by GOBOARD1:def 3;
      then A66: 1<=i & i<=len g1 by FINSEQ_1:3;
      A67:i in Seg len g1 by A65,GOBOARD1:def 3;
      A68:(X_axis(g1)).i = (g1/.i)`1 by A64,GOBOARD1:def 3;
      A69:len (X_axis(f))=len f by GOBOARD1:def 3;
      A70:g1/.i=(g1.i) by A66,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A71:i mod 2=0;
        consider j such that
        A72: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A67,A71,A72;
        then A73:(g1/.i)`1=(f/.j)`1 by A70,EUCLID:56;
          j<>0 by A65,A71,A72,FINSEQ_1:3;
        then j>0 by NAT_1:19;
then A74:     j>=0+1 by NAT_1:38;
           2*j+1<=2*(len f)-1+1 by A31,A58,A66,A71,A72,AXIOMS:24;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
        then j in Seg len f by A74,FINSEQ_1:3;
        then A75:j in dom (X_axis(f)) by A69,FINSEQ_1:def 3;
        then (X_axis(f)).j = (f/.j)`1 by GOBOARD1:def 3;
       hence thesis by A1,A68,A73,A75,GOBOARD4:def 1;
      suppose A76:i mod 2=1;
        consider j such that
        A77: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A76,A77,XCMPLX_1:26;
        then i=2*j+(1+1)-1 by XCMPLX_1:1;
        then i=2*j+2*1-1;
        then A78:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A66,JORDAN3:1;
        then A79:(g1/.i)`1=(f/.(j+1))`1 by A30,A31,A67,A70,A78;
        A80:1<=j+1 by NAT_1:29;
           2*j+1<=2*(len f)-1+1 by A31,A58,A66,A76,A77,NAT_1:38;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then j+1 in Seg len f by A80,FINSEQ_1:3;
        then A81:j+1 in dom (X_axis(f)) by A69,FINSEQ_1:def 3;
        then (X_axis(f)).(j+1) = (f/.(j+1))`1 by GOBOARD1:def 3;
       hence thesis by A1,A68,A79,A81,GOBOARD4:def 1;
    end;
   then A82:X_axis(g1) lies_between (X_axis(f)).1, (X_axis(f)).(len f)
                             by GOBOARD4:def 1;
     for i st i in dom (Y_axis(g1)) holds
    c <= (Y_axis(g1)).i & (Y_axis(g1)).i <= d
   proof let i;assume
      A83:i in dom (Y_axis(g1));
then A84:   i in Seg len (Y_axis(g1)) by FINSEQ_1:def 3;
      then i in Seg len g1 by GOBOARD1:def 4;
      then A85: 1<=i & i<=len g1 by FINSEQ_1:3;
      A86:i in Seg len g1 by A84,GOBOARD1:def 4;
      A87:(Y_axis(g1)).i = (g1/.i)`2 by A83,GOBOARD1:def 4;
      A88:len (Y_axis(f))=len f by GOBOARD1:def 4;
      A89:g1/.i=(g1.i) by A85,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A90:i mod 2=0;
        consider j such that
        A91: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A86,A90,A91;
        then A92:(g1/.i)`2=(f/.(j+1))`2 by A89,EUCLID:56;
        A93:1<=j+1 by NAT_1:29;
           2*j+1<=2*(len f)-1+1 by A31,A58,A85,A90,A91,AXIOMS:24;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then j+1 in Seg len f by A93,FINSEQ_1:3;
        then A94:j+1 in dom (Y_axis(f)) by A88,FINSEQ_1:def 3;
        then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
       hence thesis by A1,A87,A92,A94,GOBOARD4:def 1;
      suppose A95:i mod 2=1;
        consider j such that
        A96: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A95,A96,XCMPLX_1:26;
        then i=2*j+(1+1)-1 by XCMPLX_1:1;
        then i=2*j+2*1-1;
        then A97:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A85,JORDAN3:1;
        then A98:(g1/.i)`2=(f/.(j+1))`2 by A30,A31,A86,A89,A97;
        A99:1<=j+1 by NAT_1:29;
           2*j+1<=2*(len f)-1+1 by A31,A58,A85,A95,A96,NAT_1:38;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then j+1 in Seg len f by A99,FINSEQ_1:3;
         then A100:j+1 in dom (Y_axis(f)) by A88,FINSEQ_1:def 3;
        then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
       hence thesis by A1,A87,A98,A100,GOBOARD4:def 1;
   end;
   then A101:Y_axis(g1) lies_between c, d by GOBOARD4:def 1;
   A102:for i st i in dom g1 holds
   ex k st k in dom f & |. g1/.i - f/.k .| < a
    proof let i;assume A103:i in dom g1;
then A104:   i in Seg len g1 by FINSEQ_1:def 3;
      then A105:1<=i & i<=len g1 by FINSEQ_1:3;
      then A106:g1.i=g1/.i by FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A107:i mod 2=0;
        consider j such that
        A108: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
        A109:g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A103,A107,A108;
        then A110:(g1/.i)`1=(f/.j)`1 by A106,EUCLID:56;
        A111:(g1/.i)`2=(f/.(j+1))`2 by A106,A109,EUCLID:56;
        A112:g1/.i-f/.j=|[(g1/.i)`1-(f/.j)`1,(g1/.i)`2-(
          (f/.j))`2]| by EUCLID:65
                .=|[0,(g1/.i)`2-(f/.j)`2]| by A110,XCMPLX_1:14;
        then (g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2 by EUCLID:56;
        then |.g1/.i-f/.j.|=
          sqrt(((g1/.i-f/.j)`1)^2+((g1/.i)`2-(f/.j)`2)^2)
                        by Th47
         .= sqrt(0+(((f/.(j+1))`2-(f/.j)`2))^2) by A111,A112,EUCLID:56,SQUARE_1
:60
         .= sqrt((((f/.(j+1))`2-(f/.j)`2))^2);
        then |.g1/.i-f/.j.|=abs((f/.(j+1))`2-(f/.j)`2) by SQUARE_1:91
                      .=abs((f/.j)`2 -(f/.(j+1))`2) by UNIFORM1:13;
        then A113:|.g1/.i-f/.j.|
        <=|.f/.j-f/.(j+1).| by Th51;
          j<>0 by A104,A107,A108,FINSEQ_1:3;
        then j>0 by NAT_1:19;
        then A114:  j>=0+1 by NAT_1:38;
           2*j+1<=2*(len f)-1+1 by A31,A58,A105,A107,A108,AXIOMS:24;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
        then A115: j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then |. f/.j-f/.(j+1) .|<a by A1,A114;
        then A116: |. g1/.i - f/.j .|<a by A113,AXIOMS:22;
          j in dom f by A114,A115,FINSEQ_3:27;
       hence thesis by A116;
      suppose A117:i mod 2=1;
        consider j such that
        A118: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A117,A118,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A119:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A105,JORDAN3:1;
        then g1.i=f/.(j+1) by A30,A103,A119;
        then A120:|.g1/.i-f/.(j+1).|=|.0.REAL 2.| by A106,EUCLID:46
             .=0 by TOPRNS_1:24;
           2*j+1+1<=2*(len f)-1+1 by A31,A58,A105,A117,A118,AXIOMS:24;
         then 2*j+1+1<=2*(len f) by XCMPLX_1:27;
         then 2*j+1<2*(len f) by NAT_1:38;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
        then A121: j+1<=len f by NAT_1:38;
          1<=j+1 by NAT_1:29;
        then j+1 in dom f by A121,FINSEQ_3:27;
       hence thesis by A1,A120;
    end;
     for i st 1<=i & i+1<=len g1 holds |. g1/.i - g1/.(i+1) .|<a
    proof let i;assume A122:1<=i & i+1<=len g1;
      then i<=len g1 by NAT_1:38;
      then A123:i in Seg len g1 by A122,FINSEQ_1:3;
      A124:1<=i & i<=len g1 by A122,NAT_1:38;
      A125:1<=i+1 by NAT_1:29;
then A126:    i+1 in Seg (2*(len f)-'1) by A31,A122,FINSEQ_1:3;
      A127:g1.(i+1)=g1/.(i+1) by A122,A125,FINSEQ_4:24;
      A128:g1.i=g1/.i by A124,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A129:i mod 2=0;
        consider j such that
        A130: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
        A131:g1.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A123,A129,A130;
          i+1=2*j+1+1-1 by A129,A130,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A132:i+1=2*(j+1)-1 by XCMPLX_1:8;
          1<=1+i by NAT_1:29;
        then 2*(j+1)-'1 =2*(j+1)-1 by A132,JORDAN3:1;
        then A133:g1.(i+1)=f/.(j+1) by A30,A126,A132;
        A134:(g1/.i)`1=(f/.j)`1 by A128,A131,EUCLID:56;
        A135:(g1/.i)`2=(f/.(j+1))`2 by A128,A131,EUCLID:56;
        A136:(g1/.(i+1))`1=(f/.(j+1))`1 by A122,A125,A133,FINSEQ_4:24;
        A137:(g1/.(i+1))`2=(f/.(j+1))`2 by A122,A125,A133,FINSEQ_4:24;
        A138:g1/.i-g1/.(i+1)
        =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]|
                                 by EUCLID:65
                .=|[(f/.j)`1-(f/.(j+1))`1,0]|
                         by A134,A135,A136,A137,XCMPLX_1:14;
        then A139:(g1/.i-g1/.(i+1))`1=(f/.j)`1-(f/.(j+1))`1 by EUCLID:56;
         |.g1/.i-g1/.(i+1).|=
          sqrt((((g1/.i-g1/.(i+1))`1))^2+(((g1/.i-g1/.(i+1))`2))^2)
                        by Th47
         .= sqrt((((f/.j)`1-(f/.(j+1))`1))^2+0) by A138,A139,EUCLID:56,SQUARE_1
:60
         .= sqrt((((f/.j)`1-(f/.(j+1))`1))^2);
        then |.g1/.i-g1/.(i+1).|=abs((f/.j)`1-(f/.(j+1))`1)
                               by SQUARE_1:91;
        then A140:|.g1/.i-g1/.(i+1).|
        <=|.f/.j-f/.(j+1).| by Th51;
          j<>0 by A122,A129,A130;
        then j>0 by NAT_1:19;
        then A141:  j>=0+1 by NAT_1:38;
           2*j+1<=2*(len f)-1+1 by A31,A58,A122,A129,A130,NAT_1:38;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then |. f/.j-f/.(j+1) .|<a by A1,A141;
        hence thesis by A140,AXIOMS:22;
      suppose A142:i mod 2=1;
        consider j such that
        A143: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A142,A143,XCMPLX_1:26;
        then i=2*j+(1+1)-1 by XCMPLX_1:1;
        then i=2*j+2*1-1;
        then A144:i=2*(j+1)-1 by XCMPLX_1:8;
        then A145:   2*(j+1)-'1 =2*(j+1)-1 by A122,JORDAN3:1;
          i+1=2*j+(1+1) by A142,A143,XCMPLX_1:1
        .=2*j+2*1;
        then A146:i+1=2*(j+1) by XCMPLX_1:8;
        then A147:g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A126,A127;
        then A148:(g1/.(i+1))`1=(f/.(j+1))`1 by EUCLID:56;
        A149:(g1/.(i+1))`2=(f/.(j+1+1))`2 by A147,EUCLID:56;
        A150:(g1/.i)`1=(f/.(j+1))`1 by A30,A31,A123,A128,A144,A145;
        A151:(g1/.i)`2=(f/.(j+1))`2 by A30,A31,A123,A128,A144,A145;
        A152:g1/.i-g1/.(i+1)
        =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]| by EUCLID:65
                .=|[0,(f/.(j+1))`2-(f/.(j+1+1))`2]|
                         by A148,A149,A150,A151,XCMPLX_1:14;
        then A153:(g1/.i-g1/.(i+1))`1=0 by EUCLID:56;
         |.g1/.i-g1/.(i+1).|=
          sqrt((((g1/.i-g1/.(i+1))`1))^2+(((g1/.i-
           g1/.(i+1))`2))^2) by Th47
         .= sqrt((((f/.(j+1))`2-(f/.(j+1+1))`2))^2) by A152,A153,EUCLID:56,
SQUARE_1:60;
        then |.g1/.i-g1/.(i+1).|=abs((f/.(j+1))`2-(f/.(j+1+1))`2)
                              by SQUARE_1:91;
        then A154:|.g1/.i-g1/.(i+1).|
        <=|.f/.(j+1)-f/.(j+1+1).| by Th51;
        A155:  j+1>=1 by NAT_1:29;
           2*(j+1)+1<=2*(len f)-1+1 by A31,A58,A122,A146,AXIOMS:24;
         then 2*(j+1)+1<=2*(len f) by XCMPLX_1:27;
         then 2*(j+1)<2*(len f) by NAT_1:38;
         then 2*(j+1)/2<2*(len f)/2 by REAL_1:73;
         then (j+1)<2*(len f)/2 by XCMPLX_1:90;
         then (j+1)<len f by XCMPLX_1:90;
         then (j+1)+1<=len f by NAT_1:38;
         then |. f/.(j+1)-f/.(j+1+1) .|<a by A1,A155;
       hence thesis by A154,AXIOMS:22;
    end;
  hence thesis by A55,A61,A62,A63,A82,A101,A102;
 end;

theorem Th57: for f being FinSequence of TOP-REAL 2,a,c,d being Real st
 1<=len f &
 Y_axis(f) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) &
 X_axis(f) lies_between c, d & a>0 &
 (for i st 1<=i & i+1<=len f holds |. (f/.i)-(f/.(i+1)) .|<a)
 holds
 ex g being FinSequence of TOP-REAL 2 st g is special &
 g.1=f.1 & g.len g=f.len f & len g>=len f &
 Y_axis(g) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) &
 X_axis(g) lies_between c, d &
 (for j st j in dom g holds ex k st k in dom f & |. g/.j - f/.k .| < a)&
 (for j st 1<=j & j+1<=len g holds |. g/.j - g/.(j+1) .|<a)
 proof let f be FinSequence of TOP-REAL 2,a,c,d be Real;
  assume A1:1<=len f &
    Y_axis(f) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f) &
   X_axis(f) lies_between c, d & a>0 &
   (for i st 1<=i & i+1<=len f holds |. f/.i-f/.(i+1) .|<a);
defpred P[set,set] means
   (for j st $1=2*j or $1=2*j -'1 holds
   ($1 =2*j implies $2=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &($1 =2*j-'1 implies $2=f/.j));
A2: for k st k in Seg (2*(len f)-'1) ex x st P[k,x]
    proof let k;assume
      A3: k in Seg (2*(len f)-'1);
      then A4:1<=k & k<=2*(len f)-'1 by FINSEQ_1:3;
      per cases by GROUP_4:100;
      suppose A5:k mod 2=0;
       consider i such that
       A6: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
         for j st k=2*j or k=2*j -'1 holds
        (k =2*j implies |[(f/.i)`1,(f/.(i+1))`2]|
           =|[(f/.j)`1,(f/.(j+1))`2]|)
          &(k =2*j-'1 implies |[(f/.i)`1,(f/.(i+1))`2]|=f/.j)
       proof let j;assume A7:k=2*j or k=2*j -'1;
         per cases by A7;
         suppose k=2*j;
          then i=2*j/2 by A5,A6,XCMPLX_1:90;
then A8:       i=j by XCMPLX_1:90;
            now assume
            A9:k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
             then A10:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by
XCMPLX_1:40
             .=2*(j-1)+1+1-1 by XCMPLX_1:1
             .=2*(j-1)+1 by XCMPLX_1:26;
               now assume A11:j=0;
                0-1<0; then 0-'1=0 by BINARITH:def 3;
              hence contradiction by A3,A9,A11,FINSEQ_1:3;
             end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
             then k= 2*(j-'1)+1 & 1<=2 by A10,SCMFSA_7:3;
            hence contradiction by A5,NAT_1:def 2;
           end;
          hence thesis by A8;
         suppose A12:
          k=2*j-'1; then k=2*j-1 by A4,JORDAN3:1;
          then A13:k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:
40
          .=2*(j-1)+1+1-1 by XCMPLX_1:1
          .=2*(j-1)+1 by XCMPLX_1:26;
            now assume A14:j=0;
              0-1<0; then 0-'1=0 by BINARITH:def 3;
           hence contradiction by A3,A12,A14,FINSEQ_1:3;
          end; then j>0 by NAT_1:19; then j>=0+1 by NAT_1:38;
          then j-'1=j-1 by SCMFSA_7:3;
          hence thesis by A5,A13,NAT_1:def 2;
       end;
       hence thesis;
      suppose A15:k mod 2=1;
       consider i such that
       A16: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
         for j st k=2*j or k=2*j -'1 holds
        (k =2*j implies f/.(i+1)=|[(f/.j)`1,(f/.(j+1))`2]|)
          &(k =2*j-'1 implies f/.(i+1)=f/.j)
       proof let j;assume A17:k=2*j or k=2*j -'1;
         per cases by A17;
         suppose k=2*j-'1;
          then A18:k=2*j-1 by A4,JORDAN3:1;
          A19:now assume
              k=2*j-'1;
            then k=2*j-1 by A4,JORDAN3:1;
            then k=2*j-2*1+2-1 by XCMPLX_1:27 .=2*(j-1)+(1+1)-1 by XCMPLX_1:40
            .=2*(j-1)+1+1-1 by XCMPLX_1:1
            .=2*(j-1)+1 by XCMPLX_1:26;
            then 2*(j-1)=2*i+1-1 by A15,A16,XCMPLX_1:26;
            then 2*(j-1)/2=2*i/2 by XCMPLX_1:26;
            then (j-1)=2*i/2 by XCMPLX_1:90;
            then (j-1)=i by XCMPLX_1:90;
           hence f/.(i+1)=f/.j by XCMPLX_1:27;
          end;
            now assume k=2*j;
            then k-k=1 by A18,XCMPLX_1:18;
           hence contradiction by XCMPLX_1:14;
          end;
          hence thesis by A19;
         suppose k=2*j;
           then 2*j-2*i=1 by A15,A16,XCMPLX_1:26;
           then A20:2*(j-i)=1 by XCMPLX_1:40;
           then j-i>=0 by SQUARE_1:24;
           then A21:j-i=j-'i by BINARITH:def 3;
             j-i=0 or j-i>0 by A20,SQUARE_1:24;
           then j-i>=0+1 by A20,A21,NAT_1:38;
          then 2*(j-i)>=2*1 by AXIOMS:25;
          hence thesis by A20;
       end;
       hence thesis;
    end;
   A22:for k being Nat,y1,y2 being set st k in Seg (2*(len f)-'1) &
   P[k,y1] & P[k,y2] holds y1=y2
    proof let k be Nat,y1,y2 be set;
      assume A23: k in Seg (2*(len f)-'1) &
       (for j st k=2*j or k=2*j -'1 holds
        (k =2*j implies y1=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &(k =2*j-'1 implies y1=f/.j))&
       (for j st k=2*j or k=2*j -'1 holds
         (k =2*j implies y2=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &(k =2*j-'1 implies y2=f/.j));
      per cases by GROUP_4:100;
      suppose A24:k mod 2=0;
       consider i such that
       A25: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
         y1=|[(f/.i)`1,(f/.(i+1))`2]| by A23,A24,A25;
      hence thesis by A23,A24,A25;
     suppose A26:k mod 2=1;
       consider i such that
       A27: k=2*i+ (k mod 2) & k mod 2<2 by NAT_1:def 2;
A28:   k=2*i+2*1-(1+1)+1 by A26,A27,XCMPLX_1:26
       .=2*(i+1)-(1+1)+1 by XCMPLX_1:8
       .=2*(i+1)+1-(1+1) by XCMPLX_1:29
       .=2*(i+1)+1-1-1 by XCMPLX_1:36
       .=2*(i+1)-1 by XCMPLX_1:26;
         1<=1+i by NAT_1:37;
       then 2*1<=2*(i+1) by AXIOMS:25;
       then 1<=2*(i+1) by AXIOMS:22;
       then A29:2*(i+1)-'1= 2*(i+1)-1 by SCMFSA_7:3;
       then y1=f/.(i+1) by A23,A28;
      hence thesis by A23,A28,A29;
    end;
     ex p being FinSequence st dom p = Seg (2*(len f)-'1)
      & for k st k in Seg (2*(len f)-'1) holds P[k,p.k] from SeqEx(A22,A2);
   then consider p being FinSequence such that
   A30: dom p = Seg (2*(len f)-'1)
      & for k st k in Seg (2*(len f)-'1) holds
   (for j st k=2*j or k=2*j -'1 holds
   (k =2*j implies p.k=|[(f/.j)`1,(f/.(j+1))`2]|)
                     &(k =2*j-'1 implies p.k=f/.j));
    A31:len p=(2*(len f)-'1) by A30,FINSEQ_1:def 3;
     rng p c= the carrier of TOP-REAL 2
    proof let y;assume y in rng p;
      then consider x such that
      A32:x in dom p & y=p.x by FUNCT_1:def 5;
      A33:x in Seg len p by A32,FINSEQ_1:def 3;
      reconsider i=x as Nat by A32;
      A34:1 <= i & i <= len p by A33,FINSEQ_1:3;
      per cases by GROUP_4:100;
      suppose A35:i mod 2=0;
        consider j such that
        A36: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          p.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A32,A35,A36;
       hence thesis by A32;
      suppose A37:i mod 2=1;
        consider j such that
        A38: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
A39:    i=2*j+1+1-1 by A37,A38,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1
        .=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-1=2*(j+1)-'1 by A34,JORDAN3:1;
        then p.i=f/.(j+1) by A30,A32,A39;
       hence thesis by A32;
    end;
   then reconsider g1=p as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
     for i st 1 <= i & i+1 <= len g1 holds
    (g1/.i)`1 = (g1/.(i+1))`1 or (g1/.i)`2 = (g1/.(i+1))`2
    proof let i;assume A40:1 <= i & i+1 <= len g1;
      then A41:i<len g1 by NAT_1:38;
      A42:1<i+1 by A40,NAT_1:38;
      then A43:i+1 in Seg len g1 by A40,FINSEQ_1:3;
A44:  i in Seg (2*(len f)-'1) by A31,A40,A41,FINSEQ_1:3;
      A45:g1.i=g1/.i by A40,A41,FINSEQ_4:24;
      A46:g1/.(i+1)=g1.(i+1) by A40,A42,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A47:i mod 2=0;
        consider j such that
        A48: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
        A49:g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A44,A45,A47,A48;
A50:    i+1=2*j+1+1-1 by A47,A48,XCMPLX_1:26
          .=2*j+(1+1)-1 by XCMPLX_1:1
          .=2*j+2*1-1
          .=2*(j+1)-1 by XCMPLX_1:8;
          1<=1+i by NAT_1:29;
        then 2*(j+1)-'1 =2*(j+1)-1 by A50,JORDAN3:1;
        then g1/.(i+1)=f/.(j+1) by A30,A31,A43,A46,A50;
       hence thesis by A49,EUCLID:56;
      suppose A51:i mod 2=1;
        consider j such that
        A52: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A51,A52,XCMPLX_1:26;
        then i=2*j+(1+1)-1 by XCMPLX_1:1;
        then i=2*j+2*1-1;
        then A53:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A40,JORDAN3:1;
        then A54:g1/.i=f/.(j+1) by A30,A44,A45,A53;
          i+1=2*j+(1+1) by A51,A52,XCMPLX_1:1
          .=2*j+2*1
          .=2*(j+1) by XCMPLX_1:8;
        then g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A31,A43,A46;
       hence thesis by A54,EUCLID:56;
    end;
   then A55:g1 is special by TOPREAL1:def 7;
A56:  2*(len f)>=2*1 by A1,AXIOMS:25;
    then 2*(len f)>=1 by AXIOMS:22;
    then A57:2*(len f)-'1= 2*(len f)-1 by SCMFSA_7:3;
A58:2*(len f)-1>= 1+1-1 by A56,REAL_1:49;
then A59:  1 in Seg (2*(len f)-'1) by A57,FINSEQ_1:3;
      2*1-'1=1+1-'1 .=1 by BINARITH:39;
    then p.1=f/.1 by A30,A59;
   then A60:g1.1=f.1 by A1,FINSEQ_4:24;
      (2*(len f)-'1) in Seg (2*(len f)-'1) by A57,A58,FINSEQ_1:3;
 then p.(2*(len f)-'1)=f/.len f by A30;
   then A61:g1.len g1=f.len f by A1,A31,FINSEQ_4:24;
      len f + len f>=len f+1 by A1,AXIOMS:24;
    then 2*(len f)>=len f +1 by XCMPLX_1:11;
    then 2*(len f)-1>=len f +1-1 by REAL_1:49;
   then A62:len g1>=len f by A31,A57,XCMPLX_1:26;
     for i st i in dom (Y_axis(g1)) holds (Y_axis(f)).1 <= (Y_axis(g1)).i
         & (Y_axis(g1)).i <= (Y_axis(f)).(len f)
    proof let i;assume
      A63:i in dom (Y_axis(g1));
then A64:   i in Seg len (Y_axis(g1)) by FINSEQ_1:def 3;
      then i in Seg len g1 by GOBOARD1:def 4;
      then A65: 1<=i & i<=len g1 by FINSEQ_1:3;
      A66:i in Seg len g1 by A64,GOBOARD1:def 4;
      A67:(Y_axis(g1)).i = (g1/.i)`2 by A63,GOBOARD1:def 4;
      A68:len (Y_axis(f))=len f by GOBOARD1:def 4;
      A69:g1/.i=(g1.i) by A65,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A70:i mod 2=0;
        consider j such that
        A71: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
          g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A66,A69,A70,A71;
        then A72:(g1/.i)`2=(f/.(j+1))`2 by EUCLID:56;
        A73:1<=j+1 by NAT_1:29;
           2*j+1<=2*(len f)-1+1 by A31,A57,A65,A70,A71,AXIOMS:24;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then j+1 in Seg len f by A73,FINSEQ_1:3;
        then A74:j+1 in dom (Y_axis(f)) by A68,FINSEQ_1:def 3;
        then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
       hence thesis by A1,A67,A72,A74,GOBOARD4:def 1;
      suppose A75:i mod 2=1;
        consider j such that
        A76: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A75,A76,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A77:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A65,JORDAN3:1;
        then A78:(g1/.i)`2=(f/.(j+1))`2 by A30,A31,A66,A69,A77;
        A79:1<=j+1 by NAT_1:29;
           2*j+1<=2*(len f)-1+1 by A31,A57,A65,A75,A76,NAT_1:38;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then j+1 in Seg len f by A79,FINSEQ_1:3;
        then A80:j+1 in dom (Y_axis(f)) by A68,FINSEQ_1:def 3;
        then (Y_axis(f)).(j+1) = (f/.(j+1))`2 by GOBOARD1:def 4;
       hence thesis by A1,A67,A78,A80,GOBOARD4:def 1;
    end;
   then A81:Y_axis(g1) lies_between (Y_axis(f)).1, (Y_axis(f)).(len f)
                             by GOBOARD4:def 1;
     for i st i in dom (X_axis(g1)) holds
    c <= (X_axis(g1)).i & (X_axis(g1)).i <= d
   proof let i;assume
      A82:i in dom (X_axis(g1));
      then A83: i in Seg len (X_axis(g1)) by FINSEQ_1:def 3;
      then A84:i in Seg len g1 by GOBOARD1:def 3;
      then A85: 1<=i & i<=len g1 by FINSEQ_1:3;
      A86:(X_axis(g1)).i = (g1/.i)`1 by A82,GOBOARD1:def 3;
      A87:len (X_axis(f))=len f by GOBOARD1:def 3;
      A88:g1/.i=(g1.i) by A85,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A89:i mod 2=0;
        consider j such that
        A90: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
          g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A84,A88,A89,A90;
        then A91:(g1/.i)`1=(f/.j)`1 by EUCLID:56;
          j<>0 by A83,A89,A90,FINSEQ_1:3;
        then j>0 by NAT_1:19;
then A92:     j>=0+1 by NAT_1:38;
           2*j+1<=2*(len f)-1+1 by A31,A57,A85,A89,A90,AXIOMS:24;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j in Seg len f by A92,FINSEQ_1:3;
        then A93:j in dom (X_axis(f)) by A87,FINSEQ_1:def 3;
        then (X_axis(f)).j = (f/.j)`1 by GOBOARD1:def 3;
       hence thesis by A1,A86,A91,A93,GOBOARD4:def 1;
      suppose A94:i mod 2=1;
        consider j such that
        A95: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A94,A95,XCMPLX_1:26;
        then i=2*j+(1+1)-1 by XCMPLX_1:1;
        then i=2*j+2*1-1;
        then A96:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A85,JORDAN3:1;
        then A97:(g1/.i)`1=(f/.(j+1))`1 by A30,A31,A84,A88,A96;
        A98:1<=j+1 by NAT_1:29;
           2*j+1<=2*(len f)-1+1 by A31,A57,A85,A94,A95,NAT_1:38;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then j+1 in Seg len f by A98,FINSEQ_1:3;
        then A99:j+1 in dom (X_axis(f)) by A87,FINSEQ_1:def 3;
        then (X_axis(f)).(j+1) = (f/.(j+1))`1 by GOBOARD1:def 3;
       hence thesis by A1,A86,A97,A99,GOBOARD4:def 1;
   end;
   then A100:X_axis(g1) lies_between c, d by GOBOARD4:def 1;
   A101:for i st i in dom g1 holds
   ex k st k in dom f & |. g1/.i - f/.k .| < a
    proof let i;assume
A102: i in dom g1;
      then A103:1<=i & i<=len g1 by FINSEQ_3:27;
      then A104:g1.i=g1/.i by FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A105:i mod 2=0;
        consider j such that
        A106: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
        A107:g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A102,A104,A105,A106;
        then A108:(g1/.i)`1=(f/.j)`1 by EUCLID:56;
        A109:g1/.i-f/.j
             =|[(g1/.i)`1-(f/.j)`1,(g1/.i)`2-(f/.j)`2]| by EUCLID:65
            .=|[0,(g1/.i)`2-(f/.j)`2]| by A108,XCMPLX_1:14;
        then A110:(g1/.i-f/.j)`1=0 by EUCLID:56;
          (g1/.i-f/.j)`2=(g1/.i)`2-(f/.j)`2 by A109,EUCLID:56;
        then |.g1/.i-f/.j.|=
          sqrt((((g1/.i-f/.j)`1))^2+(((g1/.i)`2-(f/.j)`2))^2)
                        by Th47
         .= sqrt((((f/.(j+1))`2-(f/.j)`2))^2) by A107,A110,EUCLID:56,SQUARE_1:
60;
        then |.g1/.i-f/.j.|=abs((f/.(j+1))`2-(f/.j)`2) by SQUARE_1:91
                      .=abs((f/.j)`2 -(f/.(j+1))`2) by UNIFORM1:13;
        then A111:|.g1/.i-f/.j.|
        <=|.f/.j-f/.(j+1).| by Th51;
          j<>0 by A102,A105,A106,FINSEQ_3:27;
        then j>0 by NAT_1:19;
        then A112:  j>=0+1 by NAT_1:38;
           2*j+1<=2*(len f)-1+1 by A31,A57,A103,A105,A106,AXIOMS:24;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
        then A113: j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then |. f/.j-f/.(j+1) .|<a by A1,A112;
        then A114: |. g1/.i - f/.j .|<a by A111,AXIOMS:22;
          j in dom f by A112,A113,FINSEQ_3:27;
       hence thesis by A114;
      suppose A115:i mod 2=1;
        consider j such that
        A116: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A115,A116,XCMPLX_1:26;
        then i=2*j+(1+1)-1 by XCMPLX_1:1;
        then i=2*j+2*1-1;
        then A117:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A103,JORDAN3:1;
        then g1/.i=f/.(j+1) by A30,A102,A104,A117;
        then A118:|.g1/.i-f/.(j+1).|=|.0.REAL 2.| by EUCLID:46 .=0 by TOPRNS_1:
24;
           2*j+1+1<=2*(len f)-1+1 by A31,A57,A103,A115,A116,AXIOMS:24;
         then 2*j+1+1<=2*(len f) by XCMPLX_1:27;
         then 2*j+1<2*(len f) by NAT_1:38;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
        then A119: j+1<=len f by NAT_1:38;
          1<=j+1 by NAT_1:29;
        then j+1 in dom f by A119,FINSEQ_3:27;
       hence thesis by A1,A118;
    end;
     for i st 1<=i & i+1<=len g1 holds |. g1/.i - g1/.(i+1) .|<a
    proof let i;assume A120:1<=i & i+1<=len g1;
then i<=len g1 by NAT_1:38;
      then A121:i in Seg len g1 by A120,FINSEQ_1:3;
      A122:1<=i & i<=len g1 by A120,NAT_1:38;
      A123:1<=i+1 by NAT_1:29;
then A124: i+1 in Seg (2*(len f)-'1) by A31,A120,FINSEQ_1:3;
      A125:g1.(i+1)=g1/.(i+1) by A120,A123,FINSEQ_4:24;
      A126:g1.i=g1/.i by A122,FINSEQ_4:24;
      per cases by GROUP_4:100;
      suppose A127:i mod 2=0;
        consider j such that
        A128: i=2*j+ (i mod 2) & (i mod 2)<2 by NAT_1:def 2;
        A129:g1/.i=|[(f/.j)`1,(f/.(j+1))`2]| by A30,A31,A121,A126,A127,A128;
          i+1=2*j+1+1-1 by A127,A128,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A130:i+1=2*(j+1)-1 by XCMPLX_1:8;
          1<=1+i by NAT_1:29;
        then 2*(j+1)-'1 =2*(j+1)-1 by A130,JORDAN3:1;
        then A131:g1/.(i+1)=f/.(j+1) by A30,A124,A125,A130;
        A132:(g1/.i)`1=(f/.j)`1 by A129,EUCLID:56;
        A133:(g1/.i)`2=(f/.(j+1))`2 by A129,EUCLID:56;
        A134:g1/.i-g1/.(i+1)
           =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]|
                                 by EUCLID:65
          .=|[(f/.j)`1-(f/.(j+1))`1,0]|
                                 by A131,A132,A133,XCMPLX_1:14;
        then A135:(g1/.i-g1/.(i+1))`1=(f/.j)`1-(f/.(j+1))`1 by EUCLID:56;
         (g1/.i-g1/.(i+1))`2=0 by A134,EUCLID:56;
        then |.g1/.i-g1/.(i+1).|= sqrt((((f/.j)`1-(f/.(j+1))`1))^2+0) by A135,
Th47,SQUARE_1:60
         .= sqrt((((f/.j)`1-(f/.(j+1))`1))^2);
        then |.g1/.i-g1/.(i+1).|=abs((f/.j)`1-(f/.(j+1))`1)
                                   by SQUARE_1:91;
        then A136:|.g1/.i-g1/.(i+1).|<=|.f/.j-f/.(j+1).| by Th51;
          j<>0 by A120,A127,A128;
        then j>0 by NAT_1:19;
        then A137:  j>=0+1 by NAT_1:38;
           2*j+1<=2*(len f)-1+1 by A31,A57,A120,A127,A128,NAT_1:38;
         then 2*j+1<=2*(len f) by XCMPLX_1:27;
         then 2*j<2*(len f) by NAT_1:38;
         then 2*j/2<2*(len f)/2 by REAL_1:73;
         then j<2*(len f)/2 by XCMPLX_1:90;
         then j<len f by XCMPLX_1:90;
         then j+1<=len f by NAT_1:38;
         then |. f/.j-f/.(j+1) .|<a by A1,A137;
        hence thesis by A136,AXIOMS:22;
      suppose A138:i mod 2=1;
        consider j such that
        A139: i=2*j+ (i mod 2) & i mod 2<2 by NAT_1:def 2;
          i=2*j+1+1-1 by A138,A139,XCMPLX_1:26
        .=2*j+(1+1)-1 by XCMPLX_1:1
        .=2*j+2*1-1;
        then A140:i=2*(j+1)-1 by XCMPLX_1:8;
        then 2*(j+1)-'1 =2*(j+1)-1 by A120,JORDAN3:1;
        then A141:g1/.i=f/.(j+1) by A30,A31,A121,A126,A140;
          i+1=2*j+(1+1) by A138,A139,XCMPLX_1:1
        .=2*j+2*1;
        then A142:i+1=2*(j+1) by XCMPLX_1:8;
        then A143:g1/.(i+1)=|[(f/.(j+1))`1,(f/.(j+1+1))`2]| by A30,A124,A125;
        then A144:(g1/.(i+1))`1=(f/.(j+1))`1 by EUCLID:56;
        A145:(g1/.(i+1))`2=(f/.(j+1+1))`2 by A143,EUCLID:56;
        A146:g1/.i-g1/.(i+1)
           =|[(g1/.i)`1-(g1/.(i+1))`1,(g1/.i)`2-(g1/.(i+1))`2]|
                         by EUCLID:65
          .=|[0,(f/.(j+1))`2-(f/.(j+1+1))`2]|
                         by A141,A144,A145,XCMPLX_1:14;
        then A147:(g1/.i-g1/.(i+1))`1=0 by EUCLID:56;
         (g1/.i-g1/.(i+1))`2=(f/.(j+1))`2-(f/.(j+1+1))`2
                                    by A146,EUCLID:56;
        then |.g1/.i-g1/.(i+1).|= sqrt(0+(((f/.(j+1))`2-(f/.(j+1+1))`2))^2)
           by A147,Th47,SQUARE_1:60
         .= sqrt((((f/.(j+1))`2-(f/.(j+1+1))`2))^2);
        then |.g1/.i-g1/.(i+1).|=abs((f/.(j+1))`2-(f/.(j+1+1))`2)
                              by SQUARE_1:91;
        then A148:|.g1/.i-g1/.(i+1).|
        <=|.f/.(j+1)-f/.(j+1+1).| by Th51;
  A149:  j+1>=1 by NAT_1:29;
           2*(j+1)+1<=2*(len f)-1+1 by A31,A57,A120,A142,AXIOMS:24;
         then 2*(j+1)+1<=2*(len f) by XCMPLX_1:27;
         then 2*(j+1)<2*(len f) by NAT_1:38;
         then 2*(j+1)/2<2*(len f)/2 by REAL_1:73;
         then (j+1)<2*(len f)/2 by XCMPLX_1:90;
         then (j+1)<len f by XCMPLX_1:90;
         then (j+1)+1<=len f by NAT_1:38;
         then |. f/.(j+1)-f/.(j+1+1) .|<a by A1,A149;
       hence thesis by A148,AXIOMS:22;
    end;
  hence thesis by A55,A60,A61,A62,A81,A100,A101;
 end;

canceled;

theorem Th59:
  for f being FinSequence of TOP-REAL 2 st 1 <=len f
    holds len X_axis(f)=len f &
  X_axis(f).1=(f/.1)`1 & X_axis(f).len f=(f/.len f)`1
 proof let f be FinSequence of TOP-REAL 2;
   assume A1:1 <=len f;
   then A2: 1 in Seg len f by FINSEQ_1:3;
   A3: len (X_axis(f)) = len f &
            for k st k in dom (X_axis(f)) holds (X_axis(f)).k = (f/.k)`1
                                   by GOBOARD1:def 3;
then A4: 1 in dom (X_axis(f)) by A2,FINSEQ_1:def 3;
     len f in Seg len f by A1,FINSEQ_1:3;
   then len f in dom (X_axis(f)) by A3,FINSEQ_1:def 3;
  hence thesis by A4,GOBOARD1:def 3;
 end;

theorem Th60:
  for f being FinSequence of TOP-REAL 2 st 1 <=len f
    holds len Y_axis(f)=len f &
  Y_axis(f).1=(f/.1)`2 & Y_axis(f).len f=(f/.len f)`2
 proof let f be FinSequence of TOP-REAL 2;
   assume A1:1 <=len f;
   then A2: 1 in Seg len f by FINSEQ_1:3;
   A3: len (Y_axis(f)) = len f &
            for k st k in dom (Y_axis(f)) holds (Y_axis(f)).k = (f/.k)`2
                                   by GOBOARD1:def 4;
then A4: 1 in dom (Y_axis(f)) by A2,FINSEQ_1:def 3;
     len f in Seg len f by A1,FINSEQ_1:3;
   then len f in dom (Y_axis(f)) by A3,FINSEQ_1:def 3;
  hence thesis by A4,GOBOARD1:def 4;
 end;

theorem Th61:
  for f being FinSequence of TOP-REAL 2 st i in dom f
    holds X_axis(f).i=(f/.i)`1 & Y_axis(f).i=(f/.i)`2
proof let f be FinSequence of TOP-REAL 2;
  assume
A1: i in dom f;
    len (X_axis(f)) = len f by GOBOARD1:def 3;
  then i in dom (X_axis(f)) by A1,FINSEQ_3:31;
 hence (X_axis(f)).i = (f/.i)`1 by GOBOARD1:def 3;
    len (Y_axis(f)) = len f by GOBOARD1:def 4;
  then i in dom Y_axis f by A1,FINSEQ_3:31;
 hence thesis by GOBOARD1:def 4;
end;

:: Goboard Theorem in continuous case
theorem Th62:for P,Q being non empty Subset of TOP-REAL 2,
p1,p2,q1,q2 being Point of TOP-REAL 2 st
P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 &
 (for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1) &
 (for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1) &
 (for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2) &
 (for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2)
 holds P meets Q
proof let P,Q be non empty Subset of TOP-REAL 2,
p1,p2,q1,q2 be Point of TOP-REAL 2;
 assume that A1:P is_an_arc_of p1,p2 & Q is_an_arc_of q1,q2 and
  A2:(for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1)
  and
  A3:(for p being Point of TOP-REAL 2 st p in Q holds p1`1<=p`1 & p`1<= p2`1)
  and
  A4:(for p being Point of TOP-REAL 2 st p in P holds q1`2<=p`2 & p`2<= q2`2)
  and
  A5:(for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2);
  A6:p1<>p2 by A1,JORDAN6:49;
  A7:q1<>q2 by A1,JORDAN6:49;
  consider f being map of I[01], (TOP-REAL 2)|P such that
    A8:f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
  consider g being map of I[01], (TOP-REAL 2)|Q such that
    A9:g is_homeomorphism & g.0 = q1 & g.1 = q2 by A1,TOPREAL1:def 2;
  consider f1 being map of I[01],TOP-REAL 2 such that
  A10: f=f1 & f1 is continuous & f1 is one-to-one by A8,JORDAN7:15;
  consider g1 being map of I[01],TOP-REAL 2 such that
  A11: g=g1 & g1 is continuous & g1 is one-to-one by A9,JORDAN7:15;
   A12:TOP-REAL 2=TopSpaceMetr(Euclid 2) by EUCLID:def 8;
    A13: Euclid 2= MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;
   reconsider P'=P,Q'=Q as Subset of TopSpaceMetr(Euclid 2)
                              by A12;
   A14:P' <> {} & P' is compact & Q' <> {}
 & Q' is compact by A1,A12,JORDAN5A:1;
   assume P /\ Q= {};
     then P misses Q by XBOOLE_0:def 7;
     then A15:min_dist_min(P',Q')>0 by A14,Th55;
     set e=min_dist_min(P',Q')/5;
     A16:e*5=min_dist_min(P',Q') by XCMPLX_1:88;
A17: e>0/5 by A15,REAL_1:73;
     then consider h being FinSequence of REAL such that
     A18: h.1=0 & h.len h=1 & 5<=len h & rng h c= the carrier of I[01]
     & h is increasing
     &(for i being Nat,R being Subset of I[01],
     W being Subset of Euclid 2
      st 1<=i & i<len h & R=[.h/.i,h/.(i+1).] & W=f1.:(R) holds
     diameter(W)<e) by A8,A10,UNIFORM1:15;
     deffunc F(Nat)=f1.(h.$1);
       ex h1' being FinSequence st len h1'=len h &
     for i st i in Seg len h holds h1'.i=F(i) from SeqLambda;
     then consider h1' being FinSequence such that
     A19:len h1'=len h &
     for i st i in Seg len h holds h1'.i=f1.(h.i);
       rng h1' c= the carrier of TOP-REAL 2
      proof let y;assume y in rng h1';
        then consider x such that
        A20:x in dom h1' & y=h1'.x by FUNCT_1:def 5;
        A21:dom h1'=Seg len h1' by FINSEQ_1:def 3;
        reconsider i=x as Nat by A20;
        A22: h1'.i=f1.(h.i) by A19,A20,A21;
          i in dom h by A19,A20,A21,FINSEQ_1:def 3;
        then A23:h.i in rng h by FUNCT_1:def 5;
          dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
         .=the carrier of I[01] by PRE_TOPC:12;
        then A24:h1'.i in rng f by A10,A18,A22,A23,FUNCT_1:def 5;
          rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
         .=P by PRE_TOPC:def 10;
       hence thesis by A20,A24;
      end;
     then reconsider h1=h1' as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
A25: dom h=Seg len h by FINSEQ_1:def 3;
     A26:the carrier of TOP-REAL 2=the carrier of Euclid 2 by TOPREAL3:13;
     A27:for i st 1<=i & i+1<=len h1 holds |.h1/.i-h1/.(i+1).|<e
      proof let i;assume A28:1<=i & i+1<=len h1;
        then A29:i<len h1 by NAT_1:38;
        A30:1<i+1 by A28,NAT_1:38;
        then A31:i+1 in Seg len h by A19,A28,FINSEQ_1:3;
        A32: i in Seg len h by A19,A28,A29,FINSEQ_1:3;
        then A33:h1'.i=f1.(h.i) by A19;
        then A34:h1/.i=f1.(h.i) by A28,A29,FINSEQ_4:24;
        A35:h1'.(i+1)=f1.(h.(i+1)) by A19,A31;
        then A36:h1/.(i+1)=f1.(h.(i+1)) by A28,A30,FINSEQ_4:24;
        A37:i in dom h by A19,A28,A29,FINSEQ_3:27;
        then A38:h.i in rng h by FUNCT_1:def 5;
A39:    dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
         .=the carrier of I[01] by PRE_TOPC:12;
        then A40:h1'.i in rng f by A10,A18,A33,A38,FUNCT_1:def 5;
        A41:rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
         .=P by PRE_TOPC:def 10;
        then A42:f1.(h.i) is Element of TOP-REAL 2 by A19,A32,
A40;
          i+1 in dom h by A19,A28,A30,FINSEQ_3:27;
        then h.(i+1) in rng h by FUNCT_1:def 5;
        then h1'.(i+1) in rng f by A10,A18,A35,A39,FUNCT_1:def 5;
        then A43:f1.(h.(i+1)) is Element of TOP-REAL 2 by A19,
A31,A41;
        A44:h.i=h/.i by A19,A28,A29,FINSEQ_4:24;
        A45:i+1 in dom h by A19,A28,A30,FINSEQ_3:27;
        then A46:h.(i+1) in rng h by FUNCT_1:def 5;
        A47:h.(i+1)=h/.(i+1) by A19,A28,A30,FINSEQ_4:24;
          i<i+1 by NAT_1:38;
        then A48:0<=h/.i & h/.i <= h/.(i+1) & h/.(i+1)<=1
             by A18,A37,A38,A44,A45,A46,A47,BORSUK_1:83,GOBOARD1:def 1,TOPREAL5
:1;
       reconsider W1=P as Subset of Euclid 2 by A26;
        reconsider Pa=P as Subset of TOP-REAL 2;
        A49:Pa is compact by A1,JORDAN5A:1;
        reconsider Pa as non empty Subset of TOP-REAL 2;
        reconsider R=[.h/.i,h/.(i+1).] as Subset of I[01]
                          by A18,A38,A44,A46,A47,BORSUK_1:83,RCOMP_1:16;
        reconsider w1=f1.(h.i),w2=f1.(h.(i+1)) as Point of Euclid 2
                                   by A42,A43,TOPREAL3:13;
        A50: h.i in R by A44,A48,TOPREAL5:1;
          h.(i+1) in R by A47,A48,TOPREAL5:1;
        then A51:w1 in f1.:R & w2 in f1.:R by A39,A50,FUNCT_1:def 12;
        reconsider W=f1.:R as Subset of Euclid 2 by A26;
        A52:dom f1=[#](I[01]) & rng f1=P
                      by A8,A10,A41,TOPS_2:def 5;
          [#](I[01])=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
        then P=f1.:([.0,1.]) by A52,RELAT_1:146;
        then A53:W c= W1 by BORSUK_1:83,RELAT_1:156;
          p1 in Pa by A1,TOPREAL1:4;
        then A54: W-bound Pa <= p1`1 & p1`1 <= E-bound Pa &
        S-bound Pa <= p1`2 & p1`2 <= N-bound Pa by A49,PSCOMP_1:71;
        set r1=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))+1;
             (W-bound Pa)<=(E-bound Pa) by A54,AXIOMS:22;
           then A55:0<=((E-bound Pa) - (W-bound Pa)) by SQUARE_1:12;
             (S-bound Pa)<=(N-bound Pa) by A54,AXIOMS:22;
           then 0<=((N-bound Pa) - (S-bound Pa)) by SQUARE_1:12;
        then A56:((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
            >=0+0 by A55,REAL_1:55;
         A57: r1> ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
                             by REAL_1:69;
          for x,y being Point of Euclid 2
         st x in W1 & y in W1 holds dist(x,y)<=r1
         proof let x,y be Point of Euclid 2;
           assume A58: x in W1 & y in W1;
           then reconsider pw1=x,pw2=y as Point of TOP-REAL 2;
           A59:dist(x,y)=|.pw1-pw2.| by Th45;
           A60:|.pw1-pw2.|<=abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2) by Th49;
           A61:W-bound Pa <= pw1`1 & pw1`1 <= E-bound Pa &
                 S-bound Pa <= pw1`2 & pw1`2 <= N-bound Pa
                     by A49,A58,PSCOMP_1:71;
           A62:W-bound Pa <= pw2`1 & pw2`1 <= E-bound Pa &
                 S-bound Pa <= pw2`2 & pw2`2 <= N-bound Pa
                            by A49,A58,PSCOMP_1:71;
          then A63:abs(pw1`1-pw2`1)<=(E-bound Pa) - (W-bound Pa) by A61,Th31;
             abs(pw1`2-pw2`2)<=(N-bound Pa) - (S-bound Pa) by A61,A62,Th31;
           then A64:abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)
           <=((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
                         by A63,REAL_1:55;
             ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
           <= ((E-bound Pa) - (W-bound Pa))+((N-bound Pa) - (S-bound Pa))
            +1 by REAL_1:69;
           then abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)<=r1 by A64,AXIOMS:22;
          hence thesis by A59,A60,AXIOMS:22;
         end;
        then W1 is bounded by A56,A57,TBSP_1:def 9;
        then A65:W is bounded by A53,TBSP_1:21;
        A66: diameter(W)<e by A18,A19,A28,A29;
          dist(w1,w2)<=diameter(W) by A51,A65,TBSP_1:def 10;
        then dist(w1,w2)<e by A66,AXIOMS:22;
       hence thesis by A34,A36,Th45;
      end;
     A67:len h1>=1 by A18,A19,AXIOMS:22;
     consider hb being FinSequence of REAL
      such that
     A68: hb.1=0 & hb.len hb=1 & 5<=len hb & rng hb c= the carrier of I[01]
     & hb is increasing
     &(for i being Nat,R being Subset of I[01],
     W being Subset of Euclid 2
      st 1<=i & i<len hb & R=[.hb/.i,hb/.(i+1).] & W=g1.:(R) holds
     diameter(W)<e) by A9,A11,A17,UNIFORM1:15;
     A69: 1<=len hb by A68,AXIOMS:22;
     then A70:1 in dom hb by FINSEQ_3:27;
     A71:len hb in dom hb by A69,FINSEQ_3:27;
     deffunc F(Nat)=g1.(hb.$1);
       ex h2' being FinSequence st len h2'=len hb &
     for i st i in Seg len hb holds h2'.i=F(i) from SeqLambda;
     then consider h2' being FinSequence such that
     A72:len h2'=len hb &
     for i st i in Seg len hb holds h2'.i=g1.(hb.i);
       rng h2' c= the carrier of TOP-REAL 2
      proof let y;assume y in rng h2';
        then consider x such that
        A73:x in dom h2' & y=h2'.x by FUNCT_1:def 5;
        A74:dom h2'=Seg len h2' by FINSEQ_1:def 3;
        reconsider i=x as Nat by A73;
        A75: h2'.i=g1.(hb.i) by A72,A73,A74;
          i in dom hb by A72,A73,A74,FINSEQ_1:def 3;
        then A76:hb.i in rng hb by FUNCT_1:def 5;
          dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
         .=the carrier of I[01] by PRE_TOPC:12;
        then A77:h2'.i in rng g by A11,A68,A75,A76,FUNCT_1:def 5;
          rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
         .=Q by PRE_TOPC:def 10;
       hence thesis by A73,A77;
      end;
     then reconsider h2=h2' as FinSequence of TOP-REAL 2 by FINSEQ_1:def 4;
     A78:dom hb=Seg len hb by FINSEQ_1:def 3;
A79: for i st i in dom hb holds h2/.i=g1.(hb.i)
      proof let i;assume
A80:   i in dom hb;
        then A81:h2.i=g1.(hb.i) by A72,A78;
          1<=i & i<=len hb by A78,A80,FINSEQ_1:3;
       hence thesis by A72,A81,FINSEQ_4:24;
      end;
     A82:len h2>=1 by A68,A72,AXIOMS:22;
     A83:for i st i in dom h1 holds
 (h1/.1)`1<=(h1/.i)`1 & (h1/.i)`1<=(h1/.len h1)`1
  proof let i;assume A84:i in dom h1;
     then A85: i in Seg len h by A19,FINSEQ_1:def 3;
     then A86:i in dom h by FINSEQ_1:def 3;
       h1.i=f1.(h.i) by A19,A85;
     then A87:h1/.i=f1.(h.i) by A84,FINSEQ_4:def 4;
       1 in dom h by A19,A67,FINSEQ_3:27;
     then h1.1=f1.(h.1) by A19,A25;
     then A88:h1/.1=f1.(h.1) by A67,FINSEQ_4:24;
       len h in dom h by A19,A67,FINSEQ_3:27;
     then h1.len h1=f1.(h.len h) by A19,A25;
     then A89:h1/.len h1=f1.(h.len h) by A67,FINSEQ_4:24;
     A90:h.i in rng h by A86,FUNCT_1:def 5;
       dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
       .=the carrier of I[01] by PRE_TOPC:12;
     then A91:h1/.i in rng f by A10,A18,A87,A90,FUNCT_1:def 5;
       rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
       .=P by PRE_TOPC:def 10;
   hence thesis by A2,A8,A10,A18,A88,A89,A91;
  end;
 A92: for i st i in dom (X_axis(h1)) holds
  (X_axis(h1)).1<=(X_axis(h1)).i & (X_axis(h1)).i<=(X_axis(h1)).(len h1)
  proof let i;assume i in dom (X_axis(h1));
     then i in Seg len (X_axis(h1)) by FINSEQ_1:def 3;
     then i in Seg len h1 by A67,Th59;
     then A93:i in dom h1 by FINSEQ_1:def 3;
     then A94:(X_axis(h1)).i = (h1/.i)`1 by Th61;
     A95:(X_axis(h1)).1=(h1/.1)`1 by A67,Th59;
       (X_axis(h1)).len h1=(h1/.len h1)`1 by A67,Th59;
    hence thesis by A83,A93,A94,A95;
  end;
 A96:for i st i in dom h1 holds
 q1`2<=(h1/.i)`2 & (h1/.i)`2<=q2`2
  proof let i;assume A97:i in dom h1;
     then A98: i in Seg len h1 by FINSEQ_1:def 3;
     then A99:i in dom h by A19,FINSEQ_1:def 3;
       h1.i=f1.(h.i) by A19,A98;
     then A100:h1/.i=f1.(h.i) by A97,FINSEQ_4:def 4;
     A101:h.i in rng h by A99,FUNCT_1:def 5;
       dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
       .=the carrier of I[01] by PRE_TOPC:12;
     then A102:h1/.i in rng f by A10,A18,A100,A101,FUNCT_1:def 5;
       rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
       .=P by PRE_TOPC:def 10;
   hence thesis by A4,A102;
  end;
   for i st i in dom (Y_axis(h1)) holds
   q1`2<=(Y_axis(h1)).i & (Y_axis(h1)).i<=q2`2
  proof let i;assume i in dom (Y_axis(h1));
     then i in Seg len (Y_axis(h1)) by FINSEQ_1:def 3;
     then i in Seg len h1 by A67,Th60;
     then A103:i in dom h1 by FINSEQ_1:def 3;
     then (Y_axis(h1)).i = (h1/.i)`2 by Th61;
    hence thesis by A96,A103;
  end;
 then A104:X_axis(h1) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
 Y_axis(h1) lies_between q1`2,q2`2 by A92,GOBOARD4:def 1;
 A105:for i st i in dom h2 holds
 (h2/.1)`2<=(h2/.i)`2 & (h2/.i)`2<=(h2/.len h2)`2
  proof let i;assume i in dom h2;
     then i in Seg len h2 by FINSEQ_1:def 3;
     then A106:i in dom hb by A72,FINSEQ_1:def 3;
     then A107:h2/.i=g1.(hb.i) by A79;
       1 in Seg len hb by A72,A82,FINSEQ_1:3;
     then 1 in dom hb by FINSEQ_1:def 3;
     then A108:h2/.1=g1.(hb.1) by A79;
       len hb in Seg len hb by A72,A82,FINSEQ_1:3;
     then len hb in dom hb by FINSEQ_1:def 3;
     then A109:h2/.len h2=g1.(hb.len hb) by A72,A79;
     A110:hb.i in rng hb by A106,FUNCT_1:def 5;
       dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
       .=the carrier of I[01] by PRE_TOPC:12;
     then A111:h2/.i in rng g by A11,A68,A107,A110,FUNCT_1:def 5;
       rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
       .=Q by PRE_TOPC:def 10;
   hence thesis by A5,A9,A11,A68,A108,A109,A111;
  end;
 A112: for i st i in dom (Y_axis(h2)) holds
  (Y_axis(h2)).1<=(Y_axis(h2)).i & (Y_axis(h2)).i <=(Y_axis(h2)).(len h2)
  proof let i;assume i in dom (Y_axis(h2));
     then i in Seg len (Y_axis(h2)) by FINSEQ_1:def 3;
     then i in Seg len h2 by A82,Th60;
     then A113:i in dom h2 by FINSEQ_1:def 3;
     then A114:(Y_axis(h2)).i = (h2/.i)`2 by Th61;
     A115:(Y_axis(h2)).1=(h2/.1)`2 by A82,Th60;
       (Y_axis(h2)).len h2=(h2/.len h2)`2 by A82,Th60;
    hence thesis by A105,A113,A114,A115;
  end;
 A116:for i st i in dom h2 holds
 p1`1<=(h2/.i)`1 & (h2/.i)`1<=p2`1
  proof let i;assume i in dom h2;
     then i in Seg len h2 by FINSEQ_1:def 3;
     then A117:i in dom hb by A72,FINSEQ_1:def 3;
     then A118:h2/.i=g1.(hb.i) by A79;
     A119:hb.i in rng hb by A117,FUNCT_1:def 5;
       dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
       .=the carrier of I[01] by PRE_TOPC:12;
     then A120:h2/.i in rng g by A11,A68,A118,A119,FUNCT_1:def 5;
       rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
       .=Q by PRE_TOPC:def 10;
   hence thesis by A3,A120;
  end;
   for i st i in dom (X_axis(h2)) holds
   p1`1<= (X_axis(h2)).i & (X_axis(h2)).i<=p2`1
  proof let i;assume i in dom (X_axis(h2));
     then i in Seg len (X_axis(h2)) by FINSEQ_1:def 3;
     then i in Seg len h2 by A82,Th59;
     then A121:i in dom h2 by FINSEQ_1:def 3;
     then (X_axis(h2)).i = (h2/.i)`1 by Th61;
    hence thesis by A116,A121;
  end;
 then A122:X_axis(h2) lies_between p1`1, p2`1 &
 Y_axis(h2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2)
                                  by A112,GOBOARD4:def 1;
 A123:for i st 1<=i & i+1<=len h2 holds
 |. (h2/.i)-(h2/.(i+1)) .|<e
      proof let i;assume A124:1<=i & i+1<=len h2;
        then A125:i<len h2 by NAT_1:38;
        A126:1<i+1 by A124,NAT_1:38;
        then A127:i+1 in Seg len hb by A72,A124,FINSEQ_1:3;
          i in Seg len hb by A72,A124,A125,FINSEQ_1:3;
        then A128:h2'.i=g1.(hb.i) by A72;
        then A129:h2/.i=g1.(hb.i) by A124,A125,FINSEQ_4:24;
        A130:h2'.(i+1)=g1.(hb.(i+1)) by A72,A127;
          h2.(i+1)=h2/.(i+1) by A124,A126,FINSEQ_4:24;
        then A131:h2/.(i+1)=g1.(hb.(i+1)) by A72,A127;
          i in Seg len hb by A72,A124,A125,FINSEQ_1:3;
        then A132:i in dom hb by FINSEQ_1:def 3;
        then A133:hb.i in rng hb by FUNCT_1:def 5;
        A134: dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
         .=the carrier of I[01] by PRE_TOPC:12;
        then A135:h2'.i in rng g by A11,A68,A128,A133,FUNCT_1:def 5;
        A136:rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
         .=Q by PRE_TOPC:def 10;
          i+1 in Seg len hb by A72,A124,A126,FINSEQ_1:3;
        then i+1 in dom hb by FINSEQ_1:def 3;
        then hb.(i+1) in rng hb by FUNCT_1:def 5;
        then h2'.(i+1) in rng g by A11,A68,A130,A134,FUNCT_1:def 5;
   then A137:g1.(hb.(i+1)) is Element of TOP-REAL 2 by A72,A127,
A136;
        A138:hb.i=hb/.i by A72,A124,A125,FINSEQ_4:24;
          i+1 in Seg len hb by A72,A124,A126,FINSEQ_1:3;
        then A139:i+1 in dom hb by FINSEQ_1:def 3;
        then A140:hb.(i+1) in rng hb by FUNCT_1:def 5;
        A141:hb.(i+1)=hb/.(i+1) by A72,A124,A126,FINSEQ_4:24;
          i<i+1 by NAT_1:38;
        then A142:0<=hb/.i & hb/.i <= hb/.(i+1) & hb/.(i+1)<=1
            by A68,A132,A133,A138,A139,A140,A141,BORSUK_1:83,GOBOARD1:def 1,
TOPREAL5:1;
       reconsider W1=Q as Subset of Euclid 2 by A26;
        reconsider Qa=Q as Subset of TOP-REAL 2;
        A143:Qa is compact by A1,JORDAN5A:1;
        reconsider Qa as non empty Subset of TOP-REAL 2;
        reconsider R=[.hb/.i,hb/.(i+1).] as Subset of I[01]
                                        by A68,A133,A138,A140,A141,BORSUK_1:83,
RCOMP_1:16;
        reconsider w1=g1.(hb.i),w2=g1.(hb.(i+1)) as Point of Euclid 2
                                   by A128,A135,A136,A137,TOPREAL3:13;
        A144: hb.i in R by A138,A142,TOPREAL5:1;
          hb.(i+1) in R by A141,A142,TOPREAL5:1;
        then A145:w1 in g1.:(R) & w2 in g1.:(R) by A134,A144,FUNCT_1:def 12;
        reconsider W=g1.:(R) as Subset of Euclid 2 by A26;
        A146:dom g1=[#](I[01]) & rng g1=Q by A9,A11,A136,TOPS_2:def 5;
          [#](I[01])=[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
        then Q=g1.:([.0,1.]) by A146,RELAT_1:146;
        then A147:W c= W1 by BORSUK_1:83,RELAT_1:156;
          q1 in Qa by A1,TOPREAL1:4;
        then A148: W-bound Qa <= q1`1 & q1`1 <= E-bound Qa &
        S-bound Qa <= q1`2 & q1`2 <= N-bound Qa by A143,PSCOMP_1:71;
        set r1=
           ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))+1;
             (W-bound Qa)<=(E-bound Qa) by A148,AXIOMS:22;
           then A149:0<=((E-bound Qa) - (W-bound Qa)) by SQUARE_1:12;
             (S-bound Qa)<=(N-bound Qa) by A148,AXIOMS:22;
           then 0<=((N-bound Qa) - (S-bound Qa)) by SQUARE_1:12;
        then A150:((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
            >=0+0 by A149,REAL_1:55;
         A151: r1> ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
                             by REAL_1:69;
          for x,y being Point of Euclid 2
         st x in W1 & y in W1 holds dist(x,y)<=r1
         proof let x,y be Point of Euclid 2;
           assume A152: x in W1 & y in W1;
           then reconsider pw1=x,pw2=y as Point of TOP-REAL 2;
           A153:dist(x,y)=|.pw1-pw2.| by Th45;
           A154:|.pw1-pw2.|<=abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2) by Th49;
           A155:W-bound Qa <= pw1`1 & pw1`1 <= E-bound Qa &
                 S-bound Qa <= pw1`2 & pw1`2 <= N-bound Qa
                              by A143,A152,PSCOMP_1:71;
           A156:W-bound Qa <= pw2`1 & pw2`1 <= E-bound Qa &
                 S-bound Qa <= pw2`2 & pw2`2 <= N-bound Qa
                              by A143,A152,PSCOMP_1:71;
           then A157:abs(pw1`1-pw2`1)<=(E-bound Qa) - (W-bound Qa) by A155,Th31
;
             abs(pw1`2-pw2`2)<=(N-bound Qa) - (S-bound Qa) by A155,A156,Th31;
           then A158:abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)
           <=((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
                         by A157,REAL_1:55;
             ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
           <=
           ((E-bound Qa) - (W-bound Qa))+((N-bound Qa) - (S-bound Qa))
            +1 by REAL_1:69;
           then abs(pw1`1-pw2`1)+abs(pw1`2-pw2`2)<=r1 by A158,AXIOMS:22;
          hence thesis by A153,A154,AXIOMS:22;
         end;
        then W1 is bounded by A150,A151,TBSP_1:def 9;
        then A159:W is bounded by A147,TBSP_1:21;
        A160: diameter(W)<e by A68,A72,A124,A125;
          dist(w1,w2)<=diameter(W) by A145,A159,TBSP_1:def 10;
        then dist(w1,w2)<e by A160,AXIOMS:22;
       hence thesis by A129,A131,Th45;
      end;
     consider f2 being FinSequence of TOP-REAL 2 such that
     A161: f2 is special &
     f2.1=h1.1 & f2.len f2=h1.len h1 & len f2>=len h1 &
     X_axis(f2) lies_between (X_axis(h1)).1, (X_axis(h1)).(len h1) &
     Y_axis(f2) lies_between q1`2,q2`2 &
     (for j st j in dom f2 holds
     ex k st k in dom h1 & |.(f2/.j - h1/.k).|<e)
     &(for j st 1<=j & j+1<=len f2 holds |.f2/.j - f2/.(j+1).|<e)
                                  by A17,A27,A67,A104,Th56;
     A162:len f2>=1 by A67,A161,AXIOMS:22;
     consider g2 being FinSequence of TOP-REAL 2 such that
     A163: g2 is special &
     g2.1=h2.1 & g2.len g2=h2.len h2 & len g2>=len h2 &
     Y_axis(g2) lies_between (Y_axis(h2)).1, (Y_axis(h2)).(len h2) &
     X_axis(g2) lies_between p1`1,p2`1 &
     (for j st j in dom g2 holds
     ex k st k in dom h2 & |.((g2/.j) - h2/.k).|<e)&
     (for j st 1<=j & j+1<=len g2 holds |.(g2/.j) - g2/.(j+1).|<e)
                     by A17,A82,A122,A123,Th57;
     A164:len g2>=1 by A82,A163,AXIOMS:22;
     A165:1 in dom h by A19,A67,FINSEQ_3:27;
     A166:len h in dom h by A19,A67,FINSEQ_3:27;
     A167: h1.1=f1.(h.1) by A19,A25,A165;
     A168:h1.1=h1/.1 by A67,FINSEQ_4:24;
     A169:h1.len h1=h1/.len h1 by A67,FINSEQ_4:24;
     A170:f2.1=f2/.1 by A162,FINSEQ_4:24;
     A171:f2.len f2=f2/.len f2 by A162,FINSEQ_4:24;
     A172:X_axis(f2).1=p1`1 by A8,A10,A18,A161,A162,A167,A170,Th59;
      (h1/.len h1)=p2 by A8,A10,A18,A19,A25,A166,A169;
     then A173:X_axis(f2).len f2=p2`1 by A161,A162,A169,A171,Th59;
     A174:(h2/.1)=q1 by A9,A11,A68,A70,A79;
     A175:h2.1=h2/.1 by A69,A72,FINSEQ_4:24;
     A176:h2.len h2=h2/.len h2 by A69,A72,FINSEQ_4:24;
      g2/.1=g2.1 by A164,FINSEQ_4:24;
     then A177:Y_axis(g2).1=q1`2 by A163,A164,A174,A175,Th60;
     A178:g2/.len g2=g2.len g2 by A164,FINSEQ_4:24;
      (g2.len g2)=q2 by A9,A11,A68,A71,A72,A79,A163,A176;
     then A179:Y_axis(g2).len g2=q2`2 by A164,A178,Th60;
     A180:(X_axis(f2)).1=(h1/.1)`1 by A161,A162,A168,A170,Th59
     .=(X_axis(h1)).1 by A67,Th59;
     A181:X_axis(f2).len f2=(h1/.len h1)`1 by A161,A162,A169,A171,Th59
     .=X_axis(h1).len h1 by A67,Th59;
       g2.1=g2/.1 by A164,FINSEQ_4:24;
     then A182:(Y_axis(g2)).1=(h2/.1)`2 by A163,A164,A175,Th60
     .=(Y_axis(h2)).1 by A82,Th60;
       g2.len g2=g2/.len g2 by A164,FINSEQ_4:24;
     then A183: Y_axis(g2).len g2=(h2/.len h2)`2 by A163,A164,A176,Th60
     .=Y_axis(h2).len h2 by A82,Th60;
       5<=len f2 by A18,A19,A161,AXIOMS:22;
     then A184:2<=len f2 by AXIOMS:22;
       5<=len g2 by A68,A72,A163,AXIOMS:22;
     then A185:2<=len g2 by AXIOMS:22;
     A186:1<=len h by A18,AXIOMS:22;
     then 1 in dom h by FINSEQ_3:27;
     then A187:h1/.1=f1.(h.1) by A19,A25,A168;
       len h in dom h by A186,FINSEQ_3:27;
     then A188: f2/.1<>f2/.len f2 by A6,A8,A10,A18,A19,A25,A161,A168,A170,A171,
A187;
     A189:1<=len hb by A68,AXIOMS:22;
     then 1 in dom hb by FINSEQ_3:27;
     then A190:h2/.1=g1.(hb.1) by A79;
       len hb in dom hb by A189,FINSEQ_3:27;
     then g2.1<>g2.len g2 by A7,A9,A11,A68,A72,A79,A163,A175,A176,A190;
     then L~f2 meets L~g2 by A161,A163,A170,A171,A172,A173,A177,A179,A180,A181,
A182,A183,A184,A185,A188,Th30;
     then consider s being set such that
     A191:s in L~f2 & s in L~g2 by XBOOLE_0:3;
     reconsider ps=s as Point of TOP-REAL 2 by A191;
       ps in union{ LSeg(f2,i) : 1 <= i & i+1 <= len f2 }
                             by A191,TOPREAL1:def 6;
     then consider x such that
     A192: ps in x & x in
     { LSeg(f2,i) : 1 <= i & i+1 <= len f2 } by TARSKI:def 4;
     consider i such that
     A193: x=LSeg(f2,i) &(1 <= i & i+1 <= len f2) by A192;
     A194:LSeg(f2,i)=LSeg(f2/.i,f2/.(i+1)) by A193,TOPREAL1:def 5;
       i<len f2 by A193,NAT_1:38;
     then i in dom f2 by A193,FINSEQ_3:27;
     then consider k such that
     A195: k in dom h1 & |.f2/.i - h1/.k.|<e by A161;
     A196:|.ps-f2/.i.|<=|.f2/.i-f2/.(i+1).| by A192,A193,A194,Th53;
       |.f2/.i-f2/.(i+1).|<e by A161,A193;
     then A197:|.ps-f2/.i.|<e by A196,AXIOMS:22;
     A198:|.ps-h1/.k.|<=|.ps-f2/.i.|+|.f2/.i-h1/.k.| by TOPRNS_1:35;
       |.ps-f2/.i.|+|.f2/.i-h1/.k.|<e+e by A195,A197,REAL_1:67;
     then A199:|.ps-h1/.k.|<e+e by A198,AXIOMS:22;
     A200:k in Seg len h1 by A195,FINSEQ_1:def 3;
     then A201:k in dom h by A19,FINSEQ_1:def 3;
       1<=k & k<=len h1 by A200,FINSEQ_1:3;
     then h1.k=h1/.k by FINSEQ_4:24;
     then A202:h1/.k=f1.(h.k) by A19,A200;
     A203:h.k in rng h by A201,FUNCT_1:def 5;
     A204: dom f1= [#](I[01]) by A8,A10,TOPS_2:def 5
       .=the carrier of I[01] by PRE_TOPC:12;
       rng f=[#]((TOP-REAL 2)|P) by A8,TOPS_2:def 5
       .=P by PRE_TOPC:def 10;
     then A205: h1/.k in P by A10,A18,A202,A203,A204,FUNCT_1:def 5;
     reconsider p11=h1/.k as Point of TOP-REAL 2;
     A206: |.(p11-ps).|<e+e by A199,TOPRNS_1:28;
       ps in union{ LSeg(g2,j) : 1 <= j & j+1 <=
 len g2 } by A191,TOPREAL1:def 6;
     then consider y such that
     A207: ps in y &
     y in { LSeg(g2,j) : 1 <= j & j+1 <= len g2 } by TARSKI:def 4;
     consider j such that
     A208:y=LSeg(g2,j) &(1 <= j & j+1 <= len g2) by A207;
     A209: LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) &
      ps in LSeg(g2,j) & y=LSeg(g2,j) &(1 <= j & j+1 <= len g2)
                             by A207,A208,TOPREAL1:def 5;
      j<len g2 &
      LSeg(g2,j)=LSeg((g2/.j),g2/.(j+1)) &
      ps in LSeg(g2,j) & y=LSeg(g2,j) &(1 <= j & j+1 <= len g2)
                         by A207,A208,NAT_1:38,TOPREAL1:def 5;
     then j in Seg len g2 by FINSEQ_1:3;
     then j in dom g2 by FINSEQ_1:def 3;
     then consider k' being Nat such that
     A210: k' in dom h2 & |.((g2/.j) - h2/.k').|<e by A163;
     A211:|.ps-(g2/.j).|<=|.(g2/.j)-g2/.(j+1).| by A209,Th53;
       |.(g2/.j)-g2/.(j+1).|<e by A163,A208;
     then A212:|.ps-(g2/.j).|<e by A211,AXIOMS:22;
     A213:|.ps-h2/.k'.|<=|.ps-(g2/.j).|+|.(g2/.j)-h2/.k'.| by TOPRNS_1:35;
       |.ps-(g2/.j).|+|.(g2/.j)-(h2/.k').|<e+e by A210,A212,REAL_1:67;
     then A214:|.ps-(h2/.k').|<e+e by A213,AXIOMS:22;
       k' in Seg len h2 by A210,FINSEQ_1:def 3;
     then k' in dom hb by A72,FINSEQ_1:def 3;
     then A215:hb.k' in rng hb &
     h2/.k'=g1.(hb.k') & k' in dom hb by A79,FUNCT_1:def 5;
       dom g1= [#](I[01]) by A9,A11,TOPS_2:def 5
       .=the carrier of I[01] by PRE_TOPC:12;
     then A216:Q<>{}(TOP-REAL 2) &
     h2/.k' in rng g & hb.k' in dom g1 by A11,A68,A215,FUNCT_1:def 5;
     A217: rng g=[#]((TOP-REAL 2)|Q) by A9,TOPS_2:def 5
       .=Q by PRE_TOPC:def 10;
     reconsider q11=h2/.k' as Point of TOP-REAL 2;
     reconsider x1=p11,x2=q11 as Point of Euclid 2 by A13,EUCLID:25;
       min_dist_min(P',Q')<=dist(x1,x2) by A14,A205,A216,A217,WEIERSTR:40;
     then A218:|.(p11-q11).|<= |.(p11-ps).|+|.(ps-q11).|
       & min_dist_min(P',Q')<=|.(p11-q11).| by Th45,TOPRNS_1:35;
       |.(p11-ps).|+|.(ps-q11).| <e+e+(e+e) by A206,A214,REAL_1:67;
     then |.(p11-q11).|<e+e+(e+e) by A218,AXIOMS:22;
     then |.(p11-q11).|<e+e+e+e by XCMPLX_1:1;
     then |.(p11-q11).|<4*e by XCMPLX_1:13;
     then min_dist_min(P',Q')<4*e by A218,AXIOMS:22;
     then 4*e-5*e>0 by A16,SQUARE_1:11;
     then (4-5)*e>0 by XCMPLX_1:40; then (4-5)*e/e>0 by A17,REAL_2:127;
     then 4-5>0 by A17,XCMPLX_1:90;
    hence contradiction;
end;

reserve X,Y for non empty TopSpace;

theorem Th63:for f being map of X,Y,
 P being non empty Subset of Y,
 f1 being map of X,Y|P st f=f1 & f is continuous holds
 f1 is continuous
 proof let f be map of X,Y,
  P be non empty Subset of Y,
  f1 be map of X,Y|P;
   assume A1:f=f1 & f is continuous;
   A2:rng f1 c= the carrier of (Y|P);
     for P1 being Subset of (Y|P) st
    P1 is open holds f1"P1 is open
    proof let P1 be Subset of (Y|P);
      assume P1 is open;
      then P1 in the topology of (Y|P) by PRE_TOPC:def 5;
      then consider Q being Subset of Y such that
      A3: Q in the topology of Y &
       P1 = Q /\ [#](Y|P) by PRE_TOPC:def 9;
      reconsider Q as Subset of Y;
        Q is open by A3,PRE_TOPC:def 5;
      then A4:f"Q is open by A1,TOPS_2:55;
      A5: [#](Y|P)=P by PRE_TOPC:def 10;
      A6:f"Q=f1"(rng f1 /\ Q) by A1,RELAT_1:168;
        Q /\ [#](Y|P) c= Q by XBOOLE_1:17;
      then A7:f1"P1 c= f"Q by A1,A3,RELAT_1:178;
        rng f1 c= P by A2,A5,PRE_TOPC:12;
      then rng f1 /\ Q c= P /\ Q by XBOOLE_1:26;
      then f1"(rng f1 /\ Q) c= f1"P1 by A3,A5,RELAT_1:178;
     hence thesis by A4,A6,A7,XBOOLE_0:def 10;
    end;
  hence thesis by TOPS_2:55;
 end;

theorem Th64:for f being map of X,Y,
 P being non empty Subset of Y
 st X is compact & Y is_T2 &
 f is continuous one-to-one & P=rng f holds
 ex f1 being map of X,(Y|P) st f=f1 & f1 is_homeomorphism
proof let f be map of X,Y,P be non empty Subset of Y such that
A1: X is compact and
A2: Y is_T2 and
A3:  f is continuous one-to-one and
A4: P=rng f;
  A5:f is Function of dom f,rng f by FUNCT_2:3;
  A6:the carrier of (Y|P)=P by JORDAN1:1;
  A7:dom f=the carrier of X by FUNCT_2:def 1;
  then reconsider f2=f as map of X,(Y|P) by A4,A5,A6;
  A8:dom f2=[#]X by A7,PRE_TOPC:12;
  A9: rng f2=[#](Y|P) by A4,PRE_TOPC:def 10;
  A10:Y|P is_T2 by A2,TOPMETR:3;
    f2 is continuous by A3,Th63;
  then f2 is_homeomorphism by A1,A3,A8,A9,A10,COMPTS_1:26;
 hence thesis;
end;

::  Fashoda Meet Theorem
theorem for f,g being map of I[01],TOP-REAL 2,a,b,c,d being real number,
  O,I being Point of I[01] st O=0 & I=1 &
  f is continuous one-to-one &
  g is continuous one-to-one &
  (f.O)`1=a & (f.I)`1=b &
  (g.O)`2=c & (g.I)`2=d &
  (for r being Point of I[01] holds
    a <=(f.r)`1 & (f.r)`1<=b & a <=(g.r)`1 & (g.r)`1<=b &
    c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d)
   holds rng f meets rng g
 proof let f,g be map of I[01],TOP-REAL 2,a,b,c,d be real number,
  O,I be Point of I[01];
   assume A1: O=0 & I=1 &
     f is continuous one-to-one & g is continuous one-to-one &
     (f.O)`1=a & (f.I)`1=b & (g.O)`2=c & (g.I)`2=d &
     (for r being Point of I[01] holds
      a<=(f.r)`1 & (f.r)`1<=b & a<=(g.r)`1 & (g.r)`1<=b &
      c <=(f.r)`2 & (f.r)`2<=d & c <=(g.r)`2 & (g.r)`2<=d);
      A2:dom f= the carrier of I[01] by FUNCT_2:def 1
      .=[#](I[01]) by PRE_TOPC:12;
      A3:[#](I[01]) =[.0,1.] by BORSUK_1:83,PRE_TOPC:12;
      then 0 in dom f by A2,TOPREAL5:1;
     then reconsider P=rng f as non empty Subset of TOP-REAL 2
                        by FUNCT_1:12;
        dom g= the carrier of I[01] by FUNCT_2:def 1
      .=[#](I[01]) by PRE_TOPC:12;
      then 0 in dom g by A3,TOPREAL5:1;
     then reconsider Q=rng g as non empty Subset of TOP-REAL 2
                       by FUNCT_1:12;
     A4:I[01] is compact by HEINE:11,TOPMETR:27;
     A5:TOP-REAL 2 is_T2 by SPPOL_1:26;
     then consider f1 being map of I[01],((TOP-REAL 2)|P) such that
      A6: f=f1 & f1 is_homeomorphism by A1,A4,Th64;
     consider g1 being map of I[01],((TOP-REAL 2)|Q) such that
     A7:g=g1 & g1 is_homeomorphism by A1,A4,A5,Th64;
     A8:dom f1= [#](I[01]) by A6,TOPS_2:def 5;
     reconsider p1=f1.O as Point of TOP-REAL 2 by A1,A6;
     reconsider p2=f1.I as Point of TOP-REAL 2 by A1,A6;
     A9:dom g1= [#](I[01]) by A7,TOPS_2:def 5;
     reconsider q1=g1.O as Point of TOP-REAL 2 by A1,A7;
     reconsider q2=g1.I as Point of TOP-REAL 2 by A1,A7;
     A10:P is_an_arc_of p1,p2 by A1,A6,TOPREAL1:def 2;
     A11:Q is_an_arc_of q1,q2 by A1,A7,TOPREAL1:def 2;
     A12:for p being Point of TOP-REAL 2 st p in P holds p1`1<=p`1 & p`1<= p2`1
      proof let p be Point of TOP-REAL 2;
        assume p in P; then consider x such that
        A13:x in dom f1 & p=f1.x by A6,FUNCT_1:def 5;
        reconsider r=x as Point of I[01] by A8,A13;
          p=f.r by A6,A13;
       hence thesis by A1,A6;
      end;
     A14:(for p being Point of TOP-REAL 2
     st p in Q holds p1`1<=p`1 & p`1<= p2`1)
      proof let p be Point of TOP-REAL 2;
        assume p in Q; then consider x such that
        A15:x in dom g1 & p=g1.x by A7,FUNCT_1:def 5;
        reconsider r=x as Point of I[01] by A9,A15;
          p=g.r by A7,A15;
       hence thesis by A1,A6;
      end;
     A16:for p being Point of TOP-REAL 2 st p in P holds
     q1`2<=p`2 & p`2<= q2`2
      proof let p be Point of TOP-REAL 2;
        assume p in P; then consider x such that
        A17:x in dom f1 & p=f1.x by A6,FUNCT_1:def 5;
        reconsider r=x as Point of I[01] by A8,A17;
          p=f.r by A6,A17;
       hence thesis by A1,A7;
      end;
       for p being Point of TOP-REAL 2 st p in Q holds q1`2<=p`2 & p`2<= q2`2
      proof let p be Point of TOP-REAL 2;
        assume p in Q; then consider x such that
        A18:x in dom g1 & p=g1.x by A7,FUNCT_1:def 5;
        reconsider r=x as Point of I[01] by A9,A18;
          p=g.r by A7,A18;
       hence thesis by A1,A7;
      end;
   hence thesis by A10,A11,A12,A14,A16,Th62;
 end;


Back to top