The Mizar article:

On the Dividing Function of the Simple Closed Curve into Segments

by
Yatsuka Nakamura

Received June 16, 1998

Copyright (c) 1998 Association of Mizar Users

MML identifier: JORDAN7
[ MML identifier index ]


environ

 vocabulary PRE_TOPC, EUCLID, ARYTM_1, COMPTS_1, TOPREAL2, PSCOMP_1, JORDAN6,
      TOPREAL1, JORDAN3, BOOLE, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, FUNCT_1,
      SUBSET_1, RCOMP_1, FINSEQ_1, TBSP_1, GOBRD10, FINSEQ_4;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XREAL_0, REAL_1, NAT_1, RCOMP_1,
      RELAT_1, BINARITH, FINSEQ_1, FUNCT_1, FUNCT_2, FINSEQ_4, TOPREAL1,
      TOPREAL2, TBSP_1, GOBOARD1, GOBRD10, PRE_TOPC, TOPS_2, STRUCT_0,
      COMPTS_1, EUCLID, JORDAN3, PSCOMP_1, JORDAN5C, JORDAN6, TOPMETR;
 constructors RCOMP_1, GOBRD10, BINARITH, TOPREAL2, TOPS_2, TBSP_1, REAL_1,
      PSCOMP_1, JORDAN3, JORDAN4, JORDAN5C, JORDAN6, FINSEQ_4, GOBOARD1,
      T_0TOPSP, URYSOHN1, YELLOW_8;
 clusters STRUCT_0, RELSET_1, EUCLID, PSCOMP_1, PRE_TOPC, XREAL_0, ARYTM_3,
      GOBOARD1, BORSUK_2, MEMBERED;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
 definitions TARSKI, XBOOLE_0, FUNCT_1;
 theorems TARSKI, JORDAN6, TOPREAL1, TOPREAL5, JORDAN5C, UNIFORM1, PRE_TOPC,
      FUNCT_2, TOPS_2, RELAT_1, FUNCT_1, SCMFSA_7, FINSEQ_1, AXIOMS, TOPMETR,
      FINSEQ_2, JORDAN3, GOBOARD1, BINARITH, NAT_1, REAL_1, RCOMP_1, FINSEQ_4,
      SQUARE_1, GOBRD10, SPRECT_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, BORSUK_1,
      COMPTS_1, RELSET_1, AMI_5, JORDAN5B, XCMPLX_0, PARTFUN2, XCMPLX_1;
 schemes DOMAIN_1, NAT_1;

begin :: Definition of the Segment and its property

reserve p,p1,p2,p3,q for Point of TOP-REAL 2;

Lm1: 0 < 1;

Lm2: 2-'1 = 2-1 by SCMFSA_7:3 .=1;

Lm3:
 for i, j, k be Nat holds i-'k <= j implies i <= j + k
proof let i, j, k be Nat; assume
A1: i-'k <= j;
 per cases;
 suppose
A2: i >= k;
   i-'k +k <= j + k by A1,AXIOMS:24;
 hence i <= j + k by A2,AMI_5:4;
 suppose
A3: i <= k;
   k <= j + k by NAT_1:29;
 hence i <= j + k by A3,AXIOMS:22;
end;

Lm4: for i, j, k be Nat holds j + k <= i implies k <= i -' j
proof let i, j, k be Nat; assume
A1: j + k <= i;
 per cases by A1,AXIOMS:21;
 suppose j + k = i;
 hence k <= i -' j by BINARITH:39;
 suppose j + k < i;
 hence k <= i -' j by Lm3;
end;

theorem Th1: for P being compact non empty Subset of TOP-REAL 2
 st P is_simple_closed_curve holds
 W-min(P) in Lower_Arc(P) & E-max(P) in Lower_Arc(P) &
 W-min(P) in Upper_Arc(P) & E-max(P) in Upper_Arc(P)
 proof let P be compact non empty Subset of TOP-REAL 2;
   assume P is_simple_closed_curve;
    then Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) &
    Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by JORDAN6:65;
   hence thesis by TOPREAL1:4;
 end;

theorem Th2: for P being compact non empty Subset of TOP-REAL 2,q
 st P is_simple_closed_curve & LE q,W-min(P),P
holds q=W-min(P)
proof let P be compact non empty Subset of TOP-REAL 2,q;
 assume A1:P is_simple_closed_curve & LE q,W-min(P),P;
   then A2:q in Upper_Arc(P) & W-min(P) in Upper_Arc(P) &
    LE q,W-min(P),Upper_Arc(P),W-min(P),E-max(P) by JORDAN6:def 10;
     Upper_Arc(P) is_an_arc_of W-min(P),E-max(P)
                            by A1,JORDAN6:def 8;
 hence q=W-min(P) by A2,JORDAN6:69;
end;

theorem Th3: for P being compact non empty Subset of TOP-REAL 2,q
 st P is_simple_closed_curve & q in P holds
 LE W-min(P),q,P
proof let P be compact non empty Subset of TOP-REAL 2,q;
  assume A1: P is_simple_closed_curve & q in P;
then A2:q in Upper_Arc(P) \/ Lower_Arc(P) by JORDAN6:65;
   A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) &
    Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:65;
     A4: W-min(P) in Upper_Arc(P) by A1,Th1;
    now per cases by A2,XBOOLE_0:def 2;
   case A5:q in Upper_Arc(P);
     then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A3,JORDAN5C:10;
    hence LE W-min(P),q,P by A4,A5,JORDAN6:def 10;
   case A6:q in Lower_Arc(P);
      now per cases;
     case not q=W-min(P);
      hence LE W-min(P),q,P by A4,A6,JORDAN6:def 10;
     case A7: q=W-min(P);
       then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,JORDAN5C:9;
      hence LE W-min(P),q,P by A4,A7,JORDAN6:def 10;
     end;
    hence LE W-min(P),q,P;
   end;
  hence LE W-min(P),q,P;
end;

definition
 let P be compact non empty Subset of TOP-REAL 2,
     q1,q2 be Point of TOP-REAL 2;
 func Segment(q1,q2,P) -> Subset of TOP-REAL 2 equals
 :Def1: {p: LE q1,p,P & LE p,q2,P} if q2<>W-min(P)
           otherwise {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
  correctness
  proof
    ex B being Subset of TOP-REAL 2 st
    (q2<>W-min(P) implies B={p: LE q1,p,P & LE p,q2,P})&
    (not q2<>W-min(P) implies B={p1: LE q1,p1,P or q1 in P & p1=W-min(P)})
    proof
      now per cases;
     case A1:q2<>W-min(P);
     defpred P[Point of TOP-REAL 2] means LE q1,$1,P & LE $1,q2,P;
        {p: P[p]} is Subset of
       TOP-REAL 2 from SubsetD;
       then reconsider C = {p: LE q1,p,P & LE p,q2,P} as Subset of
         TOP-REAL 2;
        (q2<>W-min(P) implies C={p: LE q1,p,P & LE p,q2,P})&
       (not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P)})
       by A1;
      hence thesis;
     case A2: not q2<>W-min(P);
     defpred P[Point of TOP-REAL 2] means LE q1,$1,P or q1 in P & $1=W-min(P);
        {p1: P[p1]}
       is Subset of TOP-REAL 2 from SubsetD;
       then reconsider C = {p1: LE q1,p1,P or q1 in P & p1=W-min(P)}
       as Subset of TOP-REAL 2;
        (q2<>W-min(P) implies C={p: LE q1,p,P & LE p,q2,P})&
       (not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P)})
       by A2;
      hence thesis;
     end;
     hence thesis;
    end;
   hence thesis;
  end;
 end;

theorem
  for P being compact non empty Subset of TOP-REAL 2
 st P is_simple_closed_curve holds
 Segment(W-min(P),E-max(P),P)=Upper_Arc(P) &
 Segment(E-max(P),W-min(P),P)=Lower_Arc(P)
  proof let P be compact non empty Subset of TOP-REAL 2;
   assume A1:P is_simple_closed_curve;
    then A2:E-max(P)<>W-min(P) by TOPREAL5:25;
    A3: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
A4:{p: LE W-min(P),p,P & LE p,E-max(P),P} = Upper_Arc(P)
    proof
      A5: {p: LE W-min(P),p,P & LE p,E-max(P),P} c= Upper_Arc(P)
       proof let x be set;assume
           x in {p: LE W-min(P),p,P & LE p,E-max(P),P};
          then consider p such that
          A6: p=x &
          ( LE W-min(P),p,P & LE p,E-max(P),P);
             now per cases by A6,JORDAN6:def 10;
            case p in Upper_Arc(P) & E-max(P) in Lower_Arc(P)
                                              & not E-max(P)=W-min(P);
             hence x in Upper_Arc(P) by A6;
            case p in Upper_Arc(P) & E-max(P) in Upper_Arc(P) &
                 LE p,E-max(P),Upper_Arc(P),W-min(P),E-max(P);
             hence x in Upper_Arc(P) by A6;
            case A7: p in Lower_Arc(P) & E-max(P) in Lower_Arc(P)
                  & not E-max(P)=W-min(P) &
               LE p,E-max(P),Lower_Arc(P),E-max(P),W-min(P);
                Lower_Arc(P) is_an_arc_of E-max(P),W-min(P)
                            by A1,JORDAN6:def 9;
               then p=E-max(P) by A7,JORDAN6:69;
             hence x in Upper_Arc(P) by A3,A6,TOPREAL1:4;
            end;
         hence x in Upper_Arc(P);
       end;
       Upper_Arc(P) c= {p: LE W-min(P),p,P & LE p,E-max(P),P}
       proof let x be set;assume A8: x in Upper_Arc(P);
         then reconsider p2=x as Point of TOP-REAL 2;
         A9: W-min(P) in Lower_Arc(P) & E-max(P) in Lower_Arc(P) &
         W-min(P) in Upper_Arc(P) & E-max(P) in Upper_Arc(P) by A1,Th1;
            LE W-min(P),p2,Upper_Arc(P),W-min(P),E-max(P)
                                 by A3,A8,JORDAN5C:10;
          then A10: LE W-min(P),p2,P by A8,A9,JORDAN6:def 10;
          LE p2,E-max(P),P by A2,A8,A9,JORDAN6:def 10;
        hence x in {p: LE W-min(P),p,P & LE p,E-max(P),P} by A10;
       end;
     hence thesis by A5,XBOOLE_0:def 10;
    end;
     {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} = Lower_Arc(P)
    proof
      A11: {p1: LE E-max(P),p1,P or E-max(P) in P &
      p1=W-min(P)} c= Lower_Arc(P)
       proof let x be set;assume
           x in {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)};
          then consider p1 such that
          A12: p1=x & (LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P));
           now per cases by A12;
          case A13: LE E-max(P),p1,P;
             now per cases by A12,A13,JORDAN6:def 10;
            case x in Lower_Arc(P);
             hence x in Lower_Arc(P);
            case A14: E-max(P) in Upper_Arc(P) & p1 in Upper_Arc(P) &
              LE E-max(P),p1,Upper_Arc(P),W-min(P),E-max(P);
              A15:Upper_Arc(P) is_an_arc_of W-min(P),E-max(P)
                             by A1,JORDAN6:65;
              then LE p1,E-max(P),Upper_Arc(P),W-min(P),E-max(P)
                                       by A14,JORDAN5C:10;
              then A16:p1=E-max(P) by A14,A15,JORDAN5C:12;
               Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
             hence x in Lower_Arc(P) by A12,A16,TOPREAL1:4;
            end;
           hence x in Lower_Arc(P);
          case E-max(P) in P & p1=W-min(P);
            then x in {W-min(P),E-max(P)} by A12,TARSKI:def 2;
            then x in Upper_Arc(P) /\ Lower_Arc(P) by A1,JORDAN6:def 9;
           hence x in Lower_Arc(P) by XBOOLE_0:def 3;
          end;
         hence x in Lower_Arc(P);
       end;
       Lower_Arc(P) c= {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)}
       proof let x be set;assume A17: x in Lower_Arc(P);
         then reconsider p2=x as Point of TOP-REAL 2;
     Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:65;
         then not (E-max P in P & p2=W-min P) implies
          E-max P in Upper_Arc P & p2 in Lower_Arc P & not p2=W-min P
                                 by A17,SPRECT_1:16,TOPREAL1:4;
         then LE E-max(P),p2,P or E-max P in P & p2=W-min P by JORDAN6:def 10;
        hence x in {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)};
       end;
     hence thesis by A11,XBOOLE_0:def 10;
    end;
   hence thesis by A2,A4,Def1;
  end;

theorem Th5:
for P being compact non empty Subset of TOP-REAL 2,
 q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P holds
 q1 in P & q2 in P
proof let P be compact non empty Subset of TOP-REAL 2,
 q1,q2 be Point of TOP-REAL 2;
 assume A1: P is_simple_closed_curve & LE q1,q2,P;
  then A2: Upper_Arc(P) \/ Lower_Arc(P)=P by JORDAN6:65;
   now per cases by A1,JORDAN6:def 10;
  case q1 in Upper_Arc(P) & q2 in Lower_Arc(P);
   hence q1 in P & q2 in P by A2,XBOOLE_0:def 2;
  case q1 in Upper_Arc(P) & q2 in Upper_Arc(P);
   hence q1 in P & q2 in P by A2,XBOOLE_0:def 2;
  case q1 in Lower_Arc(P) & q2 in Lower_Arc(P);
   hence q1 in P & q2 in P by A2,XBOOLE_0:def 2;
  end;
 hence thesis;
end;

theorem Th6:
for P being compact non empty Subset of TOP-REAL 2,
 q1,q2 being Point of TOP-REAL 2 st P is_simple_closed_curve & LE q1,q2,P holds
 q1 in Segment(q1,q2,P) & q2 in Segment(q1,q2,P)
 proof let P be compact non empty Subset of TOP-REAL 2,
   q1,q2 be Point of TOP-REAL 2;
   assume A1: P is_simple_closed_curve & LE q1,q2,P;
   hereby per cases;
   suppose A2: q2<>W-min(P);
       q1 in P by A1,Th5;
      then LE q1,q1,P by A1,JORDAN6:71;
      then q1 in {p: LE q1,p,P & LE p,q2,P} by A1;
     hence q1 in Segment(q1,q2,P) by A2,Def1;
   suppose A3: q2=W-min(P);
       q1 in P by A1,Th5;
      then LE q1,q1,P by A1,JORDAN6:71;
      then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
     hence q1 in Segment(q1,q2,P) by A3,Def1;
   end;
   per cases;
   suppose A4: q2<>W-min(P);
       q2 in P by A1,Th5;
      then LE q2,q2,P by A1,JORDAN6:71;
      then q2 in {p: LE q1,p,P & LE p,q2,P} by A1;
     hence q2 in Segment(q1,q2,P) by A4,Def1;
   suppose A5: q2=W-min(P);
       q2 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} by A1;
     hence q2 in Segment(q1,q2,P) by A5,Def1;
 end;

theorem Th7:
for P being compact non empty Subset of TOP-REAL 2,
 q1 being Point of TOP-REAL 2 st q1 in P & P is_simple_closed_curve holds
   q1 in Segment(q1,W-min P,P)
 proof let P be compact non empty Subset of TOP-REAL 2,
   q1 be Point of TOP-REAL 2 such that
A1:  q1 in P;
   assume P is_simple_closed_curve;
      then LE q1,q1,P by A1,JORDAN6:71;
      then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
     hence q1 in Segment(q1,W-min P,P) by Def1;
 end;

theorem
  for P being compact non empty Subset of TOP-REAL 2,
 q being Point of TOP-REAL 2
 st P is_simple_closed_curve & q in P
 & q<>W-min(P) holds Segment(q,q,P)={q}
proof let P be compact non empty Subset of TOP-REAL 2,
  q be Point of TOP-REAL 2;
  assume that
A1:P is_simple_closed_curve and
A2: q in P and
A3: q <> W-min P;
   for x being set holds x in Segment(q,q,P) iff x=q
   proof let x be set;
     hereby assume x in Segment(q,q,P);
       then x in {p: LE q,p,P & LE p,q,P} by A3,Def1;
       then ex p st p=x & (LE q,p,P & LE p,q,P);
      hence x=q by A1,JORDAN6:72;
     end;
    assume A4:x=q;
       LE q,q,P by A1,A2,JORDAN6:71;
      then x in {p: LE q,p,P & LE p,q,P} by A4;
     hence x in Segment(q,q,P) by A3,Def1;
   end;
 hence thesis by TARSKI:def 1;
end;

theorem
 for P being compact non empty Subset of TOP-REAL 2,
 q1,q2 being Point of TOP-REAL 2 st
  P is_simple_closed_curve & q1<>W-min(P) & q2<>W-min(P)
 holds not W-min(P) in Segment(q1,q2,P)
proof let P be compact non empty Subset of TOP-REAL 2,
 q1,q2 be Point of TOP-REAL 2;
 assume A1: P is_simple_closed_curve & q1<>W-min(P) & q2<>W-min(P);
  then A2:Segment(q1,q2,P)={p: LE q1,p,P & LE p,q2,P} by Def1;
   now assume W-min(P) in Segment(q1,q2,P);
    then consider p such that A3: p=W-min(P) &(LE q1,p,P & LE p,q2,P) by A2;
         A4: q1 in Upper_Arc(P) & p in Upper_Arc(P) &
            LE q1,p,Upper_Arc(P),W-min(P),E-max(P) by A3,JORDAN6:def 10;
           Upper_Arc(P) is_an_arc_of W-min(P),E-max(P)
                            by A1,JORDAN6:def 8;
   hence contradiction by A1,A3,A4,JORDAN6:69;
  end;
 hence thesis;
end;

theorem Th10:
for P being compact non empty Subset of TOP-REAL 2,
 q1,q2,q3 being Point of TOP-REAL 2
 st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P
 & not(q1=q2 & q1=W-min(P)) & q1<>q3 & not(q2=q3 & q2=W-min(P)) holds
 Segment(q1,q2,P)/\ Segment(q2,q3,P)={q2}
  proof let P be compact non empty Subset of TOP-REAL 2,
    q1,q2,q3 be Point of TOP-REAL 2;
    assume A1: P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P
    & not(q1=q2 & q1=W-min(P)) & q1<>q3 & not(q2=q3 & q2=W-min(P));
    then A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
     thus Segment(q1,q2,P)/\ Segment(q2,q3,P) c= {q2}
     proof let x be set;
       assume x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
       then A3: x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by XBOOLE_0:def 3
;
        now per cases;
       case q3<>W-min(P);
         then x in {p: LE q2,p,P & LE p,q3,P} by A3,Def1;
         then consider p such that A4: p=x & (LE q2,p,P & LE p,q3,P);
          now per cases;
         case q2<>W-min(P);
           then x in {p2: LE q1,p2,P & LE p2,q2,P} by A3,Def1;
           then ex p2 st p2=x & (LE q1,p2,P & LE p2,q2,P);
          hence x=q2 by A1,A4,JORDAN6:72;
         case A5:q2=W-min(P);
             then q1 in Upper_Arc(P) & q2 in Upper_Arc(P) &
             LE q1,q2,Upper_Arc(P),W-min(P),E-max(P)
                             by A1,JORDAN6:def 10;
            hence contradiction by A1,A2,A5,JORDAN6:69;
         end;
        hence x=q2;
       case A6: q3=W-min(P);
        then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A3,Def1;
         then consider p1 such that
         A7:p1=x &(LE q2,p1,P or q2 in P & p1=W-min(P));
             p1 in {p: LE q1,p,P & LE p,q2,P} by A1,A3,A6,A7,Def1;
         then ex p st p=p1 & LE q1,p,P & LE p,q2,P;
        hence x=q2 by A1,A6,A7,JORDAN6:72;
       end;
      hence x in {q2} by TARSKI:def 1;
     end;
     let x be set;assume x in {q2};
     then A8: x=q2 by TARSKI:def 1;
     then A9: x in Segment(q1,q2,P) by A1,Th6;
      x in Segment(q2,q3,P) by A1,A8,Th6;
     hence thesis by A9,XBOOLE_0:def 3;
  end;

theorem Th11:
for P being compact non empty Subset of TOP-REAL 2,
 q1,q2 being Point of TOP-REAL 2
 st P is_simple_closed_curve & LE q1,q2,P
 & q1 <> W-min P & q2 <> W-min P holds
 Segment(q1,q2,P)/\ Segment(q2,W-min P,P)={q2}
  proof let P be compact non empty Subset of TOP-REAL 2,
    q1,q2 be Point of TOP-REAL 2;
   set q3 = W-min P;
    assume A1: P is_simple_closed_curve & LE q1,q2,P
    & q1<>q3 & not(q2=W-min(P));
     thus Segment(q1,q2,P)/\ Segment(q2,W-min P,P) c= {q2}
     proof let x be set;
       assume x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
       then A2: x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by XBOOLE_0:def 3
;
        then x in {p1: LE q2,p1,P or q2 in P & p1=W-min P} by Def1;
         then consider p1 such that
         A3:p1=x and
A4:       LE q2,p1,P or q2 in P & p1=W-min P;
             p1 in {p: LE q1,p,P & LE p,q2,P} by A1,A2,A3,Def1;
then A5:      ex p st p=p1 & LE q1,p,P & LE p,q2,P;
       per cases by A4;
       suppose LE q2,p1,P;
        then x=q2 by A1,A3,A5,JORDAN6:72;
      hence x in {q2} by TARSKI:def 1;
       suppose q2 in P & p1=W-min(P);
      hence x in {q2} by A1,A5,Th2;
     end;
     let x be set;assume x in {q2};
     then A6: x=q2 by TARSKI:def 1;
     then A7: x in Segment(q1,q2,P) by A1,Th6;
      q2 in P by A1,Th5;
     then x in Segment(q2,q3,P) by A1,A6,Th7;
     hence thesis by A7,XBOOLE_0:def 3;
  end;

theorem Th12: for P being compact non empty Subset of TOP-REAL 2,
 q1,q2 being Point of TOP-REAL 2
 st P is_simple_closed_curve & LE q1,q2,P & q1<>q2 & q1<>W-min(P) holds
 Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P)={W-min(P)}
 proof let P be compact non empty Subset of TOP-REAL 2,
   q1,q2 be Point of TOP-REAL 2;
   assume A1: P is_simple_closed_curve & LE q1,q2,P & q1<>q2 &
   q1<>W-min(P);
   then A2: q1 in P & q2 in P by Th5;
   thus Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P) c= {W-min(P)}
    proof let x be set;
     assume x in Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P);
      then A3: x in Segment(q2,W-min(P),P) & x in Segment(W-min(P),q1,P)
                              by XBOOLE_0:def 3;
      then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by Def1;
      then consider p1 such that A4: p1=x &(LE q2,p1,P or q2 in P & p1=W-min(P)
);
       now per cases by A4;
      case A5:LE q2,p1,P;
         x in {p: LE W-min(P),p,P & LE p,q1,P} by A1,A3,Def1;
        then ex p2 st p2=x & LE W-min(P),p2,P & LE p2,q1,P;
        then LE q2,q1,P by A1,A4,A5,JORDAN6:73;
       hence contradiction by A1,JORDAN6:72;
      case q2 in P & p1=W-min(P);
       hence x=W-min(P) by A4;
      end;
     hence x in {W-min(P)} by TARSKI:def 1;
    end;
    let x be set;assume x in {W-min(P)};
    then A6: x=W-min(P) by TARSKI:def 1;
    then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A2;
    then A7: x in Segment(q2,W-min(P),P) by Def1;
     LE W-min(P),q1,P by A1,A2,Th3;
    then x in Segment(W-min(P),q1,P) by A1,A6,Th6;
    hence thesis by A7,XBOOLE_0:def 3;
 end;

theorem Th13:
for P being compact non empty Subset of TOP-REAL 2,
  q1,q2,q3,q4 being Point of TOP-REAL 2
  st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & LE q3,q4,P
   & q1<>q2 & q2<>q3 holds
  Segment(q1,q2,P) misses Segment(q3,q4,P)
proof let P be compact non empty Subset of TOP-REAL 2,
  q1,q2,q3,q4 be Point of TOP-REAL 2;
  assume that
A1:P is_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: LE q3,q4,P and
A5: q1<>q2 and
A6: q2<>q3;
  assume A7:Segment(q1,q2,P)/\ Segment(q3,q4,P)<>{};
    consider x being Element of Segment(q1,q2,P)/\ Segment(q3,q4,P);
    A8:x in Segment(q1,q2,P) & x in Segment(q3,q4,P) by A7,XBOOLE_0:def 3;
     now per cases;
    case q4=W-min(P);
      then q3=W-min(P) by A1,A4,Th2;
     hence contradiction by A1,A3,A6,Th2;
    case q4<>W-min(P);
     then x in {p1: LE q3,p1,P & LE p1,q4,P} by A8,Def1;
     then consider p1 such that A9:p1=x &(LE q3,p1,P & LE p1,q4,P);
      q2<>W-min(P) by A1,A2,A5,Th2;
       then x in {p2: LE q1,p2,P & LE p2,q2,P} by A8,Def1;
       then consider p2 such that A10:p2=x &(LE q1,p2,P & LE p2,q2,P);
        LE q3,q2,P by A1,A9,A10,JORDAN6:73;
      hence contradiction by A1,A3,A6,JORDAN6:72;
    end;
   hence contradiction;
end;

theorem Th14:
for P being compact non empty Subset of TOP-REAL 2,
  q1,q2,q3 being Point of TOP-REAL 2
  st P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P & q1<>W-min P
   & q1<>q2 & q2<>q3 holds
  Segment(q1,q2,P) misses Segment(q3,W-min P,P)
