:: Go-Board Theorem
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2019 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 jmi 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 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: mi1;
1<=mi by A39,FINSEQ_3:25;
then 1len G1;
ma<=len G1 by A41,FINSEQ_3:25;
then ma {};
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 {} 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 {} 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 00;
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 w+k by A39,A41,A46,A95,A459,A462,
GOBOARD1:3;
then ma1 pf by A39,A41,A95,A359,A363,GOBOARD1:3;
now
per cases by A488,XXREAL_0:1;
suppose
pfpl;
then pl {};
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 1len G1;
ma<=len G1 by A41,FINSEQ_3:25;
then ma {} 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 {};
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 1len G1;
ma<=len G1 by A41,FINSEQ_3:25;
then ma {} 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
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 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 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 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 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;