:: On a Dividing Function of the Simple Closed Curve into Segments
:: by Yatsuka Nakamura
::
:: Received June 16, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, EUCLID, ARYTM_1, SUBSET_1, XXREAL_0, ARYTM_3,
RCOMP_1, XBOOLE_0, TOPREAL2, PSCOMP_1, JORDAN6, TOPREAL1, JORDAN3,
TARSKI, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, STRUCT_0, FINSEQ_1,
CARD_1, XXREAL_1, REAL_1, PARTFUN1, MEASURE5, GOBRD10, ORDINAL4, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RCOMP_1, NAT_D, FINSEQ_1, FUNCT_1, RELSET_1, PARTFUN1,
VALUED_0, TOPREAL1, TOPREAL2, TBSP_1, GOBRD10, PRE_TOPC, TOPS_2,
FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, PSCOMP_1, JORDAN5C, JORDAN6,
TOPMETR, XXREAL_0;
constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, COMPTS_1, TBSP_1, TOPMETR,
TOPREAL1, PSCOMP_1, GOBRD10, JORDAN5C, JORDAN6, XXREAL_2, FINSEQ_6;
registrations RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC,
EUCLID, TOPREAL1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2, FINSEQ_1,
FUNCT_1, ORDINAL1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, JORDAN6, TOPREAL1, TOPREAL5, JORDAN5C, UNIFORM1, PRE_TOPC,
FUNCT_2, TOPS_2, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, NAT_1, FINSEQ_4,
GOBRD10, SPRECT_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, BORSUK_1, COMPTS_1,
RELSET_1, JORDAN5B, PARTFUN2, XCMPLX_1, XREAL_1, XXREAL_0, PARTFUN1,
XXREAL_1, XXREAL_2, SEQM_3, NAT_D, XREAL_0, FINSEQ_6;
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: 2-'1 = 2-1 by XREAL_1:233
.=1;
Lm2: 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,XREAL_1:6;
hence thesis by A2,XREAL_1:235;
end;
suppose
A3: i <= k;
k <= j + k by NAT_1:11;
hence thesis by A3,XXREAL_0:2;
end;
end;
Lm3: 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,XXREAL_0:1;
suppose
j + k = i;
hence thesis by NAT_D:34;
end;
suppose
j + k < i;
hence thesis by Lm2;
end;
end;
theorem Th1:
for P being compact non empty Subset of TOP-REAL 2 st P is
being_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 being_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:50;
hence thesis by TOPREAL1:1;
end;
theorem Th2:
for P being compact non empty Subset of TOP-REAL 2,q st P is
being_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 P is being_simple_closed_curve & LE q,W-min(P),P;
then
LE q,W-min(P),Upper_Arc(P),W-min(P),E-max(P) & Upper_Arc(P) is_an_arc_of
W-min(P),E-max(P) by JORDAN6:def 8,def 10;
hence thesis by JORDAN6:54;
end;
theorem Th3:
for P being compact non empty Subset of TOP-REAL 2,q st P is
being_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 that
A1: P is being_simple_closed_curve and
A2: q in P;
A3: q in Upper_Arc(P) \/ Lower_Arc(P) by A1,A2,JORDAN6:50;
A4: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
A5: W-min(P) in Upper_Arc(P) by A1,Th1;
per cases by A3,XBOOLE_0:def 3;
suppose
A6: q in Upper_Arc(P);
then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A4,JORDAN5C:10;
hence thesis by A5,A6,JORDAN6:def 10;
end;
suppose
A7: q in Lower_Arc(P);
per cases;
suppose
not q=W-min(P);
hence thesis by A5,A7,JORDAN6:def 10;
end;
suppose
A8: q=W-min(P);
then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A5,JORDAN5C:9;
hence thesis by A5,A8,JORDAN6:def 10;
end;
end;
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
per cases;
suppose
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 DOMAIN_1:sch 7;
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};
hence thesis by A1;
end;
suppose
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 DOMAIN_1:sch 7;
then reconsider
C = {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} as Subset of
TOP-REAL 2;
not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P )};
hence thesis by A2;
end;
end;
hence thesis;
end;
end;
theorem
for P being compact non empty Subset of TOP-REAL 2 st P is
being_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 being_simple_closed_curve;
then
A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
A3: {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} = Lower_Arc(P)
proof
A4: {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 object;
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
A5: p1=x and
A6: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P);
per cases by A6;
suppose
A7: LE E-max(P),p1,P;
per cases by A5,A7,JORDAN6:def 10;
suppose
x in Lower_Arc(P);
hence thesis;
end;
suppose
A8: 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);
A9: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
then LE p1,E-max(P),Upper_Arc(P),W-min(P),E-max(P) by A8,JORDAN5C:10;
then
A10: p1=E-max(P) by A8,A9,JORDAN5C:12;
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
hence thesis by A5,A10,TOPREAL1:1;
end;
end;
suppose
E-max(P) in P & p1=W-min(P);
then x in {W-min(P),E-max(P)} by A5,TARSKI:def 2;
then x in Upper_Arc(P) /\ Lower_Arc(P) by A1,JORDAN6:def 9;
hence thesis by XBOOLE_0:def 4;
end;
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 object;
assume
A11: 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:50;
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 A11,SPRECT_1:14,TOPREAL1:1;
then LE E-max(P),p2,P or E-max P in P & p2=W-min P by JORDAN6:def 10;
hence thesis;
end;
hence thesis by A4;
end;
A12: E-max(P)<>W-min(P) by A1,TOPREAL5:19;
{p: LE W-min(P),p,P & LE p,E-max(P),P} = Upper_Arc(P)
proof
A13: {p: LE W-min(P),p,P & LE p,E-max(P),P} c= Upper_Arc(P)
proof
let x be object;
assume x in {p: LE W-min(P),p,P & LE p,E-max(P),P};
then consider p such that
A14: p=x and
LE W-min(P),p,P and
A15: LE p,E-max(P),P;
per cases by A15,JORDAN6:def 10;
suppose
p in Upper_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)= W-min(P);
hence thesis by A14;
end;
suppose
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 thesis by A14;
end;
suppose
A16: 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 A16,JORDAN6:54;
hence thesis by A2,A14,TOPREAL1:1;
end;
end;
Upper_Arc(P) c= {p: LE W-min(P),p,P & LE p,E-max(P),P}
proof
let x be object;
assume
A17: x in Upper_Arc(P);
then reconsider p2=x as Point of TOP-REAL 2;
E-max(P) in Lower_Arc(P) by A1,Th1;
then
A18: LE p2,E-max(P),P by A12,A17,JORDAN6:def 10;
A19: W-min(P) in Upper_Arc(P) by A1,Th1;
LE W-min(P),p2,Upper_Arc(P),W-min(P),E-max(P) by A2,A17,JORDAN5C:10;
then LE W-min(P),p2,P by A17,A19,JORDAN6:def 10;
hence thesis by A18;
end;
hence thesis by A13;
end;
hence thesis by A12,A3,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 being_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 that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P;
A3: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:50;
per cases by A2,JORDAN6:def 10;
suppose
q1 in Upper_Arc(P) & q2 in Lower_Arc(P);
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose
q1 in Upper_Arc(P) & q2 in Upper_Arc(P);
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose
q1 in Lower_Arc(P) & q2 in Lower_Arc(P);
hence thesis by A3,XBOOLE_0:def 3;
end;
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 being_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 that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P;
hereby
per cases;
suppose
A3: q2<>W-min(P);
q1 in P by A1,A2,Th5;
then LE q1,q1,P by A1,JORDAN6:56;
then q1 in {p: LE q1,p,P & LE p,q2,P} by A2;
hence q1 in Segment(q1,q2,P) by A3,Def1;
end;
suppose
A4: q2=W-min(P);
q1 in P by A1,A2,Th5;
then LE q1,q1,P by A1,JORDAN6:56;
then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
hence q1 in Segment(q1,q2,P) by A4,Def1;
end;
end;
per cases;
suppose
A5: q2<>W-min(P);
q2 in P by A1,A2,Th5;
then LE q2,q2,P by A1,JORDAN6:56;
then q2 in {p: LE q1,p,P & LE p,q2,P} by A2;
hence thesis by A5,Def1;
end;
suppose
A6: q2=W-min(P);
q2 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} by A2;
hence thesis by A6,Def1;
end;
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 being_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 being_simple_closed_curve;
then LE q1,q1,P by A1,JORDAN6:56;
then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
hence thesis 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 being_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 being_simple_closed_curve and
A2: q in P and
A3: q <> W-min P;
for x being object holds x in Segment(q,q,P) iff x=q
proof
let x be object;
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:57;
end;
assume
A4: x=q;
LE q,q,P by A1,A2,JORDAN6:56;
then x in {p: LE q,p,P & LE p,q,P} by A4;
hence thesis 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 being_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 that
A1: P is being_simple_closed_curve and
A2: q1<>W-min(P) and
A3: q2<>W-min(P);
A4: Segment(q1,q2,P)={p: LE q1,p,P & LE p,q2,P} by A3,Def1;
now
A5: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
assume W-min(P) in Segment(q1,q2,P);
then consider p such that
A6: p=W-min(P) and
A7: LE q1,p,P and
LE p,q2,P by A4;
LE q1,p,Upper_Arc(P),W-min(P),E-max(P) by A6,A7,JORDAN6:def 10;
hence contradiction by A2,A6,A5,JORDAN6:54;
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 being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & not(q1=q2 & q1=W-min(P)) & 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 that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: not(q1=q2 & q1=W-min(P)) and
A5: not(q2=q3 & q2=W-min(P));
A6: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
thus Segment(q1,q2,P)/\ Segment(q2,q3,P) c= {q2}
proof
let x be object;
assume
A7: x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
then
A8: x in Segment(q2,q3,P) by XBOOLE_0:def 4;
A9: x in Segment(q1,q2,P) by A7,XBOOLE_0:def 4;
now
per cases;
case
q3<>W-min(P);
then x in {p: LE q2,p,P & LE p,q3,P} by A8,Def1;
then
A10: ex p st p=x & LE q2,p,P & LE p,q3,P;
per cases;
suppose
q2<>W-min(P);
then x in {p2: LE q1,p2,P & LE p2,q2,P} by A9,Def1;
then ex p2 st p2=x & LE q1,p2,P & LE p2,q2,P;
hence x=q2 by A1,A10,JORDAN6:57;
end;
suppose
A11: q2=W-min(P);
then LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) by A2,JORDAN6:def 10;
hence x=q2 by A4,A6,A11,JORDAN6:54;
end;
end;
case
A12: q3=W-min(P);
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A8,Def1;
then consider p1 such that
A13: p1=x and
A14: LE q2,p1,P or q2 in P & p1=W-min(P);
p1 in {p: LE q1,p,P & LE p,q2,P} by A5,A9,A12,A13,Def1;
then ex p st p=p1 & LE q1,p,P & LE p,q2,P;
hence x=q2 by A1,A3,A12,A13,A14,JORDAN6:57;
end;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {q2};
then x=q2 by TARSKI:def 1;
then x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by A1,A2,A3,Th6;
hence thesis by XBOOLE_0:def 4;
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 being_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 that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: q1<>q3 and
A4: not q2=W-min(P);
thus Segment(q1,q2,P)/\ Segment(q2,W-min P,P) c= {q2}
proof
let x be object;
assume
A5: x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
then x in Segment(q2,q3,P) by XBOOLE_0:def 4;
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min P} by Def1;
then consider p1 such that
A6: p1=x and
A7: LE q2,p1,P or q2 in P & p1=W-min P;
x in Segment(q1,q2,P) by A5,XBOOLE_0:def 4;
then p1 in {p: LE q1,p,P & LE p,q2,P} by A4,A6,Def1;
then
A8: ex p st p=p1 & LE q1,p,P & LE p,q2,P;
per cases by A7;
suppose
LE q2,p1,P;
then x=q2 by A1,A6,A8,JORDAN6:57;
hence thesis by TARSKI:def 1;
end;
suppose
q2 in P & p1=W-min(P);
hence thesis by A1,A3,A8,Th2;
end;
end;
let x be object;
assume x in {q2};
then
A9: x=q2 by TARSKI:def 1;
q2 in P by A1,A2,Th5;
then
A10: x in Segment(q2,q3,P) by A1,A9,Th7;
x in Segment(q1,q2,P) by A1,A2,A9,Th6;
hence thesis by A10,XBOOLE_0:def 4;
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 being_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 that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: q1<>q2 and
A4: q1<>W-min(P);
thus Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P) c= {W-min(P)}
proof
let x be object;
assume
A5: x in Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P);
then x in Segment(q2,W-min(P),P) by XBOOLE_0:def 4;
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by Def1;
then consider p1 such that
A6: p1=x and
A7: LE q2,p1,P or q2 in P & p1=W-min(P);
A8: x in Segment(W-min(P),q1,P) by A5,XBOOLE_0:def 4;
now
per cases by A7;
case
A9: LE q2,p1,P;
x in {p: LE W-min(P),p,P & LE p,q1,P} by A4,A8,Def1;
then ex p2 st p2=x & LE W-min(P),p2,P & LE p2,q1,P;
then LE q2,q1,P by A1,A6,A9,JORDAN6:58;
hence contradiction by A1,A2,A3,JORDAN6:57;
end;
case
q2 in P & p1=W-min(P);
hence x=W-min(P) by A6;
end;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {W-min(P)};
then
A10: x=W-min(P) by TARSKI:def 1;
q2 in P by A1,A2,Th5;
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A10;
then
A11: x in Segment(q2,W-min(P),P) by Def1;
q1 in P by A1,A2,Th5;
then LE W-min(P),q1,P by A1,Th3;
then x in Segment(W-min(P),q1,P) by A1,A10,Th6;
hence thesis by A11,XBOOLE_0:def 4;
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 being_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 being_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;
set x = the Element of Segment(q1,q2,P)/\ Segment(q3,q4,P);
assume
A7: Segment(q1,q2,P)/\ Segment(q3,q4,P)<>{};
then
A8: x in Segment(q1,q2,P) by XBOOLE_0:def 4;
A9: x in Segment(q3,q4,P) by A7,XBOOLE_0:def 4;
per cases;
suppose
q4=W-min(P);
then q3=W-min(P) by A1,A4,Th2;
hence contradiction by A1,A3,A6,Th2;
end;
suppose
A10: q4<>W-min(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
A11: ex p2 st p2=x & LE q1,p2,P & LE p2,q2,P;
x in {p1: LE q3,p1,P & LE p1,q4,P} by A9,A10,Def1;
then ex p1 st p1=x & LE q3,p1,P & LE p1,q4,P;
then LE q3,q2,P by A1,A11,JORDAN6:58;
hence contradiction by A1,A3,A6,JORDAN6:57;
end;
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 being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & q1<>W-min P & 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 that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: q1<>W-min P and
A5: q2<>q3;
set x = the Element of Segment(q1,q2,P)/\ Segment(q3,W-min P,P);
assume
A6: Segment(q1,q2,P)/\ Segment(q3,W-min P,P)<>{};
then
A7: x in Segment(q1,q2,P) by XBOOLE_0:def 4;
x in Segment(q3,W-min P,P) by A6,XBOOLE_0:def 4;
then x in {p1: LE q3,p1,P or q3 in P & p1=W-min P} by Def1;
then
A8: ex p1 st p1=x &( LE q3,p1,P or q3 in P & p1=W-min P);
q2 <> W-min P by A1,A2,A4,Th2;
then x in {p: LE q1,p,P & LE p,q2,P} by A7,Def1;
then ex p3 st p3 = x & LE q1,p3,P & LE p3,q2,P;
then LE q3,q2,P by A1,A4,A8,Th2,JORDAN6:58;
hence contradiction by A1,A3,A5,JORDAN6:57;
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 Function of
I[01], (TOP-REAL n)|P st f is being_homeomorphism ex g being Function 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 Function of I[01], (TOP-REAL n
)|P;
A1: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 5;
the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) .=P by PRE_TOPC:def 5;
then reconsider g1=f as Function of I[01],TOP-REAL n by FUNCT_2:7;
assume
A2: f is being_homeomorphism;
then
A3: f is one-to-one by TOPS_2:def 5;
A4: [#]((TOP-REAL n)|P) <> {} & f is continuous by A2,TOPS_2:def 5;
A5: 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;
reconsider B1=P2 /\ P as Subset of (TOP-REAL n)|P by A1,XBOOLE_1:17;
f"(rng f) c= f"P by A1,RELAT_1:143;
then
A6: dom f c= f"P by RELAT_1:134;
assume P2 is open;
then B1 is open by A1,TOPS_2:24;
then
A7: f"B1 is open by A4,TOPS_2:43;
f"P c= dom f by RELAT_1:132;
then f"B1 = f"P2 /\ f"P & f"P=dom f by A6,FUNCT_1:68;
hence thesis by A7,RELAT_1:132,XBOOLE_1:28;
end;
[#]TOP-REAL n <> {};
then g1 is continuous by A5,TOPS_2:43;
hence thesis by A3;
end;
theorem Th16:
for P being non empty Subset of TOP-REAL n, g being Function of
I[01], (TOP-REAL n) st g is continuous one-to-one & rng g = P ex f being
Function of I[01],(TOP-REAL n)|P st f=g & f is being_homeomorphism
proof
let P be non empty Subset of TOP-REAL n, g be Function 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);
then
A3: the carrier of (TOP-REAL n)|P = P by PRE_TOPC:def 5;
then reconsider f=g as Function of I[01],(TOP-REAL n)|P by A2,FUNCT_2:6;
take f;
thus f = g;
A4: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 5;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1
.= [#]I[01];
A6: [#]TOP-REAL n<>{};
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 P2 is open;
then consider C being Subset of TOP-REAL n such that
A7: C is open and
A8: C /\ [#]((TOP-REAL n)|P) = P2 by TOPS_2:24;
g"P = [#]I[01] by A3,A5,RELSET_1:22;
then f"P2 = f"C /\ [#]I[01] by A4,A8,FUNCT_1:68
.= f"C by XBOOLE_1:28;
hence thesis by A1,A6,A7,TOPS_2:43;
end;
then
A9: f is continuous by A4,TOPS_2:43;
rng f = [#]((TOP-REAL n)|P) by A2,PRE_TOPC:def 5;
hence thesis by A1,A9,COMPTS_1:17;
end;
Lm4: now
let h2 be Nat;
h2<h2+1 by NAT_1:13;
then
A1: h2-1<h2+1-1 by XREAL_1:9;
then h2-1-1<h2-1 by XREAL_1:9;
hence h2-1-1<h2 by A1,XXREAL_0:2;
end;
Lm5: 0 in [.0,1.] by XXREAL_1:1;
Lm6: 1 in [.0,1.] by XXREAL_1:1;
theorem Th17:
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 Function 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 A9 = A as non empty Subset of TOP-REAL 2 by TOPREAL1:1;
consider f being Function of I[01], (TOP-REAL 2)|A9 such that
A2: f is being_homeomorphism and
A3: f.0 = p1 & f.1 = p2 by A1,TOPREAL1:def 1;
consider g being Function 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;
rng f=[#]((TOP-REAL 2)|A9) by A2,TOPS_2:def 5;
hence rng g = A by A4,PRE_TOPC:def 5;
thus thesis by A3,A4;
end;
theorem Th18:
for P being non empty Subset of TOP-REAL 2, p1, p2, q1, q2 being
Point of TOP-REAL 2, g being Function 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 Function 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 & rng g = P;
ex f being Function of I[01],(TOP-REAL 2)|P st f=g & f is
being_homeomorphism by A2,Th16;
hence thesis by A1,JORDAN5C:8;
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 Function 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 Function of I[01], TOP-REAL 2, s1, s2 be Real;
assume g is continuous one-to-one & rng g = P;
then ex f being Function of I[01],(TOP-REAL 2)|P st f=g & f is
being_homeomorphism by 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 being_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 & i,j aren't_adjacent 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 that
A1: P is being_simple_closed_curve and
A2: e > 0;
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1,JORDAN6:def 8;
then consider g1 being Function of I[01], TOP-REAL 2 such that
A4: g1 is continuous one-to-one and
A5: rng g1 = Upper_Arc P and
A6: g1.0 = W-min P and
A7: g1.1 = E-max P by Th17;
consider h1 being FinSequence of REAL such that
A8: h1.1=0 and
A9: h1.len h1=1 and
A10: 5<=len h1 and
A11: rng h1 c= the carrier of I[01] and
A12: h1 is increasing and
A13: 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 A2,A4,UNIFORM1:13;
h1 is FinSequence of the carrier of I[01] by A11,FINSEQ_1:def 4;
then reconsider h11=g1*h1 as FinSequence of the carrier of TOP-REAL 2 by
FINSEQ_2:32;
A14: 2<len h1 by A10,XXREAL_0:2;
then
A15: 2 in dom h1 by FINSEQ_3:25;
A16: 1<=len h1 by A10,XXREAL_0:2;
then
A17: 1 in dom h1 by FINSEQ_3:25;
A18: 1+1 in dom h1 by A14,FINSEQ_3:25;
then
A19: h1.(1+1) in rng h1 by FUNCT_1:def 3;
A20: h11 is one-to-one by A4,A12;
A21: Lower_Arc P is_an_arc_of E-max P, W-min P by A1,JORDAN6:def 9;
then consider g2 being Function of I[01], TOP-REAL 2 such that
A22: g2 is continuous one-to-one and
A23: rng g2 = Lower_Arc P and
A24: g2.0 = E-max P and
A25: g2.1 = W-min P by Th17;
consider h2 being FinSequence of REAL such that
A26: h2.1=0 and
A27: h2.len h2=1 and
A28: 5<=len h2 and
A29: rng h2 c= the carrier of I[01] and
A30: h2 is increasing and
A31: 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 A2,A22,UNIFORM1:13;
h2 is FinSequence of the carrier of I[01] by A29,FINSEQ_1:def 4;
then reconsider h21=g2*h2 as FinSequence of the carrier of TOP-REAL 2 by
FINSEQ_2:32;
A32: h21 is one-to-one by A22,A30;
A33: 1<=len h2 by A28,XXREAL_0:2;
then
A34: len h2 in dom h2 by FINSEQ_3:25;
then
A35: h21.len h2=W-min P by A25,A27,FUNCT_1:13;
reconsider h0=h11^(mid(h21,2,len h21-' 1)) as FinSequence of the carrier of
TOP-REAL 2;
A36: len h0=len h11+len (mid(h21,2,len h21 -'1)) by FINSEQ_1:22;
set i = len h0-'1;
take h0;
A37: rng h1 c= dom g1 by A11,FUNCT_2:def 1;
then
A38: dom h1=dom h11 by RELAT_1:27;
then
A39: len h1=len h11 by FINSEQ_3:29;
then
A40: h0.2=h11.2 by A14,FINSEQ_1:64;
A41: h0.(1+1)=h11.(1+1) by A39,A14,FINSEQ_1:64;
then
A42: h0.(1+1)=g1.(h1.(1+1)) by A18,FUNCT_1:13;
set k=len h0-'len h11+2-'1;
0+2<=len h0-'len h11 +2 by XREAL_1:6;
then
A43: 2-'1<=len h0-'len h11 +2-'1 by NAT_D:42;
A44: 0 in dom g1 by Lm5,BORSUK_1:40,FUNCT_2:def 1;
A45: len h1 in dom h1 by A16,FINSEQ_3:25;
dom g2=the carrier of I[01] by FUNCT_2:def 1;
then
A46: dom h2=dom h21 by A29,RELAT_1:27;
then
A47: len h2=len h21 by FINSEQ_3:29;
then
A48: 2<=len h21 by A28,XXREAL_0:2;
len h21<=len h21 +1 by NAT_1:12;
then
A49: len h21 -1<=len h21 +1-1 by XREAL_1:9;
then
A50: len h21-'1<=len h21 by A28,A47,XREAL_0:def 2;
2<=len h21 by A28,A47,XXREAL_0:2;
then
A51: 1+1-1<=len h21-1 by XREAL_1:9;
then
A52: len h21-'1=len h21 -1 by XREAL_0:def 2;
3<len h21 by A28,A47,XXREAL_0:2;
then
A53: 2+1-1<len h21 -1 by XREAL_1:9;
then
A54: 2<len h21 -'1 by A51,NAT_D:39;
then
A55: len h21 -'1-'2=len h21 -'1-2 by XREAL_1:233;
A56: 1<=len h21-'1 by A51,XREAL_0:def 2;
then
A57: len (mid(h21,2,len h21 -'1)) =(len h21-'1)-'2+1 by A48,A50,A54,
FINSEQ_6:118;
3+2-2<=len h2 -2 by A28,XREAL_1:9;
then
A58: 5+3<=len h1+(len h2 -2) by A10,XREAL_1:7;
then
A59: len h0 > 1+1+1 by A39,A47,A36,A52,A55,A57,XXREAL_0:2;
then
A60: len h0-'1 > 1+1 by Lm2;
then
A61: 1<i by XXREAL_0:2;
A62: 3+2-2<=len h2 -2 by A28,XREAL_1:9;
then
A63: 1<=len h2 -2 by XXREAL_0:2;
then
A64: len h1+1<=len h0 by A39,A47,A36,A52,A55,A57,XREAL_1:7;
then
A65: len h0>len h1 by NAT_1:13;
then
A66: 1<len h0 by A16,XXREAL_0:2;
then
A67: 1 in dom h0 by FINSEQ_3:25;
then
A68: h0/.1 = h0.1 by PARTFUN1:def 6;
A69: dom g1=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
then
A70: 1 in dom (g1*h1) by A8,A17,Lm5,FUNCT_1:11;
then
A71: h11.1=W-min P by A6,A8,FUNCT_1:12;
hence
A72: h0.1=W-min P by A70,FINSEQ_1:def 7;
then
A73: h0/.1=W-min(P) by A67,PARTFUN1:def 6;
A74: len h0 in dom h0 by A66,FINSEQ_3:25;
then
A75: h0/.len h0=h0.len h0 by PARTFUN1:def 6;
A76: 1 in dom h2 by A33,FINSEQ_3:25;
then
A77: h21.1=E-max P by A24,A26,FUNCT_1:13;
thus
A78: h0 is one-to-one
proof
let x,y be object;
assume that
A79: x in dom h0 and
A80: y in dom h0 and
A81: h0.x=h0.y;
reconsider nx=x,ny=y as Nat by A79,A80;
A82: 1<=nx by A79,FINSEQ_3:25;
A83: nx<=len h0 by A79,FINSEQ_3:25;
A84: 1<=ny by A80,FINSEQ_3:25;
A85: ny<=len h0 by A80,FINSEQ_3:25;
per cases;
suppose
nx<=len h1;
then
A86: nx in dom h1 by A82,FINSEQ_3:25;
then
A87: h1.nx in rng h1 by FUNCT_1:def 3;
A88: h0.nx=h11.nx by A38,A86,FINSEQ_1:def 7
.=g1.(h1.nx) by A38,A86,FUNCT_1:12;
then
A89: h0.nx in Upper_Arc(P) by A5,A37,A87,FUNCT_1:def 3;
per cases;
suppose
ny<=len h1;
then
A90: ny in dom h1 by A84,FINSEQ_3:25;
then
A91: h1.ny in rng h1 by FUNCT_1:def 3;
h0.ny=h11.ny by A38,A90,FINSEQ_1:def 7
.=g1.(h1.ny) by A90,FUNCT_1:13;
then h1.nx=h1.ny by A4,A37,A81,A87,A88,A91;
hence thesis by A12,A86,A90,FUNCT_1:def 4;
end;
suppose
A92: ny>len h1;
A93: 0+2<=ny-'len h11 +2 by XREAL_1:6;
then
A94: 1<=(ny-'len h11 +2-'1) by Lm1,NAT_D:42;
len h1 +1<=ny by A92,NAT_1:13;
then
A95: len h1 +1-len h1<=ny-len h1 by XREAL_1:9;
then 1<=ny-'len h11 by A39,A92,XREAL_1:233;
then 1+1<=ny-'len h11+1+1-1 by XREAL_1:6;
then
A96: 2<=ny-'len h11+2-'1 by A93,Lm1,NAT_D:39,42;
A97: ny-len h11=ny-'len h11 by A39,A92,XREAL_1:233;
ny-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A85,
XREAL_1:9;
then
A98: ny-'len h11+2<=len h2-2+2 by A39,A97,XREAL_1:6;
then (ny-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A99: (ny-'len h11 +2-'1) in dom h21 by A94,FINSEQ_3:25;
ny-'len h11+2-1<=len h2-1 by A98,XREAL_1:9;
then
A100: ny-'len h11+2-'1<=len h2-1 by A93,Lm1,NAT_D:39,42;
A101: ny<=len h11 + len (mid(h21,2,len h21 -'1)) by A85,FINSEQ_1:22;
then
A102: ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by XREAL_1:9
;
len h11+1<=ny by A39,A92,NAT_1:13;
then
A103: h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) by A101,FINSEQ_1:23;
then
A104: h0.ny=h21.(ny-'len h11 +2-'1) by A39,A48,A56,A50,A54,A97,A102,A95,
FINSEQ_6:118;
then h0.ny in rng h21 by A99,FUNCT_1:def 3;
then h0.ny in rng g2 by FUNCT_1:14;
then h0.nx in Upper_Arc(P)/\ Lower_Arc(P) by A23,A81,A89,XBOOLE_0:def 4
;
then
A105: h0.nx in {W-min(P),E-max(P)} by A1,JORDAN6:50;
per cases by A105,TARSKI:def 2;
suppose
h0.nx=W-min(P);
then h21.(ny-'len h11 +2-'1)=W-min(P) by A39,A48,A56,A50,A54,A81,A103
,A97,A102,A95,FINSEQ_6:118;
then len h21=(ny-'len h11 +2-'1) by A46,A47,A34,A35,A32,A99;
then len h21+1<=len h21-1+1 by A47,A100,XREAL_1:6;
then len h21+1-len h21<=len h21 -len h21 by XREAL_1:9;
then len h21+1-len h21<=0;
hence thesis;
end;
suppose
h0.nx=E-max(P);
then 1=(ny-'len h11 +2-'1) by A46,A76,A77,A32,A81,A104,A99;
hence thesis by A96;
end;
end;
end;
suppose
A106: nx>len h1;
then len h1 +1<=nx by NAT_1:13;
then
A107: len h1 +1-len h1<=nx-len h1 by XREAL_1:9;
then 1<=nx-'len h11 by A39,A106,XREAL_1:233;
then
A108: 1+1<=nx-'len h11+1+1-1 by XREAL_1:6;
A109: nx<=len h11 + len (mid(h21,2,len h21 -'1)) by A83,FINSEQ_1:22;
then
A110: nx-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by XREAL_1:9;
A111: nx-len h11=nx-'len h11 by A39,A106,XREAL_1:233;
nx-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A83,
XREAL_1:9;
then
A112: nx-'len h11+2<=len h2-2+2 by A39,A111,XREAL_1:6;
then
A113: nx-'len h11+2-1<=len h2-1 by XREAL_1:9;
A114: (nx-'len h11 +2-'1)<=len h21 by A47,A112,NAT_D:44;
A115: 0+2<=nx-'len h11 +2 by XREAL_1:6;
then 1<=(nx-'len h11 +2-'1) by Lm1,NAT_D:42;
then
A116: (nx-'len h11 +2-'1) in dom h21 by A114,FINSEQ_3:25;
len h11+1<=nx by A39,A106,NAT_1:13;
then
A117: h0.nx=(mid(h21,2,len h21 -'1)).(nx -len h11) by A109,FINSEQ_1:23;
then
A118: h0.nx=h21.(nx-'len h11 +2-'1) by A39,A48,A56,A50,A54,A111,A110,A107,
FINSEQ_6:118;
then h0.nx in rng h21 by A116,FUNCT_1:def 3;
then
A119: h0.nx in Lower_Arc(P) by A23,FUNCT_1:14;
per cases;
suppose
ny<=len h1;
then
A120: ny in dom h1 by A84,FINSEQ_3:25;
then
A121: h1.ny in rng h1 by FUNCT_1:def 3;
h0.ny=h11.ny by A38,A120,FINSEQ_1:def 7
.=g1.(h1.ny) by A38,A120,FUNCT_1:12;
then h0.ny in rng g1 by A37,A121,FUNCT_1:def 3;
then h0.ny in Upper_Arc(P)/\ Lower_Arc(P) by A5,A81,A119,XBOOLE_0:def 4
;
then
A122: h0.ny in {W-min(P),E-max(P)} by A1,JORDAN6:50;
A123: nx-'len h11+2-'1<=len h2-1 by A115,A113,Lm1,NAT_D:39,42;
A124: 2<=nx-'len h11+2-'1 by A108,A115,Lm1,NAT_D:39,42;
per cases by A122,TARSKI:def 2;
suppose
h0.ny=W-min(P);
then len h21=(nx-'len h11 +2-'1) by A46,A47,A34,A35,A32,A81,A118,A116
;
then len h21+1<=len h21-1+1 by A47,A123,XREAL_1:6;
then len h21+1-len h21<=len h21 -len h21 by XREAL_1:9;
then len h21+1-len h21<=0;
hence thesis;
end;
suppose
h0.ny=E-max(P);
then h21.(nx-'len h11 +2-'1)=E-max(P) by A39,A48,A56,A50,A54,A81,A117
,A111,A110,A107,FINSEQ_6:118;
then 1=(nx-'len h11 +2-'1) by A46,A76,A77,A32,A116;
hence thesis by A124;
end;
end;
suppose
A125: ny>len h1;
then
A126: ny-len h11=ny-'len h11 by A39,XREAL_1:233;
len h1 +1<=ny by A125,NAT_1:13;
then
A127: h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) & len h1 +1-len h1
<=ny-len h1 by A39,A36,A85,FINSEQ_1:23,XREAL_1:9;
0+2<=ny-'len h11 +2 by XREAL_1:6;
then
A128: 1<=(ny-'len h11 +2-'1) by Lm1,NAT_D:42;
ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A85,
XREAL_1:9;
then
A129: h0.ny=h21.(ny-'len h11 +2-'1) by A39,A48,A56,A50,A54,A126,A127,
FINSEQ_6:118;
ny-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A85,
XREAL_1:9;
then ny-'len h11+2<=len h2-2+2 by A39,A126,XREAL_1:6;
then (ny-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then (ny-'len h11 +2-'1) in dom h21 by A128,FINSEQ_3:25;
then nx-'len h1+2-'1=ny-'len h1+2-'1 by A39,A32,A81,A118,A116,A129;
then nx-'len h1+2-1=ny-'len h1+2-'1 by A39,A115,Lm1,NAT_D:39,42;
then nx-'len h1+(2-1)=ny-'len h1+2-1 by A39,A128,NAT_D:39;
then len h1+nx-len h1=len h1+(ny-len h1) by A39,A111,A126,XCMPLX_1:29;
hence thesis;
end;
end;
end;
then
A130: h0/.len h0 <> W-min P by A16,A72,A65,A74,A75,A67;
A131: dom g2 = [.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
thus 8<=len h0 by A38,A47,A36,A52,A55,A57,A58,FINSEQ_3:29;
rng (mid(h21,2,len h21 -'1)) c= rng h21 & rng (g2*h2) c= rng g2 by
FINSEQ_6:119,RELAT_1:26;
then rng (g1*h1) c= rng g1 & rng (mid(h21,2,len h21 -'1)) c= rng g2 by
RELAT_1:26;
then rng h11 \/ rng (mid(h21,2,len h21 -'1)) c= Upper_Arc(P) \/ Lower_Arc(P
) by A5,A23,XBOOLE_1:13;
then rng h0 c=Upper_Arc(P) \/ Lower_Arc(P) by FINSEQ_1:31;
hence rng h0 c= P by A1,JORDAN6:def 9;
A132: dom g1 =[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
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 that
A133: 1<=i and
A134: i<len h0;
A135: i+1<=len h0 by A134,NAT_1:13;
A136: i<i+1 by NAT_1:13;
A137: 1<i+1 by A133,NAT_1:13;
per cases;
suppose
A138: i<len h1;
then
A139: i+1<=len h1 by NAT_1:13;
then
A140: i+1 in dom h1 by A137,FINSEQ_3:25;
then
A141: h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A142: h1.(i+1)<=1 by A11,BORSUK_1:40,XXREAL_1:1;
h0.(i+1)=h11.(i+1) by A39,A137,A139,FINSEQ_1:64;
then
A143: h0.(i+1)=g1.(h1.(i+1)) by A140,FUNCT_1:13;
then
A144: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A141,BORSUK_1:40,FUNCT_1:def 3;
i in dom h0 by A133,A134,FINSEQ_3:25;
then
A145: h0/.i=h0.i by PARTFUN1:def 6;
A146: i in dom h1 by A133,A138,FINSEQ_3:25;
then
A147: h1.i in rng h1 by FUNCT_1:def 3;
then
A148: 0<=h1.i & h1.i<=1 by A11,BORSUK_1:40,XXREAL_1:1;
A149: g1.(h1.i) in rng g1 by A132,A11,A147,BORSUK_1:40,FUNCT_1:def 3;
h0.i=h11.i by A39,A133,A138,FINSEQ_1:64;
then
A150: h0.i=g1.(h1.i) by A146,FUNCT_1:13;
i+1 in dom h0 by A135,A137,FINSEQ_3:25;
then
A151: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
h1.i<h1.(i+1) by A12,A136,A146,A140,SEQM_3:def 1;
then LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A150,A148,A143,A142,A145,A151,Th18;
hence thesis by A5,A150,A145,A151,A149,A144,JORDAN6:def 10;
end;
suppose
A152: i>=len h1;
per cases by A152,XXREAL_0:1;
suppose
A153: i>len h1;
then len h11+1<=i by A39,NAT_1:13;
then
A154: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A36,A134,FINSEQ_1:23;
A155: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A135
,XREAL_1:9;
i+1>len h11 by A39,A153,NAT_1:13;
then
A156: i+1-len h11=i+1-'len h11 by XREAL_1:233;
A157: len h1 +1<=i by A153,NAT_1:13;
then
A158: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
A159: i-len h11=i-'len h11 by A39,A153,XREAL_1:233;
A160: len h1 +1<=i+1 by A157,NAT_1:13;
then
A161: len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
then
A162: 1<i+1-'len h11+(2-1) by A39,A156,NAT_1:13;
then
A163: 0<i+1-'len h11+2-1;
h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A135,A160,
FINSEQ_1:23;
then
A164: h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A156,A155,A161
,FINSEQ_6:118;
set j=i-'len h11+2-'1;
len h2<len h2+1 by NAT_1:13;
then
A165: len h2-1<len h2+1-1 by XREAL_1:9;
A166: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A167: 1<=(i-'len h11 +2-'1) by Lm1,NAT_D:42;
then
A168: 1<j+1 by NAT_1:13;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A134,
XREAL_1:9;
then
A169: i-'len h11+2<=len h2-2+2 by A39,A159,XREAL_1:6;
then (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A170: j in dom h2 by A46,A167,FINSEQ_3:25;
i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A134,
XREAL_1:9;
then h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A154,A159,A158,
FINSEQ_6:118;
then
A171: h0.i=g2.(h2.j) by A170,FUNCT_1:13;
A172: h2.j in rng h2 by A170,FUNCT_1:def 3;
then
A173: h0.i in Lower_Arc(P) by A23,A131,A29,A171,BORSUK_1:40,FUNCT_1:def 3;
i+1 in dom h0 by A135,A137,FINSEQ_3:25;
then
A174: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
j+1=i-'len h11+1+1-1+1 by A166,Lm1,NAT_D:39,42
.=i-'len h11+2;
then
A175: j+1 in dom h2 by A169,A168,FINSEQ_3:25;
then
A176: h2.(j+1) in rng h2 by FUNCT_1:def 3;
then
A177: h2.(j+1)<=1 by A29,BORSUK_1:40,XXREAL_1:1;
A178: j+1=i-len h11+2-1+1 by A159,A166,Lm1,NAT_D:39,42
.=i+1-'len h11+2-'1 by A156,A163,XREAL_0:def 2;
then
A179: h0.(i+1)=g2.(h2.(j+1)) by A164,A175,FUNCT_1:13;
then
A180: h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A176,BORSUK_1:40,FUNCT_1:def 3
;
A181: i+1-'len h11+2-1=i+1-'len h11+2-'1 by A162,XREAL_0:def 2;
i+1-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A135,
XREAL_1:9;
then
A182: i+1-'len h11+2<=len h2-2+2 by A39,A156,XREAL_1:6;
then i+1-'len h11+2-1<=len h2-1 by XREAL_1:9;
then i+1-'len h11+2-'1<len h2 by A181,A165,XXREAL_0:2;
then
A183: i+1-'len h11+2-'1 in dom h2 by A178,A168,FINSEQ_3:25;
A184: now
assume h0/.(i+1)=W-min(P);
then len h21=(i+1-'len h11 +2-'1) by A46,A47,A34,A35,A32,A164,A174
,A183;
then len h21+1-len h21<=len h21 -len h21 by A47,A181,A182,XREAL_1:9;
then len h21+1-len h21<=0;
hence contradiction;
end;
j<j+1 by NAT_1:13;
then
A185: h2.j<h2.(j+1) by A30,A170,A175,SEQM_3:def 1;
i in dom h0 by A133,A134,FINSEQ_3:25;
then
A186: h0/.i=h0.i by PARTFUN1:def 6;
0<=h2.j & h2.j<=1 by A29,A172,BORSUK_1:40,XXREAL_1:1;
then LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A171,A179,A177,A185,A186,A174,Th18;
hence thesis by A186,A174,A173,A180,A184,JORDAN6:def 10;
end;
suppose
A187: i=len h1;
then h0.i=h11.i & i in dom h1 by A39,A133,FINSEQ_1:64,FINSEQ_3:25;
then
A188: h0.i=E-max(P) by A7,A9,A187,FUNCT_1:13;
i in dom h0 by A133,A134,FINSEQ_3:25;
then h0/.i=E-max(P) by A188,PARTFUN1:def 6;
then
A189: h0/.i in Upper_Arc(P) by A1,Th1;
i+1 in dom h0 by A135,A137,FINSEQ_3:25;
then
A190: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
set j=i-'len h11+2-'1;
len h11-'len h11= len h11-len h11 by XREAL_1:233
.=0;
then
A191: j=2-1 by A39,A187,XREAL_1:233;
then j+1<=len h2 by A28,XXREAL_0:2;
then
A192: j+1 in dom h2 by A191,FINSEQ_3:25;
then
A193: h2.(j+1) in rng h2 by FUNCT_1:def 3;
2<=len h21 by A28,A47,XXREAL_0:2;
then
A194: 2 in dom h21 by FINSEQ_3:25;
A195: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A135
,XREAL_1:9;
A196: i+1-'len h11+2-'1=1+2-'1 by A39,A187,NAT_D:34
.=2 by NAT_D:34;
h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) & i+1-len h11=i
+1-'len h11 by A39,A36,A135,A136,A187,FINSEQ_1:23,XREAL_1:233;
then
A197: h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A187,A195,
FINSEQ_6:118;
then h0.(i+1)=g2.(h2.(j+1)) by A191,A196,A192,FUNCT_1:13;
then
A198: h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A193,BORSUK_1:40,FUNCT_1:def 3
;
len h21 <> i+1-'len h11 +2-'1 by A28,A47,A196;
then h0/.(i+1) <> W-min P by A46,A47,A34,A35,A32,A197,A196,A190,A194;
hence thesis by A189,A190,A198,JORDAN6:def 10;
end;
end;
end;
A199: i<len h0 by A66,JORDAN5B:1;
then
A200: i+1<=len h0 by NAT_1:13;
A201: 1+1<=len h0 by A65,A14,XXREAL_0:2;
then
A202: 1<=i by Lm3;
then
A203: i in dom h0 by A199,FINSEQ_3:25;
then
A204: h0/.i=h0.i by PARTFUN1:def 6;
A205: 1+1<=len h0 by A66,NAT_1:13;
then 1+1 in dom h0 by FINSEQ_3:25;
then
A206: h0/.(1+1)=h0.(1+1) by PARTFUN1:def 6;
A207: now
A208: 1+1 in dom h1 by A14,FINSEQ_3:25;
then
A209: h1.(1+1) in rng h1 by FUNCT_1:def 3;
A210: h0.(1+1)=h11.(1+1) by A39,A14,FINSEQ_1:64;
then h0.(1+1)=g1.(h1.(1+1)) by A208,FUNCT_1:13;
then
A211: h0.(1+1) in Upper_Arc(P) by A5,A132,A11,A209,BORSUK_1:40,FUNCT_1:def 3;
assume
A212: h0/.(1+1)=h0/.i;
per cases;
suppose
i<=len h1;
then h0.i=h11.i & i in dom h1 by A39,A202,FINSEQ_1:64,FINSEQ_3:25;
hence contradiction by A38,A20,A60,A204,A206,A212,A208,A210;
end;
suppose
A213: i>len h1;
i in dom h0 by A202,A199,FINSEQ_3:25;
then
A214: h0/.i=h0.i by PARTFUN1:def 6;
A215: i-len h11=i-'len h11 by A39,A213,XREAL_1:233;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
then i-'len h11+2<=len h2-2+2 by A39,A215,XREAL_1:6;
then
A216: (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
then
A217: i-'len h11+2<=len h2-2+2 by A39,A215,XREAL_1:6;
set k=i-'len h11+2-'1;
A218: i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A199,
XREAL_1:9;
A219: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A220: i-'len h11+2-'1=i-'len h11+2-1 by Lm1,NAT_D:39,42;
1<=(i-'len h11 +2-'1) by A219,Lm1,NAT_D:42;
then
A221: k in dom h2 by A46,A216,FINSEQ_3:25;
then h2.k in rng h2 by FUNCT_1:def 3;
then
A222: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
A223: len h1 +1<=i by A213,NAT_1:13;
then h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) & len h1 +1-len h1<=i-
len h1 by A39,A36,A199,FINSEQ_1:23,XREAL_1:9;
then
A224: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A215,A218,FINSEQ_6:118
;
then h0.i=g2.(h2.k) by A221,FUNCT_1:13;
then h0.i in Upper_Arc(P) /\ Lower_Arc(P) by A23,A206,A212,A211,A214,A222
,XBOOLE_0:def 4;
then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then
A225: h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2;
len h11+1-len h11<=i-len h11 by A39,A223,XREAL_1:9;
then 1<=i-'len h11 by NAT_D:39;
then 1+2<=i-'len h11+2 by XREAL_1:6;
then 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
then
A226: 1<k by A220,XXREAL_0:2;
i-'len h11+2-'1<i-'len h11+2-1+1 by A220,NAT_1:13;
hence contradiction by A46,A76,A34,A77,A35,A32,A224,A217,A226,A221,A225;
end;
end;
A227: 1 in dom g2 by Lm6,BORSUK_1:40,FUNCT_2:def 1;
A228: len h2-1-1<len h2 by Lm4;
A229: now
per cases;
case
A230: i<=len h1;
A231: h0/.(1+1) in Upper_Arc(P) by A5,A132,A11,A206,A42,A19,BORSUK_1:40
,FUNCT_1:def 3;
A232: 0 <= h1.(1+1) & h1.(1+1) <= 1 by A11,A19,BORSUK_1:40,XXREAL_1:1;
A233: i in dom h1 by A61,A230,FINSEQ_3:25;
then
A234: h1.i in rng h1 by FUNCT_1:def 3;
then
A235: h1.i<=1 by A11,BORSUK_1:40,XXREAL_1:1;
h0.i=h11.i by A39,A61,A230,FINSEQ_1:64;
then
A236: h0.i=g1.(h1.i) by A233,FUNCT_1:13;
then
A237: h0/.i in Upper_Arc(P) by A5,A132,A11,A204,A234,BORSUK_1:40,FUNCT_1:def 3;
h1.(1+1)<h1.i by A12,A60,A18,A233,SEQM_3:def 1;
then LE h0/.(1+1),h0/.i,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A204,A206,A42,A236,A235,A232,Th18;
hence LE h0/.(1+1),h0/.i,P by A231,A237,JORDAN6:def 10;
end;
case
A238: i>len h1;
1+1 in dom h1 by A14,FINSEQ_3:25;
then
A239: h11.(1+1)=g1.(h1.(1+1)) by FUNCT_1:13;
A240: i-len h11=i-'len h11 by A39,A238,XREAL_1:233;
i+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A200,XREAL_1:9;
then i-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
then i-'len h11+2<=len h2-2-1+2 by A39,A240,XREAL_1:6;
then
A241: i-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
A242: len h1 +1<=i by A238,NAT_1:13;
then
A243: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
h1.(1+1) in rng h1 by A15,FUNCT_1:def 3;
then
A244: g1.(h1.(1+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
0+2<=i-'len h11 +2 by XREAL_1:6;
then
A245: 2-'1<=(i-'len h11 +2-'1) by NAT_D:42;
set k=i-'len h11+2-'1;
0+1<=i-'len h11+1+1-1 by XREAL_1:6;
then
A246: i-'len h11+2-'1=i-'len h11+2-1 by NAT_D:39;
A247: i-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A199,
XREAL_1:9;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
then i-'len h11+2<=len h2-2+2 by A39,A240,XREAL_1:6;
then i-'len h11 +2-'1<=len h21 by A47,NAT_D:44;
then
A248: (i-'len h11 +2-'1) in dom h21 by A245,Lm1,FINSEQ_3:25;
A249: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A39,A36,A199,A242,
FINSEQ_1:23;
then h0.(i)=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A240,A247,A243,
FINSEQ_6:118;
then
A250: h0.i=g2.(h2.k) by A46,A248,FUNCT_1:13;
h2.k in rng h2 by A46,A248,FUNCT_1:def 3;
then
A251: h0.i in Lower_Arc(P) by A23,A131,A29,A250,BORSUK_1:40,FUNCT_1:def 3;
1<=i-len h11 by A38,A243,FINSEQ_3:29;
then h0.i=h21.k by A48,A56,A50,A54,A240,A247,A249,FINSEQ_6:118;
then h0/.i <> W-min P by A228,A46,A34,A35,A32,A204,A246,A248,A241;
hence LE h0/.(1+1),h0/.i,P by A5,A204,A206,A41,A239,A244,A251,
JORDAN6:def 10;
end;
end;
A252: len h0-len h11=len h0-'len h11 by A39,A65,XREAL_1:233;
then (len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,NAT_D:44;
then (len h0-'len h11 +2-'1) in dom h21 by A43,Lm1,FINSEQ_3:25;
then
A253: h21.k=g2.(h2.k) & h2.k in rng h2 by A46,FUNCT_1:13,def 3;
h1.len h1 in dom g1 by A9,A69,XXREAL_1:1;
then
A254: len h1 in dom (g1*h1) by A45,FUNCT_1:11;
then
A255: h11.len h1=E-max(P) by A7,A9,FUNCT_1:12;
A256: 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
A257: 1<=i and
A258: i+1<=len h0;
A259: i<i+1 by NAT_1:13;
A260: 1<i+1 by A257,NAT_1:13;
then i+1 in dom h0 by A258,FINSEQ_3:25;
then
A261: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A262: i<len h0 by A258,NAT_1:13;
then i in dom h0 by A257,FINSEQ_3:25;
then
A263: h0/.i=h0.i by PARTFUN1:def 6;
per cases;
suppose
A264: i<len h1;
then
A265: i+1<=len h1 by NAT_1:13;
then
A266: i+1 in dom h1 by A260,FINSEQ_3:25;
then
A267: h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A268: (h1.(i+1)) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
A269: i+1 <> 1 & i+1 <> i by A257,NAT_1:13;
A270: i in dom h1 by A257,A264,FINSEQ_3:25;
then
A271: h1.i in rng h1 by FUNCT_1:def 3;
then
A272: 0 <= (h1.i) & (h1.i) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
A273: h0.(i+1)=h11.(i+1) by A39,A260,A265,FINSEQ_1:64;
then
A274: h0.(i+1)=g1.(h1.(i+1)) by A266,FUNCT_1:13;
then
A275: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A267,BORSUK_1:40,FUNCT_1:def 3;
A276: h0.i=h11.i by A39,A257,A264,FINSEQ_1:64;
then
A277: g1.(h1.i) = h0/.i by A263,A270,FUNCT_1:13;
g1.(h1.i) in rng g1 by A132,A11,A271,BORSUK_1:40,FUNCT_1:def 3;
then
A278: h0.i in Upper_Arc(P) by A5,A276,A270,FUNCT_1:13;
h1.i<h1.(i+1) by A12,A259,A270,A266,SEQM_3:def 1;
then LE h0/.i,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A261,A274,A277,A272,A268,Th18;
hence
thesis by A38,A17,A71,A20,A263,A261,A276,A270,A273,A266,A278,A275,A269,
JORDAN6:def 10;
end;
suppose
A279: i>=len h1;
per cases by A279,XXREAL_0:1;
suppose
A280: i>len h1;
i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A262,
XREAL_1:9;
then
A281: i-len h11+2<len h2-2+2 by XREAL_1:6;
i+1>len h11 by A39,A280,NAT_1:13;
then
A282: i+1-len h11=i+1-'len h11 by XREAL_1:233;
set j=i-'len h11+2-'1;
A283: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A258
,XREAL_1:9;
A284: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A285: j+1=i-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
.=i-'len h11+(1+1);
A286: len h1 +1<=i by A280,NAT_1:13;
then
A287: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
i+1 in dom h0 by A258,A260,FINSEQ_3:25;
then
A288: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A289: len h1 +1<=i+1 by A286,NAT_1:13;
then
A290: len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
then 1<i+1-'len h11+(2-1) by A39,A282,NAT_1:13;
then
A291: 0<i+1-'len h11+2-1;
h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A258,A289,
FINSEQ_1:23;
then
A292: h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A282,A283,A290
,FINSEQ_6:118;
A293: i<=len h11 + len (mid(h21,2,len h21 -'1)) by A262,FINSEQ_1:22;
len h11+1<=i by A39,A280,NAT_1:13;
then
A294: h0.i=(mid(h21, 2,len h21 -'1)).(i -len h11) by A293,FINSEQ_1:23;
A295: i-len h11=i-'len h11 by A39,A280,XREAL_1:233;
A296: 1<=i-'len h11 +2-'1 by A284,Lm1,NAT_D:42;
then 1<j+1 by NAT_1:13;
then
A297: j+1 in dom h2 by A295,A281,A285,FINSEQ_3:25;
then
A298: h2.(j+1) in rng h2 by FUNCT_1:def 3;
then
A299: (h2.(j+1)) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A262,
XREAL_1:9;
then i-'len h11+2<=len h2-2+2 by A39,A295,XREAL_1:6;
then i-'len h11 +2-'1<=len h21 by A47,NAT_D:44;
then
A300: j in dom h2 by A46,A296,FINSEQ_3:25;
j<j+1 by NAT_1:13;
then
A301: h2.j<h2.(j+1) by A30,A300,A297,SEQM_3:def 1;
i in dom h0 by A257,A262,FINSEQ_3:25;
then
A302: h0/.i=h0.i by PARTFUN1:def 6;
i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A293,
XREAL_1:9;
then
A303: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A294,A295,A287,
FINSEQ_6:118;
then
A304: h0.i=g2.(h2.j) by A300,FUNCT_1:13;
A305: j+1=i-len h11+2-1+1 by A295,A284,Lm1,NAT_D:39,42
.=i+1-'len h11+2-'1 by A282,A291,XREAL_0:def 2;
then
A306: h0/.(i+1) <> W-min P by A46,A34,A35,A32,A295,A292,A281,A285,A297,A288;
A307: h0.(i+1)=g2.(h2.(j+1)) by A292,A305,A297,FUNCT_1:13;
then
A308: h0/.(i+1) in Lower_Arc(P) by A23,A131,A29,A298,A288,BORSUK_1:40
,FUNCT_1:def 3;
A309: h2.j in rng h2 by A300,FUNCT_1:def 3;
then
A310: j < j+1 & h0/.i in Lower_Arc(P) by A23,A131,A29,A304,A302,BORSUK_1:40
,FUNCT_1:def 3,NAT_1:13;
0 <= (h2.j) & (h2.j) <= 1 by A29,A309,BORSUK_1:40,XXREAL_1:1;
then LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A304,A307,A301,A302,A288,A299,Th18;
hence thesis by A46,A32,A303,A292,A305,A300,A297,A302,A288,A306,A310
,A308,JORDAN6:def 10;
end;
suppose
A311: i=len h1;
then
A312: i-len h11=i-'len h11 by A39,XREAL_1:233;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A262,
XREAL_1:9;
then
A313: i-'len h11+2<=len h2-2+2 by A39,A312,XREAL_1:6;
then
A314: (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
set j=i-'len h11+2-'1;
A315: j+1 <> j;
A316: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A317: j+1=i-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
.=i-'len h11+2;
2-'1<=(i-'len h11 +2-'1) by A316,NAT_D:42;
then 1<j+1 by Lm1,NAT_1:13;
then
A318: j+1 in dom h2 by A313,A317,FINSEQ_3:25;
then
A319: h2.(j+1) in rng h2 by FUNCT_1:def 3;
i+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A258,FINSEQ_1:22;
then
A320: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by
XREAL_1:9;
A321: i+1-len h11=i+1-'len h11 by A39,A259,A311,XREAL_1:233;
then
A322: 0<i+1-'len h11+2-1 by A39,A311;
h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A258,A311,
FINSEQ_1:23;
then
A323: h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A311,A321,A320
,FINSEQ_6:118;
A324: h0.i=E-max(P) by A39,A255,A257,A311,FINSEQ_1:64;
then
A325: h0.i in Upper_Arc(P) by A1,Th1;
len h1-'len h11=len h11-len h11 by A39,XREAL_0:def 2;
then 0+2-1=len h1-'len h11+2-1;
then
A326: h0.i=g2.(h2.j) by A24,A26,A311,A324,NAT_D:39;
1<=(i-'len h11 +2-'1) by A316,Lm1,NAT_D:42;
then
A327: j in dom h2 by A46,A314,FINSEQ_3:25;
then
A328: h21.j=g2.(h2.j) by FUNCT_1:13;
i in dom h0 by A257,A262,FINSEQ_3:25;
then
A329: h0/.i=h0.i by PARTFUN1:def 6;
i+1 in dom h0 by A258,A260,FINSEQ_3:25;
then
A330: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A331: j+1=i-len h11+2-1+1 by A39,A311,Lm1,XREAL_0:def 2
.=i+1-'len h11+2-'1 by A321,A322,XREAL_0:def 2;
then h0.(i+1)=g2.(h2.(j+1)) by A323,A318,FUNCT_1:13;
then
A332: h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A319,BORSUK_1:40,FUNCT_1:def 3
;
i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A262,
XREAL_1:9;
then i-len h11+2<len h2-2+2 by XREAL_1:6;
then j+1<len h2 by A39,A311,A317,XREAL_0:def 2;
then h0/.(i+1) <> W-min P by A46,A34,A35,A32,A323,A331,A318,A330;
hence thesis by A46,A32,A323,A331,A327,A328,A326,A318,A329,A330,A332
,A325,A315,JORDAN6:def 10;
end;
end;
end;
then
A333: LE h0/.1,h0/.(1+1),P & h0/.1<>h0/.(1+1) by A205;
A334: E-max P in Upper_Arc P by A1,Th1;
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 that
A335: 1<=i and
A336: i<len h0 and
A337: W=Segment(h0/.i,h0/.(i+1),P);
A338: i+1<=len h0 by A336,NAT_1:13;
A339: i<i+1 by NAT_1:13;
A340: 1<i+1 by A335,NAT_1:13;
per cases by XXREAL_0:1;
suppose
A341: i<len h1;
then
A342: i in dom h1 by A335,FINSEQ_3:25;
then
A343: h1.i in rng h1 by FUNCT_1:def 3;
then
A344: h1.i<=1 by A11,BORSUK_1:40,XXREAL_1:1;
A345: 0<=h1.i by A11,A343,BORSUK_1:40,XXREAL_1:1;
A346: h1/.i=h1.i by A335,A341,FINSEQ_4:15;
A347: h11.i=g1.(h1.i) by A342,FUNCT_1:13;
then
A348: h0.i=g1.(h1.i) by A39,A335,A341,FINSEQ_1:64;
then
A349: h0.i in Upper_Arc(P) by A5,A132,A11,A343,BORSUK_1:40,FUNCT_1:def 3;
i in dom h0 by A335,A336,FINSEQ_3:25;
then
A350: h0/.i=h0.i by PARTFUN1:def 6;
i+1 in dom h0 by A338,A340,FINSEQ_3:25;
then
A351: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A352: i+1<=len h1 by A341,NAT_1:13;
then
A353: i+1 in dom h1 by A340,FINSEQ_3:25;
then
A354: h1.i<h1.(i+1) by A12,A339,A342,SEQM_3:def 1;
A355: h1/.(i+1)=h1.(i+1) by A340,A352,FINSEQ_4:15;
A356: h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
then reconsider Q1=[.h1/.i,h1/.(i+1).] as Subset of I[01] by A11,A343
,A346,A355,BORSUK_1:40,XXREAL_2:def 12;
A357: h0.i=h11.i by A39,A335,A341,FINSEQ_1:64;
A358: h0.(i+1)=h11.(i+1) by A39,A340,A352,FINSEQ_1:64;
then
A359: h0.(i+1)=g1.(h1.(i+1)) by A353,FUNCT_1:13;
then
A360: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A356,BORSUK_1:40,FUNCT_1:def 3;
A361: Segment(h0/.i,h0/.(i+1),P) c= g1.:([.h1/.i,h1/.(i+1).])
proof
let x be object;
A362: h0/.(i+1) <> W-min P by A38,A17,A71,A20,A340,A358,A353,A351;
assume x in Segment(h0/.i,h0/.(i+1),P);
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A362,Def1;
then consider p being Point of TOP-REAL 2 such that
A363: p=x and
A364: LE h0/.i,p,P and
A365: LE p,h0/.(i+1),P;
A366: 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 A364,JORDAN6:def 10;
A367: 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 A365,JORDAN6:def 10;
now
per cases by A352,XXREAL_0:1;
suppose
i+1<len h1;
then
A368: h0/.(i+1) <> E-max P by A38,A45,A255,A20,A358,A353,A351;
A369: now
assume h0/.(i+1) in Lower_Arc(P);
then
h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A351,A360,XBOOLE_0:def 4;
then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A362,A368,TARSKI:def 2;
end;
then
A370: LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A365,
JORDAN6:def 10;
then
A371: p<>E-max(P) by A3,A368,JORDAN6:55;
A372: p in Upper_Arc(P) by A365,A369,JORDAN6:def 10;
per cases by A335,XXREAL_0:1;
suppose
i>1;
then
A373: h0/.i <> W-min P by A38,A17,A71,A20,A342,A347,A348,A350;
A374: h11.i <> E-max(P) by A38,A45,A255,A20,A341,A342;
now
assume h0/.i in Lower_Arc(P);
then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A350,A349,
XBOOLE_0:def 4;
then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A357,A350,A373,A374,TARSKI:def 2;
end;
then
A375: 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 A364,JORDAN6:def 10;
then
A376: p <> W-min P by A3,A373,JORDAN6:54;
A377: now
assume p in Lower_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A372,XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A371,A376,TARSKI:def 2;
end;
then consider z being object such that
A378: z in dom g1 and
A379: p=g1.z by A5,A375,FUNCT_1:def 3;
reconsider rz=z as Real by A132,A378;
A380: rz<=1 by A378,BORSUK_1:40,XXREAL_1:1;
h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
then
A381: 0<=h1/.(i+1) & h1/.(i+1)<=1 by A11,A355,BORSUK_1:40,XXREAL_1:1;
reconsider z as set by TARSKI:1;
take z;
thus z in dom g1 by A378;
A382: g1.(h1/.i)=h0/.i & h1/.i<=1 by A335,A341,A357,A347,A344,A350,
FINSEQ_4:15;
g1.(h1/.(i+1))=h0/.(i+1) by A340,A352,A359,A351,FINSEQ_4:15;
then
A383: rz<=h1/.(i+1) by A4,A5,A6,A7,A370,A379,A381,A380,Th19;
0<=rz by A378,BORSUK_1:40,XXREAL_1:1;
then h1/.i<=rz by A4,A5,A6,A7,A375,A377,A379,A382,A380,Th19;
hence z in [.h1/.i,h1/.(i+1).] by A383,XXREAL_1:1;
thus x = g1.z by A363,A379;
end;
suppose
A384: i=1;
now
per cases;
case
A385: p<>W-min(P);
now
assume p in Lower_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A372,
XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A371,A385,TARSKI:def 2;
end;
then consider z being object such that
A386: z in dom g1 and
A387: p=g1.z by A5,A366,FUNCT_1:def 3;
reconsider rz=z as Real by A132,A386;
A388: h1/.1<=rz by A8,A346,A384,A386,BORSUK_1:40,XXREAL_1:1;
h1.(1+1) in rng h1 by A353,A384,FUNCT_1:def 3;
then
A389: 0<=h1/.(1+1) & h1/.(1+1)<=1 by A11,A355,A384,BORSUK_1:40
,XXREAL_1:1;
A390: g1.(h1/.(1+1))=h0/.(1+1) by A352,A359,A351,A384,FINSEQ_4:15;
take rz;
rz<=1 by A386,BORSUK_1:40,XXREAL_1:1;
then rz<=h1/.(1+1) by A4,A5,A6,A7,A370,A384,A387,A390,A389
,Th19;
hence
rz in dom g1 & rz in [.h1/.1,h1/.(1+1).] & x = g1.rz by A363
,A386,A387,A388,XXREAL_1:1;
end;
case
A391: p=W-min(P);
thus 0 in [.h1/.1,h1/.(1+1).] by A8,A354,A346,A355,A384,
XXREAL_1:1;
thus x = g1.0 by A6,A363,A391;
end;
end;
hence ex y being set
st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
x = g1.y by A44,A384;
end;
end;
suppose
A392: i+1=len h1;
then
A393: h0/.(i+1)=E-max(P) by A7,A9,A45,A358,A351,FUNCT_1:13;
A394: now
assume that
A395: p in Lower_Arc(P) and
A396: not p in Upper_Arc(P);
LE h0/.(i+1),p,Lower_Arc(P),E-max(P),W-min(P) by A21,A393,A395,
JORDAN5C:10;
hence contradiction by A334,A21,A367,A393,A396,JORDAN5C:12;
end;
p in Upper_Arc(P) or p in Lower_Arc(P) by A364,JORDAN6:def 10;
then
A397: LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A393,A394,
JORDAN5C:10;
per cases;
suppose
A398: p<>E-max(P);
now
per cases;
case
A399: p<>W-min(P);
A400: now
assume p in Lower_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A394,
XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A398,A399,TARSKI:def 2;
end;
then consider z being object such that
A401: z in dom g1 and
A402: p=g1.z by A5,A366,FUNCT_1:def 3;
reconsider rz=z as Real by A132,A401;
A403: rz<=1 by A401,BORSUK_1:40,XXREAL_1:1;
h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
then
A404: 0<=h1/.(i+1) & h1/.(i+1)<=1 by A11,A355,BORSUK_1:40
,XXREAL_1:1;
g1.(h1/.(i+1))=h0/.(i+1) by A340,A352,A359,A351,FINSEQ_4:15;
then
A405: rz<=h1/.(i+1) by A4,A5,A6,A7,A397,A402,A404,A403,Th19;
take rz;
0<=rz by A401,BORSUK_1:40,XXREAL_1:1;
then h1/.i<=rz by A4,A5,A6,A7,A357,A347,A344,A350,A346,A366
,A400,A402,A403,Th19;
hence
rz in dom g1 & rz in [.h1/.i,h1/.(i+1).] & x = g1.rz by A363
,A401,A402,A405,XXREAL_1:1;
end;
case
A406: p=W-min(P);
then h11.i=W-min(P) by A3,A357,A350,A366,JORDAN6:54;
then i=1 by A38,A17,A71,A20,A342;
then 0 in [.h1/.i,h1/.(i+1).] by A8,A354,A346,A355,XXREAL_1:1
;
hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1)
.] & x = g1.y by A6,A44,A363,A406;
end;
end;
hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
x = g1.y;
end;
suppose
A407: p=E-max(P);
1 in [.h1/.i,h1/.(i+1).] by A9,A354,A346,A355,A392,XXREAL_1:1;
hence ex y being set
st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
x = g1.y by A7,A69,A363,A407,Lm6;
end;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
A408: h1.(i+1)<=1 by A11,A356,BORSUK_1:40,XXREAL_1:1;
g1.:([.h1/.i,h1/.(i+1).]) c= Segment(h0/.i,h0/.(i+1),P)
proof
A409: g1.(h1/.i)=h0/.i & 0<=h1/.i by A335,A341,A348,A345,A350,FINSEQ_4:15;
let x be object;
assume x in g1.:([.h1/.i,h1/.(i+1).]);
then consider y being object such that
A410: y in dom g1 and
A411: y in [.h1/.i,h1/.(i+1).] and
A412: x=g1.y by FUNCT_1:def 6;
reconsider sy=y as Real by A411;
A413: sy<=1 by A410,BORSUK_1:40,XXREAL_1:1;
A414: x in Upper_Arc(P) by A5,A410,A412,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
A415: h1/.i<=1 by A335,A341,A344,FINSEQ_4:15;
h1/.i<=sy by A411,XXREAL_1:1;
then LE h0/.i,p1,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7,A412
,A409,A415,A413,Th18;
then
A416: LE h0/.i,p1,P by A350,A349,A414,JORDAN6:def 10;
sy<=h1/.(i+1) & 0<=sy by A410,A411,BORSUK_1:40,XXREAL_1:1;
then LE p1,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A359,A408,A351,A355,A412,A413,Th18;
then LE p1,h0/.(i+1),P by A351,A360,A414,JORDAN6:def 10;
then
A417: x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A416;
not h0/.(i+1)=W-min P by A38,A17,A71,A20,A340,A358,A353,A351;
hence thesis by A417,Def1;
end;
then W=g1.:Q1 by A337,A361;
hence thesis by A13,A335,A341;
end;
suppose
A418: i>len h1;
i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A336,
XREAL_1:9;
then
A419: i-len h11+2<len h2-2+2 by XREAL_1:6;
A420: len h1 +1<=i by A418,NAT_1:13;
then
A421: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
A422: i-len h11=i-'len h11 by A39,A418,XREAL_1:233;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A336,
XREAL_1:9;
then
A423: i-'len h11+2<=len h2-2+2 by A39,A422,XREAL_1:6;
i+1>len h11 by A39,A418,NAT_1:13;
then
A424: i+1-len h11=i+1-'len h11 by XREAL_1:233;
i+1 in dom h0 by A338,A340,FINSEQ_3:25;
then
A425: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A426: i<=len h11 + len (mid(h21,2,len h21 -'1)) by A336,FINSEQ_1:22;
len h11+1<=i by A39,A418,NAT_1:13;
then
A427: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A426,FINSEQ_1:23;
A428: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A338,
XREAL_1:9;
i in dom h0 by A335,A336,FINSEQ_3:25;
then
A429: h0/.i=h0.i by PARTFUN1:def 6;
set j=i-'len h11+2-'1;
len h2<len h2+1 by NAT_1:13;
then
A430: len h2-1<len h2+1-1 by XREAL_1:9;
A431: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A432: j+1=i-'len h11+1+1-1+1 by Lm1,NAT_D:39,42
.=i-'len h11+(1+1);
A433: 1<=(i-'len h11 +2-'1) by A431,Lm1,NAT_D:42;
then
A434: 1<j+1 by NAT_1:13;
then
A435: j+1 in dom h2 by A423,A432,FINSEQ_3:25;
then
A436: h2.(j+1) in rng h2 by FUNCT_1:def 3;
then
A437: h2.(j+1) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
A438: h2/.(j+1)=h2.(j+1) by A423,A432,A434,FINSEQ_4:15;
(i-'len h11 +2-'1)<=len h21 by A47,A423,NAT_D:44;
then
A439: j in dom h2 by A46,A433,FINSEQ_3:25;
i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A336,
XREAL_1:9;
then
A440: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A427,A422,A421,
FINSEQ_6:118;
then
A441: h0.i=g2.(h2.j) by A439,FUNCT_1:13;
A442: h2.j in rng h2 by A439,FUNCT_1:def 3;
then g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
then
A443: h0.i in Lower_Arc(P) by A23,A440,A439,FUNCT_1:13;
i-'len h11+2-1<=len h2-1 by A423,XREAL_1:9;
then i-'len h11+2-1<len h2 by A430,XXREAL_0:2;
then
A444: j< len h2 by A431,Lm1,NAT_D:39,42;
then
A445: h2/.j=h2.j by A431,Lm1,FINSEQ_4:15,NAT_D:42;
then reconsider
Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A29,A442,A436,A438,
BORSUK_1:40,XXREAL_2:def 12;
A446: 0 <= h2.j & h2.j <= 1 by A29,A442,BORSUK_1:40,XXREAL_1:1;
A447: i-'len h11+2-'1=i-'len h11+2-1 by A431,Lm1,NAT_D:39,42;
A448: len h1 +1<=i+1 by A420,NAT_1:13;
then
A449: len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
then 1<i+1-'len h11+(2-1) by A39,A424,NAT_1:13;
then 0<i+1-'len h11+2-1;
then
A450: j+1 =i+1-'len h11+2-'1 by A422,A424,A447,XREAL_0:def 2;
h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A338,A448,
FINSEQ_1:23;
then
A451: h0.(i+1)=h21.(i+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A424,A428,A449,
FINSEQ_6:118;
then h0.(i+1)=g2.(h2.(j+1)) by A450,A435,FUNCT_1:13;
then
A452: h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A436,BORSUK_1:40,FUNCT_1:def 3;
len h1 +1<=i by A418,NAT_1:13;
then len h11+1-len h11<=i-len h11 by A39,XREAL_1:9;
then 1<=i-'len h11 by NAT_D:39;
then 1+2<=i-'len h11+2 by XREAL_1:6;
then 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
then
A453: 1<j by A447,XXREAL_0:2;
A454: Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).])
proof
h2.(j+1) in rng h2 by A435,FUNCT_1:def 3;
then
A455: 0<=h2/.(j+1) & h2/.(j+1)<=1 by A29,A438,BORSUK_1:40,XXREAL_1:1;
A456: g2.(h2/.(j+1))=h0/.(i+1) by A451,A450,A435,A425,A438,FUNCT_1:13;
j<len h2 by A423,A432,NAT_1:13;
then
A457: h0/.i <> W-min(P) by A46,A34,A35,A32,A440,A439,A429;
A458: h2/.j<=1 by A29,A442,A445,BORSUK_1:40,XXREAL_1:1;
let x be object;
assume
A459: x in Segment(h0/.i,h0/.(i+1),P);
h0/.(i+1) <> W-min P by A46,A34,A35,A32,A422,A451,A419,A432,A450,A435
,A425;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A459,Def1;
then consider p being Point of TOP-REAL 2 such that
A460: p=x and
A461: LE h0/.i,p,P and
A462: LE p,h0/.(i+1),P;
A463: 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 A461,JORDAN6:def 10;
A464: h21.j <> E-max P by A46,A76,A77,A32,A453,A439;
A465: now
assume h0/.i in Upper_Arc(P);
then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A429,A443,XBOOLE_0:def 4
;
then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A440,A429,A457,A464,TARSKI:def 2;
end;
then
A466: LE h0/.i,p,Lower_Arc P, E-max P, W-min P by A461,JORDAN6:def 10;
A467: h0/.i <> E-max(P) by A46,A76,A77,A32,A440,A453,A439,A429;
A468: now
assume p in Upper_Arc(P);
then p in Upper_Arc P /\ Lower_Arc P by A463,A465,XBOOLE_0:def 4;
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 A21,A463,A465,A467,JORDAN6:54;
end;
A469: h0/.(i+1) <> E-max P & h21.(j+1) <> W-min P by A46,A76,A34,A77,A35,A32
,A422,A451,A419,A432,A450,A434,A435,A425;
now
assume h0/.(i+1) in Upper_Arc(P);
then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A425,A452,
XBOOLE_0:def 4;
then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A451,A450,A425,A469,TARSKI:def 2;
end;
then 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 A462,JORDAN6:def 10;
then consider z being object such that
A470: z in dom g2 and
A471: p=g2.z by A23,A468,FUNCT_1:def 3;
reconsider rz=z as Real by A131,A470;
A472: rz<=1 by A470,BORSUK_1:40,XXREAL_1:1;
LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A462,A468,
JORDAN6:def 10;
then
A473: rz<=h2/.(j+1) by A22,A23,A24,A25,A471,A456,A472,A455,Th19;
0<=rz by A470,BORSUK_1:40,XXREAL_1:1;
then h2/.j<=rz by A22,A23,A24,A25,A441,A429,A445,A466,A471,A458,A472
,Th19;
then rz in [.h2/.j,h2/.(j+1).] by A473,XXREAL_1:1;
hence thesis by A460,A470,A471,FUNCT_1:def 6;
end;
A474: g2.(h2.(j+1)) = h0/.(i+1) by A451,A450,A435,A425,FUNCT_1:13;
g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
proof
let x be object;
assume x in g2.:([.h2/.j,h2/.(j+1).]);
then consider y being object such that
A475: y in dom g2 and
A476: y in [.h2/.j,h2/.(j+1).] and
A477: x=g2.y by FUNCT_1:def 6;
reconsider sy=y as Real by A476;
A478: sy<=h2/.(j+1) by A476,XXREAL_1:1;
A479: x in Lower_Arc(P) by A23,A475,A477,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
A480: h2.(j+1) <> 1 by A27,A30,A34,A422,A419,A432,A435,FUNCT_1:def 4;
A481: now
assume p1=W-min(P);
then 1=sy by A22,A25,A227,A475,A477;
hence contradiction by A437,A438,A478,A480,XXREAL_0:1;
end;
A482: sy<=1 by A475,BORSUK_1:40,XXREAL_1:1;
h2/.j<=sy by A476,XXREAL_1:1;
then LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A441,A429,A446,A445,A477,A482,Th18;
then
A483: LE h0/.i,p1,P by A429,A443,A479,A481,JORDAN6:def 10;
A484: h0/.(i+1) <> W-min P by A46,A34,A35,A32,A422,A451,A419,A432,A450,A435
,A425;
0<=sy by A475,BORSUK_1:40,XXREAL_1:1;
then LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24
,A25,A474,A437,A438,A477,A478,A482,Th18;
then LE p1,h0/.(i+1),P by A425,A452,A479,A484,JORDAN6:def 10;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A483;
hence thesis by A484,Def1;
end;
then W=g2.:(Q1) by A337,A454;
hence thesis by A31,A433,A444;
end;
suppose
A485: i=len h1;
A486: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A338,
XREAL_1:9;
then 1<=i+1-'len h11 by A39,A339,A485,XREAL_1:233;
then 1<i+1-'len h11+(2-1) by NAT_1:13;
then
A487: 0<i+1-'len h11+2-1;
i in dom h0 by A335,A336,FINSEQ_3:25;
then
A488: h0/.i=h0.i by PARTFUN1:def 6;
A489: h0.i=E-max(P) by A39,A255,A335,A485,FINSEQ_1:64;
set j=i-'len h11+2-'1;
A490: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A491: j+1=i-'len h11+1+1-1+1 by Lm1,NAT_D:39,42
.=i-'len h11+(1+1);
A492: len h1-'len h11=len h11-len h11 by A39,XREAL_0:def 2;
then
A493: 0+2-1=len h1-'len h11+2-1;
then
A494: h0.i=g2.(h2.j) by A24,A26,A485,A489,NAT_D:39;
A495: i-len h11=i-'len h11 by A39,A485,XREAL_1:233;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A336,
XREAL_1:9;
then
A496: i-'len h11+2<=len h2-2+2 by A39,A495,XREAL_1:6;
i-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A336,
XREAL_1:9;
then
A497: i-len h11+2<len h2-2+2 by XREAL_1:6;
then
A498: j+1<len h2 by A39,A485,A491,XREAL_0:def 2;
A499: h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A39,A36,A338,A485,
FINSEQ_1:23;
len h2<len h2+1 by NAT_1:13;
then
A500: len h2-1<len h2+1-1 by XREAL_1:9;
i+1 in dom h0 by A338,A340,FINSEQ_3:25;
then
A501: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A502: 1<=(i-'len h11 +2-'1) by A490,Lm1,NAT_D:42;
then
A503: 1<j+1 by NAT_1:13;
then
A504: j+1 in dom h2 by A496,A491,FINSEQ_3:25;
then
A505: h2.(j+1) in rng h2 by FUNCT_1:def 3;
then
A506: h2.(j+1) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
(i-'len h11 +2-'1)<=len h21 by A47,A496,NAT_D:44;
then
A507: j in dom h2 by A46,A502,FINSEQ_3:25;
then
A508: h2.j in rng h2 by FUNCT_1:def 3;
then g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
then
A509: h0.i in Lower_Arc P by A23,A24,A26,A485,A489,A493,NAT_D:39;
A510: h2/.(j+1)=h2.(j+1) by A496,A491,A503,FINSEQ_4:15;
i-'len h11+2-1<=len h2-1 by A496,XREAL_1:9;
then
A511: i-'len h11+2-1<len h2 by A500,XXREAL_0:2;
then
A512: j<len h2 by A490,Lm1,NAT_D:39,42;
then h2/.j=h2.j by A490,Lm1,FINSEQ_4:15,NAT_D:42;
then reconsider
Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A29,A508,A505,A510,
BORSUK_1:40,XXREAL_2:def 12;
A513: i+1-len h11=i+1-'len h11 by A39,A339,A485,XREAL_1:233;
j+1=i-len h11+2-1+1 by A39,A485,Lm1,XREAL_0:def 2
.=i+1-'len h11+2-'1 by A513,A487,XREAL_0:def 2;
then
A514: h0
.(i+1)=h21.(j+1) by A39,A48,A56,A50,A54,A485,A499,A513,A486,FINSEQ_6:118;
then
A515: h0.(i+1)=g2.(h2.(j+1)) by A504,FUNCT_1:13;
then
A516: h0.(i+1) in Lower_Arc P by A23,A131,A29,A505,BORSUK_1:40,FUNCT_1:def 3;
A517: h21.j=g2.(h2.j) by A507,FUNCT_1:13;
A518: Segment(h0/.i,h0/.(i+1),P) c= g2.:([.h2/.j,h2/.(j+1).])
proof
j+1<len h2 by A39,A485,A497,A491,XREAL_0:def 2;
then j<len h2 by NAT_1:13;
then
A519: h0/.i<>W-min(P) by A46,A34,A35,A32,A507,A517,A494,A488;
A520: g2.(h2/.(j+1))=h0/.(i+1) by A496,A491,A503,A515,A501,FINSEQ_4:15;
h2.(j+1) in rng h2 by A504,FUNCT_1:def 3;
then
A521: 0<=h2/.(j+1) & h2/.(j+1)<=1 by A29,A510,BORSUK_1:40,XXREAL_1:1;
A522: h0/.(i+1) in Lower_Arc(P) by A23,A131,A29,A515,A505,A501,BORSUK_1:40
,FUNCT_1:def 3;
let x be object;
assume
A523: x in Segment(h0/.i,h0/.(i+1),P);
h0/.(i+1) <> W-min P by A46,A34,A35,A32,A498,A514,A504,A501;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A523,Def1;
then consider p being Point of TOP-REAL 2 such that
A524: p=x and
A525: LE h0/.i,p,P and
A526: LE p,h0/.(i+1),P;
A527: 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 A525,JORDAN6:def 10;
dom (g1*h1) c= dom h0 by FINSEQ_1:26;
then
A528: h0/.i=E-max(P) by A254,A485,A489,PARTFUN1:def 6;
A529: now
assume
A530: not p in Lower_Arc(P);
then p=E-max(P) by A3,A527,A528,JORDAN6:55;
hence contradiction by A1,A530,Th1;
end;
A531: now
assume p in Upper_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A529,XBOOLE_0:def 4;
then
A532: p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
p <> W-min P by A3,A527,A519,JORDAN6:54;
hence p = E-max P by A532,TARSKI:def 2;
end;
then p in rng g2 by A1,A23,A525,Th1,JORDAN6:def 10;
then consider z being object such that
A533: z in dom g2 and
A534: p=g2.z by FUNCT_1:def 3;
reconsider rz=z as Real by A131,A533;
0<=rz by A533,BORSUK_1:40,XXREAL_1:1;
then
A535: h2/.j<=rz by A26,A485,A511,A492,Lm1,FINSEQ_4:15;
A536: not h0/.(i+1)=E-max(P) by A46,A76,A77,A32,A503,A514,A504,A501;
now
assume h0/.(i+1) in Upper_Arc(P);
then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A522,XBOOLE_0:def 4;
then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then h21.(j+1)=W-min(P) by A514,A501,A536,TARSKI:def 2;
hence contradiction by A46,A34,A35,A32,A498,A504;
end;
then 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 A526,JORDAN6:def 10;
then
A537: LE p,h0/.(i+1),Lower_Arc P, E-max P, W-min P by A21,A531,JORDAN5C:10;
rz<=1 by A533,BORSUK_1:40,XXREAL_1:1;
then rz<=h2/.(j+1) by A22,A23,A24,A25,A537,A534,A520,A521,Th19;
then rz in [.h2/.j,h2/.(j+1).] by A535,XXREAL_1:1;
hence thesis by A524,A533,A534,FUNCT_1:def 6;
end;
A538: g2.(h2.(j+1)) = h0/.(i+1) by A514,A504,A501,FUNCT_1:13;
g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
proof
let x be object;
assume x in g2.:([.h2/.j,h2/.(j+1).]);
then consider y being object such that
A539: y in dom g2 and
A540: y in [.h2/.j,h2/.(j+1).] and
A541: x=g2.y by FUNCT_1:def 6;
reconsider sy=y as Real by A540;
A542: sy<=h2/.(j+1) by A540,XXREAL_1:1;
A543: x in Lower_Arc(P) by A23,A539,A541,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
A544: h2.(j+1) <> 1 by A27,A30,A34,A498,A504,FUNCT_1:def 4;
A545: now
assume p1=W-min(P);
then 1=sy by A22,A25,A227,A539,A541;
hence contradiction by A506,A510,A542,A544,XXREAL_0:1;
end;
A546: 0<=sy & sy<=1 by A539,BORSUK_1:40,XXREAL_1:1;
then LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A489,A488,A541,Th18;
then
A547: LE h0/.i,p1,P by A488,A509,A543,A545,JORDAN6:def 10;
A548: h0/.(i+1) <> W-min(P) by A46,A34,A35,A32,A498,A514,A504,A501;
LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A538,A506,A510,A541,A542,A546,Th18;
then LE p1,h0/.(i+1),P by A501,A516,A543,A548,JORDAN6:def 10;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A547;
hence thesis by A548,Def1;
end;
then W=g2.:(Q1) by A337,A518;
hence thesis by A31,A502,A512;
end;
end;
A549: len h0=len h1+(len h2-2) by A38,A47,A36,A52,A55,A57,FINSEQ_3:29;
thus for W being Subset of Euclid 2 st W=Segment(h0/.len h0,h0/.1,P) holds
diameter W < e
proof
set i=len h0;
let W be Subset of Euclid 2;
set j=i-'len h11+2-'1;
A550: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A551: 1<=(i-'len h11 +2-'1) by Lm1,NAT_D:42;
len h11+1-len h11<=i-len h11 by A47,A36,A52,A55,A57,A62,XXREAL_0:2;
then 1<=i-'len h11 by NAT_D:39;
then 1+2<=i-'len h11+2 by XREAL_1:6;
then
A552: 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
len h0<=len h11 + len mid(h21,2,len h21 -'1) by FINSEQ_1:22;
then
A553: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A39,A64,FINSEQ_1:23;
A554: i-len h11=i-'len h11 by A39,A65,XREAL_1:233;
then (i-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,NAT_D:44;
then
A555: j in dom h2 by A46,A551,FINSEQ_3:25;
then
A556: h2.j in rng h2 by FUNCT_1:def 3;
i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 & len h1 +
1-len h1 <=i-len h1 by A549,A62,FINSEQ_1:22,XXREAL_0:2;
then
A557: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A553,A554,FINSEQ_6:118
;
then
A558: h0.i=g2.(h2.j) by A555,FUNCT_1:13;
then
A559: h0.i in Lower_Arc P by A23,A131,A29,A556,BORSUK_1:40,FUNCT_1:def 3;
A560: 2-'1<=(i-'len h11 +2-'1) by A550,NAT_D:42;
then
A561: 1<j+1 by Lm1,NAT_1:13;
then
A562: h2/.(j+1)=h2.(j+1) by A47,A36,A52,A55,A57,A554,FINSEQ_4:15;
len h2<len h2+1 by NAT_1:13;
then
A563: len h2-1<len h2+1-1 by XREAL_1:9;
then
A564: h2/.j=h2.j by A47,A36,A52,A55,A57,A554,A560,Lm1,FINSEQ_4:15;
j+1 in dom h2 by A46,A36,A52,A55,A57,A554,A561,FINSEQ_3:25;
then h2.(j+1) in rng h2 by FUNCT_1:def 3;
then reconsider Q1=[.h2/.j,h2/.(j+1).] as Subset of I[01] by A29,A556,A564
,A562,BORSUK_1:40,XXREAL_2:def 12;
i in dom h0 by A66,FINSEQ_3:25;
then
A565: h0/.i=h0.i by PARTFUN1:def 6;
i-'len h11+2-'1=i-'len h11+2-1 by A550,Lm1,NAT_D:39,42;
then
A566: 1<j by A552,XXREAL_0:2;
A567: now
assume h0.i in Upper_Arc(P);
then h0.i in Upper_Arc(P)/\ Lower_Arc(P) by A559,XBOOLE_0:def 4;
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 A46,A47,A76,A34,A77,A35,A36,A52,A55,A57,A32,A554
,A557,A563,A566,A555;
end;
A568: h2.j<=1 by A29,A556,BORSUK_1:40,XXREAL_1:1;
A569: Segment(h0/.i,h0/.1,P) c= g2.:([.h2/.j,h2/.(j+1).])
proof
let x be object;
assume
A570: x in Segment(h0/.i,h0/.1,P);
h0/.1=W-min(P) by A72,A67,PARTFUN1:def 6;
then
A571: x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)} by A570,Def1;
A572: j+1 in dom h2 by A46,A36,A52,A55,A57,A554,A561,FINSEQ_3:25;
j<j+1 & j in dom h2 by A47,A36,A52,A55,A57,A554,A560,A563,Lm1,FINSEQ_3:25
;
then h2.j<h2.(j+1) by A30,A572,SEQM_3:def 1;
then
A573: h2/.(j+1) in [.h2/.j, h2/.(j+1).] by A564,A562,XXREAL_1:1;
consider p being Point of TOP-REAL 2 such that
A574: p=x and
A575: LE h0/.i,p,P or h0/.i in P & p=W-min(P) by A571;
A576: h2/.(j+1)=1 by A27,A47,A34,A36,A52,A55,A57,A554,PARTFUN1:def 6;
now
per cases by A575;
suppose
A577: LE h0/.i,p,P & (p<>W-min(P) or not h0/.i in P);
then p in Lower_Arc(P) by A567,A565,JORDAN6:def 10;
then consider z being object such that
A578: z in dom g2 and
A579: p=g2.z by A23,FUNCT_1:def 3;
take z;
thus z in dom g2 by A578;
reconsider rz=z as Real by A131,A578;
A580: rz<=1 by A578,BORSUK_1:40,XXREAL_1:1;
then
A581: rz<=h2/.(j+1) by A27,A47,A36,A52,A55,A57,A554,A561,FINSEQ_4:15;
A582: LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A567,A565,A577,
JORDAN6:def 10;
0<=rz by A578,BORSUK_1:40,XXREAL_1:1;
then h2/.j<=rz by A22,A23,A24,A25,A558,A568,A565,A564,A582,A579,A580
,Th19;
hence z in [.h2/.j,h2/.(j+1).] & x = g2.z by A574,A579,A581,
XXREAL_1:1;
end;
suppose
h0/.i in P & p=W-min(P);
hence ex y being object
st y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x =
g2.y by A25,A227,A574,A573,A576;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
A583: 0 <= h2.j & h2.j <= 1 by A29,A556,BORSUK_1:40,XXREAL_1:1;
A584: g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.1,P)
proof
A585: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:def 9;
let x be object;
assume x in g2.:([.h2/.j,h2/.(j+1).]);
then consider y being object such that
A586: y in dom g2 and
A587: y in [.h2/.j,h2/.(j+1).] and
A588: x=g2.y by FUNCT_1:def 6;
reconsider sy=y as Real by A587;
A589: x in Lower_Arc(P) by A23,A586,A588,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
h2/.j<=sy & sy<=1 by A586,A587,BORSUK_1:40,XXREAL_1:1;
then
A590: LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25,A558
,A565,A583,A564,A588,Th18;
now
per cases;
case
p1=W-min(P);
hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A559,A565,A585,
XBOOLE_0:def 3;
end;
case
p1<>W-min(P);
hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A559,A565,A589
,A590,JORDAN6:def 10;
end;
end;
then
A591: x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)};
h0/.1=W-min(P) by A72,A67,PARTFUN1:def 6;
hence thesis by A591,Def1;
end;
assume W=Segment(h0/.len h0,h0/.1,P);
then W=g2.:Q1 by A569,A584;
hence thesis by A31,A47,A36,A52,A55,A57,A554,A560,A563,Lm1;
end;
A592: 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 that
A593: 1<=i and
A594: i+1<len h0;
A595: i+1+1<=len h0 by A594,NAT_1:13;
A596: i+1<i+1+1 by NAT_1:13;
A597: 1<i+1 by A593,NAT_1:13;
then
A598: 1<i+1+1 by NAT_1:13;
per cases;
suppose
A599: i+1<len h1;
then
A600: i+1 in dom h1 by A597,FINSEQ_3:25;
then
A601: h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A602: 0<=h1.(i+1) & h1.(i+1)<=1 by A11,BORSUK_1:40,XXREAL_1:1;
A603: 1<i+1+1 by A597,NAT_1:13;
then (i+1)+1 in dom h0 by A595,FINSEQ_3:25;
then
A604: h0/.(i+1+1)=h0.(i+1+1) by PARTFUN1:def 6;
A605: i+1+1<=len h1 by A599,NAT_1:13;
then
A606: i+1+1 in dom h1 by A603,FINSEQ_3:25;
then
A607: h1.((i+1)+1) in rng h1 by FUNCT_1:def 3;
then
A608: h1.(i+1+1)<=1 by A11,BORSUK_1:40,XXREAL_1:1;
h0.(i+1+1)=h11.(i+1+1) by A39,A605,A603,FINSEQ_1:64;
then
A609: h0.(i+1+1)=g1.(h1.(i+1+1)) by A606,FUNCT_1:13;
then
A610: h0/.(i+1+1) in Upper_Arc P by A5,A132,A11,A607,A604,BORSUK_1:40
,FUNCT_1:def 3;
i+1 in dom h0 by A594,A597,FINSEQ_3:25;
then
A611: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A612: h0.(i+1)=h11.(i+1) by A39,A597,A599,FINSEQ_1:64;
then
A613: h0.(i+1)=g1.(h1.(i+1)) by A600,FUNCT_1:13;
g1.(h1.(i+1)) in rng g1 by A132,A11,A601,BORSUK_1:40,FUNCT_1:def 3;
then
A614: h0/.(i+1) in Upper_Arc P by A5,A612,A600,A611,FUNCT_1:13;
h1.(i+1)<h1.(i+1+1) by A12,A596,A600,A606,SEQM_3:def 1;
then LE h0/.(i+1),h0/.((i+1)+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4
,A5,A6,A7,A613,A602,A609,A608,A611,A604,Th18;
hence thesis by A614,A610,JORDAN6:def 10;
end;
suppose
A615: i+1>=len h1;
per cases by A615,XXREAL_0:1;
suppose
A616: i+1>len h1;
set j=(i+1)-'len h11+2-'1;
A617: (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
by A36,A595,XREAL_1:9;
A618: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then
A619: 1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
A620: j+1=(i+1)-'len h11+(1+1)-1+1 by A618,Lm1,NAT_D:39,42
.=(i+1)-'len h11+2;
A621: len h1 +1<=i+1 by A616,NAT_1:13;
then
A622: len h1 +1-len h1<=(i+1)-len h1 by XREAL_1:9;
A623: (i+1)-len h11=(i+1)-'len h11 by A39,A616,XREAL_1:233;
(i+1)+1>len h11 by A39,A616,NAT_1:13;
then
A624: (i+1)+1-len h11=(i+1)+1-'len h11 by XREAL_1:233;
A625: len h1 +1<=(i+1)+1 by A621,NAT_1:13;
then
A626: len h1 +1-len h1<=(i+1)+1-len h1 by XREAL_1:9;
then 1<(i+1)+1-'len h11+(2-1) by A39,A624,NAT_1:13;
then
A627: 0<(i+1)+1-'len h11+2-1;
(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A618,Lm1,NAT_D:39,42;
then
A628: j+1=(i+1)+1-'len h11+2-'1 by A623,A624,A627,XREAL_0:def 2;
(i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57
,A594,XREAL_1:9;
then
A629: (i+1)-'len h11+2<=len h2-2+2 by A39,A623,XREAL_1:6;
then ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A630: j in dom h2 by A46,A619,FINSEQ_3:25;
2-'1<=((i+1)-'len h11 +2-'1) by A618,NAT_D:42;
then 1<j+1 by Lm1,NAT_1:13;
then
A631: j+1 in dom h2 by A629,A620,FINSEQ_3:25;
then
A632: h2.(j+1) in rng h2 by FUNCT_1:def 3;
then
A633: (h2.(j+1)) <= 1 by A29,BORSUK_1:40,XXREAL_1:1;
j<j+1 by NAT_1:13;
then
A634: h2.j<h2.(j+1) by A30,A630,A631,SEQM_3:def 1;
A635: i+1<=len h11 + len (mid(h21,2,len h21 -'1)) by A594,FINSEQ_1:22;
len h11+1<=i+1 by A39,A616,NAT_1:13;
then
A636: h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) by A635,FINSEQ_1:23;
(i+1)-len h11<=len h11 + len (mid(h21,2,len h21 -'1)) -len h11
by A635,XREAL_1:9;
then h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A39,A48,A56,A50,A54,A636
,A623,A622,FINSEQ_6:118;
then
A637: h0.(i+1)=g2.(h2.j) by A630,FUNCT_1:13;
A638: h2.j in rng h2 by A630,FUNCT_1:def 3;
then
A639: h0.(i+1) in Lower_Arc(P) by A23,A131,A29,A637,BORSUK_1:40,FUNCT_1:def 3
;
(i+1)+1 in dom h0 by A595,A598,FINSEQ_3:25;
then
A640: h0/.((i+1)+1)=h0.((i+1)+1) by PARTFUN1:def 6;
h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11) by A39,A36
,A595,A625,FINSEQ_1:23;
then
A641: h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A624
,A617,A626,FINSEQ_6:118;
then
A642: h0.((i+1)+1)=g2.(h2.(j+1)) by A628,A631,FUNCT_1:13;
then
A643: h0.((i+1)+1) in Lower_Arc(P) by A23,A131,A29,A632,BORSUK_1:40
,FUNCT_1:def 3;
(i+1)-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A594,
XREAL_1:9;
then (i+1)-len h11+2<len h2-2+2 by XREAL_1:6;
then
A644: h0/.(i+1+1) <> W-min P by A46,A34,A35,A32,A623,A641,A620,A628,A631,A640
;
i+1 in dom h0 by A594,A597,FINSEQ_3:25;
then
A645: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
0<=h2.j & h2.j<=1 by A29,A638,BORSUK_1:40,XXREAL_1:1;
then LE h0/.(i+1),h0/.((i+1)+1),Lower_Arc(P),E-max(P),W-min(P) by A21
,A22,A23,A24,A25,A637,A642,A634,A645,A640,A633,Th18;
hence thesis by A645,A640,A639,A643,A644,JORDAN6:def 10;
end;
suppose
A646: i+1=len h1;
then len h1+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A595,
FINSEQ_1:22;
then
A647: (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
by A646,XREAL_1:9;
then 1<=(i+1)+1-'len h11 by A39,A596,A646,XREAL_1:233;
then 1<(i+1)+1-'len h11+(2-1) by NAT_1:13;
then
A648: 0<(i+1)+1-'len h11+2-1;
A649: (i+1)+1-len h11=(i+1)+1-'len h11 by A39,A596,A646,XREAL_1:233;
len h1 in dom h0 by A594,A597,A646,FINSEQ_3:25;
then
A650: h0/.len h1=h0.len h1 by PARTFUN1:def 6;
set j=(i+1)-'len h11+2-'1;
A651: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then
A652: j+1=(i+1)-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
.=(i+1)-'len h11+(1+1);
2-'1<=((i+1)-'len h11 +2-'1) by A651,NAT_D:42;
then
A653: 1<j+1 by Lm1,NAT_1:13;
len h1-len h11=len h1-'len h11 & (i+1)-len h11<=len h1+(len h2-2
)-len h11 by A39,A47,A36,A52,A55,A57,A594,XREAL_1:9,233;
then (i+1)-'len h11+2<=len h2-2+2 by A39,A646,XREAL_1:6;
then
A654: j+1 in dom h2 by A652,A653,FINSEQ_3:25;
then
A655: h2.(j+1) in rng h2 by FUNCT_1:def 3;
h0.len h1 =E-max(P) by A39,A255,A597,A646,FINSEQ_1:64;
then
A656: h0.(i+1) in Upper_Arc(P) by A1,A646,Th1;
(i+1)+1 in dom h0 by A595,A598,FINSEQ_3:25;
then
A657: h0/.((i+1)+1)=h0.((i+1)+1) by PARTFUN1:def 6;
h0.((i+1)+1)=(mid(h21,2,len h21 -'1)).((i+1)+1 -len h11) by A39,A36
,A595,A646,FINSEQ_1:23;
then
A658: h0.((i+1)+1)=h21.((i+1)+1-'len h11 +2-'1) by A39,A48,A56,A50,A54,A646
,A649,A647,FINSEQ_6:118;
A659: j+1=(i+1)-len h11+2-1+1 by A39,A646,Lm1,XREAL_0:def 2
.=(i+1)+1-'len h11+2-'1 by A649,A648,XREAL_0:def 2;
then h0.((i+1)+1)=g2.(h2.(j+1)) by A658,A654,FUNCT_1:13;
then
A660: h0.(i+1+1) in Lower_Arc P by A23,A131,A29,A655,BORSUK_1:40
,FUNCT_1:def 3;
(i+1)-len h11<len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A594,
XREAL_1:9;
then (i+1)-len h11+2<len h2-2+2 by XREAL_1:6;
then j+1<len h2 by A39,A646,A652,XREAL_0:def 2;
then h0/.(i+1+1) <> W-min P by A46,A34,A35,A32,A658,A659,A654,A657;
hence thesis by A646,A650,A657,A660,A656,JORDAN6:def 10;
end;
end;
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
A661: 1<=i & i+1<len h0;
then
A662: LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) by A256;
h0/.i<>h0/.(i+1) & LE h0/.(i+1),h0/.(i+2),P by A592,A256,A661;
hence thesis by A1,A662,Th10;
end;
A663: 2 in dom h0 by A201,FINSEQ_3:25;
i <> 1 by A59,Lm2;
then
A664: h0/.i <> h0/.1 by A67,A78,A203,PARTFUN2:10;
A665: len h1 in dom h1 by A16,FINSEQ_3:25;
thus Segment(h0/.len h0,h0/.1,P)/\ Segment(h0/.1,h0/.2,P)={h0/.1}
proof
defpred P[Nat] means $1+2<=len h0 implies LE h0/.2,h0/.($1+2),P;
set j=len h0-'len h11+2-'1;
A666: len h0 -len h11 <=len h11 + len mid(h21,2,len h21 -'1) -len h11 by
FINSEQ_1:22;
A667: h0/.2=h0.2 by A663,PARTFUN1:def 6;
A668: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A669: k+2<=len h0 implies LE h0/.2,h0/.(k+2),P;
now
A670: k+1+1=k+2;
A671: k+1+2=k+2+1;
assume
A672: k+1+2<=len h0;
then k+2<len h0 by A671,NAT_1:13;
then LE h0/.(k+2),h0/.(k+2+1),P by A592,A671,A670,NAT_1:11;
hence LE h0/.2,h0/.(k+1+2),P by A1,A669,A672,JORDAN6:58,NAT_1:13;
end;
hence thesis;
end;
len h0 -'2=len h0-2 by A65,A14,XREAL_1:233,XXREAL_0:2;
then
A673: len h0-'2+2=len h0;
0+2<=len h0-'len h11 +2 by XREAL_1:6;
then
A674: 1<=(len h0-'len h11 +2-'1) by Lm1,NAT_D:42;
(len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,A252,NAT_D:44;
then
A675: j in dom h2 by A46,A674,FINSEQ_3:25;
h0.2=g1.(h1.2) & h1.2 in rng h1 by A15,A40,FUNCT_1:13,def 3;
then
A676: h0/.2 in Upper_Arc P by A5,A132,A11,A667,BORSUK_1:40,FUNCT_1:def 3;
Upper_Arc(P) \/ Lower_Arc(P)= P by A1,JORDAN6:50;
then h0/.2 in P by A676,XBOOLE_0:def 3;
then
A677: P[0] by A1,JORDAN6:56;
A678: for i being Nat holds P[i] from NAT_1:sch 2(A677,A668);
A679: h11.2 <> W-min(P) by A38,A17,A71,A15,A20;
len h1 +1-len h1<=len h0 -len h1 & h0.len h0=(mid(h21,2,len h21 -'1)
).(len h0 -len h11) by A39,A36,A549,A62,A64,FINSEQ_1:23,XXREAL_0:2;
then h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A48,A56,A50,A54,A252,A666
,FINSEQ_6:118;
then
A680: h0.len h0=g2.(h2.j) by A675,FUNCT_1:13;
A681: now
h2.j in rng h2 by A675,FUNCT_1:def 3;
then
A682: g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
assume h0/.2=h0/.len h0;
then h0/.2 in Upper_Arc(P)/\ Lower_Arc(P) by A23,A75,A676,A680,A682,
XBOOLE_0:def 4;
then h0/.2 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then h11.2=E-max(P) by A40,A679,A667,TARSKI:def 2;
hence contradiction by A38,A665,A255,A14,A15,A20;
end;
h0/.2<>W-min(P) by A663,A40,A679,PARTFUN1:def 6;
hence thesis by A1,A73,A681,A678,A673,Th12;
end;
A683: i+1 = len h0 by A16,A65,XREAL_1:235,XXREAL_0:2;
then LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) by A256,A202;
hence Segment(h0/.i,h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P)={h0/.len h0}
by A1,A73,A683,A664,Th11;
LE h0/.i,h0/.(i+1),P by A256,A202,A200;
hence Segment(h0/.i,h0/.len h0,P) misses Segment(h0/.1,h0/.2,P) by A1,A683
,A333,A229,A207,Th13;
thus for i,j being Nat st 1<=i & i < j & j < len h0 &
i,j aren't_adjacent
holds Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P)
proof
let i,j be Nat;
assume that
A684: 1<=i and
A685: i < j and
A686: j < len h0 and
A687: i,j aren't_adjacent;
A688: 1<j by A684,A685,XXREAL_0:2;
i<len h0 by A685,A686,XXREAL_0:2;
then
A689: i+1<=len h0 by NAT_1:13;
then
A690: LE h0/.i,h0/.(i+1),P & h0/.i<>h0/.(i+1) by A256,A684;
A691: i+1<=j by A685,NAT_1:13;
then
A692: (i+1)<len h0 by A686,XXREAL_0:2;
A693: not j=i+1 by A687,GOBRD10:def 1;
then
A694: i+1<j by A691,XXREAL_0:1;
A695: now
assume
A696: h0/.(i+1)=h0/.j;
per cases;
suppose
A697: i+1<=len h1;
A698: 1<i+1 by A684,NAT_1:13;
then
A699: i+1 in dom h1 by A697,FINSEQ_3:25;
then
A700: h1.(i+1) in rng h1 by FUNCT_1:def 3;
i+1 in dom h0 by A689,A698,FINSEQ_3:25;
then
A701: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A702: h0.(i+1)=h11.(i+1) by A39,A697,A698,FINSEQ_1:64;
then h0.(i+1)=g1.(h1.(i+1)) by A699,FUNCT_1:13;
then
A703: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A700,BORSUK_1:40,FUNCT_1:def 3;
per cases;
suppose
A704: j<=len h1;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A705: h0/.j=h0.j by PARTFUN1:def 6;
h0.(j)=h11.(j) & j in dom h1 by A39,A688,A704,FINSEQ_1:64,FINSEQ_3:25
;
hence contradiction by A38,A20,A693,A696,A699,A701,A702,A705;
end;
suppose
A706: j>len h1;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A707: h0/.j=h0.j by PARTFUN1:def 6;
A708: j-len h11=j-'len h11 by A39,A706,XREAL_1:233;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then j-'len h11+2<=len h2-2+2 by A39,A708,XREAL_1:6;
then
A709: (j-'len h11 +2-'1)<= len h21 by A47,NAT_D:44;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then
A710: j-'len h11+2<=len h2-2+2 by A39,A708,XREAL_1:6;
set k=j-'len h11+2-'1;
j<= len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
then
A711: j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by
XREAL_1:9;
A712: 0+2<=j-'len h11 +2 by XREAL_1:6;
then
A713: j-'len h11+2-'1=j-'len h11+2-1 by Lm1,NAT_D:39,42;
1<=(j-'len h11 +2-'1) by A712,Lm1,NAT_D:42;
then
A714: k in dom h2 by A46,A709,FINSEQ_3:25;
then h2.k in rng h2 by FUNCT_1:def 3;
then
A715: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
A716: len h1 +1<=j by A706,NAT_1:13;
then h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) & len h1 +1-len h1
<=j-len h1 by A39,A36,A686,FINSEQ_1:23,XREAL_1:9;
then
A717: h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A708,A711,
FINSEQ_6:118;
then h0.j=g2.(h2.k) by A714,FUNCT_1:13;
then h0.j in Upper_Arc(P) /\ Lower_Arc(P) by A23,A696,A701,A703,A707
,A715,XBOOLE_0:def 4;
then
A718: h0.j in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
len h11+1-len h11<=j-len h11 by A39,A716,XREAL_1:9;
then 1<=j-'len h11 by NAT_D:39;
then 1+2<=j-'len h11+2 by XREAL_1:6;
then 1+2-1<=j-'len h11+2-1 by XREAL_1:9;
then 1<k by A713,XXREAL_0:2;
then
A719: h0.j <> E-max P by A46,A76,A77,A32,A717,A714;
j-'len h11+2-'1<j-'len h11+2-'1+1 by NAT_1:13;
then h0.j <> W-min P by A46,A34,A35,A32,A717,A713,A710,A714;
hence contradiction by A718,A719,TARSKI:def 2;
end;
end;
suppose
A720: i+1>len h1;
then
A721: j>len h1 by A691,XXREAL_0:2;
then
A722: len h1 +1<=j by NAT_1:13;
then
A723: len h1 +1-len h1<=j-len h1 by XREAL_1:9;
len h11+1-len h11<=j-len h11 by A39,A722,XREAL_1:9;
then
A724: j-'len h11=j-len h11 by NAT_D:39;
A725: len h1 +1<=i+1 by A720,NAT_1:13;
then len h11+1-len h11<=(i+1)-len h11 by A39,XREAL_1:9;
then (i+1)-'len h11=(i+1)-len h11 by NAT_D:39;
then i+1-'len h11<j-'len h11 by A694,A724,XREAL_1:9;
then
A726: i+1-'len h11+2<j-'len h11+2 by XREAL_1:6;
set k=j-'len h11+2-'1;
set j0=(i+1)-'len h11+2-'1;
A727: j<= len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
A728: (i+1)-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
by A36,A689,XREAL_1:9;
A729: j-len h11=j-'len h11 by A39,A691,A720,XREAL_1:233,XXREAL_0:2;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then j-'len h11+2<=len h2-2+2 by A39,A729,XREAL_1:6;
then
A730: (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
A731: 0+2<=j-'len h11 +2 by XREAL_1:6;
then
A732: j-'len h11+2-'1=j-'len h11+2-1 by Lm1,NAT_D:39,42;
1<=(j-'len h11 +2-'1) by A731,Lm1,NAT_D:42;
then
A733: k in dom h2 by A46,A730,FINSEQ_3:25;
A734: (i+1)-len h11=(i+1)-'len h11 by A39,A720,XREAL_1:233;
len h11+1<=j by A39,A721,NAT_1:13;
then
A735: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by A727,FINSEQ_1:23;
j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A686,
XREAL_1:9;
then
A736: h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A735,A729,A723,
FINSEQ_6:118;
1<=i+1 by A684,NAT_1:13;
then i+1 in dom h0 by A689,FINSEQ_3:25;
then
A737: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A738: h0/.j=h0.j by PARTFUN1:def 6;
(i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57
,A689,XREAL_1:9;
then (i+1)-'len h11+2<=len h2-2+2 by A39,A734,XREAL_1:6;
then
A739: ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
A740: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then 1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
then
A741: j0 in dom h2 by A46,A739,FINSEQ_3:25;
(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A740,Lm1,NAT_D:39,42;
then
A742: (i+1)-'len h11+2-'1<j-'len h11+2-'1 by A732,A726,XREAL_1:9;
h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) & len h1 +1-
len h1<=(i+1) -len h1 by A39,A36,A689,A725,FINSEQ_1:23,XREAL_1:9;
then h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A39,A48,A56,A50,A54,A734
,A728,FINSEQ_6:118;
hence contradiction by A46,A32,A696,A741,A737,A736,A742,A733,A738;
end;
end;
A743: j+1<=len h0 by A686,NAT_1:13;
A744: 1<i+1 by A684,NAT_1:13;
A745: 1<=(i+1) by A684,NAT_1:13;
A746: i+1<len h0 by A686,A691,XXREAL_0:2;
A747: LE h0/.(i+1),h0/.j,P
proof
per cases;
suppose
A748: i+1<=len h1;
per cases;
suppose
A749: j<=len h1;
A750: 1<j by A694,A745,XXREAL_0:2;
then
A751: j in dom h1 by A749,FINSEQ_3:25;
then
A752: h1.j in rng h1 by FUNCT_1:def 3;
then
A753: (h1.j) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
j in dom h0 by A686,A750,FINSEQ_3:25;
then
A754: h0/.j=h0.j by PARTFUN1:def 6;
h0.j=h11.j by A39,A749,A750,FINSEQ_1:64;
then
A755: g1.(h1.j) = h0/.j by A751,A754,FUNCT_1:13;
then
A756: h0/.j in Upper_Arc(P) by A5,A132,A11,A752,BORSUK_1:40,FUNCT_1:def 3;
i+1 in dom h0 by A745,A692,FINSEQ_3:25;
then
A757: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A758: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
A759: (i+1) in dom h1 by A745,A748,FINSEQ_3:25;
then
A760: h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A761: 0 <= (h1.(i+1)) & (h1.(i+1)) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
h0.(i+1)=h11.(i+1) by A39,A745,A748,FINSEQ_1:64;
then
A762: g1.(h1.(i+1)) = h0/.(i+1) by A759,A757,FUNCT_1:13;
then
A763: h0/.(i+1) in Upper_Arc(P) by A5,A132,A11,A760,BORSUK_1:40
,FUNCT_1:def 3;
(h1.(i+1)) <= (h1.j) by A12,A694,A759,A751,SEQM_3:def 1;
then LE h0/.(i+1),h0/.j,Upper_Arc(P),W-min(P),E-max(P) by A4,A5,A6,A7
,A758,A762,A761,A755,A753,Th18;
hence thesis by A763,A756,JORDAN6:def 10;
end;
suppose
A764: j>len h1;
set k=j-'len h11+2-'1;
0+2<=j-'len h11 +2 by XREAL_1:6;
then
A765: 2-'1<=j-'len h11 +2-'1 by NAT_D:42;
A766: j-len h11=j-'len h11 by A39,A764,XREAL_1:233;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then j-'len h11+2<=len h2-2+2 by A39,A766,XREAL_1:6;
then (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A767: (j-'len h11 +2-'1) in dom h21 by A765,Lm1,FINSEQ_3:25;
j+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A743,XREAL_1:9;
then j-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
then j-'len h11+2<=len h2-2-1+2 by A39,A766,XREAL_1:6;
then
A768: j-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
A769: h0.(i+1)=h11.(i+1) by A39,A744,A748,FINSEQ_1:64;
i+1 in dom h1 by A744,A748,FINSEQ_3:25;
then h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A770: g1.(h1.(i+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
0+1<=j-'len h11+1+1-1 by XREAL_1:6;
then
A771: j-'len h11+2-'1=j-'len h11+2-1 by NAT_D:39;
len h1 +1<=j by A764,NAT_1:13;
then
A772: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) & len h1 +1-len h1
<=j-len h1 by A39,A36,A686,FINSEQ_1:23,XREAL_1:9;
A773: j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36
,A686,XREAL_1:9;
then h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A766,A772,
FINSEQ_6:118;
then
A774: h0.j=g2.(h2.k) by A46,A767,FUNCT_1:13;
j-len h11=j-'len h11 by A39,A764,XREAL_1:233;
then
A775: h0.j=h21.k by A39,A48,A56,A50,A54,A773,A772,FINSEQ_6:118;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A776: h0/.j=h0.j by PARTFUN1:def 6;
h2.k in rng h2 by A46,A767,FUNCT_1:def 3;
then
A777: h0.j in Lower_Arc(P) by A23,A131,A29,A774,BORSUK_1:40,FUNCT_1:def 3;
i+1 in Seg len h1 by A745,A748,FINSEQ_1:1;
then i+1 in dom h1 by FINSEQ_1:def 3;
then
A778: h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:13;
(i+1) in dom h0 by A745,A692,FINSEQ_3:25;
then
A779: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
len h2-1-1<len h2 by Lm4;
then h0/.j <> W-min P by A46,A34,A35,A32,A771,A767,A768,A775,A776;
hence thesis by A5,A769,A778,A779,A776,A770,A777,JORDAN6:def 10;
end;
end;
suppose
A780: i+1>len h1;
set j0=(i+1)-'len h11+2-'1;
set k=j-'len h11+2-'1;
A781: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then
A782: 1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
A783: j-len h11=j-'len h11 by A39,A691,A780,XREAL_1:233,XXREAL_0:2;
len h1<j by A691,A780,XXREAL_0:2;
then
A784: len h11+1<=j by A39,NAT_1:13;
then
A785: len h1 +1-len h1<=j-len h1 by A39,XREAL_1:9;
j<=len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
then
A786: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) by A784,FINSEQ_1:23;
A787: i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11 by A36
,A746,XREAL_1:9;
then j-len h11 <= len (mid(h21,2,len h21 -'1)) by A36,A686,XREAL_1:9;
then
A788: h0.j=h21.(k) by A39,A48,A56,A50,A54,A783,A786,A785,FINSEQ_6:118;
A789: (i+1)-len h11=(i+1)-'len h11 by A39,A780,XREAL_1:233;
then (i+1)-'len h11+2<=len h2-2+2 by A47,A52,A55,A57,A787,XREAL_1:6;
then ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A790: j0 in dom h2 by A46,A782,FINSEQ_3:25;
then
A791: h2.j0 in rng h2 by FUNCT_1:def 3;
then
A792: 0<=h2.j0 & h2.j0<=1 by A29,BORSUK_1:40,XXREAL_1:1;
A793: g2.(h2.j0) in rng g2 by A131,A29,A791,BORSUK_1:40,FUNCT_1:def 3;
A794: j-len h11=j-'len h11 by A39,A691,A780,XREAL_1:233,XXREAL_0:2;
j+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A743,XREAL_1:9;
then j-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
then j-'len h11+2<=len h2-2-1+2 by A39,A794,XREAL_1:6;
then
A795: j-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
0+1<=j-'len h11+1+1-1 by XREAL_1:6;
then
A796: j-'len h11+2-'1=j-'len h11+2-1 by NAT_D:39;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then j-'len h11+2<=len h2-2+2 by A39,A794,XREAL_1:6;
then
A797: (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
0+2<=j-'len h11 +2 by XREAL_1:6;
then 2-'1<=j-'len h11 +2-'1 by NAT_D:42;
then
A798: j-'len h11 +2-'1 in dom h21 by A797,Lm1,FINSEQ_3:25;
then
A799: h2.k in rng h2 by A46,FUNCT_1:def 3;
then
A800: h2.k<=1 by A29,BORSUK_1:40,XXREAL_1:1;
j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A686,
XREAL_1:9;
then
A801: h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A794,A786,A785,
FINSEQ_6:118;
then h0.j=g2.(h2.k) by A46,A798,FUNCT_1:13;
then
A802: h0.(j) in Lower_Arc(P) by A23,A131,A29,A799,BORSUK_1:40,FUNCT_1:def 3;
A803: (i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A781,Lm1,NAT_D:39,42;
A804: i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A746,FINSEQ_1:22;
(i+1)-len h11<j-len h11 by A694,XREAL_1:9;
then (i+1)-'len h11+2<j-'len h11+2 by A783,A789,XREAL_1:6;
then j0<k by A796,A803,XREAL_1:9;
then
A805: h2.(j0)<h2.(k) by A30,A46,A798,A790,SEQM_3:def 1;
(i+1) in dom h0 by A745,A692,FINSEQ_3:25;
then
A806: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
len h1+1<=i+1 by A780,NAT_1:13;
then
A807: len h1+1-len h1<=i+1-len h1 by XREAL_1:9;
then
A808: i+1-'len h11=i+1-len h11 by A39,NAT_D:39;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A809: h0/.j=h0.(j) by PARTFUN1:def 6;
len h11+1<=i+1 by A39,A780,NAT_1:13;
then h0.(i+1)=(mid(h21,2,len h21 -'1)).(i+1 -len h11) by A804,
FINSEQ_1:23
.=h21.(i+1-'len h11+2-'1) by A39,A48,A56,A50,A54,A787,A807,A808,
FINSEQ_6:118;
then
A810: h0.(i+1)=g2.(h2.j0) by A790,FUNCT_1:13;
len h2-1-1<len h2 by Lm4;
then
A811: h0/.j <> W-min P by A46,A34,A35,A32,A796,A798,A795,A788,A809;
h21.k=g2.(h2.k) by A46,A798,FUNCT_1:13;
then LE h0/.(i+1),h0/.j,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A801,A800,A810,A792,A805,A806,A809,Th18;
hence thesis by A23,A810,A806,A809,A793,A802,A811,JORDAN6:def 10;
end;
end;
LE h0/.j,h0/.(j+1),P by A256,A688,A743;
hence thesis by A1,A690,A747,A695,Th13;
end;
let i be Nat such that
A812: 1 < i and
A813: i+1 < len h0;
A814: 1<i+1 by A812,NAT_1:13;
then
A815: i+1 in dom h0 by A813,FINSEQ_3:25;
A816: 1<=len h0-len h1 by A549,A62,XXREAL_0:2;
A817: now
assume
A818: h0/.(i+1)=h0/.len h0;
per cases;
suppose
A819: i+1<=len h1;
then
A820: i+1 in dom h1 by A814,FINSEQ_3:25;
h0.(i+1)=h11.(i+1) by A39,A814,A819,FINSEQ_1:64;
then
A821: h0.(i+1)=g1.(h1.(i+1)) by A820,FUNCT_1:13;
h1.(i+1) in rng h1 by A820,FUNCT_1:def 3;
then
A822: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A821,BORSUK_1:40,FUNCT_1:def 3;
i+1 in dom h0 by A813,A814,FINSEQ_3:25;
then
A823: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
1+2<=len h0-'len h11+2 by A47,A36,A52,A55,A57,A63,A252,XREAL_1:6;
then
A824: 1+2-1<=len h0-'len h11+2-1 by XREAL_1:9;
set k=len h0-'len h11+2-'1;
A825: 0+2<=len h0-'len h11 +2 by XREAL_1:6;
then
A826: 2-'1<=(len h0-'len h11 +2-'1) by NAT_D:42;
len h0-'len h11 +2-'1 <= len h21 by A36,A52,A55,A57,A252,NAT_D:44;
then
A827: k in dom h2 by A46,A826,Lm1,FINSEQ_3:25;
then h2.k in rng h2 by FUNCT_1:def 3;
then
A828: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A39,A36,A64,
FINSEQ_1:23;
then
A829: h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A36,A48,A56,A50,A54,A816
,A252,FINSEQ_6:118;
then h0.len h0=g2.(h2.k) by A827,FUNCT_1:13;
then h0.len h0 in Upper_Arc(P) /\ Lower_Arc(P) by A23,A75,A818,A823,A822
,A828,XBOOLE_0:def 4;
then
A830: h0.len h0 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
len h0-'len h11+2-'1=len h0-'len h11+2-1 by A825,Lm1,NAT_D:39,42;
then 1<k by A824,XXREAL_0:2;
then
A831: h0.len h0 <> E-max P by A46,A76,A77,A32,A829,A827;
len h0-'len h11+2-'1<len h0-'len h11+2-'1+1 by NAT_1:13;
then h0.len h0 <> W-min P by A46,A47,A34,A35,A36,A52,A55,A57,A252,A32
,A829,A827;
hence contradiction by A830,A831,TARSKI:def 2;
end;
suppose
A832: i+1>len h1;
set k=len h0-'len h11+2-'1;
set j0=(i+1)-'len h11+2-'1;
A833: 0+2<=len h0-'len h11 +2 by XREAL_1:6;
then
A834: 2-'1<=(len h0-'len h11 +2-'1) by NAT_D:42;
len h0-'len h11 +2-'1 <= len h21 by A36,A52,A55,A57,A252,NAT_D:44;
then
A835: k in dom h2 by A46,A834,Lm1,FINSEQ_3:25;
i+1 <= len h11 + len mid(h21,2,len h21 -'1) by A813,FINSEQ_1:22;
then
A836: i+1-len h11 <=len h11 + len mid(h21,2,len h21 -'1)-len h11 by XREAL_1:9;
A837: len h1 +1<=i+1 by A832,NAT_1:13;
then len h11+1-len h11<=(i+1)-len h11 by A39,XREAL_1:9;
then
A838: (i+1)-'len h11=(i+1)-len h11 by NAT_D:39;
len h0-'len h11=len h0-len h11 by A36,A57,XREAL_0:def 2;
then i+1-'len h11<len h0-'len h11 by A813,A838,XREAL_1:9;
then
A839: i+1-'len h11+2<len h0-'len h11+2 by XREAL_1:6;
1<=i+1 by A812,NAT_1:13;
then i+1 in dom h0 by A813,FINSEQ_3:25;
then
A840: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A841: len h0-'len h11+2-'1=len h0-'len h11+2-1 by A833,Lm1,NAT_D:39,42;
A842: (i+1)-len h11=(i+1)-'len h11 by A39,A832,XREAL_1:233;
(i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A813,
XREAL_1:9;
then (i+1)-'len h11+2<=len h2-2+2 by A39,A842,XREAL_1:6;
then
A843: (i+1)-'len h11 +2-'1 <= len h21 by A47,NAT_D:44;
A844: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then 2-'1<=((i+1)-'len h11 +2-'1) by NAT_D:42;
then
A845: j0 in dom h2 by A46,A843,Lm1,FINSEQ_3:25;
h0.(i+1)=(mid(h21,2,len h21 -'1)).((i+1) -len h11) & len h1 +1-
len h1<=(i+1) -len h1 by A39,A36,A813,A837,FINSEQ_1:23,XREAL_1:9;
then
A846: h0.(i+1)=h21.((i+1)-'len h11 +2-'1) by A39,A48,A56,A50,A54,A842,A836,
FINSEQ_6:118;
(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A844,Lm1,NAT_D:39,42;
then
A847: (i+1)-'len h11+2-'1<k by A841,A839,XREAL_1:9;
h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A39,A36,A64,
FINSEQ_1:23;
then h0.len h0=h21.(len h0-'len h11 +2-'1) by A47,A36,A51,A52,A49,A48,A53
,A55,A57,A63,A252,FINSEQ_6:118;
hence contradiction by A46,A75,A32,A818,A846,A845,A840,A847,A835;
end;
end;
h0.len h0=mid(h21,2,len h21 -'1).(len h0 -len h11) by A39,A36,A64,FINSEQ_1:23
;
then
A848: h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A36,A48,A56,A50,A54,A816
,A252,FINSEQ_6:118;
then
A849: h0.len h0 in Lower_Arc(P) by A23,A131,A29,A253,BORSUK_1:40,FUNCT_1:def 3;
A850: LE h0/.(i+1),h0/.len h0,P
proof
per cases;
suppose
A851: i+1<=len h1;
then i+1 in dom h1 by A814,FINSEQ_3:25;
then h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A852: g1.(h1.(i+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
A853: h0/.(i+1)=h0.(i+1) by A815,PARTFUN1:def 6;
i+1 in dom h1 by A814,A851,FINSEQ_3:25;
then
A854: h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:13;
h0.(i+1)=h11.(i+1) by A39,A814,A851,FINSEQ_1:64;
hence thesis by A5,A75,A130,A849,A854,A853,A852,JORDAN6:def 10;
end;
suppose
A855: i+1>len h1;
then len h1+1<=i+1 by NAT_1:13;
then
A856: len h1+1-len h1<=i+1-len h1 by XREAL_1:9;
then
A857: i+1-'len h11=i+1-len h11 by A39,NAT_D:39;
A858: i+1-len h11<len h11 + len (mid(h21,2,len h21 -'1)) - len h11 by A36,A813,
XREAL_1:9;
A859: i+1<len h11 + len (mid(h21,2,len h21 -'1)) by A813,FINSEQ_1:22;
len h11+1<=i+1 by A39,A855,NAT_1:13;
then
A860: h0.(i+1) = mid(h21,2,len h21 -'1).(i+1 -len h11) by A859,FINSEQ_1:23
.= h21.(i+1-'len h11+2-'1) by A39,A48,A56,A50,A54,A858,A856,A857,
FINSEQ_6:118;
set j0=(i+1)-'len h11+2-'1;
set k=len h0-'len h11+2-'1;
0+1<=len h0-'len h11+1+1-1 by XREAL_1:6;
then
A861: len h0-'len h11+2-'1=len h0-'len h11+2-1 by NAT_D:39;
A862: (len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,A252,NAT_D:44;
then
A863: (len h0-'len h11 +2-'1) in dom h21 by A43,Lm1,FINSEQ_3:25;
then h2.k in rng h2 by A46,FUNCT_1:def 3;
then
A864: h2.k<=1 by A29,BORSUK_1:40,XXREAL_1:1;
len h0-'len h11 +2-'1 in dom h21 by A43,A862,Lm1,FINSEQ_3:25;
then
A865: h21.k=g2.(h2.k) by A46,FUNCT_1:13;
A866: (i+1)-len h11=(i+1)-'len h11 by A39,A855,XREAL_1:233;
(i+1)-len h11<=len h11+(len h2-2)-len h11 by A47,A36,A52,A55,A57,A813,
XREAL_1:9;
then (i+1)-'len h11+2<=len h2-2+2 by A866,XREAL_1:6;
then
A867: (i+1)-'len h11 +2-'1 <= len h21 by A47,NAT_D:44;
h0.(len h0) in Lower_Arc(P) by A23,A131,A29,A848,A253,BORSUK_1:40
,FUNCT_1:def 3;
then
A868: h0/.len h0 in Lower_Arc P by A74,PARTFUN1:def 6;
A869: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then 2-'1<=((i+1)-'len h11 +2-'1) by NAT_D:42;
then
A870: j0 in dom h2 by A46,A867,Lm1,FINSEQ_3:25;
then
A871: h2.j0 in rng h2 by FUNCT_1:def 3;
then
A872: 0<=h2.j0 & h2.j0<=1 by A29,BORSUK_1:40,XXREAL_1:1;
(i+1)-len h11<len h0-len h11 by A813,XREAL_1:9;
then
A873: (i+1)-'len h11+2<len h0-'len h11+2 by A252,A866,XREAL_1:6;
h0.len h0=(mid(h21,2,len h21 -'1)).(len h0 -len h11) by A39,A36,A64,
FINSEQ_1:23;
then
A874: h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A36,A48,A56,A50,A54,A816
,A252,FINSEQ_6:118;
A875: h0/.(i+1)=h0.(i+1) by A815,PARTFUN1:def 6;
g2.(h2.j0) in rng g2 by A131,A29,A871,BORSUK_1:40,FUNCT_1:def 3;
then
A876: h0.(i+1) in Lower_Arc(P) by A23,A860,A870,FUNCT_1:13;
(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A869,Lm1,NAT_D:39,42;
then j0<k by A861,A873,XREAL_1:9;
then
A877: h2.(j0)<h2.(k) by A30,A46,A863,A870,SEQM_3:def 1;
h0.(i+1)=g2.(h2.j0) by A860,A870,FUNCT_1:13;
then LE h0/.(i+1),h0/.len h0,Lower_Arc(P),E-max(P),W-min(P) by A21,A22
,A23,A24,A25,A75,A874,A865,A864,A872,A877,A875,Th18;
hence thesis by A130,A875,A876,A868,JORDAN6:def 10;
end;
end;
i<len h0 by A813,NAT_1:13;
then
A878: i in dom h0 by A812,FINSEQ_3:25;
then h0/.i = h0.i by PARTFUN1:def 6;
then
A879: h0/.i<>W-min P by A72,A67,A78,A812,A878;
LE h0/.i,h0/.(i+1),P by A256,A812,A813;
hence thesis by A1,A72,A68,A879,A850,A817,Th14;
end;