proof let P be compact non empty Subset of TOP-REAL 2,
  q1,q2,q3 be Point of TOP-REAL 2;
  assume A1:P is_simple_closed_curve & LE q1,q2,P & LE q2,q3,P
  & q1<>W-min P & q1<>q2 & q2<>q3;
  assume A2:Segment(q1,q2,P)/\ Segment(q3,W-min P,P)<>{};
    consider x being Element of Segment(q1,q2,P)/\ Segment(q3,W-min P,P);
    A3:x in Segment(q1,q2,P) & x in Segment(q3,W-min P,P) by A2,XBOOLE_0:def 3;
     then x in {p1: LE q3,p1,P or q3 in P & p1=W-min P} by Def1;
     then consider p1 such that
A4:   p1=x and
A5:   LE q3,p1,P or q3 in P & p1=W-min P;
    q2 <> W-min P by A1,Th2;
  then x in {p: LE q1,p,P & LE p,q2,P} by A3,Def1;
  then ex p3 st p3 = x & LE q1,p3,P & LE p3,q2,P;
  then LE q3,q2,P by A1,A4,A5,Th2,JORDAN6:73;
 hence contradiction by A1,JORDAN6:72;
end;

begin :: A function to divide the simple closed curve

reserve n for Nat;

theorem Th15:
  for P being non empty Subset of TOP-REAL n,
  f being map of I[01], (TOP-REAL n)|P st P<>{} & f is_homeomorphism
  ex g being map of I[01],TOP-REAL n st f=g &
  g is continuous & g is one-to-one
proof let P be non empty Subset of TOP-REAL n,
  f be map of I[01], (TOP-REAL n)|P;
  assume A1: P<>{} & f is_homeomorphism;
      the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) by PRE_TOPC:12
         .=P by PRE_TOPC:def 10;
     then f is Function of the carrier of I[01],the carrier of TOP-REAL n
                             by FUNCT_2:9;
  then reconsider g1=f as map of I[01],TOP-REAL n;
    A2:the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) by PRE_TOPC:12;
    A3:[#]((TOP-REAL n)|P)= P  by PRE_TOPC:def 10;
    A4:f is one-to-one & f is continuous & f" is continuous
                                  by A1,TOPS_2:def 5;
   for P2 being Subset of TOP-REAL n st
    P2 is open holds g1"P2 is open
  proof let P2 be Subset of TOP-REAL n;
    assume A5: P2 is open;
     P2 /\ P is Subset of (TOP-REAL n)|P
                                    by A2,A3,XBOOLE_1:17;
    then reconsider B1=P2 /\ P as Subset of (TOP-REAL n)|P;
      B1 is open by A3,A5,TOPS_2:32;
     then A6:f"B1 is open by A4,TOPS_2:55;
     A7:f"B1 = f"P2 /\ f"P by FUNCT_1:137;
      f"(rng f) c= f"P by A2,A3,RELAT_1:178;
     then A8:dom f c= f"P by RELAT_1:169;
      f"P c= dom f by RELAT_1:167;
     then A9:f"P=dom f by A8,XBOOLE_0:def 10;
      f"P2 c= dom f by RELAT_1:167;
    hence g1"P2 is open by A6,A7,A9,XBOOLE_1:28;
  end;
  then g1 is continuous by TOPS_2:55;
 hence thesis by A4;
end;

theorem Th16:
  for P being non empty Subset of TOP-REAL n,
  g being map of I[01], (TOP-REAL n) st g is continuous one-to-one
   & rng g = P
  ex f being map of I[01],(TOP-REAL n)|P st f=g &
   f is_homeomorphism
proof let P be non empty Subset of TOP-REAL n,
  g be map of I[01], (TOP-REAL n);
  assume that
A1: g is continuous one-to-one and
A2: rng g = P;
     the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) by PRE_TOPC:12;
   then A3: the carrier of (TOP-REAL n)|P = P by PRE_TOPC:def 10;
  then g is Function of the carrier of I[01],the carrier of (TOP-REAL n)|P
                             by A2,FUNCT_2:8;
  then reconsider f=g as map of I[01],(TOP-REAL n)|P;
 take f;
 thus f = g;
