:: Go-Board Theorem
:: 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, SUBSET_1, FINSEQ_1, GOBOARD1,
XXREAL_0, PARTFUN1, RELAT_1, INCSP_1, MATRIX_1, TREES_1, XBOOLE_0,
CARD_1, ARYTM_3, NAT_1, TARSKI, FUNCT_1, ARYTM_1, ZFMISC_1, COMPLEX1,
ORDINAL4, TOPREAL1, REAL_1, XXREAL_1, GOBOARD2, MCART_1, TOPREAL4,
GOBOARD4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
REAL_1, XREAL_0, COMPLEX1, XXREAL_0, XXREAL_1, NAT_1, RELAT_1, FUNCT_1,
PARTFUN1, FINSEQ_1, MATRIX_0, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1,
TOPREAL4, GOBOARD1, GOBOARD2;
constructors XXREAL_1, COMPLEX1, FINSEQ_3, TOPREAL1, TOPREAL4, GOBOARD2,
GOBOARD1, RELSET_1, REAL_1, MATRIX_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0,
EUCLID, GOBOARD2, VALUED_0, CARD_1, GOBOARD1, NAT_1, INT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI;
expansions TARSKI;
theorems TARSKI, NAT_1, ZFMISC_1, FINSEQ_1, ABSVALUE, FINSEQ_2, TOPREAL1,
TOPREAL4, GOBOARD1, GOBOARD2, FINSEQ_3, FINSEQ_4, FUNCT_1, PARTFUN2,
INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1, XXREAL_0, XXREAL_1,
PARTFUN1, SEQM_3, SEQ_4, MATRIX_0;
schemes NAT_1, FINSEQ_4;
begin
reserve p,p1,p2,q1,q2 for Point of TOP-REAL 2,
P1,P2 for Subset of TOP-REAL 2,
f,f1,f2,g1,g2 for FinSequence of TOP-REAL 2,
n,m,i,j,k for Nat,
G,G1 for Go-board,
x,y for set;
theorem Th1:
for G,f1,f2 st 1<=len f1 & 1<=len f2 &
f1 is_sequence_on G & f2 is_sequence_on G &
f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G)
holds rng f1 meets rng f2
proof
defpred P[Nat] means
for G1,g1,g2 st $1=width G1 & $1>0 & 1<=len g1 & 1<=len g2 &
g1 is_sequence_on G1 & g2 is_sequence_on G1 &
g1/.1 in rng Line(G1,1) & g1/.len g1 in rng Line(G1,len G1) &
g2/.1 in rng Col(G1,1) & g2/.len g2 in rng Col(G1,width G1)
holds rng g1 /\ rng g2 <> {};
let G,f1,f2;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
let G1,g1,g2 such that
A3: k+1=width G1 and
k+1>0 and
A4: 1<=len g1 and
A5: 1<=len g2 and
A6: g1 is_sequence_on G1 and
A7: g2 is_sequence_on G1 and
A8: g1/.1 in rng Line(G1,1) and
A9: g1/.len g1 in rng Line(G1,len G1) and
A10: g2/.1 in rng Col(G1,1) and
A11: g2/.len g2 in rng Col(G1,width G1);
defpred P[Nat] means $1 in dom g2 & g2/.$1 in rng Col(G1,width G1);
A12: ex m be Nat st P[m] by A5,A11,FINSEQ_3:25;
consider m be Nat such that
A13: P[m] & for i be Nat st P[i] holds m<=i from NAT_1:sch 5(A12);
reconsider m as Nat;
set g = g2|m;
A14: g/.1 in rng Col(G1,1) by A10,A13,FINSEQ_4:92;
A15: g is_sequence_on G1 by A7,GOBOARD1:22;
A16: m<=len g2 by A13,FINSEQ_3:25;
then
A17: len g = m by FINSEQ_1:59;
A18: rng g c= rng g2
proof
let x be object;
assume x in rng g;
then consider n being Element of NAT such that
A19: n in dom g and
A20: x=g/.n by PARTFUN2:2;
A21: n in Seg m by A17,A19,FINSEQ_1:def 3;
then
A22: n in dom g2 by A13,FINSEQ_4:71;
x=g2/.n by A13,A20,A21,FINSEQ_4:71;
hence thesis by A22,PARTFUN2:2;
end;
reconsider L1 = Line(G1,1), Ll = Line(G1,len G1) as FinSequence of
TOP-REAL 2;
A23: dom g2 = Seg len g2 by FINSEQ_1:def 3;
A24: dom g = Seg len g by FINSEQ_1:def 3;
0<>len G1 by MATRIX_0:def 10;
then
A25: 0+1<=len G1 by NAT_1:14;
then
A26: 1 in dom G1 by FINSEQ_3:25;
A27: len G1 in dom G1 by A25,FINSEQ_3:25;
A28: g/.len g in rng Col(G1,width G1) by A13,FINSEQ_4:93;
defpred P[Nat] means $1 in dom G1 & rng g /\ rng Line(G1,$1) <> {};
A29: for n be Nat st P[n] holds n<=len G1 by FINSEQ_3:25;
0<>width G1 by MATRIX_0:def 10;
then
A30: 0+1<=width G1 by NAT_1:14;
then
A31: 1 in Seg width G1 by FINSEQ_1:1;
A32: 1<=len g by A13,GOBOARD1:22;
then
A33: 1 in dom g by FINSEQ_3:25;
A34: ex n be Nat st P[n]
proof
m in dom g2 implies g2/.1 = (g2|m)/.1 by FINSEQ_4:92;
then consider i being Nat such that
A35: i in dom Col(G1,1) and
A36: g/.1=Col(G1,1).i by A10,A13,FINSEQ_2:10;
reconsider i as Nat;
take i;
i in Seg len Col(G1,1) by A35,FINSEQ_1:def 3;
then i in Seg len G1 by MATRIX_0:def 8;
hence i in dom G1 by FINSEQ_1:def 3;
then
A37: g/.1=Line(G1,i).1 by A31,A36,MATRIX_0:42;
A38: g/.1 in rng g by A33,PARTFUN2:2;
len Line(G1,i)=width G1 by MATRIX_0:def 7;
then dom Line(G1,i) = Seg width G1 by FINSEQ_1:def 3;
then g/.1 in rng Line(G1,i) by A31,A37,FUNCT_1:def 3;
hence thesis by A38,XBOOLE_0:def 4;
end;
consider mi be Nat such that
A39: P[mi] & for n be Nat st P[n] holds mi<=n from NAT_1:sch 5(A34);
A40: ex n be Nat st P[n] by A34;
consider ma be Nat such that
A41: P[ma] & for n be Nat st P[n] holds n<=ma from NAT_1:sch 6(A29,A40
);
reconsider mi,ma as Nat;
A42: 1<=mi by A39,FINSEQ_3:25;
reconsider Lmi = Line(G1,mi) as FinSequence of TOP-REAL 2;
defpred P[Nat] means $1 in dom g1 & g1/.$1 in rng Line(G1,mi);
A43: for n be Nat st P[n] holds n<=len g1 by FINSEQ_3:25;
A44: mi<=len G1 by A39,FINSEQ_3:25;
then ex n st P[n] by A4,A6,A8,A9,A42,GOBOARD1:29;
then
A45: ex n be Nat st P[n];
consider ma1 be Nat such that
A46: P[ma1] & for n be Nat st P[n] holds n<= ma1 from NAT_1:sch 6(A43,
A45);
A47: ma<=len G1 by A41,FINSEQ_3:25;
1<=mi by A39,FINSEQ_3:25;
then reconsider l1=mi-1, l2=len G1-ma as Element of NAT by A47,INT_1:5;
A48: ma<=len G1 by A41,FINSEQ_3:25;
reconsider ma1 as Nat;
consider k1 be Element of NAT such that
A49: k1 in dom Lmi and
A50: g1/.ma1 = Lmi/.k1 by A46,PARTFUN2:2;
Seg len Lmi = dom Lmi by FINSEQ_1:def 3;
then
A51: k1 in Seg width G1 by A49,MATRIX_0:def 7;
A52: dom G1 = Seg len G1 by FINSEQ_1:def 3;
A53: mi=ma implies rng g1 /\ rng g2 <> {}
proof
consider n such that
A54: n in dom g1 and
A55: g1/.n in rng Line(G1,mi) by A4,A6,A8,A9,A42,A44,GOBOARD1:29;
consider i being Element of NAT such that
A56: i in dom Line(G1,mi) and
A57: g1/.n=Lmi/.i by A55,PARTFUN2:2;
A58: 1<=i by A56,FINSEQ_3:25;
A59: len Line(G1,mi)=width G1 by MATRIX_0:def 7;
then i<=width G1 by A56,FINSEQ_3:25;
then consider m such that
A60: m in dom g and
A61: g/.m in rng Col(G1,i) by A32,A15,A14,A28,A58,GOBOARD1:33;
A62: g/.m in rng g by A60,PARTFUN2:2;
reconsider Ci = Col(G1,i) as FinSequence of TOP-REAL 2;
A63: len Col(G1,i)= len G1 by MATRIX_0:def 8;
then
A64: dom Col(G1,i) = Seg len G1 by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
assume
A65: mi=ma;
A66: dom Line(G1,mi) = Seg len Line(G1,mi) by FINSEQ_1:def 3;
consider j being Element of NAT such that
A67: j in dom Ci and
A68: g/.m=Ci/.j by A61,PARTFUN2:2;
reconsider Lj = Line(G1,j) as FinSequence of TOP-REAL 2;
len Line(G1,mi) = width G1 by MATRIX_0:def 7
.= len Lj by MATRIX_0:def 7;
then
A69: dom Line(G1,mi) = dom Lj by A66,FINSEQ_1:def 3;
A70: g/.m = Ci.j by A67,A68,PARTFUN1:def 6
.= Lj.i by A56,A66,A59,A64,A67,MATRIX_0:42
.= Lj/.i by A56,A69,PARTFUN1:def 6;
len Lj=width G1 by MATRIX_0:def 7;
then i in dom Lj by A56,A66,A59,FINSEQ_1:def 3;
then g/.m in rng Lj by A70,PARTFUN2:2;
then
A71: dom Ci = Seg len Ci & rng g /\ rng Line(G1,j) <> {}
by A62,FINSEQ_1:def 3,XBOOLE_0:def 4;
A72: now
assume j<>mi;
then j<mi or j>mi by XXREAL_0:1;
hence contradiction by A39,A52,A41,A65,A63,A67,A71;
end;
g1/.n in rng g1 by A54,PARTFUN2:2;
hence thesis by A18,A57,A62,A70,A72,XBOOLE_0:def 4;
end;
A73: width G1 in Seg width G1 by A30,FINSEQ_1:1;
deffunc F(Nat) = G1*($1,k1);
reconsider Ck1 = Col(G1,k1) as FinSequence of TOP-REAL 2;
consider h1 be FinSequence of TOP-REAL 2 such that
A74: len h1 = l1 & for n being Nat st n in dom h1 holds h1/.n=F(n)
from FINSEQ_4:sch 2;
A75: dom g1 = Seg len g1 by FINSEQ_1:def 3;
now
per cases;
suppose
A76: k=0;
reconsider c1 = Col(G1,1) as FinSequence of TOP-REAL 2;
consider x being Element of NAT such that
A77: x in dom c1 and
A78: g2/.1=c1/.x by A10,PARTFUN2:2;
reconsider lx = Line(G1,x) as FinSequence of TOP-REAL 2;
A79: 1<=x by A77,FINSEQ_3:25;
A80: len c1 = len G1 by MATRIX_0:def 8;
then x<=len G1 by A77,FINSEQ_3:25;
then consider m such that
A81: m in dom g1 and
A82: g1/.m in rng lx by A4,A6,A8,A9,A79,GOBOARD1:29;
A83: g1/.m in rng g1 by A81,PARTFUN2:2;
Seg len c1 = dom c1 by FINSEQ_1:def 3;
then
A84: x in dom G1 by A77,A80,FINSEQ_1:def 3;
A85: c1/.x = c1.x by A77,PARTFUN1:def 6;
consider y being Element of NAT such that
A86: y in dom lx and
A87: lx/.y=g1/.m by A82,PARTFUN2:2;
Seg len lx=dom lx & len lx=width G1 by FINSEQ_1:def 3,MATRIX_0:def 7;
then
A88: y =1 by A3,A76,A86,FINSEQ_1:2,TARSKI:def 1;
0<>width G1 by MATRIX_0:def 10;
then 0+1<=width G1 by NAT_1:14;
then
A89: 1 in Seg width G1 by FINSEQ_1:1;
1 in dom g2 by A5,FINSEQ_3:25;
then
A90: g2/.1 in rng g2 by PARTFUN2:2;
lx/.y = lx.y by A86,PARTFUN1:def 6;
then g1/.m=g2/.1 by A78,A89,A84,A87,A85,A88,MATRIX_0:42;
hence thesis by A83,A90,XBOOLE_0:def 4;
end;
suppose
A91: k<>0;
then
A92: 0<k;
then
A93: width G1 > 1+0 by A3,XREAL_1:8;
then
A94: width G1 in Seg width G1 by FINSEQ_1:1;
now
per cases;
suppose
mi=ma;
hence thesis by A53;
end;
suppose
A95: mi<>ma;
1<=ma1 by A46,FINSEQ_3:25;
then reconsider w=ma1-1 as Element of NAT by INT_1:5;
reconsider Lma = Line(G1,ma) as FinSequence of TOP-REAL 2;
A96: Indices G1=[:dom G1,Seg width G1:] by MATRIX_0:def 4;
A97: now
let n;
A98: l1<=mi by XREAL_1:43;
assume
A99: n in dom h1;
then
A100: 1<=n by FINSEQ_3:25;
n<=l1 by A74,A99,FINSEQ_3:25;
then
A101: n<=mi by A98,XXREAL_0:2;
mi<=len G1 by A39,FINSEQ_3:25;
then n<=len G1 by A101,XXREAL_0:2;
hence n in dom G1 by A100,FINSEQ_3:25;
end;
A102: now
let n;
assume that
A103: n in dom h1 and
A104: n+1 in dom h1;
n+1 in dom G1 by A97,A104;
then
A105: [n+1,k1] in Indices G1 by A51,A96,ZFMISC_1:87;
let i1,i2,j1,j2 be Nat;
assume that
A106: [i1,i2] in Indices G1 and
A107: [j1,j2] in Indices G1 and
A108: h1/.n=G1*(i1,i2) and
A109: h1/.(n+1)=G1*(j1,j2);
h1/.(n+1)=G1*(n+1,k1) by A74,A104;
then
A110: j1=n+1 & j2=k1 by A105,A107,A109,GOBOARD1:5;
n in dom G1 by A97,A103;
then
A111: [n,k1] in Indices G1 by A51,A96,ZFMISC_1:87;
h1/.n=G1*(n,k1) by A74,A103;
then i1=n & i2=k1 by A111,A106,A108,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.n-n+-1.|+0 by A110,ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
A112: rng h1 /\ rng g = {}
proof
set x = the Element of rng h1 /\ rng g;
assume
A113: not thesis;
then x in rng h1 by XBOOLE_0:def 4;
then consider n1 be Element of NAT such that
A114: n1 in dom h1 and
A115: x=h1/.n1 by PARTFUN2:2;
A116: n1<=l1 by A74,A114,FINSEQ_3:25;
n1 in dom G1 by A97,A114;
then
A117: [n1,k1] in Indices G1 by A51,A96,ZFMISC_1:87;
x in rng g by A113,XBOOLE_0:def 4;
then consider n2 be Element of NAT such that
A118: n2 in dom g and
A119: x=g/.n2 by PARTFUN2:2;
A120: g/.n2 in rng g by A118,PARTFUN2:2;
consider i1,i2 be Nat such that
A121: [i1,i2] in Indices G1 and
A122: g/.n2=G1*(i1,i2) by A15,A118,GOBOARD1:def 9;
reconsider L=Line(G1,i1) as FinSequence of TOP-REAL 2;
A123: i2 in Seg width G1 by A96,A121,ZFMISC_1:87;
A124: Seg len L = dom L & len L=width G1
by FINSEQ_1:def 3,MATRIX_0:def 7;
then L/.i2 = L.i2 by A123,PARTFUN1:def 6;
then g/.n2=L/.i2 by A122,A123,MATRIX_0:def 7;
then g/.n2 in rng L by A123,A124,PARTFUN2:2;
then
A125: rng g /\ rng L <> {} by A120,XBOOLE_0:def 4;
i1 in dom G1 by A96,A121,ZFMISC_1:87;
then
A126: mi<=i1 by A39,A125;
x=G1*(n1,k1) by A74,A114,A115;
then i1=n1 by A119,A121,A122,A117,GOBOARD1:5;
then mi<=mi-1 by A116,A126,XXREAL_0:2;
hence contradiction by XREAL_1:44;
end;
defpred P[Nat] means $1 in dom g1 & ma1<$1 & g1/.$1 in rng Line(G1
,ma);
A127: mi<=ma by A39,A41;
then
A128: mi<ma by A95,XXREAL_0:1;
then ex n st P[n] by A6,A9,A39,A48,A46,GOBOARD1:37;
then
A129: ex n be Nat st P[n];
consider mi1 be Nat such that
A130: P[mi1] & for n be Nat st P[n] holds mi1<=n from NAT_1:
sch 5(A129);
consider k2 be Element of NAT such that
A131: k2 in dom Lma and
A132: g1/.mi1=Lma/.k2 by A130,PARTFUN2:2;
deffunc F(Nat) = G1*(ma+$1,k2);
consider h2 be FinSequence of TOP-REAL 2 such that
A133: len h2 = l2 & for n being Nat st n in dom h2 holds h2/.n
= F(n) from FINSEQ_4:sch 2;
reconsider Ck2 = Col(G1,k2) as FinSequence of TOP-REAL 2;
dom Lma = Seg len Lma by FINSEQ_1:def 3;
then
A134: k2 in Seg width G1 by A131,MATRIX_0:def 7;
A135: now
let n;
A136: n<=n+ma by NAT_1:11;
assume
A137: n in dom h2;
then n<=l2 by A133,FINSEQ_3:25;
then
A138: ma+n<=ma+l2 by XREAL_1:7;
1<=n by A137,FINSEQ_3:25;
then 1<=n+ma by A136,XXREAL_0:2;
hence ma+n in dom G1 by A138,FINSEQ_3:25;
end;
A139: now
let n;
assume
A140: n in dom h2;
reconsider m=ma+n, k2 as Nat;
take m,k2;
ma+n in dom G1 by A135,A140;
hence [m,k2] in Indices G1 & h2/.n=G1*(m,k2) by A134,A133,A96
,A140,ZFMISC_1:87;
end;
A141: now
let n;
assume that
A142: n in dom h2 and
A143: n+1 in dom h2;
ma+(n+1) in dom G1 by A135,A143;
then
A144: [ma+n+1,k2] in Indices G1 by A134,A96,ZFMISC_1:87;
let i1,i2,j1,j2 be Nat;
assume that
A145: [i1,i2] in Indices G1 and
A146: [j1,j2] in Indices G1 and
A147: h2/.n=G1* (i1,i2) and
A148: h2/.(n+1)=G1*(j1,j2);
h2/.(n+1)=G1*(ma+(n+1),k2) by A133,A143;
then
A149: j1=ma+n+1 & j2=k2 by A144,A146,A148,GOBOARD1:5;
ma+n in dom G1 by A135,A142;
then
A150: [ma+n,k2] in Indices G1 by A134,A96,ZFMISC_1:87;
h2/.n=G1 *(ma+n,k2) by A133,A142;
then i1=ma+n & i2=k2 by A150,A145,A147,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.ma+n-(ma+n)+-1.|+0 by A149,
ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
A151: mi1<=mi1+1 by NAT_1:11;
A152: 0+1<width G1 by A3,A92,XREAL_1:6;
A153: len DelCol(G1,width G1)= len G1 by MATRIX_0:def 13;
ma1<=mi1 by A130;
then reconsider l=mi1+1-ma1 as Element of NAT by A151,INT_1:5
,XXREAL_0:2;
set f1=g1|mi1;
defpred P[Nat,Element of TOP-REAL 2] means $2=f1/.(w+$1);
A154: for n being Nat st n in Seg l ex p st P[n,p];
consider f such that
A155: len f = l & for n being Nat st n in Seg l holds P[n,f/.n
] from FINSEQ_4:sch 1(A154);
A156: w+l= mi1;
A157: dom f = Seg l by A155,FINSEQ_1:def 3;
set ff = h1^f^h2;
ma1+1<=mi1 by A130,NAT_1:13;
then ma1+1<=mi1+1 by NAT_1:13;
then
A158: 1<=l by XREAL_1:19;
A159: now
per cases;
suppose
A160: mi=1;
1<=ma1 by A75,A46,FINSEQ_1:1;
then
A161: ma1 in Seg mi1 by A130,FINSEQ_1:1;
A162: w+1=ma1;
A163: 1 in Seg l by A158,FINSEQ_1:1;
h1 = {} by A74,A160;
then ff=f^h2 by FINSEQ_1:34;
then ff/.1=f/.1 by A157,A163,FINSEQ_4:68
.= f1/.ma1 by A155,A163,A162
.= g1/.ma1 by A130,A161,FINSEQ_4:71;
hence ff/.1 in rng Line(G1,1) by A46,A160;
end;
suppose
A164: mi<>1;
1<=mi by A39,FINSEQ_3:25;
then 1<mi by A164,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A165: 1<=l1 by XREAL_1:19;
then
A166: 1 in dom h1 by A74,FINSEQ_3:25;
A167: len Line(G1,1)=width G1 by MATRIX_0:def 7;
then
A168: k1 in dom L1 by A51,FINSEQ_1:def 3;
dom Line(G1,1) = Seg width G1 by A167,FINSEQ_1:def 3;
then
A169: L1/.k1 = L1.k1 by A51,PARTFUN1:def 6;
len(h1^f)=len h1 + len f & 0<=len f by FINSEQ_1:22;
then 0+1<=len(h1^f) by A74,A165,XREAL_1:7;
then 1 in dom(h1^f) by FINSEQ_3:25;
then ff/.1=(h1^f)/.1 by FINSEQ_4:68
.=h1/.1 by A166,FINSEQ_4:68
.=G1*(1,k1) by A74,A166
.=L1/.k1 by A51,A169,MATRIX_0:def 7;
hence ff/.1 in rng Line(G1,1) by A168,PARTFUN2:2;
end;
end;
A170: for n st n in Seg l holds f1/.(w+n)=g1/.(w+n) & w+n in dom g1
proof
0+1<=ma1 by A46,FINSEQ_3:25;
then
A171: 0<=ma1-1 by XREAL_1:19;
let n such that
A172: n in Seg l;
n<=l by A172,FINSEQ_1:1;
then n+ma1<=l+ma1 by XREAL_1:7;
then
A173: n+ma1-1<=mi1 by XREAL_1:20;
1<=n by A172,FINSEQ_1:1;
then 0+1<=ma1-1+n by A171,XREAL_1:7;
then w+n in Seg mi1 by A173,FINSEQ_1:1;
hence thesis by A130,FINSEQ_4:71;
end;
A174: now
let n;
assume
A175: n in dom f;
then w+n in dom g1 by A170,A157;
then consider i,j such that
A176: [i,j] in Indices G1 & g1/.(w+n)=G1*(i,j) by A6,GOBOARD1:def 9;
take i,j;
f/.n=f1/.(w+n) by A155,A157,A175;
hence [i,j] in Indices G1 & f/.n=G1*(i,j) by A170,A157,A175,A176;
end;
A177: Seg len f=dom f by FINSEQ_1:def 3;
A178: rng f c= rng g1
proof
let x be object;
assume x in rng f;
then consider n being Element of NAT such that
A179: n in dom f and
A180: x=f/.n by PARTFUN2:2;
f/.n=f1/.(w+n) by A155,A177,A179;
then
A181: f/.n=g1/.(w+n) by A170,A155,A177,A179;
w+n in dom g1 by A170,A155,A177,A179;
hence thesis by A180,A181,PARTFUN2:2;
end;
A182: dom h2 = Seg len h2 by FINSEQ_1:def 3;
A183: now
per cases;
suppose
A184: ma=len G1;
1<=mi1 by A130,FINSEQ_3:25;
then
A185: mi1 in Seg mi1 by FINSEQ_1:1;
A186: len f in dom f by A155,A177,A158,FINSEQ_1:1;
h2 = {} by A133,A184;
then
A187: ff=h1^f by FINSEQ_1:34;
then ff/.len ff=ff/.(len h1+len f) by FINSEQ_1:22
.= f/.l by A155,A187,A186,FINSEQ_4:69
.= f1/.mi1 by A155,A157,A156,A186
.= g1/.mi1 by A130,A185,FINSEQ_4:71;
hence ff/.len ff in rng Line(G1,len G1) by A130,A184;
end;
suppose
A188: ma<>len G1;
ma<=len G1 by A41,FINSEQ_3:25;
then ma<len G1 by A188,XXREAL_0:1;
then ma+1<=len G1 by NAT_1:13;
then
A189: 1<=l2 by XREAL_1:19;
then
A190: l2 in Seg l2 by FINSEQ_1:1;
A191: len h2 in dom h2 by A133,A189,FINSEQ_3:25;
A192: len Line(G1,len G1)=width G1 by MATRIX_0:def 7;
then
A193: k2 in dom Ll by A134,FINSEQ_1:def 3;
k2 in dom Ll by A134,A192,FINSEQ_1:def 3;
then
A194: Ll/.k2 = Ll.k2 by PARTFUN1:def 6;
ff/.len ff=ff/.(len(h1^f)+len h2) by FINSEQ_1:22
.=h2/.l2 by A133,A191,FINSEQ_4:69
.=G1*(ma+l2,k2) by A133,A182,A190
.=Ll/.k2 by A134,A194,MATRIX_0:def 7;
hence ff/.len ff in rng Line(G1,len G1) by A193,PARTFUN2:2;
end;
end;
A195: 0+1<=len f+(len h1+len h2) by A155,A158,XREAL_1:7;
A196: rng ff = rng(h1^f) \/ rng h2 by FINSEQ_1:31
.= rng h1 \/ rng f \/ rng h2 by FINSEQ_1:31;
A197: for k st k in Seg width G1 & rng f /\ rng Col(G1,k)={} holds
rng ff /\ rng Col(G1,k)={}
proof
A198: len Col(G1,k2)=len G1 by MATRIX_0:def 8;
A199: len Col(G1,k1)=len G1 by MATRIX_0:def 8;
A200: w+1=ma1;
let k;
assume that
A201: k in Seg width G1 and
A202: rng f /\ rng Col(G1,k)={};
set gg=Col(G1,k);
assume
A203: rng ff /\ rng gg <> {};
set x = the Element of rng ff /\ rng gg;
rng ff = rng f \/ (rng h1 \/ rng h2) by A196,XBOOLE_1:4;
then
A204: rng ff /\ rng gg = {} \/ (rng h1 \/ rng h2) /\ rng gg by A202,
XBOOLE_1:23
.= rng h1 /\ rng gg \/ rng h2 /\ rng gg by XBOOLE_1:23;
now
per cases by A203,A204,XBOOLE_0:def 3;
suppose
A205: x in rng h1 /\ rng gg;
then x in rng h1 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A206: i in dom h1 and
A207: x=h1/.i by PARTFUN2:2;
A208: x=G1*(i,k1) by A74,A206,A207;
reconsider y=x as Point of TOP-REAL 2 by A207;
A209: Lmi/.k1 = Lmi.k1 by A49,PARTFUN1:def 6;
A210: x in rng gg by A205,XBOOLE_0:def 4;
A211: dom Col(G1,k1) = Seg len G1 by A199,FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then
A212: Ck1/.mi = Ck1.mi by A39,PARTFUN1:def 6;
A213: i in dom Ck1 by A97,A206,A211;
Ck1/.i = Ck1.i by A97,A206,A211,PARTFUN1:def 6;
then y=Ck1/.i by A208,A211,A213,MATRIX_0:def 8;
then y in rng Ck1 by A213,PARTFUN2:2;
then
A214: k1 =k by A51,A201,A210,GOBOARD1:4;
A215: 1 in Seg l by A158,FINSEQ_1:1;
then f/.1=f1/.ma1 & f1/.ma1=g1/.(w+1) by A170,A155,A200;
then f/.1= Ck1/.mi by A39,A50,A51,A209,A212,MATRIX_0:42;
then
A216: f/.1 in rng Col(G1,k) by A39,A211,A214,PARTFUN2:2;
f/.1 in rng f by A157,A215,PARTFUN2:2;
hence contradiction by A202,A216,XBOOLE_0:def 4;
end;
suppose
A217: x in rng h2 /\ rng gg;
then x in rng h2 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A218: i in dom h2 and
A219: x=h2/.i by PARTFUN2:2;
A220: x=G1*(ma+i,k2) by A133,A218,A219;
reconsider y=x as Point of TOP-REAL 2 by A219;
A221: Lma/.k2 = Lma.k2 by A131,PARTFUN1:def 6;
A222: x in rng gg by A217,XBOOLE_0:def 4;
A223: dom Col(G1,k2) = Seg len G1 by A198,FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then
A224: Ck2/.ma = Ck2.ma by A41,PARTFUN1:def 6;
A225: ma+i in dom Ck2 by A135,A218,A223;
Ck2/.(ma+i) = Ck2.(ma+i) by A135,A218,A223,PARTFUN1:def 6;
then y=Ck2/.(ma+i) by A220,A223,A225,MATRIX_0:def 8;
then y in rng Ck2 by A225,PARTFUN2:2;
then
A226: k2=k by A134,A201,A222,GOBOARD1:4;
A227: l in Seg l by A158,FINSEQ_1:1;
then f/.l=f1/.(w+l) & f1/.(w+l)=g1/.(w+l) by A170,A155;
then f/.l=Ck2/.ma by A41,A132,A134,A221,A224,MATRIX_0:42;
then
A228: f/.l in rng Col(G1,k) by A41,A223,A226,PARTFUN2:2;
f/.l in rng f by A157,A227,PARTFUN2:2;
hence contradiction by A202,A228,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
rng h2 /\ rng g = {}
proof
set x = the Element of rng h2 /\ rng g;
assume
A229: not thesis;
then x in rng h2 by XBOOLE_0:def 4;
then consider n1 be Element of NAT such that
A230: n1 in dom h2 and
A231: x=h2/.n1 by PARTFUN2:2;
A232: 1<=n1 by A230,FINSEQ_3:25;
ma+n1 in dom G1 by A135,A230;
then
A233: [ma+n1,k2] in Indices G1 by A134,A96,ZFMISC_1:87;
x in rng g by A229,XBOOLE_0:def 4;
then consider n2 be Element of NAT such that
A234: n2 in dom g and
A235: x=g/.n2 by PARTFUN2:2;
consider i1,i2 be Nat such that
A236: [i1,i2] in Indices G1 and
A237: g/.n2=G1*(i1,i2) by A15,A234,GOBOARD1:def 9;
reconsider L=Line(G1,i1) as FinSequence of TOP-REAL 2;
A238: i2 in Seg width G1 by A96,A236,ZFMISC_1:87;
A239: Seg len L = dom L & len L=width G1 by FINSEQ_1:def 3
,MATRIX_0:def 7;
then L/.i2 = L.i2 by A238,PARTFUN1:def 6;
then g/.n2=L/.i2 by A237,A238,MATRIX_0:def 7;
then
A240: g/.n2 in rng L by A238,A239,PARTFUN2:2;
g/.n2 in rng g by A234,PARTFUN2:2;
then
A241: rng g /\ rng L <> {} by A240,XBOOLE_0:def 4;
A242: i1 in dom G1 by A96,A236,ZFMISC_1:87;
x=G1*(ma+n1,k2) by A133,A230,A231;
then i1=ma+n1 by A235,A236,A237,A233,GOBOARD1:5;
then n1<=0 by A41,A242,A241,XREAL_1:29;
hence contradiction by A232;
end;
then rng ff /\ rng g = ((rng h1 \/ rng f) /\ rng g) \/ {} by A196,
XBOOLE_1:23
.= {} \/ rng f /\ rng g by A112,XBOOLE_1:23
.= rng f /\ rng g;
then
A243: rng ff /\ rng g c= rng g1 /\ rng g2 by A18,A178,XBOOLE_1:27;
A244: len DelCol(G1,1)=len G1 by MATRIX_0:def 13;
then
A245: dom DelCol(G1,1) = Seg len G1 by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
A246: now
let n;
assume that
A247: n in dom f and
A248: n+1 in dom f;
f/.n=f1/.(w+n) by A155,A157,A247;
then
A249: f/.n=g1 /.(w+n) by A170,A157,A247;
f/.(n+1)=f1/.(w+(n+1)) by A155,A157,A248;
then
A250: w+n+1 in dom g1 & f/.(n+1)=g1/.(w+n+1) by A170,A157,A248;
let i1,i2,j1,j2 be Nat;
assume
A251: [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & f/.n=
G1*(i1,i2) & f/. (n+1)=G1*(j1,j2);
w+n in dom g1 by A170,A157,A247;
hence |.i1-j1.|+|.i2-j2.|=1 by A6,A249,A250,A251,GOBOARD1:def 9;
end;
set hf=h1^f;
A252: len ff=len(h1^f)+len h2 by FINSEQ_1:22
.=len h1+len f+len h2 by FINSEQ_1:22;
A253: now
let i1,i2,j1,j2 be Nat;
assume that
A254: [ i1,i2] in Indices G1 and
A255: [j1,j2] in Indices G1 and
A256: hf/.len hf=G1*(i1,i2) and
A257: h2/.1=G1*(j1,j2) and
len hf in dom hf and
A258: 1 in dom h2;
ma+1 in dom G1 by A135,A258;
then
A259: [ma+1,k2] in Indices G1 by A134,A96,ZFMISC_1:87;
A260: [ma,k2] in Indices G1 by A41,A134,A96,ZFMISC_1:87;
A261: Lma/.k2 = Lma.k2 by A131,PARTFUN1:def 6;
A262: len f in dom f by A155,A157,A158,FINSEQ_1:1;
hf/.len hf=hf/.(len h1+len f) by FINSEQ_1:22
.= f/.len f by A262,FINSEQ_4:69
.= f1/.(w+l) by A155,A157,A262
.= g1/.mi1 by A170,A155,A157,A262
.= G1*(ma,k2) by A132,A134,A261,MATRIX_0:def 7;
then
A263: i1=ma & i2=k2 by A254,A256,A260,GOBOARD1:5;
h2/.1=G1*(ma+1,k2) by A133,A258;
then j1=ma+1 & j2=k2 by A255,A257,A259,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|=|.ma-(ma+1).|+0 by A263,ABSVALUE:2
.=|.-(ma+1 -ma).|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
now
A264: [mi,k1] in Indices G1 by A39,A51,A96,ZFMISC_1:87;
A265: Lmi/.k1 = Lmi.k1 by A49,PARTFUN1:def 6;
let i1,i2,j1,j2 be Nat;
assume that
A266: [i1,i2] in Indices G1 and
A267: [j1,j2] in Indices G1 and
A268: h1/.len h1=G1*(i1,i2) and
A269: f/.1=G1*(j1,j2) and
A270: len h1 in dom h1 and
A271: 1 in dom f;
l1 in dom G1 by A74,A97,A270;
then
A272: [l1,k1] in Indices G1 by A51,A96,ZFMISC_1:87;
A273: w+1=ma1;
then f/.1=f1/.ma1 by A155,A157,A271;
then f/.1=g1/.ma1 by A170,A157,A271,A273
.= G1*(mi,k1) by A50,A51,A265,MATRIX_0:def 7;
then
A274: j1=mi & j2=k1 by A267,A269,A264,GOBOARD1:5;
h1/.len h1=G1*(l1,k1) by A74,A270;
then i1=l1 & i2=k1 by A266,A268,A272,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.mi-1-mi.|+0 by A274,ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
then for n st n in dom(h1^f) & n+1 in dom(h1^f) for i1,i2,j1,j2
be Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & (h1^f)/.n=
G1*(i1,i2) & (h1^f)/.(n+1)=G1*(j1,j2) holds |.i1-j1.|+|.i2-j2.|=1 by A102
,A246,GOBOARD1:24;
then
A275: for n st n in dom ff & n+1 in dom ff for m,k,i,j st [m,k] in
Indices G1 & [i,j] in Indices G1 & ff/.n=G1*(m,k) & ff/.(n+1)=G1*(i,j) holds
|.m-i.|+|.k-j.|=1 by A141,A253,GOBOARD1:24;
now
let n;
assume
A276: n in dom h1;
reconsider k1 as Nat;
take i=n,k1;
n in dom G1 by A97,A276;
hence
[i,k1] in Indices G1 & h1/.n=G1*(i,k1) by A74,A51,A96,A276,
ZFMISC_1:87;
end;
then for n st n in dom(h1^f) ex i,j st [i,j] in Indices G1 & (h1^
f)/.n=G1*(i,j) by A174,GOBOARD1:23;
then for n st n in dom ff ex i,j st [i,j] in Indices G1 & ff/.n=
G1*(i,j) by A139,GOBOARD1:23;
then
A277: ff is_sequence_on G1 by A275,GOBOARD1:def 9;
A278: Seg len ff=dom ff by FINSEQ_1:def 3;
then
A279: len ff in dom ff by A252,A195,FINSEQ_1:1;
A280: 1 in dom ff by A252,A195,A278,FINSEQ_1:1;
thus thesis
proof
per cases;
suppose
A281: rng f /\ rng Col(G1,1)={};
set D = DelCol(G1,1);
A282: 1 in Seg width G1 by A152,FINSEQ_1:1;
A283: D is not empty-yielding by A152,A282,MATRIX_0:65;
rng ff /\ rng Col(G1,1)={} by A31,A197,A281;
then
A284: rng ff misses rng Col(G1,1) by XBOOLE_0:def 7;
then
A285: ff is_sequence_on D & ff/.1 in rng Line(D,1) by A31,A26,A277
,A159,A152,A280,GOBOARD1:25,MATRIX_0:75;
A286: ff/.len ff in rng Line(D,len D) by A31,A27,A183,A152,A244,A279
,A284,MATRIX_0:75;
defpred P[Nat] means $1 in dom g & g/.$1 in rng Col(G1,1);
A287: ex m be Nat st P[m]
proof
take 1;
thus thesis by A10,A13,A32,FINSEQ_3:25,FINSEQ_4:92;
end;
A288: for m be Nat st P[m] holds m<=len g by FINSEQ_3:25;
consider m be Nat such that
A289: P [m] & for k be Nat st P[k] holds k<=m from NAT_1:
sch 6(A288,A287);
reconsider m as Nat;
reconsider p=g/.m as Point of TOP-REAL 2;
A290: now
assume
A291: m>=len g;
m<=len g by A289,FINSEQ_3:25;
then p in rng Col(G1,width G1) by A28,A291,XXREAL_0:1;
then 1=k+1 by A3,A31,A73,A289,GOBOARD1:4;
hence contradiction by A91;
end;
then reconsider ll = len g-m as Element of NAT by INT_1:5;
deffunc F(Nat) = g/.(m+$1);
consider t be FinSequence of TOP-REAL 2 such that
A292: len t = ll & for n being Nat st n in dom t holds t/.
n = F(n) from FINSEQ_4:sch 2;
A293: dom t = Seg ll by A292,FINSEQ_1:def 3;
A294: rng t c= rng g
proof
let y be object;
assume y in rng t;
then consider x being Element of NAT such that
A295: x in dom t and
A296: t/.x=y by PARTFUN2:2;
x<=ll by A293,A295,FINSEQ_1:1;
then
A297: m+x<=m+ll by XREAL_1:7;
A298: x<=x+m by NAT_1:11;
1<=x by A293,A295,FINSEQ_1:1;
then 1<=x+m by A298,XXREAL_0:2;
then m+x in dom g by A297,FINSEQ_3:25;
then g/.(m+x) in rng g by PARTFUN2:2;
hence thesis by A292,A295,A296;
end;
A299: for n st n in dom t holds m+n in dom g
proof
let n;
A300: n<=n+m by NAT_1:11;
assume
A301: n in dom t;
then n<=ll by A293,FINSEQ_1:1;
then
A302: m+n<=m+ll by XREAL_1:7;
1<=n by A293,A301,FINSEQ_1:1;
then 1<=n+m by A300,XXREAL_0:2;
hence thesis by A302,FINSEQ_3:25;
end;
A303: Seg len t = dom t by FINSEQ_1:def 3;
reconsider t as FinSequence of TOP-REAL 2;
A304: width D = k by A3,A31,MATRIX_0:63;
A305: Indices D = [:dom D,Seg width D:] by MATRIX_0:def 4;
A306: now
let n;
assume
A307: n in dom t;
then m+n in dom g by A299;
then consider i1,i2 be Nat such that
A308: [i1,i2] in Indices G1 and
A309: g/.(m+n)=G1*(i1,i2) by A15,GOBOARD1:def 9;
A310: i2 in Seg width G1 by A96,A308,ZFMISC_1:87;
then
A311: 1<=i2 by FINSEQ_1:1;
then reconsider l=i2-1 as Element of NAT by INT_1:5;
reconsider Ci2 = Col(G1,i2) as FinSequence of TOP-REAL 2;
A312: i1 in dom G1 by A96,A308,ZFMISC_1:87;
len Ci2 = len G1 by MATRIX_0:def 8;
then
A313: dom Ci2 = Seg len G1 by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then Ci2/.i1 = Ci2.i1 by A312,PARTFUN1:def 6;
then Ci2/.i1 = G1*(i1,i2) by A312,MATRIX_0:def 8;
then
A314: g/.(m+n) in rng Col(G1,i2) by A309,A312,A313,PARTFUN2:2;
now
1<=n by A293,A307,FINSEQ_1:1;
then
A315: m+1<=m+n by XREAL_1:7;
assume i2=1;
then m+n<=m by A289,A299,A307,A314;
then m+1<=m by A315,XXREAL_0:2;
then 1<=m-m by XREAL_1:19;
then 1<=0;
hence contradiction;
end;
then 1<i2 by A311,XXREAL_0:1;
then 1+1<=i2 by NAT_1:13;
then
A316: 1<=l by XREAL_1:19;
reconsider i1,l as Nat;
take i1;
take l;
A317: t/.n=g/.(m+n) by A292,A307;
i2<=width G1 by A310,FINSEQ_1:1;
then
A318: l<=width D by A3,A304,XREAL_1:20;
then l in Seg width D by A316,FINSEQ_1:1;
hence [i1,l] in Indices D by A245,A305,A312,ZFMISC_1:87;
l+1=i2;
hence
t/.n = D*(i1,l) by A3,A31,A304,A309,A312,A317,A316,A318,
MATRIX_0:70;
end;
0<width D by A283,MATRIX_0:def 10,NAT_1:3;
then
A319: 0+1<=width D by NAT_1:13;
then
A320: Col(D,1)=Col(G1,1+1) & 1+1 in Seg width G1 by A3,A31,A304,
MATRIX_0:68;
m+1<=len g by A290,NAT_1:13;
then
A321: 1<=len t by A292,XREAL_1:19;
then t/.1 = g/.(m+1) by A292,A303,FINSEQ_1:1;
then
A322: t/.1 in rng Col(D,1) by A32,A15,A28,A31,A289,A320,
GOBOARD1:32;
now
let n;
assume that
A323: n in dom t and
A324: n+1 in dom t;
let i1,i2,j1,j2 be Nat;
assume that
A325: [ i1,i2] in Indices D and
A326: [j1,j2] in Indices D and
A327: t/.n=D*(i1,i2) and
A328: t/.(n+1)=D*(j1,j2);
A329: i1 in dom D by A305,A325,ZFMISC_1:87;
i2 in Seg k by A304,A305,A325,ZFMISC_1:87;
then
A330: 1<=i2 & i2<=k by FINSEQ_1:1;
then i2+1 in Seg width G1 by A3,A31,A245,A329,MATRIX_0:70;
then
A331: [i1,i2+1] in Indices G1 by A96,A245,A329,ZFMISC_1:87;
t/.n=g/.(m+n) by A292,A323;
then
A332: g/.(m+n)=G1*(i1,i2+1) by A3,A31,A245,A327,A329,A330,
MATRIX_0:70;
m+(n+1)=m+n+1;
then
A333: m+n+1 in dom g by A299,A324;
A334: j1 in dom D by A305,A326,ZFMISC_1:87;
j2 in Seg k by A304,A305,A326,ZFMISC_1:87;
then
A335: 1<=j2 & j2<=k by FINSEQ_1:1;
then j2+1 in Seg width G1 by A3,A31,A245,A329,MATRIX_0:70;
then
A336: [j1,j2+1] in Indices G1 by A96,A245,A334,ZFMISC_1:87;
t/.(n+1)=g/.(m+(n+1)) by A292,A324;
then
A337: g/.(m+n+1)=G1* (j1,j2+1) by A3,A31,A245,A328,A334,A335,
MATRIX_0:70;
m+n in dom g by A299,A323;
hence 1= |.i1-j1.|+|.i2+1 -(j2+1).| by A15,A332,A337,A331
,A336,A333,GOBOARD1:def 9
.=|.i1-j1.|+|.i2-j2.|;
end;
then
A338: t is_sequence_on D by A306,GOBOARD1:def 9;
set x = the Element of rng ff /\ rng t;
A339: rng ff /\ rng t c= rng ff /\ rng g by A294,XBOOLE_1:26;
len t in Seg ll by A292,A321,FINSEQ_1:1;
then t/.len t = g/.(m+ll) by A292,A303
.= g/.len g;
then t/.len t in rng Col(D,width D) by A3,A28,A31,A304,A319
,MATRIX_0:68;
then rng ff /\ rng t <> {} by A2,A92,A252,A195,A304,A321,A322
,A338,A285,A286,A283;
then x in rng ff /\ rng g by A339;
hence thesis by A243;
end;
suppose
A340: rng f /\ rng Col(G1,1) <> {};
set D = DelCol(G1,width G1);
A341: D is not empty-yielding by A93,A94,MATRIX_0:65;
A342: 0+1<k+1 by A92,XREAL_1:6;
now
per cases;
suppose
rng f /\ rng Col(G1,width G1) = {};
then rng ff /\ rng Col(G1,width G1) = {} by A73,A197;
then
A343: rng ff misses rng Col(G1,width G1) by XBOOLE_0:def 7;
then
A344: ff is_sequence_on D by A73,A277,A152,GOBOARD1:25;
consider t be FinSequence of TOP-REAL 2 such that
A345: t/.1 in rng Col(D,1) & t/.len t in rng Col(D,
width D) & 1<=len t & t is_sequence_on D and
A346: rng t c= rng g by A3,A32,A15,A14,A28,A342,GOBOARD1:35;
set x = the Element of rng ff /\ rng t;
A347: rng ff /\ rng t c= rng ff /\ rng g by A346,XBOOLE_1:26;
A348: width D = k by A3,A73,MATRIX_0:63;
ff/.1 in rng Line(D,1) & ff/.len ff in rng Line(D,
len D) by A73,A26,A27,A159,A183,A152,A153,A280,A279,A343,MATRIX_0:75;
then rng ff /\ rng t <> {} by A2,A92,A252,A195,A345,A348
,A344,A341;
then x in rng ff /\ rng g by A347;
hence thesis by A243;
end;
suppose
A349: rng f /\ rng Col(G1,width G1) <> {};
A350: f is_sequence_on G1 by A174,A246,GOBOARD1:def 9;
then consider t be FinSequence of TOP-REAL 2 such that
A351: rng t c= rng f and
A352: t/.1 in rng Col(G1,1) & t/.len t in rng Col(G1,
width G1) & 1<=len t & t is_sequence_on G1 by A340,A349,GOBOARD1:36;
consider tt be FinSequence of TOP-REAL 2 such that
A353: tt/.1 in rng Col(D,1) & tt/.len tt in rng Col(D,
width D) & 1<=len tt & tt is_sequence_on D and
A354: rng tt c= rng t by A3,A342,A352,GOBOARD1:35;
A355: Seg len Lma = dom Lma & len Lma=width G1 by FINSEQ_1:def 3
,MATRIX_0:def 7;
reconsider lg=len g-1 as Element of NAT by A32,INT_1:5;
defpred P[Nat] means $1 in dom g & g/.$1 in rng Line(G1,mi
);
defpred R[Nat] means $1 in dom g & g/.$1 in rng Line(G1,ma
);
A356: lg<=len g by XREAL_1:43;
A357: now
set x = the Element of rng g /\ rng Line(G1,mi);
x in rng g by A39,XBOOLE_0:def 4;
then consider n being Element of NAT such that
A358: n in dom g & x=g/.n by PARTFUN2:2;
reconsider n as Nat;
take n;
thus P[n] by A39,A358,XBOOLE_0:def 4;
end;
consider pf be Nat such that
A359: P [pf] & for n be Nat st P[n] holds pf<=n from
NAT_1:sch 5(A357);
defpred PP[Nat] means
$1 in dom f implies for m
st m in dom G1 & f/.$1 in rng Line(G1,m) holds mi<=m;
reconsider C = Col(G1,width G1), Li= Line(G1,mi), La= Line
(G1,ma) as FinSequence of TOP-REAL 2;
A360: lg+ 1=len g;
A361: now
set x = the Element of rng g /\ rng Line(G1,ma);
x in rng g by A41,XBOOLE_0:def 4;
then consider n being Element of NAT such that
A362: n in dom g & x=g/.n by PARTFUN2:2;
reconsider n as Nat;
take n;
thus R[n] by A41,A362,XBOOLE_0:def 4;
end;
consider pl be Nat such that
A363: R [pl] & for n be Nat st R[n] holds pl<=n from
NAT_1:sch 5(A361);
reconsider pf,pl as Nat;
A364: 1<=pf by A359,FINSEQ_3:25;
consider K2 be Element of NAT such that
A365: K2 in dom Lma and
A366: g/.pl=Lma/.K2 by A363,PARTFUN2:2;
reconsider CK2 = Col(G1,K2) as FinSequence of TOP-REAL 2;
consider K1 be Element of NAT such that
A367: K1 in dom Li and
A368: g/.pf=Li/.K1 by A359,PARTFUN2:2;
reconsider CK1 = Col(G1,K1) as FinSequence of TOP-REAL 2;
deffunc F(Nat) = G1*($1,K1);
consider h1 be FinSequence of TOP-REAL 2 such that
A369: len h1 = l1 & for n being Nat st n in dom h1
holds h1/.n=F(n) from FINSEQ_4:sch 2;
A370: for k st PP[k] holds PP[k+1]
proof
let k such that
A371: PP[k];
assume
A372: k+1 in dom f;
let m such that
A373: m in dom G1 & f/.(k+1) in rng Line(G1,m);
now
per cases;
suppose
A374: k=0;
w+1=ma1 & 1 in Seg l by A158,FINSEQ_1:1;
then f/.1=f1/.ma1 & f1/.ma1=g1/.ma1 by A170,A155;
then f/.(k+1) in rng Li by A49,A50,A374,PARTFUN2:2;
hence thesis by A39,A373,GOBOARD1:3;
end;
suppose
k<>0;
then 0<k;
then
A375: 0+1<=k by NAT_1:13;
k+1<=len f by A372,FINSEQ_3:25;
then
A376: k<=len f by NAT_1:13;
then
A377: k in dom f by A375,FINSEQ_3:25;
then consider i1,i2 be Nat such that
A378: [i1,i2] in Indices G1 and
A379: f/.k=G1*(i1,i2) by A174;
A380: i2 in Seg width G1 by A96,A378,ZFMISC_1:87;
consider j1,j2 be Nat such that
A381: [ j1,j2] in Indices G1 and
A382: f/.(k+1)=G1*(j1,j2) by A174,A372;
reconsider Lj1 = Line(G1,j1) as FinSequence of
TOP-REAL 2;
A383: j2 in Seg width G1 by A96,A381,ZFMISC_1:87;
A384: Seg len Lj1 = dom Lj1 & len Lj1=width G1 by
FINSEQ_1:def 3,MATRIX_0:def 7;
then Lj1/.j2 = Lj1.j2 by A383,PARTFUN1:def 6;
then f/.(k+1)=Lj1/.j2 by A382,A383,MATRIX_0:def 7;
then
A385: f/.(k+1) in rng Lj1 by A383,A384,PARTFUN2:2;
A386: j1 in dom G1 by A96,A381,ZFMISC_1:87;
reconsider Li1 = Line(G1,i1) as FinSequence of
TOP-REAL 2;
A387: i1 in dom G1 by A96,A378,ZFMISC_1:87;
A388: Seg len Li1 = dom Li1 & len Li1=width G1 by
FINSEQ_1:def 3,MATRIX_0:def 7;
then
A389: Li1/.i2 = Li1.i2 by A380,PARTFUN1:def 6;
then f/.k=Li1/.i2 by A379,A380,MATRIX_0:def 7;
then
A390: f/.k in rng Li1 by A380,A388,PARTFUN2:2;
then
A391: mi<=i1 by A371,A375,A376,A387,FINSEQ_3:25;
now
per cases by A391,XXREAL_0:1;
suppose
A392: mi=i1;
g1/.(w+k) = f1/.(w+k) by A170,A157,A377
.= f/.k by A155,A157,A377
.= Li1/.i2 by A379,A380,A389,MATRIX_0:def 7;
then g1/.(w+k) in rng Line(G1,mi) by A380,A388
,A392,PARTFUN2:2;
then
A393: w+k<=ma1 by A46,A170,A157,A377;
w+1<=w+k by A375,XREAL_1:7;
then w+k=ma1 by A393,XXREAL_0:1;
then
A394: ma1+1=w+(k+1);
mi+1<=ma by A128,NAT_1:13;
then
A395: mi+1<=len G1 by A48,XXREAL_0:2;
1<=mi+1 by A42,NAT_1:13;
then
A396: mi+1 in dom G1 by A395,FINSEQ_3:25;
f /.(k+1)=f1/.(w+(k+1)) & f1/.(w+(k+1))=g1
/.(w+(k+1)) by A170,A155,A157,A372;
then f/.(k+1) in rng Line(G1,mi+1) by A4,A6,A9
,A39,A46,A394,A396,GOBOARD1:28;
then m=mi+1 by A373,A396,GOBOARD1:3;
hence thesis by NAT_1:11;
end;
suppose
A397: mi<i1;
now
per cases by A350,A372,A377,A387,A390,
GOBOARD1:27;
suppose
f/.(k+1) in rng Line(G1,i1);
hence thesis by A373,A387,A397,GOBOARD1:3;
end;
suppose
for l be Nat st f/.(k+1
) in rng Line(G1,l) & l in dom G1 holds |.i1-l.|=1;
then
A398: |.i1-j1.|=1 by A386,A385;
now
per cases by A398,SEQM_3:41;
suppose
A399: j1<i1 & i1=j1+1;
then mi<=i1-1 by A397,NAT_1:13;
hence thesis by A373,A386,A385,A399,
GOBOARD1:3;
end;
suppose
i1<j1 & j1=i1+1;
then mi<j1 by A397,XXREAL_0:2;
hence thesis by A373,A386,A385,GOBOARD1:3
;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A400: Seg len Li = dom Li & len Li=width G1 by FINSEQ_1:def 3
,MATRIX_0:def 7;
A401: now
let n;
A402: l1<=mi by XREAL_1:43;
assume
A403: n in dom h1;
then
A404: 1<=n by FINSEQ_3:25;
n<=l1 by A369,A403,FINSEQ_3:25;
then
A405: n<=mi by A402,XXREAL_0:2;
mi<= len G1 by A39,FINSEQ_3:25;
then n<=len G1 by A405,XXREAL_0:2;
hence n in dom G1 by A404,FINSEQ_3:25;
end;
A406: now
let n;
assume
A407: n in dom h1;
reconsider i=n,K1 as Nat;
take i,K1;
n in dom G1 by A401,A407;
hence
[i,K1] in Indices G1 & h1/.n=G1*(i,K1) by A96,A367,A400
,A369,A407,ZFMISC_1:87;
end;
A408: now
let n;
assume that
A409: n in dom h1 and
A410: n+1 in dom h1;
n+1 in dom G1 by A401,A410;
then
A411: [n+1,K1 ] in Indices G1 by A96,A367,A400,ZFMISC_1:87;
let i1,i2,j1,j2 be Nat;
assume that
A412: [i1,i2] in Indices G1 and
A413: [j1,j2] in Indices G1 and
A414: h1/.n=G1*(i1,i2) and
A415: h1/.(n+1)=G1*(j1,j2);
h1/.(n+1)=G1*(n+1,K1) by A369,A410;
then
A416: j1=n+1 & j2=K1 by A411,A413,A415,GOBOARD1:5;
n in dom G1 by A401,A409;
then
A417: [n,K1] in Indices G1 by A96,A367,A400,ZFMISC_1:87;
h1/.n=G1*(n,K1) by A369,A409;
then i1=n & i2=K1 by A417,A412,A414,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.n-n+-1.|+0 by A416,
ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
A418: pf<=len g by A359,FINSEQ_3:25;
A419: Lma/.K2 = Lma.K2 by A365,PARTFUN1:def 6;
then
A420: g/.pl=G1*(ma, K2) by A365,A366,A355,MATRIX_0:def 7;
deffunc F(Nat) = G1*(ma+$1,K2);
consider h2 be FinSequence of TOP-REAL 2 such that
A421: len h2=l2 & for n being Nat st n in dom h2 holds
h2/.n=F(n) from FINSEQ_4:sch 2;
A422: PP[0] by FINSEQ_3:25;
A423: for n holds PP[n] from NAT_1:sch 2(A422,A370);
A424: rng h1 /\ rng tt = {}
proof
set x = the Element of rng h1 /\ rng tt;
assume
A425: not thesis;
then x in rng h1 by XBOOLE_0:def 4;
then consider i2 be Element of NAT such that
A426: i2 in dom h1 and
A427: h1/.i2=x by PARTFUN2:2;
Seg len h1 = dom h1 by FINSEQ_1:def 3;
then
A428: l1<mi & i2<=l1 by A369,A426,FINSEQ_1:1,XREAL_1:44;
i2 in dom G1 by A401,A426;
then
A429: [i2,K1] in Indices G1 by A96,A367,A400,ZFMISC_1:87;
x in rng tt by A425,XBOOLE_0:def 4;
then x in rng t by A354;
then consider i1 be Element of NAT such that
A430: i1 in dom f and
A431: f/.i1=x by A351,PARTFUN2:2;
consider n1,n2 be Nat such that
A432: [n1,n2] in Indices G1 and
A433: f/.i1=G1*(n1,n2) by A174,A430;
reconsider Ln1 = Line(G1,n1) as FinSequence of TOP-REAL
2;
A434: n2 in Seg width G1 by A96,A432,ZFMISC_1:87;
A435: Seg len Ln1 = dom Ln1 & len Ln1=width G1 by
FINSEQ_1:def 3,MATRIX_0:def 7;
then Ln1/.n2 = Ln1.n2 by A434,PARTFUN1:def 6;
then f/.i1=Ln1/.n2 by A433,A434,MATRIX_0:def 7;
then
A436: f/.i1 in rng Ln1 by A434,A435,PARTFUN2:2;
n1 in dom G1 by A96,A432,ZFMISC_1:87;
then
A437: mi<=n1 by A423,A430,A436;
x=G1*(i2,K1) by A369,A426,A427;
then i2=n1 by A431,A432,A433,A429,GOBOARD1:5;
hence contradiction by A437,A428,XXREAL_0:2;
end;
defpred PP[Nat] means
$1 in dom f implies for m
st m in dom G1 & f/.$1 in rng Line(G1,m) holds m<=ma;
A438: for k st PP[k] holds PP[k+1]
proof
let k such that
A439: PP[k];
assume
A440: k+1 in dom f;
let m such that
A441: m in dom G1 & f/.(k+1) in rng Line(G1,m);
now
per cases;
suppose
A442: k=0;
1 in Seg l by A158,FINSEQ_1:1;
then f/.1=f1/.(w+1) & f1/.(w+1)=g1/.(w+1) by A170
,A155;
then f/.(k+1) in rng Li by A49,A50,A442,PARTFUN2:2;
hence thesis by A39,A127,A441,GOBOARD1:3;
end;
suppose
A443: k<>0;
A444: k+1<= len f by A177,A440,FINSEQ_1:1;
then
A445: k<=len f by NAT_1:13;
consider j1,j2 be Nat such that
A446: [ j1,j2] in Indices G1 and
A447: f/.(k+1)=G1*(j1,j2) by A174,A440;
reconsider Lj1 = Line(G1,j1) as FinSequence of
TOP-REAL 2;
A448: j2 in Seg width G1 by A96,A446,ZFMISC_1:87;
A449: Seg len Lj1 = dom Lj1 & len Lj1=width G1 by
FINSEQ_1:def 3,MATRIX_0:def 7;
then Lj1/.j2 = Lj1.j2 by A448,PARTFUN1:def 6;
then f/.(k+1)=Lj1/.j2 by A447,A448,MATRIX_0:def 7;
then
A450: f/.(k+1) in rng Lj1 by A448,A449,PARTFUN2:2;
A451: j1 in dom G1 by A96,A446,ZFMISC_1:87;
then
A452: j1=m by A441,A450,GOBOARD1:3;
0<k by A443;
then
A453: 0+1<=k by NAT_1:13;
then
A454: k in dom f by A445,FINSEQ_3:25;
then consider i1,i2 be Nat such that
A455: [i1,i2] in Indices G1 and
A456: f/.k=G1*(i1,i2) by A174;
reconsider Li1 = Line(G1,i1) as FinSequence of
TOP-REAL 2;
A457: i2 in Seg width G1 by A96,A455,ZFMISC_1:87;
A458: Seg len Li1 = dom Li1 & len Li1=width G1 by
FINSEQ_1:def 3,MATRIX_0:def 7;
then Li1/.i2 = Li1.i2 by A457,PARTFUN1:def 6;
then f/.k=Li1/.i2 by A456,A457,MATRIX_0:def 7;
then
A459: f/.k in rng Li1 by A457,A458,PARTFUN2:2;
A460: i1 in dom G1 by A96,A455,ZFMISC_1:87;
then
A461: i1<=ma by A439,A453,A445,A459,FINSEQ_3:25;
now
per cases by A461,XXREAL_0:1;
case
A462: ma=i1;
A463: w+1<=w+k by A453,XREAL_1:7;
A464: f /.k=f1/.(w+k) & f1/.(w+k)=g1/.(w+k) by A170
,A155,A157,A454;
then ma1 <> w+k by A39,A41,A46,A95,A459,A462,
GOBOARD1:3;
then ma1<w+k by A463,XXREAL_0:1;
then
A465: mi1<=w+k by A130,A170,A157,A454,A459,A462,A464;
w+k<=mi1 by A155,A156,A445,XREAL_1:7;
then w+k=mi1 by A465,XXREAL_0:1;
hence contradiction by A155,A444,NAT_1:13;
end;
case
A466: i1<ma;
now
per cases by A350,A440,A454,A460,A459,
GOBOARD1:27;
suppose
f/.(k+1) in rng Line(G1,i1);
hence thesis by A441,A460,A466,GOBOARD1:3;
end;
suppose
for l be Nat st f/.(k+1
) in rng Line(G1,l) & l in dom G1 holds |.i1-l.|=1;
then
A467: |.i1-j1.|=1 by A451,A450;
now
per cases by A467,SEQM_3:41;
suppose
j1<i1 & i1=j1+1;
hence thesis by A452,A466,XXREAL_0:2;
end;
suppose
i1<j1 & j1=i1+1;
hence thesis by A452,A466,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A468: Seg len h1 = dom h1 by FINSEQ_1:def 3;
A469: now
let n;
A470: n<=n+ma by NAT_1:11;
assume
A471: n in dom h2;
then n<=l2 by A421,FINSEQ_3:25;
then
A472: ma+n<=ma+l2 by XREAL_1:7;
1<=n by A471,FINSEQ_3:25;
then 1<=n+ma by A470,XXREAL_0:2;
hence ma+n in dom G1 by A472,FINSEQ_3:25;
end;
A473: now
let n;
assume
A474: n in dom h2;
reconsider m=ma+n,K2 as Nat;
take m,K2;
ma+n in dom G1 by A469,A474;
hence
[m,K2] in Indices G1 & h2/.n=G1*(m,K2) by A96,A365,A355
,A421,A474,ZFMISC_1:87;
end;
A475: now
let n;
assume that
A476: n in dom h2 and
A477: n+1 in dom h2;
ma+(n+1) in dom G1 by A469,A477;
then
A478: [ma+ n+1,K2] in Indices G1 by A96,A365,A355,ZFMISC_1:87;
let i1,i2,j1,j2 be Nat;
assume that
A479: [i1,i2] in Indices G1 and
A480: [j1,j2] in Indices G1 and
A481: h2/.n=G1*(i1,i2) and
A482: h2/.(n+1)=G1*(j1,j2);
h2/.(n+1)=G1*(ma+(n+1),K2) by A421,A477;
then
A483: j1=ma+n+1 & j2=K2 by A478,A480,A482,GOBOARD1:5;
ma +n in dom G1 by A469,A476;
then
A484: [ma+n,K2] in Indices G1 by A96,A365,A355,ZFMISC_1:87;
h2/.n=G1*(ma+n,K2) by A421,A476;
then i1=ma+n & i2=K2 by A484,A479,A481,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.ma+n-(ma+n)+-1.|+0 by
A483,ABSVALUE:2
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
A485: Seg len h2 = dom h2 by FINSEQ_1:def 3;
A486: pl<=len g by A363,FINSEQ_3:25;
A487: 1<=pl by A363,FINSEQ_3:25;
A488: pl <> pf by A39,A41,A95,A359,A363,GOBOARD1:3;
now
per cases by A488,XXREAL_0:1;
suppose
pf<pl;
then pf<len g by A486,XXREAL_0:2;
then 1<len g by A364,XXREAL_0:2;
hence 1+1<=len g by NAT_1:13;
end;
suppose
pf>pl;
then pl<len g by A418,XXREAL_0:2;
then 1<len g by A487,XXREAL_0:2;
hence 1+1<=len g by NAT_1:13;
end;
end;
then 1<=len g - 1 by XREAL_1:19;
then
A489: lg in dom g by A356,FINSEQ_3:25;
A490: PP[0] by FINSEQ_3:25;
A491: for n holds PP[n] from NAT_1:sch 2(A490,A438);
A492: rng h2 /\ rng tt = {}
proof
set x = the Element of rng h2 /\ rng tt;
assume
A493: not thesis;
then x in rng h2 by XBOOLE_0:def 4;
then consider i2 be Element of NAT such that
A494: i2 in dom h2 and
A495: h2/.i2=x by PARTFUN2:2;
0+1<=i2 by A494,FINSEQ_3:25;
then
A496: 0<i2;
ma+i2 in dom G1 by A469,A494;
then
A497: [ma+i2,K2] in Indices G1 by A96,A365,A355,ZFMISC_1:87;
x in rng tt by A493,XBOOLE_0:def 4;
then x in rng t by A354;
then consider i1 be Element of NAT such that
A498: i1 in dom f and
A499: f/.i1=x by A351,PARTFUN2:2;
consider n1,n2 be Nat such that
A500: [n1,n2] in Indices G1 and
A501: f/.i1=G1*(n1,n2) by A174,A498;
reconsider Ln1 = Line(G1,n1) as FinSequence of TOP-REAL
2;
A502: n2 in Seg width G1 by A96,A500,ZFMISC_1:87;
A503: Seg len Ln1 = dom Ln1 & len Ln1=width G1 by
FINSEQ_1:def 3,MATRIX_0:def 7;
then Ln1/.n2 = Ln1.n2 by A502,PARTFUN1:def 6;
then f/.i1=Ln1/.n2 by A501,A502,MATRIX_0:def 7;
then
A504: f/.i1 in rng Ln1 by A502,A503,PARTFUN2:2;
A505: n1 in dom G1 by A96,A500,ZFMISC_1:87;
x=G1*(ma+i2,K2) by A421,A494,A495;
then ma+i2=n1 by A499,A500,A501,A497,GOBOARD1:5;
hence contradiction by A491,A498,A505,A504,A496,
XREAL_1:29;
end;
1<=len g by A13,GOBOARD1:22;
then
A506: len g in dom g by FINSEQ_3:25;
A507: dom g c= dom g2 by A23,A24,A16,A17,FINSEQ_1:5;
now
consider i2 be Element of NAT such that
A508: i2 in dom C and
A509: C/.i2=g/.len g by A28,PARTFUN2:2;
A510: dom C = Seg len C by FINSEQ_1:def 3
.= Seg len G1 by MATRIX_0:def 8
.= dom G1 by FINSEQ_1:def 3;
then
A511: [i2,width G1] in Indices G1 by A73,A96,A508,ZFMISC_1:87;
C/.i2 = C.i2 by A508,PARTFUN1:def 6;
then
A512: g/.len g=G1*(i2,width G1) by A508,A509,A510,
MATRIX_0:def 8;
assume
A513: pl=len g;
consider n1,n2 be Nat such that
A514: [n1,n2] in Indices G1 and
A515: g/.lg=G1*(n1,n2) by A15,A489,GOBOARD1:def 9;
A516: n1 in dom G1 by A96,A514,ZFMISC_1:87;
A517: n2 in Seg width G1 by A96,A514,ZFMISC_1:87;
[ma,K2] in Indices G1 by A41,A96,A365,A355,ZFMISC_1:87;
then i2=ma by A420,A513,A512,A511,GOBOARD1:5;
then
A518: |.n1-ma.|+|.n2- width G1.|=1 by A15,A489,A506,A360,A512
,A511,A514,A515,GOBOARD1:def 9;
now
per cases by A518,SEQM_3:42;
suppose
A519: |.n1-ma.|=1 & n2=width G1;
A520: dom C = Seg len C by FINSEQ_1:def 3
.= Seg len G1 by MATRIX_0:def 8
.= dom G1 by FINSEQ_1:def 3;
then C/.n1 = C.n1 by A516,PARTFUN1:def 6;
then g/.lg=C/.n1 by A515,A516,A519,MATRIX_0:def 8;
then
A521: g/.lg in rng C by A516,A520,PARTFUN2:2;
g/.lg=g2/.lg by A13,A24,A17,A489,FINSEQ_4:71;
hence contradiction by A13,A17,A489,A507,A521,
XREAL_1:44;
end;
suppose
A522: |.n2-width G1.|=1 & n1=ma;
len Lma = width G1 by MATRIX_0:def 7;
then
A523: n2 in dom Lma by A517,FINSEQ_1:def 3;
then La/.n2 = Lma.n2 by PARTFUN1:def 6;
then g/.lg=Lma/.n2 by A515,A517,A522,MATRIX_0:def 7;
then g/.lg in rng Lma by A523,PARTFUN2:2;
hence contradiction by A363,A489,A513,XREAL_1:44;
end;
end;
hence contradiction;
end;
then
A524: pl<len g by A486,XXREAL_0:1;
len C=len G1 by MATRIX_0:def 8;
then
A525: dom C = Seg len G1 by FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
A526: Li/.K1 = Li.K1 by A367,PARTFUN1:def 6;
then
A527: g/.pf=G1*(mi, K1) by A367,A368,A400,MATRIX_0:def 7;
now
consider i2 be Element of NAT such that
A528: i2 in dom C and
A529: C/.i2=g/.len g by A28,PARTFUN2:2;
C/.i2 = C.i2 by A528,PARTFUN1:def 6;
then
A530: g/.len g=G1*(i2,width G1) by A525,A528,A529,
MATRIX_0:def 8;
A531: [i2,width G1] in Indices G1 by A73,A96,A525,A528,
ZFMISC_1:87;
assume
A532: pf=len g;
consider n1,n2 be Nat such that
A533: [n1,n2] in Indices G1 and
A534: g/.lg=G1*(n1,n2) by A15,A489,GOBOARD1:def 9;
A535: n1 in dom G1 by A96,A533,ZFMISC_1:87;
A536: n2 in Seg width G1 by A96,A533,ZFMISC_1:87;
[mi,K1] in Indices G1 by A39,A96,A367,A400,ZFMISC_1:87;
then i2=mi by A527,A532,A530,A531,GOBOARD1:5;
then
A537: |.n1-mi.|+|.n2- width G1.|=1 by A15,A489,A506,A360,A530
,A531,A533,A534,GOBOARD1:def 9;
now
per cases by A537,SEQM_3:42;
suppose
A538: |.n1-mi.|=1 & n2=width G1;
A539: dom C = Seg len C by FINSEQ_1:def 3
.= Seg len G1 by MATRIX_0:def 8
.= dom G1 by FINSEQ_1:def 3;
then C/.n1 = C.n1 by A535,PARTFUN1:def 6;
then g/.lg=C/.n1 by A534,A535,A538,MATRIX_0:def 8;
then
A540: g/.lg in rng C by A535,A539,PARTFUN2:2;
g/.lg=g2/.lg by A13,A24,A17,A489,FINSEQ_4:71;
hence contradiction by A13,A17,A489,A507,A540,
XREAL_1:44;
end;
suppose
A541: |.n2-width G1.|=1 & n1=mi;
len Li = width G1 by MATRIX_0:def 7;
then
A542: n2 in dom Li by A536,FINSEQ_1:def 3;
then Li/.n2 = Li.n2 by PARTFUN1:def 6;
then g/.lg=Li/.n2 by A534,A536,A541,MATRIX_0:def 7;
then g/.lg in rng Li by A542,PARTFUN2:2;
hence contradiction by A359,A489,A532,XREAL_1:44;
end;
end;
hence contradiction;
end;
then
A543: pf<len g by A418,XXREAL_0:1;
now
per cases by A488,XXREAL_0:1;
suppose
A544: pf<pl;
pl<=pl+1 by NAT_1:11;
then reconsider LL=pl+1-pf as Element of NAT by A544,
INT_1:5,XXREAL_0:2;
reconsider w1=pf-1 as Element of NAT by A364,INT_1:5;
set F1=g|pl;
defpred P[Nat, Element of TOP-REAL 2] means $2 = F1/.(
w1+$1);
A545: for n being Nat st n in Seg LL ex p st P[n,p];
consider F be FinSequence of TOP-REAL 2 such that
A546: len F = LL & for n being Nat st n in Seg LL
holds P[n,F/.n] from FINSEQ_4:sch 1(A545);
set hf=h1^F;
set FF = h1^F^h2;
A547: Seg len F = dom F by FINSEQ_1:def 3;
A548: for n st n in Seg LL holds F1/.(w1+n)=g/.(w1+n)
& w1+n in dom g
proof
let n such that
A549: n in Seg LL;
n<=LL by A549,FINSEQ_1:1;
then n+pf<=LL+ pf by XREAL_1:7;
then
A550: n+pf-1<=pl by XREAL_1:20;
1<=n by A549,FINSEQ_1:1;
then 0+1<=w1+n by XREAL_1:7;
then w1+n in Seg pl by A550,FINSEQ_1:1;
hence thesis by A363,FINSEQ_4:71;
end;
A551: rng F c= rng g2
proof
let x be object;
assume x in rng F;
then consider n being Element of NAT such that
A552: n in dom F and
A553: x=F/.n by PARTFUN2:2;
F/.n= F1/.(w1+n) by A546,A547,A552;
then
A554: F/.n=g/.(w1+n) by A548,A546,A547,A552;
w1+n in dom g by A548,A546,A547,A552;
then x in rng g by A553,A554,PARTFUN2:2;
hence thesis by A18;
end;
pf+1<=pl by A544,NAT_1:13;
then pf+1<=pl+1 by NAT_1:13;
then
A555: 1<=LL by XREAL_1:19;
A556: now
let i1,i2,j1,j2 be Nat;
assume that
A557: [ i1,i2] in Indices G1 and
A558: [j1,j2] in Indices G1 and
A559: hf/.len hf=G1*( i1,i2) and
A560: h2/.1=G1*(j1,j2) and
len hf in dom hf and
A561: 1 in dom h2;
ma+1 in dom G1 by A469,A561;
then
A562: [
ma+1,K2] in Indices G1 by A96,A365,A355,ZFMISC_1:87;
A563: [ma,K2] in Indices G1 by A41,A96,A365,A355,
ZFMISC_1:87;
A564: len F in dom F by A546,A547,A555,FINSEQ_1:1;
hf/.len hf=hf/.(len h1+len F) by FINSEQ_1:22
.= F/.len F by A564,FINSEQ_4:69
.= F1/.(w1+LL) by A546,A547,A564
.= G1*(ma,K2) by A420,A548,A546,A547,A564;
then
A565: i1=ma & i2=K2 by A557,A559,A563,GOBOARD1:5;
h2/.1=G1*(ma+1,K2) by A421,A561;
then j1=ma+1 & j2=K2 by A558,A560,A562,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|=|.ma-(ma+1).|+0 by A565,
ABSVALUE:2
.=|.-(ma+1 -ma).|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
A566: rng FF = rng(h1^F) \/ rng h2 by FINSEQ_1:31
.= rng h1 \/ rng F \/ rng h2 by FINSEQ_1:31;
A567: for k st k in Seg width G1 & rng F /\ rng Col(G1
,k)={} holds rng FF /\ rng Col(G1,k)={}
proof
A568: len Col(G1,K2)=len G1 by MATRIX_0:def 8;
A569: len Col(G1,K1)=len G1 by MATRIX_0:def 8;
let k;
assume that
A570: k in Seg width G1 and
A571: rng F /\ rng Col(G1,k)={};
set gg=Col(G1,k);
assume
A572: rng FF /\ rng gg <> {};
set x = the Element of rng FF /\ rng gg;
rng FF = rng F \/ (rng h1 \/ rng h2) by A566,
XBOOLE_1:4;
then
A573: rng FF /\ rng gg = {} \/ (rng h1 \/ rng h2) /\
rng gg by A571,XBOOLE_1:23
.= rng h1 /\ rng gg \/ rng h2 /\ rng gg by
XBOOLE_1:23;
now
per cases by A572,A573,XBOOLE_0:def 3;
suppose
A574: x in rng h1 /\ rng gg;
then x in rng h1 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A575: i in dom h1 and
A576: x=h1/.i by PARTFUN2:2;
A577: x=G1*(i,K1) by A369,A575,A576;
reconsider y=x as Point of TOP-REAL 2 by A576;
A578: Lmi/.K1 = Lmi.K1 by A367,PARTFUN1:def 6;
A579: x in rng gg by A574,XBOOLE_0:def 4;
A580: dom CK1 = Seg len G1 by A569,FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then
A581: CK1/.mi = CK1.mi by A39,PARTFUN1:def 6;
A582: i in dom CK1 by A401,A575,A580;
CK1/.i = CK1.i by A401,A575,A580,PARTFUN1:def 6;
then y=CK1/.i by A577,A580,A582,MATRIX_0:def 8;
then y in rng CK1 by A582,PARTFUN2:2;
then
A583: K1=k by A367,A400,A570,A579,GOBOARD1:4;
A584: 1 in Seg LL by A555,FINSEQ_1:1;
then F/.1=F1/.(w1+1) & F1/.(w1+1)=g/.(w1+1) by
A548,A546;
then F/.1= CK1/.mi by A39,A367,A368,A400,A578
,A581,MATRIX_0:42;
then
A585: F/.1 in rng Col(G1,k) by A39,A580,A583,PARTFUN2:2
;
F/.1 in rng F by A546,A547,A584,PARTFUN2:2;
hence contradiction by A571,A585,XBOOLE_0:def 4;
end;
suppose
A586: x in rng h2 /\ rng gg;
then x in rng h2 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A587: i in dom h2 and
A588: x=h2/.i by PARTFUN2:2;
A589: x=G1*(ma+i,K2) by A421,A587,A588;
reconsider y=x as Point of TOP-REAL 2 by A588;
A590: Lma /.K2 = Lma.K2 by A365,PARTFUN1:def 6;
A591: x in rng gg by A586,XBOOLE_0:def 4;
A592: dom CK2 = Seg len G1 by A568,FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then
A593: CK2/.ma = CK2.ma by A41,PARTFUN1:def 6;
A594: ma+i in dom CK2 by A469,A587,A592;
CK2/.(ma+i) = CK2.(ma+i) by A469,A587,A592,
PARTFUN1:def 6;
then y=CK2/.(ma+i) by A589,A592,A594,
MATRIX_0:def 8;
then y in rng CK2 by A594,PARTFUN2:2;
then
A595: K2=k by A365,A355,A570,A591,GOBOARD1:4;
A596: LL in Seg LL by A555,FINSEQ_1:1;
then F/.LL=F1/.(w1+LL) & F1/.(w1+LL)=g/.(w1+LL
) by A548,A546;
then F/.LL= CK2/.ma by A41,A365,A366,A355,A590
,A593,MATRIX_0:42;
then
A597: F/.LL in rng Col(G1,k) by A41,A592,A595,
PARTFUN2:2;
F/.LL in rng F by A546,A547,A596,PARTFUN2:2;
hence contradiction by A571,A597,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
rng F /\ rng C = {}
proof
reconsider w=w1 as Nat;
set x = the Element of rng F /\ rng C;
assume
A598: not thesis;
then
A599: x in rng C by XBOOLE_0:def 4;
x in rng F by A598,XBOOLE_0:def 4;
then consider i1 be Element of NAT such that
A600: i1 in dom F and
A601: F/.i1=x by PARTFUN2:2;
A602: Seg len F = dom F by FINSEQ_1:def 3;
then i1<=LL by A546,A600,FINSEQ_1:1;
then
A603: w+i1<=w+LL by XREAL_1:7;
A604: w1+i1 in dom g by A548,A546,A600,A602;
then
A605: w+i1 in dom g2 by A13,A24,A17,FINSEQ_4:71;
F /.i1=F1/.(w1+i1) & F1/.(w1+i1)= g/.(w1+i1)
by A548,A546,A600,A602;
then g2/.(w+i1) in rng C by A13,A24,A17,A599,A601
,A604,FINSEQ_4:71;
then m<=w+i1 by A13,A605;
hence contradiction by A17,A524,A603,XXREAL_0:2;
end;
then rng FF /\ rng Col(G1,width G1) = {} by A73,A567;
then
A606: rng FF misses rng Col(G1,width G1) by XBOOLE_0:def 7;
now
reconsider w=w1 as Nat;
let n;
assume
A607: n in dom F;
then w1+n in dom g by A548,A546,A547;
then consider i,j such that
A608: [i,j] in Indices G1 & g/.(w+n)=G1*(i,j) by A15,
GOBOARD1:def 9;
take i,j;
F/.n= F1/.(w1+n) by A546,A547,A607;
hence [i,j] in Indices G1 & F/.n=G1*(i,j) by A548
,A546,A547,A607,A608;
end;
then for n st n in dom(h1^F) ex i,j st [i,j] in
Indices G1 & (h1^F)/.n=G1*(i,j) by A406,GOBOARD1:23;
then
A609: for n st n in dom FF ex i,j st [i,j] in Indices
G1 & FF/.n=G1*(i,j) by A473,GOBOARD1:23;
A610: now
A611: [mi,K1] in Indices G1 by A39,A96,A367,A400,
ZFMISC_1:87;
let i1,i2,j1,j2 be Nat;
assume that
A612: [i1,i2] in Indices G1 and
A613: [j1,j2] in Indices G1 and
A614: h1/.len h1=G1*(i1,i2) and
A615: F/.1=G1*(j1,j2) and
A616: len h1 in dom h1 and
A617: 1 in dom F;
F/.1=F1/.(w1+1) by A546,A547,A617;
then F/.1=g/.(w1+1) by A548,A546,A547,A617
.= G1*(mi,K1) by A367,A368,A400,A526,MATRIX_0:def 7
;
then
A618: j1=mi & j2=K1 by A613,A615,A611,GOBOARD1:5;
l1 in dom G1 by A369,A401,A616;
then
A619: [l1,K1] in Indices G1 by A96,A367,A400,ZFMISC_1:87;
h1/.len h1=G1*(l1,K1) by A369,A616;
then i1=l1 & i2=K1 by A612,A614,A619,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.mi-1-mi.|+0 by A618,
ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
now
let n;
assume that
A620: n in dom F and
A621: n+1 in dom F;
F/.n=F1/.(w1+n) by A546,A547,A620;
then
A622: F/.n=g/.(w1+n) by A548,A546,A547,A620;
F/.(n+1)=F1/.(w1+(n+1)) by A546,A547,A621;
then
A623: w1+n+1 in dom g & F/.(n+1)=g/.(w1+n+1) by A548,A546
,A547,A621;
let i1,i2,j1,j2 be Nat;
assume
A624: [i1,i2] in Indices G1 & [j1,j2] in Indices
G1 & F/.n=G1*(i1,i2) & F/. (n+1)=G1*(j1,j2);
w1+n in dom g by A548,A546,A547,A620;
hence |.i1-j1.|+|.i2-j2.|=1 by A15,A622,A623,A624,
GOBOARD1:def 9;
end;
then for n st n in dom(h1^F) & n+1 in dom(h1^F) for
i1,i2,j1,j2 be Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1
& (h1^F)/.n=G1*(i1,i2) & (h1^F)/.(n+1)=G1*(j1,j2) holds |.i1-j1.|+|.i2-j2.|=1
by A408,A610,GOBOARD1:24;
then for n st n in dom FF & n+1 in dom FF for i1,i2,
j1,j2 be Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1 & FF/.
n=G1*(i1,i2) & FF/.(n+1)=G1*(j1,j2) holds |.i1-j1.|+|.i2-j2.|=1 by A475,A556,
GOBOARD1:24;
then FF is_sequence_on G1 by A609,GOBOARD1:def 9;
then
A625: FF is_sequence_on D by A73,A152,A606,GOBOARD1:25;
set x = the Element of rng FF /\ rng tt;
A626: 0+1<=len F+(len h1+len h2) by A546,A555,XREAL_1:7;
A627: now
per cases;
suppose
A628: mi=1;
A629: pf in Seg pl by A364,A544,FINSEQ_1:1;
A630: 1 in Seg LL by A555,FINSEQ_1:1;
h1 = {} by A369,A628;
then FF=F^h2 by FINSEQ_1:34;
then FF/.1=F/.1 by A546,A547,A630,FINSEQ_4:68
.= F1/.(w1+1) by A546,A630
.= g/.pf by A363,A629,FINSEQ_4:71;
hence FF/.1 in rng Line(G1,1) by A359,A628;
end;
suppose
A631: mi<>1;
1<=mi by A39,FINSEQ_3:25;
then 1<mi by A631,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A632: 1<=l1 by XREAL_1:19;
then
A633: 1 in Seg l1 by FINSEQ_1:1;
len Line(G1,1)=width G1 by MATRIX_0:def 7;
then
A634: K1 in dom L1 by A367,A400,FINSEQ_1:def 3;
then
A635: L1/.K1 = L1.K1 by PARTFUN1:def 6;
len(h1^F)=len h1 + len F & 0<=len F by FINSEQ_1:22;
then 0+1<=len(h1^F) by A369,A632,XREAL_1:7;
then 1 in dom(h1^F) by FINSEQ_3:25;
then FF/.1=(h1^F)/.1 by FINSEQ_4:68
.=h1/.1 by A369,A468,A633,FINSEQ_4:68
.=G1*(1,K1) by A369,A468,A633
.=L1/.K1 by A367,A400,A635,MATRIX_0:def 7;
hence FF/.1 in rng Line(G1,1) by A634,PARTFUN2:2;
end;
end;
A636: w1+LL= pl;
A637: now
per cases;
suppose
A638: ma=len G1;
1<=pl by A24,A363,FINSEQ_1:1;
then
A639: pl in Seg pl by FINSEQ_1:1;
A640: len F in dom F by A546,A555,FINSEQ_3:25;
h2 = {} by A421,A638;
then
A641: FF=h1^F by FINSEQ_1:34;
then FF/.len FF=FF/.(len h1+len F) by FINSEQ_1:22
.= F/.LL by A546,A641,A640,FINSEQ_4:69
.= F1/.pl by A546,A547,A636,A640
.= g/.pl by A363,A639,FINSEQ_4:71;
hence FF/.len FF in rng Line(G1,len G1) by A363
,A638;
end;
suppose
A642: ma<>len G1;
ma<=len G1 by A41,FINSEQ_3:25;
then ma<len G1 by A642,XXREAL_0:1;
then ma+1<=len G1 by NAT_1:13;
then
A643: 1<=l2 by XREAL_1:19;
then
A644: l2 in Seg l2 by FINSEQ_1:1;
len Line(G1,len G1)=width G1 by MATRIX_0:def 7;
then
A645: K2 in dom Ll by A365,A355,FINSEQ_1:def 3;
then
A646: Ll/.K2 = Ll.K2 by PARTFUN1:def 6;
A647: len h2 in dom h2 by A421,A643,FINSEQ_3:25;
FF/.len FF=FF/.(len(h1^F)+len h2) by FINSEQ_1:22
.=h2/.l2 by A421,A647,FINSEQ_4:69
.=G1*(ma+l2,K2) by A421,A485,A644
.=Ll/.K2 by A365,A355,A646,MATRIX_0:def 7;
hence FF/.len FF in rng Line(G1,len G1) by A645,
PARTFUN2:2;
end;
end;
rng tt c= rng f by A351,A354;
then
A648: rng tt c= rng g1 by A178;
A649: len FF=len(h1^F)+len h2 by FINSEQ_1:22
.=len h1+len F+len h2 by FINSEQ_1:22;
then 1 in dom FF by A626,FINSEQ_3:25;
then
A650: FF/. 1 in rng Line(D,1) by A73,A26,A152,A627,A606,
MATRIX_0:75;
len FF in dom FF by A649,A626,FINSEQ_3:25;
then
A651: FF/.len FF in rng Line(D,len D) by A73,A27,A152,A153
,A637,A606,MATRIX_0:75;
width D=k by A3,A73,MATRIX_0:63;
then rng FF /\ rng tt <> {} by A2,A92,A353,A649,A626
,A625,A650,A651,A341;
then
A652: x in rng FF /\ rng tt;
rng tt /\ rng FF = ((rng h1 \/ rng F) /\ rng tt
) \/ {} by A492,A566,XBOOLE_1:23
.= {} \/ rng F /\ rng tt by A424,XBOOLE_1:23
.= rng tt /\ rng F;
then rng FF /\ rng tt c= rng g1 /\ rng g2 by A648,A551,
XBOOLE_1:27;
hence thesis by A652;
end;
suppose
A653: pl<pf;
pf<=pf+1 by NAT_1:11;
then reconsider LL=pf+1-pl as Element of NAT by A653,
INT_1:5,XXREAL_0:2;
set F1=g|pf;
defpred P[Nat,Element of TOP-REAL 2] means for k st k
= pf+1-$1 holds $2 = F1/.k;
A654: for n,k st n in Seg LL & k = pf+1-n holds F1/.k
=g/.k & k in dom g
proof
let n,k;
assume that
A655: n in Seg LL and
A656: k = pf+1-n;
A657: n<=LL by A655,FINSEQ_1:1;
1<=n by A655,FINSEQ_1:1;
then
A658: pf+1-n<=pf+1-1 by XREAL_1:13;
LL<=pf+1-0 by XREAL_1:13;
then reconsider w=pf+1-n as Element of NAT by A657,
INT_1:5,XXREAL_0:2;
pf+1-LL<=pf+1-n by A657,XREAL_1:13;
then 1<=pf+1-n by A487,XXREAL_0:2;
then w in Seg pf by A658,FINSEQ_1:1;
hence thesis by A359,A656,FINSEQ_4:71;
end;
A659: for n st n in Seg LL holds pf+1-n is Element of NAT
proof
let n;
A660: LL<=pf+1-0 by XREAL_1:13;
assume n in Seg LL;
then n<=LL by FINSEQ_1:1;
hence thesis by A660,INT_1:5,XXREAL_0:2;
end;
A661: for n being Nat st n in Seg LL ex p st P[n,p]
proof
let n be Nat;
assume
A662: n in Seg LL;
then reconsider
k = pf+1-n as Nat by A659;
take g/.k;
thus thesis by A654,A662;
end;
consider F be FinSequence of TOP-REAL 2 such that
A663: len F = LL & for n being Nat st n in Seg LL
holds P[n,F/.n] from FINSEQ_4:sch 1(A661);
set hf=h1^F;
set FF = h1^F^h2;
A664: Seg len F = dom F by FINSEQ_1:def 3;
A665: rng F c= rng g2
proof
let x be object;
assume x in rng F;
then consider n being Element of NAT such that
A666: n in dom F and
A667: x=F/.n by PARTFUN2:2;
reconsider u = pf+1-n as Nat by A659,A663
,A664,A666;
F/.n=F1/.u by A663,A664,A666;
then pf+1-n in dom g & F/.n=g/.u by A654,A663,A664
,A666;
then x in rng g by A667,PARTFUN2:2;
hence thesis by A18;
end;
pl+1<=pf by A653,NAT_1:13;
then pl+1<=pf+1 by NAT_1:13;
then
A668: 1<=LL by XREAL_1:19;
A669: now
reconsider u = pf+1-LL as Nat;
let i1,i2,j1,j2 be Nat;
assume that
A670: [ i1,i2] in Indices G1 and
A671: [j1,j2] in Indices G1 and
A672: hf/.len hf=G1*(i1,i2) and
A673: h2/.1=G1*(j1,j2) and
len hf in dom hf and
A674: 1 in dom h2;
ma+1 in dom G1 by A469,A674;
then
A675: [ma+1,K2] in Indices G1 by A96,A365,A355,ZFMISC_1:87;
A676: [ma,K2] in Indices G1 by A41,A96,A365,A355,
ZFMISC_1:87;
A677: len F in dom F by A663,A668,FINSEQ_3:25;
hf/.len hf=hf/.(len h1+len F) by FINSEQ_1:22
.= F/.len F by A677,FINSEQ_4:69
.= F1/.u by A663,A664,A677
.= g/.u by A654,A663,A664,A677
.= G1*(ma,K2) by A365,A366,A355,A419,MATRIX_0:def 7
;
then
A678: i1=ma & i2=K2 by A670,A672,A676,GOBOARD1:5;
h2/.1=G1*(ma+1,K2) by A421,A674;
then j1=ma+1 & j2=K2 by A671,A673,A675,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|=|.ma-(ma+1).|+0 by A678,
ABSVALUE:2
.=|.-(ma+1 -ma).|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
now
let n;
assume
A679: n in dom F;
then reconsider
w=pf+1-n as Nat by A659,A663,A664;
A680: F/.n=F1/.w by A663,A664,A679;
then pf+1-n in dom g by A654,A663,A664,A679;
then consider i,j such that
A681: [i,j] in Indices G1 & g/.w=G1*(i,j) by A15,
GOBOARD1:def 9;
take i,j;
thus [i,j] in Indices G1 & F/.n=G1*(i,j) by A654,A663
,A664,A679,A680,A681;
end;
then for n st n in dom(h1^F) ex i,j st [i,j] in
Indices G1 & (h1^F)/.n=G1*(i,j) by A406,GOBOARD1:23;
then
A682: for n st n in dom FF ex i,j st [i,j] in Indices
G1 & FF/.n=G1*(i,j) by A473,GOBOARD1:23;
set x = the Element of rng FF /\ rng tt;
A683: 0+1<=len F+(len h1+len h2) by A663,A668,XREAL_1:7;
A684: rng FF = rng(h1^F) \/ rng h2 by FINSEQ_1:31
.= rng h1 \/ rng F \/ rng h2 by FINSEQ_1:31;
A685: for k st k in Seg width G1 & rng F /\ rng Col(
G1,k)={} holds rng FF /\ rng Col(G1,k)={}
proof
A686: len Col(G1,K2)=len G1 by MATRIX_0:def 8;
A687: len Col(G1,K1)=len G1 by MATRIX_0:def 8;
let k;
assume that
A688: k in Seg width G1 and
A689: rng F /\ rng Col(G1,k)={};
set gg=Col(G1,k);
assume
A690: rng FF /\ rng gg <> {};
set x = the Element of rng FF /\ rng gg;
rng FF = rng F \/ (rng h1 \/ rng h2) by A684,
XBOOLE_1:4;
then
A691: rng FF /\ rng gg = {} \/ (rng h1 \/ rng h2)
/\ rng gg by A689,XBOOLE_1:23
.= rng h1 /\ rng gg \/ rng h2 /\ rng gg by
XBOOLE_1:23;
now
per cases by A690,A691,XBOOLE_0:def 3;
suppose
A692: x in rng h1 /\ rng gg;
then
A693: x in rng gg by XBOOLE_0:def 4;
A694: 1 in Seg LL by A668,FINSEQ_1:1;
pf+1-1 = pf;
then
A695: F/.1=F1/.pf & F1/.pf=g/.pf by A654,A663,A694;
x in rng h1 by A692,XBOOLE_0:def 4;
then consider i being Element of NAT such that
A696: i in dom h1 and
A697: x=h1/.i by PARTFUN2:2;
A698: x=G1*(i,K1) by A369,A696,A697;
reconsider y=x as Point of TOP-REAL 2 by A697;
A699: Lmi/.K1 = Lmi.K1 by A367,PARTFUN1:def 6;
A700: dom CK1 = Seg len G1 by A687,FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then
A701: i in dom CK1 by A401,A696;
CK1/.i = CK1.i by A401,A696,A700,PARTFUN1:def 6;
then y=CK1/.i by A698,A700,A701,MATRIX_0:def 8;
then y in rng CK1 by A701,PARTFUN2:2;
then
A702: K1=k by A367,A400,A688,A693,GOBOARD1:4;
CK1/.mi = CK1.mi by A39,A700,PARTFUN1:def 6;
then F/.1=CK1/.mi by A39,A367,A368,A400,A699,A695
,MATRIX_0:42;
then
A703: F/.1 in rng Col(G1,k) by A39,A700,A702,PARTFUN2:2
;
F/.1 in rng F by A663,A664,A694,PARTFUN2:2;
hence contradiction by A689,A703,XBOOLE_0:def 4;
end;
suppose
A704: x in rng h2 /\ rng gg;
then x in rng h2 by XBOOLE_0:def 4;
then consider i being Element of NAT such that
A705: i in dom h2 and
A706: x=h2/.i by PARTFUN2:2;
A707: x=G1*(ma+i,K2) by A421,A705,A706;
reconsider y=x as Point of TOP-REAL 2 by A706;
A708: x in rng gg by A704,XBOOLE_0:def 4;
reconsider u = pf+1-LL as Nat;
A709: Lma /.K2 = Lma.K2 by A365,PARTFUN1:def 6;
A710: dom CK2 = Seg len G1 by A686,FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3;
then
A711: CK2/.ma = CK2.ma by A41,PARTFUN1:def 6;
A712: ma+i in dom CK2 by A469,A705,A710;
CK2/.(ma+i) = CK2.(ma+i) by A469,A705,A710,
PARTFUN1:def 6;
then y=CK2/.(ma+i) by A707,A710,A712,
MATRIX_0:def 8;
then y in rng CK2 by A712,PARTFUN2:2;
then
A713: K2=k by A365,A355,A688,A708,GOBOARD1:4;
A714: LL in Seg LL by A668,FINSEQ_1:1;
then F/.LL=F1/.u & F1/.u=g/.u by A654,A663;
then F/.LL= CK2/.ma by A41,A365,A366,A355,A709
,A711,MATRIX_0:42;
then
A715: F/.LL in rng Col(G1,k) by A41,A710,A713,
PARTFUN2:2;
F/.LL in rng F by A663,A664,A714,PARTFUN2:2;
hence contradiction by A689,A715,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
rng F /\ rng C = {}
proof
set x = the Element of rng F /\ rng C;
assume
A716: not thesis;
then
A717: x in rng C by XBOOLE_0:def 4;
x in rng F by A716,XBOOLE_0:def 4;
then consider i1 be Element of NAT such that
A718: i1 in dom F and
A719: F/.i1=x by PARTFUN2:2;
reconsider w=pf+1-i1 as Nat by A659,A663
,A664,A718;
1<=i1 by A718,FINSEQ_3:25;
then
A720: w<=pf+1-1 by XREAL_1:13;
A721: w in dom g by A654,A663,A664,A718;
then
A722: w in dom g2 by A13,A24,A17,FINSEQ_4:71;
F/.i1=F1/.w & F1/.w=g/.w by A654,A663,A664,A718;
then g2/.w in rng C by A13,A24,A17,A717,A719,A721,
FINSEQ_4:71;
then m<=w by A13,A722;
hence contradiction by A17,A543,A720,XXREAL_0:2;
end;
then rng FF /\ rng Col(G1,width G1) = {} by A73,A685;
then
A723: rng FF misses rng Col(G1,width G1) by XBOOLE_0:def 7;
A724: now
let n;
assume that
A725: n in dom F and
A726: n+1 in dom F;
reconsider w3=pf+1-n, w2=pf+1-(n+1) as Element of
NAT by A659,A663,A664,A725,A726;
F/.n=F1/.w3 by A663,A664,A725;
then
A727: pf+1-n in dom g & F/.n =g/.w3 by A654,A663,A664,A725;
F/.(n+1)=F1/.w2 by A663,A664,A726;
then
A728: pf+1-(n+1) in dom g & F/.(n+1)=g/.w2 by A654,A663
,A664,A726;
let i1,i2,j1,j2 be Nat;
assume
A729: [i1,i2] in Indices G1 & [j1,j2] in
Indices G1 & F/.n=G1*(i1,i2) & F/. (n+1)=G1*(j1,j2);
w2+1=pf+1-n;
hence 1=|.j1-i1.|+|.j2-i2.| by A15,A727,A728,A729,
GOBOARD1:def 9
.= |.-(i1-j1).|+|.-(i2-j2).|
.= |.i1-j1.|+|.-(i2-j2).| by COMPLEX1:52
.= |.i1-j1.|+|.i2-j2.| by COMPLEX1:52;
end;
A730: pf+1-1 = pf;
A731: now
per cases;
suppose
A732: mi=1;
A733: pf in Seg pf by A364,FINSEQ_1:1;
A734: 1 in Seg LL by A668,FINSEQ_1:1;
h1 = {} by A369,A732;
then FF=F^h2 by FINSEQ_1:34;
then FF/.1=F/.1 by A663,A664,A734,FINSEQ_4:68
.= F1/.pf by A663,A730,A734
.= g/.pf by A359,A733,FINSEQ_4:71;
hence FF/.1 in rng Line(G1,1) by A359,A732;
end;
suppose
A735: mi<>1;
1<=mi by A39,FINSEQ_3:25;
then 1<mi by A735,XXREAL_0:1;
then 1+1<=mi by NAT_1:13;
then
A736: 1<=l1 by XREAL_1:19;
then
A737: 1 in Seg l1 by FINSEQ_1:1;
len Line(G1,1)=width G1 by MATRIX_0:def 7;
then
A738: K1 in dom L1 by A367,A400,FINSEQ_1:def 3;
then
A739: L1/.K1 = L1.K1 by PARTFUN1:def 6;
len(h1^F)=len h1 + len F & 0<=len F by FINSEQ_1:22;
then 0+1<=len(h1^F) by A369,A736,XREAL_1:7;
then 1 in dom(h1^F) by FINSEQ_3:25;
then FF/.1=(h1^F)/.1 by FINSEQ_4:68
.=h1/.1 by A369,A468,A737,FINSEQ_4:68
.=G1*(1,K1) by A369,A468,A737
.=L1/.K1 by A367,A400,A739,MATRIX_0:def 7;
hence FF/.1 in rng Line(G1,1) by A738,PARTFUN2:2;
end;
end;
rng tt c= rng f by A351,A354;
then
A740: rng tt c= rng g1 by A178;
now
A741: [mi,K1] in Indices G1 by A39,A96,A367,A400,
ZFMISC_1:87;
reconsider w4 = pf + 1 - 1 as Nat;
let i1,i2,j1,j2 be Nat;
assume that
A742: [i1,i2] in Indices G1 and
A743: [j1,j2] in Indices G1 and
A744: h1/.len h1=G1*(i1,i2) and
A745: F/.1=G1*(j1,j2) and
A746: len h1 in dom h1 and
A747: 1 in dom F;
F/.1 = F1/.w4 by A663,A664,A747
.= g/.w4 by A654,A663,A664,A747
.= G1*(mi,K1) by A367,A368,A400,A526,MATRIX_0:def 7
;
then
A748: j1=mi & j2=K1 by A743,A745,A741,GOBOARD1:5;
l1 in dom G1 by A369,A401,A746;
then
A749: [l1,K1] in Indices G1 by A96,A367,A400,ZFMISC_1:87;
h1/.len h1=G1*(l1,K1) by A369,A746;
then i1=l1 & i2=K1 by A742,A744,A749,GOBOARD1:5;
hence |.i1-j1.|+|.i2-j2.|= |.mi-1-mi.|+0 by A748,
ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
then for n st n in dom(h1^F) & n+1 in dom(h1^F) for
i1,i2,j1,j2 be Nat st [i1,i2] in Indices G1 & [j1,j2] in Indices G1
& (h1^F)/.n=G1*(i1,i2) & (h1^F)/.(n+1)=G1*(j1,j2) holds |.i1-j1.|+|.i2-j2.|=1
by A408,A724,GOBOARD1:24;
then for n st n in dom FF & n+1 in dom FF for m,k,i,
j st [m,k] in Indices G1 & [i,j] in Indices G1 & FF/.n=G1*(m,k) & FF/.(n+1)=G1*
(i,j) holds |.m-i.|+|.k-j.|=1 by A475,A669,GOBOARD1:24;
then FF is_sequence_on G1 by A682,GOBOARD1:def 9;
then
A750: FF is_sequence_on D by A73,A152,A723,GOBOARD1:25;
A751: len FF=len(h1^F)+len h2 by FINSEQ_1:22
.=len h1+len F+len h2 by FINSEQ_1:22;
then 1 in dom FF by A683,FINSEQ_3:25;
then
A752: FF/. 1 in rng Line(D,1) by A73,A26,A152,A731,A723,
MATRIX_0:75;
A753: now
per cases;
suppose
A754: ma=len G1;
A755: pl in Seg pf by A487,A653,FINSEQ_1:1;
A756: pf+1-(pf+1-pl) = pl;
A757: len F in dom F by A663,A668,FINSEQ_3:25;
h2 = {} by A421,A754;
then
A758: FF=h1^F by FINSEQ_1:34;
then FF/.len FF=FF/.(len h1+len F) by FINSEQ_1:22
.= F/.LL by A663,A758,A757,FINSEQ_4:69
.= F1/.pl by A663,A664,A756,A757
.= g/.pl by A359,A755,FINSEQ_4:71;
hence FF/.len FF in rng Line(G1,len G1) by A363
,A754;
end;
suppose
A759: ma<>len G1;
ma<=len G1 by A41,FINSEQ_3:25;
then ma<len G1 by A759,XXREAL_0:1;
then ma+1<=len G1 by NAT_1:13;
then
A760: 1<=l2 by XREAL_1:19;
then
A761: l2 in Seg l2 by FINSEQ_1:1;
len Line(G1,len G1)=width G1 by MATRIX_0:def 7;
then
A762: K2 in dom Ll by A365,A355,FINSEQ_1:def 3;
then
A763: Ll/.K2 = Ll.K2 by PARTFUN1:def 6;
A764: len h2 in dom h2 by A421,A760,FINSEQ_3:25;
FF/.len FF=FF/.(len(h1^F)+len h2) by FINSEQ_1:22
.=h2/.l2 by A421,A764,FINSEQ_4:69
.=G1*(ma+l2,K2) by A421,A485,A761
.=Ll/.K2 by A365,A355,A763,MATRIX_0:def 7;
hence FF/.len FF in rng Line(G1,len G1) by A762,
PARTFUN2:2;
end;
end;
len FF in dom FF by A751,A683,FINSEQ_3:25;
then
A765: FF/.len FF in rng Line(D,len D) by A73,A27,A152,A153
,A753,A723,MATRIX_0:75;
width D=k by A3,A73,MATRIX_0:63;
then rng FF /\ rng tt <> {} by A2,A92,A353,A751,A683
,A750,A752,A765,A341;
then
A766: x in rng FF /\ rng tt;
rng tt /\ rng FF = ((rng h1 \/ rng F) /\ rng tt
) \/ {} by A492,A684,XBOOLE_1:23
.= {} \/ rng F /\ rng tt by A424,XBOOLE_1:23
.= rng tt /\ rng F;
then rng FF /\ rng tt c= rng g1 /\ rng g2 by A740,A665,
XBOOLE_1:27;
hence thesis by A766;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A767: P[0];
A768: for k holds P[k] from NAT_1:sch 2(A767,A1);
A769: now
let k;
let G1,g1,g2;
assume k=width G1 & k>0 & 1<=len g1 & 1<=len g2 & g1 is_sequence_on G1
& g2 is_sequence_on G1 & g1/.1 in rng Line(G1,1) & g1/.len g1 in rng Line(G1,
len G1) & g2/.1 in rng Col(G1,1) & g2/.len g2 in rng Col(G1,width G1);
then rng g1 /\ rng g2 <> {} by A768;
hence rng g1 meets rng g2 by XBOOLE_0:def 7;
end;
width G <> 0 by MATRIX_0:def 10;
then
A770: width G > 0;
assume 1<=len f1 & 1<=len f2 & f1 is_sequence_on G & f2 is_sequence_on G &
f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) & f2/.1 in rng Col(G,
1) & f2/.len f2 in rng Col(G,width G);
hence thesis by A769,A770;
end;
theorem Th2:
for G,f1,f2 st 2<=len f1 & 2<=len f2 & f1 is_sequence_on G & f2
is_sequence_on G & f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds L~f1 meets L~f2
proof
let G,f1,f2;
assume that
A1: 2<=len f1 and
A2: 2<=len f2 and
A3: f1 is_sequence_on G & f2 is_sequence_on G & f1/.1 in rng Line(G,1) &
f1/. len f1 in rng Line(G,len G) & f2/.1 in rng Col(G,1) & f2/.len f2 in rng
Col( G,width G);
1<=len f1 & 1<=len f2 by A1,A2,XXREAL_0:2;
then rng f1 meets rng f2 by A3,Th1;
then consider x being object such that
A4: x in rng f1 and
A5: x in rng f2 by XBOOLE_0:3;
ex m being Element of NAT st m in dom f2 & f2/.m=x by A5,PARTFUN2:2;
then
A6: x in L~f2 by A2,GOBOARD1:1;
ex n being Element of NAT st n in dom f1 & f1/.n=x by A4,PARTFUN2:2;
then x in L~f1 by A1,GOBOARD1:1;
hence thesis by A6,XBOOLE_0:3;
end;
theorem
for G,f1,f2 st 2 <= len f1 & 2 <= len f2 & f1 is_sequence_on G & f2
is_sequence_on G & f1/.1 in rng Line(G,1) & f1/.len f1 in rng Line(G,len G) &
f2/.1 in rng Col(G,1) & f2/.len f2 in rng Col(G,width G) holds L~f1 meets L~f2
by Th2;
definition
let f be Relation, r,s be Real;
pred f lies_between r,s means
rng f c= [. r,s .];
end;
definition
let f be FinSequence of REAL, r,s be Real;
redefine pred f lies_between r,s means :: redefines lies_between (GOBOARD4, definition)
for n st n in dom f holds r <= f.n & f.n <= s;
compatibility
proof
hereby
assume f lies_between r,s;
then
A1: rng f c= [. r,s .];
let n;
assume n in dom f;
then f.n in rng f by FUNCT_1:3;
hence r <= f.n & f.n <= s by A1,XXREAL_1:1;
end;
assume
A2: for n st n in dom f holds r <= f.n & f.n <= s;
let y be object;
assume y in rng f;
then consider x being object such that
A3: x in dom f and
A4: y = f.x by FUNCT_1:def 3;
reconsider n=x as Nat by A3;
r <= f.n & f.n <= s by A2,A3;
hence thesis by A4,XXREAL_1:1;
end;
end;
theorem Th4:
for f1,f2 being FinSequence of TOP-REAL 2 st 2<=len f1 & 2<=len
f2 & f1 is special & f2 is special & (for n st n in dom f1 & n+1 in dom f1
holds f1/.n <> f1/.(n+1)) & (for n st n in dom f2 & n+1 in dom f2 holds f2/.n
<> f2/.(n+1)) & X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & Y_axis(f1)
lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) & Y_axis(f2) lies_between (
Y_axis(f2)).1, (Y_axis(f2)).(len f2) holds L~f1 meets L~f2
proof
let f1,f2 be FinSequence of TOP-REAL 2;
assume that
A1: 2<=len f1 and
A2: 2<=len f2 and
A3: f1 is special and
A4: f2 is special and
A5: for n st n in dom f1 & n+1 in dom f1 holds f1/.n <> f1/.(n+1) and
A6: for n st n in dom f2 & n+1 in dom f2 holds f2/.n <> f2/.(n+1) and
A7: X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) and
A8: X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) and
A9: Y_axis(f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) and
A10: Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2);
len f1 <> 0 & len f2 <> 0 by A1,A2;
then reconsider f1, f2 as non empty FinSequence of TOP-REAL 2;
reconsider f = f1^f2 as non empty FinSequence of TOP-REAL 2;
A11: Seg len f2=dom f2 by FINSEQ_1:def 3;
reconsider p1=f1/.1, p2=f1/.len f1, q1=f2/.1, q2=f2/.len f2 as Point of
TOP-REAL 2;
set x = X_axis(f), y = Y_axis(f), x1 = X_axis(f1), y1 = Y_axis(f1), x2 =
X_axis(f2), y2 = Y_axis(f2);
A12: Seg len f1=dom f1 by FINSEQ_1:def 3;
A13: 1<=len f1 by A1,XXREAL_0:2;
then
A14: 1 in dom f1 by FINSEQ_3:25;
then
A15: f/.1=f1/.1 by FINSEQ_4:68;
A16: Seg len f=dom f by FINSEQ_1:def 3;
set G = GoB(f);
A17: dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
A18: Seg len x2=dom x2 & len x2=len f2 by FINSEQ_1:def 3,GOBOARD1:def 1;
A19: len f = len f1 + len f2 by FINSEQ_1:22;
A20: Seg len x1=dom x1 & len x1=len f1 by FINSEQ_1:def 3,GOBOARD1:def 1;
then
A21: x1.1=p1`1 by A12,A14,GOBOARD1:def 1;
A22: now
let m;
set s = x.m;
assume
A23: m in dom f;
then
A24: m<=len f by FINSEQ_3:25;
A25: 1<=m by A23,FINSEQ_3:25;
now
per cases;
suppose
A26: m<=len f1;
reconsider u=f1/.m as Point of TOP-REAL 2;
A27: m in dom f1 by A25,A26,FINSEQ_3:25;
then f/.m=u by FINSEQ_4:68;
then
A28: x.m=u`1 by A16,A17,A23,GOBOARD1:def 1;
x1.m=u`1 by A12,A20,A27,GOBOARD1:def 1;
hence p1`1<=s by A7,A12,A20,A21,A27,A28;
end;
suppose
A29: len f1<m;
then reconsider w5 = m-len f1 as Element of NAT by INT_1:5;
w5 > 0 by A29,XREAL_1:50;
then
A30: 1<=w5 by NAT_1:14;
A31: m = w5 + len f1;
then reconsider m1=m-len f1 as Nat;
reconsider u=f2/.m1 as Point of TOP-REAL 2;
A32: w5<=len f2 by A19,A24,A31,XREAL_1:6;
then f/.m = f2/.w5 by A31,A30,SEQ_4:136;
then
A33: x.m=u`1 by A16,A17,A23,GOBOARD1:def 1;
A34: m1 in dom f2 by A30,A32,FINSEQ_3:25;
then x2.m1=u`1 by A11,A18,GOBOARD1:def 1;
hence p1`1<=s by A8,A11,A18,A21,A34,A33;
end;
end;
hence p1`1<=s;
end;
len f = len f1 + len f2 by FINSEQ_1:22;
then 2+2<=len f by A1,A2,XREAL_1:7;
then 1<=len f by XXREAL_0:2;
then
A35: 1 in dom f by FINSEQ_3:25;
then x.1=p1`1 by A16,A17,A15,GOBOARD1:def 1;
then
A36: f/.1 in rng Line(G,1) by A35,A22,GOBOARD2:15;
A37: len f1 in dom f1 by A13,FINSEQ_3:25;
then
A38: f/.len f1=f1/.len f1 by FINSEQ_4:68;
A39: x1.(len f1) = p2`1 by A12,A20,A37,GOBOARD1:def 1;
A40: now
let m;
set s = x.m;
assume
A41: m in dom f;
then
A42: m<=len f by FINSEQ_3:25;
A43: 1<=m by A41,FINSEQ_3:25;
now
per cases;
suppose
A44: m<=len f1;
reconsider u=f1/.m as Point of TOP-REAL 2;
A45: m in dom f1 by A43,A44,FINSEQ_3:25;
then f/.m=u by FINSEQ_4:68;
then
A46: x.m=u`1 by A16,A17,A41,GOBOARD1:def 1;
x1.m=u`1 by A12,A20,A45,GOBOARD1:def 1;
hence s<=p2`1 by A7,A12,A20,A39,A45,A46;
end;
suppose
A47: len f1<m;
then reconsider w5 = m-len f1 as Element of NAT by INT_1:5;
w5 > 0 by A47,XREAL_1:50;
then
A48: 1<=w5 by NAT_1:14;
A49: m = w5 + len f1;
then reconsider m1=m-len f1 as Nat;
reconsider u=f2/.m1 as Point of TOP-REAL 2;
A50: w5<=len f2 by A19,A42,A49,XREAL_1:6;
then f/.m = f2/.w5 by A49,A48,SEQ_4:136;
then
A51: x.m=u`1 by A16,A17,A41,GOBOARD1:def 1;
A52: m1 in dom f2 by A48,A50,FINSEQ_3:25;
then x2.m1=u`1 by A11,A18,GOBOARD1:def 1;
hence s<=p2`1 by A8,A11,A18,A39,A52,A51;
end;
end;
hence s<=p2`1;
end;
A53: dom f1 c= dom f by FINSEQ_1:26;
then x.(len f1) = p2`1 by A16,A17,A37,A38,GOBOARD1:def 1;
then
A54: f/.len f1 in rng Line(G,len G) by A53,A37,A40,GOBOARD2:16;
now
let n;
assume
A55: n in dom f1;
dom f1 c= dom f by FINSEQ_1:26;
then consider i,j such that
A56: [i,j] in Indices G & f/.n=G*(i,j) by A55,GOBOARD2:14;
take i,j;
thus [i,j] in Indices G & f1/.n=G*(i,j) by A55,A56,FINSEQ_4:68;
end;
then consider g1 such that
A57: g1 is_sequence_on G & L~g1=L~f1 & g1/.1=f1/.1 & g1/.len g1=f1/.len f1 and
A58: len f1 <= len g1 by A3,A5,GOBOARD2:12;
now
let n;
assume
A59: n in dom f2;
then len f1+n in dom f by FINSEQ_1:28;
then consider i,j such that
A60: [i,j] in Indices G & f/.(len f1+n)=G*(i,j) by GOBOARD2:14;
take i,j;
thus [i,j] in Indices G & f2/.n=G*(i,j) by A59,A60,FINSEQ_4:69;
end;
then consider g2 such that
A61: g2 is_sequence_on G & L~g2=L~f2 & g2/.1=f2/.1 & g2/.len g2=f2/.len f2 and
A62: len f2 <= len g2 by A4,A6,GOBOARD2:12;
A63: 2<=len g2 by A2,A62,XXREAL_0:2;
A64: 1<=len f2 by A2,XXREAL_0:2;
then
A65: 1 in dom f2 by FINSEQ_3:25;
then
A66: f/.(len f1+1)=f2/.1 by FINSEQ_4:69;
A67: Seg len y = dom y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
A68: Seg len y1=dom y1 & len y1=len f1 by FINSEQ_1:def 3,GOBOARD1:def 2;
A69: Seg len y2=dom y2 & len y2=len f2 by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A70: y2.1=q1`2 by A11,A65,GOBOARD1:def 2;
A71: now
let m;
set s = y.m;
assume
A72: m in dom f;
then
A73: m<=len f by FINSEQ_3:25;
A74: 1<=m by A72,FINSEQ_3:25;
now
per cases;
suppose
A75: m<=len f1;
reconsider u=f1/.m as Point of TOP-REAL 2;
A76: m in dom f1 by A74,A75,FINSEQ_3:25;
then f/.m=u by FINSEQ_4:68;
then
A77: y.m=u`2 by A16,A67,A72,GOBOARD1:def 2;
y1.m=u`2 by A12,A68,A76,GOBOARD1:def 2;
hence q1`2<=s by A9,A12,A68,A70,A76,A77;
end;
suppose
A78: len f1<m;
then reconsider w5 = m-len f1 as Element of NAT by INT_1:5;
w5 > 0 by A78,XREAL_1:50;
then
A79: 1<=w5 by NAT_1:14;
A80: m = w5 + len f1;
then reconsider m1=m-len f1 as Nat;
reconsider u=f2/.m1 as Point of TOP-REAL 2;
A81: w5<=len f2 by A19,A73,A80,XREAL_1:6;
then f/.m = f2/.w5 by A80,A79,SEQ_4:136;
then
A82: y.m=u`2 by A16,A67,A72,GOBOARD1:def 2;
A83: m1 in dom f2 by A79,A81,FINSEQ_3:25;
then y2.m1=u`2 by A11,A69,GOBOARD1:def 2;
hence q1`2<=s by A10,A11,A69,A70,A83,A82;
end;
end;
hence q1`2<=s;
end;
A84: len f1+1 in dom f by A65,FINSEQ_1:28;
then y.(len f1+1)=q1`2 by A16,A67,A66,GOBOARD1:def 2;
then
A85: f/.(len f1+1) in rng Col(G,1) by A84,A71,GOBOARD2:17;
A86: len f2 in dom f2 by A64,FINSEQ_3:25;
then
A87: f/.(len f1+len f2)=f2/.len f2 by FINSEQ_4:69;
A88: y2.(len f2)=q2`2 by A11,A69,A86,GOBOARD1:def 2;
A89: now
let m;
set s = y.m;
assume
A90: m in dom f;
then
A91: m<=len f by FINSEQ_3:25;
A92: 1<=m by A90,FINSEQ_3:25;
now
per cases;
suppose
A93: m<=len f1;
reconsider u=f1/.m as Point of TOP-REAL 2;
A94: m in dom f1 by A92,A93,FINSEQ_3:25;
then f/.m=u by FINSEQ_4:68;
then
A95: y.m=u`2 by A16,A67,A90,GOBOARD1:def 2;
y1.m=u`2 by A12,A68,A94,GOBOARD1:def 2;
hence s<=q2`2 by A9,A12,A68,A88,A94,A95;
end;
suppose
A96: len f1<m;
then reconsider w5 = m-len f1 as Element of NAT by INT_1:5;
w5 > 0 by A96,XREAL_1:50;
then
A97: 1<=w5 by NAT_1:14;
A98: m = w5 + len f1;
then reconsider m1=m-len f1 as Nat;
reconsider u=f2/.m1 as Point of TOP-REAL 2;
A99: w5<=len f2 by A19,A91,A98,XREAL_1:6;
then f/.m = f2/.w5 by A98,A97,SEQ_4:136;
then
A100: y.m=u`2 by A16,A67,A90,GOBOARD1:def 2;
A101: m1 in dom f2 by A97,A99,FINSEQ_3:25;
then y2.m1=u`2 by A11,A69,GOBOARD1:def 2;
hence s<=q2`2 by A10,A11,A69,A88,A101,A100;
end;
end;
hence s<=q2`2;
end;
A102: len f1+len f2 in dom f by A86,FINSEQ_1:28;
then y.(len f1+len f2)=q2`2 by A16,A67,A87,GOBOARD1:def 2;
then
A103: f/.(len f1+len f2) in rng Col(G,width G) by A102,A89,GOBOARD2:18;
2<=len g1 by A1,A58,XXREAL_0:2;
hence thesis by A57,A61,A15,A38,A66,A87,A36,A54,A85,A103,A63,Th2;
end;
theorem Th5:
for f1,f2 being FinSequence of TOP-REAL 2 st f1 is one-to-one
special & 2 <= len f1 & f2 is one-to-one special & 2 <= len f2 & X_axis(f1)
lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) & X_axis(f2) lies_between (
X_axis(f1)).1, (X_axis(f1)).(len f1) & Y_axis(f1) lies_between (Y_axis(f2)).1,
(Y_axis(f2)).(len f2) & Y_axis(f2) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(
len f2) holds L~f1 meets L~f2
proof
let f1,f2 be FinSequence of TOP-REAL 2;
assume that
A1: f1 is one-to-one special and
A2: 2 <= len f1 and
A3: f2 is one-to-one special and
A4: 2 <= len f2 & X_axis(f1) lies_between (X_axis(f1)).1, (X_axis(f1)).(
len f1 ) & X_axis(f2) lies_between (X_axis(f1)).1, (X_axis(f1)).(len f1) &
Y_axis ( f1) lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2) & Y_axis(f2)
lies_between (Y_axis(f2)).1, (Y_axis(f2)).(len f2);
A5: for n st n in dom f2 & n+1 in dom f2 holds f2/.n <> f2/.(n+1)
proof
let n;
assume n in dom f2 & n+1 in dom f2 & f2/.n=f2/.(n+1);
then n=n+1 by A3,PARTFUN2:10;
hence contradiction;
end;
for n st n in dom f1 & n+1 in dom f1 holds f1/.n <> f1/.(n+1)
proof
let n;
assume n in dom f1 & n+1 in dom f1 & f1/.n=f1/.(n+1);
then n=n+1 by A1,PARTFUN2:10;
hence contradiction;
end;
hence thesis by A1,A2,A3,A4,A5,Th4;
end;
theorem
for P1,P2,p1,p2,q1,q2 st P1 is_S-P_arc_joining p1,q1 & P2
is_S-P_arc_joining p2,q2 & (for p st p in P1 \/ P2 holds p1`1<=p`1 & p`1<=q1`1)
& (for p st p in P1 \/ P2 holds p2`2<=p`2 & p`2<=q2`2) holds P1 meets P2
proof
let P1,P2,p1,p2,q1,q2;
assume that
A1: P1 is_S-P_arc_joining p1,q1 and
A2: P2 is_S-P_arc_joining p2,q2 and
A3: for p st p in P1 \/ P2 holds p1`1<=p`1 & p`1<=q1`1 and
A4: for p st p in P1 \/ P2 holds p2`2<=p`2 & p`2<=q2`2;
consider f1 such that
A5: f1 is being_S-Seq and
A6: P1=L~f1 and
A7: p1=f1/.1 and
A8: q1=f1/.len f1 by A1,TOPREAL4:def 1;
len f1 <> 0 by A5,TOPREAL1:def 8;
then reconsider f1 as non empty FinSequence of TOP-REAL 2;
A9: Seg len f1=dom f1 by FINSEQ_1:def 3;
consider f2 such that
A10: f2 is being_S-Seq and
A11: P2=L~f2 and
A12: p2=f2/.1 and
A13: q2=f2/.len f2 by A2,TOPREAL4:def 1;
len f2 <> 0 by A10,TOPREAL1:def 8;
then reconsider f2 as non empty FinSequence of TOP-REAL 2;
A14: Seg len f2=dom f2 by FINSEQ_1:def 3;
set x1 = X_axis(f1), y1 = Y_axis(f1), x2 = X_axis(f2), y2 = Y_axis(f2);
A15: Seg len x1=dom x1 & len x1= len f1 by FINSEQ_1:def 3,GOBOARD1:def 1;
A16: dom y2=Seg len y2 & len y2=len f2 by FINSEQ_1:def 3,GOBOARD1:def 2;
A17: 2<=len f2 by A10,TOPREAL1:def 8;
then
A18: 1<=len f2 by XXREAL_0:2;
then 1 in dom f2 by FINSEQ_3:25;
then
A19: y2.1=p2`2 by A12,A14,A16,GOBOARD1:def 2;
len f2 in dom f2 by A18,FINSEQ_3:25;
then
A20: y2.(len f2)=q2`2 by A13,A14,A16,GOBOARD1:def 2;
A21: y2 lies_between y2.1, y2.len f2
proof
let n;
set q = f2/.n;
assume
A22: n in dom y2;
then q in L~f2 by A17,A14,A16,GOBOARD1:1;
then
A23: q in P1 \/ P2 by A11,XBOOLE_0:def 3;
y2.n=q`2 by A22,GOBOARD1:def 2;
hence thesis by A4,A19,A20,A23;
end;
A24: 2<=len f1 by A5,TOPREAL1:def 8;
then
A25: 1<=len f1 by XXREAL_0:2;
then 1 in dom f1 by FINSEQ_3:25;
then
A26: x1.1=p1`1 by A7,A9,A15,GOBOARD1:def 1;
len f1 in dom f1 by A25,FINSEQ_3:25;
then
A27: x1.(len f1)=q1`1 by A8,A9,A15,GOBOARD1:def 1;
A28: x1 lies_between x1.1, x1.len f1
proof
let n;
set q=f1/.n;
assume
A29: n in dom x1;
then q in L~f1 by A24,A9,A15,GOBOARD1:1;
then
A30: q in P1 \/ P2 by A6,XBOOLE_0:def 3;
x1.n=q`1 by A29,GOBOARD1:def 1;
hence thesis by A3,A26,A27,A30;
end;
A31: dom x2=Seg len x2 & len x2=len f2 by FINSEQ_1:def 3,GOBOARD1:def 1;
A32: x2 lies_between x1.1, x1.len f1
proof
let n;
set q=f2/.n;
assume
A33: n in dom x2;
then q in L~f2 by A17,A14,A31,GOBOARD1:1;
then
A34: q in P1 \/ P2 by A11,XBOOLE_0:def 3;
x2.n=q`1 by A33,GOBOARD1:def 1;
hence thesis by A3,A26,A27,A34;
end;
A35: dom y1=Seg len y1 & len y1=len f1 by FINSEQ_1:def 3,GOBOARD1:def 2;
A36: y1 lies_between y2.1, y2.len f2
proof
let n;
set q=f1/.n;
assume
A37: n in dom y1;
then q in L~f1 by A24,A9,A35,GOBOARD1:1;
then
A38: q in P1 \/ P2 by A6,XBOOLE_0:def 3;
y1.n=q`2 by A37,GOBOARD1:def 2;
hence thesis by A4,A19,A20,A38;
end;
A39: f2 is one-to-one special by A10,TOPREAL1:def 8;
f1 is one-to-one special by A5,TOPREAL1:def 8;
hence thesis by A6,A11,A39,A24,A17,A28,A32,A36,A21,Th5;
end;