:: Properties of Go-Board - Part III
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-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, FINSEQ_1, SUBSET_1, GOBOARD1, RELAT_1,
ARYTM_3, CARD_1, XXREAL_0, TOPREAL1, NAT_1, RLTOPSP1, PARTFUN1, MATRIX_1,
FUNCT_1, COMPLEX1, ARYTM_1, ZFMISC_1, TREES_1, INCSP_1, TARSKI, XBOOLE_0,
ORDINAL2, MCART_1, ORDINAL4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, NAT_1, FUNCT_1, PARTFUN1, SEQM_3, FINSEQ_1, PRE_TOPC, MATRIX_0,
STRUCT_0, MATRIX_1, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0;
constructors COMPLEX1, TOPREAL1, GOBOARD1, RELSET_1, DOMAIN_1, MATRIX_1,
REAL_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, EUCLID,
INT_1, CARD_1, FINSEQ_1, VALUED_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, TOPREAL1, XBOOLE_0;
equalities TOPREAL1, XBOOLE_0;
expansions TARSKI, TOPREAL1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, FINSEQ_3,
EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, GOBOARD2, FINSEQ_4, PARTFUN2,
INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, PARTFUN1,
ORDINAL1, SEQM_3, RLTOPSP1, SEQ_4, MATRIX_0;
schemes NAT_1, FINSEQ_4;
begin
reserve p,p1,p2,q for Point of TOP-REAL 2,
f,g,g1,g2 for FinSequence of TOP-REAL 2,
n,m,i,j,k for Nat,
G for Go-board,
x for set;
Lm1: now
let f,k;
A1: dom(f|k)=Seg len(f|k) by FINSEQ_1:def 3;
assume
A2: len f=k+1;
then
A3: len (f|k)=k by FINSEQ_1:59,NAT_1:11;
assume k<>0;
then
A4: 0+1<=k by NAT_1:13;
assume
A5: f is unfolded;
A6: k<=k+1 by NAT_1:11;
then
A7: k in dom f by A2,A4,FINSEQ_3:25;
thus f|k is unfolded
proof
let n be Nat;
set f1 = f|k;
assume that
A8: 1<=n and
A9: n+2 <= len f1;
reconsider n as Element of NAT by ORDINAL1:def 12;
A10: n+1 in dom f1 by A8,A9,SEQ_4:135;
n in dom f1 by A8,A9,SEQ_4:135;
then
A11: LSeg(f1,n)=LSeg(f,n) by A10,TOPREAL3:17;
len f1 <= len f by A2,A6,FINSEQ_1:59;
then
A12: n+2 <= len f by A9,XXREAL_0:2;
A13: n+1+1=n+(1+1);
n+2 in dom f1 by A8,A9,SEQ_4:135;
then
A14: LSeg(f1,n+1)=LSeg(f,n+1) by A10,A13,TOPREAL3:17;
f1/.(n+1)=f/.(n+1) by A7,A3,A1,A10,FINSEQ_4:71;
hence thesis by A5,A8,A11,A14,A12;
end;
end;
theorem Th1:
(for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j))
& f is one-to-one unfolded s.n.c. special implies ex g st g is_sequence_on G &
g is one-to-one unfolded s.n.c. special & L~f = L~g & f/.1 = g/.1 & f/.len f =
g/.len g & len f <= len g
proof
defpred P[Nat] means for f st len f = $1 & (for n st n in dom f
ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) & f is one-to-one unfolded s.n.c.
special ex g st g is_sequence_on G & g is one-to-one unfolded s.n.c. special &
L~f=L~g & f/.1=g/.1 & f/.len f=g/.len g & len f<=len g;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
let f such that
A3: len f=k+1 and
A4: for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j) and
A5: f is one-to-one and
A6: f is unfolded and
A7: f is s.n.c. and
A8: f is special;
per cases;
suppose
A9: k=0;
take g=f;
A10: dom f = {1} by A3,A9,FINSEQ_1:2,def 3;
now
let n;
assume that
A11: n in dom g and
A12: n+1 in dom g;
n=1 by A10,A11,TARSKI:def 1;
hence for i1,i2,j1,j2 be Nat st [i1,i2] in Indices G & [j1,
j2] in Indices G & g/.n=G*(i1,i2) & g/.(n+1)=G*(j1,j2)
holds |.i1-j1.|+|.i2-j2.|=1 by A10,A12,TARSKI:def 1;
end;
hence g is_sequence_on G by A4,GOBOARD1:def 9;
thus thesis by A5,A6,A7,A8;
end;
suppose
A13: k<>0;
A14: len (f|k)=k by A3,FINSEQ_1:59,NAT_1:11;
set f1=f|k;
A15: f1 is unfolded by A3,A6,A13,Lm1;
A16: f1 is s.n.c. by A7,GOBOARD2:7;
f1 = f|Seg k by FINSEQ_1:def 16;
then
A17: f1 is one-to-one by A5,FUNCT_1:52;
A18: dom G = Seg len G by FINSEQ_1:def 3;
1<=len f by A3,NAT_1:11;
then
A19: k+1 in dom f by A3,FINSEQ_3:25;
then consider j1,j2 be Nat such that
A20: [j1,j2] in Indices G and
A21: f/.(k+1)=G*(j1,j2) by A4;
A22: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
then
A23: j1 in dom G by A20,ZFMISC_1:87;
A24: 0+1<=k by A13,NAT_1:13;
then
A25: 1 in Seg k by FINSEQ_1:1;
A26: k<=k+1 by NAT_1:11;
then
A27: k in dom f by A3,A24,FINSEQ_3:25;
then consider i1,i2 be Nat such that
A28: [i1,i2] in Indices G and
A29: f/.k=G*(i1,i2) by A4;
reconsider l1 = Line(G,i1), c1 = Col(G,i2) as FinSequence of TOP-REAL 2;
set x1 = X_axis(l1), y1 = Y_axis(l1), x2 = X_axis(c1), y2 = Y_axis(c1);
A30: dom y1=Seg len y1 & len y1=len l1 by FINSEQ_1:def 3,GOBOARD1:def 2;
A31: dom(f|k)=Seg len(f|k) by FINSEQ_1:def 3;
A32: f1 is special
proof
let n be Nat;
assume that
A33: 1<=n and
A34: n+1 <= len f1;
n+1 in dom f1 by A33,A34,SEQ_4:134;
then
A35: f1/.(n+1)=f/.(n+1) by A27,A14,A31,FINSEQ_4:71;
len f1 <=len f by A3,A26,FINSEQ_1:59;
then
A36: n+1 <= len f by A34,XXREAL_0:2;
n in dom f1 by A33,A34,SEQ_4:134;
then f1/.n=f/.n by A27,A14,A31,FINSEQ_4:71;
hence thesis by A8,A33,A35,A36;
end;
now
let n;
assume
A37: n in dom f1;
then n in dom f by A27,A14,A31,FINSEQ_4:71;
then consider i,j such that
A38: [i,j] in Indices G & f/.n=G*(i,j) by A4;
take i,j;
thus [i,j] in Indices G & f1/.n=G*(i,j) by A27,A14,A31,A37,A38,
FINSEQ_4:71;
end;
then consider g1 such that
A39: g1 is_sequence_on G and
A40: g1 is one-to-one and
A41: g1 is unfolded and
A42: g1 is s.n.c. and
A43: g1 is special and
A44: L~g1=L~f1 and
A45: g1/.1=f1/.1 and
A46: g1/.len g1=f1/.len f1 and
A47: len f1<=len g1 by A2,A14,A17,A15,A16,A32;
A48: for n st n in dom g1 & n+1 in dom g1 holds for m,k,i,j st [m,k] in
Indices G & [i,j] in Indices G & g1/.n = G*(m,k) & g1/.(n+1) = G*(i,j) holds
|.m-i.|+|.k-j.| = 1 by A39,GOBOARD1:def 9;
A49: 1<k implies rng g1 c= L~f1
proof
assume 1<k;
then
A50: 1+1<=k by NAT_1:13;
let x be object;
assume x in rng g1;
then ex n being Element of NAT st n in dom g1 & g1/.n=x by PARTFUN2:2;
hence thesis by A14,A44,A47,A50,GOBOARD1:1,XXREAL_0:2;
end;
A51: k in Seg k by A24,FINSEQ_1:1;
A52: k=1 implies L~g1={} & rng g1 = {f/.k}
proof
A53: g1/.len g1=f/.k by A27,A14,A51,A46,FINSEQ_4:71;
assume
A54: k=1;
hence L~g1={} by A14,A44,TOPREAL1:22;
then
A55: len g1=1 or len g1=0 by TOPREAL1:22;
A56: rng g1 c= {f/.k}
proof
let x be object;
assume x in rng g1;
then consider n being Element of NAT such that
A57: n in dom g1 and
A58: g1/.n=x by PARTFUN2:2;
n in Seg len g1 by A57,FINSEQ_1:def 3;
then n=len g1 by A55,FINSEQ_1:2,TARSKI:def 1;
hence thesis by A53,A58,TARSKI:def 1;
end;
1<=len g1 by A3,A47,A54,FINSEQ_1:59;
then len g1 in dom g1 by FINSEQ_3:25;
then f/.k in rng g1 by A53,PARTFUN2:2;
then {f/.k} c= rng g1 by ZFMISC_1:31;
hence thesis by A56;
end;
A59: len c1 = len G by MATRIX_0:def 8;
then
A60: dom c1 = Seg len G by FINSEQ_1:def 3
.= dom G by FINSEQ_1:def 3;
A61: dom y2=Seg len y2 & len y2=len c1 by FINSEQ_1:def 3,GOBOARD1:def 2;
A62: dom x1=Seg len x1 & len x1=len l1 by FINSEQ_1:def 3,GOBOARD1:def 1;
A63: dom x2= Seg len x2 by FINSEQ_1:def 3;
A64: len x2=len c1 by GOBOARD1:def 1;
then
A65: dom c1 = Seg len x2 by FINSEQ_1:def 3
.= dom x2 by FINSEQ_1:def 3;
A66: i1 in dom G by A28,A22,ZFMISC_1:87;
then
A67: x1 is constant by GOBOARD1:def 4;
A68: i2 in Seg width G by A28,A22,ZFMISC_1:87;
then
A69: x2 is increasing by GOBOARD1:def 7;
A70: y2 is constant by A68,GOBOARD1:def 5;
A71: y1 is increasing by A66,GOBOARD1:def 6;
A72: len l1=width G by MATRIX_0:def 7;
then
A73: Seg width G = dom l1 by FINSEQ_1:def 3;
A74: j2 in Seg width G by A20,A22,ZFMISC_1:87;
A75: for n st n in dom g1 ex m,k st [m,k] in Indices G & g1/.n=G*(m,k)
by A39,GOBOARD1:def 9;
now
per cases by A8,A27,A28,A29,A19,A20,A21,GOBOARD2:11;
suppose
A76: i1=j1;
set ppi = G*(i1,i2), pj = G*(i1,j2);
now
per cases by XXREAL_0:1;
case
A77: i2>j2;
l1/.i2=l1.i2 by A68,A73,PARTFUN1:def 6;
then
A78: l1/.i2=ppi by A68,MATRIX_0:def 7;
then
A79: y1.i2=ppi`2 by A68,A30,A72,GOBOARD1:def 2;
l1/.j2 = l1.j2 by A74,A73,PARTFUN1:def 6;
then
A80: l1/.j2=pj by A74,MATRIX_0:def 7;
then
A81: y1.j2=pj`2 by A74,A30,A72,GOBOARD1:def 2;
then
A82: pj`2<ppi`2 by A68,A74,A71,A30,A72,A77,A79,SEQM_3:def 1;
reconsider l=i2-j2 as Element of NAT by A77,INT_1:5;
defpred P1[Nat,set] means for m st m=i2-$1 holds $2=G*(i1,m);
set lk={w where w is Point of TOP-REAL 2: w`1=ppi`1 & pj`2<=w`2
& w`2<= ppi`2};
A83: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
A84: now
let n;
assume n in Seg l;
then
A85: n<=l by FINSEQ_1:1;
l<=i2 by XREAL_1:43;
then reconsider w=i2-n as Element of NAT by A85,INT_1:5
,XXREAL_0:2;
i2-n<=i2 & i2<=width G by A68,FINSEQ_1:1,XREAL_1:43;
then
A86: w<=width G by XXREAL_0:2;
A87: 1<=j2 by A74,FINSEQ_1:1;
i2-l<=i2-n by A85,XREAL_1:13;
then 1<=w by A87,XXREAL_0:2;
then w in Seg width G by A86,FINSEQ_1:1;
hence
i2-n is Element of NAT & [i1,i2-n] in Indices G & i2-n in
Seg width G by A22,A66,ZFMISC_1:87;
end;
A88: now
let n be Nat;
assume n in Seg l;
then reconsider m=i2-n as Element of NAT by A84;
take p=G*(i1,m);
thus P1[n,p];
end;
consider g2 such that
A89: len g2=l & for n being Nat st n in Seg l holds P1[n,g2
/.n] from FINSEQ_4:sch 1(A88);
take g=g1^g2;
A90: dom g2 = Seg l by A89,FINSEQ_1:def 3;
now
let n;
assume
A91: n in dom g2;
then i2-n is Element of NAT by A84,A90;
then reconsider m=i2-n as Nat;
take k=i1,m;
thus [k,m] in Indices G & g2/.n=G*(k,m) by A84,A89,A90,A91;
end;
then
A92: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*
(i,j) by A75,GOBOARD1:23;
A93: dom g2=Seg len g2 by FINSEQ_1:def 3;
A94: x1.i2=ppi`1 by A68,A62,A72,A78,GOBOARD1:def 1;
A95: now
let n,p;
assume that
A96: n in dom g2 and
A97: g2/.n=p;
reconsider n1=i2-n as Element of NAT by A84,A90,A96;
n<=len g2 by A96,FINSEQ_3:25;
then
A98: i2-len g2<= n1 by XREAL_1:13;
set pn = G*(i1,n1);
A99: g2/.n=pn by A89,A93,A96;
A100: i2-n in Seg width G by A84,A89,A93,A96;
then
A101: x1.n1=x1.i2 by A68,A67,A62,A72,SEQM_3:def 10;
l1/.n1=l1.n1 by A73,A100,PARTFUN1:def 6;
then
A102: l1/.n1=pn by A100,MATRIX_0:def 7;
then
A103: y1.n1=pn`2 by A30,A72,A100,GOBOARD1:def 2;
x1.n1=pn`1 by A62,A72,A100,A102,GOBOARD1:def 1;
hence
p`1=ppi`1 & pj`2<=p`2 & p`2<=ppi`2 by A68,A74,A71,A30,A72,A89
,A79,A81,A94,A97,A100,A99,A98,A101,A103,SEQ_4:137,XREAL_1:43;
dom l1 = Seg len l1 by FINSEQ_1:def 3;
hence p in rng l1 by A72,A97,A100,A99,A102,PARTFUN2:2;
1<=n by A96,FINSEQ_3:25;
then n1<i2 by XREAL_1:44;
hence p`2<ppi`2 by A68,A71,A30,A72,A79,A97,A100,A99,A103,
SEQM_3:def 1;
end;
A104: g2 is special
proof
let n be Nat;
set p = g2/.n;
assume
A105: 1<=n & n+1 <= len g2;
then n in dom g2 by SEQ_4:134;
then
A106: p`1=ppi`1 by A95;
n+1 in dom g2 by A105,SEQ_4:134;
hence thesis by A95,A106;
end;
A107: now
let n,m,p,q;
assume that
A108: n in dom g2 and
A109: m in dom g2 and
A110: n<m and
A111: g2/.n=p & g2/.m=q;
A112: i2-n in Seg width G by A84,A90,A108;
reconsider n1=i2-n, m1=i2-m as Element of NAT by A84,A90,A108
,A109;
set pn = G*(i1,n1), pm = G*(i1,m1);
A113: m1<n1 by A110,XREAL_1:15;
l1/.n1=l1.n1 by A73,A84,A90,A108,PARTFUN1:def 6;
then l1/.n1=pn by A112,MATRIX_0:def 7;
then
A114: y1.n1=pn`2 by A30,A72,A112,GOBOARD1:def 2;
A115: i2-m in Seg width G by A84,A90,A109;
l1/.m1 = l1.m1 by A73,A84,A90,A109,PARTFUN1:def 6;
then l1/.m1= pm by A115,MATRIX_0:def 7;
then
A116: y1.m1=pm`2 by A30,A72,A115,GOBOARD1:def 2;
g2/.n=pn & g2/.m=pm by A89,A90,A108,A109;
hence q`2<p`2 by A71,A30,A72,A111,A112,A115,A113,A114,A116,
SEQM_3:def 1;
end;
for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom
g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m)
proof
let n,m;
assume that
A117: m>n+1 and
A118: n in dom g2 and
A119: n+1 in dom g2 and
A120: m in dom g2 and
A121: m+1 in dom g2 and
A122: LSeg(g2,n) /\ LSeg(g2,m) <> {};
reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as
Point of TOP-REAL 2;
A123: p1`1=ppi`1 & p2`1= ppi`1 by A95,A118,A119;
n<n+1 by NAT_1:13;
then
A124: p2`2<p1`2 by A107,A118,A119;
set lp = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & p2`2<=
w`2 & w`2<=p1`2}, lq = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & q2`2<=w`2
& w`2<=q1`2};
A125: p1=|[p1`1,p1`2]| & p2=|[p2`1,p2`2]| by EUCLID:53;
m<m+1 by NAT_1:13;
then
A126: q2`2<q1`2 by A107,A120,A121;
A127: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
set x = the Element of LSeg(g2,n) /\ LSeg(g2,m);
A128: x in LSeg(g2,n) by A122,XBOOLE_0:def 4;
A129: q1`1= ppi`1 & q2`1=ppi`1 by A95,A120,A121;
A130: x in LSeg(g2,m) by A122,XBOOLE_0:def 4;
1 <= m & m+1<= len g2 by A120,A121,FINSEQ_3:25;
then LSeg(g2,m) = LSeg(q2,q1) by TOPREAL1:def 3
.=lq by A126,A129,A127,TOPREAL3:9;
then
A131: ex tm be Point of TOP-REAL 2 st tm=x & tm`1=ppi`1 & q2`2
<=tm`2 & tm`2<=q1`2 by A130;
1 <= n & n+1 <= len g2 by A118,A119,FINSEQ_3:25;
then LSeg(g2,n) = LSeg(p2,p1) by TOPREAL1:def 3
.=lp by A124,A123,A125,TOPREAL3:9;
then
A132: ex tn be Point of TOP-REAL 2 st tn=x & tn`1=ppi`1 & p2`2
<=tn`2 & tn`2<=p1`2 by A128;
q1`2<p2`2 by A107,A117,A119,A120;
hence contradiction by A132,A131,XXREAL_0:2;
end;
then
A133: g2 is s.n.c. by GOBOARD2:1;
A134: not f/.k in L~g2
proof
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume f/.k in L~g2;
then consider X be set such that
A135: f/.k in X and
A136: X in ls by TARSKI:def 4;
consider m such that
A137: X=LSeg(g2,m) and
A138: 1<=m & m+1 <= len g2 by A136;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A139: m in dom g2 by A138,SEQ_4:134;
then
A140: q1`1=ppi`1 by A95;
set lq={w where w is Point of TOP-REAL 2: w`1=ppi`1 & q2`2<=w
`2 & w`2<=q1`2};
A141: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
A142: m+1 in dom g2 by A138,SEQ_4:134;
then
A143: q2`1=ppi`1 by A95;
m<m+1 by NAT_1:13;
then
A144: q2`2<q1`2 by A107,A139,A142;
LSeg(g2,m)=LSeg(q2,q1) by A138,TOPREAL1:def 3
.=lq by A140,A143,A144,A141,TOPREAL3:9;
then ex p st p=f/.k & p`1=ppi`1 & q2`2<=p`2 & p`2<=q1`2 by A135
,A137;
hence contradiction by A29,A95,A139;
end;
x1.j2 =pj`1 by A74,A62,A72,A80,GOBOARD1:def 1;
then
A145: ppi`1=pj`1 by A68,A74,A67,A62,A72,A94,SEQM_3:def 10;
now
let n,m be Element of NAT;
assume that
A146: n in dom g2 & m in dom g2 and
A147: n<>m;
reconsider n1=i2-n, m1=i2-m as Element of NAT by A84,A90,A146;
A148: g2/.n=G*(i1,n1) & g2/.m=G*(i1,m1) by A89,A90,A146;
assume
A149: g2/.n=g2/.m;
[i1,i2-n] in Indices G & [i1,i2-m] in Indices G by A84,A90,A146
;
then n1=m1 by A148,A149,GOBOARD1:5;
hence contradiction by A147;
end;
then for n,m being Element of NAT
st n in dom g2 & m in dom g2 & g2/.n = g2/.m holds
n = m;
then
A150: g2 is one-to-one by PARTFUN2:9;
reconsider m1=i2-l as Element of NAT by ORDINAL1:def 12;
A151: pj=|[pj`1,pj`2]| by EUCLID:53;
A152: LSeg(f,k)=LSeg(pj,ppi) by A3,A24,A29,A21,A76,TOPREAL1:def 3
.= lk by A82,A145,A83,A151,TOPREAL3:9;
A153: rng g2 c= LSeg(f,k)
proof
let x be object;
assume x in rng g2;
then consider n being Element of NAT such that
A154: n in dom g2 and
A155: g2/.n=x by PARTFUN2:2;
reconsider n1=i2-n as Element of NAT by A84,A89,A93,A154;
set pn = G*(i1,n1);
A156: g2/.n=pn by A89,A93,A154;
then
A157: pn`2<=ppi`2 by A95,A154;
pn`1=ppi`1 & pj`2<=pn`2 by A95,A154,A156;
hence thesis by A152,A155,A156,A157;
end;
A158: now
let n;
assume that
A159: n in dom g2 and
A160: n+1 in dom g2;
reconsider m1=i2-n,m2=i2-(n+1) as Element of NAT by A84,A90
,A159,A160;
let l1,l2,l3,l4 be Nat;
assume that
A161: [l1,l2] in Indices G and
A162: [l3,l4] in Indices G and
A163: g2/.n=G*(l1,l2) and
A164: g2/.(n+1)=G*(l3,l4);
[i1,i2-(n+1)] in Indices G & g2/.(n+1)=G*(i1,m2) by A84,A89,A90
,A160;
then
A165: l3=i1 & l4=m2 by A162,A164,GOBOARD1:5;
[i1,i2-n] in Indices G & g2/.n=G*(i1,m1) by A84,A89,A90,A159;
then l1=i1 & l2=m1 by A161,A163,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= 0+|.i2-n-(i2-(n+1)).| by A165,
ABSVALUE:2
.= 1 by ABSVALUE:def 1;
end;
now
let l1,l2,l3,l4 be Nat;
assume that
A166: [l1,l2] in Indices G and
A167: [l3,l4] in Indices G and
A168: g1/.len g1=G*(l1,l2) and
A169: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A170: 1 in dom g2;
reconsider m1=i2-1 as Element of NAT by A84,A90,A170;
[i1,i2-1] in Indices G & g2/.1=G*(i1,m1) by A84,A89,A90,A170;
then
A171: l3=i1 & l4=m1 by A167,A169,GOBOARD1:5;
f1/.len f1=f/.k by A27,A14,A51,FINSEQ_4:71;
then l1=i1 & l2=i2 by A46,A28,A29,A166,A168,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=0+|.i2-(i2-1).| by A171,ABSVALUE:2
.=1 by ABSVALUE:def 1;
end;
then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [m
,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A48,A158,GOBOARD1:24;
hence g is_sequence_on G by A92,GOBOARD1:def 9;
A172: LSeg(f,k)=LSeg(ppi,pj) by A3,A24,A29,A21,A76,TOPREAL1:def 3;
A173: not f/.k in rng g2
proof
assume f/.k in rng g2;
then consider n being Element of NAT such that
A174: n in dom g2 and
A175: g2/.n=f/.k by PARTFUN2:2;
reconsider n1=i2-n as Element of NAT by A84,A89,A93,A174;
[i1,i2-n] in Indices G & g2/.n=G*(i1,n1) by A84,A89,A93,A174;
then
A176: n1=i2 by A28,A29,A175,GOBOARD1:5;
0<n by A93,A174,FINSEQ_1:1;
hence contradiction by A176;
end;
rng g1 /\ rng g2 = {}
proof
set x = the Element of rng g1 /\ rng g2;
assume
A177: not thesis;
then
A178: x in rng g2 by XBOOLE_0:def 4;
A179: x in rng g1 by A177,XBOOLE_0:def 4;
now
per cases by A24,XXREAL_0:1;
suppose
k=1;
hence contradiction by A52,A173,A179,A178,TARSKI:def 1;
end;
suppose
1<k;
then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k} by
A3,A6,A7,A49,A153,A179,A178,GOBOARD2:4,XBOOLE_0:def 4;
hence contradiction by A173,A178,TARSKI:def 1;
end;
end;
hence contradiction;
end;
then rng g1 misses rng g2;
hence g is one-to-one by A40,A150,FINSEQ_3:91;
A180: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2,
n+1) = {g2/.(n+1)}
proof
let n;
assume that
A181: 1<=n and
A182: n+2 <= len g2;
A183: n+1 in dom g2 by A181,A182,SEQ_4:135;
then g2/.(n+1) in rng g2 by PARTFUN2:2;
then g2/.(n+1) in lk by A152,A153;
then consider u1 be Point of TOP-REAL 2 such that
A184: g2/.(n+1)=u1 and
A185: u1`1=ppi`1 and
pj`2<=u1`2 and
u1`2<=ppi`2;
A186: n+2 in dom g2 by A181,A182,SEQ_4:135;
then g2/.(n+2) in rng g2 by PARTFUN2:2;
then g2/.(n+2) in lk by A152,A153;
then consider u2 be Point of TOP-REAL 2 such that
A187: g2/.(n+2)=u2 and
A188: u2`1=ppi`1 and
pj`2<=u2`2 and
u2`2<=ppi`2;
n+(1+1) = n+1+1 & 1 <= n+1 by NAT_1:11;
then
A189: LSeg(g2,n+1)=LSeg(u1,u2) by A182,A184,A187,TOPREAL1:def 3;
n+1<n+1+1 by NAT_1:13;
then
A190: u2`2<u1`2 by A107,A183,A186,A184,A187;
A191: n in dom g2 by A181,A182,SEQ_4:135;
then g2/.n in rng g2 by PARTFUN2:2;
then g2/.n in lk by A152,A153;
then consider u be Point of TOP-REAL 2 such that
A192: g2/.n=u and
A193: u`1=ppi`1 and
pj`2<=u`2 and
u`2<=ppi`2;
n+1 <= n+2 by XREAL_1:6;
then n+1 <= len g2 by A182,XXREAL_0:2;
then
A194: LSeg(g2,n)=LSeg(u,u1) by A181,A192,A184,TOPREAL1:def 3;
set lg = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & u2`2<=
w`2 & w`2<=u`2};
n<n+1 by NAT_1:13;
then
A195: u1`2<u`2 by A107,A191,A183,A192,A184;
then
A196: u1 in lg by A185,A190;
u=|[u`1,u`2]| & u2=|[u2`1,u2`2 ]| by EUCLID:53;
then LSeg(g2/.n,g2/.(n+2))=lg by A192,A193,A187,A188,A190,A195,
TOPREAL3:9,XXREAL_0:2;
hence thesis by A192,A184,A187,A194,A189,A196,TOPREAL1:8;
end;
thus g is unfolded
proof
let n be Nat;
assume that
A197: 1<=n and
A198: n+2 <= len g;
A199: n+1+1<=len g by A198;
A200: n+(1+1)=n+1+1;
A201: n<=n+1 by NAT_1:11;
n+1<=n+1+1 by NAT_1:11;
then
A202: n+1 <= len g by A198,XXREAL_0:2;
A203: len g=len g1+len g2 by FINSEQ_1:22;
n+2-len g1 = n-len g1 +2;
then
A204: n-len g1 + 2 <= len g2 by A198,A203,XREAL_1:20;
A205: 1 <= n+1 & n+1+1 = n+(1+1) by NAT_1:11;
per cases;
suppose
A206: n+2 <= len g1;
A207: n+(1+1)=n+1+1;
A208: n+1 in dom g1 by A197,A206,SEQ_4:135;
then
A209: g/.(n+1)=g1/.(n+1) by FINSEQ_4:68;
n in dom g1 by A197,A206,SEQ_4:135;
then
A210: LSeg(g1,n)=LSeg(g,n) by A208,TOPREAL3:18;
n+2 in dom g1 by A197,A206,SEQ_4:135;
then LSeg(g1,n+1)=LSeg(g,n+1) by A208,A207,TOPREAL3:18;
hence thesis by A41,A197,A206,A210,A209;
end;
suppose
len g1 < n+2;
then len g1+1<=n+2 by NAT_1:13;
then
A211: len g1<=n+2-1 by XREAL_1:19;
now
per cases;
suppose
A212: len g1=n+1;
now
1<len g1 by A197,A212,NAT_1:13;
then
A213: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A213,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A214: L~f1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,GOBOARD2:4;
g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1) by A197
,A198,A202,A205,TOPREAL1:21;
then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by
XBOOLE_0:def 4;
then
A215: {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:31;
A216: 1<=len g-len g1 by A199,A212,XREAL_1:19;
then 1 in dom g2 by A203,FINSEQ_3:25;
then
A217: g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A152,A153;
then consider u1 be Point of TOP-REAL 2 such that
A218: g2/.1=u1 and
u1`1=ppi`1 and
pj`2<=u1`2 and
u1`2<=ppi`2;
ppi in LSeg(ppi,pj) by RLTOPSP1:68;
then
A219: LSeg(ppi,u1) c= LSeg(f,k) by A172,A153,A217,A218,
TOPREAL1:6;
1<=n+1 by NAT_1:11;
then
A220: n+1 in dom g1 by A212,FINSEQ_3:25;
then
A221: g/.(n+1)=f1/.len f1 by A46,A212,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
n in dom g1 by A197,A201,A212,FINSEQ_3:25;
then
A222: LSeg(g,n)=LSeg(g1,n) by A220,TOPREAL3:18;
g/.(n+2)=g2/.1 by A200,A203,A212,A216,SEQ_4:136;
then
A223: LSeg(g,n+1)=LSeg(ppi,u1 ) by A198,A205,A221,A218,
TOPREAL1:def 3;
LSeg(g1,n) c= L~f1 by A44,TOPREAL3:19;
then LSeg(g,n) /\ LSeg(g,n+1) c= {g /.(n+1)} by A29,A214
,A222,A221,A219,A223,XBOOLE_1:27;
hence thesis by A215;
end;
suppose
len g1<>n+1;
then len g1<n+1 by A211,XXREAL_0:1;
then
A224: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A225: len g1=n;
then 1 <= len g2 by A202,A203,XREAL_1:6;
then
A226: g/.(n+1)=g2/.1 by A225,SEQ_4:136;
A227: 0+2<=len g2 by A198,A203,A225,XREAL_1:6;
then 1<=len g2 by XXREAL_0:2;
then
A228: 1 in dom g2 by FINSEQ_3:25;
then g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A152,A153;
then consider u1 be Point of TOP-REAL 2 such that
A229: g2/.1=u1 and
A230: u1`1=ppi`1 and
pj`2<=u1`2 and
A231: u1`2<=ppi`2;
A232: 2 in dom g2 by A227,FINSEQ_3:25;
then g2/.2 in rng g2 by PARTFUN2:2;
then g2/.2 in lk by A152,A153;
then consider u2 be Point of TOP-REAL 2 such that
A233: g2 /.2=u2 and
A234: u2`1=ppi`1 and
pj`2<=u2`2 and
A235: u2`2<=ppi`2;
set lg = {w where w is Point of TOP-REAL 2 : w`1=ppi
`1 & u2`2<=w`2 & w`2<=ppi`2};
u2`2<u1`2 by A107,A228,A232,A229,A233;
then
A236: u1 in lg by A230,A231;
u2=|[u2`1,u2`2]| by EUCLID:53;
then
A237: LSeg
(ppi,g2/.2)=lg by A83,A233,A234,A235,TOPREAL3:9;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then g/.n=f1/.len f1 by A46,A225,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
then
A238: LSeg(g,n)=LSeg(ppi,u1) by A197,A202,A226,A229,
TOPREAL1:def 3;
2 <= len g2 by A198,A203,A225,XREAL_1:6;
then g/.(n+2)=g2/.2 by A225,SEQ_4:136;
then
LSeg(g,n+1)=LSeg(u1,u2) by A198,A205,A226,A229,A233,TOPREAL1:def 3;
hence thesis by A226,A229,A233,A236,A238,A237,
TOPREAL1:8;
end;
suppose
len g1<>n;
then
A239: len g1<n by A224,XXREAL_0:1;
then len g1+1<=n by NAT_1:13;
then
A240: 1<=n1 by XREAL_1:19;
n1 + len g1 = n;
then
A241: LSeg(g,n)=LSeg(g2,n1) by A202,A239,GOBOARD2:5;
A242: n+1 = n1+1+len g1;
n1 + 1 + len g1 = n + 1;
then n1+1 <= len g2 by A202,A203,XREAL_1:6;
then
A243: g/.(n+1)=g2/.(n1+1) by A242,NAT_1:11,SEQ_4:136;
len g1<n+1 by A201,A239,XXREAL_0:2;
then LSeg (g,n+1)=LSeg(g2,n1+1) by A199,A242,
GOBOARD2:5;
hence thesis by A180,A204,A241,A243,A240;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
A244: L~g2 c= LSeg(f,k)
proof
let x be object;
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume x in L~g2;
then consider X be set such that
A245: x in X and
A246: X in ls by TARSKI:def 4;
consider m such that
A247: X=LSeg(g2,m) and
A248: 1<=m & m+1 <= len g2 by A246;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A249: LSeg(g2,m)=LSeg(q1,q2) by A248,TOPREAL1:def 3;
m+1 in dom g2 by A248,SEQ_4:134;
then
A250: g2/.(m+1) in rng g2 by PARTFUN2:2;
m in dom g2 by A248,SEQ_4:134;
then g2/.m in rng g2 by PARTFUN2:2;
then LSeg(q1,q2) c= LSeg(ppi,pj) by A172,A153,A250,TOPREAL1:6;
hence thesis by A172,A245,A247,A249;
end;
A251: L~g1 /\ L~g2 = {}
proof
per cases;
suppose
k=1;
hence thesis by A52;
end;
suppose
k<>1;
then 1<k by A24,XXREAL_0:1;
then L~g1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,A44,GOBOARD2:4;
then
A252: L~g1 /\ L~g2 c= {f/.k} by A244,XBOOLE_1:26;
now
set x = the Element of L~g1 /\ L~g2;
assume L~g1 /\ L~g2 <> {};
then x in {f/.k} & x in L~g2 by A252,XBOOLE_0:def 4;
hence contradiction by A134,TARSKI:def 1;
end;
hence thesis;
end;
end;
for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g
& m+1 in dom g holds LSeg(g,n) misses LSeg(g,m)
proof
A253: 1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A254: g/.len g1=g1/.len g1 by FINSEQ_4:68
.= ppi by A27,A14,A51,A46,A29,FINSEQ_4:71;
reconsider qq=g2/.1 as Point of TOP-REAL 2;
set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j):
1<=j & j+1 <= len g2};
let n,m;
assume that
A255: m>n+1 and
A256: n in dom g and
A257: n+1 in dom g and
A258: m in dom g and
A259: m+1 in dom g;
A260: 1<=n by A256,FINSEQ_3:25;
j2+1<=i2 by A77,NAT_1:13;
then
A261: 1<=l by XREAL_1:19;
then
A262: 1 in dom g2 by A89,FINSEQ_3:25;
then
A263: qq`1=ppi`1 & qq`2<ppi`2 by A95;
A264: g/.(len g1+1)=qq by A89,A261,SEQ_4:136;
A265: pj`2<=qq`2 by A95,A262;
A266: m+1<=len g by A259,FINSEQ_3:25;
A267: 1<=m+1 by A259,FINSEQ_3:25;
A268: 1<=n+1 by A257,FINSEQ_3:25;
A269: n+1<=len g by A257,FINSEQ_3:25;
A270: qq=|[qq`1,qq`2]| by EUCLID:53;
A271: 1<=m by A258,FINSEQ_3:25;
set ql={z where z is Point of TOP-REAL 2: z`1=ppi`1 & qq`2<=z
`2 & z`2<=ppi`2};
A272: n<=n+1 by NAT_1:11;
A273: len g=len g1+len g2 by FINSEQ_1:22;
then len g1+1<=len g by A89,A261,XREAL_1:7;
then
A274: LSeg (g,len g1)=LSeg(qq,ppi) by A253,A254,A264,TOPREAL1:def 3
.= ql by A83,A263,A270,TOPREAL3:9;
A275: m<=m+1 by NAT_1:11;
then
A276: n+1<=m+1 by A255,XXREAL_0:2;
now
per cases;
suppose
A277: m+1<=len g1;
then m<=len g1 by A275,XXREAL_0:2;
then
A278: m in dom g1 by A271,FINSEQ_3:25;
m+1 in dom g1 by A267,A277,FINSEQ_3:25;
then
A279: LSeg(g,m)=LSeg(g1,m) by A278,TOPREAL3:18;
A280: n+1<=len g1 by A276,A277,XXREAL_0:2;
then n<=len g1 by A272,XXREAL_0:2;
then
A281: n in dom g1 by A260,FINSEQ_3:25;
n+1 in dom g1 by A268,A280,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A281,TOPREAL3:18;
hence thesis by A42,A255,A279;
end;
suppose
len g1<m+1;
then
A282: len g1<=m by NAT_1:13;
then reconsider m1=m-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A283: m=len g1;
A284: LSeg(g,m) c= LSeg(f,k)
proof
let x be object;
assume x in LSeg(g,m);
then consider px be Point of TOP-REAL 2 such that
A285: px=x & px`1=ppi`1 and
A286: qq`2<=px`2 and
A287: px`2<= ppi`2 by A274,A283;
pj`2<=px`2 by A265,A286,XXREAL_0:2;
hence thesis by A152,A285,A287;
end;
n<=len g1 by A255,A272,A283,XXREAL_0:2;
then
A288: n in dom g1 by A260,FINSEQ_3:25;
now
1<len g1 by A255,A268,A283,XXREAL_0:2;
then
A289: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A289,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A290: L~f1 /\ LSeg(f,k) ={f/.k} by A3,A6,A7,GOBOARD2:4;
A291: n+1 in dom g1 by A255,A268,A283,FINSEQ_3:25;
then
A292: LSeg(g,n)=LSeg(g1,n) by A288,TOPREAL3:18;
then LSeg(g,n) in l1 by A255,A260,A283;
then LSeg(g,n) c= L~f1 by A44,ZFMISC_1:74;
then
A293: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A290,A284,
XBOOLE_1:27;
now
set x = the Element of LSeg(g,n) /\ LSeg(g,m);
assume
A294: LSeg(g,n)/\ LSeg(g,m)<>{};
then
A295: x in LSeg(g,n) by XBOOLE_0:def 4;
x in {f/.k} by A293,A294;
then
A296: x=f/.k by TARSKI:def 1;
f/.k=g1/.len g1 by A27,A14,A51,A46,FINSEQ_4:71;
hence contradiction by A40,A41,A42,A255,A283,A288
,A291,A292,A295,A296,GOBOARD2:2;
end;
hence thesis;
end;
suppose
m<>len g1;
then
A297: len g1<m by A282,XXREAL_0:1;
then len g1+1<= m by NAT_1:13;
then
A298: 1<=m1 by XREAL_1:19;
m+1 = m1+1 +len g1;
then
A299: m1+1 <= len g2 by A266,A273,XREAL_1:6;
m = m1+len g1;
then
A300: LSeg(g,m)=LSeg(g2,m1) by A266,A297,GOBOARD2:5;
then LSeg(g,m) in l2 by A298,A299;
then
A301: LSeg(g,m) c= L~g2 by ZFMISC_1:74;
now
per cases;
suppose
A302: n+1<=len g1;
then n<=len g1 by A272,XXREAL_0:2;
then
A303: n in dom g1 by A260,FINSEQ_3:25;
n+1 in dom g1 by A268,A302,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A303,TOPREAL3:18;
then LSeg(g,n) in l1 by A260,A302;
then LSeg(g,n) c= L~g1 by ZFMISC_1:74;
then LSeg(g,n) /\ LSeg(g,m) = {} by A251,A301,
XBOOLE_1:3,27;
hence thesis;
end;
suppose
len g1<n+1;
then
A304: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by
INT_1:5;
A305: n - len g1 + 1 = n + 1 - len g1;
A306: n = n1 + len g1;
now
per cases;
suppose
A307: len g1=n;
now
reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point
of TOP-REAL 2;
set x = the Element of LSeg(g,n) /\ LSeg(g,m );
set q1l={v where v is Point of TOP-REAL 2: v
`1=ppi`1 & q2`2<=v`2 & v`2<=q1`2};
A308: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by
EUCLID:53;
assume
A309: LSeg(g,n) /\ LSeg(g,m)<>{};
then
A310: x in LSeg(g,m) by XBOOLE_0:def 4;
x in LSeg(g,n) by A309,XBOOLE_0:def 4;
then
A311: ex qx be Point of TOP-REAL 2 st qx=x &
qx`1=ppi`1 & qq`2<=qx`2 & qx`2<=ppi`2 by A274,A307;
A312: m1 in dom g2 by A298,A299,SEQ_4:134;
then
A313: q1 `1=ppi`1 by A95;
A314: m1+1 in dom g2 by A298,A299,SEQ_4:134;
then
A315: q2`1=ppi`1 by A95;
m1<m1+1 by NAT_1:13;
then
A316: q2`2<q1`2 by A107,A312,A314;
LSeg(g2,m1)=LSeg(q2,q1) by A298,A299,
TOPREAL1:def 3
.=q1l by A313,A315,A316,A308,TOPREAL3:9;
then
A317: ex qy be Point of TOP-REAL 2 st qy=x &
qy`1=ppi`1 & q2`2<=qy`2 & qy`2<=q1`2 by A300,A310;
m1 > n1 + 1 & n1 + 1 >= 1 by A255,A305,
NAT_1:11,XREAL_1:9;
then m1 > 1 by XXREAL_0:2;
then q1`2 < qq`2 by A107,A262,A312;
hence contradiction by A311,A317,XXREAL_0:2;
end;
hence thesis;
end;
suppose
n<>len g1;
then len g1<n by A304,XXREAL_0:1;
then
A318: LSeg(g,n)=LSeg(g2,n1) by A269,A306,GOBOARD2:5;
m1>n1+1 by A255,A305,XREAL_1:9;
hence thesis by A133,A300,A318;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence g is s.n.c. by GOBOARD2:1;
now
set p=g1/.len g1, q=g2/.1;
j2+1<=i2 by A77,NAT_1:13;
then 1<=l by XREAL_1:19;
then 1 in dom g2 by A90,FINSEQ_1:1;
then q`1=ppi`1 by A95;
hence p`1=q`1 or p`2=q`2 by A27,A14,A51,A46,A29,FINSEQ_4:71;
end;
hence g is special by A43,A104,GOBOARD2:8;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1 <= len g}, lf = {LSeg(f,j): 1
<=j & j+1 <= len f};
A319: len g = len g1 + len g2 by FINSEQ_1:22;
A320: now
let j;
assume that
A321: len g1<=j and
A322: j<=len g;
reconsider w = j-len g1 as Element of NAT by A321,INT_1:5;
let p such that
A323: p=g/.j;
now
per cases;
suppose
A324: j=len g1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A325: g/.len g1 = f1/.len f1 by A46,FINSEQ_4:68
.= G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence p`1=G*(i1,i2)`1 by A323,A324;
thus G*(i1,j2)`2<=p`2 & p`2<=G*(i1,i2)`2 by A68,A74,A71
,A30,A72,A77,A79,A81,A323,A324,A325,SEQM_3:def 1;
dom l1 = Seg len l1 by FINSEQ_1:def 3;
hence p in rng l1 by A68,A72,A78,A323,A324,A325,
PARTFUN2:2;
end;
suppose
j<>len g1;
then len g1 < j by A321,XXREAL_0:1;
then len g1 + 1<=j by NAT_1:13;
then
A326: 1<=w by XREAL_1:19;
A327: w<=len g2 by A319,A322,XREAL_1:20;
then
A328: w in dom g2 by A326,FINSEQ_3:25;
w + len g1 = j;
then g/.j=g2/.w by A326,A327,SEQ_4:136;
hence p`1=ppi`1 & pj`2<=p`2 & p`2<= ppi`2 & p in rng l1
by A95,A323,A328;
end;
end;
hence p`1=ppi`1 & pj`2<=p`2 & p`2<=ppi`2 & p in rng l1;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A329: x in X and
A330: X in lg by TARSKI:def 4;
consider i such that
A331: X=LSeg(g,i) and
A332: 1<=i and
A333: i+1 <= len g by A330;
per cases;
suppose
A334: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A334,XXREAL_0:2;
then
A335: i in dom g1 by A332,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A334,FINSEQ_3:25;
then X=LSeg(g1,i) by A331,A335,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A332,A334;
then
A336: x in L~f1 by A44,A329,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A336;
end;
suppose
A337: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A338: i<=len g by A333,NAT_1:13;
A339: len g1<=i by A337,NAT_1:13;
then
A340: q1`1=ppi`1 by A320,A338;
A341: q1`2<=ppi`2 by A320,A339,A338;
A342: pj`2<=q1`2 by A320,A339,A338;
q2`1=ppi`1 by A320,A333,A337;
then
A343: q2=|[q1`1,q2`2 ]| by A340,EUCLID:53;
A344: q2`2<=ppi`2 by A320,A333,A337;
A345: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A332,A333,
EUCLID:53,TOPREAL1:def 3;
A346: pj`2<= q2`2 by A320,A333,A337;
now
per cases by XXREAL_0:1;
suppose
q1`2>q2`2;
then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1
`2} by A343,A345,TOPREAL3:9;
then consider p2 such that
A347: p2 =x & p2`1=q1`1 and
A348: q2`2<=p2`2 & p2`2<=q1`2 by A329,A331;
pj`2<=p2`2 & p2`2<=ppi`2 by A341,A346,A348,XXREAL_0:2;
then
A349: x in LSeg(f,k) by A152,A340,A347;
LSeg(f,k) in lf by A3,A24;
hence thesis by A349,TARSKI:def 4;
end;
suppose
q1`2=q2`2;
then LSeg(g,i)={q1} by A343,A345,RLTOPSP1:70;
then x=q1 by A329,A331,TARSKI:def 1;
then
A350: x in LSeg(f,k) by A152,A340,A342,A341;
LSeg(f,k) in lf by A3,A24;
hence thesis by A350,TARSKI:def 4;
end;
suppose
q1`2<q2`2;
then LSeg(g,i)= {p1: p1`1=q1`1 & q1`2<=p1`2 & p1`2<=
q2`2} by A343,A345,TOPREAL3:9;
then consider p2 such that
A351: p2 =x & p2`1=q1`1 and
A352: q1`2<=p2`2 & p2`2<=q2`2 by A329,A331;
pj`2<=p2`2 & p2`2<=ppi`2 by A342,A344,A352,XXREAL_0:2;
then
A353: x in LSeg(f,k) by A152,A340,A351;
LSeg(f,k) in lf by A3,A24;
hence thesis by A353,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
let x be object;
assume x in L~f;
then
A354: x in L~f1 \/ LSeg(f,k) by A3,A13,GOBOARD2:3;
per cases by A354,XBOOLE_0:def 3;
suppose
A355: x in L~f1;
L~g1 c= L~g by GOBOARD2:6;
hence thesis by A44,A355;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A356: p1=x and
A357: p1`1=ppi`1 and
A358: pj`2<=p1`2 and
A359: p1`2<=ppi`2 by A152;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g
/.$1 holds q`2>=p1`2;
A360: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A319,XREAL_1:31;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A361: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A46,A361,FINSEQ_4:68
.=G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence thesis by A359;
end;
end;
A362: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A363: P2[ma] & for n be Nat st P2[n] holds n<=ma from
NAT_1:sch 6 (A362,A360);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A364: ma=len g;
j2+1<=i2 by A77,NAT_1:13;
then
A365: 1<=l by XREAL_1:19;
then len g1+1<=ma by A89,A319,A364,XREAL_1:7;
then
A366: len g1<=ma-1 by XREAL_1:19;
then 0+1<=ma by XREAL_1:19;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
reconsider q=g/.m1 as Point of TOP-REAL 2;
A367: ma-1<=len g by A364,XREAL_1:43;
then
A368: q`1=ppi`1 by A320,A366;
A369: pj`2<=q`2 by A320,A367,A366;
set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1 & pj
`2<=e`2 & e`2<=q`2};
A370: i2-l=j2;
A371: l in dom g2 by A89,A365,FINSEQ_3:25;
then
A372: g/.ma=g2/.l by A89,A319,A364,FINSEQ_4:69
.= pj by A89,A90,A371,A370;
then p1`2<=pj`2 by A363;
then
A373: p1`2=pj`2 by A358,XXREAL_0:1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A374: 1<=m1 by A366,XXREAL_0:2;
A375: m1+1=ma;
then q=|[q`1,q`2]| & LSeg(g,m1)=LSeg(pj,q) by A364,A372
,A374,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A145,A151,A368,A369,TOPREAL3:9;
then
A376: p1 in LSeg(g,m1) by A357,A373,A369;
LSeg(g,m1) in lg by A364,A374,A375;
hence thesis by A356,A376,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A363,XXREAL_0:1;
then
A377: ma+1<=len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL
2;
set lma = {p2: p2`1=ppi`1 & qa1`2<=p2`2 & p2`2<=qa`2};
A378: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A379: p1`2<=qa`2 by A363;
A380: len g1<=ma+1 by A363,NAT_1:13;
then
A381: qa1 `1 = ppi`1 by A320,A377;
A382: now
assume p1`2<=qa1`2;
then for q holds q=g/.(ma+1) implies p1`2<=q`2;
then ma+1<=ma by A363,A377,A380;
hence contradiction by XREAL_1:29;
end;
A383: qa`1=ppi`1 & qa=|[qa`1,qa`2]| by A320,A363,EUCLID:53;
A384: 1<=ma by A24,A14,A47,A363,NAT_1:13;
then LSeg(g,ma)=LSeg(qa1,qa) by A377,TOPREAL1:def 3
.= lma by A379,A382,A381,A383,A378,TOPREAL3:9
,XXREAL_0:2;
then
A385: x in LSeg(g,ma) by A356,A357,A379,A382;
LSeg(g,ma) in lg by A377,A384;
hence thesis by A385,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
A386: len g=len g1 + len g2 by FINSEQ_1:22;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A45,FINSEQ_4:68
.=f/.1 by A27,A25,FINSEQ_4:71;
j2+1<=i2 by A77,NAT_1:13;
then
A387: 1<=l by XREAL_1:19;
then
A388: l in dom g2 by A90,FINSEQ_1:1;
hence g/.len g=g2/.l by A89,A386,FINSEQ_4:69
.=G*(i1,m1) by A89,A90,A388
.=f/.len f by A3,A21,A76;
thus len f<=len g by A3,A14,A47,A89,A387,A386,XREAL_1:7;
end;
case
A389: i2=j2;
k<>k+1;
hence contradiction by A5,A27,A29,A19,A21,A76,A389,PARTFUN2:10;
end;
case
A390: i2<j2;
l1/.i2=l1.i2 by A68,A73,PARTFUN1:def 6;
then
A391: l1/.i2=ppi by A68,MATRIX_0:def 7;
then
A392: y1.i2=ppi`2 by A68,A30,A72,GOBOARD1:def 2;
l1/.j2=l1.j2 by A74,A73,PARTFUN1:def 6;
then
A393: l1/.j2=pj by A74,MATRIX_0:def 7;
then
A394: y1.j2=pj`2 by A74,A30,A72,GOBOARD1:def 2;
then
A395: ppi`2<pj`2 by A68,A74,A71,A30,A72,A390,A392,SEQM_3:def 1;
reconsider l=j2-i2 as Element of NAT by A390,INT_1:5;
deffunc F(Nat) = G*(i1,i2+$1);
consider g2 such that
A396: len g2=l & for n being Nat st n in dom g2 holds g2/.n=
F(n) from FINSEQ_4:sch 2;
take g=g1^g2;
A397: dom g2 = Seg len g2 by FINSEQ_1:def 3;
A398: now
let n;
A399: n<=i2+n by NAT_1:11;
assume
A400: n in Seg l;
then n<=l by FINSEQ_1:1;
then
A401: i2+n<=l+i2 by XREAL_1:7;
j2<=width G by A74,FINSEQ_1:1;
then
A402: i2+n<=width G by A401,XXREAL_0:2;
1<=n by A400,FINSEQ_1:1;
then 1<=i2+n by A399,XXREAL_0:2;
hence i2+n in Seg width G by A402,FINSEQ_1:1;
hence [i1,i2+n] in Indices G by A22,A66,ZFMISC_1:87;
end;
now
let n such that
A403: n in dom g2;
take m=i1,k=i2+n;
thus [m,k] in Indices G & g2/.n=G*(m,k) by A396,A398,A397,A403;
end;
then
A404: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*
(i,j) by A75,GOBOARD1:23;
A405: x1.i2=ppi`1 by A68,A62,A72,A391,GOBOARD1:def 1;
A406: now
let n,p;
assume that
A407: n in dom g2 and
A408: g2/.n=p;
A409: g2/.n=G*(i1,i2+n) by A396,A407;
set n1=i2+n;
set pn = G*(i1,n1);
A410: i2+n in Seg width G by A396,A398,A397,A407;
then
A411: x1.n1=x1.i2 by A68,A67,A62,A72,SEQM_3:def 10;
l1/.n1=l1.n1 by A73,A396,A398,A397,A407,PARTFUN1:def 6;
then
A412: l1/.n1=pn by A410,MATRIX_0:def 7;
then
A413: y1.n1=pn`2 by A30,A72,A410,GOBOARD1:def 2;
n<=len g2 by A397,A407,FINSEQ_1:1;
then
A414: n1<=i2+len g2 by XREAL_1:7;
x1.n1=pn`1 by A62,A72,A410,A412,GOBOARD1:def 1;
hence
p`1=ppi`1 & ppi`2<=p`2 & p`2<=pj`2 by A68,A74,A71,A30,A72,A396
,A392,A394,A405,A408,A409,A410,A414,A411,A413,SEQ_4:137,XREAL_1:31;
dom l1 = Seg len l1 by FINSEQ_1:def 3;
hence p in rng l1 by A72,A408,A409,A410,A412,PARTFUN2:2;
1<=n by A397,A407,FINSEQ_1:1;
then i2<n1 by XREAL_1:29;
hence p`2>ppi`2 by A68,A71,A30,A72,A392,A408,A409,A410,A413,
SEQM_3:def 1;
end;
A415: g2 is special
proof
let n be Nat;
set p = g2/.n;
assume
A416: 1<=n & n+1 <= len g2;
then n in dom g2 by SEQ_4:134;
then
A417: p`1=ppi`1 by A406;
n+1 in dom g2 by A416,SEQ_4:134;
hence thesis by A406,A417;
end;
now
let n,m be Element of NAT;
assume that
A418: n in dom g2 & m in dom g2 and
A419: n<>m;
A420: g2/.n=G*(i1,i2+n) & g2/.m=G*(i1,i2+m) by A396,A418;
assume
A421: g2/.n=g2/.m;
[ i1,i2+n] in Indices G & [i1,i2+m] in Indices G by A396,A398
,A397,A418;
then i2+n=i2+m by A420,A421,GOBOARD1:5;
hence contradiction by A419;
end;
then for n,m being Element of NAT
st n in dom g2 & m in dom g2 & g2/.n = g2/.m holds
n = m;
then
A422: g2 is one-to-one by PARTFUN2:9;
set lk={w where w is Point of TOP-REAL 2: w`1=ppi`1 & ppi`2<=w`2
& w`2<= pj`2};
A423: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
A424: now
let n,m,p,q;
assume that
A425: n in dom g2 and
A426: m in dom g2 and
A427: n<m and
A428: g2/.n=p & g2/.m=q;
A429: i2+n in Seg width G by A396,A398,A397,A425;
set n1=i2+n, m1=i2+m;
set pn = G*(i1,n1), pm = G*(i1,m1);
A430: n1<m1 by A427,XREAL_1:8;
l1/.n1=l1.n1 by A73,A396,A398,A397,A425,PARTFUN1:def 6;
then l1/.n1=pn by A429,MATRIX_0:def 7;
then
A431: y1.n1=pn`2 by A30,A72,A429,GOBOARD1:def 2;
A432: i2+m in Seg width G by A396,A398,A397,A426;
l1/.m1 = l1.m1 by A73,A396,A398,A397,A426,PARTFUN1:def 6;
then l1/.m1=pm by A432,MATRIX_0:def 7;
then
A433: y1.m1=pm`2 by A30,A72,A432,GOBOARD1:def 2;
g2/.n=G*(i1,i2+n) & g2/.m=G*(i1,i2+m) by A396,A425,A426;
hence p`2<q`2 by A71,A30,A72,A428,A429,A432,A430,A431,A433,
SEQM_3:def 1;
end;
for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom
g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m)
proof
let n,m;
assume that
A434: m>n+1 and
A435: n in dom g2 and
A436: n+1 in dom g2 and
A437: m in dom g2 and
A438: m+1 in dom g2 and
A439: LSeg(g2,n) /\ LSeg(g2,m) <> {};
reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as
Point of TOP-REAL 2;
A440: p1`1=ppi`1 & p2`1= ppi`1 by A406,A435,A436;
n<n+1 by NAT_1:13;
then
A441: p1`2<p2`2 by A424,A435,A436;
set lp = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & p1`2<=
w`2 & w`2<=p2`2}, lq = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & q1`2<=w`2
& w`2<=q2`2};
A442: p1=|[p1`1,p1`2]| & p2=|[p2`1,p2`2]| by EUCLID:53;
m<m+1 by NAT_1:13;
then
A443: q1`2<q2`2 by A424,A437,A438;
A444: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
set x = the Element of LSeg(g2,n) /\ LSeg(g2,m);
A445: x in LSeg(g2,n) by A439,XBOOLE_0:def 4;
A446: q1`1= ppi`1 & q2`1=ppi`1 by A406,A437,A438;
A447: x in LSeg(g2,m) by A439,XBOOLE_0:def 4;
1 <= m & m+1<= len g2 by A437,A438,FINSEQ_3:25;
then LSeg(g2,m) = LSeg(q1,q2) by TOPREAL1:def 3
.=lq by A443,A446,A444,TOPREAL3:9;
then
A448: ex tm be Point of TOP-REAL 2 st tm=x & tm`1=ppi`1 & q1`2
<=tm`2 & tm`2<=q2`2 by A447;
1 <= n & n+1 <= len g2 by A435,A436,FINSEQ_3:25;
then LSeg(g2,n) = LSeg(p1,p2) by TOPREAL1:def 3
.=lp by A441,A440,A442,TOPREAL3:9;
then
A449: ex tn be Point of TOP-REAL 2 st tn=x & tn`1=ppi`1 & p1`2
<=tn`2 & tn`2<=p2`2 by A445;
p2`2<q1`2 by A424,A434,A436,A437;
hence contradiction by A449,A448,XXREAL_0:2;
end;
then
A450: g2 is s.n.c. by GOBOARD2:1;
A451: not f/.k in L~g2
proof
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume f/.k in L~g2;
then consider X be set such that
A452: f/.k in X and
A453: X in ls by TARSKI:def 4;
consider m such that
A454: X=LSeg(g2,m) and
A455: 1<=m & m+1 <= len g2 by A453;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A456: m in dom g2 by A455,SEQ_4:134;
then
A457: q1`1=ppi`1 by A406;
set lq={w where w is Point of TOP-REAL 2: w`1=ppi`1 & q1`2<=w
`2 & w`2<=q2`2};
A458: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
A459: m+1 in dom g2 by A455,SEQ_4:134;
then
A460: q2`1=ppi`1 by A406;
m<m+1 by NAT_1:13;
then
A461: q1`2<q2`2 by A424,A456,A459;
LSeg(g2,m)=LSeg(q1,q2) by A455,TOPREAL1:def 3
.=lq by A457,A460,A461,A458,TOPREAL3:9;
then ex p st p=f/.k & p`1=ppi`1 & q1`2<=p`2 & p`2<=q2`2 by A452
,A454;
hence contradiction by A29,A406,A456;
end;
x1.j2 =pj`1 by A74,A62,A72,A393,GOBOARD1:def 1;
then
A462: ppi`1=pj`1 by A68,A74,A67,A62,A72,A405,SEQM_3:def 10;
A463: now
let n;
assume that
A464: n in dom g2 and
A465: n+1 in dom g2;
let l1,l2,l3,l4 be Nat;
assume that
A466: [l1,l2] in Indices G and
A467: [l3,l4] in Indices G and
A468: g2/.n=G*(l1,l2) and
A469: g2/.(n+1)=G*(l3,l4);
g2/.(n+1)=G*(i1,i2+(n+1)) & [i1,i2+(n+1)] in Indices G
by A396,A398,A397,A465;
then
A470: l3=i1 & l4=i2+(n+1) by A467,A469,GOBOARD1:5;
g2/.n=G*(i1,i2+n) & [i1,i2+n] in Indices G by A396,A398,A397
,A464;
then l1=i1 & l2=i2+n by A466,A468,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= 0+|.i2+n-(i2+(n+1)).| by A470,
ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
now
let l1,l2,l3,l4 be Nat;
assume that
A471: [ l1,l2] in Indices G and
A472: [l3,l4] in Indices G and
A473: g1/.len g1=G*(l1,l2) and
A474: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A475: 1 in dom g2;
g2/.1=G* (i1,i2+1) & [i1,i2+1] in Indices G by A396,A398,A397
,A475;
then
A476: l3=i1 & l4=i2+1 by A472,A474,GOBOARD1:5;
f1/.len f1=f/.k by A27,A14,A51,FINSEQ_4:71;
then l1=i1 & l2=i2 by A46,A28,A29,A471,A473,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=0+|.i2-(i2+1).| by A476,ABSVALUE:2
.=|.i2-i2+-1.|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [m
,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A48,A463,GOBOARD1:24;
hence g is_sequence_on G by A404,GOBOARD1:def 9;
A477: pj=|[pj`1,pj `2]| by EUCLID:53;
A478: LSeg(f,k)=LSeg(ppi,pj) by A3,A24,A29,A21,A76,TOPREAL1:def 3
.= lk by A395,A462,A423,A477,TOPREAL3:9;
A479: rng g2 c= LSeg(f,k)
proof
let x be object;
assume x in rng g2;
then consider n being Element of NAT such that
A480: n in dom g2 and
A481: g2/.n=x by PARTFUN2:2;
set pn = G*(i1,(i2+n));
A482: g2/.n=G*(i1,i2+n) by A396,A480;
then
A483: pn`2<=pj`2 by A406,A480;
pn`1=ppi`1 & ppi`2<=pn`2 by A406,A480,A482;
hence thesis by A478,A481,A482,A483;
end;
A484: not f/.k in rng g2
proof
assume f/.k in rng g2;
then consider n being Element of NAT such that
A485: n in dom g2 and
A486: g2/.n=f/.k by PARTFUN2:2;
A487: 0<n by A485,FINSEQ_3:25;
A488: g2/.n=G*(i1,i2+n) by A396,A485;
dom g2 = Seg len g2 by FINSEQ_1:def 3;
then [i1,i2+n] in Indices G by A396,A398,A485;
then i2+n=i2 by A28,A29,A486,A488,GOBOARD1:5;
hence contradiction by A487;
end;
rng g1 /\ rng g2 = {}
proof
set x = the Element of rng g1 /\ rng g2;
assume
A489: not thesis;
then
A490: x in rng g2 by XBOOLE_0:def 4;
A491: x in rng g1 by A489,XBOOLE_0:def 4;
now
per cases by A24,XXREAL_0:1;
suppose
k=1;
hence contradiction by A52,A484,A491,A490,TARSKI:def 1;
end;
suppose
1<k;
then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k} by
A3,A6,A7,A49,A479,A491,A490,GOBOARD2:4,XBOOLE_0:def 4;
hence contradiction by A484,A490,TARSKI:def 1;
end;
end;
hence contradiction;
end;
then rng g1 misses rng g2;
hence g is one-to-one by A40,A422,FINSEQ_3:91;
A492: LSeg(f,k)=LSeg(ppi,pj) by A3,A24,A29,A21,A76,TOPREAL1:def 3;
A493: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2,
n+1) = {g2/.(n+1)}
proof
let n;
assume that
A494: 1<=n and
A495: n+2 <= len g2;
A496: n+1 in dom g2 by A494,A495,SEQ_4:135;
then g2/.(n+1) in rng g2 by PARTFUN2:2;
then g2/.(n+1) in lk by A478,A479;
then consider u1 be Point of TOP-REAL 2 such that
A497: g2/.(n+1)=u1 and
A498: u1`1=ppi`1 and
ppi`2<=u1`2 and
u1`2<=pj`2;
A499: n+2 in dom g2 by A494,A495,SEQ_4:135;
then g2/.(n+2) in rng g2 by PARTFUN2:2;
then g2/.(n+2) in lk by A478,A479;
then consider u2 be Point of TOP-REAL 2 such that
A500: g2/.(n+2)=u2 and
A501: u2`1=ppi`1 and
ppi`2<=u2`2 and
u2`2<=pj`2;
1<= n+1 & n+1+1 = n+(1+1) by NAT_1:11;
then
A502: LSeg(g2,n+1)=LSeg( u1,u2) by A495,A497,A500,TOPREAL1:def 3;
n+1<n+1+1 by NAT_1:13;
then
A503: u1`2<u2`2 by A424,A496,A499,A497,A500;
A504: n in dom g2 by A494,A495,SEQ_4:135;
then g2/.n in rng g2 by PARTFUN2:2;
then g2/.n in lk by A478,A479;
then consider u be Point of TOP-REAL 2 such that
A505: g2/.n=u and
A506: u`1=ppi`1 and
ppi`2<=u`2 and
u`2<=pj`2;
n+1 <= n+2 by XREAL_1:6;
then n+1 <= len g2 by A495,XXREAL_0:2;
then
A507: LSeg(g2,n)=LSeg(u,u1) by A494,A505,A497,TOPREAL1:def 3;
set lg = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & u`2<=w
`2 & w`2<=u2`2};
n<n+1 by NAT_1:13;
then
A508: u`2<u1`2 by A424,A504,A496,A505,A497;
then
A509: u1 in lg by A498,A503;
u=|[u`1,u`2]| & u2=|[u2`1,u2`2 ]| by EUCLID:53;
then LSeg(g2/.n,g2/.(n+2))=lg by A505,A506,A500,A501,A503,A508,
TOPREAL3:9,XXREAL_0:2;
hence thesis by A505,A497,A500,A507,A502,A509,TOPREAL1:8;
end;
thus g is unfolded
proof
let n be Nat;
assume that
A510: 1<=n and
A511: n+2 <= len g;
A512: n+1+1<=len g by A511;
n+1<=n+1+1 by NAT_1:11;
then
A513: n+1 <= len g by A511,XXREAL_0:2;
A514: len g=len g1+len g2 by FINSEQ_1:22;
n+2-len g1 = n-len g1 +2;
then
A515: n-len g1 + 2 <= len g2 by A511,A514,XREAL_1:20;
A516: 1<= n+1 by NAT_1:11;
A517: n<=n+1 by NAT_1:11;
A518: n+(1+1)=n+1+1;
per cases;
suppose
A519: n+2 <= len g1;
A520: n+(1+1)=n+1+1;
A521: n+1 in dom g1 by A510,A519,SEQ_4:135;
then
A522: g/.(n+1)=g1/.(n+1) by FINSEQ_4:68;
n in dom g1 by A510,A519,SEQ_4:135;
then
A523: LSeg(g1,n)=LSeg(g,n) by A521,TOPREAL3:18;
n+2 in dom g1 by A510,A519,SEQ_4:135;
then LSeg(g1,n+1)=LSeg(g,n+1) by A521,A520,TOPREAL3:18;
hence thesis by A41,A510,A519,A523,A522;
end;
suppose
len g1 < n+2;
then len g1+1<=n+2 by NAT_1:13;
then
A524: len g1<=n+2-1 by XREAL_1:19;
now
per cases;
suppose
A525: len g1=n+1;
now
1<len g1 by A510,A525,NAT_1:13;
then
A526: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A526,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A527: L~f1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,GOBOARD2:4;
g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1) by A510
,A511,A516,A513,A518,TOPREAL1:21;
then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by
XBOOLE_0:def 4;
then
A528: {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:31;
A529: 1<=len g-len g1 by A512,A525,XREAL_1:19;
then 1 in dom g2 by A514,FINSEQ_3:25;
then
A530: g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A478,A479;
then consider u1 be Point of TOP-REAL 2 such that
A531: g2/.1=u1 and
u1`1=ppi`1 and
ppi`2<=u1`2 and
u1`2<=pj`2;
ppi in LSeg(ppi,pj) by RLTOPSP1:68;
then
A532: LSeg(ppi,u1) c= LSeg(f,k) by A492,A479,A530,A531,
TOPREAL1:6;
1<=n+1 by NAT_1:11;
then
A533: n+1 in dom g1 by A525,FINSEQ_3:25;
then
A534: g/.(n+1)=f1/.len f1 by A46,A525,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
n in dom g1 by A510,A517,A525,FINSEQ_3:25;
then
A535: LSeg(g,n)=LSeg(g1,n) by A533,TOPREAL3:18;
g/.(n+2)=g2/.1 by A518,A514,A525,A529,SEQ_4:136;
then
A536: LSeg(g,n+1)=LSeg(ppi,u1 ) by A511,A516,A518,A534,A531,
TOPREAL1:def 3;
LSeg(g1,n) c= L~f1 by A44,TOPREAL3:19;
then LSeg(g,n) /\ LSeg(g,n+1) c= {g /.(n+1)} by A29,A527
,A535,A534,A532,A536,XBOOLE_1:27;
hence thesis by A528;
end;
suppose
len g1<>n+1;
then len g1<n+1 by A524,XXREAL_0:1;
then
A537: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A538: len g1=n;
then
A539: 2 <= len g2 by A511,A514,XREAL_1:6;
then 1 <= len g2 by XXREAL_0:2;
then
A540: g/.(n+1)=g2/.1 by A538,SEQ_4:136;
1<=len g2 by A539,XXREAL_0:2;
then
A541: 1 in dom g2 by FINSEQ_3:25;
then g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A478,A479;
then consider u1 be Point of TOP-REAL 2 such that
A542: g2/.1=u1 and
A543: u1`1=ppi`1 & ppi`2<=u1`2 and
u1`2<=pj`2;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then g/.n=f1/.len f1 by A46,A538,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
then
A544: LSeg(g,n)=LSeg(ppi,u1) by A510,A513,A540,A542,
TOPREAL1:def 3;
A545: 2 in dom g2 by A539,FINSEQ_3:25;
then g2/.2 in rng g2 by PARTFUN2:2;
then g2/.2 in lk by A478,A479;
then consider u2 be Point of TOP-REAL 2 such that
A546: g2 /.2=u2 and
A547: u2`1=ppi`1 & ppi`2<=u2`2 and
u2`2<=pj`2;
set lg = {w where w is Point of TOP-REAL 2 : w`1=ppi
`1 & ppi`2<=w`2 & w`2<=u2`2};
u1`2<u2`2 by A424,A541,A545,A542,A546;
then u2=|[u2`1,u2`2]| & u1 in lg by A543,EUCLID:53;
then
A548: u1 in LSeg(ppi,u2) by A423,A547,TOPREAL3:9;
g/.(n+2)=g2/.2 by A538,A539,SEQ_4:136;
then LSeg(g,n+1)=LSeg(u1,u2) by A511,A516,A518,A540
,A542,A546,TOPREAL1:def 3;
hence thesis by A540,A542,A544,A548,TOPREAL1:8;
end;
suppose
len g1<>n;
then
A549: len g1<n by A537,XXREAL_0:1;
then len g1+1<=n by NAT_1:13;
then
A550: 1<=n1 by XREAL_1:19;
n1 + len g1 = n;
then
A551: LSeg(g,n)=LSeg(g2,n1) by A513,A549,GOBOARD2:5;
A552: n1+1+len g1 = n+1;
then n1+1<=len g2 by A513,A514,XREAL_1:6;
then
A553: g/.(n+1)=g2/.(n1+1) by A552,NAT_1:11,SEQ_4:136;
len g1<n+1 by A517,A549,XXREAL_0:2;
then LSeg(g,n+1)=LSeg(g2,n1+1) by A512,A552,
GOBOARD2:5;
hence thesis by A493,A515,A551,A553,A550;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
A554: L~g2 c= LSeg(f,k)
proof
let x be object;
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume x in L~g2;
then consider X be set such that
A555: x in X and
A556: X in ls by TARSKI:def 4;
consider m such that
A557: X=LSeg(g2,m) and
A558: 1<=m & m+1 <= len g2 by A556;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A559: LSeg(g2,m)=LSeg(q1,q2) by A558,TOPREAL1:def 3;
m+1 in dom g2 by A558,SEQ_4:134;
then
A560: g2/.(m+1) in rng g2 by PARTFUN2:2;
m in dom g2 by A558,SEQ_4:134;
then g2/.m in rng g2 by PARTFUN2:2;
then LSeg(q1,q2) c= LSeg(ppi,pj) by A492,A479,A560,TOPREAL1:6;
hence thesis by A492,A555,A557,A559;
end;
A561: L~g1 /\ L~g2 = {}
proof
per cases;
suppose
k=1;
hence thesis by A52;
end;
suppose
k<>1;
then 1<k by A24,XXREAL_0:1;
then L~g1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,A44,GOBOARD2:4;
then
A562: L~g1 /\ L~g2 c= {f/.k} by A554,XBOOLE_1:26;
now
set x = the Element of L~g1 /\ L~g2;
assume L~g1 /\ L~g2 <> {};
then x in {f/.k} & x in L~g2 by A562,XBOOLE_0:def 4;
hence contradiction by A451,TARSKI:def 1;
end;
hence thesis;
end;
end;
for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g
& m+1 in dom g holds LSeg(g,n) misses LSeg(g,m)
proof
A563: 1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A564: g/.len g1=g1/.len g1 by FINSEQ_4:68
.= ppi by A27,A14,A51,A46,A29,FINSEQ_4:71;
reconsider qq=g2/.1 as Point of TOP-REAL 2;
set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j):
1<=j & j+1 <= len g2};
let n,m;
assume that
A565: m>n+1 and
A566: n in dom g and
A567: n+1 in dom g and
A568: m in dom g and
A569: m+1 in dom g;
A570: 1<=n by A566,FINSEQ_3:25;
i2+1<=j2 by A390,NAT_1:13;
then
A571: 1<=l by XREAL_1:19;
then
A572: 1 in dom g2 by A396,FINSEQ_3:25;
then
A573: qq`1=ppi`1 & qq`2>ppi`2 by A406;
A574: g/.(len g1+1)=qq by A396,A571,SEQ_4:136;
A575: qq`2<=pj`2 by A406,A572;
A576: m+1<=len g by A569,FINSEQ_3:25;
A577: 1<=m+1 by A569,FINSEQ_3:25;
A578: 1<=n+1 by A567,FINSEQ_3:25;
A579: n+1<=len g by A567,FINSEQ_3:25;
A580: qq=|[qq`1,qq`2]| by EUCLID:53;
A581: 1<=m by A568,FINSEQ_3:25;
set ql={z where z is Point of TOP-REAL 2: z`1=ppi`1 & ppi`2<=z
`2 & z`2<=qq`2};
A582: n<=n+1 by NAT_1:11;
A583: len g=len g1+len g2 by FINSEQ_1:22;
then len g1+1<=len g by A396,A571,XREAL_1:7;
then
A584: LSeg (g,len g1)=LSeg(ppi,qq) by A563,A564,A574,TOPREAL1:def 3
.= ql by A423,A573,A580,TOPREAL3:9;
A585: m<=m+1 by NAT_1:11;
then
A586: n+1<=m+1 by A565,XXREAL_0:2;
now
per cases;
suppose
A587: m+1<=len g1;
then m<=len g1 by A585,XXREAL_0:2;
then
A588: m in dom g1 by A581,FINSEQ_3:25;
m+1 in dom g1 by A577,A587,FINSEQ_3:25;
then
A589: LSeg(g,m)=LSeg(g1,m) by A588,TOPREAL3:18;
A590: n+1<=len g1 by A586,A587,XXREAL_0:2;
then n<=len g1 by A582,XXREAL_0:2;
then
A591: n in dom g1 by A570,FINSEQ_3:25;
n+1 in dom g1 by A578,A590,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A591,TOPREAL3:18;
hence thesis by A42,A565,A589;
end;
suppose
len g1<m+1;
then
A592: len g1<=m by NAT_1:13;
then reconsider m1=m-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A593: m=len g1;
A594: LSeg(g,m) c= LSeg(f,k)
proof
let x be object;
assume x in LSeg(g,m);
then consider px be Point of TOP-REAL 2 such that
A595: px =x & px`1=ppi`1 & ppi`2<=px`2 and
A596: px`2<= qq`2 by A584,A593;
pj`2>=px`2 by A575,A596,XXREAL_0:2;
hence thesis by A478,A595;
end;
n<=len g1 by A565,A582,A593,XXREAL_0:2;
then
A597: n in dom g1 by A570,FINSEQ_3:25;
now
1<len g1 by A565,A578,A593,XXREAL_0:2;
then
A598: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A598,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A599: L~f1 /\ LSeg(f,k) ={f/.k} by A3,A6,A7,GOBOARD2:4;
A600: n+1 in dom g1 by A565,A578,A593,FINSEQ_3:25;
then
A601: LSeg(g,n)=LSeg(g1,n) by A597,TOPREAL3:18;
then LSeg(g,n) in l1 by A565,A570,A593;
then LSeg(g,n) c= L~f1 by A44,ZFMISC_1:74;
then
A602: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A599,A594,
XBOOLE_1:27;
now
set x = the Element of LSeg(g,n)/\ LSeg(g,m);
assume
A603: LSeg(g,n)/\ LSeg(g,m)<>{};
then
A604: x in LSeg(g,n) by XBOOLE_0:def 4;
x in {f/.k} by A602,A603;
then
A605: x=f/.k by TARSKI:def 1;
f/.k=g1/.len g1 by A27,A14,A51,A46,FINSEQ_4:71;
hence contradiction by A40,A41,A42,A565,A593,A597
,A600,A601,A604,A605,GOBOARD2:2;
end;
hence thesis;
end;
suppose
m<>len g1;
then
A606: len g1<m by A592,XXREAL_0:1;
then len g1+1<= m by NAT_1:13;
then
A607: 1<=m1 by XREAL_1:19;
m+1=m1+1+len g1;
then
A608: m1+1 <= len g2 by A576,A583,XREAL_1:6;
m = m1+len g1;
then
A609: LSeg(g,m)=LSeg(g2,m1) by A576,A606,GOBOARD2:5;
then LSeg(g,m) in l2 by A607,A608;
then
A610: LSeg(g,m) c= L~g2 by ZFMISC_1:74;
now
per cases;
suppose
A611: n+1<=len g1;
then n<=len g1 by A582,XXREAL_0:2;
then
A612: n in dom g1 by A570,FINSEQ_3:25;
n+1 in dom g1 by A578,A611,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A612,TOPREAL3:18;
then LSeg(g,n) in l1 by A570,A611;
then LSeg(g,n) c= L~g1 by ZFMISC_1:74;
then LSeg(g,n) /\ LSeg(g,m) = {} by A561,A610,
XBOOLE_1:3,27;
hence thesis;
end;
suppose
len g1<n+1;
then
A613: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by
INT_1:5;
A614: n - len g1 + 1 = n + 1 - len g1;
A615: n = n1 + len g1;
now
per cases;
suppose
A616: len g1=n;
now
reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point
of TOP-REAL 2;
set x = the Element of LSeg(g,n) /\ LSeg(g,m);
set q1l={v where v is Point of TOP-REAL 2: v
`1=ppi`1 & q1`2<=v`2 & v`2<=q2`2};
A617: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]|
by EUCLID:53;
assume
A618: LSeg(g,n) /\ LSeg(g,m)<>{};
then
A619: x in LSeg(g,m) by XBOOLE_0:def 4;
x in LSeg(g,n) by A618,XBOOLE_0:def 4;
then
A620: ex qx be Point of TOP-REAL 2 st qx=x
& qx`1=ppi`1 & ppi`2<=qx`2 & qx`2<=qq`2 by A584,A616;
A621: m1 in dom g2 by A607,A608,SEQ_4:134;
then
A622: q1 `1=ppi`1 by A406;
A623: m1+1 in dom g2 by A607,A608,SEQ_4:134;
then
A624: q2`1=ppi`1 by A406;
m1<m1+1 by NAT_1:13;
then
A625: q1`2<q2`2 by A424,A621,A623;
LSeg(g2,m1)=LSeg(q1,q2) by A607,A608,
TOPREAL1:def 3
.=q1l by A622,A624,A625,A617,TOPREAL3:9;
then
A626: ex qy be Point of TOP-REAL 2 st qy=x
& qy`1=ppi`1 & q1`2<=qy`2 & qy`2<=q2`2 by A609,A619;
m1 > n1 + 1 & n1 + 1 >= 1 by A565,A614,
NAT_1:11,XREAL_1:9;
then m1 > 1 by XXREAL_0:2;
then qq`2 < q1`2 by A424,A572,A621;
hence contradiction by A620,A626,XXREAL_0:2;
end;
hence thesis;
end;
suppose
n<>len g1;
then len g1<n by A613,XXREAL_0:1;
then
A627: LSeg(g,n)=LSeg(g2,n1) by A579,A615,GOBOARD2:5;
m1>n1+1 by A565,A614,XREAL_1:9;
hence thesis by A450,A609,A627;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence g is s.n.c. by GOBOARD2:1;
now
set p=g1/.len g1, q=g2/.1;
i2+1<=j2 by A390,NAT_1:13;
then 1<=l by XREAL_1:19;
then 1 in dom g2 by A396,FINSEQ_3:25;
then q`1=ppi`1 by A406;
hence p`1=q`1 or p`2=q`2 by A27,A14,A51,A46,A29,FINSEQ_4:71;
end;
hence g is special by A43,A415,GOBOARD2:8;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1 <= len g}, lf = {LSeg(f,j): 1
<=j & j+1 <= len f};
A628: len g = len g1 + len g2 by FINSEQ_1:22;
A629: now
let j;
assume that
A630: len g1<=j and
A631: j<=len g;
reconsider w = j-len g1 as Element of NAT by A630,INT_1:5;
let p such that
A632: p=g/.j;
per cases;
suppose
A633: j=len g1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A634: g/.len g1 = f1/.len f1 by A46,FINSEQ_4:68
.= G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence p`1=G*(i1,i2)`1 by A632,A633;
thus G*(i1,i2)`2<=p`2 & p`2<=G* (i1,j2)`2 by A68,A74,A71
,A30,A72,A390,A392,A394,A632,A633,A634,SEQM_3:def 1;
dom l1 = Seg len l1 by FINSEQ_1:def 3;
hence p in rng l1 by A68,A72,A391,A632,A633,A634,PARTFUN2:2
;
end;
suppose
j<>len g1;
then len g1 < j by A630,XXREAL_0:1;
then len g1 + 1<=j by NAT_1:13;
then
A635: 1<=w by XREAL_1:19;
A636: w<=len g2 by A628,A631,XREAL_1:20;
then
A637: w in dom g2 by A635,FINSEQ_3:25;
j = w + len g1;
then g/.j=g2/.w by A635,A636,SEQ_4:136;
hence p`1=ppi`1 & ppi`2<=p`2 & p`2<= pj`2 & p in rng l1 by
A406,A632,A637;
end;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A638: x in X and
A639: X in lg by TARSKI:def 4;
consider i such that
A640: X=LSeg(g,i) and
A641: 1<=i and
A642: i+1 <= len g by A639;
per cases;
suppose
A643: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A643,XXREAL_0:2;
then
A644: i in dom g1 by A641,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A643,FINSEQ_3:25;
then X=LSeg(g1,i) by A640,A644,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A641,A643;
then
A645: x in L~f1 by A44,A638,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A645;
end;
suppose
A646: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A647: i<=len g by A642,NAT_1:13;
A648: len g1<=i by A646,NAT_1:13;
then
A649: q1 `1=ppi`1 by A629,A647;
A650: q1`2<=pj`2 by A629,A648,A647;
A651: ppi`2<=q1`2 by A629,A648,A647;
q2`1=ppi`1 by A629,A642,A646;
then
A652: q2=|[q1`1,q2`2 ]| by A649,EUCLID:53;
A653: q2`2<=pj`2 by A629,A642,A646;
A654: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A641,A642,
EUCLID:53,TOPREAL1:def 3;
A655: ppi`2<= q2`2 by A629,A642,A646;
now
per cases by XXREAL_0:1;
suppose
q1`2>q2`2;
then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2<=
q1`2} by A652,A654,TOPREAL3:9;
then consider p2 such that
A656: p2 =x & p2`1=q1`1 and
A657: q2`2<=p2`2 & p2`2<=q1`2 by A638,A640;
ppi`2<=p2`2 & p2`2<=pj`2 by A650,A655,A657,XXREAL_0:2;
then
A658: x in LSeg(f,k) by A478,A649,A656;
LSeg(f,k) in lf by A3,A24;
hence thesis by A658,TARSKI:def 4;
end;
suppose
q1`2=q2`2;
then LSeg(g,i)={q1} by A652,A654,RLTOPSP1:70;
then x=q1 by A638,A640,TARSKI:def 1;
then
A659: x in LSeg(f,k) by A478,A649,A651,A650;
LSeg(f,k) in lf by A3,A24;
hence thesis by A659,TARSKI:def 4;
end;
suppose
q1`2<q2`2;
then LSeg(g,i)= {p1: p1`1=q1`1 & q1`2<=p1`2 & p1`2<=
q2`2} by A652,A654,TOPREAL3:9;
then consider p2 such that
A660: p2 =x & p2`1=q1`1 and
A661: q1`2<=p2`2 & p2`2<=q2`2 by A638,A640;
ppi`2<=p2`2 & p2`2<=pj`2 by A651,A653,A661,XXREAL_0:2;
then
A662: x in LSeg(f,k) by A478,A649,A660;
LSeg(f,k) in lf by A3,A24;
hence thesis by A662,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
let x be object;
assume x in L~f;
then
A663: x in L~f1 \/ LSeg(f,k) by A3,A13,GOBOARD2:3;
now
per cases by A663,XBOOLE_0:def 3;
suppose
A664: x in L~f1;
L~g1 c= L~g by GOBOARD2:6;
hence thesis by A44,A664;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A665: p1=x and
A666: p1`1=ppi`1 and
A667: ppi`2<=p1`2 and
A668: p1`2<=pj`2 by A478;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=
g/.$1 holds q`2<=p1`2;
A669: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A628,XREAL_1:31;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A670: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A46,A670,FINSEQ_4:68
.=G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence thesis by A667;
end;
end;
A671: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A672: P2[ma] & for n be Nat st P2[n] holds n<=ma from
NAT_1:sch 6 (A671,A669);
reconsider ma as Nat;
now
per cases;
suppose
A673: ma=len g;
i2+1<=j2 by A390,NAT_1:13;
then
A674: 1<=l by XREAL_1:19;
then len g1+1<=ma by A396,A628,A673,XREAL_1:7;
then
A675: len g1<=ma-1 by XREAL_1:19;
then 0+1<=ma by XREAL_1:19;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
reconsider q=g/.m1 as Point of TOP-REAL 2;
A676: ma-1<=len g by A673,XREAL_1:43;
then
A677: q`1=ppi`1 by A629,A675;
A678: q`2<=pj`2 by A629,A676,A675;
set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1 &
q`2<=e`2 & e`2<=pj`2};
A679: i2+l=j2;
A680: l in dom g2 by A396,A674,FINSEQ_3:25;
then
A681: g/.ma=g2/.l by A396,A628,A673,FINSEQ_4:69
.= pj by A396,A680,A679;
then pj`2<=p1`2 by A672;
then
A682: p1`2=pj`2 by A668,XXREAL_0:1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A683: 1<=m1 by A675,XXREAL_0:2;
A684: m1+1=ma;
then q=|[q`1,q`2]| & LSeg(g,m1)=LSeg(q,pj) by A673,A681
,A683,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A462,A477,A677,A678,TOPREAL3:9;
then
A685: p1 in LSeg(g,m1) by A666,A682,A678;
LSeg(g,m1) in lg by A673,A683,A684;
hence thesis by A665,A685,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A672,XXREAL_0:1;
then
A686: ma+1<=len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of
TOP-REAL 2;
set lma = {p2: p2`1=ppi`1 & qa`2<=p2`2 & p2`2<=qa1`2};
A687: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A688: qa`2<=p1`2 by A672;
A689: len g1<=ma+1 by A672,NAT_1:13;
then
A690: qa1 `1 = ppi`1 by A629,A686;
A691: now
assume qa1`2<=p1`2;
then for q holds q=g/.(ma+1) implies q`2<=p1`2;
then ma+1<=ma by A672,A686,A689;
hence contradiction by XREAL_1:29;
end;
A692: qa`1=ppi`1 & qa=|[qa`1,qa`2]| by A629,A672,EUCLID:53;
A693: 1<=ma by A24,A14,A47,A672,NAT_1:13;
then LSeg(g,ma)=LSeg(qa,qa1) by A686,TOPREAL1:def 3
.= lma by A688,A691,A690,A692,A687,TOPREAL3:9
,XXREAL_0:2;
then
A694: x in LSeg(g,ma) by A665,A666,A688,A691;
LSeg(g,ma) in lg by A686,A693;
hence thesis by A694,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A45,FINSEQ_4:68
.=f/.1 by A27,A25,FINSEQ_4:71;
A695: len g=len g1 + l by A396,FINSEQ_1:22;
i2+1<=j2 by A390,NAT_1:13;
then
A696: 1<=l by XREAL_1:19;
then
A697: l in dom g2 by A396,FINSEQ_3:25;
hence g/.len g=g2/.l by A695,FINSEQ_4:69
.=G*(i1,i2+l) by A396,A697
.=f/.len f by A3,A21,A76;
thus len f<=len g by A3,A14,A47,A696,A695,XREAL_1:7;
end;
end;
hence thesis;
end;
suppose
A698: i2=j2;
set ppi = G*(i1,i2), pj = G*(j1,i2);
now
per cases by XXREAL_0:1;
case
A699: i1>j1;
c1/.i1=c1.i1 by A66,A60,PARTFUN1:def 6;
then
A700: c1/.i1=ppi by A66,MATRIX_0:def 8;
then
A701: x2.i1=ppi`1 by A66,A18,A63,A64,A59,GOBOARD1:def 1;
c1/.j1=c1.j1 by A23,A60,PARTFUN1:def 6;
then
A702: c1/.j1=pj by A23,MATRIX_0:def 8;
then
A703: x2.j1 =pj`1 by A23,A18,A63,A64,A59,GOBOARD1:def 1;
then
A704: pj`1<ppi`1 by A66,A23,A18,A69,A63,A64,A59,A699,A701,SEQM_3:def 1;
reconsider l=i1-j1 as Element of NAT by A699,INT_1:5;
defpred P1[Nat,set] means for m st m=i1-$1 holds $2=G*(m,i2);
set lk={w where w is Point of TOP-REAL 2: w`2=ppi`2 & pj`1<=w`1
& w`1<= ppi`1};
A705: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
A706: now
let n;
assume n in Seg l;
then
A707: n<=l by FINSEQ_1:1;
l<=i1 by XREAL_1:43;
then reconsider w=i1-n as Element of NAT by A707,INT_1:5
,XXREAL_0:2;
i1-n<=i1 & i1<=len G by A66,FINSEQ_3:25,XREAL_1:43;
then
A708: w<=len G by XXREAL_0:2;
A709: 1<=j1 by A23,FINSEQ_3:25;
i1-l<=i1-n by A707,XREAL_1:13;
then 1<=w by A709,XXREAL_0:2;
then w in dom G by A708,FINSEQ_3:25;
hence
i1-n is Nat & [i1-n,i2] in Indices G & i1-n in
dom G by A22,A68,ZFMISC_1:87;
end;
A710: now
let n be Nat;
assume n in Seg l;
then reconsider m=i1-n as Nat by A706;
take p=G*(m,i2);
thus P1[n,p];
end;
consider g2 such that
A711: len g2 = l & for n being Nat st n in Seg l holds P1[n
,g2/.n] from FINSEQ_4:sch 1(A710);
take g=g1^g2;
A712: dom g2=Seg l by A711,FINSEQ_1:def 3;
now
let n;
assume
A713: n in dom g2;
then reconsider m=i1-n as Nat by A706,A712;
take m,k=i2;
thus [m,k] in Indices G & g2/.n=G*(m,k) by A706,A711,A712,A713;
end;
then
A714: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G
*(i,j) by A75,GOBOARD1:23;
A715: Seg len g2=dom g2 by FINSEQ_1:def 3;
A716: y2.i1=ppi`2 by A66,A18,A61,A59,A700,GOBOARD1:def 2;
A717: now
let n,p;
assume that
A718: n in dom g2 and
A719: g2/.n=p;
reconsider n1=i1-n as Nat by A706,A712,A718;
n<=len g2 by A715,A718,FINSEQ_1:1;
then
A720: i1-len g2<= n1 by XREAL_1:13;
set pn = G*(n1,i2);
A721: g2/.n=pn by A711,A715,A718;
A722: i1-n in dom G by A706,A711,A715,A718;
then
A723: y2.n1=y2.i1 by A66,A18,A70,A61,A59,SEQM_3:def 10;
c1/.n1=c1.n1 by A60,A722,PARTFUN1:def 6;
then
A724: c1/.n1=pn by A722,MATRIX_0:def 8;
then
A725: x2.n1=pn`1 by A18,A63,A64,A59,A722,GOBOARD1:def 1;
y2.n1=pn`2 by A18,A61,A59,A722,A724,GOBOARD1:def 2;
hence
p`2=ppi`2 & pj`1<=p`1 & p`1<=ppi`1 by A66,A23,A18,A69,A63,A64
,A59,A711,A716,A701,A703,A719,A722,A721,A720,A723,A725,SEQ_4:137,XREAL_1:43;
thus p in rng c1 by A60,A719,A722,A721,A724,PARTFUN2:2;
1<=n by A715,A718,FINSEQ_1:1;
then n1<i1 by XREAL_1:44;
hence p`1<ppi`1 by A66,A18,A69,A63,A64,A59,A701,A719,A722,A721
,A725,SEQM_3:def 1;
end;
A726: g2 is special
proof
let n be Nat;
set p = g2/.n;
assume
A727: 1<=n & n+1 <= len g2;
then n in dom g2 by SEQ_4:134;
then
A728: p`2=ppi`2 by A717;
n+1 in dom g2 by A727,SEQ_4:134;
hence thesis by A717,A728;
end;
A729: now
let n,m,p,q;
assume that
A730: n in dom g2 and
A731: m in dom g2 and
A732: n<m and
A733: g2/.n=p & g2/.m=q;
A734: i1-n in dom G by A706,A712,A730;
reconsider n1=i1-n, m1=i1-m as Nat by A706,A712,A730
,A731;
set pn = G*(n1,i2), pm = G*(m1,i2);
A735: m1<n1 by A732,XREAL_1:15;
c1/.n1=c1.n1 by A60,A706,A712,A730,PARTFUN1:def 6;
then c1/.n1=pn by A734,MATRIX_0:def 8;
then
A736: x2.n1=pn`1 by A65,A60,A734,GOBOARD1:def 1;
A737: i1-m in dom G by A706,A712,A731;
c1/.m1 = c1.m1 by A60,A706,A712,A731,PARTFUN1:def 6;
then c1/.m1= pm by A737,MATRIX_0:def 8;
then
A738: x2.m1=pm`1 by A65,A60,A737,GOBOARD1:def 1;
g2/.n=pn & g2/.m=pm by A711,A712,A730,A731;
hence q`1<p`1 by A69,A65,A60,A733,A734,A737,A735,A736,A738,
SEQM_3:def 1;
end;
for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom
g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m)
proof
let n,m;
assume that
A739: m>n+1 and
A740: n in dom g2 and
A741: n+1 in dom g2 and
A742: m in dom g2 and
A743: m+1 in dom g2 and
A744: LSeg(g2,n) /\ LSeg(g2,m) <> {};
reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as
Point of TOP-REAL 2;
A745: p1`2=ppi`2 & p2`2= ppi`2 by A717,A740,A741;
n<n+1 by NAT_1:13;
then
A746: p2`1<p1`1 by A729,A740,A741;
set lp = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & p2`1<=
w`1 & w`1<=p1`1}, lq = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & q2`1<=w`1
& w`1<=q1`1};
A747: p1=|[p1`1,p1`2]| & p2=|[p2`1,p2`2]| by EUCLID:53;
m<m+1 by NAT_1:13;
then
A748: q2`1<q1`1 by A729,A742,A743;
A749: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
set x = the Element of LSeg(g2,n) /\ LSeg(g2,m);
A750: x in LSeg(g2,n) by A744,XBOOLE_0:def 4;
A751: q1`2= ppi`2 & q2`2=ppi`2 by A717,A742,A743;
A752: x in LSeg(g2,m) by A744,XBOOLE_0:def 4;
1 <= m & m+1<= len g2 by A742,A743,FINSEQ_3:25;
then LSeg(g2,m) = LSeg(q2,q1) by TOPREAL1:def 3
.=lq by A748,A751,A749,TOPREAL3:10;
then
A753: ex tm be Point of TOP-REAL 2 st tm=x & tm`2=ppi`2 & q2
`1<=tm`1 & tm`1<=q1`1 by A752;
1 <= n & n+1 <= len g2 by A740,A741,FINSEQ_3:25;
then LSeg(g2,n) = LSeg(p2,p1) by TOPREAL1:def 3
.=lp by A746,A745,A747,TOPREAL3:10;
then
A754: ex tn be Point of TOP-REAL 2 st tn=x & tn`2=ppi`2 & p2
`1<=tn`1 & tn`1<=p1`1 by A750;
q1`1<p2`1 by A729,A739,A741,A742;
hence contradiction by A754,A753,XXREAL_0:2;
end;
then
A755: g2 is s.n.c. by GOBOARD2:1;
A756: not f/.k in L~g2
proof
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume f/.k in L~g2;
then consider X be set such that
A757: f/.k in X and
A758: X in ls by TARSKI:def 4;
consider m such that
A759: X=LSeg(g2,m) and
A760: 1<=m & m+1 <= len g2 by A758;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A761: m in dom g2 by A760,SEQ_4:134;
then
A762: q1`2=ppi`2 by A717;
set lq={w where w is Point of TOP-REAL 2: w`2=ppi`2 & q2`1<=w
`1 & w`1<=q1`1};
A763: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
A764: m+1 in dom g2 by A760,SEQ_4:134;
then
A765: q2`2=ppi`2 by A717;
m<m+1 by NAT_1:13;
then
A766: q2`1<q1`1 by A729,A761,A764;
LSeg(g2,m)=LSeg(q2,q1) by A760,TOPREAL1:def 3
.=lq by A762,A765,A766,A763,TOPREAL3:10;
then ex p st p=f/.k & p`2=ppi`2 & q2`1<=p`1 & p`1<=q1`1 by A757
,A759;
hence contradiction by A29,A717,A761;
end;
y2.j1=pj`2 by A23,A18,A61,A59,A702,GOBOARD1:def 2;
then
A767: ppi`2=pj`2 by A66,A23,A18,A70,A61,A59,A716,SEQM_3:def 10;
now
let n,m be Element of NAT;
assume that
A768: n in dom g2 & m in dom g2 and
A769: n<>m;
reconsider n1=i1-n, m1=i1-m as Nat by A706,A712,A768;
A770: g2/.n=G*(n1,i2) & g2/.m=G*(m1,i2) by A711,A712,A768;
assume
A771: g2/.n=g2/.m;
[i1-n,i2] in Indices G & [i1-m,i2] in Indices G by A706,A712
,A768;
then n1=m1 by A770,A771,GOBOARD1:5;
hence contradiction by A769;
end;
then for n,m being Element of NAT
st n in dom g2 & m in dom g2 & g2/.n = g2/.m
holds n = m;
then
A772: g2 is one-to-one by PARTFUN2:9;
reconsider m1=i1-l as Nat;
A773: pj=|[pj`1,pj `2]| by EUCLID:53;
A774: LSeg(f,k)=LSeg(pj,ppi) by A3,A24,A29,A21,A698,TOPREAL1:def 3
.= lk by A704,A767,A705,A773,TOPREAL3:10;
A775: rng g2 c= LSeg(f,k)
proof
let x be object;
assume x in rng g2;
then consider n being Element of NAT such that
A776: n in dom g2 and
A777: g2/.n=x by PARTFUN2:2;
reconsider n1=i1-n as Nat by A706,A711,A715,A776;
set pn = G*(n1,i2);
A778: g2/.n=pn by A711,A715,A776;
then
A779: pn`1<=ppi`1 by A717,A776;
pn`2=ppi`2 & pj`1<=pn`1 by A717,A776,A778;
hence thesis by A774,A777,A778,A779;
end;
A780: now
let n;
assume that
A781: n in dom g2 and
A782: n+1 in dom g2;
reconsider m1=i1-n,m2=i1-(n+1) as Nat by A706,A712
,A781,A782;
let l1,l2,l3,l4 be Nat;
assume that
A783: [l1,l2] in Indices G and
A784: [l3,l4] in Indices G and
A785: g2/.n=G*(l1,l2) and
A786: g2/.(n+1)=G*(l3,l4);
[i1-(n+1),i2] in Indices G & g2/.(n+1)=G*(m2,i2) by A706,A711
,A712,A782;
then
A787: l3=m2 & l4=i2 by A784,A786,GOBOARD1:5;
[i1-n,i2] in Indices G & g2/.n=G*(m1,i2) by A706,A711,A712,A781
;
then l1=m1 & l2=i2 by A783,A785,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= |.i1-n-(i1-(n+1)).|+0 by A787,
ABSVALUE:2
.= 1 by ABSVALUE:def 1;
end;
now
let l1,l2,l3,l4 be Nat;
assume that
A788: [ l1,l2] in Indices G and
A789: [l3,l4] in Indices G and
A790: g1/.len g1=G*(l1,l2) and
A791: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A792: 1 in dom g2;
reconsider m1=i1-1 as Nat by A706,A712,A792;
[i1-1,i2] in Indices G & g2/.1=G*(m1,i2) by A706,A711,A712,A792
;
then
A793: l3=m1 & l4=i2 by A789,A791,GOBOARD1:5;
f1/.len f1=f/.k by A27,A14,A51,FINSEQ_4:71;
then l1=i1 & l2=i2 by A46,A28,A29,A788,A790,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=|.i1-(i1-1).|+0 by A793,ABSVALUE:2
.=1 by ABSVALUE:def 1;
end;
then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [
m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A48,A780,GOBOARD1:24;
hence g is_sequence_on G by A714,GOBOARD1:def 9;
A794: LSeg(f,k)=LSeg(ppi,pj) by A3,A24,A29,A21,A698,TOPREAL1:def 3;
A795: not f/.k in rng g2
proof
assume f/.k in rng g2;
then consider n being Element of NAT such that
A796: n in dom g2 and
A797: g2/.n=f/.k by PARTFUN2:2;
reconsider n1=i1-n as Nat by A706,A711,A715,A796;
[i1-n,i2] in Indices G & g2/.n=G*(n1,i2) by A706,A711,A715,A796
;
then
A798: n1=i1 by A28,A29,A797,GOBOARD1:5;
0<n by A715,A796,FINSEQ_1:1;
hence contradiction by A798;
end;
rng g1 /\ rng g2 = {}
proof
set x = the Element of rng g1 /\ rng g2;
assume
A799: not thesis;
then
A800: x in rng g2 by XBOOLE_0:def 4;
A801: x in rng g1 by A799,XBOOLE_0:def 4;
now
per cases by A24,XXREAL_0:1;
suppose
k=1;
hence contradiction by A52,A795,A801,A800,TARSKI:def 1;
end;
suppose
1<k;
then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k}
by A3,A6,A7,A49,A775,A801,A800,GOBOARD2:4,XBOOLE_0:def 4;
hence contradiction by A795,A800,TARSKI:def 1;
end;
end;
hence contradiction;
end;
then rng g1 misses rng g2;
hence g is one-to-one by A40,A772,FINSEQ_3:91;
A802: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2
,n+1) = {g2/.(n+1)}
proof
let n;
assume that
A803: 1<=n and
A804: n+2 <= len g2;
A805: n+1 in dom g2 by A803,A804,SEQ_4:135;
then g2/.(n+1) in rng g2 by PARTFUN2:2;
then g2/.(n+1) in lk by A774,A775;
then consider u1 be Point of TOP-REAL 2 such that
A806: g2/.(n+1)=u1 and
A807: u1`2=ppi`2 and
pj`1<=u1`1 and
u1`1<=ppi`1;
A808: n+2 in dom g2 by A803,A804,SEQ_4:135;
then g2/.(n+2) in rng g2 by PARTFUN2:2;
then g2/.(n+2) in lk by A774,A775;
then consider u2 be Point of TOP-REAL 2 such that
A809: g2/.(n+2)=u2 and
A810: u2`2=ppi`2 and
pj`1<=u2`1 and
u2`1<=ppi`1;
1<= n+1 & n+1+1 = n+(1+1) by NAT_1:11;
then
A811: LSeg(g2,n+1)=LSeg( u1,u2) by A804,A806,A809,TOPREAL1:def 3;
n+1<n+1+1 by NAT_1:13;
then
A812: u2`1<u1`1 by A729,A805,A808,A806,A809;
A813: n in dom g2 by A803,A804,SEQ_4:135;
then g2/.n in rng g2 by PARTFUN2:2;
then g2/.n in lk by A774,A775;
then consider u be Point of TOP-REAL 2 such that
A814: g2/.n=u and
A815: u`2=ppi`2 and
pj`1<=u`1 and
u`1<=ppi`1;
n+1 <= n+2 by XREAL_1:6;
then n+1 <= len g2 by A804,XXREAL_0:2;
then
A816: LSeg(g2,n)=LSeg(u,u1) by A803,A814,A806,TOPREAL1:def 3;
set lg = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & u2`1<=
w`1 & w`1<=u`1};
n<n+1 by NAT_1:13;
then
A817: u1`1<u`1 by A729,A813,A805,A814,A806;
then
A818: u1 in lg by A807,A812;
u=|[u`1,u`2]| & u2=|[u2`1,u2`2 ]| by EUCLID:53;
then LSeg(g2/.n,g2/.(n+2))=lg by A814,A815,A809,A810,A812,A817,
TOPREAL3:10,XXREAL_0:2;
hence thesis by A814,A806,A809,A816,A811,A818,TOPREAL1:8;
end;
thus g is unfolded
proof
let n be Nat;
assume that
A819: 1<=n and
A820: n+2 <= len g;
A821: n+1+1<=len g by A820;
n+1<=n+1+1 by NAT_1:11;
then
A822: n+1 <= len g by A820,XXREAL_0:2;
A823: len g=len g1+len g2 by FINSEQ_1:22;
n+2-len g1 = n-len g1 +2;
then
A824: n-len g1 + 2 <= len g2 by A820,A823,XREAL_1:20;
A825: 1 <= n+1 by NAT_1:11;
A826: n<=n+1 by NAT_1:11;
A827: n+(1+1)=n+1+1;
per cases;
suppose
A828: n+2 <= len g1;
A829: n+(1+1)=n+1+1;
A830: n+1 in dom g1 by A819,A828,SEQ_4:135;
then
A831: g/.(n+1)=g1/.(n+1) by FINSEQ_4:68;
n in dom g1 by A819,A828,SEQ_4:135;
then
A832: LSeg(g1,n)=LSeg(g,n) by A830,TOPREAL3:18;
n+2 in dom g1 by A819,A828,SEQ_4:135;
then LSeg(g1,n+1)=LSeg(g,n+1) by A830,A829,TOPREAL3:18;
hence thesis by A41,A819,A828,A832,A831;
end;
suppose
len g1 < n+2;
then len g1+1<=n+2 by NAT_1:13;
then
A833: len g1<=n+2-1 by XREAL_1:19;
thus thesis
proof
per cases;
suppose
A834: len g1=n+1;
then 1<=len g-len g1 by A821,XREAL_1:19;
then 1 in dom g2 by A823,FINSEQ_3:25;
then
A835: g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A774,A775;
then consider u1 be Point of TOP-REAL 2 such that
A836: g2/.1=u1 and
u1`2=ppi`2 and
pj`1<=u1`1 and
u1`1<=ppi`1;
ppi in LSeg(ppi,pj) by RLTOPSP1:68;
then
A837: LSeg(ppi,u1) c= LSeg(f,k) by A794,A775,A835,A836,
TOPREAL1:6;
1<=n+1 by NAT_1:11;
then
A838: n+1 in dom g1 by A834,FINSEQ_3:25;
then
A839: g/.(n+1)=f1/.len f1 by A46,A834,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
now
1<len g1 by A819,A834,NAT_1:13;
then
A840: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A840,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A841: L~f1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,GOBOARD2:4;
A842: LSeg(g1,n) c= L~f1 by A44,TOPREAL3:19;
n in dom g1 by A819,A826,A834,FINSEQ_3:25;
then
A843: LSeg(g,n)=LSeg(g1,n) by A838,TOPREAL3:18;
g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1)
by A819,A820,A825,A822,A827,TOPREAL1:21;
then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by
XBOOLE_0:def 4;
then
A844: {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:31;
1 <= len g2 by A820,A827,A823,A834,XREAL_1:6;
then g/.(n+2)=g2/.1 by A827,A834,SEQ_4:136;
then LSeg(g,n+1)=LSeg(ppi,u1 ) by A820,A825,A827,A839
,A836,TOPREAL1:def 3;
then LSeg(g,n) /\ LSeg(g,n+1) c= {g /.(n+1)} by A29,A842
,A841,A843,A839,A837,XBOOLE_1:27;
hence thesis by A844;
end;
suppose
len g1<>n+1;
then len g1<n+1 by A833,XXREAL_0:1;
then
A845: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by INT_1:5;
thus thesis
proof
per cases;
suppose
A846: len g1=n;
then
A847: 2 <= len g2 by A820,A823,XREAL_1:6;
then 1<= len g2 by XXREAL_0:2;
then
A848: g/.(n+1)=g2/.1 by A846,SEQ_4:136;
1<=len g2 by A847,XXREAL_0:2;
then
A849: 1 in dom g2 by FINSEQ_3:25;
then g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A774,A775;
then consider u1 be Point of TOP-REAL 2 such that
A850: g2/.1=u1 and
A851: u1`2=ppi`2 and
pj`1<=u1`1 and
A852: u1`1<=ppi`1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then g/.n=f1/.len f1 by A46,A846,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
then
A853: LSeg(g,n)=LSeg(ppi,u1) by A819,A822,A848,A850,
TOPREAL1:def 3;
A854: 2 in dom g2 by A847,FINSEQ_3:25;
then g2/.2 in rng g2 by PARTFUN2:2;
then g2/.2 in lk by A774,A775;
then consider u2 be Point of TOP-REAL 2 such that
A855: g2 /.2=u2 and
A856: u2`2=ppi`2 and
pj`1<=u2`1 and
A857: u2`1<=ppi`1;
set lg = {w where w is Point of TOP-REAL 2 : w`2=ppi
`2 & u2`1<=w`1 & w`1<=ppi`1};
u2=|[u2`1,u2`2]| by EUCLID:53;
then
A858: LSeg(ppi,g2/.2)=lg by A705,A855,A856,A857,TOPREAL3:10
;
u2`1<u1`1 by A729,A849,A854,A850,A855;
then
A859: u1 in lg by A851,A852;
g/.(n+2)=g2/.2 by A846,A847,SEQ_4:136;
then LSeg(g,n+1)=LSeg(u1,u2) by A820,A825,A827,A848
,A850,A855,TOPREAL1:def 3;
hence thesis by A848,A850,A855,A859,A853,A858,
TOPREAL1:8;
end;
suppose
len g1<>n;
then
A860: len g1<n by A845,XXREAL_0:1;
then len g1+1<=n by NAT_1:13;
then
A861: 1<=n1 by XREAL_1:19;
n1 + len g1 = n;
then
A862: LSeg(g,n)=LSeg(g2,n1) by A822,A860,GOBOARD2:5;
A863: n+1 = n1+1+len g1;
n1 + 1 + len g1 = n + 1;
then n1+1 <= len g2 by A822,A823,XREAL_1:6;
then
A864: g/.(n+1)=g2/.(n1+1) by A863,NAT_1:11,SEQ_4:136;
len g1<n+1 by A826,A860,XXREAL_0:2;
then LSeg(g,n+1)=LSeg(g2,n1+1) by A821,A863,
GOBOARD2:5;
hence thesis by A802,A824,A862,A864,A861;
end;
end;
end;
end;
end;
end;
A865: L~g2 c= LSeg(f,k)
proof
let x be object;
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume x in L~g2;
then consider X be set such that
A866: x in X and
A867: X in ls by TARSKI:def 4;
consider m such that
A868: X=LSeg(g2,m) and
A869: 1<=m & m+1 <= len g2 by A867;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A870: LSeg(g2,m)=LSeg(q1,q2) by A869,TOPREAL1:def 3;
m+1 in dom g2 by A869,SEQ_4:134;
then
A871: g2/.(m+1) in rng g2 by PARTFUN2:2;
m in dom g2 by A869,SEQ_4:134;
then g2/.m in rng g2 by PARTFUN2:2;
then LSeg(q1,q2) c= LSeg(ppi,pj) by A794,A775,A871,TOPREAL1:6;
hence thesis by A794,A866,A868,A870;
end;
A872: L~g1 /\ L~g2 = {}
proof
per cases;
suppose
k=1;
hence thesis by A52;
end;
suppose
k<>1;
then 1<k by A24,XXREAL_0:1;
then L~g1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,A44,GOBOARD2:4;
then
A873: L~g1 /\ L~g2 c= {f/.k} by A865,XBOOLE_1:26;
now
set x = the Element of L~g1 /\ L~g2;
assume L~g1 /\ L~g2 <> {};
then x in {f/.k} & x in L~g2 by A873,XBOOLE_0:def 4;
hence contradiction by A756,TARSKI:def 1;
end;
hence thesis;
end;
end;
for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g
& m+1 in dom g holds LSeg(g,n) misses LSeg(g,m)
proof
A874: 1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A875: g/.len g1=g1/.len g1 by FINSEQ_4:68
.= ppi by A27,A14,A51,A46,A29,FINSEQ_4:71;
reconsider qq=g2/.1 as Point of TOP-REAL 2;
set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j):
1<=j & j+1 <= len g2};
let n,m;
assume that
A876: m>n+1 and
A877: n in dom g and
A878: n+1 in dom g and
A879: m in dom g and
A880: m+1 in dom g;
A881: 1<=n by A877,FINSEQ_3:25;
j1+1<=i1 by A699,NAT_1:13;
then
A882: 1<=l by XREAL_1:19;
then
A883: 1 in dom g2 by A711,FINSEQ_3:25;
then
A884: qq`2=ppi`2 & qq`1<ppi`1 by A717;
A885: g/.(len g1+1)=qq by A711,A882,SEQ_4:136;
A886: pj`1<=qq`1 by A717,A883;
A887: m+1<=len g by A880,FINSEQ_3:25;
A888: 1<=m+1 by A880,FINSEQ_3:25;
A889: 1<=n+1 by A878,FINSEQ_3:25;
A890: n+1<=len g by A878,FINSEQ_3:25;
A891: qq=|[qq`1,qq`2]| by EUCLID:53;
A892: 1<=m by A879,FINSEQ_3:25;
set ql={z where z is Point of TOP-REAL 2: z`2=ppi`2 & qq`1<=z
`1 & z`1<=ppi`1};
A893: n<=n+1 by NAT_1:11;
A894: len g=len g1+len g2 by FINSEQ_1:22;
then len g1+1<=len g by A711,A882,XREAL_1:7;
then
A895: LSeg (g,len g1)=LSeg(qq,ppi) by A874,A875,A885,TOPREAL1:def 3
.= ql by A705,A884,A891,TOPREAL3:10;
A896: m<=m+1 by NAT_1:11;
then
A897: n+1<=m+1 by A876,XXREAL_0:2;
now
per cases;
suppose
A898: m+1<=len g1;
then m<=len g1 by A896,XXREAL_0:2;
then
A899: m in dom g1 by A892,FINSEQ_3:25;
m+1 in dom g1 by A888,A898,FINSEQ_3:25;
then
A900: LSeg(g,m)=LSeg(g1,m) by A899,TOPREAL3:18;
A901: n+1<=len g1 by A897,A898,XXREAL_0:2;
then n<=len g1 by A893,XXREAL_0:2;
then
A902: n in dom g1 by A881,FINSEQ_3:25;
n+1 in dom g1 by A889,A901,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A902,TOPREAL3:18;
hence thesis by A42,A876,A900;
end;
suppose
len g1<m+1;
then
A903: len g1<=m by NAT_1:13;
then reconsider m1=m-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A904: m=len g1;
A905: LSeg(g,m) c= LSeg(f,k)
proof
let x be object;
assume x in LSeg(g,m);
then consider px be Point of TOP-REAL 2 such that
A906: px=x & px`2=ppi`2 and
A907: qq`1<=px`1 and
A908: px`1<= ppi`1 by A895,A904;
pj`1<=px`1 by A886,A907,XXREAL_0:2;
hence thesis by A774,A906,A908;
end;
n<=len g1 by A876,A893,A904,XXREAL_0:2;
then
A909: n in dom g1 by A881,FINSEQ_3:25;
now
1<len g1 by A876,A889,A904,XXREAL_0:2;
then
A910: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A910,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A911: L~f1 /\ LSeg(f,k) ={f/.k} by A3,A6,A7,GOBOARD2:4;
A912: n+1 in dom g1 by A876,A889,A904,FINSEQ_3:25;
then
A913: LSeg(g,n)=LSeg(g1,n) by A909,TOPREAL3:18;
then LSeg(g,n) in l1 by A876,A881,A904;
then LSeg(g,n) c= L~f1 by A44,ZFMISC_1:74;
then
A914: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A911,A905,
XBOOLE_1:27;
now
set x = the Element of LSeg(g,n)/\ LSeg(g,m);
assume
A915: LSeg(g,n)/\ LSeg(g,m)<>{};
then
A916: x in LSeg(g,n) by XBOOLE_0:def 4;
x in {f/.k} by A914,A915;
then
A917: x=f/.k by TARSKI:def 1;
f/.k=g1/.len g1 by A27,A14,A51,A46,FINSEQ_4:71;
hence
contradiction by A40,A41,A42,A876,A904,A909,A912,A913
,A916,A917,GOBOARD2:2;
end;
hence thesis;
end;
suppose
m<>len g1;
then
A918: len g1<m by A903,XXREAL_0:1;
then len g1+1<= m by NAT_1:13;
then
A919: 1<=m1 by XREAL_1:19;
m+1=m1+1+len g1;
then
A920: m1+1 <= len g2 by A887,A894,XREAL_1:6;
m = m1+len g1;
then
A921: LSeg(g,m)=LSeg(g2,m1) by A887,A918,GOBOARD2:5;
then LSeg(g,m) in l2 by A919,A920;
then
A922: LSeg(g,m) c= L~g2 by ZFMISC_1:74;
now
per cases;
suppose
A923: n+1<=len g1;
then n<=len g1 by A893,XXREAL_0:2;
then
A924: n in dom g1 by A881,FINSEQ_3:25;
n+1 in dom g1 by A889,A923,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A924,TOPREAL3:18;
then LSeg(g,n) in l1 by A881,A923;
then LSeg(g,n) c= L~g1 by ZFMISC_1:74;
then LSeg(g,n) /\ LSeg(g,m) = {} by A872,A922,
XBOOLE_1:3,27;
hence thesis;
end;
suppose
len g1<n+1;
then
A925: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by
INT_1:5;
A926: n - len g1 + 1 = n + 1 - len g1;
A927: n = n1 + len g1;
now
per cases;
suppose
A928: len g1=n;
now
reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point
of TOP-REAL 2;
set x = the Element of LSeg(g,n) /\ LSeg(g,m);
set q1l={v where v is Point of TOP-REAL 2: v
`2=ppi`2 & q2`1<=v`1 & v`1<=q1`1};
A929: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]|
by EUCLID:53;
assume
A930: LSeg(g,n) /\ LSeg(g,m)<>{};
then
A931: x in LSeg(g,m) by XBOOLE_0:def 4;
x in LSeg(g,n) by A930,XBOOLE_0:def 4;
then
A932: ex qx be Point of TOP-REAL 2 st qx=x
& qx`2=ppi`2 & qq`1<=qx`1 & qx`1<= ppi`1 by A895,A928;
A933: m1 in dom g2 by A919,A920,SEQ_4:134;
then
A934: q1 `2=ppi`2 by A717;
A935: m1+1 in dom g2 by A919,A920,SEQ_4:134;
then
A936: q2`2=ppi`2 by A717;
m1<m1+1 by NAT_1:13;
then
A937: q2`1<q1`1 by A729,A933,A935;
LSeg(g2,m1)=LSeg(q2,q1) by A919,A920,
TOPREAL1:def 3
.=q1l by A934,A936,A937,A929,TOPREAL3:10;
then
A938: ex qy be Point of TOP-REAL 2 st qy=x
& qy`2=ppi`2 & q2`1<=qy`1 & qy`1<= q1`1 by A921,A931;
m1 > n1 + 1 & n1 + 1 >= 1 by A876,A926,
NAT_1:11,XREAL_1:9;
then m1 > 1 by XXREAL_0:2;
then q1`1 < qq`1 by A729,A883,A933;
hence contradiction by A932,A938,XXREAL_0:2;
end;
hence thesis;
end;
suppose
n<>len g1;
then len g1<n by A925,XXREAL_0:1;
then
A939: LSeg(g,n)=LSeg(g2,n1) by A890,A927,GOBOARD2:5;
m1>n1+1 by A876,A926,XREAL_1:9;
hence thesis by A755,A921,A939;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence g is s.n.c. by GOBOARD2:1;
now
set p=g1/.len g1, q=g2/.1;
j1+1<=i1 by A699,NAT_1:13;
then 1<=l by XREAL_1:19;
then 1 in dom g2 by A712,FINSEQ_1:1;
then q`2=ppi`2 by A717;
hence p`1=q`1 or p`2=q`2 by A27,A14,A51,A46,A29,FINSEQ_4:71;
end;
hence g is special by A43,A726,GOBOARD2:8;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1 <= len g}, lf = {LSeg(f,j): 1
<=j & j+1 <= len f};
A940: len g = len g1 + len g2 by FINSEQ_1:22;
A941: now
let j;
assume that
A942: len g1<=j and
A943: j<=len g;
reconsider w = j-len g1 as Element of NAT by A942,INT_1:5;
let p such that
A944: p=g/.j;
per cases;
suppose
A945: j=len g1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A946: g/.len g1 = f1/.len f1 by A46,FINSEQ_4:68
.= G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence p`2=G*(i1,i2)`2 by A944,A945;
thus G*(j1,i2)`1<=p`1 & p`1<=G* (i1,i2)`1 by A66,A23,A18
,A69,A63,A64,A59,A699,A701,A703,A944,A945,A946,SEQM_3:def 1;
Seg len c1 = dom c1 by FINSEQ_1:def 3;
hence p in rng c1 by A66,A18,A59,A700,A944,A945,A946,
PARTFUN2:2;
end;
suppose
j<>len g1;
then len g1 < j by A942,XXREAL_0:1;
then len g1 + 1<=j by NAT_1:13;
then
A947: 1<=w by XREAL_1:19;
A948: w<=len g2 by A940,A943,XREAL_1:20;
then
A949: w in dom g2 by A947,FINSEQ_3:25;
j = w + len g1;
then g/.j=g2/.w by A947,A948,SEQ_4:136;
hence p`2=ppi`2 & pj`1<=p`1 & p`1<= ppi`1 & p in rng c1 by
A717,A944,A949;
end;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A950: x in X and
A951: X in lg by TARSKI:def 4;
consider i such that
A952: X=LSeg(g,i) and
A953: 1<=i and
A954: i+1 <= len g by A951;
per cases;
suppose
A955: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A955,XXREAL_0:2;
then
A956: i in dom g1 by A953,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A955,FINSEQ_3:25;
then X=LSeg(g1,i) by A952,A956,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A953,A955;
then
A957: x in L~f1 by A44,A950,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A957;
end;
suppose
A958: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A959: i<=len g by A954,NAT_1:13;
A960: len g1<=i by A958,NAT_1:13;
then
A961: q1`2=ppi`2 by A941,A959;
A962: q1`1<=ppi`1 by A941,A960,A959;
A963: pj`1<=q1`1 by A941,A960,A959;
q2`2=ppi`2 by A941,A954,A958;
then
A964: q2=|[q2`1,q1`2 ]| by A961,EUCLID:53;
A965: q2`1<=ppi`1 by A941,A954,A958;
A966: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A953,A954,
EUCLID:53,TOPREAL1:def 3;
A967: pj`1<= q2`1 by A941,A954,A958;
now
per cases by XXREAL_0:1;
suppose
q1`1>q2`1;
then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1<=
q1`1} by A964,A966,TOPREAL3:10;
then consider p2 such that
A968: p2 =x & p2`2=q1`2 and
A969: q2`1<=p2`1 & p2`1<=q1`1 by A950,A952;
pj`1<=p2`1 & p2`1<=ppi`1 by A962,A967,A969,XXREAL_0:2;
then
A970: x in LSeg(f,k) by A774,A961,A968;
LSeg(f,k) in lf by A3,A24;
hence thesis by A970,TARSKI:def 4;
end;
suppose
q1`1=q2`1;
then LSeg(g,i)={q1} by A964,A966,RLTOPSP1:70;
then x=q1 by A950,A952,TARSKI:def 1;
then
A971: x in LSeg(f,k) by A774,A961,A963,A962;
LSeg(f,k) in lf by A3,A24;
hence thesis by A971,TARSKI:def 4;
end;
suppose
q1`1<q2`1;
then LSeg(g,i)= {p1: p1`2=q1`2 & q1`1<=p1`1 & p1`1<=
q2`1} by A964,A966,TOPREAL3:10;
then consider p2 such that
A972: p2 =x & p2`2=q1`2 and
A973: q1`1<=p2`1 & p2`1<=q2`1 by A950,A952;
pj`1<=p2`1 & p2`1<=ppi`1 by A963,A965,A973,XXREAL_0:2;
then
A974: x in LSeg(f,k) by A774,A961,A972;
LSeg(f,k) in lf by A3,A24;
hence thesis by A974,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
let x be object;
assume x in L~f;
then
A975: x in L~f1 \/ LSeg(f,k) by A3,A13,GOBOARD2:3;
per cases by A975,XBOOLE_0:def 3;
suppose
A976: x in L~f1;
L~g1 c= L~g by GOBOARD2:6;
hence thesis by A44,A976;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A977: p1=x and
A978: p1`2=ppi`2 and
A979: pj`1<=p1`1 and
A980: p1`1<=ppi`1 by A774;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g
/.$1 holds q`1>=p1`1;
A981: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A940,XREAL_1:31;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A982: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A46,A982,FINSEQ_4:68
.=G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence thesis by A980;
end;
end;
A983: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A984: P2[ma] & for n be Nat st P2[n] holds n<=ma from
NAT_1:sch 6 (A983,A981);
reconsider ma as Nat;
now
per cases;
suppose
A985: ma=len g;
j1+1<=i1 by A699,NAT_1:13;
then
A986: 1<=l by XREAL_1:19;
then len g1+1<=ma by A711,A940,A985,XREAL_1:7;
then
A987: len g1<=ma-1 by XREAL_1:19;
then 0+1<=ma by XREAL_1:19;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
reconsider q=g/.m1 as Point of TOP-REAL 2;
A988: ma-1<=len g by A985,XREAL_1:43;
then
A989: q`2=ppi`2 by A941,A987;
A990: pj`1<=q`1 by A941,A988,A987;
set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2 & pj
`1<=e`1 & e`1<=q`1};
A991: i1-l=j1;
A992: l in dom g2 by A711,A986,FINSEQ_3:25;
then
A993: g/.ma=g2/.l by A711,A940,A985,FINSEQ_4:69
.= pj by A711,A712,A992,A991;
then p1`1<=pj`1 by A984;
then
A994: p1`1=pj`1 by A979,XXREAL_0:1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A995: 1<=m1 by A987,XXREAL_0:2;
A996: m1+1=ma;
then q=|[q`1,q`2]| & LSeg(g,m1)=LSeg(pj,q) by A985,A993
,A995,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A767,A773,A989,A990,TOPREAL3:10;
then
A997: p1 in LSeg(g,m1) by A978,A994,A990;
LSeg(g,m1) in lg by A985,A995,A996;
hence thesis by A977,A997,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A984,XXREAL_0:1;
then
A998: ma+1<=len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL
2;
set lma = {p2: p2`2=ppi`2 & qa1`1<=p2`1 & p2`1<=qa`1};
A999: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A1000: p1`1<=qa`1 by A984;
A1001: len g1<=ma+1 by A984,NAT_1:13;
then
A1002: qa1 `2 = ppi`2 by A941,A998;
A1003: now
assume p1`1<=qa1`1;
then for q holds q=g/.(ma+1) implies p1`1<=q`1;
then ma+1<=ma by A984,A998,A1001;
hence contradiction by XREAL_1:29;
end;
A1004: qa`2=ppi`2 & qa=|[qa`1,qa`2]| by A941,A984,EUCLID:53;
A1005: 1<=ma by A24,A14,A47,A984,NAT_1:13;
then LSeg(g,ma)=LSeg(qa1,qa) by A998,TOPREAL1:def 3
.= lma by A1000,A1003,A1002,A1004,A999,TOPREAL3:10
,XXREAL_0:2;
then
A1006: x in LSeg(g,ma) by A977,A978,A1000,A1003;
LSeg(g,ma) in lg by A998,A1005;
hence thesis by A1006,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
A1007: len g=len g1 + len g2 by FINSEQ_1:22;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A45,FINSEQ_4:68
.=f/.1 by A27,A25,FINSEQ_4:71;
j1+1<=i1 by A699,NAT_1:13;
then
A1008: 1<=l by XREAL_1:19;
then
A1009: l in dom g2 by A712,FINSEQ_1:1;
hence g/.len g=g2/.l by A711,A1007,FINSEQ_4:69
.=G*(m1,i2) by A711,A712,A1009
.=f/.len f by A3,A21,A698;
thus len f<=len g by A3,A14,A47,A711,A1008,A1007,XREAL_1:7;
end;
case
A1010: i1=j1;
k<>k+1;
hence contradiction by A5,A27,A29,A19,A21,A698,A1010,PARTFUN2:10;
end;
case
A1011: i1<j1;
c1/.i1=c1.i1 by A66,A60,PARTFUN1:def 6;
then
A1012: c1/.i1=ppi by A66,MATRIX_0:def 8;
then
A1013: x2.i1=ppi`1 by A66,A65,A60,GOBOARD1:def 1;
c1/.j1=c1.j1 by A23,A60,PARTFUN1:def 6;
then
A1014: c1/.j1=pj by A23,MATRIX_0:def 8;
then
A1015: x2.j1 =pj`1 by A23,A65,A60,GOBOARD1:def 1;
then
A1016: ppi`1<pj`1 by A66,A23,A69,A65,A60,A1011,A1013,SEQM_3:def 1;
reconsider l=j1-i1 as Element of NAT by A1011,INT_1:5;
deffunc F(Nat) = G*(i1+$1,i2);
consider g2 such that
A1017: len g2 = l & for n being Nat st n in dom g2 holds g2
/.n = F(n) from FINSEQ_4:sch 2;
take g=g1^g2;
A1018: now
let n;
A1019: n<=i1+n by NAT_1:11;
assume
A1020: n in Seg l;
then n<=l by FINSEQ_1:1;
then
A1021: i1+n<=l+i1 by XREAL_1:7;
j1<=len G by A23,FINSEQ_3:25;
then
A1022: i1+n<=len G by A1021,XXREAL_0:2;
1<=n by A1020,FINSEQ_1:1;
then 1<=i1+n by A1019,XXREAL_0:2;
hence i1+n in dom G by A1022,FINSEQ_3:25;
hence [i1+n,i2] in Indices G by A22,A68,ZFMISC_1:87;
end;
A1023: Seg len g2 = dom g2 by FINSEQ_1:def 3;
now
let n such that
A1024: n in dom g2;
take m=i1+n,k=i2;
thus [m,k] in Indices G & g2/.n=G*(m,k) by A1017,A1018,A1023
,A1024;
end;
then
A1025: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G
*(i,j) by A75,GOBOARD1:23;
A1026: y2.i1=ppi`2 by A66,A63,A64,A65,A61,A60,A1012,GOBOARD1:def 2;
A1027: now
let n,p;
assume that
A1028: n in dom g2 and
A1029: g2/.n=p;
A1030: g2/.n=G*(i1+n,i2) by A1017,A1028;
set n1=i1+n;
set pn = G*(n1,i2);
A1031: i1+ n in dom G by A1017,A1018,A1023,A1028;
then
A1032: y2.n1=y2.i1 by A66,A70,A63,A64,A65,A61,A60,SEQM_3:def 10;
c1/.n1=c1.n1 by A60,A1017,A1018,A1023,A1028,PARTFUN1:def 6;
then
A1033: c1/.n1=pn by A1031,MATRIX_0:def 8;
then
A1034: x2.n1=pn`1 by A65,A60,A1031,GOBOARD1:def 1;
n<=len g2 by A1028,FINSEQ_3:25;
then
A1035: n1<=i1+len g2 by XREAL_1:7;
y2.n1=pn`2 by A63,A64,A65,A61,A60,A1031,A1033,GOBOARD1:def 2;
hence p`2=ppi`2 & ppi`1<=p`1 & p`1<=pj`1 by A66,A23,A69,A65,A60
,A1017,A1026,A1013,A1015,A1029,A1030,A1031,A1035,A1032,A1034,SEQ_4:137
,XREAL_1:31;
thus p in rng c1 by A60,A1029,A1030,A1031,A1033,PARTFUN2:2;
1<=n by A1028,FINSEQ_3:25;
then i1<n1 by XREAL_1:29;
hence p`1>ppi`1 by A66,A69,A65,A60,A1013,A1029,A1030,A1031
,A1034,SEQM_3:def 1;
end;
A1036: g2 is special
proof
let n be Nat;
set p = g2/.n;
assume
A1037: 1<=n & n+1 <= len g2;
then n in dom g2 by SEQ_4:134;
then
A1038: p`2=ppi`2 by A1027;
n+1 in dom g2 by A1037,SEQ_4:134;
hence thesis by A1027,A1038;
end;
now
let n,m be Element of NAT;
assume that
A1039: n in dom g2 & m in dom g2 and
A1040: n<>m;
A1041: g2/.n=G*(i1+n,i2) & g2/.m=G*(i1+m,i2) by A1017,A1039;
assume
A1042: g2/.n=g2/.m;
[ i1+n,i2] in Indices G & [i1+m,i2] in Indices G by A1017,A1018
,A1023,A1039;
then i1+n=i1+m by A1041,A1042,GOBOARD1:5;
hence contradiction by A1040;
end;
then for n,m being Element of NAT
st n in dom g2 & m in dom g2 & g2/.n = g2/.m
holds n = m;
then
A1043: g2 is one-to-one by PARTFUN2:9;
set lk={w where w is Point of TOP-REAL 2: w`2=ppi`2 & ppi`1<=w`1
& w`1<= pj`1};
A1044: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
A1045: now
let n,m,p,q;
assume that
A1046: n in dom g2 and
A1047: m in dom g2 and
A1048: n<m and
A1049: g2/.n=p & g2/.m=q;
A1050: i1+n in dom G by A1017,A1018,A1023,A1046;
set n1=i1+n, m1=i1+m;
set pn = G*(n1,i2), pm = G*(m1,i2);
A1051: n1<m1 by A1048,XREAL_1:8;
c1/.n1=c1.n1 by A60,A1017,A1018,A1023,A1046,PARTFUN1:def 6;
then c1/.n1=pn by A1050,MATRIX_0:def 8;
then
A1052: x2.n1=pn`1 by A65,A60,A1050,GOBOARD1:def 1;
A1053: i1+m in dom G by A1017,A1018,A1023,A1047;
c1/.m1 = c1.m1 by A60,A1017,A1018,A1023,A1047,PARTFUN1:def 6;
then c1/.m1=pm by A1053,MATRIX_0:def 8;
then
A1054: x2.m1=pm`1 by A65,A60,A1053,GOBOARD1:def 1;
g2/.n=G*(i1+n,i2) & g2/.m=G*(i1+m,i2) by A1017,A1046,A1047;
hence p`1<q`1 by A69,A65,A60,A1049,A1050,A1053,A1051,A1052
,A1054,SEQM_3:def 1;
end;
for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom
g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m)
proof
let n,m;
assume that
A1055: m>n+1 and
A1056: n in dom g2 and
A1057: n+1 in dom g2 and
A1058: m in dom g2 and
A1059: m+1 in dom g2 and
A1060: LSeg(g2,n) /\ LSeg(g2,m) <> {};
reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as
Point of TOP-REAL 2;
A1061: p1`2=ppi`2 & p2`2= ppi`2 by A1027,A1056,A1057;
n<n+1 by NAT_1:13;
then
A1062: p1`1<p2`1 by A1045,A1056,A1057;
set lp = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & p1`1<=
w`1 & w`1<=p2`1}, lq = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & q1`1<=w`1
& w`1<=q2`1};
A1063: p1=|[p1`1,p1`2]| & p2=|[p2`1,p2`2]| by EUCLID:53;
m<m+1 by NAT_1:13;
then
A1064: q1`1<q2`1 by A1045,A1058,A1059;
A1065: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
set x = the Element of LSeg(g2,n) /\ LSeg(g2,m);
A1066: x in LSeg(g2,n) by A1060,XBOOLE_0:def 4;
A1067: q1`2= ppi`2 & q2`2=ppi`2 by A1027,A1058,A1059;
A1068: x in LSeg(g2,m) by A1060,XBOOLE_0:def 4;
1 <= m & m+1<= len g2 by A1058,A1059,FINSEQ_3:25;
then LSeg(g2,m) = LSeg(q1,q2) by TOPREAL1:def 3
.=lq by A1064,A1067,A1065,TOPREAL3:10;
then
A1069: ex tm be Point of TOP-REAL 2 st tm=x & tm`2=ppi`2 & q1
`1<=tm`1 & tm`1<=q2`1 by A1068;
1 <= n & n+1 <= len g2 by A1056,A1057,FINSEQ_3:25;
then LSeg(g2,n) = LSeg(p1,p2) by TOPREAL1:def 3
.=lp by A1062,A1061,A1063,TOPREAL3:10;
then
A1070: ex tn be Point of TOP-REAL 2 st tn=x & tn`2=ppi`2 & p1
`1<=tn`1 & tn`1<=p2`1 by A1066;
p2`1<q1`1 by A1045,A1055,A1057,A1058;
hence contradiction by A1070,A1069,XXREAL_0:2;
end;
then
A1071: g2 is s.n.c. by GOBOARD2:1;
A1072: not f/.k in L~g2
proof
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume f/.k in L~g2;
then consider X be set such that
A1073: f/.k in X and
A1074: X in ls by TARSKI:def 4;
consider m such that
A1075: X=LSeg(g2,m) and
A1076: 1<=m & m+1 <= len g2 by A1074;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A1077: m in dom g2 by A1076,SEQ_4:134;
then
A1078: q1`2=ppi`2 by A1027;
set lq={w where w is Point of TOP-REAL 2: w`2=ppi`2 & q1`1<=w
`1 & w`1<=q2`1};
A1079: q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by EUCLID:53;
A1080: m+1 in dom g2 by A1076,SEQ_4:134;
then
A1081: q2`2=ppi`2 by A1027;
m<m+1 by NAT_1:13;
then
A1082: q1`1<q2`1 by A1045,A1077,A1080;
LSeg(g2,m)=LSeg(q1,q2) by A1076,TOPREAL1:def 3
.=lq by A1078,A1081,A1082,A1079,TOPREAL3:10;
then ex p st p=f/.k & p`2=ppi`2 & q1`1<=p`1 & p`1<=q2`1 by
A1073,A1075;
hence contradiction by A29,A1027,A1077;
end;
y2.j1=pj`2 by A23,A63,A64,A65,A61,A60,A1014,GOBOARD1:def 2;
then
A1083: ppi`2=pj`2 by A66,A23,A70,A63,A64,A65,A61,A60,A1026,SEQM_3:def 10
;
A1084: now
let n;
assume that
A1085: n in dom g2 and
A1086: n+1 in dom g2;
let l1,l2,l3,l4 be Nat;
assume that
A1087: [l1,l2] in Indices G and
A1088: [l3,l4] in Indices G and
A1089: g2/.n=G*(l1,l2) and
A1090: g2/.(n+1)=G*(l3,l4);
g2/.(n+1)=G*(i1+(n+1),i2) & [i1+(n+1),i2] in Indices G
by A1017,A1018,A1023,A1086;
then
A1091: l3=i1+(n+1) & l4=i2 by A1088,A1090,GOBOARD1:5;
g2/.n=G*(i1+n,i2) & [i1+n,i2] in Indices G by A1017,A1018,A1023
,A1085;
then l1=i1+n & l2=i2 by A1087,A1089,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= |.i1+n-(i1+(n+1)).|+0 by A1091,
ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
now
let l1,l2,l3,l4 be Nat;
assume that
A1092: [l1,l2] in Indices G and
A1093: [l3,l4] in Indices G and
A1094: g1/.len g1=G*(l1, l2) and
A1095: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A1096: 1 in dom g2;
g2/.1=G* (i1+1,i2) & [i1+1,i2] in Indices G by A1017,A1018
,A1023,A1096;
then
A1097: l3=i1+1 & l4=i2 by A1093,A1095,GOBOARD1:5;
f1/.len f1=f/.k by A27,A14,A51,FINSEQ_4:71;
then l1=i1 & l2=i2 by A46,A28,A29,A1092,A1094,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=|.i1-(i1+1).|+0 by A1097,
ABSVALUE:2
.=|.i1-i1+-1.|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [
m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A48,A1084,GOBOARD1:24;
hence g is_sequence_on G by A1025,GOBOARD1:def 9;
A1098: pj=|[pj`1,pj`2]| by EUCLID:53;
A1099: LSeg(f,k)=LSeg(ppi,pj) by A3,A24,A29,A21,A698,TOPREAL1:def 3
.= lk by A1016,A1083,A1044,A1098,TOPREAL3:10;
A1100: rng g2 c= LSeg(f,k)
proof
let x be object;
assume x in rng g2;
then consider n being Element of NAT such that
A1101: n in dom g2 and
A1102: g2/.n=x by PARTFUN2:2;
set pn = G*((i1+n),i2);
A1103: g2/.n=G*(i1+n,i2) by A1017,A1101;
then
A1104: pn`1<=pj`1 by A1027,A1101;
pn`2=ppi`2 & ppi`1<=pn`1 by A1027,A1101,A1103;
hence thesis by A1099,A1102,A1103,A1104;
end;
A1105: Seg l = dom g2 by A1017,FINSEQ_1:def 3;
A1106: not f/.k in rng g2
proof
assume f/.k in rng g2;
then consider n being Element of NAT such that
A1107: n in dom g2 and
A1108: g2/.n=f/.k by PARTFUN2:2;
g2/.n=G*(i1+n,i2) & [i1+n,i2] in Indices G by A1017,A1105,A1018
,A1107;
then
A1109: i1+n=i1 by A28,A29,A1108,GOBOARD1:5;
0<n by A1107,FINSEQ_3:25;
hence contradiction by A1109;
end;
rng g1 /\ rng g2 = {}
proof
set x = the Element of rng g1 /\ rng g2;
assume
A1110: not thesis;
then
A1111: x in rng g2 by XBOOLE_0:def 4;
A1112: x in rng g1 by A1110,XBOOLE_0:def 4;
now
per cases by A24,XXREAL_0:1;
suppose
k=1;
hence contradiction by A52,A1106,A1112,A1111,TARSKI:def 1;
end;
suppose
1<k;
then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k}
by A3,A6,A7,A49,A1100,A1112,A1111,GOBOARD2:4,XBOOLE_0:def 4;
hence contradiction by A1106,A1111,TARSKI:def 1;
end;
end;
hence contradiction;
end;
then rng g1 misses rng g2;
hence g is one-to-one by A40,A1043,FINSEQ_3:91;
A1113: LSeg(f,k)=LSeg(ppi,pj) by A3,A24,A29,A21,A698,TOPREAL1:def 3;
A1114: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2
,n+1) = {g2/.(n+1)}
proof
let n;
assume that
A1115: 1<=n and
A1116: n+2 <= len g2;
A1117: n+1 in dom g2 by A1115,A1116,SEQ_4:135;
then g2/.(n+1) in rng g2 by PARTFUN2:2;
then g2/.(n+1) in lk by A1099,A1100;
then consider u1 be Point of TOP-REAL 2 such that
A1118: g2/.(n+1)=u1 and
A1119: u1`2=ppi`2 and
ppi`1<=u1`1 and
u1`1<=pj`1;
A1120: n+2 in dom g2 by A1115,A1116,SEQ_4:135;
then g2/.(n+2) in rng g2 by PARTFUN2:2;
then g2/.(n+2) in lk by A1099,A1100;
then consider u2 be Point of TOP-REAL 2 such that
A1121: g2/.(n+2)=u2 and
A1122: u2`2=ppi`2 and
ppi`1<=u2`1 and
u2`1<=pj`1;
1<= n+1 & n+1+1 = n+(1+1) by NAT_1:11;
then
A1123: LSeg(g2,n+1)=LSeg( u1,u2) by A1116,A1118,A1121,TOPREAL1:def 3;
n+1<n+1+1 by NAT_1:13;
then
A1124: u1`1<u2`1 by A1045,A1117,A1120,A1118,A1121;
A1125: n in dom g2 by A1115,A1116,SEQ_4:135;
then g2/.n in rng g2 by PARTFUN2:2;
then g2/.n in lk by A1099,A1100;
then consider u be Point of TOP-REAL 2 such that
A1126: g2/.n=u and
A1127: u`2=ppi`2 and
ppi`1<=u`1 and
u`1<=pj`1;
n+1 <= n+2 by XREAL_1:6;
then n+1 <= len g2 by A1116,XXREAL_0:2;
then
A1128: LSeg(g2,n)=LSeg(u,u1) by A1115,A1126,A1118,TOPREAL1:def 3;
set lg = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & u`1<=w
`1 & w`1<=u2`1};
n<n+1 by NAT_1:13;
then
A1129: u`1<u1`1 by A1045,A1125,A1117,A1126,A1118;
then
A1130: u1 in lg by A1119,A1124;
u=|[u`1,u`2]| & u2=|[u2`1,u2`2 ]| by EUCLID:53;
then LSeg(g2/.n,g2/.(n+2))=lg by A1126,A1127,A1121,A1122,A1124
,A1129,TOPREAL3:10,XXREAL_0:2;
hence thesis by A1126,A1118,A1121,A1128,A1123,A1130,TOPREAL1:8;
end;
thus g is unfolded
proof
let n be Nat;
assume that
A1131: 1<=n and
A1132: n+2 <= len g;
A1133: n+1+1<=len g by A1132;
n+1<=n+1+1 by NAT_1:11;
then
A1134: n+1 <= len g by A1132,XXREAL_0:2;
A1135: len g=len g1+len g2 by FINSEQ_1:22;
n+2-len g1 = n-len g1 +2;
then
A1136: n-len g1 + 2 <= len g2 by A1132,A1135,XREAL_1:20;
A1137: 1<= n+1 by NAT_1:11;
A1138: n<=n+1 by NAT_1:11;
A1139: n+(1+1)=n+1+1;
per cases;
suppose
A1140: n+2 <= len g1;
A1141: n+(1+1)=n+1+1;
A1142: n+1 in dom g1 by A1131,A1140,SEQ_4:135;
then
A1143: g/.(n+1)=g1/.(n+1) by FINSEQ_4:68;
n in dom g1 by A1131,A1140,SEQ_4:135;
then
A1144: LSeg(g1,n)=LSeg(g,n) by A1142,TOPREAL3:18;
n+2 in dom g1 by A1131,A1140,SEQ_4:135;
then LSeg(g1,n+1)=LSeg(g,n+1) by A1142,A1141,TOPREAL3:18;
hence thesis by A41,A1131,A1140,A1144,A1143;
end;
suppose
len g1 < n+2;
then len g1+1<=n+2 by NAT_1:13;
then
A1145: len g1<=n+2-1 by XREAL_1:19;
now
per cases;
suppose
A1146: len g1=n+1;
then 1<=len g-len g1 by A1133,XREAL_1:19;
then 1 in dom g2 by A1135,FINSEQ_3:25;
then
A1147: g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A1099,A1100;
then consider u1 be Point of TOP-REAL 2 such that
A1148: g2/.1=u1 and
u1`2=ppi`2 and
ppi`1<=u1`1 and
u1`1<=pj`1;
ppi in LSeg(ppi,pj) by RLTOPSP1:68;
then
A1149: LSeg(ppi,u1) c= LSeg(f,k) by A1113,A1100,A1147,A1148,
TOPREAL1:6;
1<=n+1 by NAT_1:11;
then
A1150: n+1 in dom g1 by A1146,FINSEQ_3:25;
then
A1151: g/.(n+1)=f1/.len f1 by A46,A1146,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
now
1<len g1 by A1131,A1146,NAT_1:13;
then
A1152: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A1152,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A1153: L~f1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,GOBOARD2:4;
A1154: LSeg(g1,n) c= L~f1 by A44,TOPREAL3:19;
n in dom g1 by A1131,A1138,A1146,FINSEQ_3:25;
then
A1155: LSeg(g,n)=LSeg(g1,n) by A1150,TOPREAL3:18;
g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1)
by A1131,A1132,A1137,A1134,A1139,TOPREAL1:21;
then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by
XBOOLE_0:def 4;
then
A1156: {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:31;
n+2 = 1+len g1 & 1 <= len g2 by A1132,A1139,A1135,A1146,
XREAL_1:6;
then g/.(n+2)=g2/.1 by SEQ_4:136;
then LSeg(g,n+1)=LSeg(ppi,u1 ) by A1132,A1137,A1139,A1151
,A1148,TOPREAL1:def 3;
then LSeg(g,n) /\ LSeg(g,n+1) c= {g /.(n+1)} by A29,A1154
,A1153,A1155,A1151,A1149,XBOOLE_1:27;
hence thesis by A1156;
end;
suppose
len g1<>n+1;
then len g1<n+1 by A1145,XXREAL_0:1;
then
A1157: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A1158: len g1=n;
then
A1159: 2 <= len g2 by A1132,A1135,XREAL_1:6;
then 1 <= len g2 by XXREAL_0:2;
then
A1160: g/.(n+1)=g2/.1 by A1158,SEQ_4:136;
1<=len g2 by A1159,XXREAL_0:2;
then
A1161: 1 in dom g2 by FINSEQ_3:25;
then g2/.1 in rng g2 by PARTFUN2:2;
then g2/.1 in lk by A1099,A1100;
then consider u1 be Point of TOP-REAL 2 such that
A1162: g2/.1=u1 and
A1163: u1`2=ppi`2 & ppi`1<=u1`1 and
u1`1<=pj`1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then g/.n=f1/.len f1 by A46,A1158,FINSEQ_4:68
.= ppi by A27,A14,A51,A29,FINSEQ_4:71;
then
A1164: LSeg(g,n)=LSeg(ppi,u1) by A1131,A1134,A1160,A1162,
TOPREAL1:def 3;
A1165: 2 in dom g2 by A1159,FINSEQ_3:25;
then g2/.2 in rng g2 by PARTFUN2:2;
then g2/.2 in lk by A1099,A1100;
then consider u2 be Point of TOP-REAL 2 such that
A1166: g2 /.2=u2 and
A1167: u2`2=ppi`2 & ppi`1<=u2`1 and
u2`1<=pj`1;
set lg = {w where w is Point of TOP-REAL 2 : w`2=ppi
`2 & ppi`1<=w`1 & w`1<=u2`1};
u1`1<u2`1 by A1045,A1161,A1165,A1162,A1166;
then u2=|[u2`1,u2`2]| & u1 in lg by A1163,EUCLID:53;
then
A1168: u1 in LSeg(ppi,u2) by A1044,A1167,TOPREAL3:10;
g/.(n+2)=g2/.2 by A1158,A1159,SEQ_4:136;
then LSeg(g,n+1)=LSeg(u1,u2) by A1132,A1137,A1139
,A1160,A1162,A1166,TOPREAL1:def 3;
hence thesis by A1160,A1162,A1164,A1168,TOPREAL1:8;
end;
suppose
len g1<>n;
then
A1169: len g1<n by A1157,XXREAL_0:1;
then len g1+1<=n by NAT_1:13;
then
A1170: 1<=n1 by XREAL_1:19;
n1 + len g1 = n;
then
A1171: LSeg(g,n)=LSeg(g2,n1) by A1134,A1169,GOBOARD2:5;
A1172: n+1 = n1+1+len g1;
then n1+1<=len g2 by A1134,A1135,XREAL_1:6;
then
A1173: g/.(n+1)=g2/.(n1+1) by A1172,NAT_1:11,SEQ_4:136;
len g1<n+1 by A1138,A1169,XXREAL_0:2;
then LSeg(g,n+1)=LSeg(g2,n1+1) by A1133,A1172,
GOBOARD2:5;
hence thesis by A1114,A1136,A1171,A1173,A1170;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
A1174: L~g2 c= LSeg(f,k)
proof
let x be object;
set ls={LSeg(g2,m): 1<=m & m+1 <= len g2};
assume x in L~g2;
then consider X be set such that
A1175: x in X and
A1176: X in ls by TARSKI:def 4;
consider m such that
A1177: X=LSeg(g2,m) and
A1178: 1<=m & m+1 <= len g2 by A1176;
reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2;
A1179: LSeg(g2,m)=LSeg(q1,q2) by A1178,TOPREAL1:def 3;
m+1 in dom g2 by A1178,SEQ_4:134;
then
A1180: g2/.(m+1) in rng g2 by PARTFUN2:2;
m in dom g2 by A1178,SEQ_4:134;
then g2/.m in rng g2 by PARTFUN2:2;
then LSeg(q1,q2) c= LSeg(ppi,pj) by A1113,A1100,A1180,
TOPREAL1:6;
hence thesis by A1113,A1175,A1177,A1179;
end;
A1181: L~g1 /\ L~g2 = {}
proof
per cases;
suppose
k=1;
hence thesis by A52;
end;
suppose
k<>1;
then 1<k by A24,XXREAL_0:1;
then L~g1 /\ LSeg(f,k)={f/.k} by A3,A6,A7,A44,GOBOARD2:4;
then
A1182: L~g1 /\ L~g2 c= {f/.k} by A1174,XBOOLE_1:26;
now
set x = the Element of L~g1 /\ L~g2;
assume L~g1 /\ L~g2 <> {};
then x in {f/.k} & x in L~g2 by A1182,XBOOLE_0:def 4;
hence contradiction by A1072,TARSKI:def 1;
end;
hence thesis;
end;
end;
for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g
& m+1 in dom g holds LSeg(g,n) misses LSeg(g,m)
proof
A1183: 1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A1184: g/.len g1=g1/.len g1 by FINSEQ_4:68
.= ppi by A27,A14,A51,A46,A29,FINSEQ_4:71;
reconsider qq=g2/.1 as Point of TOP-REAL 2;
set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j):
1<=j & j+1 <= len g2};
let n,m;
assume that
A1185: m>n+1 and
A1186: n in dom g and
A1187: n+1 in dom g and
A1188: m in dom g and
A1189: m+1 in dom g;
A1190: 1<=n by A1186,FINSEQ_3:25;
i1+1<=j1 by A1011,NAT_1:13;
then
A1191: 1<=l by XREAL_1:19;
then
A1192: 1 in dom g2 by A1017,FINSEQ_3:25;
then
A1193: qq`2=ppi`2 & qq`1>ppi`1 by A1027;
A1194: g/.(len g1+1)=qq by A1017,A1191,SEQ_4:136;
A1195: qq`1<=pj`1 by A1027,A1192;
A1196: m+1<=len g by A1189,FINSEQ_3:25;
A1197: 1<=m+1 by A1189,FINSEQ_3:25;
A1198: 1<=n+1 by A1187,FINSEQ_3:25;
A1199: n+1<=len g by A1187,FINSEQ_3:25;
A1200: qq=|[qq`1,qq`2]| by EUCLID:53;
A1201: 1<=m by A1188,FINSEQ_3:25;
set ql={z where z is Point of TOP-REAL 2: z`2=ppi`2 & ppi`1<=z
`1 & z`1<=qq`1};
A1202: n<=n+1 by NAT_1:11;
A1203: len g=len g1+len g2 by FINSEQ_1:22;
then len g1+1<=len g by A1017,A1191,XREAL_1:7;
then
A1204: LSeg(g,len g1)=LSeg(ppi,qq) by A1183,A1184,A1194,TOPREAL1:def 3
.= ql by A1044,A1193,A1200,TOPREAL3:10;
A1205: m<=m+1 by NAT_1:11;
then
A1206: n+1<=m+1 by A1185,XXREAL_0:2;
now
per cases;
suppose
A1207: m+1<=len g1;
then m<=len g1 by A1205,XXREAL_0:2;
then
A1208: m in dom g1 by A1201,FINSEQ_3:25;
m+1 in dom g1 by A1197,A1207,FINSEQ_3:25;
then
A1209: LSeg(g,m)=LSeg(g1,m) by A1208,TOPREAL3:18;
A1210: n+1<=len g1 by A1206,A1207,XXREAL_0:2;
then n<=len g1 by A1202,XXREAL_0:2;
then
A1211: n in dom g1 by A1190,FINSEQ_3:25;
n+1 in dom g1 by A1198,A1210,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A1211,TOPREAL3:18;
hence thesis by A42,A1185,A1209;
end;
suppose
len g1<m+1;
then
A1212: len g1<=m by NAT_1:13;
then reconsider m1=m-len g1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A1213: m=len g1;
A1214: LSeg(g,m) c= LSeg(f,k)
proof
let x be object;
assume x in LSeg(g,m);
then consider px be Point of TOP-REAL 2 such that
A1215: px =x & px`2=ppi`2 & ppi`1<=px`1 and
A1216: px`1<=qq`1 by A1204,A1213;
pj`1>=px`1 by A1195,A1216,XXREAL_0:2;
hence thesis by A1099,A1215;
end;
n<=len g1 by A1185,A1202,A1213,XXREAL_0:2;
then
A1217: n in dom g1 by A1190,FINSEQ_3:25;
now
1<len g1 by A1185,A1198,A1213,XXREAL_0:2;
then
A1218: 1+1<=len g1 by NAT_1:13;
assume k=1;
hence contradiction by A52,A1218,TOPREAL1:23;
end;
then 1<k by A24,XXREAL_0:1;
then
A1219: L~f1 /\ LSeg(f,k) ={f/.k} by A3,A6,A7,GOBOARD2:4;
A1220: n+1 in dom g1 by A1185,A1198,A1213,FINSEQ_3:25;
then
A1221: LSeg(g,n)=LSeg(g1,n) by A1217,TOPREAL3:18;
then LSeg(g,n) in l1 by A1185,A1190,A1213;
then LSeg(g,n) c= L~f1 by A44,ZFMISC_1:74;
then
A1222: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A1219,A1214,
XBOOLE_1:27;
now
set x = the Element of LSeg(g,n)/\ LSeg(g,m);
assume
A1223: LSeg(g,n)/\ LSeg(g,m)<>{};
then
A1224: x in LSeg(g,n) by XBOOLE_0:def 4;
x in {f/.k} by A1222,A1223;
then
A1225: x=f/.k by TARSKI:def 1;
f/.k=g1/.len g1 by A27,A14,A51,A46,FINSEQ_4:71;
hence
contradiction by A40,A41,A42,A1185,A1213,A1217,A1220
,A1221,A1224,A1225,GOBOARD2:2;
end;
hence thesis;
end;
suppose
m<>len g1;
then
A1226: len g1<m by A1212,XXREAL_0:1;
then len g1+1<= m by NAT_1:13;
then
A1227: 1<=m1 by XREAL_1:19;
m+1=m1+1+len g1;
then
A1228: m1+1 <= len g2 by A1196,A1203,XREAL_1:6;
m = m1+len g1;
then
A1229: LSeg(g,m)=LSeg(g2,m1) by A1196,A1226,GOBOARD2:5;
then LSeg(g,m) in l2 by A1227,A1228;
then
A1230: LSeg(g,m) c= L~g2 by ZFMISC_1:74;
now
per cases;
suppose
A1231: n+1<=len g1;
then n<=len g1 by A1202,XXREAL_0:2;
then
A1232: n in dom g1 by A1190,FINSEQ_3:25;
n+1 in dom g1 by A1198,A1231,FINSEQ_3:25;
then LSeg(g,n)=LSeg(g1,n) by A1232,TOPREAL3:18;
then LSeg(g,n) in l1 by A1190,A1231;
then LSeg(g,n) c= L~g1 by ZFMISC_1:74;
then LSeg(g,n) /\ LSeg(g,m) = {} by A1181,A1230,
XBOOLE_1:3,27;
hence thesis;
end;
suppose
len g1<n+1;
then
A1233: len g1<=n by NAT_1:13;
then reconsider n1=n-len g1 as Element of NAT by
INT_1:5;
A1234: n - len g1 + 1 = n + 1 - len g1;
A1235: n = n1 + len g1;
now
per cases;
suppose
A1236: len g1=n;
now
reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point
of TOP-REAL 2;
set x = the Element of LSeg(g,n) /\ LSeg(g,m);
set q1l={v where v is Point of TOP-REAL 2: v
`2=ppi`2 & q1`1<=v`1 & v`1<=q2`1};
A1237: q1=|[q1`1,q1 `2]| & q2=|[q2`1,q2`2]|
by EUCLID:53;
assume
A1238: LSeg(g,n) /\ LSeg(g,m)<>{};
then
A1239: x in LSeg(g,m) by XBOOLE_0:def 4;
x in LSeg(g,n) by A1238,XBOOLE_0:def 4;
then
A1240: ex qx be Point of TOP-REAL 2 st qx=x
& qx`2=ppi`2 & ppi`1<=qx`1 & qx`1<=qq`1 by A1204,A1236;
A1241: m1 in dom g2 by A1227,A1228,SEQ_4:134;
then
A1242: q1 `2=ppi`2 by A1027;
A1243: m1+1 in dom g2 by A1227,A1228,SEQ_4:134;
then
A1244: q2`2=ppi`2 by A1027;
m1<m1+1 by NAT_1:13;
then
A1245: q1`1<q2`1 by A1045,A1241,A1243;
LSeg(g2,m1)=LSeg(q1,q2) by A1227,A1228,
TOPREAL1:def 3
.=q1l by A1242,A1244,A1245,A1237,
TOPREAL3:10;
then
A1246: ex qy be Point of TOP-REAL 2 st qy=x
& qy`2=ppi`2 & q1`1<=qy`1 & qy`1<=q2`1 by A1229,A1239;
m1 > n1 + 1 & n1 + 1 >= 1 by A1185,A1234,
NAT_1:11,XREAL_1:9;
then m1 > 1 by XXREAL_0:2;
then qq`1<q1`1 by A1045,A1192,A1241;
hence contradiction by A1240,A1246,XXREAL_0:2
;
end;
hence thesis;
end;
suppose
n<>len g1;
then len g1<n by A1233,XXREAL_0:1;
then
A1247: LSeg(g,n)=LSeg(g2,n1) by A1199,A1235,GOBOARD2:5
;
m1>n1+1 by A1185,A1234,XREAL_1:9;
hence thesis by A1071,A1229,A1247;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence g is s.n.c. by GOBOARD2:1;
now
set p=g1/.len g1, q=g2/.1;
i1+1<=j1 by A1011,NAT_1:13;
then 1<=l by XREAL_1:19;
then 1 in dom g2 by A1017,FINSEQ_3:25;
then q`2=ppi`2 by A1027;
hence p`1=q`1 or p`2=q`2 by A27,A14,A51,A46,A29,FINSEQ_4:71;
end;
hence g is special by A43,A1036,GOBOARD2:8;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1 <= len g}, lf = {LSeg(f,j): 1
<=j & j+1 <= len f};
A1248: len g = len g1 + len g2 by FINSEQ_1:22;
A1249: now
let j;
assume that
A1250: len g1<=j and
A1251: j<=len g;
reconsider w = j-len g1 as Element of NAT by A1250,INT_1:5;
let p such that
A1252: p=g/.j;
now
per cases;
suppose
A1253: j=len g1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A1254: g/.len g1 = f1/.len f1 by A46,FINSEQ_4:68
.= G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence p`2=G*(i1,i2)`2 by A1252,A1253;
thus G*(i1,i2)`1<=p`1 & p`1<=G* (j1,i2)`1 by A66,A23,A69
,A65,A60,A1011,A1013,A1015,A1252,A1253,A1254,SEQM_3:def 1;
thus p in rng c1 by A66,A60,A1012,A1252,A1253,A1254,
PARTFUN2:2;
end;
suppose
j<>len g1;
then len g1 < j by A1250,XXREAL_0:1;
then len g1 + 1 <= j by NAT_1:13;
then
A1255: 1<=w by XREAL_1:19;
A1256: w<=len g2 by A1248,A1251,XREAL_1:20;
then
A1257: w in dom g2 by A1255,FINSEQ_3:25;
j = w + len g1;
then g/.j=g2/.w by A1255,A1256,SEQ_4:136;
hence p`2=ppi`2 & ppi`1<=p`1 & p`1<= pj`1 & p in rng c1
by A1027,A1252,A1257;
end;
end;
hence p`2=ppi`2 & ppi`1<=p`1 & p`1<=pj`1 & p in rng c1;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A1258: x in X and
A1259: X in lg by TARSKI:def 4;
consider i such that
A1260: X=LSeg(g,i) and
A1261: 1<=i and
A1262: i+1 <= len g by A1259;
now
per cases;
suppose
A1263: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A1263,XXREAL_0:2;
then
A1264: i in dom g1 by A1261,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A1263,FINSEQ_3:25;
then X=LSeg(g1,i) by A1260,A1264,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A1261
,A1263;
then
A1265: x in L~f1 by A44,A1258,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A1265;
end;
suppose
A1266: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A1267: i<=len g by A1262,NAT_1:13;
A1268: len g1<=i by A1266,NAT_1:13;
then
A1269: q1`2=ppi`2 by A1249,A1267;
A1270: q1`1<=pj`1 by A1249,A1268,A1267;
A1271: ppi`1<=q1`1 by A1249,A1268,A1267;
q2`2=ppi`2 by A1249,A1262,A1266;
then
A1272: q2=|[q2`1, q1`2]| by A1269,EUCLID:53;
A1273: q2`1<=pj`1 by A1249,A1262,A1266;
A1274: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A1261,A1262,
EUCLID:53,TOPREAL1:def 3;
A1275: ppi`1<= q2`1 by A1249,A1262,A1266;
now
per cases by XXREAL_0:1;
suppose
q1`1>q2`1;
then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1
<=q1`1} by A1272,A1274,TOPREAL3:10;
then consider p2 such that
A1276: p2 =x & p2`2=q1`2 and
A1277: q2`1<=p2`1 & p2`1<=q1`1 by A1258,A1260;
ppi`1<=p2`1 & p2`1<=pj`1 by A1270,A1275,A1277,
XXREAL_0:2;
then
A1278: x in LSeg(f,k) by A1099,A1269,A1276;
LSeg(f,k) in lf by A3,A24;
hence thesis by A1278,TARSKI:def 4;
end;
suppose
q1`1=q2`1;
then LSeg(g,i)={q1} by A1272,A1274,RLTOPSP1:70;
then x=q1 by A1258,A1260,TARSKI:def 1;
then
A1279: x in LSeg(f,k) by A1099,A1269,A1271,A1270;
LSeg(f,k) in lf by A3,A24;
hence thesis by A1279,TARSKI:def 4;
end;
suppose
q1`1<q2`1;
then LSeg(g,i)= {p1: p1`2=q1`2 & q1`1<=p1`1 & p1`1
<=q2`1} by A1272,A1274,TOPREAL3:10;
then consider p2 such that
A1280: p2 =x & p2`2=q1`2 and
A1281: q1`1<=p2`1 & p2`1<=q2`1 by A1258,A1260;
ppi`1<=p2`1 & p2`1<=pj`1 by A1271,A1273,A1281,
XXREAL_0:2;
then
A1282: x in LSeg(f,k) by A1099,A1269,A1280;
LSeg(f,k) in lf by A3,A24;
hence thesis by A1282,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let x be object;
assume x in L~f;
then
A1283: x in L~f1 \/ LSeg(f,k) by A3,A13,GOBOARD2:3;
now
per cases by A1283,XBOOLE_0:def 3;
suppose
A1284: x in L~f1;
L~g1 c= L~g by GOBOARD2:6;
hence thesis by A44,A1284;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A1285: p1=x and
A1286: p1`2=ppi`2 and
A1287: ppi`1<=p1`1 and
A1288: p1`1<=pj`1 by A1099;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=
g/.$1 holds q`1<=p1`1;
A1289: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A1248,XREAL_1:31;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A1290: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A46,A1290,FINSEQ_4:68
.=G*(i1,i2) by A27,A14,A51,A29,FINSEQ_4:71;
hence thesis by A1287;
end;
end;
A1291: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A1292: P2[ma] & for n be Nat st P2[n] holds n<=ma from
NAT_1:sch 6 (A1291,A1289);
reconsider ma as Nat;
now
per cases;
suppose
A1293: ma=len g;
i1+1<=j1 by A1011,NAT_1:13;
then
A1294: 1<=l by XREAL_1:19;
then len g1+1<=ma by A1017,A1248,A1293,XREAL_1:7;
then
A1295: len g1<=ma-1 by XREAL_1:19;
then 0+1<=ma by XREAL_1:19;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
reconsider q=g/.m1 as Point of TOP-REAL 2;
A1296: ma-1<=len g by A1293,XREAL_1:43;
then
A1297: q`2=ppi`2 by A1249,A1295;
A1298: q`1<=pj`1 by A1249,A1296,A1295;
set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2 &
q`1<=e`1 & e`1<=pj`1};
A1299: i1+l=j1;
A1300: l in dom g2 by A1017,A1294,FINSEQ_3:25;
then
A1301: g/.ma=g2/.l by A1017,A1248,A1293,FINSEQ_4:69
.= pj by A1017,A1300,A1299;
then pj`1<=p1`1 by A1292;
then
A1302: p1`1=pj`1 by A1288,XXREAL_0:1;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then
A1303: 1<=m1 by A1295,XXREAL_0:2;
A1304: m1+1=ma;
then q=|[q`1,q`2]| & LSeg(g,m1)=LSeg(q,pj) by A1293
,A1301,A1303,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A1083,A1098,A1297,A1298,
TOPREAL3:10;
then
A1305: p1 in LSeg(g,m1) by A1286,A1302,A1298;
LSeg(g,m1) in lg by A1293,A1303,A1304;
hence thesis by A1285,A1305,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A1292,XXREAL_0:1;
then
A1306: ma+1<=len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of
TOP-REAL 2;
set lma = {p2: p2`2=ppi`2 & qa`1<=p2`1 & p2`1<=qa1`1};
A1307: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A1308: qa`1<=p1`1 by A1292;
A1309: len g1<=ma+1 by A1292,NAT_1:13;
then
A1310: qa1 `2 = ppi`2 by A1249,A1306;
A1311: now
assume qa1`1<=p1`1;
then for q holds q=g/.(ma+1) implies q`1<=p1`1;
then ma+1<=ma by A1292,A1306,A1309;
hence contradiction by XREAL_1:29;
end;
A1312: qa`2=ppi`2 & qa=|[qa`1,qa`2]| by A1249,A1292,EUCLID:53;
A1313: 1<=ma by A24,A14,A47,A1292,NAT_1:13;
then LSeg(g,ma)=LSeg(qa,qa1) by A1306,TOPREAL1:def 3
.= lma by A1308,A1311,A1310,A1312,A1307,TOPREAL3:10
,XXREAL_0:2;
then
A1314: x in LSeg(g,ma) by A1285,A1286,A1308,A1311;
LSeg(g,ma) in lg by A1306,A1313;
hence thesis by A1314,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
1<=len g1 by A24,A14,A47,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A45,FINSEQ_4:68
.=f/.1 by A27,A25,FINSEQ_4:71;
A1315: len g=len g1 + l by A1017,FINSEQ_1:22;
i1+1<=j1 by A1011,NAT_1:13;
then
A1316: 1<=l by XREAL_1:19;
then
A1317: l in dom g2 by A1017,FINSEQ_3:25;
hence g/.len g=g2/.l by A1315,FINSEQ_4:69
.=G*(i1+l,i2) by A1017,A1317
.=f/.len f by A3,A21,A698;
thus len f<=len g by A3,A14,A47,A1316,A1315,XREAL_1:7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
A1318: P[0]
proof
let f such that
A1319: len f=0 and
A1320: ( for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j))
& f is one-to-one unfolded s.n.c. special;
take g=f;
f= {} by A1319;
then
for n holds n in dom g & n+1 in dom g implies for m,k,i,j st [m,k] in
Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds |.m-i.|
+|.k-j.|=1;
hence thesis by A1320,GOBOARD1:def 9;
end;
for k holds P[k] from NAT_1:sch 2(A1318,A1);
hence thesis;
end;
theorem
(for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) & f
is being_S-Seq implies ex g st g is_sequence_on G & g is being_S-Seq & L~f = L~
g & f/.1 = g/.1 & f/.len f = g/.len g & len f<=len g
proof
assume that
A1: for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j) and
A2: f is being_S-Seq;
f is one-to-one & f is unfolded s.n.c. special by A2;
then consider g such that
A3: g is_sequence_on G and
A4: g is one-to-one unfolded s.n.c. special and
A5: L~f = L~g & f/.1 = g/.1 & f/.len f = g/.len g and
A6: len f <= len g by A1,Th1;
take g;
thus g is_sequence_on G by A3;
2<=len f by A2;
then 2<=len g by A6,XXREAL_0:2;
hence g is being_S-Seq by A4;
thus thesis by A5,A6;
end;