:: Properties of Go-Board - Part III
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2016 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 15;
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: 1j2;
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`2n+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;
nm;
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;
0n+1;
then len g1n;
then
A239: len g11;
then 1 {};
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{};
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{};
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 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 g1n1+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=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 mak+1;
hence contradiction by A5,A27,A29,A19,A21,A76,A389,PARTFUN2:10;
end;
case
A390: i2ppi`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: nn+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;
nn+1;
then len g1n;
then
A549: len g11;
then 1 {};
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=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{};
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{};
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 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 g1n1+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`2len g;
then maj1;
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`1n+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;
nm;
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;
0n+1;
then len g1n;
then
A860: len g11;
then 1 {};
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{};
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{};
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 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 g1n1+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=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 mak+1;
hence contradiction by A5,A27,A29,A19,A21,A698,A1010,PARTFUN2:10;
end;
case
A1011: i1ppi`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: nn+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;
nn+1;
then len g1n;
then
A1169: len g11;
then 1 {};
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=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{};
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{};
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 n1 + 1 & n1 + 1 >= 1 by A1185,A1234,
NAT_1:11,XREAL_1:9;
then m1 > 1 by XXREAL_0:2;
then qq`1len g1;
then len g1n1+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`1len g;
then ma