:: The Ordering of Points on a Curve, Part { I }
:: by Adam Grabowski and Yatsuka Nakamura
::
:: Received September 10, 1997
:: Copyright (c) 1997-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, NAT_1, XXREAL_0, ARYTM_1, ARYTM_3, CARD_1, STRUCT_0,
BORSUK_1, PRE_TOPC, EUCLID, MCART_1, RLTOPSP1, REAL_1, RELAT_1, SUPINF_2,
XXREAL_1, FINSEQ_1, XBOOLE_0, SUBSET_1, FUNCT_1, TOPREAL1, TOPS_2,
PARTFUN1, TOPMETR, TREAL_1, VALUED_1, FUNCT_4, RCOMP_1, TARSKI, ORDINAL2,
PCOMPS_1, METRIC_1, JORDAN3, RFINSEQ, FINSEQ_5, GROUP_2, ORDINAL4,
GOBOARD5, GOBOARD2, TREES_1, TOPREAL4, GOBOARD1, MATRIX_1, FUNCT_2;
notations TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, NUMBERS, XXREAL_0, XCMPLX_0,
XREAL_0, REAL_1, NAT_1, NAT_D, RCOMP_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_4, TOPMETR, FINSEQ_6, SEQ_4, JORDAN3,
STRUCT_0, TOPREAL1, RFINSEQ, PRE_TOPC, TOPS_2, COMPTS_1, BORSUK_1,
RLVECT_1, RLTOPSP1, EUCLID, TREAL_1, METRIC_1, GOBOARD1, GOBOARD2,
MATRIX_0, TOPREAL4, GOBOARD5, FUNCT_4, FINSEQ_5, PCOMPS_1;
constructors FUNCT_4, REAL_1, SEQ_4, RCOMP_1, FINSEQ_4, RFINSEQ, NAT_D,
FINSEQ_5, TOPS_2, COMPTS_1, TREAL_1, TOPREAL4, GOBOARD2, GOBOARD5,
JORDAN3, GOBOARD1, CONVEX1, BINOP_2, PCOMPS_1, MONOID_0;
registrations FUNCT_1, RELSET_1, FUNCT_2, XREAL_0, MEMBERED, STRUCT_0,
PRE_TOPC, METRIC_1, BORSUK_1, EUCLID, TOPMETR, TOPREAL1, GOBOARD2,
GOBOARD5, VALUED_0, XXREAL_2, RLTOPSP1, SEQ_4, SPPOL_2, NAT_1, ORDINAL1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, JORDAN3, TOPREAL4, XBOOLE_0;
equalities XBOOLE_0, STRUCT_0, RELAT_1, RLTOPSP1, RLVECT_1;
expansions TARSKI, JORDAN3, XBOOLE_0;
theorems BORSUK_1, COMPTS_1, EUCLID, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2,
RELAT_1, JORDAN3, GOBOARD1, NAT_1, GOBOARD9, FUNCT_4, TOPMETR2, GOBOARD2,
PRE_TOPC, RCOMP_1, HEINE, PCOMPS_1, SPPOL_2, TARSKI, TOPMETR, TOPREAL1,
TOPREAL3, RFINSEQ, FINSEQ_5, GOBOARD5, GOBOARD7, FINSEQ_1, TOPS_2,
TREAL_1, JORDAN5A, ZFMISC_1, PARTFUN2, INT_1, RELSET_1,
FINSEQ_6, XBOOLE_0, XBOOLE_1, XCMPLX_1, FINSEQ_2, XREAL_1, XXREAL_0,
PARTFUN1, CARD_1, MATRIX_0, XXREAL_1, XXREAL_2, NAT_D, RLTOPSP1, SEQ_4,
RLVECT_1;
schemes NAT_1;
begin :: Preliminaries
theorem Th1:
for i1 being Nat st 1 <= i1 holds i1-'1<i1
proof
let i1 be Nat;
assume
A1: 1 <= i1;
i1 - 1 < i1 - 0 by XREAL_1:15;
hence thesis by A1,XREAL_1:233;
end;
theorem
for i, k being Nat holds i+1 <= k implies 1 <= k-'i
proof
let i, k be Nat;
assume i+1 <= k;
then i+1 -' i <= k -' i by NAT_D:42;
hence thesis by NAT_D:34;
end;
theorem
for i, k being Nat holds 1 <= i & 1 <= k implies (k-'i)+1 <= k
proof
let i, k be Nat;
assume that
A1: 1 <= i and
A2: 1 <= k;
(k-'i) <= k -' 1 by A1,NAT_D:41;
then (k-'i)+1 <= k -' 1+1 by XREAL_1:6;
hence thesis by A2,XREAL_1:235;
end;
Lm1: for r be Real st 0 <= r & r <= 1 holds 0 <= 1-r & 1-r <= 1
proof
let r be Real;
assume that
A1: 0 <= r and
A2: r <= 1;
A3: 1-1 <= 1-r by A2,XREAL_1:13;
1-r <= 1-0 by A1,XREAL_1:13;
hence thesis by A3;
end;
theorem
for r being Real st r in the carrier of I[01] holds
1 - r in the carrier of I[01]
proof
let r be Real;
assume
A1: r in the carrier of I[01];
then
A2: 0 <= r by BORSUK_1:43;
A3: r <= 1 by A1,BORSUK_1:43;
then
A4: 0 <= 1-r by A2,Lm1;
1-r <= 1 by A2,A3,Lm1;
hence thesis by A4,BORSUK_1:43;
end;
theorem
for p, q, p1 being Point of TOP-REAL 2 st p`2 <> q`2 & p1 in LSeg (p, q)
holds ( p1`2 = p`2 implies p1 = p )
proof
let p, q, p1 be Point of TOP-REAL 2;
assume that
A1: p`2 <> q`2 and
A2: p1 in LSeg (p, q);
assume
A3: p1`2 = p`2;
assume
A4: p1 <> p;
consider l1 be Real such that
A5: p1 = (1-l1)*p + l1*q and 0 <= l1
and l1 <= 1 by A2;
A6: (1-l1)*p + l1*q = |[ ((1-l1)*p)`1 + (l1*q)`1 , ((1-l1)*p)`2 + (l1*q)`2 ]|
by EUCLID:55;
A7: (1-l1)*p = |[ (1-l1)*p`1, (1-l1)*p`2 ]| by EUCLID:57;
A8: l1*q = |[ l1*q`1, l1*q`2 ]| by EUCLID:57;
p`2 = ( (1-l1)*p )`2 + ( l1*q )`2 by A3,A5,A6,EUCLID:52
.= (1-l1)*p`2 + (l1*q)`2 by A7,EUCLID:52
.= (1-l1)*p`2 + l1*q`2 by A8,EUCLID:52;
then (1 - (1-l1))*p`2 = l1*q`2;
then l1 = 0 by A1,XCMPLX_1:5;
then p1 = 1*p + 0.TOP-REAL 2 by A5,RLVECT_1:10
.= p + 0.TOP-REAL 2 by RLVECT_1:def 8
.= p by RLVECT_1:4;
hence thesis by A4;
end;
theorem
for p, q, p1 being Point of TOP-REAL 2 st p`1 <> q`1 & p1 in LSeg (p, q)
holds ( p1`1 = p`1 implies p1 = p )
proof
let p, q, p1 be Point of TOP-REAL 2;
assume that
A1: p`1 <> q`1 and
A2: p1 in LSeg (p, q);
assume
A3: p1`1 = p`1;
assume
A4: p1 <> p;
consider l1 be Real such that
A5: p1 = (1-l1)*p + l1*q and 0 <= l1
and l1 <= 1 by A2;
A6: (1-l1)*p + l1*q = |[ ((1-l1)*p)`1 + (l1*q)`1 , ((1-l1)*p)`2 + (l1*q)`2 ]|
by EUCLID:55;
A7: (1-l1)*p = |[ (1-l1)*p`1, (1-l1)*p`2 ]| by EUCLID:57;
A8: l1*q = |[ l1*q`1, l1*q`2 ]| by EUCLID:57;
p`1 = ( (1-l1)*p )`1 + ( l1*q )`1 by A3,A5,A6,EUCLID:52
.= (1-l1)*p`1 + (l1*q)`1 by A7,EUCLID:52
.= (1-l1)*p`1 + l1*q`1 by A8,EUCLID:52;
then (1 - (1-l1))*p`1 = l1*q`1;
then l1 = 0 by A1,XCMPLX_1:5;
then p1 = 1*p + 0.TOP-REAL 2 by A5,RLVECT_1:10
.= p + 0.TOP-REAL 2 by RLVECT_1:def 8
.= p by RLVECT_1:4;
hence thesis by A4;
end;
reconsider jj=1 as Real;
theorem Th7:
for f being FinSequence of TOP-REAL 2,
P being non empty Subset of TOP-REAL 2,
F being Function of I[01], (TOP-REAL 2) | P,
i being Nat st 1 <= i & i+1 <= len f & f is being_S-Seq &
P = L~f &
F is being_homeomorphism & F.0 = f/.1 & F.1 = f/.len f
ex p1, p2 being Real
st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 &
LSeg (f, i) = F.:[.p1, p2.] & F.p1 = f/.i & F.p2 = f/.(i+1)
proof
let f be FinSequence of TOP-REAL 2, P be non empty Subset of TOP-REAL 2,
Ff be Function of I[01], (TOP-REAL 2)|P, i be Nat;
assume that
A1: 1 <= i and
A2: i+1 <= len f and
A3: f is being_S-Seq and
A4: P = L~f and
A5: Ff is being_homeomorphism and
A6: Ff.0 = f/.1 and
A7: Ff.1 = f/.len f;
A8: f is one-to-one by A3;
A9: the carrier of Closed-Interval-TSpace(1/2,1) = [.1/2,1.] by TOPMETR:18;
A10: [#]Closed-Interval-TSpace(0, 1/2) = [.0,1/2.] by TOPMETR:18;
A11: [#]Closed-Interval-TSpace(1/2,1) = [.1/2,1.] by TOPMETR:18;
A12: len f >= 2 by A3,TOPREAL1:def 8;
deffunc Q(Nat) = L~(f|($1+2));
defpred ARC[Nat] means 1 <= $1 + 2 & $1 + 2 <= len f implies
ex NE being non empty Subset of TOP-REAL 2 st NE = Q($1) &
for j be Nat for F being Function of I[01], (TOP-REAL 2)|NE st
1 <= j & j+1 <= $1+2 & F is being_homeomorphism & F.0 = f/.1 &
F.1 = f/.($1+2)
ex p1, p2 be Real st p1 < p2 &
0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f, j) = F.:[.p1, p2.]
& F.p1 = f/.j & F.p2 = f/.(j+1);
reconsider h1 = len f - 2 as Element of NAT by A12,INT_1:5;
A13: f|(len f) = f|(Seg len f) by FINSEQ_1:def 16
.= f|(dom f) by FINSEQ_1:def 3
.= f by RELAT_1:68;
A14: ARC[0]
proof
assume that
A15: 1 <= 0 + 2 and
A16: 0 + 2 <= len f;
A17: 1 <= len (f|2) by A15,A16,FINSEQ_1:59;
A18: 2 <= len (f|2) by A16,FINSEQ_1:59;
then reconsider NE = Q(0) as non empty Subset of TOP-REAL 2
by TOPREAL1:23;
take NE;
thus NE = Q(0);
let j be Nat;
let F be Function of I[01], (TOP-REAL 2)|NE;
assume that
A19: 1 <= j and
A20: j+1 <= 0+2 and
A21: F is being_homeomorphism and
A22: F.0 = f/.1 and
A23: F.1 = f/.(0+2);
j <= 1+1-1 by A20,XREAL_1:19;
then
A24: j = 1 by A19,XXREAL_0:1;
A25: len (f|2) = 2 by A16,FINSEQ_1:59;
A26: 1 in dom (f|2) by A17,FINSEQ_3:25;
A27: 2 in dom (f|2) by A18,FINSEQ_3:25;
A28: (f|2)/.1 = (f|2).1 by A26,PARTFUN1:def 6;
A29: (f|2)/.2 = (f|2).2 by A27,PARTFUN1:def 6;
A30: (f|2)/.1 = f/.1 by A26,FINSEQ_4:70;
A31: 1 + 1 <= len f by A16;
A32: rng F = [#]((TOP-REAL 2)|NE) by A21,TOPS_2:def 5
.= L~(f|2) by PRE_TOPC:def 5
.= L~<* (f|2)/.1, (f|2)/.2 *> by A25,A28,A29,FINSEQ_1:44
.= LSeg ((f|2)/.1, (f|2)/.2) by SPPOL_2:21
.= LSeg (f/.1, f/.2) by A27,A30,FINSEQ_4:70
.= LSeg (f, 1) by A31,TOPREAL1:def 3;
take 0, jj;
thus thesis by A22,A23,A24,A32,BORSUK_1:40,RELSET_1:22;
end;
A33: for n being Nat st ARC[n] holds ARC[n+1]
proof
let n be Nat;
assume
A34: ARC[n];
assume that
A35: 1 <= n + 1 + 2 and
A36: n + 1 + 2 <= len f;
A37: 2 <= n + 2 by NAT_1:11;
n+2 <= n+2+1 by NAT_1:11;
then consider NE being non empty Subset of TOP-REAL 2 such that
A38: NE = Q(n) and
A39: for j be Nat for F being Function of I[01], (TOP-REAL 2)
|NE st 1 <= j & j+1 <= n+2 & F is being_homeomorphism & F.0 = f/.1 & F.1 = f/.(
n+2)
ex p1, p2 be Real
st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 &
LSeg (f, j) = F.:[.p1, p2.] & F.p1 = f/.j & F.p2 = f/.(j+1)
by A34,A36,A37,XXREAL_0:2;
A40: len (f|(n+1+2)) = n+1+2 by A36,FINSEQ_1:59;
A41: n + 1 + 2 = n + 2 + 1;
A42: 1 <= n + 1 + 1 by NAT_1:11;
A43: n + 1 + 1 <= n + 2 + 1 by NAT_1:11;
then
A44: n + 1 + 1 <= len f by A36,XXREAL_0:2;
A45: n+2 <= len f by A36,A43,XXREAL_0:2;
A46: n+2 in dom (f|(n+3)) by A40,A42,A43,FINSEQ_3:25;
then
A47: f/.(n+2) = (f|(n+3))/.(n+2) by FINSEQ_4:70;
reconsider NE1 = Q(n+1) as non empty Subset of TOP-REAL 2
by A40,NAT_1:11,TOPREAL1:23;
take NE1;
thus NE1 = Q(n+1);
let j be Nat, G be Function of I[01], (TOP-REAL 2)|NE1;
assume that
A48: 1 <= j and
A49: j+1 <= n+1+2 and
A50: G is being_homeomorphism and
A51: G.0 = f/.1 and
A52: G.1 = f/.(n+1+2);
A53: G is one-to-one by A50,TOPS_2:def 5;
A54: rng G = [#]((TOP-REAL 2) | Q(n+1)) by A50,TOPS_2:def 5;
A55: dom G = [#]I[01] by A50,TOPS_2:def 5;
A56: rng G = L~(f|(n+3)) by A54,PRE_TOPC:def 5;
set pp = G".(f/.(n+2));
G is onto by A54,FUNCT_2:def 3;
then
A57: pp = (G qua Function)".(f/.(n+2)) by A53,TOPS_2:def 4;
A58: n+2 <= len (f|(n+2)) by A36,A43,FINSEQ_1:59,XXREAL_0:2;
A59: 1 <= len (f|(n+2)) by A36,A42,A43,FINSEQ_1:59,XXREAL_0:2;
A60: n+2 in dom (f|(n+2)) by A42,A58,FINSEQ_3:25;
A61: 1 in dom (f|(n+2)) by A59,FINSEQ_3:25;
A62: f/.(n+2) in rng G by A40,A46,A47,A56,GOBOARD1:1,NAT_1:11;
then
A63: pp in dom G by A53,A57,FUNCT_1:32;
A64: f/.(n+2) = G.pp by A53,A57,A62,FUNCT_1:32;
reconsider pp as Real;
A65: n + 1 + 1 <> n + 2 + 1;
A66: n+2 <> n+3;
A67: n+2 in dom f by A42,A45,FINSEQ_3:25;
A68: n+3 in dom f by A35,A36,FINSEQ_3:25;
A69: 1 <> pp
proof
assume pp = 1;
then f/.(n+2) = f/.(n+1+2) by A52,A53,A57,A62,FUNCT_1:32;
hence thesis by A8,A66,A67,A68,PARTFUN2:10;
end;
A70: 0 <= pp by A63,BORSUK_1:43;
pp <= 1 by A63,BORSUK_1:43;
then
A71: pp < 1 by A69,XXREAL_0:1;
set pn = f/.(n+2), pn1 = f/.(n+2+1);
A72: pn = (f|(n+2))/.(n+2) by A60,FINSEQ_4:70;
A73: (f|(n+2))/.1 = f/.1 by A61,FINSEQ_4:70;
A74: len (f|(n+2)) = n+2 by A36,A43,FINSEQ_1:59,XXREAL_0:2;
f|(n+2) is being_S-Seq by A3,JORDAN3:4,NAT_1:11;
then NE is_an_arc_of (f|(n+2))/.1, pn by A38,A72,A74,TOPREAL1:25;
then consider F be Function of I[01], (TOP-REAL 2)|NE such that
A75: F is being_homeomorphism and
A76: F.0 = f/.1 and
A77: F.1 = pn by A73,TOPREAL1:def 1;
A78: n + 1 + 1 in dom f by A42,A44,FINSEQ_3:25;
n + 2 + 1 in dom f by A35,A36,FINSEQ_3:25;
then LSeg(pn, pn1) is_an_arc_of pn, pn1 by A8,A65,A78,PARTFUN2:10
,TOPREAL1:9;
then consider F9 be Function of I[01], (TOP-REAL 2)|LSeg(pn, pn1) such that
A79: F9 is being_homeomorphism and
A80: F9.0 = pn and
A81: F9.1 = pn1 by TOPREAL1:def 1;
set Ex1 = P[01]( 0, 1/2, (#)(0,1),(0,1)(#) ),
Ex2 = P[01]( 1/2, 1, (#)(0,1),(0,1)(#) );
set F1 = F * Ex1, F19 = F9 * Ex2;
A82: Ex1 is being_homeomorphism by TREAL_1:17;
A83: Ex2 is being_homeomorphism by TREAL_1:17;
A84: dom Ex1 = [#]Closed-Interval-TSpace(0,1/2) by A82,TOPS_2:def 5;
then
A85: dom Ex1 = [.0,1/2.] by TOPMETR:18;
dom F = [#]I[01] by A75,TOPS_2:def 5;
then
A86: rng Ex1 = dom F by A82,TOPMETR:20,TOPS_2:def 5;
then rng F1 = rng F by RELAT_1:28;
then rng F1 = [#] ((TOP-REAL 2) | NE) by A75,TOPS_2:def 5;
then
A87: rng F1 = Q(n) by A38,PRE_TOPC:def 5;
dom F1 = the carrier of Closed-Interval-TSpace(0, 1/2) by A84,A86,
RELAT_1:27;
then reconsider F1 as Function
of Closed-Interval-TSpace (0,1/2), (TOP-REAL 2)|NE by FUNCT_2:def 1;
A88: F1 is being_homeomorphism by A75,A82,TOPMETR:20,TOPS_2:57;
then
A89: rng F1 = [#]((TOP-REAL 2)|NE) by TOPS_2:def 5
.= Q(n) by A38,PRE_TOPC:def 5;
A90: dom Ex2 = [#]Closed-Interval-TSpace(1/2, 1) by A83,TOPS_2:def 5;
dom F9 = [#]I[01] by A79,TOPS_2:def 5;
then
A91: rng Ex2 = dom F9 by A83,TOPMETR:20,TOPS_2:def 5;
then dom F19 = the carrier of Closed-Interval-TSpace(1/2, 1) by A90,
RELAT_1:27;
then reconsider F19 as Function of Closed-Interval-TSpace (1/2,1),
(TOP-REAL 2)|LSeg(pn, pn1) by FUNCT_2:def 1;
A92: F19 is being_homeomorphism by A79,A83,TOPMETR:20,TOPS_2:57;
then
A93: rng F19 = [#]((TOP-REAL 2)|LSeg(pn, pn1)) by TOPS_2:def 5
.= LSeg(pn, pn1) by PRE_TOPC:def 5;
set FF = F1 +* F19;
reconsider T1 = Closed-Interval-TSpace(0,1/2),
T2 = Closed-Interval-TSpace(1/2, 1) as SubSpace of I[01]
by TOPMETR:20,TREAL_1:3;
A94: Q(n+1) = Q(n) \/ LSeg(pn, pn1) by A67,A68,TOPREAL3:38;
A95: the carrier of ((TOP-REAL 2)|Q(n+1)) = [#]((TOP-REAL 2)|Q(n+1))
.= Q(n+1) by PRE_TOPC:def 5;
dom F1 = the carrier of T1 by A84,A86,RELAT_1:27;
then reconsider g11 = F1 as Function
of T1, ((TOP-REAL 2)|NE1) by A87,A94,A95,RELSET_1:4,XBOOLE_1:7;
dom F19 = the carrier of T2 by A90,A91,RELAT_1:27;
then reconsider g22 = F19 as Function
of T2, ((TOP-REAL 2)|NE1) by A93,A94,A95,RELSET_1:4,XBOOLE_1:7;
A96: [.0,1/2.] = dom F1 by A10,A88,TOPS_2:def 5;
A97: [.1/2, 1.] = dom F19 by A11,A92,TOPS_2:def 5;
A98: 1/2 in { l where l is Real: 0 <= l & l <= 1/2 };
A99: 1/2 in { l where l is Real: 1/2 <= l & l <= 1 };
A100: 1/2 in dom F1 by A96,A98,RCOMP_1:def 1;
A101: 1/2 in dom F19 by A97,A99,RCOMP_1:def 1;
A102: dom FF = [.0,1/2.] \/ [.1/2,1.] by A96,A97,FUNCT_4:def 1
.= [.0,1.] by XXREAL_1:174;
A103: I[01] is compact by HEINE:4,TOPMETR:20;
A104: (TOP-REAL 2)|NE1 is T_2 by TOPMETR:2;
A105: Ex1.(1/2) = Ex1.(0,1/2)(#) by TREAL_1:def 2
.= (0,1)(#) by TREAL_1:13
.= 1 by TREAL_1:def 2;
A106: Ex2.(1/2) = Ex2.(#)(1/2,1) by TREAL_1:def 1
.= (#)(0,1) by TREAL_1:13
.= 0 by TREAL_1:def 1;
A107: F1.(1/2) = f/.(n+2) by A77,A100,A105,FUNCT_1:12;
A108: F19.(1/2) = f/.(n+2) by A80,A101,A106,FUNCT_1:12;
A109: [.0,1/2.] /\ [.1/2,1.] = [.1/2,1/2.] by XXREAL_1:143;
then
A110: dom F1 /\ dom F19 = {1/2} by A96,A97,XXREAL_1:17;
A111: for x being set holds x in Q(n) /\ LSeg(pn,pn1) iff x = pn
proof
let x be set;
thus x in Q(n) /\ LSeg(pn,pn1) implies x = pn
proof
assume
A112: x in Q(n) /\ LSeg(pn,pn1);
then
A113: x in LSeg(pn,pn1) by XBOOLE_0:def 4;
x in Q(n) by A112,XBOOLE_0:def 4;
then x in union { LSeg(f|(n+2),k) where k is Nat :
1 <= k & k+1 <= len(f|(n+2)) } by TOPREAL1:def 4;
then consider X being set such that
A114: x in X and
A115: X in { LSeg(f|(n+2),k) where k is Nat :
1 <= k & k+1 <= len(f|(n+2)) } by TARSKI:def 4;
consider k be Nat such that
A116: X = LSeg(f|(n+2),k) and
A117: 1 <= k and
A118: k+1 <= len(f|(n+2)) by A115;
A119: len(f|(n+2)) = n+(1+1) by A36,A43,FINSEQ_1:59,XXREAL_0:2;
A120: len(f|(n+2)) = n+1+1 by A36,A43,FINSEQ_1:59,XXREAL_0:2;
then
A121: k <= n+1 by A118,XREAL_1:6;
A122: f is s.n.c. by A3;
A123: f is unfolded by A3;
now
assume
A124: k < n+1;
A125: 1 <= 1+k by NAT_1:11;
A126: k+1 <= len f by A44,A118,A120,XXREAL_0:2;
A127: k+1 < n+1+1 by A124,XREAL_1:6;
set p19 = f/.k, p29 = f/.(k+1);
n+1 <= n+1+1 by NAT_1:11;
then k <= n+2 by A124,XXREAL_0:2;
then
A128: k in Seg len(f|(n+2)) by A117,A119,FINSEQ_1:1;
A129: k+1 in Seg len(f|(n+2)) by A118,A125,FINSEQ_1:1;
A130: k in dom(f|(n+2)) by A128,FINSEQ_1:def 3;
A131: k+1 in dom(f|(n+2)) by A129,FINSEQ_1:def 3;
A132: (f|(n+2))/.k = p19 by A130,FINSEQ_4:70;
A133: (f|(n+2))/.(k+1) = p29 by A131,FINSEQ_4:70;
A134: LSeg(f,k) = LSeg(p19,p29) by A117,A126,TOPREAL1:def 3
.= LSeg(f|(n+2),k) by A117,A118,A132,A133,TOPREAL1:def 3;
LSeg(f,n+2) = LSeg(pn,pn1) by A36,A42,TOPREAL1:def 3;
then LSeg(f|(n+2),k) misses LSeg(pn,pn1)
by A122,A127,A134,TOPREAL1:def 7;
then LSeg(f|(n+2),k) /\ LSeg(pn,pn1) = {};
hence contradiction by A113,A114,A116,XBOOLE_0:def 4;
end;
then
A135: k = n + 1 by A121,XXREAL_0:1;
A136: 1 <= n+1 by A117,A121,XXREAL_0:2;
A137: n+1+1 <= len f by A36,A43,XXREAL_0:2;
set p19 = f/.(n+1), p29 = f/.(n+1+1);
A138: n+1 <= n+1+1 by NAT_1:11;
A139: 1 <= 1+n by NAT_1:11;
A140: 1 <= 1+(n+1) by NAT_1:11;
A141: n+1 in Seg len(f|(n+2)) by A119,A138,A139,FINSEQ_1:1;
A142: n+1+1 in Seg len(f|(n+2)) by A119,A140,FINSEQ_1:1;
A143: n+1 in dom(f|(n+2)) by A141,FINSEQ_1:def 3;
A144: n+1+1 in dom(f|(n+2)) by A142,FINSEQ_1:def 3;
A145: (f|(n+2))/.(n+1) = p19 by A143,FINSEQ_4:70;
A146: (f|(n+2))/.(n+1+1) = p29 by A144,FINSEQ_4:70;
A147: LSeg(f,n+1) = LSeg(p19,p29) by A136,A137,TOPREAL1:def 3
.= LSeg(f|(n+2),n+1) by A119,A139,A145,A146,TOPREAL1:def 3;
LSeg(pn,pn1) = LSeg(f,n+1+1) by A36,A42,TOPREAL1:def 3;
then
A148: x in LSeg(f,n+1) /\ LSeg(f,n+1+1)
by A113,A114,A116,A135,A147,XBOOLE_0:def 4;
1 <= n+1 by NAT_1:11;
then LSeg(f,n+1) /\ LSeg(f,n+1+1) = {f/.(n+1+1)}
by A36,A123,TOPREAL1:def 6;
hence thesis by A148,TARSKI:def 1;
end;
assume
A149: x = pn;
then
A150: x in LSeg(pn,pn1) by RLTOPSP1:68;
A151: len(f|(n+2)) = n+2 by A36,A43,FINSEQ_1:59,XXREAL_0:2;
then
A152: dom(f|(n+2)) = Seg(n+2) by FINSEQ_1:def 3;
n + 2 in Seg(n+2) by A42,FINSEQ_1:1;
then
A153: x = (f|(n+2))/.(n+1+1) by A149,A152,FINSEQ_4:70;
1 <= n+1 by NAT_1:11;
then
A154: x in LSeg(f|(n+2),n+1) by A151,A153,TOPREAL1:21;
A155: 1 <= n+1 by NAT_1:11;
n+1+1 <= len(f|(n+2)) by A36,A43,FINSEQ_1:59,XXREAL_0:2;
then LSeg(f|(n+2),n+1) in {LSeg(f|(n+2),k) where k is Nat :
1 <= k & k+1 <= len(f|(n+2))} by A155;
then x in union {LSeg(f|(n+2),k) where k is Nat :
1 <= k & k+1 <= len(f|(n+2))} by A154,TARSKI:def 4;
then x in Q(n) by TOPREAL1:def 4;
hence thesis by A150,XBOOLE_0:def 4;
end;
f/.(n+2) in rng F19 by A101,A108,FUNCT_1:def 3;
then
A156: {f/.(n+2)} c= rng F19 by ZFMISC_1:31;
A157: F1.:(dom F1 /\ dom F19) = Im(F1,1/2) by A96,A97,A109,XXREAL_1:17
.= {f/.(n+2)} by A100,A107,FUNCT_1:59;
then
A158: rng FF = Q(n) \/ LSeg(pn, pn1) by A89,A93,A156,TOPMETR2:2;
then
A159: rng FF = [#]((TOP-REAL 2)|Q(n+1)) by A67,A68,A95,TOPREAL3:38;
rng FF c= the carrier of ((TOP-REAL 2)|Q(n+1)) by A89,A93,A94,A95,A156,A157
,TOPMETR2:2;
then reconsider FF as Function of I[01], (TOP-REAL 2)|NE1 by A102,
BORSUK_1:40,FUNCT_2:2;
A160: rng Ex1 = [#] Closed-Interval-TSpace(0,1) by A82,TOPS_2:def 5;
A161: 0 in { l where l is Real: 0 <= l & l <= 1/2 };
A162: 1/2 in { l where l is Real: 0 <= l & l <= 1/2 };
A163: 0 in dom Ex1 by A85,A161,RCOMP_1:def 1;
A164: 1/2 in dom Ex1 by A85,A162,RCOMP_1:def 1;
A165: Ex1 is one-to-one continuous by A82,TOPS_2:def 5;
A166: Ex1.0 = Ex1.(#)(0,1/2) by TREAL_1:def 1
.= (#)(0,1) by TREAL_1:13
.= 0 by TREAL_1:def 1;
A167: Ex1 is onto by A160,FUNCT_2:def 3;
then
A168: Ex1".0 = (Ex1 qua Function)".0 by A165,TOPS_2:def 4
.= 0 by A163,A165,A166,FUNCT_1:32;
A169: Ex2.(1/2) = Ex2.(#)(1/2,1) by TREAL_1:def 1
.= (#)(0,1) by TREAL_1:13
.= 0 by TREAL_1:def 1;
A170: Ex1".1 = (Ex1 qua Function)".1 by A167,A165,TOPS_2:def 4
.= 1/2 by A105,A164,A165,FUNCT_1:32;
A171: Ex2.1 = Ex2.(1/2,1)(#) by TREAL_1:def 2
.= (0,1)(#) by TREAL_1:13
.= 1 by TREAL_1:def 2;
A172: LSeg(pn, pn1) = F19.:[.1/2,1.] by A9,A93,RELSET_1:22;
A173: FF.(1/2) = f/.(n+2) by A101,A108,FUNCT_4:13;
A174: for x be set st x in [.0,1/2.] & x <> 1/2 holds not x in dom F19
proof
let x be set;
assume that
A175: x in [.0,1/2.] and
A176: x <> 1/2;
assume x in dom F19;
then x in dom F1 /\ dom F19 by A96,A175,XBOOLE_0:def 4;
hence thesis by A110,A176,TARSKI:def 1;
end;
A177: FF.:[.1/2,1.] c= F19.:[.1/2,1.]
proof
let a be object;
assume a in FF.:[.1/2,1.];
then consider x be object such that
x in dom FF and
A178: x in [.1/2,1.] and
A179: a = FF.x by FUNCT_1:def 6;
FF.x = F19.x by A97,A178,FUNCT_4:13;
hence thesis by A97,A178,A179,FUNCT_1:def 6;
end;
F19.:[.1/2,1.] c= FF.:[.1/2,1.]
proof
let a be object;
assume a in F19.:[.1/2,1.];
then consider x be object such that
A180: x in dom F19 and
A181: x in [.1/2,1.] and
A182: a = F19.x by FUNCT_1:def 6;
A183: x in dom FF by A180,FUNCT_4:12;
a = FF.x by A180,A182,FUNCT_4:13;
hence thesis by A181,A183,FUNCT_1:def 6;
end;
then
A184: FF.:[.1/2,1.] = F19.:[.1/2,1.] by A177;
set GF = G" * FF;
reconsider GF as Function of I[01],I[01];
A185: 0 in dom FF by A102,BORSUK_1:40,43;
A186: 1 in dom FF by A102,BORSUK_1:40,43;
0 in { l where l is Real: 0 <= l & l <= 1/2 };
then 0 in [.0,1/2.] by RCOMP_1:def 1;
then
A187: FF.0 = F1.0 by A174,FUNCT_4:11
.= f/.1 by A76,A163,A166,FUNCT_1:13;
1 in { l where l is Real: 1/2 <= l & l <= 1 };
then
A188: 1 in dom F19 by A97,RCOMP_1:def 1;
then
A189: FF.1 = F19.1 by FUNCT_4:13
.= pn1 by A81,A171,A188,FUNCT_1:12;
A190: 0 in dom G by A55,BORSUK_1:43;
A191: G is onto by A54,FUNCT_2:def 3;
then
A192: G".(f/.1) = (G qua Function)".(f/.1) by A53,TOPS_2:def 4
.= 0 by A51,A53,A190,FUNCT_1:32;
then
A193: GF.0 = 0 by A185,A187,FUNCT_1:13;
A194: 1 in dom G by A55,BORSUK_1:43;
A195: G".pn1 = (G qua Function)".pn1 by A191,A53,TOPS_2:def 4
.= 1 by A52,A53,A194,FUNCT_1:32;
then
A196: GF.1 = 1 by A186,A189,FUNCT_1:13;
reconsider ppp = 1/2 as Point of I[01] by BORSUK_1:43;
TopSpaceMetr RealSpace is T_2 by PCOMPS_1:34;
then
A197: I[01] is T_2 by TOPMETR:2,20,def 6;
A198: T1 is compact by HEINE:4;
A199: T2 is compact by HEINE:4;
A200: F1 is continuous by A88,TOPS_2:def 5;
A201: F19 is continuous by A92,TOPS_2:def 5;
A202: (TOP-REAL 2)|NE is SubSpace of ((TOP-REAL 2)|NE1) by A38,A94,TOPMETR:4;
A203: (TOP-REAL 2)|LSeg(pn, pn1) is SubSpace of (TOP-REAL 2)|NE1 by A94,
TOPMETR:4;
A204: g11 is continuous by A200,A202,PRE_TOPC:26;
A205: g22 is continuous by A201,A203,PRE_TOPC:26;
A206: [#] T1 = [.0,1/2.] by TOPMETR:18;
A207: [#] T2 = [.1/2,1.] by TOPMETR:18;
then
A208: ([#] T1) \/ ([#]T2) = [#] I[01] by A206,BORSUK_1:40,XXREAL_1:174;
([#] T1) /\ ([#]T2) = {ppp} by A206,A207,XXREAL_1:418;
then reconsider FF as continuous Function of I[01],(TOP-REAL 2)|NE1
by A107,A108,A197,A198,A199,A204,A205,A208,COMPTS_1:20;
A209: F1 is one-to-one by A88,TOPS_2:def 5;
A210: F19 is one-to-one by A92,TOPS_2:def 5;
for x1,x2 be set st x1 in dom F19 & x2 in dom F1 \ dom F19 holds
F19.x1 <> F1.x2
proof
let x1,x2 be set;
assume that
A211: x1 in dom F19 and
A212: x2 in dom F1 \ dom F19;
assume
A213: F19.x1 = F1.x2;
A214: F19.x1 in LSeg(pn, pn1) by A93,A211,FUNCT_2:4;
A215: x2 in dom F1 by A212,XBOOLE_0:def 5;
A216: not x2 in dom F19 by A212,XBOOLE_0:def 5;
F1.x2 in NE by A38,A89,A212,FUNCT_2:4;
then F1.x2 in NE /\ LSeg(pn, pn1) by A213,A214,XBOOLE_0:def 4;
then F1.x2 = pn by A38,A111;
hence thesis by A100,A101,A107,A209,A215,A216,FUNCT_1:def 4;
end;
then
A217: FF is one-to-one by A209,A210,TOPMETR2:1;
A218: G" is being_homeomorphism by A50,TOPS_2:56;
FF is being_homeomorphism by A103,A104,A159,A217,COMPTS_1:17;
then
A219: GF is being_homeomorphism by A218,TOPS_2:57;
then
A220: GF is continuous by TOPS_2:def 5;
A221: dom GF = [#]I[01] by A219,TOPS_2:def 5;
A222: rng GF = [#]I[01] by A219,TOPS_2:def 5;
A223: GF is one-to-one by A219,TOPS_2:def 5;
then
A224: dom (GF") = [#]I[01] by A222,TOPS_2:49;
A225: rng G = [#]((TOP-REAL 2)|Q(n+1)) by A50,TOPS_2:def 5
.= rng FF by A67,A68,A95,A158,TOPREAL3:38;
A226: G * (G" * FF) = (FF qua Relation) * ( G * (G" qua Function) )
by RELAT_1:36
.= id rng G * FF by A53,A54,TOPS_2:52
.= FF by A225,RELAT_1:54;
A227: 1/2 in dom GF by A221,BORSUK_1:43;
then
A228: GF.(1/2) in rng GF by FUNCT_1:def 3;
A229: GF.(1/2) = G".(FF.(1/2)) by A227,FUNCT_1:12
.= pp by A101,A108,FUNCT_4:13;
A230: [.pp,1.] c= GF.:[.1/2,1.]
proof
let a be object;
assume a in [.pp,1.];
then a in { l where l is Real: pp <= l & l <= 1 }
by RCOMP_1:def 1;
then consider l1 be Real such that
A231: l1 = a and
A232: pp <= l1 and
A233: l1 <= 1;
A234: 0 <= pp by A228,A229,BORSUK_1:43;
set cos = GF".l1;
l1 in dom (GF") by A224,A232,A233,A234,BORSUK_1:43;
then
A235: cos in rng (GF") by FUNCT_1:def 3;
A236: l1 in rng GF by A222,A232,A233,A234,BORSUK_1:43;
GF is onto by A222,FUNCT_2:def 3;
then
A237: GF.cos = GF.((GF qua Function)".l1) by A223,TOPS_2:def 4
.= l1 by A223,A236,FUNCT_1:35;
reconsider cos as Real;
reconsider A3 = cos, A4 = 1, A5 = 1/2 as Point of I[01]
by A235,BORSUK_1:43;
reconsider A1 = GF.A3, A2 = GF.A4 as Point of I[01];
reconsider Fhc = A1, Fh0 = A2, Fh12 = GF.A5 as Real;
A238: cos <= 1
proof
assume cos > 1;
then Fhc > Fh0 by A193,A196,A220,A223,JORDAN5A:16;
hence thesis by A102,A189,A195,A233,A237,BORSUK_1:40,FUNCT_1:13;
end;
cos >= 1/2
proof
assume cos < 1/2;
then Fhc < Fh12 by A193,A196,A220,A223,JORDAN5A:16;
hence thesis by A102,A173,A232,A237,BORSUK_1:40,FUNCT_1:13;
end;
then cos in { l where l is Real: 1/2 <= l & l <= 1 } by A238;
then cos in [.1/2,1.] by RCOMP_1:def 1;
hence thesis by A221,A231,A235,A237,FUNCT_1:def 6;
end;
GF.:[.1/2,1.] c= [.pp,1.]
proof
let a be object;
assume a in GF.:[.1/2,1.];
then consider x be object such that
x in dom GF and
A239: x in [.1/2,1.] and
A240: a = GF.x by FUNCT_1:def 6;
x in { l where l is Real: 1/2 <= l & l <= 1 }
by A239,RCOMP_1:def 1;
then consider l1 be Real such that
A241: l1 = x and
A242: 1/2 <= l1 and
A243: l1 <= 1;
reconsider ll = l1, pol = 1/2 as Point of I[01] by A242,A243,BORSUK_1:43;
reconsider A1 = GF.1[01], A2 = GF.ll, A3 = GF.pol as Point of I[01];
reconsider A4 = A1, A5 = A2, A6 = A3 as Real;
A244: A4 >= A5
proof
per cases;
suppose 1 <> l1;
then 1 > l1 by A243,XXREAL_0:1;
hence thesis by A193,A196,A220,A223,BORSUK_1:def 15,JORDAN5A:16;
end;
suppose 1 = l1;
hence thesis by BORSUK_1:def 15;
end;
end;
A5 >= A6
proof
per cases;
suppose l1 <> 1/2;
then l1 > 1/2 by A242,XXREAL_0:1;
hence thesis by A193,A196,A220,A223,JORDAN5A:16;
end;
suppose l1 = 1/2;
hence thesis;
end;
end;
then A5 in { l where l is Real: pp <= l & l <= 1 }
by A196,A229,A244,BORSUK_1:def 15;
hence thesis by A240,A241,RCOMP_1:def 1;
end;
then [.pp,1.] = GF.:[.1/2,1.] by A230;
then
A245: G.:[.pp,1.] = LSeg (pn, pn1) by A172,A184,A226,RELAT_1:126;
ex p1, p2 be Real st p1 < p2 &
0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f, j) = G.:[.p1, p2.]
& G.p1 = f/.j & G.p2 = f/.(j+1)
proof
per cases;
suppose j+1 <= n+2;
then consider r1, r2 be Real such that
A246: r1 < r2 and
A247: 0 <= r1 and
A248: r1 <= 1 and 0 <= r2 and
A249: r2 <= 1 and
A250: LSeg (f, j) = F.:[.r1, r2.] and
A251: F.r1 = f/.j and
A252: F.r2 = f/.(j+1) by A39,A48,A75,A76,A77;
set f1 = Ex1".r1, f2 = Ex1".r2;
A253: Ex1 is continuous one-to-one by A82,TOPS_2:def 5;
A254: dom Ex1 = [#]Closed-Interval-TSpace(0,1/2) by A82,TOPS_2:def 5;
A255: rng Ex1 = [#]Closed-Interval-TSpace(0,1) by A82,TOPS_2:def 5;
then
A256: Ex1 is onto by FUNCT_2:def 3;
then
A257: f1 = (Ex1 qua Function)".r1 by A253,TOPS_2:def 4;
A258: f2 = (Ex1 qua Function)".r2 by A253,A256,TOPS_2:def 4;
A259: rng Ex1 = [#]I[01] by A82,TOPMETR:20,TOPS_2:def 5
.= the carrier of I[01];
then
A260: r1 in rng Ex1 by A247,A248,BORSUK_1:43;
A261: r2 in rng Ex1 by A246,A247,A249,A259,BORSUK_1:43;
A262: f1 in the carrier of Closed-Interval-TSpace(0,1/2) by A253,A254,A257
,A260,FUNCT_1:32;
A263: f2 in the carrier of Closed-Interval-TSpace(0,1/2) by A253,A254,A258
,A261,FUNCT_1:32;
A264: f1 in [.0,1/2.] by A262,TOPMETR:18;
A265: f2 in [.0,1/2.] by A263,TOPMETR:18;
reconsider f1, f2 as Real;
reconsider r19 = r1, r29 = r2 as Point of Closed-Interval-TSpace(0,1)
by A246,A247,A248,A249,BORSUK_1:43,TOPMETR:20;
A266: Ex1" is being_homeomorphism by A82,TOPS_2:56;
A267: f1 = Ex1".r19;
A268: f2 = Ex1".r29;
A269: Ex1" is continuous one-to-one by A266,TOPS_2:def 5;
then
A270: f1 < f2 by A168,A170,A246,A267,A268,JORDAN5A:15;
A271: [.0,1/2.] c= [.0,1.] by XXREAL_1:34;
A272: r1 = Ex1.f1 by A253,A257,A260,FUNCT_1:32;
A273: r2 = Ex1.f2 by A253,A258,A261,FUNCT_1:32;
A274: f1 in { l where l is Real: 0 <= l & l <= 1/2 }
by A264,RCOMP_1:def 1;
A275: f2 in { l where l is Real: 0 <= l & l <= 1/2 }
by A265,RCOMP_1:def 1;
A276: ex ff1 be Real st ( ff1 = f1)&( 0 <= ff1)&( ff1 <= 1/2) by A274;
ex ff2 be Real st ( ff2 = f2)&( 0 <= ff2)&( ff2 <= 1/2) by A275;
then
A277: Ex1.:
[.f1,f2.] = [.r1,r2.] by A82,A105,A166,A270,A272,A273,A276,JORDAN5A:20;
A278: F1.:[.f1,f2.] c= FF.:[.f1, f2.]
proof
let a be object;
assume a in F1.:[.f1, f2.];
then consider x be object such that
A279: x in dom F1 and
A280: x in [.f1, f2.] and
A281: a = F1.x by FUNCT_1:def 6;
A282: now per cases;
suppose x <> 1/2;
hence FF.x = F1.x by A10,A174,A279,FUNCT_4:11;
end;
suppose x = 1/2;
hence FF.x = F1.x by A101,A107,A108,FUNCT_4:13;
end;
end;
x in dom FF by A279,FUNCT_4:12;
hence thesis by A280,A281,A282,FUNCT_1:def 6;
end;
FF.:[.f1,f2.] c= F1.:[.f1, f2.]
proof
let a be object;
assume a in FF.:[.f1, f2.];
then consider x be object such that
x in dom FF and
A283: x in [.f1, f2.] and
A284: a = FF.x by FUNCT_1:def 6;
A285: [.f1, f2.] c= [.0,1/2.] by A264,A265,XXREAL_2:def 12;
now per cases;
suppose x <> 1/2;
hence FF.x = F1.x by A174,A283,A285,FUNCT_4:11;
end;
suppose x = 1/2;
hence FF.x = F1.x by A101,A107,A108,FUNCT_4:13;
end;
end;
hence thesis by A96,A283,A284,A285,FUNCT_1:def 6;
end;
then F1.:[.f1,f2.] = FF.:[.f1, f2.] by A278;
then
A286: F.:[.r1, r2.] = FF.:[.f1, f2.] by A277,RELAT_1:126;
set e1 = GF.f1, e2 = GF.f2;
A287: e1 in the carrier of I[01] by A264,A271,BORSUK_1:40,FUNCT_2:5;
A288: e2 in the carrier of I[01] by A265,A271,BORSUK_1:40,FUNCT_2:5;
A289: e1 in { l where l is Real: 0 <= l & l <= 1 }
by A287,BORSUK_1:40,RCOMP_1:def 1;
A290: e2 in { l where l is Real : 0 <= l & l <= 1 }
by A288,BORSUK_1:40,RCOMP_1:def 1;
consider l1 be Real such that
A291: l1 = e1 and
A292: 0 <= l1 and
A293: l1 <= 1 by A289;
consider l2 be Real such that
A294: l2 = e2 and 0 <= l2 and
A295: l2 <= 1 by A290;
reconsider f19 = f1, f29 = f2 as Point of I[01] by A264,A265,A271,BORSUK_1:40;
A296: GF.0 = 0 by A185,A187,A192,FUNCT_1:13;
A297: GF.1 = 1 by A186,A189,A195,FUNCT_1:13;
A298: l1 = GF.f19 by A291;
l2 = GF.f29 by A294;
then
A299: l1 < l2 by A220,A223,A270,A296,A297,A298,JORDAN5A:16;
A300: f1 < f2 by A168,A170,A246,A267,A268,A269,JORDAN5A:15;
A301: 0 <= f1 by A264,A271,BORSUK_1:40,43;
f2 <= 1 by A265,A271,BORSUK_1:40,43;
then
A302: G.:[.l1, l2.] = G.:(GF.:[.f1, f2.])
by A193,A196,A219,A291,A294,A300,A301,JORDAN5A:20,TOPMETR:20
.= FF.:[.f1, f2.] by A226,RELAT_1:126;
A303: FF.f19 = F.r19
proof
per cases;
suppose
A304: f19 = 1/2;
then FF.f19 = F19.(1/2) by A101,FUNCT_4:13
.= F9.0 by A101,A169,FUNCT_1:12
.= F.r19 by A77,A80,A105,A253,A255,A257,A304,FUNCT_1:32;
hence thesis;
end;
suppose f19 <> 1/2;
then FF.f19 = F1.f19 by A174,A264,FUNCT_4:11
.= F.(Ex1.f19) by A85,A264,FUNCT_1:13
.= F.r19 by A253,A255,A257,FUNCT_1:32;
hence thesis;
end;
end;
A305: FF.f29 = F.r29
proof
per cases;
suppose
A306: f29 = 1/2;
then FF.f29 = F19.(1/2) by A101,FUNCT_4:13
.= F9.0 by A101,A169,FUNCT_1:12
.= F.r29 by A77,A80,A105,A253,A255,A258,A306,FUNCT_1:32;
hence thesis;
end;
suppose f29 <> 1/2;
then FF.f29 = F1.f29 by A174,A265,FUNCT_4:11
.= F.(Ex1.f29) by A85,A265,FUNCT_1:13
.= F.r29 by A253,A255,A258,FUNCT_1:32;
hence thesis;
end;
end;
A307: G.l1 = f/.j by A102,A226,A251,A291,A303,BORSUK_1:40,FUNCT_1:12;
G.l2 = f/.(j+1) by A102,A226,A252,A294,A305,BORSUK_1:40,FUNCT_1:12;
hence thesis by A250,A286,A292,A293,A295,A299,A302,A307;
end;
suppose j+1 > n+2;
then
A308: j+1 = n+3 by A41,A49,NAT_1:9;
then LSeg(f,j) = LSeg (pn, pn1) by A36,A42,TOPREAL1:def 3;
hence thesis by A52,A64,A70,A71,A245,A308;
end;
end;
hence thesis;
end;
A309: for n be Nat holds ARC[n] from NAT_1:sch 2(A14,A33);
1 <= h1 + 2 by A12,XXREAL_0:2;
then ex NE being non empty Subset of TOP-REAL 2 st ( NE = Q(h1))
&( for j be Nat for F being Function of I[01], (TOP-REAL 2 )|NE st 1
<= j & j+1 <= h1+2 & F is being_homeomorphism & F.0 = f/.1 & F.1 = f /.(h1+2)
ex p1, p2 be Real
st p1 < p2 & 0 <= p1 & p1 <= 1 & 0 <= p2 & p2 <= 1 & LSeg (f,
j) = F.:[.p1, p2.] & F.p1 = f/.j & F.p2 = f/.(j+1)) by A309;
hence thesis by A1,A2,A4,A5,A6,A7,A13;
end;
theorem
for f being FinSequence of TOP-REAL 2,
Q, R being non empty Subset of TOP-REAL 2,
F being Function of I[01], (TOP-REAL 2)|Q, i being Nat,
P being non empty Subset of I[01] st
f is being_S-Seq & F is being_homeomorphism & F.0 = f/.1 & F.1 = f/.len f &
1 <= i & i+1 <= len f & F.:P = LSeg (f,i) & Q = L~f & R = LSeg(f,i)
ex G being Function of I[01]|P, (TOP-REAL 2)|R st
G = F|P & G is being_homeomorphism
proof
let f be FinSequence of TOP-REAL 2, Q, R be non empty Subset of TOP-REAL 2,
F be Function of I[01], (TOP-REAL 2)|Q, i be Nat,
P be non empty Subset of I[01];
assume that
A1: f is being_S-Seq and
A2: F is being_homeomorphism and
A3: F.0 = f/.1 and
A4: F.1 = f/.len f and
A5: 1 <= i and
A6: i+1 <= len f and
A7: F.:P = LSeg (f,i) and
A8: Q = L~f and
A9: R = LSeg(f,i);
consider ppi, pi1 be Real such that
A10: ppi < pi1 and
A11: 0 <= ppi and ppi <= 1
and 0 <= pi1 and
A12: pi1 <= 1 and
A13: LSeg (f, i) = F.:[.ppi, pi1.] and F.ppi = f/.i
and F.pi1 = f/.(i+1) by A1,A2,A3,A4,A5,A6,A8,Th7;
ppi in { dd where dd is Real: ppi <= dd & dd <= pi1 } by A10;
then reconsider Poz = [.ppi, pi1.] as non empty Subset of I[01]
by A11,A12,BORSUK_1:40,RCOMP_1:def 1,XXREAL_1:34;
A14: the carrier of (I[01]|Poz) = [#] (I[01]|Poz) .= Poz by PRE_TOPC:def 5;
A15: dom F = [#]I[01] by A2,TOPS_2:def 5
.= [.0,1.] by BORSUK_1:40;
A16: F is one-to-one by A2,TOPS_2:def 5;
then
A17: P c= Poz by A7,A13,A15,BORSUK_1:40,FUNCT_1:87;
Poz c= P by A7,A13,A15,A16,BORSUK_1:40,FUNCT_1:87;
then
A18: P = Poz by A17;
set gg = F | P;
reconsider gg as Function of I[01]|Poz, (TOP-REAL 2)| Q by A14,A18,FUNCT_2:32
;
reconsider SEG= LSeg (f, i) as non empty Subset of (TOP-REAL 2)|Q by A7,A9;
A19: the carrier of (((TOP-REAL 2) | Q) | SEG) = [#](((TOP-REAL 2) | Q) | SEG)
.= SEG by PRE_TOPC:def 5;
A20: rng gg c= SEG
proof
let ii be object;
assume ii in rng gg;
then consider j be object such that
A21: j in dom gg and
A22: ii = gg.j by FUNCT_1:def 3;
j in dom F /\ Poz by A18,A21,RELAT_1:61;
then j in dom F by XBOOLE_0:def 4;
then F.j in LSeg (f,i) by A13,A14,A21,FUNCT_1:def 6;
hence thesis by A14,A18,A21,A22,FUNCT_1:49;
end;
reconsider SEG as non empty Subset of (TOP-REAL 2)|Q;
A23: ((TOP-REAL 2) | Q) | SEG = (TOP-REAL 2) | R by A9,GOBOARD9:2;
reconsider hh9 = gg as Function
of I[01]|Poz, ((TOP-REAL 2) | Q)| SEG by A19,A20,FUNCT_2:6;
A24: F is continuous by A2,TOPS_2:def 5;
A25: F is one-to-one by A2,TOPS_2:def 5;
gg is continuous by A18,A24,TOPMETR:7;
then
A26: hh9 is continuous by TOPMETR:6;
A27: hh9 is one-to-one by A25,FUNCT_1:52;
reconsider hh = hh9 as Function of I[01]|Poz, (TOP-REAL 2) | R by A9,
GOBOARD9:2;
A28: dom hh = [#] (I[01] | Poz) by FUNCT_2:def 1;
then
A29: dom hh = Poz by PRE_TOPC:def 5;
A30: rng hh = hh.:(dom hh) by A28,RELSET_1:22
.= [#](((TOP-REAL 2) | Q) | SEG) by A7,A13,A15,A16,A19,A29,BORSUK_1:40
,FUNCT_1:87,RELAT_1:129;
reconsider A = Closed-Interval-TSpace (ppi,pi1) as
strict SubSpace of I[01] by A10,A11,A12,TOPMETR:20,TREAL_1:3;
A31: Poz = [#] A by A10,TOPMETR:18;
Closed-Interval-TSpace (ppi,pi1) is compact by A10,HEINE:4;
then [#] Closed-Interval-TSpace (ppi,pi1) is compact by COMPTS_1:1;
then for P being Subset of A st P=Poz holds P is compact by A10,TOPMETR:18;
then Poz is compact by A31,COMPTS_1:2;
then
A32: I[01]|Poz is compact by COMPTS_1:3;
(TOP-REAL 2)|R is T_2 by TOPMETR:2;
hence thesis by A18,A23,A26,A27,A30,A32,COMPTS_1:17;
end;
begin :: Some properties of real intervals
theorem Th9:
for p1, p2, p being Point of TOP-REAL 2 st
p1 <> p2 & p in LSeg(p1,p2) holds LE p,p,p1,p2
by JORDAN5A:2;
theorem Th10:
for p, p1, p2 being Point of TOP-REAL 2 st p1 <> p2 &
p in LSeg(p1,p2) holds LE p1,p,p1,p2
proof
let p, p1, p2 be Point of TOP-REAL 2;
assume that
A1: p1 <> p2 and
A2: p in LSeg(p1,p2);
thus LE p1,p,p1,p2
proof
thus p1 in LSeg(p1,p2) & p in LSeg(p1,p2) by A2,RLTOPSP1:68;
let r1,r2 be Real;
assume that
0<=r1 and r1<=1 and
A3: p1=(1-r1)*p1+r1*p2 and
A4: 0<=r2 and r2<=1
and p=(1-r2)*p1+r2*p2;
0.TOP-REAL 2 = (1-r1)*p1+r1*p2+-p1 by A3,RLVECT_1:5
.= (1-r1)*p1+r1*p2-p1
.= (1-r1)*p1+(r1*p2-p1) by RLVECT_1:def 3
.= (1-r1)*p1+(-p1+r1*p2)
.= (1-r1)*p1+-p1+r1*p2 by RLVECT_1:def 3
.= ((1-r1)*p1-p1)+r1*p2;
then -r1*p2=(((1-r1)*p1-p1)+r1*p2)+-r1*p2 by RLVECT_1:4
.=(((1-r1)*p1-p1)+r1*p2)-r1*p2
.=((1-r1)*p1-p1)+(r1*p2-r1*p2) by RLVECT_1:def 3
.=((1-r1)*p1-p1)+0.TOP-REAL 2 by RLVECT_1:5
.=(1-r1)*p1-p1 by RLVECT_1:4
.=(1-r1)*p1-1*p1 by RLVECT_1:def 8
.=(1-r1-1)*p1 by RLVECT_1:35
.=(-r1)*p1
.=-r1*p1 by RLVECT_1:79;
then r1*p1=--r1*p2
.= r1*p2;
hence thesis by A1,A4,RLVECT_1:36;
end;
end;
theorem Th11:
for p, p1, p2 being Point of TOP-REAL 2 st p in LSeg(p1,p2) & p1 <> p2
holds LE p,p2,p1,p2
proof
let p, p1, p2 be Point of TOP-REAL 2;
assume that
A1: p in LSeg(p1,p2) and
A2: p1 <> p2;
thus LE p,p2,p1,p2
proof
thus p in LSeg(p1,p2) & p2 in LSeg(p1,p2) by A1,RLTOPSP1:68;
let r1,r2 be Real such that
0<=r1 and
A3: r1<=1 and p=(1-r1)*p1+r1*p2
and 0<=r2
and r2<=1 and
A4: p2=(1-r2)*p1+r2*p2;
p2 = 1*p2 by RLVECT_1:def 8
.= 0.TOP-REAL 2 + 1*p2 by RLVECT_1:4
.= (1-1)*p1 + 1*p2 by RLVECT_1:10;
hence thesis by A2,A3,A4,JORDAN5A:2;
end;
end;
theorem
for p1, p2, q1, q2, q3 being Point of TOP-REAL 2 st p1 <> p2 &
LE q1,q2,p1,p2 & LE q2,q3,p1,p2 holds LE q1,q3,p1,p2
proof
let p1, p2, q1, q2, q3 be Point of TOP-REAL 2;
assume that
A1: p1<>p2 and
A2: LE q1,q2,p1,p2 and
A3: LE q2,q3,p1,p2;
A4: q1 in LSeg(p1,p2) by A2;
A5: q2 in LSeg(p1,p2) by A2;
A6: q3 in LSeg(p1,p2) by A3;
consider s1 being Real such that
A7: q1=(1-s1)*p1+s1*p2 and 0<=s1 and
A8: s1<=1 by A4;
consider s2 being Real such that
A9: q2=(1-s2)*p1+s2*p2 and
A10: 0<=s2 and
A11: s2<=1 by A5;
A12: s1 <= s2 by A2,A7,A8,A9,A10,A11;
consider s3 being Real such that
A13: q3=(1-s3)*p1+s3*p2 and
A14: 0<=s3 and
A15: s3<=1 by A6;
s2 <= s3 by A3,A9,A11,A13,A14,A15;
then
A16: s1 <= s3 by A12,XXREAL_0:2;
thus LE q1,q3,p1,p2
proof
thus q1 in LSeg(p1,p2) & q3 in LSeg(p1,p2) by A2,A3;
let r1,r2 be Real;
assume that
0<=r1 and r1<=1 and
A17: q1=(1-r1)*p1+r1*p2 and 0<=r2
and r2<=1 and
A18: q3=(1-r2)*p1+r2*p2;
s1 = r1 by A1,A7,A17,JORDAN5A:2;
hence thesis by A1,A13,A16,A18,JORDAN5A:2;
end;
end;
theorem
for p, q being Point of TOP-REAL 2 st p <> q holds LSeg (p, q) =
{ p1 where p1 is Point of TOP-REAL 2 : LE p, p1, p, q & LE p1, q, p, q }
proof
let p, q be Point of TOP-REAL 2;
assume
A1: p <> q;
thus LSeg (p, q) c=
{ p1 where p1 is Point of TOP-REAL 2 : LE p, p1, p, q & LE p1, q, p, q }
proof
let a be object;
assume
A2: a in LSeg (p, q);
then reconsider a9 = a as Point of TOP-REAL 2;
A3: LE p, a9, p, q by A1,A2,Th10;
LE a9, q, p, q by A1,A2,Th11;
hence thesis by A3;
end;
thus { p1 where p1 is Point of TOP-REAL 2 :
LE p, p1, p, q & LE p1, q, p, q } c= LSeg (p, q)
proof
let a be object;
assume a in { p1 where p1 is Point of TOP-REAL 2 :
LE p, p1, p, q & LE p1, q, p, q };
then ex a9 be Point of TOP-REAL 2 st ( a9 = a)&( LE p, a9, p, q)
&( LE a9, q, p, q);
hence thesis;
end;
end;
theorem
for n being Nat, P being Subset of TOP-REAL n,
p1, p2 being Point of TOP-REAL n st
P is_an_arc_of p1,p2 holds P is_an_arc_of p2,p1
proof
let n be Nat, P be Subset of TOP-REAL n,
p1,p2 be Point of TOP-REAL n;
assume
A1: P is_an_arc_of p1, p2;
then consider f being Function of I[01], (TOP-REAL n) | P such that
A2: f is being_homeomorphism and
A3: f.0 = p1 and
A4: f.1 = p2 by TOPREAL1:def 1;
set Ex = L[01]((0,1)(#),(#)(0,1));
A5: Ex is being_homeomorphism by TREAL_1:18;
set g = f * Ex;
A6: Ex.(0,1)(#) = 0 by BORSUK_1:def 14,TREAL_1:5,9;
A7: Ex.(#)(0,1) = 1 by BORSUK_1:def 15,TREAL_1:5,9;
dom f = [#]I[01] by A2,TOPS_2:def 5;
then rng Ex = dom f by A5,TOPMETR:20,TOPS_2:def 5;
then
A8: dom g = dom Ex by RELAT_1:27;
reconsider P as non empty Subset of TOP-REAL n by A1,TOPREAL1:1;
A9: dom g = [#]I[01] by A5,A8,TOPMETR:20,TOPS_2:def 5;
reconsider g as Function of I[01], (TOP-REAL n) | P by TOPMETR:20;
A10: g is being_homeomorphism by A2,A5,TOPMETR:20,TOPS_2:57;
A11: g.0 = p2 by A4,A7,A9,BORSUK_1:def 14,FUNCT_1:12,TREAL_1:5;
g.1 = p1 by A3,A6,A9,BORSUK_1:def 15,FUNCT_1:12,TREAL_1:5;
hence thesis by A10,A11,TOPREAL1:def 1;
end;
theorem
for i being Nat, f being FinSequence of TOP-REAL 2,
P being Subset of TOP-REAL 2 st
f is being_S-Seq & 1 <= i & i+1 <= len f & P = LSeg(f,i) holds
P is_an_arc_of f/.i, f/.(i+1)
proof
let i be Nat, f be FinSequence of TOP-REAL 2,
P be Subset of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: 1 <= i and
A3: i+1 <= len f and
A4: P = LSeg(f,i);
A5: i in dom f by A2,A3,SEQ_4:134;
A6: i+1 in dom f by A2,A3,SEQ_4:134;
A7: f is one-to-one by A1;
A8: LSeg (f,i) = LSeg (f/.i, f/.(i+1)) by A2,A3,TOPREAL1:def 3;
f/.i <> f/.(i+1)
proof
assume f/.i = f/.(i+1);
then i = i + 1 by A5,A6,A7,PARTFUN2:10;
hence thesis;
end;
hence thesis by A4,A8,TOPREAL1:9;
end;
begin :: Cutting off sequences
theorem
for g1 being FinSequence of TOP-REAL 2, i being Nat
st 1 <= i & i <= len g1 & g1 is being_S-Seq holds
g1/.1 in L~mid(g1, i, len g1) implies i = 1
proof
let g1 be FinSequence of TOP-REAL 2, i be Nat;
assume that
A1: 1 <= i and
A2: i <= len g1 and
A3: g1 is being_S-Seq;
assume g1/.1 in L~mid(g1, i, len g1);
then consider j being Nat such that
A4: 1 <= j and
A5: j+1 <= len mid(g1, i, len g1) and
A6: g1/.1 in LSeg(mid(g1, i, len g1),j) by SPPOL_2:13;
A7: j+1 in dom mid(g1, i, len g1) by A4,A5,SEQ_4:134;
A8: mid(g1, i, len g1) = g1/^(i-'1) by A2,FINSEQ_6:117;
j <= j+1 by NAT_1:11;
then
A9: j <= len (g1/^(i-'1)) by A5,A8,XXREAL_0:2;
then
A10: j in dom (g1/^(i-'1)) by A4,FINSEQ_3:25;
i-'1 <= i by A1,Th1;
then
A11: i-'1 <= len g1 by A2,XXREAL_0:2;
then
A12: j <= len g1 - (i-'1) by A9,RFINSEQ:def 1;
j <= i-'1+j by NAT_1:11;
then
A13: 1 <= i-'1+j by A4,XXREAL_0:2;
A14: j+(i-'1) <= len g1 by A12,XREAL_1:19;
then
A15: i-'1+j in dom g1 by A13,FINSEQ_3:25;
A16: (g1/^(i-'1))/.j = (g1/^(i-'1)).j by A10,PARTFUN1:def 6
.= g1.(i-'1+j) by A4,A14,FINSEQ_6:114
.= g1/.(i-'1+j) by A15,PARTFUN1:def 6;
A17: 1 <= j+1 by NAT_1:11;
j+1 <= i-'1+(j+1) by NAT_1:11;
then
A18: 1 <= i-'1+(j+1) by A17,XXREAL_0:2;
j+1 <= len (g1/^(i-'1)) by A2,A5,FINSEQ_6:117;
then
A19: j+1 <= len g1 - (i-'1) by A11,RFINSEQ:def 1;
A20: 1 <= j+1 by A7,FINSEQ_3:25;
A21: j+1+(i-'1) <= len g1 by A19,XREAL_1:19;
then
A22: i-'1+(j+1) in dom g1 by A18,FINSEQ_3:25;
j+1 in dom (g1/^(i-'1)) by A2,A7,FINSEQ_6:117;
then
A23: (g1/^(i-'1))/.(j+1) = (g1/^(i-'1)).(j+1) by PARTFUN1:def 6
.= g1.(i-'1+(j+1)) by A20,A21,FINSEQ_6:114
.= g1/.(i-'1+(j+1)) by A22,PARTFUN1:def 6;
A24: i-'1+j+1 = i-'1+(j+1);
A25: i-'1+j+1 <= len g1 by A21;
A26: LSeg(mid(g1, i, len g1),j) =
LSeg (g1/.(i-'1+j), g1/.(i-'1+(j+1)) ) by A4,A5,A8,A16,A23,TOPREAL1:def 3
.= LSeg ( g1, i-'1+j ) by A13,A21,A24,TOPREAL1:def 3;
A27: 1+1 <= len g1 by A3,TOPREAL1:def 8;
then g1/.1 in LSeg ( g1, 1 ) by TOPREAL1:21;
then
A28: g1/.1 in LSeg ( g1, 1 ) /\ LSeg ( g1, i-'1+j ) by A6,A26,XBOOLE_0:def 4;
then
A29: LSeg (g1, 1) meets LSeg ( g1, i-'1+j );
assume i <> 1;
then 1 < i by A1,XXREAL_0:1;
then 1+1 <= i by NAT_1:13;
then 2-'1 <= i-'1 by NAT_D:42;
then 2-'1+1 <= i-'1+j by A4,XREAL_1:7;
then
A30: i-'1+j >= 2 by XREAL_1:235;
A31: g1 is s.n.c. unfolded one-to-one by A3;
A32: 1 in dom g1 by A27,SEQ_4:134;
A33: 1+1 in dom g1 by A27,SEQ_4:134;
per cases by A30,XXREAL_0:1;
suppose i-'1+j = 2;
then g1/.1 in { g1/.(1+1) } by A25,A28,A31,TOPREAL1:def 6;
then g1/.1 = g1/.(1+1) by TARSKI:def 1;
hence thesis by A31,A32,A33,PARTFUN2:10;
end;
suppose i-'1+j > 2;
then i-'1+j > 1+1;
hence thesis by A29,A31,TOPREAL1:def 7;
end;
end;
theorem
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st f is being_S-Seq & p = f.len f holds
L_Cut (f,p) = <*p*>
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: f is being_S-Seq and
A2: p = f.len f;
len f >= 2 by A1,TOPREAL1:def 8;
then p in L~f by A2,JORDAN3:1;
then
A3: p in L~Rev f by SPPOL_2:22;
A4: L_Cut(f,p) =L_Cut(Rev Rev f,p)
.= Rev R_Cut(Rev f,p) by A1,A3,JORDAN3:22;
p = (Rev f).1 by A2,FINSEQ_5:62;
then R_Cut(Rev f,p) = <*p*> by JORDAN3:def 4;
hence thesis by A4,FINSEQ_5:60;
end;
theorem
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st
p in L~f & p <> f.len f & f is being_S-Seq holds Index (p, L_Cut(f,p)) = 1
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: p <> f.len f and
A3: f is being_S-Seq;
L_Cut(f,p) is being_S-Seq by A1,A2,A3,JORDAN3:34;
then
A4: 2 <= len L_Cut(f,p) by TOPREAL1:def 8;
then 1 <= len L_Cut(f,p) by XXREAL_0:2;
then 1 in dom L_Cut(f,p) by FINSEQ_3:25;
then (L_Cut(f,p))/.1 = (L_Cut(f,p)).1 by PARTFUN1:def 6
.= p by A1,JORDAN3:23;
hence thesis by A4,JORDAN3:11;
end;
theorem Th19:
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st
p in L~f & f is being_S-Seq & p <> f.len f holds p in L~L_Cut (f,p)
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: f is being_S-Seq;
assume p <> f.len f;
then L_Cut (f,p) is being_S-Seq by A1,A2,JORDAN3:34;
then
A3: len L_Cut (f,p) >= 2 by TOPREAL1:def 8;
L_Cut (f,p).1 = p by A1,JORDAN3:23;
hence thesis by A3,JORDAN3:1;
end;
theorem
for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st
p in L~f & f is being_S-Seq & p <> f.1 holds p in L~R_Cut (f,p)
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: f is being_S-Seq;
assume p <> f.1;
then R_Cut (f,p) is being_S-Seq by A1,A2,JORDAN3:35;
then
A3: len R_Cut (f,p) >= 2 by TOPREAL1:def 8;
R_Cut (f,p).len R_Cut (f,p) = p by A1,JORDAN3:24;
hence thesis by A3,JORDAN3:1;
end;
theorem Th21:
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f & f is one-to-one
holds B_Cut(f,p,p) = <*p*>
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: f is one-to-one;
A3: Index(p,f) <> Index(p,f)+1;
A4: Index(p,f) < len f by A1,JORDAN3:8;
A5: 1 <= Index(p,f) by A1,JORDAN3:8;
A6: Index(p,f) + 1 <= len f by A4,NAT_1:13;
then
A7: Index(p,f) in dom f by A5,SEQ_4:134;
A8: Index(p,f) + 1 in dom f by A5,A6,SEQ_4:134;
p in LSeg(f,Index(p,f)) by A1,JORDAN3:9;
then p in LSeg(f/.Index(p,f), f/.(Index(p,f)+1)) by A5,A6,TOPREAL1:def 3;
then
A9: LE p,p,f/.Index(p,f),f/.(Index(p,f)+1) by A2,A3,A7,A8,Th9,PARTFUN2:10;
(L_Cut(f,p)).1 = p by A1,JORDAN3:23;
then R_Cut(L_Cut(f,p),p) = <*p*> by JORDAN3:def 4;
hence thesis by A9,JORDAN3:def 7;
end;
Lm2: for f being FinSequence of TOP-REAL 2, p, q being Point of TOP-REAL 2 st
p in L~f & q in L~f & p <> f.len f &
f is being_S-Seq holds
p in L~L_Cut(f,q) or q in L~L_Cut(f,p)
proof
let f be FinSequence of TOP-REAL 2, p, q be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: q in L~f and
A3: p <> f.len f and
A4: f is being_S-Seq;
A5: Index (p, f) < len f by A1,JORDAN3:8;
A6: 1 <= Index (p, f) by A1,JORDAN3:8;
A7: Index (p, f) + 1 <= len f by A5,NAT_1:13;
then
A8: LSeg (f, Index(p,f)) = LSeg (f/.Index(p,f), f/.(Index(p,f)+1))
by A6,TOPREAL1:def 3;
A9: Index(p,f) in dom f by A6,A7,SEQ_4:134;
A10: Index(p,f)+1 in dom f by A6,A7,SEQ_4:134;
A11: f is one-to-one by A4;
Index(p,f) < Index(p,f)+1 by NAT_1:13;
then
A12: f/.Index(p,f) <> f/.(Index(p,f)+1) by A9,A10,A11,PARTFUN2:10;
per cases by XXREAL_0:1;
suppose Index(p,f) < Index(q,f);
hence thesis by A1,A2,JORDAN3:29;
end;
suppose
A13: Index(p,f) = Index (q,f);
A14: p in LSeg (f/.Index(p,f), f/.(Index(p,f)+1)) by A1,A8,JORDAN3:9;
q in LSeg (f/.Index(p,f), f/.(Index(p,f)+1)) by A2,A8,A13,JORDAN3:9;
then
A15: LE p, q, f/.Index(p,f), f/.(Index(p,f)+1) or
LT q, p, f/.Index(p,f), f/.(Index(p,f)+1) by A12,A14,JORDAN3:28;
now per cases by A15;
suppose
A16: LE p, q, f/.Index(p,f), f/.(Index(p,f)+1);
thus p in L~L_Cut(f,q) or q in L~L_Cut(f,p)
proof
per cases;
suppose p <> q;
hence thesis by A1,A2,A13,A16,JORDAN3:31;
end;
suppose p = q;
hence thesis by A1,A3,A4,Th19;
end;
end;
end;
suppose
A17: LE q, p, f/.Index(p,f), f/.(Index(p,f)+1);
thus p in L~L_Cut(f,q) or q in L~L_Cut(f,p)
proof
per cases;
suppose p <> q;
hence thesis by A1,A2,A13,A17,JORDAN3:31;
end;
suppose p = q;
hence thesis by A1,A3,A4,Th19;
end;
end;
end;
end;
hence thesis;
end;
suppose Index(p,f) > Index(q,f);
hence thesis by A1,A2,JORDAN3:29;
end;
end;
theorem Th22:
for f being FinSequence of TOP-REAL 2, p, q being Point of TOP-REAL 2 st
p in L~f & q in L~f & q <> f.len f & p = f.len f & f is being_S-Seq holds
p in L~L_Cut(f,q)
proof
let f be FinSequence of TOP-REAL 2, p, q be Point of TOP-REAL 2;
assume that
A1: p in L~f and
A2: q in L~f and
A3: q <> f.len f and
A4: p = f.len f and
A5: f is being_S-Seq;
1 + 1 <= len f by A5,TOPREAL1:def 8;
then
A6: 1 < len f by XXREAL_0:2;
then
A7: Index(p,f) + 1 = len f by A4,A5,JORDAN3:12;
AA: len f in dom f by A6,FINSEQ_3:25; then
AB: mid(f,len f,len f) = <*f.len f*> by FINSEQ_6:193
.= <*f/.len f*> by AA,PARTFUN1:def 6;
Index(q,f) < len f by A2,JORDAN3:8;
then
A8: Index(q,f) <= Index(p,f) by A7,NAT_1:13;
per cases by A8,XXREAL_0:1;
suppose Index (q,f) = Index (p,f);
then
A9: L_Cut(f,q) = <*q*>^mid(f,len f,len f) by A3,A7,JORDAN3:def 3
.= <*q*>^<*f/.len f*> by AB
.= <*q,f/.len f*> by FINSEQ_1:def 9
.= <*q,p*> by A4,A6,FINSEQ_4:15;
then rng L_Cut(f,q) = {p,q} by FINSEQ_2:127;
then
A10: p in rng L_Cut(f,q) by TARSKI:def 2;
len L_Cut(f,q) = 2 by A9,FINSEQ_1:44;
then rng L_Cut(f,q) c= L~L_Cut(f,q) by SPPOL_2:18;
hence thesis by A10;
end;
suppose Index (q,f) < Index (p,f);
hence thesis by A1,A2,JORDAN3:29;
end;
end;
theorem
for f being FinSequence of TOP-REAL 2, p, q being Point of TOP-REAL 2 st
p <> f.len f & p in L~f & q in L~f & f is being_S-Seq holds
p in L~L_Cut(f,q) or q in L~L_Cut(f,p)
proof
let f be FinSequence of TOP-REAL 2, p, q be Point of TOP-REAL 2;
assume
A1: p <> f.len f;
assume that
A2: p in L~f and
A3: q in L~f and
A4: f is being_S-Seq;
per cases by A1;
suppose p <> f.len f & q = f.len f;
hence thesis by A2,A3,A4,Th22;
end;
suppose p = f.len f & q <> f.len f;
hence thesis by A2,A3,A4,Th22;
end;
suppose p <> f.len f & q <> f.len f;
hence thesis by A2,A3,A4,Lm2;
end;
end;
Lm3: for f be FinSequence of TOP-REAL 2
for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f &
( Index(p,f) < Index(q,f) or
Index(p,f) = Index(q,f) & LE p,q,f/.Index(p,f),f/.(Index(p,f)+1) ) &
p <> q holds L~B_Cut(f,p,q) c= L~f
proof
let f be FinSequence of TOP-REAL 2;
let p,q be Point of TOP-REAL 2 such that
A1: p in L~f and
A2: q in L~f and
A3: Index(p,f)<Index(q,f) or
Index(p,f)=Index(q,f) & LE p,q,f/.Index(p,f),f/.(Index(p,f)+1) and
A4: p <> q;
A5: B_Cut(f,p,q) = R_Cut(L_Cut(f,p),q) by A1,A2,A3,JORDAN3:def 7;
now per cases by A3;
case Index(p,f)<Index(q,f);
then q in L~(L_Cut(f,p)) by A1,A2,JORDAN3:29;
hence ex i1 being Nat st 1<=i1 & i1+1<=len L_Cut(f,p) &
q in LSeg(L_Cut(f,p),i1) by SPPOL_2:13;
end;
case Index(p,f)=Index(q,f) & LE p,q,f/.Index(p,f),f/.(Index(p,f)+1);
then q in L~(L_Cut(f,p)) by A1,A2,A4,JORDAN3:31;
hence ex i1 being Nat st 1<=i1 & i1+1<=len L_Cut(f,p) &
q in LSeg(L_Cut(f,p),i1) by SPPOL_2:13;
end;
end;
then
A6: L~B_Cut(f,p,q) c= L~L_Cut(f,p) by A5,JORDAN3:41,SPPOL_2:17;
L~L_Cut(f,p) c= L~f by A1,JORDAN3:42;
hence thesis by A6;
end;
theorem
for f being FinSequence of TOP-REAL 2,
p, q being Point of TOP-REAL 2 st p in L~f & q in L~f & f is being_S-Seq
holds L~B_Cut(f,p,q) c= L~f
proof
let f be FinSequence of TOP-REAL 2, p, q be Point of TOP-REAL 2 such that
A1: p in L~f and
A2: q in L~f and
A3: f is being_S-Seq;
A4: f is one-to-one by A3;
per cases;
suppose p = q;
then B_Cut(f,p,q) = <*p*> by A1,A4,Th21;
then len B_Cut(f,p,q) = 1 by FINSEQ_1:39;
then L~B_Cut(f,p,q) = {} by TOPREAL1:22;
hence thesis;
end;
suppose p <> q & (Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f)
& LE p,q,f/.Index(p,f),f/.(Index(p,f)+1));
hence thesis by A1,A2,Lm3;
end;
suppose that
A5: p <> q and
A6: not(Index(p,f)<Index(q,f) or Index(p,f)=Index(q,f)
& LE p,q,f/.Index(p,f),f/.(Index(p,f)+1));
A7: B_Cut(f,p,q)=Rev R_Cut(L_Cut(f,q),p) by A6,JORDAN3:def 7;
A8: Index(q,f) < Index(p,f)
or Index(p,f)=Index(q,f) & not LE p,q,f/.Index(p,f),f/.(Index(p,f)+1)
by A6,XXREAL_0:1;
A9: now
assume that
A10: Index(p,f)=Index(q,f) and
A11: not LE p,q,f/.Index(p,f),f/.(Index(p,f)+1);
A12: 1 <= Index(p,f) by A1,JORDAN3:8;
A13: Index(p,f) < len f by A1,JORDAN3:8;
then
A14: Index(p,f)+1 <= len f by NAT_1:13;
then
A15: LSeg(f,Index(p,f)) = LSeg(f/.Index(p,f),f/.(Index(p,f)+1))
by A12,TOPREAL1:def 3;
then
A16: p in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A1,JORDAN3:9;
A17: q in LSeg(f/.Index(p,f),f/.(Index(p,f)+1)) by A2,A10,A15,JORDAN3:9;
A18: Index(p,f) in dom f by A12,A13,FINSEQ_3:25;
1 <= Index(p,f)+1 by NAT_1:11;
then
A19: Index(p,f)+1 in dom f by A14,FINSEQ_3:25;
Index(p,f)+0 <> Index(p,f)+1;
then f/.Index(p,f)<>f/.(Index(p,f)+1) by A4,A18,A19,PARTFUN2:10;
then LT q,p,f/.Index(p,f), f/.(Index(p,f)+1) by A11,A16,A17,JORDAN3:28;
hence LE q,p,f/.Index(q,f),f/.(Index(q,f)+1) by A10;
end;
then
A20: Rev B_Cut(f,q,p) = B_Cut(f,p,q) by A1,A2,A7,A8,JORDAN3:def 7;
L~B_Cut(f,q,p) c= L~f by A1,A2,A5,A8,A9,Lm3;
hence thesis by A20,SPPOL_2:22;
end;
end;
theorem
for f being non constant standard special_circular_sequence,
i, j being Nat st 1 <= i & j <= len GoB f & i < j holds
LSeg((GoB f)*(1,width GoB f), (GoB f)*(i,width GoB f)) /\
LSeg((GoB f)*(j,width GoB f), (GoB f)*(len GoB f,width GoB f)) = {}
proof
let f be non constant standard special_circular_sequence,
i, j be Nat;
assume that
A1: 1 <= i and
A2: j <= len GoB f and
A3: i < j;
set A = LSeg((GoB f)*(1,width GoB f), (GoB f)*(i,width GoB f)),
B = LSeg((GoB f)*(j,width GoB f), (GoB f)*(len GoB f,width GoB f));
assume A /\ B <> {};
then A meets B;
then consider x be object such that
A4: x in A and
A5: x in B by XBOOLE_0:3;
reconsider x1 = x as Point of TOP-REAL 2 by A4;
A6: 1 <= width GoB f by GOBOARD7:33;
A7: i <= len GoB f by A2,A3,XXREAL_0:2;
((GoB f)*(1,width GoB f))`1 <= ((GoB f)*(i,width GoB f))`1
proof
per cases by A1,XXREAL_0:1;
suppose i = 1;
hence thesis;
end;
suppose i > 1;
hence thesis by A6,A7,GOBOARD5:3;
end;
end;
then
A8: x1`1 <= ((GoB f)*(i,width GoB f) )`1 by A4,TOPREAL1:3;
A9: ((GoB f)*(j,width GoB f))`1 > ((GoB f)*(i,width GoB f))`1
by A1,A2,A3,A6,GOBOARD5:3;
A10: 1 <= j by A1,A3,XXREAL_0:2;
((GoB f)*(j,width GoB f))`1 <= ((GoB f)*(len GoB f,width GoB f))`1
proof
per cases by A2,XXREAL_0:1;
suppose j < len GoB f;
hence thesis by A6,A10,GOBOARD5:3;
end;
suppose j = len GoB f;
hence thesis;
end;
end;
then x1`1 >= ((GoB f)*(j,width GoB f))`1 by A5,TOPREAL1:3;
hence thesis by A8,A9,XXREAL_0:2;
end;
theorem
for f being non constant standard special_circular_sequence,
i, j being Nat st 1 <= i & j <= width GoB f & i < j holds
LSeg((GoB f)*(len GoB f,1), (GoB f)*(len GoB f,i)) /\
LSeg((GoB f)*(len GoB f,j), (GoB f)*(len GoB f,width GoB f)) = {}
proof
let f be non constant standard special_circular_sequence,
i, j be Nat;
assume that
A1: 1 <= i and
A2: j <= width GoB f and
A3: i < j;
set A = LSeg((GoB f)*(len GoB f,1), (GoB f)*(len GoB f,i)),
B = LSeg((GoB f)*(len GoB f,j), (GoB f)*(len GoB f,width GoB f));
assume A /\ B <> {};
then A meets B;
then consider x be object such that
A4: x in A and
A5: x in B by XBOOLE_0:3;
reconsider x1 = x as Point of TOP-REAL 2 by A4;
A6: 1 <= len GoB f by GOBOARD7:32;
A7: i <= width GoB f by A2,A3,XXREAL_0:2;
((GoB f)*(len GoB f,1))`2 <= ((GoB f)*(len GoB f,i))`2
proof
per cases by A1,XXREAL_0:1;
suppose i = 1;
hence thesis;
end;
suppose i > 1;
hence thesis by A6,A7,GOBOARD5:4;
end;
end;
then
A8: x1`2 <= ((GoB f)*(len GoB f,i)) `2 by A4,TOPREAL1:4;
A9: ((GoB f)*(len GoB f,j))`2 > ((GoB f)*(len GoB f,i))`2 by A1,A2,A3,A6,
GOBOARD5:4;
A10: 1 <= j by A1,A3,XXREAL_0:2;
((GoB f)*(len GoB f,j))`2 <= ((GoB f)*(len GoB f,width GoB f))`2
proof
per cases by A2,XXREAL_0:1;
suppose j < width GoB f;
hence thesis by A6,A10,GOBOARD5:4;
end;
suppose j = width GoB f;
hence thesis;
end;
end;
then x1`2 >= ((GoB f)*(len GoB f,j))`2 by A5,TOPREAL1:4;
hence thesis by A8,A9,XXREAL_0:2;
end;
theorem Th27:
for f being FinSequence of TOP-REAL 2 st f is being_S-Seq
holds L_Cut (f,f/.1) = f
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is being_S-Seq;
then
A2: 1+1 <= len f by TOPREAL1:def 8;
then 1 <= len f by XXREAL_0:2;
then
A3: 1 in dom f by FINSEQ_3:25;
A4: 1+1 in dom f by A2,FINSEQ_3:25;
A5: 1 < len f by A2,NAT_1:13;
A6: f is one-to-one by A1;
A7: f/.1 = f.1 by A3,PARTFUN1:def 6;
A8: Index(f/.1,f) = 1 by A2,JORDAN3:11;
f/.1 <> f/.(1+1) by A3,A4,A6,PARTFUN2:10;
then f/.1 <> f.(1+1) by A4,PARTFUN1:def 6;
hence L_Cut (f,f/.1) = <*f/.1*>^mid(f,Index(f/.1,f)+1,len f)
by A8,JORDAN3:def 3
.= mid(f,1,len f) by A3,A5,A7,A8,FINSEQ_6:126
.= f by A2,FINSEQ_6:120,XXREAL_0:2;
end;
theorem
for f being FinSequence of TOP-REAL 2 st f is being_S-Seq holds
R_Cut (f,f/.len f) = f
proof
let f be FinSequence of TOP-REAL 2;
assume
A1: f is being_S-Seq;
then
A2: 2 <= len f by TOPREAL1:def 8;
then
A3: f/.len f in L~f by JORDAN3:1;
A4: f/.len f = (Rev f)/.1 by A2,CARD_1:27,FINSEQ_5:65;
thus R_Cut (f,f/.len f) = Rev Rev R_Cut (f,f/.len f)
.= Rev L_Cut(Rev f,f/.len f) by A1,A3,JORDAN3:22
.= Rev Rev f by A1,A4,Th27
.= f;
end;
theorem
for f being FinSequence of TOP-REAL 2,
p being Point of TOP-REAL 2 st p in L~f holds
p in LSeg ( f/.Index(p,f), f/.(Index(p,f)+1) )
proof
let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2;
assume
A1: p in L~f;
then
A2: Index(p,f) < len f by JORDAN3:8;
A3: 1 <= Index(p,f) by A1,JORDAN3:8;
A4: Index(p,f)+1 <= len f by A2,NAT_1:13;
p in LSeg(f,Index(p,f)) by A1,JORDAN3:9;
hence thesis by A3,A4,TOPREAL1:def 3;
end;
theorem
for f be FinSequence of TOP-REAL 2 for i be Nat st
f is unfolded s.n.c. one-to-one & len f >= 2 & f/.1 in LSeg (f,i) holds
i = 1
proof
let f be FinSequence of TOP-REAL 2, i be Nat;
assume that
A1: f is unfolded s.n.c. one-to-one and
A2: 2 <= len f;
1 <= len f by A2,XXREAL_0:2;
then
A3: 1 in dom f by FINSEQ_3:25;
A4: 2 in dom f by A2,FINSEQ_3:25;
assume
A5: f/.1 in LSeg (f,i);
assume
A6: i <> 1;
per cases by A6,XXREAL_0:1;
suppose
A7: i > 1;
1+1 <= len f by A2;
then f/.1 in LSeg (f,1) by TOPREAL1:21;
then
A8: f/.1 in LSeg (f,1) /\ LSeg (f,i) by A5,XBOOLE_0:def 4;
then
A9: LSeg (f,1) meets LSeg (f,i);
now per cases by XXREAL_0:1;
suppose
A10: i = 2;
then
A11: 1 + 2 <= len f by A5,TOPREAL1:def 3;
1 + 1 = 2;
then f/.1 in { f/.2 } by A1,A8,A10,A11,TOPREAL1:def 6;
then f/.1 = f/.2 by TARSKI:def 1;
hence contradiction by A1,A3,A4,PARTFUN2:10;
end;
suppose i > 2;
then 1 + 1 < i;
hence contradiction by A1,A9,TOPREAL1:def 7;
end;
suppose i < 2;
then i < 1+1;
hence contradiction by A7,NAT_1:13;
end;
end;
hence thesis;
end;
suppose i < 1;
hence thesis by A5,TOPREAL1:def 3;
end;
end;
theorem
for f be non constant standard special_circular_sequence,
j be Nat, P be Subset of TOP-REAL 2 st
1 <= j & j <= width GoB f &
P = LSeg ((GoB f)*(1,j), (GoB f)*(len (GoB f),j)) holds
P is_S-P_arc_joining (GoB f)*(1,j), (GoB f)*(len (GoB f),j)
proof
let f be non constant standard special_circular_sequence,
j be Nat, P be Subset of TOP-REAL 2;
assume that
A1: 1 <= j and
A2: j <= width GoB f and
A3: P = LSeg ((GoB f)*(1,j), (GoB f)*(len (GoB f),j));
set p = (GoB f)*(1,j), q = (GoB f)*(len GoB f, j);
1 <= len GoB f by GOBOARD7:32;
then
A4: p`2 = q`2 by A1,A2,GOBOARD5:1;
A5: p`1 <> q`1
proof
assume
A6: p`1 = q`1;
A7: GoB f = GoB(Incr(X_axis(f)),Incr(Y_axis(f))) by GOBOARD2:def 2;
A8: 1 <= len GoB f by GOBOARD7:32;
then
A9: [1,j] in Indices GoB(Incr(X_axis f),Incr(Y_axis(f))) by A1,A2,A7,
MATRIX_0:30;
A10: [len GoB f,j] in Indices GoB(Incr(X_axis f),Incr(Y_axis(f))) by A1,A2,A7
,A8,MATRIX_0:30;
(GoB f)*(1,j)= (GoB(Incr(X_axis(f)),Incr(Y_axis(f))))*(1,j)
by GOBOARD2:def 2
.= |[Incr(X_axis(f)).1,Incr(Y_axis(f)).j]|
by A9,GOBOARD2:def 1;
then
A11: p`1 = Incr(X_axis(f)).1 by EUCLID:52;
A12: (GoB f)*(len GoB f, j) =
(GoB(Incr(X_axis(f)),Incr(Y_axis(f))))*(len GoB f, j) by GOBOARD2:def 2
.= |[Incr(X_axis(f)).(len GoB f), Incr(Y_axis(f)).j]|
by A10,GOBOARD2:def 1;
A13: len Incr (X_axis(f)) = len GoB f by A7,GOBOARD2:def 1;
A14: 1 <= len GoB f by GOBOARD7:32;
A15: 1 <= len Incr (X_axis(f)) by A13,GOBOARD7:32;
A16: len GoB f in dom Incr (X_axis(f)) by A13,A14,FINSEQ_3:25;
1 in dom Incr (X_axis(f)) by A15,FINSEQ_3:25;
then len GoB f = 1 by A6,A11,A12,A16,EUCLID:52,SEQ_4:138;
hence thesis by GOBOARD7:32;
end;
reconsider gg = <*p,q*> as FinSequence of the carrier of TOP-REAL 2;
A17: len gg = 2 by FINSEQ_1:44;
take gg;
thus gg is being_S-Seq by A4,A5,SPPOL_2:43;
thus P = L~gg by A3,SPPOL_2:21;
thus thesis by A17,FINSEQ_4:17;
end;
theorem
for f be non constant standard special_circular_sequence,
j be Nat, P be Subset of TOP-REAL 2 st 1 <= j & j <= len GoB f &
P = LSeg ((GoB f)*(j,1), (GoB f)*(j,width GoB f)) holds
P is_S-P_arc_joining (GoB f)*(j,1), (GoB f)*(j,width GoB f)
proof
let f be non constant standard special_circular_sequence,
j be Nat, P be Subset of TOP-REAL 2;
assume that
A1: 1 <= j and
A2: j <= len GoB f and
A3: P = LSeg ((GoB f)*(j,1), (GoB f)*(j,width GoB f));
set p = (GoB f)*(j, 1), q = (GoB f)*(j, width GoB f);
1 <= width GoB f by GOBOARD7:33;
then
A4: p`1 = q`1 by A1,A2,GOBOARD5:2;
A5: p`2 <> q`2
proof
assume
A6: p`2 = q`2;
A7: GoB f = GoB(Incr(X_axis(f)),Incr(Y_axis(f))) by GOBOARD2:def 2;
A8: 1 <= width GoB f by GOBOARD7:33;
then
A9: [j,1] in Indices GoB(Incr(X_axis f),Incr(Y_axis(f))) by A1,A2,A7,
MATRIX_0:30;
A10: [j,width GoB f] in Indices GoB(Incr(X_axis f),Incr(Y_axis(f))) by A1,A2,A7
,A8,MATRIX_0:30;
(GoB f)*(j,1)= (GoB(Incr(X_axis(f)),Incr(Y_axis(f))))*(j,1)
by GOBOARD2:def 2
.= |[Incr(X_axis(f)).j,Incr(Y_axis(f)).1]|
by A9,GOBOARD2:def 1;
then
A11: p`2 = Incr(Y_axis(f)).1 by EUCLID:52;
A12: (GoB f)*(j, width GoB f)=
(GoB(Incr(X_axis(f)),Incr(Y_axis(f))))*(j, width GoB f) by GOBOARD2:def 2
.= |[Incr(X_axis(f)).j, Incr(Y_axis(f)).(width GoB f)]|
by A10,GOBOARD2:def 1;
A13: len Incr (Y_axis(f)) = width GoB f by A7,GOBOARD2:def 1;
A14: 1 <= width GoB f by GOBOARD7:33;
A15: 1 <= len Incr (Y_axis(f)) by A13,GOBOARD7:33;
A16: width GoB f in dom Incr (Y_axis(f)) by A13,A14,FINSEQ_3:25;
1 in dom Incr (Y_axis(f)) by A15,FINSEQ_3:25;
then width GoB f = 1 by A6,A11,A12,A16,EUCLID:52,SEQ_4:138;
hence thesis by GOBOARD7:33;
end;
reconsider gg = <*p,q*> as FinSequence of the carrier of TOP-REAL 2;
A17: len gg = 2 by FINSEQ_1:44;
take gg;
thus gg is being_S-Seq by A4,A5,SPPOL_2:43;
thus P = L~gg by A3,SPPOL_2:21;
thus thesis by A17,FINSEQ_4:17;
end;
theorem
for f be FinSequence of TOP-REAL 2
for p,q be Point of TOP-REAL 2 st p in L~f & q in L~f &
( Index(p,f) < Index(q,f) or
Index(p,f) = Index(q,f) & LE p,q,f/.Index(p,f),f/.(Index(p,f)+1) ) &
p <> q holds L~B_Cut(f,p,q) c= L~f by Lm3;