A4: dom f = the carrier of I[01] by FUNCT_2:def 1
      .= [#]I[01] by PRE_TOPC:12;
A5: rng f = [#]((TOP-REAL n)|P) by A2,PRE_TOPC:def 10;
A6: [#]((TOP-REAL n)|P)= P  by PRE_TOPC:def 10;
   for P2 being Subset of (TOP-REAL n)|P st
    P2 is open holds f"P2 is open
  proof let P2 be Subset of (TOP-REAL n)|P;
   assume
A7: P2 is open;
    consider C being Subset of TOP-REAL n such that
A8:  C is open and
A9:  C /\ [#]((TOP-REAL n)|P) = P2 by A7,TOPS_2:32;
A10:   f"C c= [#]I[01] by PRE_TOPC:14;
     g"P = [#]I[01] by A3,A4,RELSET_1:38;
    then f"P2 = f"C /\ [#]I[01] by A6,A9,FUNCT_1:137
         .= f"C by A10,XBOOLE_1:28;
    hence f"P2 is open by A1,A8,TOPS_2:55;
  end;
  then A11: f is continuous by TOPS_2:55;
   (TOP-REAL n)|P is_T2 by TOPMETR:3;
 hence thesis by A1,A4,A5,A11,COMPTS_1:26;
end;

definition
 cluster increasing -> one-to-one FinSequence of REAL;
 coherence
 proof let f be FinSequence of REAL;
   assume A1:f is increasing;
    let x,y be set;assume A2: x in dom f & y in dom f & f.x=f.y;
      then reconsider nx=x,ny=y as Nat;
      A3: nx<=ny by A1,A2,GOBOARD1:def 1;
         nx>=ny by A1,A2,GOBOARD1:def 1;
     hence x=y by A3,REAL_1:def 5;
 end;
end;

theorem Th17:
 for f being FinSequence of REAL st
 f is increasing holds f is one-to-one
 proof let f be FinSequence of REAL;
   assume f is increasing;
    then reconsider f as increasing FinSequence of REAL;
    f is one-to-one;
  hence thesis;
 end;

Lm5: now
  let h2 be Nat;
   h2<h2+1 by NAT_1:38;
  then h2-1<h2+1-1 by REAL_1:54;
  then h2-1<h2 by XCMPLX_1:26;
  then h2-1-1<h2-1 & h2-1<h2 by REAL_1:54;
  hence h2-1-1<h2 by AXIOMS:22;
end;

Lm6: 0 in [.0,1.] & 1 in [.0,1.] by RCOMP_1:15;

theorem Th18:
 for A being Subset of TOP-REAL 2,
     p1,p2 being Point of TOP-REAL 2
  st A is_an_arc_of p1,p2
 ex g being map of I[01], TOP-REAL 2 st
  g is continuous one-to-one & rng g = A & g.0 = p1 & g.1 = p2
 proof let A be Subset of TOP-REAL 2,
     p1,p2 being Point of TOP-REAL 2;
  assume
A1: A is_an_arc_of p1,p2;
   then reconsider A' = A as non empty Subset of TOP-REAL 2
                     by TOPREAL1:4;
   consider f being map of I[01], (TOP-REAL 2)|A' such that
A2: f is_homeomorphism & f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 2;
A3: rng f=[#]((TOP-REAL 2)|A') by A2,TOPS_2:def 5;
   consider g being map of I[01], TOP-REAL 2 such that
A4: f=g and
A5: g is continuous one-to-one by A2,Th15;
  take g;
  thus g is continuous one-to-one by A5;
  thus rng g = A by A3,A4,PRE_TOPC:def 10;
  thus thesis by A2,A4;
 end;

theorem Th19:
 for P being non empty Subset of TOP-REAL 2,
     p1, p2, q1, q2 being Point of TOP-REAL 2,
     g being map of I[01], TOP-REAL 2,
     s1, s2 being Real st
  P is_an_arc_of p1,p2 & g is continuous one-to-one & rng g = P
  & g.0 = p1 & g.1 = p2
  & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1 & s1 <= s2
 holds LE q1,q2,P,p1,p2
proof let P be non empty Subset of TOP-REAL 2,
     p1, p2, q1, q2 be Point of TOP-REAL 2,
     g be map of I[01], TOP-REAL 2,
     s1, s2 be Real such that
A1: P is_an_arc_of p1,p2 and
A2: g is continuous one-to-one and
A3: rng g = P;
   ex f being map of I[01],(TOP-REAL 2)|P st
   f=g & f is_homeomorphism by A2,A3,Th16;
 hence thesis by A1,JORDAN5C:8;
end;

theorem Th20:
 for P being non empty Subset of TOP-REAL 2,
     p1, p2, q1, q2 being Point of TOP-REAL 2,
     g being map of I[01], TOP-REAL 2,
     s1, s2 being Real st
  g is continuous one-to-one & rng g = P
  & g.0 = p1 & g.1 = p2
  & g.s1 = q1 & 0 <= s1 & s1 <= 1 & g.s2 = q2 & 0 <= s2 & s2 <= 1
  & LE q1,q2,P,p1,p2
 holds s1 <= s2
proof
 let P be non empty Subset of TOP-REAL 2,
     p1, p2, q1, q2 be Point of TOP-REAL 2,
     g be map of I[01], TOP-REAL 2,
     s1, s2 be Real such that
A1: g is continuous one-to-one and
A2: rng g = P;
   ex f being map of I[01],(TOP-REAL 2)|P st
   f=g & f is_homeomorphism by A1,A2,Th16;
 hence thesis by JORDAN5C:def 3;
end;

theorem :: Dividing simple closed curve into segments.
  for P being compact non empty Subset of TOP-REAL 2, e being Real
   st P is_simple_closed_curve & e > 0
   ex h being FinSequence of the carrier of TOP-REAL 2
   st h.1=W-min(P) & h is one-to-one & 8<=len h & rng h c= P
   &(for i being Nat st 1<=i & i<len h holds LE h/.i,h/.(i+1),P)
   &(for i being Nat,W being Subset of Euclid 2
   st 1<=i & i<len h & W=Segment(h/.i,h/.(i+1),P) holds
   diameter(W)<e)
   & (for W being Subset of Euclid 2 st
   W=Segment(h/.len h,h/.1,P)  holds diameter(W)<e)
   & (for i being Nat st 1<=i & i+1<len h holds
    Segment(h/.i,h/.(i+1),P)/\ Segment(h/.(i+1),h/.(i+2),P)={h/.(i+1)})
   & Segment(h/.len h,h/.1,P)/\ Segment(h/.1,h/.2,P)={h/.1}
   & Segment(h/.(len h-' 1),h/.len h,P)/\ Segment(h/.len h,h/.1,P)={h/.len h}
   & Segment(h/.(len h-'1),h/.len h,P) misses Segment(h/.1,h/.2,P)
  &(for i,j being Nat st 1<=i & i < j & j < len h & not(i,j are_adjacent1)
    holds Segment(h/.i,h/.(i+1),P) misses Segment(h/.j,h/.(j+1),P))
  & (for i being Nat st 1 < i & i+1 < len h holds
      Segment(h/.len h,h/.1,P) misses Segment(h/.i,h/.(i+1),P))
 proof
   let P be compact non empty Subset of TOP-REAL 2, e be Real;
   assume
A1: P is_simple_closed_curve & e > 0;
    then A2: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
    then consider g1 being map of I[01], TOP-REAL 2 such that
A3:  g1 is continuous one-to-one and
A4: rng g1 = Upper_Arc P and
A5: g1.0 = W-min P & g1.1 = E-max P by Th18;
A6: dom g1 =[.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
A7: 0 in dom g1 & 1 in dom g1 by Lm6,BORSUK_1:83,FUNCT_2:def 1;
A8: E-max P in Upper_Arc P & W-min P in Upper_Arc P by A1,Th1;
   consider h1 being FinSequence of REAL such that
   A9: h1.1=0 & h1.len h1=1 & 5<=len h1 & rng h1 c= the carrier of I[01]
    & h1 is increasing
    &(for i being Nat,Q being Subset of I[01],
    W being Subset of Euclid 2
    st 1<=i & i<len h1 & Q=[.h1/.i,h1/.(i+1).]
    & W=g1.:Q holds diameter(W)<e) by A1,A3,A5,UNIFORM1:15;
    A10:h1 is one-to-one by A9,Th17;
A11: Lower_Arc P is_an_arc_of E-max P, W-min P by A1,JORDAN6:def 9;
    then consider g2 being map of I[01], TOP-REAL 2 such that
A12:  g2 is continuous one-to-one and
A13: rng g2 = Lower_Arc P and
A14: g2.0 = E-max P & g2.1 = W-min P by Th18;
A15: dom g2 = [.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
   consider h2 being FinSequence of REAL such that
   A16: h2.1=0 & h2.len h2=1 & 5<=len h2 & rng h2 c= the carrier of I[01]
    & h2 is increasing
    &(for i being Nat,Q being Subset of I[01],
    W being Subset of Euclid 2
    st 1<=i & i<len h2 & Q=[.h2/.i,h2/.(i+1).]
    & W=g2.:Q holds diameter(W)<e) by A1,A12,A14,UNIFORM1:15;
A17: len h2-1-1<len h2 by Lm5;
    A18:h2 is one-to-one by A16,Th17;
     h1 is FinSequence of the carrier of I[01] by A9,FINSEQ_1:def 4;
    then reconsider h11=g1*h1 as FinSequence of the carrier of TOP-REAL 2
                                                 by FINSEQ_2:36;
    A19:rng h1 c= dom g1 by A9,FUNCT_2:def 1;
    then A20:dom h1=dom h11 by RELAT_1:46;
    then A21: len h1=len h11 by FINSEQ_3:31;
     h2 is FinSequence of the carrier of I[01] by A16,FINSEQ_1:def 4;
    then reconsider h21=g2*h2 as FinSequence of the carrier of TOP-REAL 2
                                                 by FINSEQ_2:36;
     dom g2=the carrier of I[01] by FUNCT_2:def 1;
    then A22:dom h2=dom h21 by A16,RELAT_1:46;
    then A23: len h2=len h21 by FINSEQ_3:31;
A24: 1<=len h1 by A9,AXIOMS:22;
    then A25: 1 in dom h1 by FINSEQ_3:27;
A26:len h1 in dom h1 by A24,FINSEQ_3:27;
    A27: 1<=len h2 by A16,AXIOMS:22;
    then A28:1 in dom h2 by FINSEQ_3:27;
A29: len h2 in dom h2 by A27,FINSEQ_3:27;
A30: h21.1=E-max P by A14,A16,A28,FUNCT_1:23;
A31: h21.len h2=W-min P by A14,A16,A29,FUNCT_1:23;
    A32:1 in dom g2 by Lm6,BORSUK_1:83,FUNCT_2:def 1;
    A33:dom g1=[.0,1.] by BORSUK_1:83,FUNCT_2:def 1;
    then A34:1 in dom (g1*h1) by A9,A25,Lm6,FUNCT_1:21;
A35:len h1 in dom h1 by A24,FINSEQ_3:27;
     h1.len h1 in dom g1 by A9,A33,TOPREAL5:1;
    then A36:len h1 in dom (g1*h1) by A26,FUNCT_1:21;
    then A37: h11.len h1=E-max(P) by A5,A9,FUNCT_1:22;
    reconsider h0=h11^(mid(h21,2,len h21-' 1))
                as FinSequence of the carrier of TOP-REAL 2;
A38: h11.1=W-min P by A5,A9,A34,FUNCT_1:22;
   take h0;
   thus
A39: h0.1=W-min P by A34,A38,FINSEQ_1:def 7;
    A40:len h0=len h11+len (mid(h21,2,len h21 -'1)) by FINSEQ_1:35;
     2<=len h21 by A16,A23,AXIOMS:22;
then A41:1+1-1<=len h21-1 by REAL_1:49;
    then 0<=len h21-1 by AXIOMS:22;
    then A42:len h21-'1=len h21 -1 by BINARITH:def 3;
     len h21<=len h21 +1 by NAT_1:37;
    then len h21 -1<=len h21 +1-1 by REAL_1:49;
    then A43:2<=len h21 & 1<=len h21-'1 & len h21-'1<=len h21
                              by A16,A23,A41,A42,AXIOMS:22,XCMPLX_1:26;
     3<len h21 by A16,A23,AXIOMS:22;
    then 2+1-1<len h21 -1 by REAL_1:54;
    then A44:2<len h21 -'1 by A41,JORDAN3:1;
    then A45:len h21 -'1-'2=len h21 -'1-2 by SCMFSA_7:3;
    A46:len (mid(h21,2,len h21 -'1))
                          =(len h21-'1)-'2+1 by A43,A44,JORDAN3:27;
    then A47:len h0=len h1+(len h2-2) by A21,A23,A40,A42,A45,XCMPLX_1:229;
                  3+2-2<=len h2 -2 by A16,REAL_1:49;
                 then 1<=len h2 -2 by AXIOMS:22;
then A48:   len h1+1<=len h0 by A47,REAL_1:55;
        then A49:   len h0>len h1 by NAT_1:38;
       then A50:     1<len h0 by A24,AXIOMS:22;
        then A51:    len h0 in dom h0 by FINSEQ_3:27;
        then A52:    h0/.len h0=h0.len h0 by FINSEQ_4:def 4;
A53:   1<=len h0-len h1 by A48,REAL_1:84;
A54: len h0-len h11=len h0-'len h11 by A21,A49,SCMFSA_7:3;
then A55:   1<=len h0-'len h11 by A21,A48,REAL_1:84;
A56:  2<len h1 by A9,AXIOMS:22;
    then A57:2 in dom h1 by FINSEQ_3:27;
    A58: 1+1<=len h0 by A49,A56,AXIOMS:22;
    then A59:2 in dom h0 by FINSEQ_3:27;
    A60:h0.2=h11.2 by A21,A56,SCMFSA_7:9;
A61:  1 in dom h0 by A50,FINSEQ_3:27;
then A62: h0/.1 = h0.1 by FINSEQ_4:def 4;
A63: h0/.1=W-min(P) by A39,A61,FINSEQ_4:def 4;
    A64:h11 is one-to-one by A3,A10,FUNCT_1:46;
    A65:h21 is one-to-one by A12,A18,FUNCT_1:46;
   thus
A66:  h0 is one-to-one
     proof let x,y be set;assume
     A67: x in dom h0 & y in dom h0 & h0.x=h0.y;
       then reconsider nx=x,ny=y as Nat;
       A68:1<=nx & nx<=len h0 by A67,FINSEQ_3:27;
       A69:1<=ny & ny<=len h0 by A67,FINSEQ_3:27;
        now per cases;
       case nx<=len h1;
         then A70:nx in dom h1 by A68,FINSEQ_3:27;
then A71:      h1.nx in rng h1 by FUNCT_1:def 5;
         A72:h0.nx=h11.nx by A20,A70,FINSEQ_1:def 7
            .=g1.(h1.nx) by A20,A70,FUNCT_1:22;
         then A73:h0.nx in Upper_Arc(P) by A4,A19,A71,FUNCT_1:def 5;
          now per cases;
         case ny<=len h1;
           then A74:ny in dom h1 by A69,FINSEQ_3:27;
then A75:        h1.ny in rng h1 by FUNCT_1:def 5;
            h0.ny=h11.ny by A20,A74,FINSEQ_1:def 7
              .=g1.(h1.ny) by A74,FUNCT_1:23;
           then h1.nx=h1.ny by A3,A19,A67,A71,A72,A75,FUNCT_1:def 8;
          hence nx=ny by A10,A70,A74,FUNCT_1:def 8;
         case A76:ny>len h1;
           then A77:len h1 +1<=ny by NAT_1:38;
           A78:len h11+1<=ny & ny<=len h11 + len (mid(h21,2,len h21 -'1))
                                 by A21,A69,A76,FINSEQ_1:35,NAT_1:38;
           then A79:h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) by FINSEQ_1:36
;
           A80:ny-len h11=ny-'len h11 by A21,A76,SCMFSA_7:3;
A81:        ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A78,REAL_1:49;
            len h1 +1-len h1<=ny-len h1 by A77,REAL_1:49;
           then A82:1<=ny-'len h11 & ny-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A80,A81,XCMPLX_1:26;
           then A83:h0.ny=h21.(ny-'len h11 +2-'1)
                             by A43,A44,A79,A80,JORDAN3:27;
            1+1<=ny-'len h11+1 by A82,AXIOMS:24;
           then 1+1<=ny-'len h11+1+1-1 by XCMPLX_1:26;
           then A84:2<=ny-'len h11+2-1 by XCMPLX_1:1;
            0<=ny-'len h11 by NAT_1:18;
then A85:        0+2<=ny-'len h11 +2 by AXIOMS:24;
            ny-len h11<=len h1+(len h2-2)-len h11 by A47,A69,REAL_1:49;
           then ny-len h11<=(len h2-2) by A21,XCMPLX_1:26;
           then ny-'len h11+2<=len h2-2+2 by A80,AXIOMS:24;
then A86:       ny-'len h11+2<=len h2 by XCMPLX_1:27;
           then A87:ny-'len h11+2-1<=len h2-1 by REAL_1:49;
           A88:1<=(ny-'len h11 +2-'1) & (ny-'len h11 +2-'1)<=len h21
                      by A23,A85,A86,Lm2,JORDAN3:5,7;
           then A89:(ny-'len h11 +2-'1) in dom h21 by FINSEQ_3:27;
           then h0.ny in rng h21 by A83,FUNCT_1:def 5;
           then h0.ny in rng g2 by FUNCT_1:25;
           then h0.nx in Upper_Arc(P)/\ Lower_Arc(P)
                         by A13,A67,A73,XBOOLE_0:def 3;
then A90:         h0.nx in {W-min(P),E-max(P)} by A1,JORDAN6:65;
           A91:ny-'len h11+2-'1<=len h2-1 by A87,A88,JORDAN3:1;
           A92:2<=ny-'len h11+2-'1 by A84,A88,JORDAN3:1;
            now per cases by A90,TARSKI:def 2;
           case h0.nx=W-min(P);
             then h21.(ny-'len h11 +2-'1)=W-min(P)
               by A43,A44,A67,A79,A80,A82,JORDAN3:27;
             then len h21=(ny-'len h11 +2-'1)
                         by A22,A23,A29,A31,A65,A89,FUNCT_1:def 8;
             then len h21+1<=len h21-1+1 by A23,A91,AXIOMS:24;
             then len h21+1<=len h21-(1-1) by XCMPLX_1:37;
             then len h21+1-len h21<=len h21 -len h21 by REAL_1:49;
             then len h21+1-len h21<=0 by XCMPLX_1:14;
            hence contradiction by Lm1,XCMPLX_1:26;
           case h0.nx=E-max(P);
             then 1=(ny-'len h11 +2-'1)
                       by A22,A28,A30,A65,A67,A83,A89,FUNCT_1:def 8;
            hence contradiction by A92;
           end;
          hence nx=ny;
         end;
        hence nx=ny;
       case A93:nx>len h1;
         then A94:len h1 +1<=nx by NAT_1:38;
         A95:len h11+1<=nx & nx<=len h11 + len (mid(h21,2,len h21 -'1))
                            by A21,A68,A93,FINSEQ_1:35,NAT_1:38;
         then A96:h0.nx=(mid(h21,2,len h21 -'1)).(nx -len h11) by FINSEQ_1:36;
         A97:nx-len h11=nx-'len h11 by A21,A93,SCMFSA_7:3;
A98:     nx-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A95,REAL_1:49;
          len h1 +1-len h1<=nx-len h1 by A94,REAL_1:49;
         then A99:1<=nx-'len h11 & nx-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A97,A98,XCMPLX_1:26;
         then A100:h0.nx=h21.(nx-'len h11 +2-'1)
                             by A43,A44,A96,A97,JORDAN3:27;
          1+1<=nx-'len h11+1 by A99,AXIOMS:24;
         then 1+1<=nx-'len h11+1+1-1 by XCMPLX_1:26;
         then A101:2<=nx-'len h11+2-1 by XCMPLX_1:1;
          0<=nx-'len h11 by NAT_1:18;
then A102:    0+2<=nx-'len h11 +2 by AXIOMS:24;
          nx-len h11<=len h1+(len h2-2)-len h11 by A47,A68,REAL_1:49;
         then nx-len h11<=(len h2-2) by A21,XCMPLX_1:26;
         then nx-'len h11+2<=len h2-2+2 by A97,AXIOMS:24;
then A103:    nx-'len h11+2<=len h2 by XCMPLX_1:27;
         then A104:nx-'len h11+2-1<=len h2-1 by REAL_1:49;
         A105:1<=(nx-'len h11 +2-'1) & (nx-'len h11 +2-'1)<=len h21
                      by A23,A102,A103,Lm2,JORDAN3:5,7;
         then A106:(nx-'len h11 +2-'1) in dom h21 by FINSEQ_3:27;
         then h0.nx in rng h21 by A100,FUNCT_1:def 5;
         then A107:h0.nx in Lower_Arc(P) by A13,FUNCT_1:25;
          now per cases;
         case ny<=len h1;
           then A108:ny in dom h1 by A69,FINSEQ_3:27;
then A109:      h1.ny in rng h1 by FUNCT_1:def 5;
            h0.ny=h11.ny by A20,A108,FINSEQ_1:def 7
              .=g1.(h1.ny) by A20,A108,FUNCT_1:22;
           then h0.ny in rng g1 by A19,A109,FUNCT_1:def 5;
           then h0.ny in Upper_Arc(P)/\ Lower_Arc(P) by A4,A67,A107,XBOOLE_0:
def 3;
           then A110:       h0.ny in {W-min(P),E-max(P)} by A1,JORDAN6:65;
           A111:nx-'len h11+2-'1<=len h2-1 by A104,A105,JORDAN3:1;
           A112:2<=nx-'len h11+2-'1 by A101,A105,JORDAN3:1;
            now per cases by A110,TARSKI:def 2;
           case h0.ny=W-min(P);
             then len h21=(nx-'len h11 +2-'1)
                     by A22,A23,A29,A31,A65,A67,A100,A106,FUNCT_1:def 8;
             then len h21+1<=len h21-1+1 by A23,A111,AXIOMS:24;
             then len h21+1<=len h21-(1-1) by XCMPLX_1:37;
             then len h21+1-len h21<=len h21 -len h21 by REAL_1:49;
             then len h21+1-len h21<=0 by XCMPLX_1:14;
            hence contradiction by Lm1,XCMPLX_1:26;
           case h0.ny=E-max(P);
             then h21.(nx-'len h11 +2-'1)=E-max(P)
               by A43,A44,A67,A96,A97,A99,JORDAN3:27;
             then 1=(nx-'len h11 +2-'1)
                         by A22,A28,A30,A65,A106,FUNCT_1:def 8;
            hence contradiction by A112;
           end;
          hence nx=ny;
         case A113:ny>len h1;
           then A114:len h1 +1<=ny by NAT_1:38;
           then A115:h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11)
             by A21,A40,A69,FINSEQ_1:36;
           A116:ny-len h11=ny-'len h11 by A21,A113,SCMFSA_7:3;
            ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
             by A40,A69,REAL_1:49;
           then A117:ny-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
            len h1 +1-len h1<=ny-len h1 by A114,REAL_1:49;
           then 1<=ny-len h11 by A21,XCMPLX_1:26;
           then A118:h0.ny=h21.(ny-'len h11 +2-'1)
                             by A43,A44,A115,A116,A117,JORDAN3:27;
            0<=ny-'len h11 by NAT_1:18;
then A119:        0+2<=ny-'len h11 +2 by AXIOMS:24;
            ny-len h11<=len h1+(len h2-2)-len h11 by A47,A69,REAL_1:49;
           then ny-len h11<=(len h2-2) by A21,XCMPLX_1:26;
           then ny-'len h11+2<=len h2-2+2 by A116,AXIOMS:24;
           then ny-'len h11+2<=len h2 by XCMPLX_1:27;
           then A120:1<=(ny-'len h11 +2-'1) & (ny-'len h11 +2-'1)<=len h21
                         by A23,A119,Lm2,JORDAN3:5,7;
           then (ny-'len h11 +2-'1) in dom h21 by FINSEQ_3:27;
           then nx-'len h1+2-'1=ny-'len h1+2-'1
                           by A21,A65,A67,A100,A106,A118,FUNCT_1:def 8;
           then nx-'len h1+2-1=ny-'len h1+2-'1 by A21,A105,JORDAN3:1;
           then nx-'len h1+2-1=ny-'len h1+2-1 by A21,A120,JORDAN3:1;
           then nx-'len h1+(2-1)=ny-'len h1+2-1 by XCMPLX_1:29;
           then nx-'len h1+(2-1)=ny-'len h1+(2-1) by XCMPLX_1:29;
           then nx-'len h1=ny-'len h1+(2-1)-(2-1) by XCMPLX_1:26;
           then nx-len h1=ny-len h1 by A21,A97,A116,XCMPLX_1:26;
           then len h1+nx-len h1=len h1+(ny-len h1) by XCMPLX_1:29;
           then nx=len h1+(ny-len h1) by XCMPLX_1:26;
           then nx=len h1+ny-len h1 by XCMPLX_1:29;
          hence nx=ny by XCMPLX_1:26;
         end;
        hence nx=ny;
       end;
      hence x=y;
     end;
then A121: h0/.len h0 <> W-min P by A24,A39,A49,A51,A52,A61,FUNCT_1:def 8;
     3+2-2<=len h2 -2 by A16,REAL_1:49;
    then 5+3<=len h1+(len h2 -2) by A9,REAL_1:55;
   hence
A122: 8<=len h0 by A21,A23,A40,A42,A45,A46,XCMPLX_1:229;
     A123:rng (g1*h1) c= rng g1 by RELAT_1:45;
     A124:rng (mid(h21,2,len h21 -'1)) c= rng h21 by JORDAN3:28;
      rng (g2*h2) c= rng g2 by RELAT_1:45;
     then rng (mid(h21,2,len h21 -'1)) c= rng g2 by A124,XBOOLE_1:1;
     then rng h11 \/ rng (mid(h21,2,len h21 -'1)) c= Upper_Arc(P) \/
 Lower_Arc(P)
                 by A4,A13,A123,XBOOLE_1:13;
     then rng h0 c=Upper_Arc(P) \/ Lower_Arc(P) by FINSEQ_1:44;
   hence rng h0 c= P by A1,JORDAN6:def 9;
   thus for i being Nat st 1<=i & i<len h0 holds LE h0/.i,h0/.(i+1),P
     proof let i be Nat;assume A125: 1<=i & i<len h0;
       then A126:i+1<=len h0 by NAT_1:38;
       A127:1<i+1 by A125,NAT_1:38;
       A128:i<i+1 by NAT_1:38;
        now per cases;
       case A129:i<len h1;
         then A130:i+1<=len h1 by NAT_1:38;
         A131:h0.i=h11.i by A21,A125,A129,SCMFSA_7:9;
         A132:i in dom h1 by A125,A129,FINSEQ_3:27;
         then A133:h0.i=g1.(h1.i) by A131,FUNCT_1:23;
A134:      h1.i in rng h1 by A132,FUNCT_1:def 5;
         then A135:0<=h1.i & h1.i<=1 by A9,BORSUK_1:83,TOPREAL5:1;
         A136:h0.(i+1)=h11.(i+1) by A21,A127,A130,SCMFSA_7:9;
         A137:i+1 in dom h1 by A127,A130,FINSEQ_3:27;
         then A138:h0.(i+1)=g1.(h1.(i+1)) by A136,FUNCT_1:23;
A139:    h1.(i+1) in rng h1 by A137,FUNCT_1:def 5;
         then A140:0<=h1.(i+1) & h1.(i+1)<=1 by A9,BORSUK_1:83,TOPREAL5:1;
         A141:h1.i<h1.(i+1) by A9,A128,A132,A137,GOBOARD1:def 1;
          i in dom h0 by A125,FINSEQ_3:27;
         then A142:h0/.i=h0.i by FINSEQ_4:def 4;
          i+1 in dom h0 by A126,A127,FINSEQ_3:27;
         then A143:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
         A144:g1.(h1.i) in rng g1
            by A6,A9,A134,BORSUK_1:83,FUNCT_1:def 5;
         A145:h0.(i+1) in Upper_Arc(P)
         by A4,A6,A9,A138,A139,BORSUK_1:83,FUNCT_1:def 5;
          LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
            by A2,A3,A4,A5,A133,A135,A138,A140,A141,A142,A143,Th19;
        hence LE h0/.i,h0/.(i+1),P
          by A4,A133,A142,A143,A144,A145,JORDAN6:def 10;
       case A146: i>=len h1;
          now per cases by A146,REAL_1:def 5;
         case A147:i>len h1;
           then A148:len h1 +1<=i by NAT_1:38;
           len h11+1<=i by A21,A147,NAT_1:38;
           then A149:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11)
                       by A40,A125,FINSEQ_1:36;
           A150:i-len h11=i-'len h11 by A21,A147,SCMFSA_7:3;
A151:        i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                 by A40,A125,REAL_1:49;
            len h1 +1-len h1<=i-len h1 by A148,REAL_1:49;
           then 1<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A150,A151,XCMPLX_1:26;
           then A152:h0.i=h21.(i-'len h11 +2-'1)
                             by A43,A44,A149,A150,JORDAN3:27;
           A153:len h1 +1<=i+1 by A148,NAT_1:38;
           then A154:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                                      by A21,A40,A126,FINSEQ_1:36;
            i+1>len h11 by A21,A147,NAT_1:38;
           then A155:i+1-len h11=i+1-'len h11 by SCMFSA_7:3;
A156:      i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                  by A40,A126,REAL_1:49;
            len h1 +1-len h1<=i+1-len h1 by A153,REAL_1:49;
           then A157:1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A155,A156,XCMPLX_1:26;
           then A158:h0.(i+1)=h21.(i+1-'len h11 +2-'1)
                    by A43,A44,A154,A155,JORDAN3:27;
            1<i+1-'len h11+(2-1) by A157,NAT_1:38;
           then 1<i+1-'len h11+2-1 by XCMPLX_1:29;
then A159:       0<i+1-'len h11+2-1 by AXIOMS:22;
           then A160:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3;
            0<=i-'len h11 by NAT_1:18;
then A161:        0+2<=i-'len h11 +2 by AXIOMS:24;
            i-len h11<=len h1+(len h2-2)-len h11 by A47,A125,REAL_1:49;
           then i-len h11<=len h2-2 by A21,XCMPLX_1:26;
           then i-'len h11+2<=len h2-2+2 by A150,AXIOMS:24;
then A162:      i-'len h11+2<=len h2 by XCMPLX_1:27;
           then A163:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                          by A23,A161,Lm2,JORDAN3:5,7;
           set j=i-'len h11+2-'1;
A164:      j+1=i-'len h11+(1+1)-1+1 by A163,JORDAN3:1
               .=i-'len h11+1+1-1+1 by XCMPLX_1:1
               .=i-'len h11+1+1 by XCMPLX_1:26
               .=i-'len h11+(1+1) by XCMPLX_1:1
               .=i-'len h11+2;
           A165:j+1=i-len h11+2-1+1 by A150,A163,JORDAN3:1
               .=1+(i-len h11+(2-1)) by XCMPLX_1:29
               .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8
               .=(i+1)+-len h11+(2-1) by XCMPLX_1:1
               .=i+1-len h11+(2-1) by XCMPLX_0:def 8
               .=i+1-len h11+2-1 by XCMPLX_1:29
               .=i+1-'len h11+2-'1 by A155,A159,BINARITH:def 3;
           A166:j in dom h2 by A22,A163,FINSEQ_3:27;
           then A167:h0.i=g2.(h2.j) by A152,FUNCT_1:23;
A168:      h2.j in rng h2 by A166,FUNCT_1:def 5;
           then A169:0<=h2.j & h2.j<=1 by A16,BORSUK_1:83,TOPREAL5:1;
           A170:j<j+1 by NAT_1:38;
           A171:1<j+1 by A163,NAT_1:38;
           then A172:j+1 in dom h2 by A162,A164,FINSEQ_3:27;
           then A173:h0.(i+1)=g2.(h2.(j+1)) by A158,A165,FUNCT_1:23;
A174:      h2.(j+1) in rng h2 by A172,FUNCT_1:def 5;
           then A175:0<=h2.(j+1) & h2.(j+1)<=1 by A16,BORSUK_1:83,TOPREAL5:1;
           A176:h2.j<h2.(j+1) by A16,A166,A170,A172,GOBOARD1:def 1;
            i in dom h0 by A125,FINSEQ_3:27;
           then A177:h0/.i=h0.i by FINSEQ_4:def 4;
            i+1 in dom h0 by A126,A127,FINSEQ_3:27;
           then A178:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
           A179:h0.i in Lower_Arc(P)
              by A13,A15,A16,A167,A168,BORSUK_1:83,FUNCT_1:def 5;
           A180:h0.(i+1) in Lower_Arc(P)
             by A13,A15,A16,A173,A174,BORSUK_1:83,FUNCT_1:def 5;
            i+1-len h11<=len h1+(len h2-2)-len h11 by A47,A126,REAL_1:49;
           then i+1-'len h11<=len h2-2 by A21,A155,XCMPLX_1:26;
           then i+1-'len h11+2<=len h2-2+2 by AXIOMS:24;
           then i+1-'len h11+2<=len h2 by XCMPLX_1:27;
           then A181:i+1-'len h11+2-1<=len h2-1 by REAL_1:49;
            len h2<len h2+1 by NAT_1:38;
           then len h2-1<len h2+1-1 by REAL_1:54;
           then len h2-1<len h2 by XCMPLX_1:26;
           then i+1-'len h11+2-'1<len h2 by A160,A181,AXIOMS:22;
           then A182:i+1-'len h11+2-'1 in dom h2 by A165,A171,FINSEQ_3:27;
A183:      now assume h0/.(i+1)=W-min(P);
             then len h21=(i+1-'len h11 +2-'1)
                   by A22,A23,A29,A31,A65,A158,A178,A182,FUNCT_1:def 8;
             then len h21+1<=len h21-1+1 by A23,A160,A181,AXIOMS:24;
             then len h21+1<=len h21-(1-1) by XCMPLX_1:37;
             then len h21+1-len h21<=len h21 -len h21 by REAL_1:49;
             then len h21+1-len h21<=0 by XCMPLX_1:14;
            hence contradiction by Lm1,XCMPLX_1:26;
           end;
            LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P)
            by A11,A12,A13,A14,A167,A169,A173,A175,A176,A177,A178,Th19;
          hence LE h0/.i,h0/.(i+1),P
            by A177,A178,A179,A180,A183,JORDAN6:def 10;
         case A184:i=len h1;
          then A185:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                                 by A21,A40,A126,FINSEQ_1:36;
           A186:i+1-len h11=i+1-'len h11 by A21,A128,A184,SCMFSA_7:3;
            i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                               by A40,A126,REAL_1:49;
           then A187:i+1-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
            1<=i+1-len h11 by A21,A184,XCMPLX_1:26;
           then A188:h0.(i+1)=h21.(i+1-'len h11 +2-'1)
                    by A43,A44,A185,A186,A187,JORDAN3:27;
           A189:h0.i=h11.i by A21,A125,A184,SCMFSA_7:9;
            i in dom h1 by A125,A184,FINSEQ_3:27;
           then A190:h0.i=E-max(P) by A5,A9,A184,A189,FUNCT_1:23;
            i in dom h0 by A125,FINSEQ_3:27;
           then h0/.i=E-max(P) by A190,FINSEQ_4:def 4;
           then A191:h0/.i in Upper_Arc(P) by A1,Th1;
           set j=i-'len h11+2-'1;
           len h11-'len h11= len h11-len h11 by SCMFSA_7:3.=0
                              by XCMPLX_1:14;
then A192:      j=2-1 by A21,A184,SCMFSA_7:3;
           then A193:j+1<=len h2 by A16,AXIOMS:22;
           A194:i+1-'len h11+2-'1=1+2-'1 by A21,A184,BINARITH:39
           .=2 by BINARITH:39;
           A195:j+1 in dom h2 by A192,A193,FINSEQ_3:27;
           then A196:h0.(i+1)=g2.(h2.(j+1)) by A188,A192,A194,FUNCT_1:23;
A197:      h2.(j+1) in rng h2 by A195,FUNCT_1:def 5;
            i+1 in dom h0 by A126,A127,FINSEQ_3:27;
           then A198:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
           A199:h0.(i+1) in Lower_Arc(P)
              by A13,A15,A16,A196,A197,BORSUK_1:83,FUNCT_1:def 5;
            2<=len h21 by A16,A23,AXIOMS:22;
           then A200:2 in dom h21 by FINSEQ_3:27;
           len h21 <> i+1-'len h11 +2-'1 by A16,A23,A194;
           then h0/.(i+1) <> W-min P
            by A22,A23,A29,A31,A65,A188,A194,A198,A200,FUNCT_1:def 8;
          hence LE h0/.i,h0/.(i+1),P by A191,A198,A199,JORDAN6:def 10;
         end;
        hence LE h0/.i,h0/.(i+1),P;
       end;
      hence LE h0/.i,h0/.(i+1),P;
     end;
    thus for i being Nat,W being Subset of Euclid 2
      st 1<=i & i<len h0 & W=Segment(h0/.i,h0/.(i+1),P) holds
      diameter(W)<e
     proof let i be Nat,W be Subset of Euclid 2;
      assume
       A201:1<=i & i<len h0 & W=Segment(h0/.i,h0/.(i+1),P);
       then A202:i+1<=len h0 by NAT_1:38;
       A203:1<i+1 by A201,NAT_1:38;
       A204:i<i+1 by NAT_1:38;
        now per cases by REAL_1:def 5;
       case A205:i<len h1;
         then A206:i+1<=len h1 by NAT_1:38;
         A207:h0.i=h11.i by A21,A201,A205,SCMFSA_7:9;
         A208:i in dom h1 by A201,A205,FINSEQ_3:27;
         then A209:h11.i=g1.(h1.i) by FUNCT_1:23;
         then A210:h0.i=g1.(h1.i) by A21,A201,A205,SCMFSA_7:9;
A211:    h1.i in rng h1 by A208,FUNCT_1:def 5;
         then A212:0<=h1.i & h1.i<=1 by A9,BORSUK_1:83,TOPREAL5:1;
         A213:h0.(i+1)=h11.(i+1) by A21,A203,A206,SCMFSA_7:9;
         A214:i+1 in dom h1 by A203,A206,FINSEQ_3:27;
         then A215:h0.(i+1)=g1.(h1.(i+1)) by A213,FUNCT_1:23;
A216:      h1.(i+1) in rng h1 by A214,FUNCT_1:def 5;
         then A217:0<=h1.(i+1) & h1.(i+1)<=1 by A9,BORSUK_1:83,TOPREAL5:1;
         A218:h1.i<h1.(i+1) by A9,A204,A208,A214,GOBOARD1:def 1;
          i in dom h0 by A201,FINSEQ_3:27;
         then A219:h0/.i=h0.i by FINSEQ_4:def 4;
          i+1 in dom h0 by A202,A203,FINSEQ_3:27;
         then A220:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
         A221:h0.i in Upper_Arc(P)
             by A4,A6,A9,A210,A211,BORSUK_1:83,FUNCT_1:def 5;
         A222:h0.(i+1) in Upper_Arc(P)
           by A4,A6,A9,A215,A216,BORSUK_1:83,FUNCT_1:def 5;
          A223:h1/.i=h1.i by A201,A205,FINSEQ_4:24;
          A224:h1/.(i+1)=h1.(i+1) by A203,A206,FINSEQ_4:24;
         then reconsider Q1=[.h1/.i,h1/.(i+1).]
          as Subset of I[01]
             by A9,A211,A216,A223,BORSUK_1:83,RCOMP_1:16;
         A225:Segment(h0/.i,h0/.(i+1),P) c= g1.:([.h1/.i,h1/.(i+1).])
          proof let x be set;assume
           A226:x in Segment(h0/.i,h0/.(i+1),P);
A227:         h0/.(i+1) <> W-min P
               by A20,A25,A38,A64,A203,A213,A214,A220,FUNCT_1:def 8;
            then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A226,Def1;
            then consider p being Point of TOP-REAL 2 such that
            A228:p=x & (LE h0/.i,p,P & LE p,h0/.(i+1),P);
       A229:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or
            h0/.i in Upper_Arc(P) & p in Upper_Arc(P) &
             LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) or
            h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) &
             LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P)
                                   by A228,JORDAN6:def 10;
            A230:p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P) or
            p in Upper_Arc(P) & h0/.(i+1) in Upper_Arc(P) &
             LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) or
            p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)&
             LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P)
                                   by A228,JORDAN6:def 10;
             now per cases by A206,REAL_1:def 5;
            case i+1<len h1;
             then A231:         h0/.(i+1) <> E-max P
                       by A20,A26,A37,A64,A213,A214,A220,FUNCT_1:def 8;
A232:            now assume h0/.(i+1) in Lower_Arc(P);
                  then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P)
                             by A220,A222,XBOOLE_0:def 3;
                  then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                 hence contradiction by A227,A231,TARSKI:def 2;
                end;
              then A233:p in Upper_Arc(P) & h0/.(i+1) in Upper_Arc(P)
                by A228,JORDAN6:def 10;
A234:           LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
                   by A228,A232,JORDAN6:def 10;
                then A235:         p<>E-max(P) by A2,A231,JORDAN6:70;
               now per cases by A201,REAL_1:def 5;
              case i>1;
then A236:        h0/.i <> W-min P
                  by A20,A25,A38,A64,A208,A209,A210,A219,FUNCT_1:def 8;
A237:         h11.i <> E-max(P) by A20,A26,A37,A64,A205,A208,FUNCT_1:def 8;
                 now assume h0/.i in Lower_Arc(P);
                  then h0/.i in Upper_Arc(P)/\ Lower_Arc(P)
                             by A219,A221,XBOOLE_0:def 3;
                  then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                 hence contradiction by A207,A219,A236,A237,TARSKI:def 2;
                end;
                then A238:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)
                 & not p=W-min(P) or
                h0/.i in Upper_Arc(P) & p in Upper_Arc(P) &
                LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P)
                  by A228,JORDAN6:def 10;
then A239:            p <> W-min P by A2,A236,JORDAN6:69;
A240:             now assume p in Lower_Arc(P);
                  then p in Upper_Arc(P)/\ Lower_Arc(P) by A233,XBOOLE_0:def 3
;
                then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                 hence contradiction by A235,A239,TARSKI:def 2;
                end;
                  then consider z being set such that A241:z in dom g1 & p=g1.z
                                   by A4,A238,FUNCT_1:def 5;
                  reconsider rz=z as Real by A6,A241;
                A242:g1.(h1/.i)=h0/.i by A201,A205,A207,A209,A219,FINSEQ_4:24;
                  A243:0<=h1/.i & h1/.i<=1 &
                   g1.(h1/.(i+1))=h0/.(i+1)
                by A201,A203,A205,A206,A212,A215,A220,FINSEQ_4:24;
                    h1.(i+1) in rng h1 by A214,FUNCT_1:def 5;
              then A244:0<=h1/.(i+1) & h1/.(i+1)<=1
                by A9,A224,BORSUK_1:83,TOPREAL5:1;
               take rz;
               thus rz in dom g1 by A241;
                   A245:0<=rz & rz<=1 by A6,A241,TOPREAL5:1;
                   then A246:h1/.i<=rz
                  by A3,A4,A5,A238,A240,A241,A242,A243,Th20;
                    rz<=h1/.(i+1)
                    by A3,A4,A5,A234,A241,A243,A244,A245,Th20;
               hence rz in [.h1/.i,h1/.(i+1).] by A246,TOPREAL5:1;
               thus x = g1.rz by A228,A241;
              case A247:i=1;
                 now per cases;
                case A248:p<>W-min(P);
               now assume p in Lower_Arc(P);
                    then p in Upper_Arc(P)/\ Lower_Arc(P) by A233,XBOOLE_0:def
3;
                    then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                   hence contradiction by A235,A248,TARSKI:def 2;
                  end;
                  then consider z being set such that A249:z in dom g1 & p=g1.z
                                   by A4,A229,FUNCT_1:def 5;
                  reconsider rz=z as Real by A6,A249;
              take rz;
              A250:g1.(h1/.(1+1))=h0/.(1+1)
                  by A206,A215,A220,A247,FINSEQ_4:24;
                    h1.(1+1) in rng h1 by A214,A247,FUNCT_1:def 5;
              then A251:0<=h1/.(1+1) & h1/.(1+1)<=1
              by A9,A224,A247,BORSUK_1:83,TOPREAL5:1;
                   A252:0<=rz & rz<=1 by A6,A249,TOPREAL5:1;
         A253:h1/.1<=rz by A6,A9,A223,A247,A249,TOPREAL5:1;
                    rz<=h1/.(1+1)
                   by A3,A4,A5,A234,A247,A249,A250,A251,A252,Th20;
                 hence rz in dom g1
                      & rz in [.h1/.1,h1/.(1+1).]
                      & x = g1.rz by A228,A249,A253,TOPREAL5:1;
                case A254:p=W-min(P);
                 thus 0 in [.h1/.1,h1/.(1+1).]
                    by A9,A218,A223,A224,A247,TOPREAL5:1;
                 thus x = g1.0 by A5,A228,A254;
                end;
               hence ex y being set st y in dom g1 &
               y in [.h1/.1,h1/.(1+1).] & x = g1.y by A7;
              end;
             hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).]
              & x = g1.y;
            case A255:i+1=len h1;
              then A256:h0/.(i+1)=E-max(P)
                by A5,A9,A26,A213,A220,FUNCT_1:23;
              A257:p in Upper_Arc(P) or p in Lower_Arc(P)
              by A228,JORDAN6:def 10;
A258:           now assume A259:p in Lower_Arc(P)& not p in Upper_Arc(P);
                then LE h0/.(i+1),p,Lower_Arc(P),E-max(P),W-min(P)
                   by A11,A256,JORDAN5C:10;
               hence contradiction by A8,A11,A230,A256,A259,JORDAN5C:12;
              end;
              then A260:LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
                               by A2,A256,A257,JORDAN5C:10;
               now per cases;
              case A261:p<>E-max(P);
                 now per cases;
                case A262:p<>W-min(P);
A263:               now assume p in Lower_Arc(P);
                    then p in Upper_Arc(P)/\ Lower_Arc(P) by A258,XBOOLE_0:def
3;
                    then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                   hence contradiction by A261,A262,TARSKI:def 2;
                  end;
                  then consider z being set such that A264:z in dom g1 & p=g1.z
                                   by A4,A229,FUNCT_1:def 5;
                  reconsider rz=z as Real by A6,A264;
                 take rz;
A265:             g1.(h1/.(i+1))=h0/.(i+1) by A203,A206,A215,A220,FINSEQ_4:24;
                    h1.(i+1) in rng h1 by A214,FUNCT_1:def 5;
              then A266:0<=h1/.(i+1) & h1/.(i+1)<=1
              by A9,A224,BORSUK_1:83,TOPREAL5:1;
                   A267:0<=rz & rz<=1 by A6,A264,TOPREAL5:1;
                   then A268:h1/.i<=rz
                    by A3,A4,A5,A207,A209,A212,A219,A223,A229,A263,A264,Th20;
                    rz<=h1/.(i+1)
         by A3,A4,A5,A260,A264,A265,A266,A267,Th20;
                 hence rz in dom g1 &
                 rz in [.h1/.i,h1/.(i+1).]
                      & x = g1.rz by A228,A264,A268,TOPREAL5:1;
                case A269:p=W-min(P);
                  then h11.i=W-min(P) by A2,A207,A219,A229,JORDAN6:69;
                  then i=1 by A20,A25,A38,A64,A208,FUNCT_1:def 8;
                  then 0 in [.h1/.i,h1/.(i+1).]
                    by A9,A218,A223,A224,TOPREAL5:1;
                 hence ex y being set st y in dom g1 &
                 y in [.h1/.i,h1/.(i+1).]
                     & x = g1.y by A5,A7,A228,A269;
                end;
               hence ex y being set st y in dom g1 &
               y in [.h1/.i,h1/.(i+1).] & x = g1.y;
               case A270:p=E-max(P);
                 1 in [.h1/.i,h1/.(i+1).]
                 by A9,A218,A223,A224,A255,TOPREAL5:1;
               hence ex y being set st
                y in dom g1 & y in [.h1/.i,h1/.(i+1).]
                  & x = g1.y by A5,A33,A228,A270,Lm6;
               end;
              hence ex y being set st y in dom g1 & y in [.h1/.i,
              h1/.(i+1).] & x = g1.y;
            end;
           hence x in g1.:([.h1/.i,h1/.(i+1).]) by FUNCT_1:def 12;
          end;
          g1.:([.h1/.i,h1/.(i+1).]) c= Segment(h0/.i,h0/.(i+1),P)
          proof let x be set;assume x in g1.:([.h1/.i,h1/.(i+1).]);
            then consider y being set such that
      A271: y in dom g1 & y in [.h1/.i,h1/.(i+1).] & x=g1.y by FUNCT_1:def 12;
            A272:x in Upper_Arc(P) by A4,A271,FUNCT_1:def 5;
            then reconsider p1=x as Point of TOP-REAL 2;
            reconsider sy=y as Real by A271;
             A273:g1.(h1/.i)=h0/.i by A201,A205,A210,A219,FINSEQ_4:24;
             A274:h1/.i<=sy & sy<=h1/.(i+1) by A271,TOPREAL5:1;
             A275:0<=h1/.i & h1/.i<=1 by A201,A205,A212,FINSEQ_4:24;
             A276:0<=sy & sy<=1 by A6,A271,TOPREAL5:1;
             then A277:             LE h0/.i,p1,Upper_Arc(P),W-min(P),E-max(P)
              by A2,A3,A4,A5,A271,A273,A274,A275,Th19;
              LE p1,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
           by A2,A3,A4,A5,A215,A217,A220,A224,A271,A274,A276,Th19;
                           then A278: LE h0/.i,p1,P & LE p1,h0/.(i+1),P
                       by A219,A220,A221,A222,A272,A277,JORDAN6:def 10;
A279:       not h0/.(i+1)=W-min P
               by A20,A25,A38,A64,A203,A213,A214,A220,FUNCT_1:def 8;
             x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A278;
           hence x in Segment(h0/.i,h0/.(i+1),P) by A279,Def1;
          end;
         then W=g1.:Q1 by A201,A225,XBOOLE_0:def 10;
        hence diameter(W)<e by A9,A201,A205;
       case A280:i>len h1;
           then A281:len h1 +1<=i by NAT_1:38;
            len h11+1<=i & i<=len h11 + len (mid(h21,2,len h21 -'1))
                                 by A21,A201,A280,FINSEQ_1:35,NAT_1:38;
           then A282:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by FINSEQ_1:36;
           A283:i-len h11=i-'len h11 by A21,A280,SCMFSA_7:3;
A284:       i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                      by A40,A201,REAL_1:49;
            len h1 +1-len h1<=i-len h1 by A281,REAL_1:49;
           then 1<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A283,A284,XCMPLX_1:26;
           then A285:h0.i=h21.(i-'len h11 +2-'1)
                             by A43,A44,A282,A283,JORDAN3:27;
           A286:len h1 +1<=i+1 by A281,NAT_1:38;
           then A287:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                                      by A21,A40,A202,FINSEQ_1:36;
            i+1>len h11 by A21,A280,NAT_1:38;
           then A288:i+1-len h11=i+1-'len h11 by SCMFSA_7:3;
A289:       i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A202,REAL_1:49;
            len h1 +1-len h1<=i+1-len h1 by A286,REAL_1:49;
           then A290:1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A288,A289,XCMPLX_1:26;
           then A291:h0.(i+1)=h21.(i+1-'len h11 +2-'1)
                    by A43,A44,A287,A288,JORDAN3:27;
            1<i+1-'len h11+(2-1) by A290,NAT_1:38;
           then 1<i+1-'len h11+2-1 by XCMPLX_1:29;
           then 0<i+1-'len h11+2-1 by AXIOMS:22;
           then A292:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3;
            0<=i-'len h11 by NAT_1:18;
then A293:      0+2<=i-'len h11 +2 by AXIOMS:24;
            i-len h11<=len h1+(len h2-2)-len h11 by A47,A201,REAL_1:49;
           then i-len h11<=(len h2-2) by A21,XCMPLX_1:26;
           then i-'len h11+2<=len h2-2+2 by A283,AXIOMS:24;
then A294:      i-'len h11+2<=len h2 by XCMPLX_1:27;
           then A295:i-'len h11+2-1<=len h2-1 by REAL_1:49;
           A296:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                         by A23,A293,A294,Lm2,JORDAN3:5,7;
            len h2<len h2+1 by NAT_1:38;
           then len h2-1<len h2+1-1 by REAL_1:54;
           then len h2-1<len h2 by XCMPLX_1:26;
           then A297:i-'len h11+2-1<len h2 by A295,AXIOMS:22;
           A298:i-'len h11+2-'1=i-'len h11+2-1 by A296,JORDAN3:1;
           set j=i-'len h11+2-'1;
            len h1 +1<=i by A280,NAT_1:38;
           then len h11+1-len h11<=i-len h11 by A21,REAL_1:49;
           then 1<=i-len h11 by XCMPLX_1:26;
           then 1<=i-'len h11 by JORDAN3:1;
           then 1+2<=i-'len h11+2 by AXIOMS:24;
           then 1+2-1<=i-'len h11+2-1 by REAL_1:49;
           then A299:1<j by A298,AXIOMS:22;
            i-len h11<len h11+(len h2-2)-len h11 by A21,A47,A201,REAL_1:54;
           then i-len h11<len h2-2 by XCMPLX_1:26;
then A300:       i-len h11+2<len h2-2+2 by REAL_1:53;
           A301:j< len h2 by A296,A297,JORDAN3:1;
           A302:j+1=i-'len h11+(1+1)-1+1 by A296,JORDAN3:1
               .=i-'len h11+1+1-1+1 by XCMPLX_1:1
               .=i-'len h11+1+1 by XCMPLX_1:26
               .=i-'len h11+(1+1) by XCMPLX_1:1;
           then A303:j+1<len h2 by A283,A300,XCMPLX_1:27;
           A304:j+1 =1+(i-len h11+(2-1)) by A283,A298,XCMPLX_1:29
               .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8
               .=(i+1)+-len h11+(2-1) by XCMPLX_1:1
               .=i+1-len h11+(2-1) by XCMPLX_0:def 8
               .=i+1-'len h11+2-'1 by A288,A292,XCMPLX_1:29;
           A305:j in dom h2 by A22,A296,FINSEQ_3:27;
           then A306:h0.i=g2.(h2.j) by A285,FUNCT_1:23;
A307:        h2.j in rng h2 by A305,FUNCT_1:def 5;
           A308:1<j+1 by A296,NAT_1:38;
           then A309:j+1 in dom h2 by A294,A302,FINSEQ_3:27;
then A310:      h0.(i+1)=g2.(h2.(j+1)) by A291,A304,FUNCT_1:23;
A311:        h2.(j+1) in rng h2 by A309,FUNCT_1:def 5;
            i in dom h0 by A201,FINSEQ_3:27;
           then A312:h0/.i=h0.i by FINSEQ_4:def 4;
            i+1 in dom h0 by A202,A203,FINSEQ_3:27;
           then A313:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
            g2.(h2.j) in rng g2 by A15,A16,A307,BORSUK_1:83,FUNCT_1:def 5;
           then A314:h0.i in Lower_Arc(P) by A13,A285,A305,FUNCT_1:23;
           A315:h0.(i+1) in Lower_Arc(P)
            by A13,A15,A16,A310,A311,BORSUK_1:83,FUNCT_1:def 5;
A316: 0 <= h2.j by A16,A307,BORSUK_1:83,TOPREAL5:1;
A317: h2.j <= 1 by A16,A307,BORSUK_1:83,TOPREAL5:1;
A318: g2.(h2.(j+1)) = h0/.(i+1) by A291,A304,A309,A313,FUNCT_1:23;
A319: h2.(j+1) <= 1 by A16,A311,BORSUK_1:83,TOPREAL5:1;
          A320:h2/.j=h2.j by A296,A301,FINSEQ_4:24;
          A321:h2/.(j+1)=h2.(j+1) by A294,A302,A308,FINSEQ_4:24;
         then reconsider Q1=[.h2/.j,h2/.(j+1).] as Subset of
I[01]
            by A16,A307,A311,A320,BORSUK_1:83,RCOMP_1:16;
         A322:Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).])
          proof let x be set;assume
           A323:x in Segment(h0/.i,h0/.(i+1),P);
             h0/.(i+1) <> W-min P
                   by A22,A29,A31,A65,A291,A303,A304,A309,A313,FUNCT_1:def 8;
            then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A323,Def1;
            then consider p being Point of TOP-REAL 2 such that
            A324:p=x & (LE h0/.i,p,P & LE p,h0/.(i+1),P);
            A325:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or
            h0/.i in Upper_Arc(P) & p in Upper_Arc(P) &
             LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) or
            h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) &
             LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P)
                                   by A324,JORDAN6:def 10;
                A326:j<len h2 by A294,A302,NAT_1:38;
              A327: h0/.(i+1) <> E-max P
              by A22,A28,A30,A65,A291,A304,A308,A309,A313,FUNCT_1:def 8;
A328:       h21.(j+1) <> W-min P by A22,A29,A31,A65,A303,A309,FUNCT_1:def 8;
                 now assume h0/.(i+1) in Upper_Arc(P);
                  then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P)
                             by A313,A315,XBOOLE_0:def 3;
                  then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                 hence contradiction by A291,A304,A313,A327,A328,TARSKI:def 2;
                end;
     then A329:p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& not
            h0/.(i+1)=W-min(P)
             & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or
            p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P)
                 & not h0/.(i+1)=W-min(P) by A324,JORDAN6:def 10;
A330:        h0/.i <> W-min(P)
                    by A22,A29,A31,A65,A285,A305,A312,A326,FUNCT_1:def 8;
A331:         h21.j <> E-max P by A22,A28,A30,A65,A299,A305,FUNCT_1:def 8;
A332:         now assume h0/.i in Upper_Arc(P);
                  then h0/.i in Upper_Arc(P)/\ Lower_Arc(P)
                                   by A312,A314,XBOOLE_0:def 3;
                  then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                 hence contradiction by A285,A312,A330,A331,TARSKI:def 2;
              end;
then A333:         LE h0/.i,p,Lower_Arc P, E-max P, W-min P
                      by A324,JORDAN6:def 10;
A334:         h0/.i <> E-max(P) by A22,A28,A30,A65,A285,A299,A305,A312,FUNCT_1:
def 8;
A335:             now assume p in Upper_Arc(P);
                  then p in Upper_Arc P /\ Lower_Arc P by A325,A332,XBOOLE_0:
def 3;
                  then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                  then p=W-min(P) or p=E-max(P) by TARSKI:def 2;
                 hence contradiction by A11,A325,A332,A334,JORDAN6:69;
                end;
then A336:           LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P)
                  by A324,JORDAN6:def 10;
                  consider z being set such that A337:z in dom g2 & p=g2.z
                                   by A13,A329,A335,FUNCT_1:def 5;
                  reconsider rz=z as Real by A15,A337;
                  A338:g2.(h2/.(j+1))=h0/.(i+1)
                      by A291,A304,A309,A313,A321,FUNCT_1:23;
                   A339:0<=h2/.j & h2/.j<=1
                      by A16,A307,A320,BORSUK_1:83,TOPREAL5:1;
                    h2.(j+1) in rng h2 by A309,FUNCT_1:def 5;
                then 0<=rz & rz<=1 & 0<=h2/.(j+1) & h2/.(j+1)<=1
                               by A15,A16,A321,A337,BORSUK_1:83,TOPREAL5:1;
                   then rz<=h2/.(j+1)& h2/.j<=rz
               by A12,A13,A14,A306,A312,A320,A333,A336,A337,A338,A339,Th20;
             then rz in [.h2/.j,h2/.(j+1).] by TOPREAL5:1;
           hence x in g2.:([.h2/.j,h2/.(j+1).]) by A324,A337,FUNCT_1:def 12;
          end;
          g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
          proof let x be set;assume x in g2.:([.h2/.j,h2/.(j+1).]);
            then consider y being set such that
A340: y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x=g2.y by FUNCT_1:def 12;
            A341:x in Lower_Arc(P) by A13,A340,FUNCT_1:def 5;
            then reconsider p1=x as Point of TOP-REAL 2;
            reconsider sy=y as Real by A340;
             A342:h2/.j<=sy & sy<=h2/.(j+1) by A340,TOPREAL5:1;
             A343:0<=sy & sy<=1 by A15,A340,TOPREAL5:1;
A344:         h2.(j+1) <> 1 by A16,A18,A29,A303,A309,FUNCT_1:def 8;
A345:         now assume p1=W-min(P);
             then 1=sy by A12,A14,A32,A340,FUNCT_1:def 8;
             hence contradiction by A319,A321,A342,A344,AXIOMS:21;
            end;
A346:       h0/.(i+1) <> W-min P
            by A22,A29,A31,A65,A291,A303,A304,A309,A313,FUNCT_1:def 8;
A347:          LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P)
                  by A11,A12,A13,A14,A306,A312,A316,A317,A320,A340,A342,A343,
Th19;
              LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P)
                       by A11,A12,A13,A14,A318,A319,A321,A340,A342,A343,Th19;
             then LE h0/.i,p1,P & LE p1,h0/.(i+1),P
                    by A312,A313,A314,A315,A341,A345,A346,A347,JORDAN6:def 10;
            then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P};
           hence x in Segment(h0/.i,h0/.(i+1),P) by A346,Def1;
          end;
         then W=g2.:(Q1) by A201,A322,XBOOLE_0:def 10;
        hence diameter(W)<e by A16,A296,A301;
       case A348:i=len h1;
           then A349:h0.i=E-max(P) by A21,A37,A201,SCMFSA_7:9;
           A350:i-len h11=i-'len h11 by A21,A348,SCMFSA_7:3;
           A351:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                            by A21,A40,A202,A348,FINSEQ_1:36;
           A352:i+1-len h11=i+1-'len h11 by A21,A204,A348,SCMFSA_7:3;
       i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A202,REAL_1:49;
           then A353:1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A348,A352,XCMPLX_1:26;
           then 1<i+1-'len h11+(2-1) by NAT_1:38;
           then 1<i+1-'len h11+2-1 by XCMPLX_1:29;
           then 0<i+1-'len h11+2-1 by AXIOMS:22;
           then A354:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def 3;
            0<=i-'len h11 by NAT_1:18;
then A355:      0+2<=i-'len h11 +2 by AXIOMS:24;
            i-len h11<=len h1+(len h2-2)-len h11 by A47,A201,REAL_1:49;
           then i-len h11<=(len h2-2) by A21,XCMPLX_1:26;
           then i-'len h11+2<=len h2-2+2 by A350,AXIOMS:24;
then A356:      i-'len h11+2<=len h2 by XCMPLX_1:27;
           then A357:i-'len h11+2-1<=len h2-1 by REAL_1:49;
           A358:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                                    by A23,A355,A356,Lm2,JORDAN3:5,7;
            len h2<len h2+1 by NAT_1:38;
           then len h2-1<len h2+1-1 by REAL_1:54;
           then len h2-1<len h2 by XCMPLX_1:26;
           then A359:i-'len h11+2-1<len h2 by A357,AXIOMS:22;
           A360:i-'len h11+2-'1=i-'len h11+2-1 by A358,JORDAN3:1;
           set j=i-'len h11+2-'1;
            len h1-len h11>=0 by A21,XCMPLX_1:14;
           then len h1-'len h11=len h11-len h11 by A21,BINARITH:def 3;
then A361:      0+2-1=len h1-'len h11+2-1 by XCMPLX_1:14;
           A362:0<=i-len h11 by A21,A348,XCMPLX_1:14;
            i-len h11<len h11+(len h2-2)-len h11 by A21,A47,A201,REAL_1:54;
           then i-len h11<len h2-2 by XCMPLX_1:26;
           then i-len h11+2<len h2-2+2 by REAL_1:53;
           then A363:i-len h11+2<len h2 by XCMPLX_1:27;
           A364:j+1=i-'len h11+(1+1)-1+1 by A358,JORDAN3:1
               .=i-'len h11+1+1-1+1 by XCMPLX_1:1
               .=i-'len h11+1+1 by XCMPLX_1:26
               .=i-'len h11+(1+1) by XCMPLX_1:1;
           then A365:j+1<len h2 by A362,A363,BINARITH:def 3;
           A366:j+1=i-len h11+2-1+1 by A360,A362,BINARITH:def 3
               .=1+(i-len h11+(2-1)) by XCMPLX_1:29
               .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8
               .=(i+1)+-len h11+(2-1) by XCMPLX_1:1
               .=i+1-len h11+(2-1) by XCMPLX_0:def 8
               .=i+1-'len h11+2-'1 by A352,A354,XCMPLX_1:29;
           A367:j in dom h2 by A22,A358,FINSEQ_3:27;
           then A368:h21.j=g2.(h2.j) by FUNCT_1:23;
           A369:h0.i=g2.(h2.j) by A14,A16,A348,A349,A361,JORDAN3:1;
A370:        h2.j in rng h2 by A367,FUNCT_1:def 5;
           A371:1<j+1 by A358,NAT_1:38;
           A372:  h0.(i+1)=h21.(j+1) by A43,A44,A351,A352,A353,A366,JORDAN3:27;
           A373:j+1 in dom h2 by A356,A364,A371,FINSEQ_3:27;
           then A374:h0.(i+1)=g2.(h2.(j+1)) by A372,FUNCT_1:23;
A375:        h2.(j+1) in rng h2 by A373,FUNCT_1:def 5;
            i in dom h0 by A201,FINSEQ_3:27;
           then A376:h0/.i=h0.i by FINSEQ_4:def 4;
            i+1 in dom h0 by A202,A203,FINSEQ_3:27;
           then A377:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
           g2.(h2.j) in rng g2 by A15,A16,A370,BORSUK_1:83,FUNCT_1:def 5;
           then A378:h0.i in Lower_Arc P
              by A13,A14,A16,A348,A349,A361,JORDAN3:1;
           A379:h0.(i+1) in Lower_Arc P
                 by A13,A15,A16,A374,A375,BORSUK_1:83,FUNCT_1:def 5;
           A380:1<=j & j<len h2 by A358,A359,JORDAN3:1;
A381:    g2.(h2.(j+1)) = h0/.(i+1) by A372,A373,A377,FUNCT_1:23;
A382:    h2.(j+1) <= 1 by A16,A375,BORSUK_1:83,TOPREAL5:1;
           A383:h2/.j=h2.j by A380,FINSEQ_4:24;
           A384:h2/.(j+1)=h2.(j+1) by A356,A364,A371,FINSEQ_4:24;
         then reconsider Q1=[.h2/.j,h2/.(j+1).]
                     as Subset of I[01]
                          by A16,A370,A375,A383,BORSUK_1:83,RCOMP_1:16;
         A385:Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).])
          proof let x be set;assume
           A386:x in Segment(h0/.i,h0/.(i+1),P);
             h0/.(i+1) <> W-min P
              by A22,A29,A31,A65,A365,A372,A373,A377,FUNCT_1:def 8;
            then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A386,Def1;
            then consider p being Point of TOP-REAL 2 such that
            A387:p=x & LE h0/.i,p,P & LE p,h0/.(i+1),P;
       A388:h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or
            h0/.i in Upper_Arc(P) & p in Upper_Arc(P) &
             LE h0/.i,p,Upper_Arc(P),W-min(P),E-max(P) or
            h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) &
             LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P)
                                   by A387,JORDAN6:def 10;
            j+1<len h2 by A362,A363,A364,BINARITH:def 3;
            then A389:j<len h2 by NAT_1:38;
              A390:not h0/.(i+1)=E-max(P)
                      by A22,A28,A30,A65,A371,A372,A373,A377,FUNCT_1:def 8;
                A391:h0/.(i+1) in Lower_Arc(P)
                   by A13,A15,A16,A374,A375,A377,BORSUK_1:83,FUNCT_1:def 5;
             now assume h0/.(i+1) in Upper_Arc(P);
              then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P)
                       by A391,XBOOLE_0:def 3;
              then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
              then h21.(j+1)=W-min(P) by A372,A377,A390,TARSKI:def 2;
             hence contradiction by A22,A29,A31,A65,A365,A373,FUNCT_1:def 8;
            end;
            then A392:p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)
            & not h0/.(i+1)=W-min(P)
             & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or
            p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P)
                 & not h0/.(i+1)=W-min(P) by A387,JORDAN6:def 10;
                A393:h0/.i<>W-min(P)
                  by A22,A29,A31,A65,A367,A368,A369,A376,A389,FUNCT_1:def 8;
                 dom (g1*h1) c= dom h0 by FINSEQ_1:39;
                then A394: h0/.i=E-max(P) by A36,A348,A349,FINSEQ_4:def 4;
A395:           now assume A396:not p in Lower_Arc(P);
                  then p=E-max(P) by A2,A388,A394,JORDAN6:70;
                 hence contradiction by A1,A396,Th1;
                end;
A397:           now assume p in Upper_Arc(P);
                  then p in Upper_Arc(P)/\ Lower_Arc(P) by A395,XBOOLE_0:def 3
;
then A398:             p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                   p <> W-min P by A2,A388,A393,JORDAN6:69;
                 hence p = E-max P by A398,TARSKI:def 2;
                end;
then A399:           LE p,h0/.(i+1),Lower_Arc P, E-max P, W-min P
                    by A11,A392,JORDAN5C:10;
                 p in rng g2 by A1,A13,A387,A397,Th1,JORDAN6:def 10;
                then consider z being set such that A400:z in dom g2 & p=g2.z
                                 by FUNCT_1:def 5;
                reconsider rz=z as Real by A15,A400;
A401:          g2.(h2/.(j+1))=h0/.(i+1)
                 by A356,A364,A371,A374,A377,FINSEQ_4:24;
                    h2.(j+1) in rng h2 by A373,FUNCT_1:def 5;
              then 0<=rz & rz<=1 & 0<=h2/.(j+1) & h2/.(j+1)<=1
                 by A15,A16,A384,A400,BORSUK_1:83,TOPREAL5:1;
              then rz<=h2/.(j+1)& h2/.j<=rz
                 by A12,A13,A14,A16,A348,A361,A383,A399,A400,A401,Th20,JORDAN3:
1;
             then rz in [.h2/.j,h2/.(j+1).] by TOPREAL5:1;
           hence x in g2.:([.h2/.j,h2/.(j+1).]) by A387,A400,FUNCT_1:def 12;
          end;
          g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
          proof let x be set;assume x in g2.:([.h2/.j,h2/.(j+1).]);
            then consider y being set such that
      A402: y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x=g2.y by FUNCT_1:def 12;
            A403:x in Lower_Arc(P) by A13,A402,FUNCT_1:def 5;
            then reconsider p1=x as Point of TOP-REAL 2;
            reconsider sy=y as Real by A402;
             A404:h2/.j<=sy & sy<=h2/.(j+1) by A402,TOPREAL5:1;
             A405:0<=sy & sy<=1 by A15,A402,TOPREAL5:1;
A406:         h2.(j+1) <> 1 by A16,A18,A29,A365,A373,FUNCT_1:def 8;
A407:        now assume p1=W-min(P);
              then 1=sy by A12,A14,A32,A402,FUNCT_1:def 8;
             hence contradiction by A382,A384,A404,A406,AXIOMS:21;
            end;
A408:        h0/.(i+1) <> W-min(P)
                 by A22,A29,A31,A65,A365,A372,A373,A377,FUNCT_1:def 8;
              LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P)
                by A11,A12,A13,A14,A349,A376,A402,A405,Th19;
            then A409: LE h0/.i,p1,P by A376,A378,A403,A407,JORDAN6:def 10;
             LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P)
                    by A11,A12,A13,A14,A381,A382,A384,A402,A404,A405,Th19;
            then LE p1,h0/.(i+1),P by A377,A379,A403,A408,JORDAN6:def 10;
            then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A409;
           hence x in Segment(h0/.i,h0/.(i+1),P) by A408,Def1;
          end;
         then W=g2.:(Q1) by A201,A385,XBOOLE_0:def 10;
        hence diameter(W)<e by A16,A380;
       end;
       hence diameter(W)<e;
      end;
   thus for W being Subset of Euclid 2 st
       W=Segment(h0/.len h0,h0/.1,P)  holds diameter W < e
      proof let W be Subset of Euclid 2;
       assume
A410:   W=Segment(h0/.len h0,h0/.1,P);
         set i=len h0;
         len h0<=len h11 + len mid(h21,2,len h21 -'1) by FINSEQ_1:35;
        then A411:    h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A21,A48,
FINSEQ_1:36;
           A412:i-len h11=i-'len h11 by A21,A49,SCMFSA_7:3;
            i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                          by FINSEQ_1:35;
           then A413:i-len h11<= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
            len h1 +1-len h1<=i-len h1 by A48,REAL_1:49;
           then 1<=i-len h1 by XCMPLX_1:26;
           then A414:h0.i=h21.(i-'len h11 +2-'1)
                             by A21,A43,A44,A411,A412,A413,JORDAN3:27;
             A415:i-'len h11+2
              =(len h21-2)+2 by A21,A23,A47,A412,XCMPLX_1:26
             .=len h21 by XCMPLX_1:27;
            0<=i-'len h11 by NAT_1:18;
then A416:      0+2<=i-'len h11 +2 by AXIOMS:24;
then A417:      2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
            i-'len h11+2<=len h2-2+2 by A21,A47,A412,XCMPLX_1:26;
then A418:        i-'len h11+2<=len h2 by XCMPLX_1:27;
           then A419:i-'len h11+2-1<=len h2-1 by REAL_1:49;
           A420:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                             by A23,A416,A418,Lm2,JORDAN3:5,7;
            len h2<len h2+1 by NAT_1:38;
           then len h2-1<len h2+1-1 by REAL_1:54;
           then len h2-1<len h2 by XCMPLX_1:26;
           then A421:i-'len h11+2-1<len h2 by A419,AXIOMS:22;
           A422:i-'len h11+2-'1=i-'len h11+2-1 by A417,Lm2,JORDAN3:1;
           set j=i-'len h11+2-'1;
            len h11+1-len h11<=i-len h11 by A21,A48,REAL_1:49;
           then 1<=i-len h11 by XCMPLX_1:26;
           then 1<=i-'len h11 by JORDAN3:1;
           then 1+2<=i-'len h11+2 by AXIOMS:24;
           then 1+2-1<=i-'len h11+2-1 by REAL_1:49;
           then A423:1<j by A422,AXIOMS:22;
           A424:j< len h2 by A417,A421,Lm2,JORDAN3:1;
           A425:j+1=i-'len h11+(1+1)-1+1 by A417,Lm2,JORDAN3:1
               .=i-'len h11+1+1-1+1 by XCMPLX_1:1
               .=i-'len h11+1+1 by XCMPLX_1:26
               .=i-'len h11+(1+1) by XCMPLX_1:1;
           A426:j in dom h2 by A22,A420,FINSEQ_3:27;
           then A427:h0.i=g2.(h2.j) by A414,FUNCT_1:23;
A428:       h2.j in rng h2 by A426,FUNCT_1:def 5;
           then A429:0<=h2.j & h2.j<=1 by A16,BORSUK_1:83,TOPREAL5:1;
           A430:1<j+1 by A417,Lm2,NAT_1:38;
           A431:h0.i in Lower_Arc P
                       by A13,A15,A16,A427,A428,BORSUK_1:83,FUNCT_1:def 5;
A432:      now assume h0.i in Upper_Arc(P);
             then h0.i in Upper_Arc(P)/\ Lower_Arc(P) by A431,XBOOLE_0:def 3;
             then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
             then h0.i=W-min(P) or h0.i=E-max(P) by TARSKI:def 2;
            hence contradiction
            by A22,A28,A29,A30,A31,A65,A414,A423,A424,A426,FUNCT_1:def 8;
           end;
           j+1 in dom h2 by A22,A415,A425,A430,FINSEQ_3:27;
then A433:      h2.(j+1) in rng h2 by FUNCT_1:def 5;
            i in dom h0 by A50,FINSEQ_3:27;
           then A434:h0/.i=h0.i by FINSEQ_4:def 4;
A435:     0 <= h2.j by A16,A428,BORSUK_1:83,TOPREAL5:1;
A436:     h2.j <= 1 by A16,A428,BORSUK_1:83,TOPREAL5:1;
          A437:h2/.j=h2.j by A417,A424,Lm2,FINSEQ_4:24;
          A438:h2/.(j+1)=h2.(j+1) by A418,A425,A430,FINSEQ_4:24;
         then reconsider Q1=[.h2/.j,h2/.(j+1).]
                     as Subset of I[01]
                by A16,A428,A433,A437,BORSUK_1:83,RCOMP_1:16;
         A439:Segment(h0/.i,h0/.1,P) c= g2.:([.h2/.j,h2/.(j+1).])
          proof let x be set;assume
           A440:x in Segment(h0/.i,h0/.1,P);
             h0/.1=W-min(P) by A39,A61,FINSEQ_4:def 4;
            then x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)}
                                      by A440,Def1;
            then consider p being Point of TOP-REAL 2 such that
            A441:p=x & (LE h0/.i,p,P or h0/.i in P & p=W-min(P));
              A442:j<j+1 by NAT_1:38;
              A443:j in dom h2 by A417,A424,Lm2,FINSEQ_3:27;
               j+1 in dom h2 by A418,A425,A430,FINSEQ_3:27;
              then h2.j<h2.(j+1) by A16,A442,A443,GOBOARD1:def 1;
              then A444:h2/.(j+1) in [.h2/.j,
              h2/.(j+1).] by A437,A438,RCOMP_1:15;
              A445: h2/.(j+1)=1 by A16,A23,A29,A415,A425,FINSEQ_4:def 4;
             now per cases by A441;
            case LE h0/.i,p,P & (p<>W-min(P) or not h0/.i in P);
then A446:h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) &
               LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P)
                          by A432,A434,JORDAN6:def 10;
                  then consider z being set such that A447:z in dom g2 & p=g2.z
                                   by A13,FUNCT_1:def 5;
                  reconsider rz=z as Real by A15,A447;
              take rz;
A448:               0<=rz & rz<=1 by A15,A447,TOPREAL5:1;
then A449:         h2/.j<=rz
                 by A12,A13,A14,A427,A429,A434,A437,A446,A447,Th20;
             thus rz in dom g2 by A447;
               rz<=h2/.(j+1) by A16,A22,A415,A425,A438,A448,FINSEQ_3:31;
             hence rz in [.h2/.j,h2/.(j+1).] & x = g2.rz
                         by A441,A447,A449,TOPREAL5:1;
            case h0/.i in P & p=W-min(P);
             hence ex y being set st y in dom g2 & y in [.h2/.j,h2/.(j+1).]
              & x = g2.y by A14,A32,A441,A444,A445;
            end;
           hence x in g2.:([.h2/.j,h2/.(j+1).]) by FUNCT_1:def 12;
          end;
          g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.1,P)
          proof let x be set;assume x in g2.:([.h2/.j,h2/.(j+1).]);
            then consider y being set such that
      A450: y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x=g2.y by FUNCT_1:def 12;
            A451:x in Lower_Arc(P) by A13,A450,FUNCT_1:def 5;
            then reconsider p1=x as Point of TOP-REAL 2;
            reconsider sy=y as Real by A450;
             A452:h2/.j<=sy & sy<=h2/.(j+1) by A450,TOPREAL5:1;
             A453:0<=sy & sy<=1 by A15,A450,TOPREAL5:1;
            A454:h0/.1=W-min(P) by A39,A61,FINSEQ_4:def 4;
A455:      Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:def 9;
A456:        LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P)
               by A11,A12,A13,A14,A427,A434,A435,A436,A437,A450,A452,A453,Th19;
             now per cases;
            case p1=W-min(P);
             hence LE h0/.i,p1,P or  h0/.i in P & p1=W-min(P)
              by A431,A434,A455,XBOOLE_0:def 2;
            case p1<>W-min(P);
             hence LE h0/.i,p1,P or  h0/.i in P & p1=W-min(P)
                              by A431,A434,A451,A456,JORDAN6:def 10;
            end;
            then x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)};
           hence x in Segment(h0/.i,h0/.1,P) by A454,Def1;
          end;
         then W=g2.:Q1 by A410,A439,XBOOLE_0:def 10;
        hence diameter(W)<e by A16,A417,A424,Lm2;
      end;
      A457: for i being Nat st 1<=i & i+1<len h0 holds
         LE h0/.(i+1),h0/.(i+2),P
            proof let i be Nat;assume
            A458: 1<=i & i+1<len h0;
              then A459:i+1+1<=len h0 by NAT_1:38;
              A460:1<i+1 by A458,NAT_1:38;
              then A461:1<i+1+1 by NAT_1:38;
A462:         i+1<i+1+1 by NAT_1:38;
               now per cases;
              case A463:i+1<len h1;
                then A464:i+1+1<=len h1 by NAT_1:38;
                A465:h0.(i+1)=h11.(i+1) by A21,A460,A463,SCMFSA_7:9;
                A466:i+1 in dom h1 by A460,A463,FINSEQ_3:27;
                then A467:h0.(i+1)=g1.(h1.(i+1)) by A465,FUNCT_1:23;
A468:            h1.(i+1) in rng h1 by A466,FUNCT_1:def 5;
                then A469:0<=h1.(i+1) & h1.(i+1)<=1
                    by A9,BORSUK_1:83,TOPREAL5:1;
                A470:1<i+1+1 by A460,NAT_1:38;
                then A471:h0.(i+1+1)=h11.(i+1+1) by A21,A464,SCMFSA_7:9;
                A472:i+1+1 in dom h1 by A464,A470,FINSEQ_3:27;
                then A473:h0.(i+1+1)=g1.(h1.(i+1+1)) by A471,FUNCT_1:23;
A474:            h1.((i+1)+1) in rng h1 by A472,FUNCT_1:def 5;
then A475:           0<=h1.(i+1+1) by A9,BORSUK_1:83,TOPREAL5:1;
A476:           h1.(i+1+1)<=1 by A9,A474,BORSUK_1:83,TOPREAL5:1;
                A477:h1.(i+1)<h1.(i+1+1) by A9,A462,A466,A472,GOBOARD1:def 1;
                 i+1 in dom h0 by A458,A460,FINSEQ_3:27;
                then A478:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                 (i+1)+1 in dom h0 by A459,A470,FINSEQ_3:27;
                then A479:h0/.(i+1+1)=h0.(i+1+1) by FINSEQ_4:def 4;
                A480:g1.(h1.(i+1)) in rng g1
                     by A6,A9,A468,BORSUK_1:83,FUNCT_1:def 5;
                A481: i+1+1=i+(1+1) by XCMPLX_1:1;
A482:           h0/.(i+1) in Upper_Arc P
                       by A4,A465,A466,A478,A480,FUNCT_1:23;
A483:           h0/.(i+1+1) in Upper_Arc P
                      by A4,A6,A9,A473,A474,A479,BORSUK_1:83,FUNCT_1:def 5;
                 LE h0/.(i+1),h0/.((i+1)+1),Upper_Arc(P),W-min(P),E-max(P)
                by A2,A3,A4,A5,A467,A469,A473,A475,A476,A477,A478,A479,Th19;
               hence thesis by A481,A482,A483,JORDAN6:def 10;
              case
A484:          i+1>=len h1;
                 now per cases by A484,REAL_1:def 5;
                case A485:i+1>len h1;
                  then A486:len h1 +1<=i+1 by NAT_1:38;
A487:             len h11+1<=i+1 by A21,A485,NAT_1:38;
A488:             i+1<=len h11 + len (mid(h21,2,len h21 -'1))
                                by A458,FINSEQ_1:35;
                  then A489:h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11)
                                               by A487,FINSEQ_1:36;
                  A490:(i+1)-len h11=(i+1)-'len h11 by A21,A485,SCMFSA_7:3;
                   (i+1)-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len
h11
                                         by A488,REAL_1:49;
                  then A491:(i+1)-len h11<= len (mid(h21,2,len h21 -'1))
                                             by XCMPLX_1:26;
                   len h1 +1-len h1<=(i+1)-len h1 by A486,REAL_1:49;
then             1<=(i+1)-'len h11 by A21,A490,XCMPLX_1:26;
                  then A492:h0.(i+1)=h21.((i+1)-'len h11 +2-'1)
                             by A43,A44,A489,A490,A491,JORDAN3:27;
                  A493:len h1 +1<=(i+1)+1 by A486,NAT_1:38;
                  then A494:h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len
h11)
                                      by A21,A40,A459,FINSEQ_1:36;
                   (i+1)+1>len h11 by A21,A485,NAT_1:38;
                  then A495:(i+1)+1-len h11=(i+1)+1-'len h11 by SCMFSA_7:3;
A496:             (i+1)+1-len h11
                      <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A459,REAL_1:49;
                   len h1 +1-len h1<=(i+1)+1-len h1 by A493,REAL_1:49;
                  then A497:1<=(i+1)+1-'len h11
                      & (i+1)+1-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A495,A496,XCMPLX_1:26;
                  then A498:h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1)
                    by A43,A44,A494,A495,JORDAN3:27;
                   1<(i+1)+1-'len h11+(2-1) by A497,NAT_1:38;
                  then 1<(i+1)+1-'len h11+2-1 by XCMPLX_1:29;
then A499:             0<(i+1)+1-'len h11+2-1 by AXIOMS:22;
                   0<=(i+1)-'len h11 by NAT_1:18;
then A500:             0+2<=(i+1)-'len h11 +2 by AXIOMS:24;
then A501:             2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5;
                   (i+1)-len h11<=len h1+(len h2-2)-len h11
                             by A47,A458,REAL_1:49;
                  then (i+1)-len h11<=(len h2-2) by A21,XCMPLX_1:26;
                  then (i+1)-'len h11+2<=len h2-2+2 by A490,AXIOMS:24;
then A502:              (i+1)-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A503:1<=((i+1)-'len h11 +2-'1)
                            & ((i+1)-'len h11 +2-'1)<=len h21
                                    by A23,A500,Lm2,JORDAN3:5,7;
                  A504:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1
                                      by A501,Lm2,JORDAN3:1;
                  set j=(i+1)-'len h11+2-'1;
                   (i+1)-len h11<len h11+(len h2-2)-len h11
                                     by A21,A47,A458,REAL_1:54;
                  then (i+1)-len h11<len h2-2 by XCMPLX_1:26;
                  then (i+1)-len h11+2<len h2-2+2 by REAL_1:53;
                  then A505:(i+1)-len h11+2<len h2 by XCMPLX_1:27;
                A506:j+1=(i+1)-'len h11+(1+1)-1+1 by A501,Lm2,JORDAN3:1
                  .=(i+1)-'len h11+1+1-1+1 by XCMPLX_1:1
                  .=(i+1)-'len h11+1+1 by XCMPLX_1:26
                  .=(i+1)-'len h11+(1+1) by XCMPLX_1:1
                  .=(i+1)-'len h11+2;
                  A507:j+1=1+((i+1)-len h11+(2-1)) by A490,A504,XCMPLX_1:29
                  .=1+((i+1)+-len h11+(2-1)) by XCMPLX_0:def 8
                  .=((i+1)+1)+-len h11+(2-1) by XCMPLX_1:1
                  .=(i+1)+1-len h11+(2-1) by XCMPLX_0:def 8
                  .=(i+1)+1-len h11+2-1 by XCMPLX_1:29
                  .=(i+1)+1-'len h11+2-'1 by A495,A499,BINARITH:def 3;
A508:             j in dom h2 by A22,A503,FINSEQ_3:27;
                  then A509:h0.(i+1)=g2.(h2.j) by A492,FUNCT_1:23;
A510:              h2.j in rng h2 by A508,FUNCT_1:def 5;
                  then A511:0<=h2.j & h2.j<=1 by A16,BORSUK_1:83,TOPREAL5:1;
                  A512:j<j+1 by NAT_1:38;
                  1<j+1 by A501,Lm2,NAT_1:38;
                  then A513:j+1 in dom h2 by A502,A506,FINSEQ_3:27;
                  then A514:h0.((i+1)+1)=g2.(h2.(j+1))
                     & h21.(j+1)=g2.(h2.(j+1))  by A498,A507,FUNCT_1:23;
A515:              h2.(j+1) in rng h2 by A513,FUNCT_1:def 5;
                  A516:h2.j<h2.(j+1) by A16,A508,A512,A513,GOBOARD1:def 1;
                   i+1 in dom h0 by A458,A460,FINSEQ_3:27;
                  then A517:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                   (i+1)+1 in dom h0 by A459,A461,FINSEQ_3:27;
                  then A518:h0/.((i+1)+1)=h0.((i+1)+1) by FINSEQ_4:def 4;
                  A519:h0.(i+1) in Lower_Arc(P)
                     by A13,A15,A16,A509,A510,BORSUK_1:83,FUNCT_1:def 5;
                  A520:h0.((i+1)+1) in Lower_Arc(P)
                   by A13,A15,A16,A514,A515,BORSUK_1:83,FUNCT_1:def 5;
A521: 0 <= (h2.(j+1)) by A16,A515,BORSUK_1:83,TOPREAL5:1;
A522: (h2.(j+1)) <= 1 by A16,A515,BORSUK_1:83,TOPREAL5:1;
A523:            h0/.(i+1+1) <> W-min P
           by A22,A29,A31,A65,A490,A498,A505,A506,A507,A513,A518,FUNCT_1:def 8;
                A524:i+1+1=i+(1+1) by XCMPLX_1:1;
                 LE h0/.(i+1),h0/.((i+1)+1),Lower_Arc(P),E-max(P),W-min(P)
                             by A11,A12,A13,A14,A509,A511,A514,A516,A517,A518,
A521,A522,Th19;
                 hence thesis by A517,A518,A519,A520,A523,A524,JORDAN6:def 10;
                case A525:i+1=len h1;
                  then A526:h0.len h1 =E-max(P) by A21,A37,A460,SCMFSA_7:9;
                  A527:len h1-len h11=len h1-'len h11 by A21,SCMFSA_7:3;
A528:             len h1+1 <=len h11 + len (mid(h21,2,len h21 -'1))
                                          by A459,A525,FINSEQ_1:35;
                  A529:h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11)
                                      by A21,A40,A459,A525,FINSEQ_1:36;
                  A530:(i+1)+1-len h11=(i+1)+1-'len h11
                                by A21,A462,A525,SCMFSA_7:3;
             (i+1)+1-len h11
                       <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A525,A528,REAL_1:49;
                  then A531:1<=(i+1)+1-'len h11
                         & (i+1)+1-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A525,A530,XCMPLX_1:26;
                  then A532:h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1)
                    by A43,A44,A529,A530,JORDAN3:27;
                   1<(i+1)+1-'len h11+(2-1) by A531,NAT_1:38;
                  then 1<(i+1)+1-'len h11+2-1 by XCMPLX_1:29;
                  then 0<(i+1)+1-'len h11+2-1 by AXIOMS:22;
                  then A533:(i+1)+1-'len h11+2-1=(i+1)+1-'len h11+2-'1
                            by BINARITH:def 3;
                   0<=(i+1)-'len h11 by NAT_1:18;
                  then 0+2<=(i+1)-'len h11 +2 by AXIOMS:24;
                  then A534:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5;
                   (i+1)-len h11<=len h1+(len h2-2)-len h11
                               by A47,A458,REAL_1:49;
                  then (i+1)-'len h11<=len h2-2 by A21,A525,A527,XCMPLX_1:26;
                  then (i+1)-'len h11+2<=len h2-2+2 by AXIOMS:24;
then A535:              (i+1)-'len h11+2<=len h2 by XCMPLX_1:27;
                  A536:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1
                                  by A534,Lm2,JORDAN3:1;
                  set j=(i+1)-'len h11+2-'1;
                  A537:0<=(i+1)-len h11 by A21,A525,XCMPLX_1:14;
                   (i+1)-len h11<len h11+(len h2-2)-len h11
                  by A21,A47,A458,REAL_1:54;
                  then (i+1)-len h11<len h2-2 by XCMPLX_1:26;
                  then (i+1)-len h11+2<len h2-2+2 by REAL_1:53;
                  then A538:(i+1)-len h11+2<len h2 by XCMPLX_1:27;
                  A539:j+1=(i+1)-'len h11+(1+1)-1+1 by A534,Lm2,JORDAN3:1
                  .=(i+1)-'len h11+1+1-1+1 by XCMPLX_1:1
                  .=(i+1)-'len h11+1+1 by XCMPLX_1:26
                  .=(i+1)-'len h11+(1+1) by XCMPLX_1:1;
                  then A540:j+1<len h2 by A537,A538,BINARITH:def 3;
                  A541:j+1=(i+1)-len h11+2-1+1 by A536,A537,BINARITH:def 3
                  .=1+((i+1)-len h11+(2-1)) by XCMPLX_1:29
                  .=1+((i+1)+-len h11+(2-1)) by XCMPLX_0:def 8
                  .=((i+1)+1)+-len h11+(2-1) by XCMPLX_1:1
                  .=(i+1)+1-len h11+(2-1) by XCMPLX_0:def 8
                  .=(i+1)+1-'len h11+2-'1 by A530,A533,XCMPLX_1:29;
                  1<j+1 by A534,Lm2,NAT_1:38;
                  then A542:j+1 in dom h2 by A535,A539,FINSEQ_3:27;
                  then A543:h0.((i+1)+1)=g2.(h2.(j+1))
                         & h21.(j+1)=g2.(h2.(j+1)) by A532,A541,FUNCT_1:23;
A544:             h2.(j+1) in rng h2 by A542,FUNCT_1:def 5;
                   len h1 in dom h0 by A458,A460,A525,FINSEQ_3:27;
                  then A545:h0/.len h1=h0.len h1 by FINSEQ_4:def 4;
                   (i+1)+1 in dom h0 by A459,A461,FINSEQ_3:27;
                  then A546:h0/.((i+1)+1)=h0.((i+1)+1) by FINSEQ_4:def 4;
                  A547:h0.(i+1+1) in Lower_Arc P
                        by A13,A15,A16,A543,A544,BORSUK_1:83,FUNCT_1:def 5;
                  A548: h0.(i+1) in Upper_Arc(P) by A1,A525,A526,Th1;
A549:             h0/.(i+1+1) <> W-min P
                    by A22,A29,A31,A65,A532,A540,A541,A542,A546,FUNCT_1:def 8;
                   i+1+1=i+(1+1) by XCMPLX_1:1 .=i+2;
                 hence thesis by A525,A545,A546,A547,A548,A549,JORDAN6:def 10;
                end;
               hence thesis;
              end;
             hence thesis;
            end;
      A550: for i being Nat st 1<=i & i+1<=len h0 holds
         LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1)
       proof let i be Nat such that
A551:    1<=i and
A552:    i+1<=len h0;
A553:    1<i+1 by A551,NAT_1:38;
A554:    i<len h0 by A552,NAT_1:38;
A555:    i<i+1 by NAT_1:38;
          i in dom h0 by A551,A554,FINSEQ_3:27;
then A556:    h0/.i=h0.i by FINSEQ_4:def 4;
                 i+1 in dom h0 by A552,A553,FINSEQ_3:27;
then A557:    h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
              now per cases;
              case A558:i<len h1;
                then A559:i+1<=len h1 by NAT_1:38;
                A560:h0.i=h11.i by A21,A551,A558,SCMFSA_7:9;
                A561:i in dom h1 by A551,A558,FINSEQ_3:27;
then A562:            h1.i in rng h1 by FUNCT_1:def 5;
                A563:h0.(i+1)=h11.(i+1) by A21,A553,A559,SCMFSA_7:9;
                A564:i+1 in dom h1 by A553,A559,FINSEQ_3:27;
                then A565:h0.(i+1)=g1.(h1.(i+1)) by A563,FUNCT_1:23;
A566:            h1.(i+1) in rng h1 by A564,FUNCT_1:def 5;
                A567:h1.i<h1.(i+1) by A9,A555,A561,A564,GOBOARD1:def 1;
                g1.(h1.i) in rng g1
                        by A6,A9,A562,BORSUK_1:83,FUNCT_1:def 5;
                then A568:h0.i in Upper_Arc(P) by A4,A560,A561,FUNCT_1:23;
           A569:h0.(i+1) in Upper_Arc(P)
                  by A4,A6,A9,A565,A566,BORSUK_1:83,FUNCT_1:def 5;
A570: g1.(h1.i) = h0/.i by A556,A560,A561,FUNCT_1:23;
A571: 0 <= (h1.i) by A9,A562,BORSUK_1:83,TOPREAL5:1;
A572: (h1.i) <= 1 by A9,A562,BORSUK_1:83,TOPREAL5:1;
A573: 0 <= (h1.(i+1)) by A9,A566,BORSUK_1:83,TOPREAL5:1;
A574: (h1.(i+1)) <= 1 by A9,A566,BORSUK_1:83,TOPREAL5:1;
     A575: i+1 <> 1 by A551,NAT_1:38;
    A576: i+1 <> i by NAT_1:38;
                 LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
                    by A2,A3,A4,A5,A557,A565,A567,A570,A571,A572,A573,A574,Th19
;
               hence thesis by A20,A25,A38,A64,A556,A557,A560,A561,A563,A564,
A568,A569,A575,A576,FUNCT_1:def 8,JORDAN6:def 10;
              case
A577:          i>=len h1;
                 now per cases by A577,REAL_1:def 5;
                case A578:i>len h1;
                  then A579:len h1 +1<=i by NAT_1:38;
                  A580:len h11+1<=i & i<=len h11 + len (mid(h21,2,len h21 -'1))
                                      by A21,A554,A578,FINSEQ_1:35,NAT_1:38;
                                          then A581:             h0.i=(mid(h21,
2,len h21 -'1)).(i -len h11) by FINSEQ_1:36;
                  A582:i-len h11=i-'len h11 by A21,A578,SCMFSA_7:3;
A583:             i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A580,REAL_1:49;
                   len h1 +1-len h1<=i-len h1 by A579,REAL_1:49;
                  then 1<=i-'len h11 & i-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A582,A583,XCMPLX_1:26;
                  then A584:h0.i=h21.(i-'len h11 +2-'1)
                             by A43,A44,A581,A582,JORDAN3:27;
                  A585:len h1 +1<=i+1 by A579,NAT_1:38;
                  then A586:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                                      by A21,A40,A552,FINSEQ_1:36;
                   i+1>len h11 by A21,A578,NAT_1:38;
                  then A587:i+1-len h11=i+1-'len h11 by SCMFSA_7:3;
A588:             i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A552,REAL_1:49;
                   len h1 +1-len h1<=i+1-len h1 by A585,REAL_1:49;
then A589:             1<=i+1-'len h11 & i+1-'len h11<=len mid(h21,2,len h21 -'
1)
                             by A21,A587,A588,XCMPLX_1:26;
                  then A590:h0.(i+1)=h21.(i+1-'len h11 +2-'1)
                    by A43,A44,A586,A587,JORDAN3:27;
                   1<i+1-'len h11+(2-1) by A589,NAT_1:38;
                  then 1<i+1-'len h11+2-1 by XCMPLX_1:29;
                  then 0<i+1-'len h11+2-1 by AXIOMS:22;
                  then A591:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def
3;
                   0<=i-'len h11 by NAT_1:18;
then A592:             0+2<=i-'len h11 +2 by AXIOMS:24;
then A593:             2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
                   i-len h11<=len h1+(len h2-2)-len h11
                                      by A47,A554,REAL_1:49;
                  then i-len h11<=(len h2-2) by A21,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by A582,AXIOMS:24;
then A594:               i-'len h11+2<=len h2 by XCMPLX_1:27;
A595:             1<=i-'len h11 +2-'1 by A592,Lm2,JORDAN3:5;
A596:             i-'len h11 +2-'1<=len h21 by A23,A594,JORDAN3:7;
                  set j=i-'len h11+2-'1;
                   i-len h11<len h11+(len h2-2)-len h11
                                  by A21,A47,A554,REAL_1:54;
                  then i-len h11<len h2-2 by XCMPLX_1:26;
then A597:             i-len h11+2<len h2-2+2 by REAL_1:53;
                   j+1=i-'len h11+(1+1)-1+1 by A593,Lm2,JORDAN3:1
                  .=i-'len h11+1+1-1+1 by XCMPLX_1:1
                  .=i-'len h11+1+1 by XCMPLX_1:26
                  .=i-'len h11+(1+1) by XCMPLX_1:1;
                  then A598:j+1<len h2 by A582,A597,XCMPLX_1:27;
                  A599:j+1=i-len h11+2-1+1 by A582,A593,Lm2,JORDAN3:1
                  .=1+(i-len h11+(2-1)) by XCMPLX_1:29
                  .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8
                  .=(i+1)+-len h11+(2-1) by XCMPLX_1:1
                  .=i+1-len h11+(2-1) by XCMPLX_0:def 8
                  .=i+1-'len h11+2-'1 by A587,A591,XCMPLX_1:29;
                  A600:j in dom h2 by A22,A595,A596,FINSEQ_3:27;
                  then A601:h0.i=g2.(h2.j) by A584,FUNCT_1:23;
A602:              h2.j in rng h2 by A600,FUNCT_1:def 5;
                  A603:j<j+1 by NAT_1:38;
                  1<j+1 by A595,NAT_1:38;
                  then A604:j+1 in dom h2 by A598,FINSEQ_3:27;
                  then A605:h0.(i+1)=g2.(h2.(j+1))
                     & h21.(j+1)=g2.(h2.(j+1))  by A590,A599,FUNCT_1:23;
A606:              h2.(j+1) in rng h2 by A604,FUNCT_1:def 5;
A607:          h2.j<h2.(j+1) by A16,A600,A603,A604,GOBOARD1:def 1;
                   i in dom h0 by A551,A554,FINSEQ_3:27;
                  then A608:h0/.i=h0.i by FINSEQ_4:def 4;
                   i+1 in dom h0 by A552,A553,FINSEQ_3:27;
                  then A609:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
A610: 0 <= (h2.j) by A16,A602,BORSUK_1:83,TOPREAL5:1;
A611: (h2.j) <= 1 by A16,A602,BORSUK_1:83,TOPREAL5:1;
A612: 0 <= (h2.(j+1)) by A16,A606,BORSUK_1:83,TOPREAL5:1;
A613: (h2.(j+1)) <= 1 by A16,A606,BORSUK_1:83,TOPREAL5:1;
A614:           h0/.(i+1) <> W-min P
                by A22,A29,A31,A65,A590,A598,A599,A604,A609,FUNCT_1:def 8;
                A615: j < j+1 by NAT_1:38;
                 h0/.i in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)
                   & LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P)
                                             by A11,A12,A13,A14,A15,A16,A601,
A602,A605,A606,A607,A608,A609,A610,A611,A612,A613,Th19,BORSUK_1:83,FUNCT_1:def
5;
                 hence thesis by A22,A65,A584,A590,A599,A600,A604,A608,A609,
A614,A615,FUNCT_1:def 8,JORDAN6:def 10;
                case A616:i=len h1;
                  then A617:h0.i=E-max(P) by A21,A37,A551,SCMFSA_7:9;
                  A618:i-len h11=i-'len h11 by A21,A616,SCMFSA_7:3;
A619:             i+1 <=len h11 + len (mid(h21,2,len h21 -'1))
                                          by A552,FINSEQ_1:35;
                  A620:h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                                      by A21,A40,A552,A616,FINSEQ_1:36;
                  A621:i+1-len h11=i+1-'len h11 by A21,A555,A616,SCMFSA_7:3;
A622:             i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A619,REAL_1:49;
A623:              1<=i+1-'len h11 by A21,A616,A621,XCMPLX_1:26;
                   i+1-'len h11<= len mid(h21,2,len h21 -'1)
                     by A621,A622,XCMPLX_1:26;
                  then A624:h0.(i+1)=h21.(i+1-'len h11 +2-'1)
                    by A43,A44,A620,A621,A623,JORDAN3:27;
                   1<i+1-'len h11+(2-1) by A623,NAT_1:38;
                  then 1<i+1-'len h11+2-1 by XCMPLX_1:29;
                  then 0<i+1-'len h11+2-1 by AXIOMS:22;
                  then A625:i+1-'len h11+2-1=i+1-'len h11+2-'1 by BINARITH:def
3;
                   0<=i-'len h11 by NAT_1:18;
                  then A626: 0+2<=i-'len h11 +2 by AXIOMS:24;
                  then A627:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
                   i-len h11<=len h1+(len h2-2)-len h11 by A47,A554,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A618,XCMPLX_1:26;
then A628:              i-'len h11+2<=len h2-2+2 by AXIOMS:24;
then              i-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A629:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                                    by A23,A626,Lm2,JORDAN3:5,7;
                  A630:i-'len h11+2-'1=i-'len h11+2-1 by A627,Lm2,JORDAN3:1;
                  set j=i-'len h11+2-'1;
                   len h1-len h11>=0 by A21,XCMPLX_1:14;
                  then len h1-'len h11=len h11-len h11 by A21,BINARITH:def 3;
                               then A631:             0+2-1=len h1-'len h11+2-1
by XCMPLX_1:14;
                  A632:0<=i-len h11 by A21,A616,XCMPLX_1:14;
                   i-len h11<len h11+(len h2-2)-len h11
                                  by A21,A47,A554,REAL_1:54;
                  then i-len h11<len h2-2 by XCMPLX_1:26;
                  then i-len h11+2<len h2-2+2 by REAL_1:53;
                  then A633:i-len h11+2<len h2 by XCMPLX_1:27;
                  A634:j+1=i-'len h11+(1+1)-1+1 by A627,Lm2,JORDAN3:1
                  .=i-'len h11+1+1-1+1 by XCMPLX_1:1
                  .=i-'len h11+1+1 by XCMPLX_1:26
                  .=i-'len h11+(1+1) by XCMPLX_1:1
                  .=i-'len h11+2;
                  then A635:j+1<=len h2 by A628,XCMPLX_1:27;
                  A636:j+1<len h2 by A632,A633,A634,BINARITH:def 3;
                  A637:j+1=i-len h11+2-1+1 by A630,A632,BINARITH:def 3
                  .=1+(i-len h11+(2-1)) by XCMPLX_1:29
                  .=1+(i+-len h11+(2-1)) by XCMPLX_0:def 8
                  .=(i+1)+-len h11+(2-1) by XCMPLX_1:1
                  .=i+1-len h11+(2-1) by XCMPLX_0:def 8
                  .=i+1-'len h11+2-'1 by A621,A625,XCMPLX_1:29;
                  A638:j in dom h2 by A22,A629,FINSEQ_3:27;
                  then A639:h21.j=g2.(h2.j) by FUNCT_1:23;
                  A640:h0.i=g2.(h2.j) by A14,A16,A616,A617,A631,JORDAN3:1;
                  1<j+1 by A627,Lm2,NAT_1:38;
                  then A641:j+1 in dom h2 by A635,FINSEQ_3:27;
                  then A642:h0.(i+1)=g2.(h2.(j+1)) by A624,A637,FUNCT_1:23;
A643:             h2.(j+1) in rng h2 by A641,FUNCT_1:def 5;
                   i in dom h0 by A551,A554,FINSEQ_3:27;
                  then A644:h0/.i=h0.i by FINSEQ_4:def 4;
                   i+1 in dom h0 by A552,A553,FINSEQ_3:27;
                  then A645:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                  A646:h0.(i+1) in Lower_Arc(P)
                         by A13,A15,A16,A642,A643,BORSUK_1:83,FUNCT_1:def 5;
                  A647: h0.i in Upper_Arc(P) by A1,A617,Th1;
A648:            h0/.(i+1) <> W-min P
                 by A22,A29,A31,A65,A624,A636,A637,A641,A645,FUNCT_1:def 8;
                  j+1 <> j by NAT_1:38;
                 hence thesis
                 by A22,A65,A624,A637,A638,A639,A640,A641,A644,A645,A646,A647,
A648,FUNCT_1:def 8,JORDAN6:def 10;
                end;
               hence thesis;
              end;
             hence thesis;
       end;
   thus for i being Nat st 1<=i & i+1<len h0 holds
         Segment(h0/.i,h0/.(i+1),P)/\ Segment(h0/.(i+1),h0/.(i+2),P)
         ={h0/.(i+1)}
      proof let i be Nat;assume
        A649: 1<=i & i+1<len h0;
then A650:LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1)
             by A550;
        A651: LE h0/.(i+1),h0/.(i+2),P by A457,A649;
        then h0/.i<>h0/.(i+2) by A1,A650,JORDAN6:72;
        hence Segment(h0/.i,h0/.(i+1),P)/\ Segment(h0/.(i+1),h0/.(i+2),P)
         ={h0/.(i+1)} by A1,A650,A651,Th10;
      end;
   thus Segment(h0/.len h0,h0/.1,P)/\ Segment(h0/.1,h0/.2,P)={h0/.1}
    proof A652: h11.2 <> W-min(P) by A20,A25,A38,A57,A64,FUNCT_1:def 8;
                A653:h0.2=g1.(h1.2) by A57,A60,FUNCT_1:23;
A654:           h1.2 in rng h1 by A57,FUNCT_1:def 5;
                A655:h0/.2=h0.2 by A59,FINSEQ_4:def 4;
then A656:     h0/.2 in Upper_Arc P
               by A4,A6,A9,A653,A654,BORSUK_1:83,FUNCT_1:def 5;
                  len h1 +1-len h1<=len h0 -len h1 by A48,REAL_1:49;
                 then A657: 1<=len h0 -len h1 by XCMPLX_1:26;
                  A658:h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11)
                                   by A21,A40,A48,FINSEQ_1:36;
                len h0 -len h11 <=len h11 + len mid(h21,2,len h21 -'1) -len h11
                                         by FINSEQ_1:35;
               then len h0-len h11<= len (mid(h21,2,len h21 -'1))
                 by XCMPLX_1:26;
                  then A659:h0.len h0=h21.(len h0-'len h11 +2-'1)
                    by A21,A43,A44,A54,A657,A658,JORDAN3:27;
                   0<=len h0-'len h11 by NAT_1:18;
then A660:             0+2<=len h0-'len h11 +2 by AXIOMS:24;
                   len h0-'len h11+2<=len h2-2+2
                              by A21,A47,A54,XCMPLX_1:26;
                  then len h0-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A661:1<=(len h0-'len h11 +2-'1)
                     & (len h0-'len h11 +2-'1)<=len h21
                                    by A23,A660,Lm2,JORDAN3:5,7;
                  set j=len h0-'len h11+2-'1;
                  A662:j in dom h2 by A22,A661,FINSEQ_3:27;
                  then A663:h0.len h0=g2.(h2.j) by A659,FUNCT_1:23;
            A664: now assume A665:h0/.2=h0/.len h0;
                   h2.j in rng h2 by A662,FUNCT_1:def 5;
                then g2.(h2.j) in rng g2 by A15,A16,BORSUK_1:83,FUNCT_1:def 5;
                then h0/.2 in Upper_Arc(P)/\  Lower_Arc(P)
                     by A13,A52,A656,A663,A665,XBOOLE_0:def 3;
                then h0/.2 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
                then h11.2=E-max(P) by A60,A652,A655,TARSKI:def 2;
             hence contradiction by A20,A35,A37,A56,A57,A64,FUNCT_1:def 8;
            end;
      defpred P[Nat] means
      $1+2<=len h0 implies LE h0/.2,h0/.($1+2),P;
         Upper_Arc(P) \/ Lower_Arc(P)= P by A1,JORDAN6:65;
        then h0/.2 in P by A656,XBOOLE_0:def 2;
        then A666: P[0] by A1,JORDAN6:71;
        A667:for k being Nat st P[k] holds P[k+1]
         proof let k be Nat;assume
          A668: k+2<=len h0 implies LE h0/.2,h0/.(k+2),P;
            now assume A669:k+1+2<=len h0;
             A670:k+1+2=k+2+1 by XCMPLX_1:1;
             then A671:k+2<len h0 by A669,NAT_1:38;
             A672:1<=1+k by NAT_1:29;
              k+1+1=k+(1+1) by XCMPLX_1:1 .=k+2;
             then LE h0/.(k+2),h0/.(k+2+1),P by A457,A670,A671,A672;
            hence LE h0/.2,h0/.(k+1+2),P
             by A1,A668,A669,A670,JORDAN6:73,NAT_1:38;
           end;
          hence (k+1+2<=len h0 implies LE h0/.2,h0/.(k+1+2),P);
         end;
        A673:for i being Nat holds P[i]
            from Ind(A666,A667);
             len h0 -'2=len h0-2 by A58,SCMFSA_7:3;
            then len h0-'2+2=len h0 by XCMPLX_1:27;
           then LE h0/.2,h0/.len h0,P & h0/.2<>h0/.len h0
                         & h0/.2<>W-min(P) by A59,A60,A652,A664,A673,FINSEQ_4:
def 4;
       hence thesis by A1,A63,Th12;
      end;
      set i = len h0-'1;
A674:    i+1 = len h0 by A50,AMI_5:4;
A675:    1<=i by A58,Lm4;
      A676: len h0 > 1+1+1 by A122,AXIOMS:22;
      then A677:   len h0-'1 > 1+1 by Lm3;
A678:  i<len h0 by A50,JORDAN5B:1;
then A679:   i in dom h0 by A675,FINSEQ_3:27;
then A680:h0/.i=h0.i by FINSEQ_4:def 4;
        A681:i+1<=len h0 by A678,NAT_1:38;
        A682:1+1<=len h0 by A50,NAT_1:38;
        A683:LE h0/.i,h0/.(i+1),P by A550,A675,A681;
        A684:LE h0/.1,h0/.(1+1),P by A550,A682;
           1+1 in dom h0 by A682,FINSEQ_3:27;
then A685:h0/.(1+1)=h0.(1+1) by FINSEQ_4:def 4;
        A686:h0/.1<>h0/.(1+1) by A550,A682;
        A687:h0.(1+1)=h11.(1+1) by A21,A56,SCMFSA_7:9;
        A688: 1+1 in dom h1 by A56,FINSEQ_3:27;
        then A689:h0.(1+1)=g1.(h1.(1+1)) by A687,FUNCT_1:23;
A690:    h1.(1+1) in rng h1 by A688,FUNCT_1:def 5;
        A691:1<i by A677,AXIOMS:22;
A692:  now per cases;
               case A693:i<=len h1;
                then A694:h0.i=h11.i by A21,A691,SCMFSA_7:9;
        A695:i in dom h1 by A691,A693,FINSEQ_3:27;
        then A696:h1.(1+1)<h1.i by A9,A677,A688,GOBOARD1:def 1;
A697:    h1.i in rng h1 by A695,FUNCT_1:def 5;
                A698:h0.i=g1.(h1.i) by A694,A695,FUNCT_1:23;
        A699:0<=h1.i & h1.i<=1 by A9,A697,BORSUK_1:83,TOPREAL5:1;
            0 <= h1.(1+1) & h1.(1+1) <= 1 by A9,A690,BORSUK_1:83,TOPREAL5:1;
                then h0/.(1+1) in Upper_Arc(P) & h0/.i in Upper_Arc(P) &
                LE h0/.(1+1),h0/.i,Upper_Arc(P),W-min(P),E-max(P)
                  by A2,A3,A4,A5,A6,A9,A680,A685,A689,A690,A696,A697,A698,A699,
Th19,BORSUK_1:83,FUNCT_1:def 5;
               hence LE h0/.(1+1),h0/.i,P by JORDAN6:def 10;
               case A700:i>len h1;
                  then A701:i-len h11=i-'len h11 by A21,SCMFSA_7:3;
                   i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                        by A40,A678,REAL_1:49;
then A702:0<=i-'len h11
                      & i-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A700,A701,SQUARE_1:12,XCMPLX_1:26;
                   i-len h11
                       <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                by A40,A678,REAL_1:49;
                  then A703:i-len h11
                      <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
                   0+1<=i-'len h11+1 by A702,AXIOMS:24;
                  then 0+1<=i-'len h11+1+1-1 by XCMPLX_1:26;
                  then 0+1<=i-'len h11+(1+1)-1 by XCMPLX_1:1;
                  then A704:i-'len h11+2-'1=i-'len h11+2-1 by JORDAN3:1;
                   0<=i-'len h11 by NAT_1:18;
                  then 0+2<=i-'len h11 +2 by AXIOMS:24;
                  then A705:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
                   i-len h11<=len h1+(len h2-2)-len h11 by A47,A678,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A701,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then i-'len h11+2<=len h2 by XCMPLX_1:27;
then i-'len h11 +2-'1<=len h21 by A23,JORDAN3:7;
then A706:           (i-'len h11 +2-'1) in dom h21 by A705,Lm2,FINSEQ_3:27;
              1+1 in dom h1 by A56,FINSEQ_3:27;
                  then A707: h11.(1+1)=g1.(h1.(1+1)) by FUNCT_1:23;
                  A708:len h1 +1<=i by A700,NAT_1:38;
                  then A709:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11)
                                      by A21,A40,A678,FINSEQ_1:36;
                   len h1 +1-len h1<=i-len h1 by A708,REAL_1:49;
                  then A710: 1<=i-len h11 by A21,XCMPLX_1:26;
                  then A711:h0.(i)=h21.(i-'len h11 +2-'1)
                    by A43,A44,A701,A703,A709,JORDAN3:27;
                   i+1-1<=len h1+(len h2-2)-1 by A47,A681,REAL_1:49;
                  then i<=len h1+(len h2-2)-1 by XCMPLX_1:26;
                  then i-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49;
                  then i-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29
;
                  then i-'len h11<=len h2-2-1 by A21,A701,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2-1+2 by AXIOMS:24;
                  then i-'len h11+2<=len h2-1 by XCMPLX_1:229;
                  then A712:i-'len h11+2-1<=len h2-1-1 by REAL_1:49;
                  set k=i-'len h11+2-'1;
                  A713: h2.k in rng h2 by A22,A706,FUNCT_1:def 5;
                  A714: h1.(1+1) in rng h1 by A57,FUNCT_1:def 5;
                  A715:h0.i=h21.k by A43,A44,A701,A703,A709,A710,JORDAN3:27;
                  A716:h0.i=g2.(h2.k)
                         & h21.k=g2.(h2.k) by A22,A706,A711,FUNCT_1:23;
A717:g1.(h1.(1+1)) in rng g1 by A6,A9,A714,BORSUK_1:83,FUNCT_1:def 5;
                  A718:h0.i in Lower_Arc(P)
                  by A13,A15,A16,A713,A716,BORSUK_1:83,FUNCT_1:def 5;
                   h0/.i <> W-min P
              by A17,A22,A29,A31,A65,A680,A704,A706,A712,A715,FUNCT_1:def 8;
                 hence LE h0/.(1+1),h0/.i,P
                 by A4,A680,A685,A687,A707,A717,A718,JORDAN6:def 10;
               end;
   thus Segment(h0/.(len h0-' 1),h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P)
               ={h0/.len h0}
      proof
A719:LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1)
             by A550,A674,A675;
       i <> 1 by A676,Lm3;
      then h0/.i <> h0/.1 by A61,A66,A679,PARTFUN2:17;

       hence
          Segment(h0/.i,h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P)={h0/.len h0
}
          by A1,A63,A674,A719,Th11;
      end;
          now
           now assume A720:h0/.(1+1)=h0/.i;
             now
                A721:1+1 in dom h1 by A56,FINSEQ_3:27;
                then A722: h1.(1+1) in rng h1 by FUNCT_1:def 5;
                A723:h0.(1+1)=h11.(1+1) by A21,A56,SCMFSA_7:9;
                then h0.(1+1)=g1.(h1.(1+1)) by A721,FUNCT_1:23;
          then A724:h0.(1+1) in Upper_Arc(P) by A4,A6,A9,A722,BORSUK_1:83,
FUNCT_1:def 5;
              now
             per cases;
             case A725:i<=len h1;
                then A726:h0.i=h11.i by A21,A675,SCMFSA_7:9;
                 i in dom h1 by A675,A725,FINSEQ_3:27;
              hence contradiction
               by A20,A64,A677,A680,A685,A720,A721,A723,A726,FUNCT_1:def 8;
             case A727:i>len h1;
                  then A728:len h1 +1<=i by NAT_1:38;
then A729:     h0.i=(mid(h21,2,len h21 -'1)).(i -len h11)
                  by A21,A40,A678,FINSEQ_1:36;
                  A730:i-len h11=i-'len h11 by A21,A727,SCMFSA_7:3;
                   i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A678,REAL_1:49;
                  then A731:i-len h11<= len (mid(h21,2,len h21 -'1))
                                             by XCMPLX_1:26;
                   len h1 +1-len h1<=i-len h1 by A728,REAL_1:49;
                  then 1<=i-len h1 by XCMPLX_1:26;
                  then A732:h0.i=h21.(i-'len h11 +2-'1)
                             by A21,A43,A44,A729,A730,A731,JORDAN3:27;
                   0<=i-'len h11 by NAT_1:18;
                  then A733: 0+2<=i-'len h11 +2 by AXIOMS:24;
                  then A734:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
                   i-len h11<=len h1+(len h2-2)-len h11
                    by A47,A678,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A730,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then i-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A735:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                                    by A23,A733,Lm2,JORDAN3:5,7;
                  A736:i-'len h11+2-'1=i-'len h11+2-1
                          by A734,Lm2,JORDAN3:1;
                  set k=i-'len h11+2-'1;
                   i-len h11<=len h1+(len h2-2)-len h11 by A47,A678,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A730,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then A737:i-'len h11+2<=len h2 by XCMPLX_1:27;
                   i-'len h11+2-'1<i-'len h11+2-1+1 by A736,NAT_1:38;
                  then A738: i-'len h11+2-'1<i-'len h11+2 by XCMPLX_1:27;
                   len h11+1-len h11<=i-len h11 by A21,A728,REAL_1:49;
                  then 1<=i-len h11 by XCMPLX_1:26;
                  then 1<=i-'len h11 by JORDAN3:1;
                  then 1+2<=i-'len h11+2 by AXIOMS:24;
                  then 1+2-1<=i-'len h11+2-1 by REAL_1:49;
                  then A739:1<k by A736,AXIOMS:22;
                  A740:k in dom h2 by A22,A735,FINSEQ_3:27;
                  then A741:h0.i=g2.(h2.k) by A732,FUNCT_1:23;
                  A742: h2.k in rng h2 by A740,FUNCT_1:def 5;
                   i in dom h0 by A675,A678,FINSEQ_3:27;
                  then A743:h0/.i=h0.i by FINSEQ_4:def 4;
                g2.(h2.k) in rng g2 by A15,A16,A742,BORSUK_1:83,FUNCT_1:def 5;
               then h0.i in Upper_Arc(P) /\ Lower_Arc(P)
                         by A13,A685,A720,A724,A741,A743,XBOOLE_0:def 3;
               then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
               then h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2;
              hence contradiction by A22,A28,A29,A30,A31,A65,A732,A737,A738,
A739,A740,FUNCT_1:def 8;
             end;
             hence contradiction;
            end;
           hence contradiction;
          end;
         hence Segment(h0/.1,h0/.(1+1),P) misses Segment(h0/.i,h0/.len h0,P)
           by A1,A674,A683,A684,A686,A692,Th13;
        end;
     hence Segment(h0/.i,h0/.len h0,P) misses Segment(h0/.1,h0/.2,P);
     thus for i,j being Nat
           st 1<=i & i < j & j < len h0 & not i,j are_adjacent1
         holds Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P)
     proof
      let i,j be Nat;assume that
A744:    1<=i and
A745:    i < j and
A746:    j < len h0 and
A747:    not i,j are_adjacent1;
A748:  i<len h0 by A745,A746,AXIOMS:22;
A749:  1<j by A744,A745,AXIOMS:22;
        i in dom h0 by A744,A748,FINSEQ_3:27;
then A750:h0/.i=h0.i by FINSEQ_4:def 4;
        A751:i+1<=len h0 by A748,NAT_1:38;
        A752:j+1<=len h0 by A746,NAT_1:38;
        A753:LE h0/.i,h0/.(i+1),P by A550,A744,A751;
        A754:LE h0/.j,h0/.(j+1),P by A550,A749,A752;
        A755:not(j=i+1 or i=j+1) by A747,GOBRD10:def 1;
           1<j+1 by A749,NAT_1:38;
          then j+1 in dom h0 by A752,FINSEQ_3:27;
then A756:h0/.(j+1)=h0.(j+1) by FINSEQ_4:def 4;
          now per cases;
         case i<j;
then A757:       i+1<=j by NAT_1:38;
           then A758:i+1<j by A755,REAL_1:def 5;
           A759:i+1<len h0 by A746,A757,AXIOMS:22;
          A760:h0/.i<>h0/.(i+1) by A550,A744,A751;
          A761:1<i+1 by A744,NAT_1:38;
          A762:1<=(i+1) & (i+1)<len h0 by A744,A746,A757,AXIOMS:22,NAT_1:38;
          A763:LE h0/.(i+1),h0/.j,P
            proof
               now per cases;
              case A764:i+1<=len h1;
                now per cases;
               case A765:j<=len h1;
                A766:h0.(i+1)=h11.(i+1) by A21,A762,A764,SCMFSA_7:9;
                A767:(i+1) in dom h1 by A762,A764,FINSEQ_3:27;
then A768:            h1.(i+1) in rng h1 by FUNCT_1:def 5;
                A769:1<j by A758,A762,AXIOMS:22;
                then A770:h0.j=h11.j by A21,A765,SCMFSA_7:9;
                A771:j in dom h1 by A765,A769,FINSEQ_3:27;
then A772:            h1.j in rng h1 by FUNCT_1:def 5;
                 i+1 in dom h0 by A762,FINSEQ_3:27;
                then A773:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                 j in dom h0 by A746,A769,FINSEQ_3:27;
                then h0/.j=h0.j by FINSEQ_4:def 4;
                then Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) &
                g1.(h1.(i+1)) = h0/.(i+1) & 0 <= (h1.(i+1)) & (h1.(i+1)) <= 1
                & g1.(h1.j) = h0/.j
                & 0 <= (h1.j) & (h1.j) <= 1
                                  & (h1.(i+1)) <= (h1.j)
                      by A1,A9,A758,A766,A767,A768,A770,A771,A772,A773,BORSUK_1
:83,FUNCT_1:23,GOBOARD1:def 1,JORDAN6:def 8,TOPREAL5:1;
                then h0/.(i+1) in Upper_Arc(P) & h0/.j in Upper_Arc(P) &
                LE h0/.(i+1),h0/.j,Upper_Arc(P),W-min(P),E-max(P)
                                       by A3,A4,A5,A6,A9,A768,A772,Th19,
BORSUK_1:83,FUNCT_1:def 5;
               hence thesis by JORDAN6:def 10;
               case A774:j>len h1;
                   then A775:len h11<=j
                   & j<=len h11 + len (mid(h21,2,len h21 -'1))
                                        by A20,A746,FINSEQ_1:35,FINSEQ_3:31;
                  A776:j-len h11=j-'len h11 by A21,A774,SCMFSA_7:3;
                   j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                        by A775,REAL_1:49;
then A777:0<=j-'len h11
                      & j-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A774,A776,SQUARE_1:12,XCMPLX_1:26;
                  A778: j-len h11
                       <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                           by A40,A746,REAL_1:49;
                  then A779:j-len h11
                      <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
                   0+1<=j-'len h11+1 by A777,AXIOMS:24;
                  then 0+1<=j-'len h11+1+1-1 by XCMPLX_1:26;
                  then 0+1<=j-'len h11+(1+1)-1 by XCMPLX_1:1;
                  then A780:j-'len h11+2-'1=j-'len h11+2-1 by JORDAN3:1;
                   0<=j-'len h11 by NAT_1:18;
                  then 0+2<=j-'len h11 +2 by AXIOMS:24;
                  then A781:2-'1<=j-'len h11 +2-'1 by JORDAN3:5;
                   j-len h11<=len h1+(len h2-2)-len h11
                            by A47,A746,REAL_1:49;
                  then j-len h11<=(len h2-2) by A21,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2+2 by A776,AXIOMS:24;
                  then j-'len h11+2<=len h2 by XCMPLX_1:27;
then A782: (j-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7;
                  then A783:(j-'len h11 +2-'1) in dom h21 by A781,Lm2,FINSEQ_3:
27;
                  i+1 in Seg len h1 by A762,A764,FINSEQ_1:3;
then             i+1 in dom h1 by FINSEQ_1:def 3;
                  then A784: j-len h11=j-'len h11
                  & h0.(i+1)=h11.(i+1) & (j-'len h11 +2-'1) in dom h21
                  & j-'len h11+2-'1=j-'len h11+2-1
                  & j-len h11 <= len (mid(h21,2,len h21 -'1))
                  & (i+1) in dom h1 & h11.(i+1)=g1.(h1.(i+1))
              by A21,A761,A764,A774,A778,A781,A782,Lm2,FINSEQ_3:27,FUNCT_1:23,
JORDAN3:1,SCMFSA_7:3,9,XCMPLX_1:26;
                  A785:len h1 +1<=j by A774,NAT_1:38;
                  then A786:h0.j=(mid(h21,2,len h21 -'1)).(j -len h11)
                                      by A21,A40,A746,FINSEQ_1:36;
                   len h1 +1-len h1<=j-len h1 by A785,REAL_1:49;
                  then A787: 1<=j-len h1 by XCMPLX_1:26;
                  then A788:h0.j=h21.(j-'len h11 +2-'1)
                    by A21,A43,A44,A776,A779,A786,JORDAN3:27;
                   j+1-1<=len h1+(len h2-2)-1 by A47,A752,REAL_1:49;
                  then j<=len h1+(len h2-2)-1 by XCMPLX_1:26;
                  then j-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49;
                  then j-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29
;
                  then j-len h11<=(len h2-2-1) by A21,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2-1+2 by A776,AXIOMS:24;
                  then j-'len h11+2<=len h2-1 by XCMPLX_1:229;
                  then A789:j-'len h11+2-1<=len h2-1-1 by REAL_1:49;
                  A790: len h2-1-1<len h2 by Lm5;
                  set k=j-'len h11+2-'1;
                  A791: h2.k in rng h2 by A22,A783,FUNCT_1:def 5;
                   i+1 in dom h1 by A761,A764,FINSEQ_3:27;
                  then A792: h1.(i+1) in rng h1 by FUNCT_1:def 5;
                  A793:  h0.j=h21.k by A21,A43,A44,A784,A786,A787,JORDAN3:27;
                  A794:h0.j=g2.(h2.k) & h21.k=g2.(h2.k) by A22,A783,A788,
FUNCT_1:23;
                   (i+1) in dom h0 by A762,FINSEQ_3:27;
                  then A795:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                   j in dom h0 by A746,A749,FINSEQ_3:27;
                  then A796:h0/.j=h0.j by FINSEQ_4:def 4;
                  A797:g1.(h1.(i+1)) in rng g1 by A6,A9,A792,BORSUK_1:83,
FUNCT_1:def 5;
                  A798:h0.j in Lower_Arc(P)
                           by A13,A15,A16,A791,A794,BORSUK_1:83,FUNCT_1:def 5;
                   h0/.j <> W-min P
                 by A22,A29,A31,A65,A780,A783,A789,A790,A793,A796,FUNCT_1:def 8
;
                 hence thesis by A4,A784,A795,A796,A797,A798,JORDAN6:def 10;
               end;
               hence thesis;
              case A799:i+1>len h1;
then A800:                len h1<j by A757,AXIOMS:22;
                  then A801:j-len h11=j-'len h11 by A21,SCMFSA_7:3;
                   j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                        by A40,A746,REAL_1:49;
then A802:0<=j-'len h11
                      & j-'len h11<=len mid(h21,2,len h21 -'1)
                               by A21,A800,A801,SQUARE_1:12,XCMPLX_1:26;
                  A803: j-len h11
                       <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A746,REAL_1:49;
                  then A804:j-len h11
                      <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
                   0+1<=j-'len h11+1 by A802,AXIOMS:24;
                  then 0+1<=j-'len h11+1+1-1 by XCMPLX_1:26;
                  then 0+1<=j-'len h11+(1+1)-1 by XCMPLX_1:1;
                  then A805:j-'len h11+2-'1=j-'len h11+2-1 by JORDAN3:1;
                   0<=j-'len h11 by NAT_1:18;
                  then 0+2<=j-'len h11 +2 by AXIOMS:24;
                  then A806:2-'1<=j-'len h11 +2-'1 by JORDAN3:5;
                   j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49;
                  then j-len h11<=len h2-2 by A21,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2+2 by A801,AXIOMS:24;
                  then j-'len h11+2<=len h2 by XCMPLX_1:27;
then A807: (j-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7;
                  then A808:j-'len h11 +2-'1 in dom h21 by A806,Lm2,FINSEQ_3:27
;
                  A809:len h11+1<=i+1
                      & i+1<len h11 + len (mid(h21,2,len h21 -'1))
                                   by A21,A759,A799,FINSEQ_1:35,NAT_1:38;
                  A810: i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) -
len h11
                             by A40,A759,REAL_1:54;
                  then A811:i+1-len h11<len (mid(h21,2,len h21 -'1))
                                           by XCMPLX_1:26;
                   len h1+1<=i+1 by A799,NAT_1:38;
                  then len h1+1-len h1<=i+1-len h1 by REAL_1:49;
                  then 1<=i+1-len h1 by XCMPLX_1:26;
                  then A812:1<=i+1-'len h11 & i+1-'len h11=i+1-len h11
                                     by A21,JORDAN3:1;
A813:               h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11)
                                      by A809,FINSEQ_1:36
                              .=h21.(i+1-'len h11+2-'1)
                    by A43,A44,A811,A812,JORDAN3:27;
                  then A814: j-len h11=j-'len h11 & (i+1)-len h11=(i+1)-'len
h11
                  & h0.(i+1)=h21.(i+1-'len h11+2-'1)
                  & (j-'len h11 +2-'1) in dom h21
                  & len h11+1<=i+1
                  & i+1<=len h11 + len (mid(h21,2,len h21 -'1))
                  & j-'len h11+2-'1=j-'len h11+2-1
                  & j-len h11 <= len (mid(h21,2,len h21 -'1))
                  & i+1-len h11<len (mid(h21,2,len h21 -'1))
                  by A21,A759,A799,A800,A803,A806,A807,A810,Lm2,FINSEQ_1:35,
FINSEQ_3:27,JORDAN3:1,NAT_1:38,SCMFSA_7:3,XCMPLX_1:26;
                   len h1<j by A757,A799,AXIOMS:22;
                  then A815:len h11+1<=j
                   & j<=len h11 + len (mid(h21,2,len h21 -'1))
                               by A21,A746,FINSEQ_1:35,NAT_1:38;
                  then A816:h0.j=(mid(h21,2,len h21 -'1)).(j -len h11)
                                      by FINSEQ_1:36;
                   len h1 +1-len h1<=j-len h1 by A21,A815,REAL_1:49
;
                  then A817: 1<=j-len h1 by XCMPLX_1:26;
                  then A818:h0.j=h21.(j-'len h11 +2-'1)
                    by A21,A43,A44,A801,A804,A816,JORDAN3:27;
                   0<=(i+1)-'len h11 by NAT_1:18;
                  then A819: 0+2<=(i+1)-'len h11 +2 by AXIOMS:24;
                  then A820:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5;
                   (i+1)-len h11<=len h11+(len h2-2)-len h11
                                    by A21,A47,A759,REAL_1:49;
                  then (i+1)-len h11<=(len h2-2) by XCMPLX_1:26;
                  then (i+1)-'len h11+2<=len h2-2+2 by A814,AXIOMS:24;
                  then (i+1)-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A821:1<=((i+1)-'len h11 +2-'1)
                      & ((i+1)-'len h11 +2-'1)<=len h21
                                    by A23,A819,Lm2,JORDAN3:5,7;
                  A822:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1
                                  by A820,Lm2,JORDAN3:1;
                   j+1-1<=len h1+(len h2-2)-1 by A47,A752,REAL_1:49
;
                  then j<=len h1+(len h2-2)-1 by XCMPLX_1:26;
                  then j-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49;
                  then j-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29
;
                  then j-len h11<=(len h2-2-1) by A21,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2-1+2 by A801,AXIOMS:24;
                  then j-'len h11+2<=len h2-1 by XCMPLX_1:229;
                  then A823:j-'len h11+2-1<=len h2-1-1 by REAL_1:49;
                  A824: len h2-1-1<len h2 by Lm5;
                  set k=j-'len h11+2-'1;
                  set j0=(i+1)-'len h11+2-'1;
                   (i+1)-len h11<j-len h11 by A758,REAL_1:54;
                  then (i+1)-'len h11+2<j-'len h11+2 by A814,REAL_1:53;
                  then A825:j0<k by A805,A822,REAL_1:54;
                  A826:h21.k=g2.(h2.k) by A22,A808,FUNCT_1:23;
A827:              h2.k in rng h2 by A22,A808,FUNCT_1:def 5;
                  then A828:0<=h2.k & h2.k<=1 by A16,BORSUK_1:83,TOPREAL5:1;
                  A829:j0 in dom h2 by A22,A821,FINSEQ_3:27;
                  then A830:h0.(i+1)=g2.(h2.j0) by A813,FUNCT_1:23;
A831:              h2.j0 in rng h2 by A829,FUNCT_1:def 5;
                  then A832:0<=h2.j0 & h2.j0<=1 by A16,BORSUK_1:83,TOPREAL5:1;
                  A833:h2.(j0)<h2.(k) by A16,A22,A808,A825,A829,GOBOARD1:def 1;
                  A834:  h0.j=h21.(k) by A21,A43,A44,A814,A816,A817,JORDAN3:27;
                  A835:h0.j=g2.(h2.k) & h21.k=g2.(h2.k) by A22,A808,A818,
FUNCT_1:23;
                   (i+1) in dom h0 by A762,FINSEQ_3:27;
                  then A836:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                   j in dom h0 by A746,A749,FINSEQ_3:27;
                  then A837:h0/.j=h0.(j) by FINSEQ_4:def 4;
                  A838:g2.(h2.j0) in rng g2 by A15,A16,A831,BORSUK_1:83,FUNCT_1
:def 5;
                  A839:h0.(j) in Lower_Arc(P)
                   by A13,A15,A16,A827,A835,BORSUK_1:83,FUNCT_1:def 5;
A840:            h0/.j <> W-min P
                  by A22,A29,A31,A65,A805,A808,A823,A824,A834,A837,FUNCT_1:def
8;
                 LE h0/.(i+1),h0/.j,Lower_Arc(P),E-max(P),W-min(P)
                     by A11,A12,A13,A14,A818,A826,A828,A830,A832,A833,A836,A837
,Th19;
                 hence thesis by A13,A830,A836,A837,A838,A839,A840,JORDAN6:def
10;
              end;
             hence thesis;
            end;
           now assume A841:h0/.(i+1)=h0/.j;
             now per cases;
            case A842:i+1<=len h1;
                A843:1<i+1 by A744,NAT_1:38;
                then A844:i+1 in dom h1 by A842,FINSEQ_3:27;
                 i+1 in dom h0 by A751,A843,FINSEQ_3:27;
                then A845:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                A846:h0.(i+1)=h11.(i+1) by A21,A842,A843,SCMFSA_7:9;
                then A847:h0.(i+1)=g1.(h1.(i+1)) by A844,FUNCT_1:23;
                 h1.(i+1) in rng h1 by A844,FUNCT_1:def 5;
                then A848:h0.(i+1) in Upper_Arc(P)
                             by A4,A6,A9,A847,BORSUK_1:83,FUNCT_1:def 5;
              now per cases;
             case A849:j<=len h1;
                then A850:h0.(j)=h11.(j) by A21,A749,SCMFSA_7:9;
                A851:j in dom h1 by A749,A849,FINSEQ_3:27;
                 j in dom h0 by A746,A749,FINSEQ_3:27;
                then h0/.j=h0.j by FINSEQ_4:def 4;
              hence contradiction by A20,A64,A755,A841,A844,A845,A846,A850,A851
,FUNCT_1:def 8;
             case A852:j>len h1;
                  then A853:len h1 +1<=j by NAT_1:38;
                  A854:len h11+1<=j & j<=
len h11 + len (mid(h21,2,len h21 -'1)) by A21,A746,A852,FINSEQ_1:35,NAT_1:38;
A855: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11)
              by A21,A40,A746,A853,FINSEQ_1:36;
                  A856:j-len h11=j-'len h11 by A21,A852,SCMFSA_7:3;
                   j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A854,REAL_1:49;
                  then A857:j-len h11<= len (mid(h21,2,len h21 -'1))
                                             by XCMPLX_1:26;
                   len h1 +1-len h1<=j-len h1 by A853,REAL_1:49;
                  then 1<=j-len h11 by A21,XCMPLX_1:26;
                  then A858:h0.j=h21.(j-'len h11 +2-'1)
                             by A43,A44,A855,A856,A857,JORDAN3:27;
                   0<=j-'len h11 by NAT_1:18;
                  then A859: 0+2<=j-'len h11 +2 by AXIOMS:24;
                  then A860:2-'1<=(j-'len h11 +2-'1) by JORDAN3:5;
                   j-len h11<=len h1+(len h2-2)-len h11
                           by A47,A746,REAL_1:49;
                  then j-'len h11<=len h2-2 by A21,A856,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then j-'len h11+2<=len h2 by XCMPLX_1:27;
then A861:1<=(j-'len h11 +2-'1) & (j-'len h11 +2-'1)<=
len h21
                                    by A23,A859,Lm2,JORDAN3:5,7;
                  A862:j-'len h11+2-'1=j-'len h11+2-1
                     by A860,Lm2,JORDAN3:1;
                  set k=j-'len h11+2-'1;
                   j-len h11<=len h1+(len h2-2)-len h11
                                   by A47,A746,REAL_1:49;
                  then j-'len h11<=len h2-2 by A21,A856,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then A863:j-'len h11+2<=len h2 by XCMPLX_1:27;
                   j-'len h11+2-'1<j-'len h11+2-'1+1 by NAT_1:38;
                  then A864: j-'len h11+2-'1<j-'len h11+2 by A862,XCMPLX_1:27;
                   len h11+1-len h11<=j-len h11 by A21,A853,REAL_1:49
;
                  then 1<=j-len h11 by XCMPLX_1:26;
                  then 1<=j-'len h11 by JORDAN3:1;
                  then 1+2<=j-'len h11+2 by AXIOMS:24;
                  then 1+2-1<=j-'len h11+2-1 by REAL_1:49;
                  then A865:1<k by A862,AXIOMS:22;
                  A866:k in dom h2 by A22,A861,FINSEQ_3:27;
                  then A867:h0.j=g2.(h2.k) by A858,FUNCT_1:23;
                  A868: h2.k in rng h2 by A866,FUNCT_1:def 5;
                   j in dom h0 by A746,A749,FINSEQ_3:27;
                  then A869:h0/.j=h0.j by FINSEQ_4:def 4;
                   g2.(h2.k) in rng g2 by A15,A16,A868,BORSUK_1:83,FUNCT_1:def
5;
                  then h0.j in Upper_Arc(P) /\ Lower_Arc(P)
                            by A13,A841,A845,A848,A867,A869,XBOOLE_0:def 3;
                  then A870:         h0.j in {W-min(P),E-max(P)} by A1,JORDAN6:
def 9;
A871:         h0.j <> W-min P
                   by A22,A29,A31,A65,A858,A863,A864,A866,FUNCT_1:def 8;
                h0.j <> E-max P
                   by A22,A28,A30,A65,A858,A865,A866,FUNCT_1:def 8;
              hence contradiction by A870,A871,TARSKI:def 2;
             end;
             hence contradiction;
            case A872:i+1>len h1;
                  then A873:len h1 +1<=i+1 by NAT_1:38;
                  then A874:h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11)
                                     by A21,A40,A751,FINSEQ_1:36;
                  A875:(i+1)-len h11=(i+1)-'len h11 by A21,A872,SCMFSA_7:3;
                   (i+1)-len h11
                   <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A751,REAL_1:49;
                  then A876:(i+1)-len h11<= len (mid(h21,2,len h21 -'1))
                                             by XCMPLX_1:26;
                   len h1 +1-len h1<=(i+1)-len h1 by A873,REAL_1:49
;
                  then 1<=(i+1)-len h11 by A21,XCMPLX_1:26;
                  then A877:h0.(i+1)=h21.((i+1)-'len h11 +2-'1)
                             by A43,A44,A874,A875,A876,JORDAN3:27;
                   0<=(i+1)-'len h11 by NAT_1:18;
                  then A878: 0+2<=(i+1)-'len h11 +2 by AXIOMS:24;
                  then A879:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5;
                   (i+1)-len h11<=len h1+(len h2-2)-len h11
                            by A47,A751,REAL_1:49;
                  then (i+1)-len h11<=(len h2-2) by A21,XCMPLX_1:26;
                  then (i+1)-'len h11+2<=len h2-2+2 by A875,AXIOMS:24;
                  then (i+1)-'len h11+2<=len h2 by XCMPLX_1:27;
then A880:1<=((i+1)-'len h11 +2-'1)
                  & ((i+1)-'len h11 +2-'1)<=len h21
                                    by A23,A878,Lm2,JORDAN3:5,7;
                  A881:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1
                                 by A879,Lm2,JORDAN3:1;
                  set j0=(i+1)-'len h11+2-'1;
                   len h11+1-len h11<=(i+1)-len h11
                           by A21,A873,REAL_1:49;
                  then 1<=(i+1)-len h11 by XCMPLX_1:26;
                  then A882:(i+1)-'len h11=(i+1)-len h11 by JORDAN3:1;
                  A883:j0 in dom h2 by A22,A880,FINSEQ_3:27;
                   1<=i+1 by A744,NAT_1:38;
                  then i+1 in dom h0 by A751,FINSEQ_3:27;
                  then A884:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                  A885:j>len h1 by A757,A872,AXIOMS:22;
                  then A886:len h1 +1<=j by NAT_1:38;
                   len h11+1<=j & j<=
len h11 + len (mid(h21,2,len h21 -'1)) by A21,A746,A885,FINSEQ_1:35,NAT_1:38;
then A887: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11)
                     by FINSEQ_1:36;
                  A888:j-len h11=j-'len h11 by A21,A885,SCMFSA_7:3;
                  A889: j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len
h11
                                    by A40,A746,REAL_1:49;
                   len h1 +1-len h1<=j-len h1 by A886,REAL_1:49;
                  then 1<=j-'len h11 & j-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A888,A889,XCMPLX_1:26;
                  then A890:h0.j=h21.(j-'len h11 +2-'1)
                             by A43,A44,A887,A888,JORDAN3:27;
                   0<=j-'len h11 by NAT_1:18;
                  then A891: 0+2<=j-'len h11 +2 by AXIOMS:24;
                  then A892:2-'1<=(j-'len h11 +2-'1) by JORDAN3:5;
                   j-len h11<=len h1+(len h2-2)-len h11 by A47,A746,REAL_1:49;
                  then j-len h11<=len h2-2 by A21,XCMPLX_1:26;
                  then j-'len h11+2<=len h2-2+2 by A888,AXIOMS:24;
                  then j-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A893:1<=(j-'len h11 +2-'1) & (j-'len h11 +2-'1)<=len h21
                                    by A23,A891,Lm2,JORDAN3:5,7;
                  A894:j-'len h11+2-'1=j-'len h11+2-1
                      by A892,Lm2,JORDAN3:1;
                  set k=j-'len h11+2-'1;
                   len h11+1-len h11<=j-len h11 by A21,A886,REAL_1:49
;
                  then 1<=j-len h11 by XCMPLX_1:26;
                  then j-'len h11=j-len h11 by JORDAN3:1;
                  then i+1-'len h11<j-'len h11 by A758,A882,REAL_1:54;
                  then i+1-'len h11+2<j-'len h11+2 by REAL_1:53;
                  then A895:(i+1)-'len h11+2-'1<j-'len h11+2-'1
                            by A881,A894,REAL_1:54;
                  A896:k in dom h2 by A22,A893,FINSEQ_3:27;
                   j in dom h0 by A746,A749,FINSEQ_3:27;
                  then h0/.j=h0.j by FINSEQ_4:def 4;
                 hence contradiction
      by A22,A65,A841,A877,A883,A884,A890,A895,A896,FUNCT_1:def 8;
            end;
           hence contradiction;
          end;
         hence
           Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P)
                   by A1,A753,A754,A760,A763,Th13;
        case A897: j<=i;
          A898:h0/.j<>h0/.(j+1) by A550,A749,A752;
          A899:1<j+1 by A749,NAT_1:38;
          A900:LE h0/.(j+1),h0/.i,P
            proof
               now per cases;
              case A901:j+1<=len h1;
              then A902:h0.(j+1)=h11.(j+1) by A21,A899,SCMFSA_7:9;
                now per cases;
               case i<=len h1;
               thus thesis by A745,A897;
               case A903:i>len h1;
                  then A904:i-len h11=i-'len h11 by A21,SCMFSA_7:3;
                   i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                        by A40,A748,REAL_1:49;
then A905:0<=i-'len h11
                      & i-'len h11<=len mid(h21,2,len h21 -'1)
                             by A21,A903,A904,SQUARE_1:12,XCMPLX_1:26;
                   i-len h11
                       <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                by A40,A748,REAL_1:49;
                  then A906:i-len h11
                      <= len (mid(h21,2,len h21 -'1)) by XCMPLX_1:26;
                   0+1<=i-'len h11+1 by A905,AXIOMS:24;
                  then 0+1<=i-'len h11+1+1-1 by XCMPLX_1:26;
                  then 0+1<=i-'len h11+(1+1)-1 by XCMPLX_1:1;
                  then A907:i-'len h11+2-'1=i-'len h11+2-1 by JORDAN3:1;
                   0<=i-'len h11 by NAT_1:18;
                  then 0+2<=i-'len h11 +2 by AXIOMS:24;
                  then A908:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
                   i-len h11<=len h1+(len h2-2)-len h11 by A47,A748,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A904,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then i-'len h11+2<=len h2 by XCMPLX_1:27;
then i-'len h11 +2-'1<=len h21 by A23,JORDAN3:7;
then A909:           (i-'len h11 +2-'1) in dom h21 by A908,Lm2,FINSEQ_3:27;
              j+1 in dom h1 by A899,A901,FINSEQ_3:27;
                  then A910: h11.(j+1)=g1.(h1.(j+1)) by FUNCT_1:23;
                  A911:len h1 +1<=i by A903,NAT_1:38;
                  then A912:h0.i=(mid(h21,2,len h21 -'1)).(i -len h11)
                                      by A21,A40,A748,FINSEQ_1:36;
                   len h1 +1-len h1<=i-len h1 by A911,REAL_1:49;
                  then A913: 1<=i-len h11 by A21,XCMPLX_1:26;
                  then A914:h0.(i)=h21.(i-'len h11 +2-'1)
                    by A43,A44,A904,A906,A912,JORDAN3:27;
                   i+1-1<=len h1+(len h2-2)-1 by A47,A751,REAL_1:49;
                  then i<=len h1+(len h2-2)-1 by XCMPLX_1:26;
                  then i-len h11<=len h1+(len h2-2)-1-len h11 by REAL_1:49;
                  then i-len h11<=len h1+((len h2-2)-1)-len h11 by XCMPLX_1:29
;
                  then i-'len h11<=len h2-2-1 by A21,A904,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2-1+2 by AXIOMS:24;
                  then i-'len h11+2<=len h2-1 by XCMPLX_1:229;
                  then A915:i-'len h11+2-1<=len h2-1-1 by REAL_1:49;
A916:               len h2-1-1<len h2 by Lm5;
                  set k=i-'len h11+2-'1;
                  A917: h2.k in rng h2 by A22,A909,FUNCT_1:def 5;
                   j+1 in dom h1 by A899,A901,FINSEQ_3:27;
                  then A918: h1.(j+1) in rng h1 by FUNCT_1:def 5;
                  A919:h0.i=h21.k by A43,A44,A904,A906,A912,A913,JORDAN3:27;
                  A920:h0.i=g2.(h2.k)
                         & h21.k=g2.(h2.k) by A22,A909,A914,FUNCT_1:23;
A921:g1.(h1.(j+1)) in rng g1 by A6,A9,A918,BORSUK_1:83,FUNCT_1:def 5;
                  A922:h0.i in Lower_Arc(P)
                  by A13,A15,A16,A917,A920,BORSUK_1:83,FUNCT_1:def 5;
                   h0/.i <> W-min P
              by A22,A29,A31,A65,A750,A907,A909,A915,A916,A919,FUNCT_1:def 8;
                 hence thesis by A4,A750,A756,A902,A910,A921,A922,JORDAN6:def
10;
               end;
               hence thesis;
              case j+1>len h1;
               thus thesis by A745,A897;
              end;
             hence thesis;
            end;
          A923:1<j+1 by A749,NAT_1:38;
           now assume A924:h0/.(j+1)=h0/.i;
             now per cases;
            case A925:j+1<=len h1;
                then A926:j+1 in dom h1 by A923,FINSEQ_3:27;
                then A927: h1.(j+1) in rng h1 by FUNCT_1:def 5;
                A928:h0.(j+1)=h11.(j+1) by A21,A923,A925,SCMFSA_7:9;
                then h0.(j+1)=g1.(h1.(j+1)) by A926,FUNCT_1:23;
          then A929:h0.(j+1) in Upper_Arc(P) by A4,A6,A9,A927,BORSUK_1:83,
FUNCT_1:def 5;
              now per cases;
             case A930:i<=len h1;
                then A931:h0.i=h11.i by A21,A744,SCMFSA_7:9;
                 i in dom h1 by A744,A930,FINSEQ_3:27;
              hence contradiction
               by A20,A64,A750,A755,A756,A924,A926,A928,A931,FUNCT_1:def 8;
             case A932:i>len h1;
                  then A933:len h1 +1<=i by NAT_1:38;
then A934:     h0.i=(mid(h21,2,len h21 -'1)).(i -len h11)
                  by A21,A40,A748,FINSEQ_1:36;
                  A935:i-len h11=i-'len h11 by A21,A932,SCMFSA_7:3;
                   i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11
                                         by A40,A748,REAL_1:49;
                  then A936:i-len h11<= len (mid(h21,2,len h21 -'1))
                                             by XCMPLX_1:26;
                   len h1 +1-len h1<=i-len h1 by A933,REAL_1:49;
                  then 1<=i-len h1 by XCMPLX_1:26;
                  then A937:h0.i=h21.(i-'len h11 +2-'1)
                             by A21,A43,A44,A934,A935,A936,JORDAN3:27;
                   0<=i-'len h11 by NAT_1:18;
                  then A938: 0+2<=i-'len h11 +2 by AXIOMS:24;
                  then A939:2-'1<=(i-'len h11 +2-'1) by JORDAN3:5;
                   i-len h11<=len h1+(len h2-2)-len h11
                    by A47,A748,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A935,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then i-'len h11+2<=len h2 by XCMPLX_1:27;
                  then A940:1<=(i-'len h11 +2-'1) & (i-'len h11 +2-'1)<=len h21
                                    by A23,A938,Lm2,JORDAN3:5,7;
                  A941:i-'len h11+2-'1=i-'len h11+2-1
                          by A939,Lm2,JORDAN3:1;
                  set k=i-'len h11+2-'1;
                   i-len h11<=len h1+(len h2-2)-len h11 by A47,A748,REAL_1:49;
                  then i-'len h11<=len h2-2 by A21,A935,XCMPLX_1:26;
                  then i-'len h11+2<=len h2-2+2 by AXIOMS:24;
                  then A942:i-'len h11+2<=len h2 by XCMPLX_1:27;
                   i-'len h11+2-'1<i-'len h11+2-1+1 by A941,NAT_1:38;
                  then A943: i-'len h11+2-'1<i-'len h11+2 by XCMPLX_1:27;
                   len h11+1-len h11<=i-len h11 by A21,A933,REAL_1:49;
                  then 1<=i-len h11 by XCMPLX_1:26;
                  then 1<=i-'len h11 by JORDAN3:1;
                  then 1+2<=i-'len h11+2 by AXIOMS:24;
                  then 1+2-1<=i-'len h11+2-1 by REAL_1:49;
                  then A944:1<k by A941,AXIOMS:22;
                  A945:k in dom h2 by A22,A940,FINSEQ_3:27;
                  then A946:h0.i=g2.(h2.k) by A937,FUNCT_1:23;
                  A947: h2.k in rng h2 by A945,FUNCT_1:def 5;
                   i in dom h0 by A744,A748,FINSEQ_3:27;
                  then A948:h0/.i=h0.i by FINSEQ_4:def 4;
                g2.(h2.k) in rng g2 by A15,A16,A947,BORSUK_1:83,FUNCT_1:def 5;
               then h0.i in Upper_Arc(P) /\ Lower_Arc(P)
                         by A13,A756,A924,A929,A946,A948,XBOOLE_0:def 3;
               then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
               then h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2;
              hence contradiction by A22,A28,A29,A30,A31,A65,A937,A942,A943,
A944,A945,FUNCT_1:def 8;
             end;
             hence contradiction;
            case j+1>len h1;
                 thus contradiction by A745,A897;
            end;
           hence contradiction;
          end;
         hence Segment(h0/.j,h0/.(j+1),P) misses Segment(h0/.i,
         h0/.(i+1),P) by A1,A753,A754,A898,A900,Th13;
        end;
     hence Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P);
    end;
   let i be Nat such that
A949: 1 < i and
A950: i+1 < len h0;
A951:  i<len h0 by A950,NAT_1:38;
A952: LE h0/.i,h0/.(i+1),P by A550,A949,A950;
A953: 1<i+1 by A949,NAT_1:38;
A954: h0/.i<>h0/.(i+1) by A550,A949,A950;
A955: i in dom h0 by A949,A951,FINSEQ_3:27;
     then h0/.i = h0.i by FINSEQ_4:def 4;
then A956: h0/.i<>W-min P by A39,A61,A66,A949,A955,FUNCT_1:def 8;
A957: i+1 in dom h0 by A950,A953,FINSEQ_3:27;
A958: len h0-len h11 <= len (mid(h21,2,len h21 -'1)) by A40,XCMPLX_1:26;
      set k=len h0-'len h11+2-'1;
       0<=len h0-'len h11 by NAT_1:18;
      then 0+2<=len h0-'len h11 +2 by AXIOMS:24;
then A959: 2-'1<=len h0-'len h11 +2-'1 by JORDAN3:5;
       len h0-'len h11+2<=len h2-2+2 by A21,A47,A54,XCMPLX_1:26;
      then len h0-'len h11+2<=len h2 by XCMPLX_1:27;
      then (len h0-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7;
      then A960: (len h0-'len h11 +2-'1) in dom h21 by A959,Lm2,FINSEQ_3:27;
 h0.len h0=mid(h21,2,len h21 -'1).(len h0 -len h11)
                        by A21,A40,A48,FINSEQ_1:36;
then A961: h0.len h0=h21.(len h0-'len h11 +2-'1)
             by A21,A43,A44,A53,A54,A958,JORDAN3:27;
A962: h21.k=g2.(h2.k) by A22,A960,FUNCT_1:23;
      A963: h2.k in rng h2 by A22,A960,FUNCT_1:def 5;
then A964: h0.len h0 in Lower_Arc(P) by A13,A15,A16,A961,A962,BORSUK_1:83,
FUNCT_1:def 5;
A965:LE h0/.(i+1),h0/.len h0,P
      proof
       per cases;
       suppose A966:i+1<=len h1;
then A967:      h0.(i+1)=h11.(i+1) by A21,A953,SCMFSA_7:9;
          i+1 in dom h1 by A953,A966,FINSEQ_3:27;
         then A968:      h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:23;
                   i+1 in dom h1 by A953,A966,FINSEQ_3:27;
                  then A969: h1.(i+1) in rng h1 by FUNCT_1:def 5;
                  A970:h0/.(i+1)=h0.(i+1) by A957,FINSEQ_4:def 4;
                        g1.(h1.(i+1)) in rng g1 by A6,A9,A969,BORSUK_1:83,
FUNCT_1:def 5;
        hence thesis by A4,A52,A121,A964,A967,A968,A970,JORDAN6:def 10;
       suppose A971:i+1>len h1;
A972:             0<=len h0-'len h11 by A21,A49,A54,SQUARE_1:12;
                  A973:len h0-len h11
                      <= len (mid(h21,2,len h21 -'1)) by A40,XCMPLX_1:26;
                   0+1<=len h0-'len h11+1 by A972,AXIOMS:24;
                  then 0+1<=len h0-'len h11+1+1-1 by XCMPLX_1:26;
                  then 0+1<=len h0-'len h11+(1+1)-1 by XCMPLX_1:1;
                  then A974:len h0-'len h11+2-'1=len h0-'len h11+2-1 by JORDAN3
:1;
                   len h0-'len h11+2<=len h2-2+2
                        by A21,A47,A54,XCMPLX_1:26;
                  then len h0-'len h11+2<=len h2 by XCMPLX_1:27;
then A975: (len h0-'len h11 +2-'1)<=len h21 by A23,JORDAN3:7;
                  then A976:len h0-'len h11 +2-'1 in dom h21
                  by A959,Lm2,FINSEQ_3:27;
A977:             len h11+1<=i+1 by A21,A971,NAT_1:38;
A978:             i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A950,FINSEQ_1:
35;
                   i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11
                             by A40,A950,REAL_1:54;
                  then A979:i+1-len h11<len (mid(h21,2,len h21 -'1)) by
XCMPLX_1:26;
                   len h1+1<=i+1 by A971,NAT_1:38;
                  then len h1+1-len h1<=i+1-len h1 by REAL_1:49;
then A980:              1<=i+1-len h1 by XCMPLX_1:26;
then A981:             i+1-'len h11=i+1-len h11 by A21,JORDAN3:1;
A982:              h0.(i+1) = mid(h21,2,len h21 -'1).(i+1 -len h11)
                                      by A977,A978,FINSEQ_1:36
                          .= h21.(i+1-'len h11+2-'1)
                    by A21,A43,A44,A979,A980,A981,JORDAN3:27;
A983:             (i+1)-len h11=(i+1)-'len h11 by A21,A971,SCMFSA_7:3;
A984:             (len h0-'len h11 +2-'1) in dom h21 by A959,A975,Lm2,FINSEQ_3:
27;
                  h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11)
                                      by A21,A40,A48,FINSEQ_1:36;
                  then A985:h0.len h0=h21.(len h0-'len h11 +2-'1)
                    by A21,A43,A44,A53,A54,A973,JORDAN3:27;
                   0<=(i+1)-'len h11 by NAT_1:18;
                  then 0+2<=(i+1)-'len h11 +2 by AXIOMS:24;
                  then A986:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5;
                   (i+1)-len h11<=len h11+(len h2-2)-len h11
                                    by A21,A47,A950,REAL_1:49;
                  then (i+1)-len h11<=(len h2-2) by XCMPLX_1:26;
                  then (i+1)-'len h11+2<=len h2-2+2 by A983,AXIOMS:24;
then            (i+1)-'len h11+2<=len h2 by XCMPLX_1:27;
then A987:           (i+1)-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7;
                  A988:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1
                                  by A986,Lm2,JORDAN3:1;
                  set k=len h0-'len h11+2-'1;
                  set j0=(i+1)-'len h11+2-'1;
                   (i+1)-len h11<len h0-len h11 by A950,REAL_1:54;
                  then (i+1)-'len h11+2<len h0-'len h11+2 by A54,A983,REAL_1:53
;
                  then A989:j0<k by A974,A988,REAL_1:54;
                  A990:h21.k=g2.(h2.k) by A22,A976,FUNCT_1:23;
A991:              h2.k in rng h2 by A22,A984,FUNCT_1:def 5;
then A992:             0<=h2.k by A16,BORSUK_1:83,TOPREAL5:1;
A993:             h2.k<=1 by A16,A991,BORSUK_1:83,TOPREAL5:1;
                  A994:j0 in dom h2 by A22,A986,A987,Lm2,FINSEQ_3:27;
                  then A995:h0.(i+1)=g2.(h2.j0) by A982,FUNCT_1:23;
A996:              h2.j0 in rng h2 by A994,FUNCT_1:def 5;
then A997:             0<=h2.j0 by A16,BORSUK_1:83,TOPREAL5:1;
A998:             h2.j0<=1 by A16,A996,BORSUK_1:83,TOPREAL5:1;
                  A999:h2.(j0)<h2.(k)
                  by A16,A22,A984,A989,A994,GOBOARD1:def 1;
                  A1000:h0/.(i+1)=h0.(i+1) by A957,FINSEQ_4:def 4;
                  g2.(h2.j0) in rng g2 by A15,A16,A996,BORSUK_1:83,FUNCT_1:def
5;
                  then A1001:h0.(i+1) in Lower_Arc(P) by A13,A982,A994,FUNCT_1:
23;
                  h0.(len h0) in Lower_Arc(P) by A13,A15,A16,A961,A962,A963,
BORSUK_1:83,FUNCT_1:def 5;
then A1002:       h0/.len h0 in Lower_Arc P by A51,FINSEQ_4:def 4;
         LE h0/.(i+1),h0/.len h0,Lower_Arc(P),E-max(P),W-min(P)
             by A11,A12,A13,A14,A52,A985,A990,A992,A993,A995,A997,A998,A999,
A1000,Th19;
       hence thesis by A121,A1000,A1001,A1002,JORDAN6:def 10;
      end;
           now assume A1003:h0/.(i+1)=h0/.len h0;
             now per cases;
            case A1004:i+1<=len h1;
                 i+1 in dom h0 by A950,A953,FINSEQ_3:27;
                then A1005:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
                A1006:h0.(i+1)=h11.(i+1) by A21,A953,A1004,SCMFSA_7:9;
                A1007:i+1 in dom h1 by A953,A1004,FINSEQ_3:27;
                then A1008:h0.(i+1)=g1.(h1.(i+1)) by A1006,FUNCT_1:23;
                 h1.(i+1) in rng h1 by A1007,FUNCT_1:def 5;
                then A1009:h0.(i+1) in Upper_Arc(P)
                             by A4,A6,A9,A1008,BORSUK_1:83,FUNCT_1:def 5;
A1010: h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11)
              by A21,A40,A48,FINSEQ_1:36;
                  len h0-len h11<= len (mid(h21,2,len h21 -'1))
                                             by A40,XCMPLX_1:26;
                  then A1011:h0.len h0=h21.(len h0-'len h11 +2-'1)
                             by A21,A43,A44,A53,A54,A1010,JORDAN3:27;
                   0<=len h0-'len h11 by NAT_1:18;
                  then 0+2<=len h0-'len h11 +2 by AXIOMS:24;
                  then A1012:2-'1<=(len h0-'len h11 +2-'1) by JORDAN3:5;
                   len h0-'len h11+2<=len h2-2+2
                           by A21,A47,A54,XCMPLX_1:26;
then             len h0-'len h11+2<=len h2 by XCMPLX_1:27;
then A1013:            len h0-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7;
                  A1014:len h0-'len h11+2-'1=len h0-'len h11+2-1
                     by A1012,Lm2,JORDAN3:1;
                  set k=len h0-'len h11+2-'1;
                   len h0-'len h11+2<=len h2-2+2
                      by A21,A47,A54,XCMPLX_1:26;
                  then A1015:len h0-'len h11+2<=len h2 by XCMPLX_1:27;
                   len h0-'len h11+2-'1<len h0-'len h11+2-'1+1 by NAT_1:38;
                  then A1016: len h0-'len h11+2-'1<len h0-'len h11+2 by A1014,
XCMPLX_1:27;
                   1+2<=len h0-'len h11+2 by A55,AXIOMS:24;
                  then 1+2-1<=len h0-'len h11+2-1 by REAL_1:49;
                  then A1017:1<k by A1014,AXIOMS:22;
                  A1018:k in dom h2 by A22,A1012,A1013,Lm2,FINSEQ_3:27;
                  then A1019:h0.len h0=g2.(h2.k) by A1011,FUNCT_1:23;
                   h2.k in rng h2 by A1018,FUNCT_1:def 5;
                  then g2.(h2.k) in rng g2 by A15,A16,BORSUK_1:83,FUNCT_1:def 5
;
                  then h0.len h0 in Upper_Arc(P) /\ Lower_Arc(P)
                   by A13,A52,A1003,A1005,A1009,A1019,XBOOLE_0:def 3;
then A1020:         h0.len h0 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
A1021:         h0.len h0 <> W-min P
                     by A22,A29,A31,A65,A1011,A1015,A1016,A1018,FUNCT_1:def 8;
                h0.len h0 <> E-max P
                    by A22,A28,A30,A65,A1011,A1017,A1018,FUNCT_1:def 8;
              hence contradiction by A1020,A1021,TARSKI:def 2;
            case A1022:i+1>len h1;
                  then A1023:len h1 +1<=i+1 by NAT_1:38;
A1024:        i+1 <= len h11 + len mid(h21,2,len h21 -'1) by A950,FINSEQ_1:35;
                  A1025:h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11)
                                     by A21,A40,A950,A1023,FINSEQ_1:36;
                  A1026:(i+1)-len h11=(i+1)-'len h11 by A21,A1022,SCMFSA_7:3;
                   i+1-len h11
                   <=len h11 + len mid(h21,2,len h21 -'1)-len h11
                                         by A1024,REAL_1:49;
                  then A1027:(i+1)-len h11<= len (mid(h21,2,len h21 -'1))
                                             by XCMPLX_1:26;
                   len h1 +1-len h1<=(i+1)-len h1 by A1023,REAL_1:49;
                  then 1<=(i+1)-len h11 by A21,XCMPLX_1:26;
                  then A1028:h0.(i+1)=h21.((i+1)-'len h11 +2-'1)
                             by A43,A44,A1025,A1026,A1027,JORDAN3:27;
                   0<=(i+1)-'len h11 by NAT_1:18;
                  then 0+2<=(i+1)-'len h11 +2 by AXIOMS:24;
                  then A1029:2-'1<=((i+1)-'len h11 +2-'1) by JORDAN3:5;
                   (i+1)-len h11<=len h1+(len h2-2)-len h11
                            by A47,A950,REAL_1:49;
                  then (i+1)-len h11<=(len h2-2) by A21,XCMPLX_1:26;
                  then (i+1)-'len h11+2<=len h2-2+2 by A1026,AXIOMS:24;
then              (i+1)-'len h11+2<=len h2 by XCMPLX_1:27;
then A1030:            (i+1)-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7;
                  A1031:(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1
                                 by A1029,Lm2,JORDAN3:1;
                  set j0=(i+1)-'len h11+2-'1;
                   len h11+1-len h11<=(i+1)-len h11
                           by A21,A1023,REAL_1:49;
                  then 1<=(i+1)-len h11 by XCMPLX_1:26;
                  then A1032:(i+1)-'len h11=(i+1)-len h11 by JORDAN3:1;
                 A1033:j0 in dom h2 by A22,A1029,A1030,Lm2,FINSEQ_3:27;
                   1<=i+1 by A949,NAT_1:38;
                  then i+1 in dom h0 by A950,FINSEQ_3:27;
                  then A1034:h0/.(i+1)=h0.(i+1) by FINSEQ_4:def 4;
A1035: h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11)
                     by A21,A40,A48,FINSEQ_1:36;
                  len h0-len h11<= len (mid(h21,2,len h21 -'1))
                                             by A40,XCMPLX_1:26;
                  then A1036:h0.len h0=h21.(len h0-'len h11 +2-'1)
                             by A43,A44,A54,A55,A1035,JORDAN3:27;
                   0<=len h0-'len h11 by NAT_1:18;
                  then 0+2<=len h0-'len h11 +2 by AXIOMS:24;
                  then A1037:2-'1<=(len h0-'len h11 +2-'1) by JORDAN3:5;
                   len h0-'len h11+2<=len h2-2+2
                    by A21,A47,A54,XCMPLX_1:26;
then              len h0-'len h11+2<=len h2 by XCMPLX_1:27;
then A1038:            len h0-'len h11 +2-'1 <= len h21 by A23,JORDAN3:7;
                  A1039:len h0-'len h11+2-'1=len h0-'len h11+2-1
                      by A1037,Lm2,JORDAN3:1;
                  set k=len h0-'len h11+2-'1;
                   len h0-'len h11=len h0-len h11 by A21,A53,JORDAN3:1;
                  then i+1-'len h11<len h0-'len h11 by A950,A1032,REAL_1:54;
                  then i+1-'len h11+2<len h0-'len h11+2 by REAL_1:53;
                  then A1040:            (i+1)-'len h11+2-'1<len h0-'len h11+2
-'1
                             by A1031,A1039,REAL_1:54;
                 k in dom h2 by A22,A1037,A1038,Lm2,FINSEQ_3:27;
              hence contradiction by A22,A52,A65,A1003,A1028,A1033,A1034,A1036,
A1040,FUNCT_1:def 8;
            end;
           hence contradiction;
          end;
   hence Segment(h0/.len h0,h0/.1,P) misses Segment(h0/.i,h0/.(i+1),P)
                   by A1,A39,A62,A952,A954,A956,A965,Th14;
  end;

Back to top