:: Introduction to Go-Board - Part I. Basic Notations
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, PRE_TOPC, EUCLID, FINSEQ_1, REAL_1, SUBSET_1, COMPLEX1,
ARYTM_1, XXREAL_0, ARYTM_3, CARD_1, NAT_1, RELAT_1, FINSEQ_3, FUNCT_1,
XBOOLE_0, TARSKI, ORDINAL2, PARTFUN1, MCART_1, TOPREAL1, RLTOPSP1,
MATRIX_1, TREES_1, INCSP_1, ZFMISC_1, ORDINAL4, GOBOARD1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XXREAL_0, COMPLEX1, NAT_1,
VALUED_0, FINSEQ_1, FINSEQ_3, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1,
MATRIX_0, MATRIX_1;
constructors PARTFUN1, XXREAL_0, NAT_1, COMPLEX1, MATRIX_1, TOPREAL1, SEQM_3,
RELSET_1, REAL_1, MATRIX_0;
registrations RELAT_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1,
STRUCT_0, EUCLID, VALUED_0, INT_1;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, SEQM_3;
equalities XBOOLE_0;
expansions XBOOLE_0, SEQM_3;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, FINSEQ_2,
FINSEQ_3, MATRIX_0, TOPREAL1, TOPREAL3, FINSEQ_4, RELAT_1, INT_1,
PARTFUN2, XBOOLE_0, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, PARTFUN1,
SEQM_3, XREAL_0;
schemes NAT_1, FINSEQ_1, FINSEQ_4;
begin
reserve p for Point of TOP-REAL 2,
f,f1,f2,g for FinSequence of TOP-REAL 2,
v, v1,v2 for FinSequence of REAL,
r,s for Real,
n,m,i,j,k for Nat,
x for set;
definition
let f;
func X_axis(f) -> FinSequence of REAL means
:Def1:
len it = len f & for n st n in dom it holds it.n = (f/.n)`1;
existence
proof
defpred P[Nat,set] means $2 = (f/.$1)`1;
A1: for k be Nat st k in Seg len f ex r being Element of REAL st P[k,r]
proof let k be Nat;
(f/.k)`1 in REAL by XREAL_0:def 1;
hence thesis;
end;
consider v such that
A2: dom v = Seg len f and
A3: for k be Nat st k in Seg len f holds P[k,v.k] from FINSEQ_1:sch 5(A1);
take v;
thus len v = len f by A2,FINSEQ_1:def 3;
let n;
assume n in dom v;
hence thesis by A2,A3;
end;
uniqueness
proof
let v1,v2;
assume that
A4: len v1 = len f and
A5: for n st n in dom v1 holds v1.n = (f/.n)`1 and
A6: len v2 = len f and
A7: for n st n in dom v2 holds v2.n = (f/.n)`1;
A8: dom v2 = Seg len v2 by FINSEQ_1:def 3;
A9: dom f = Seg len f by FINSEQ_1:def 3;
A10: dom v1 = Seg len v1 by FINSEQ_1:def 3;
now
let n be Nat;
assume
A11: n in (dom f);
hence v1.n = (f/.n)`1 by A4,A5,A10,A9
.= v2.n by A6,A7,A8,A9,A11;
end;
hence thesis by A4,A6,A10,A8,A9,FINSEQ_1:13;
end;
func Y_axis(f) -> FinSequence of REAL means
:Def2:
len it = len f & for n st n in dom it holds it.n = (f/.n)`2;
existence
proof
defpred P[Nat,set] means $2 = (f/.$1)`2;
A12: for k be Nat st k in Seg len f ex r being Element of REAL st P[k,r]
proof let k be Nat;
(f/.k)`2 in REAL by XREAL_0:def 1;
hence thesis;
end;
consider v such that
A13: dom v = Seg len f and
A14: for k be Nat st k in Seg len f holds P[k,v.k] from FINSEQ_1:sch 5(A12);
take v;
thus len v = len f by A13,FINSEQ_1:def 3;
let n;
assume n in dom v;
hence thesis by A13,A14;
end;
uniqueness
proof
let v1,v2;
assume that
A15: len v1 = len f and
A16: for n st n in dom v1 holds v1.n = (f/.n)`2 and
A17: len v2 = len f and
A18: for n st n in dom v2 holds v2.n = (f/.n)`2;
A19: dom v2 = Seg len v2 by FINSEQ_1:def 3;
A20: dom f = Seg len f by FINSEQ_1:def 3;
A21: dom v1 = Seg len v1 by FINSEQ_1:def 3;
now
let n be Nat;
assume
A22: n in (dom f);
hence v1.n = (f/.n)`2 by A15,A16,A21,A20
.= v2.n by A17,A18,A19,A20,A22;
end;
hence thesis by A15,A17,A21,A19,A20,FINSEQ_1:13;
end;
end;
theorem Th1:
i in dom f & 2<=len f implies f/.i in L~f
proof
assume that
A1: i in dom f and
A2: 2<=len f;
A3: 1<=i by A1,FINSEQ_3:25;
A4: i<=len f by A1,FINSEQ_3:25;
per cases by A4,XXREAL_0:1;
suppose
A5: i=len f;
reconsider l=i-1 as Element of NAT by A3,INT_1:5;
1+1<=i by A2,A5;
then 1<=l by XREAL_1:19;
then
A6: f/.(l+1) in LSeg(f,l) by A4,TOPREAL1:21;
LSeg(f,l) c=L~f by TOPREAL3:19;
hence thesis by A6;
end;
suppose
i<len f;
then i+1<=len f by NAT_1:13;
then
A7: f/.i in LSeg(f,i) by A3,TOPREAL1:21;
LSeg(f,i) c= L~f by TOPREAL3:19;
hence thesis by A7;
end;
end;
begin
:: Matrix preliminaries
definition
::$CD
let M be Matrix of TOP-REAL 2;
attr M is X_equal-in-line means
:Def3:
for n st n in dom M holds X_axis(Line (M,n)) is constant;
attr M is Y_equal-in-column means
:Def4:
for n st n in Seg width M holds Y_axis(Col(M,n)) is constant;
attr M is Y_increasing-in-line means
:Def5:
for n st n in dom M holds Y_axis (Line(M,n)) is increasing;
attr M is X_increasing-in-column means
:Def6:
for n st n in Seg width M holds X_axis(Col(M,n)) is increasing;
end;
registration
cluster non empty-yielding X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column for Matrix of TOP-REAL 2;
existence
proof
set p = the Point of TOP-REAL 2;
take M = <* <*p*> *>;
A1: len M=1 by MATRIX_0:24;
A2: width M=1 by MATRIX_0:24;
hence M is non empty-yielding by A1,MATRIX_0:def 10;
thus M is X_equal-in-line
proof
let n such that
n in dom M;
set L = X_axis(Line(M,n));
let k; let m be Nat;
assume that
A3: k in dom L and
A4: m in dom L;
A5: len L = len Line(M,n) by Def1;
k in Seg len L by A3,FINSEQ_1:def 3;
then k in {1} by A2,A5,FINSEQ_1:2,MATRIX_0:def 7;
then
A6: k = 1 by TARSKI:def 1;
m in Seg len L by A4,FINSEQ_1:def 3;
then m in {1} by A2,A5,FINSEQ_1:2,MATRIX_0:def 7;
hence L.k = L.m by A6,TARSKI:def 1;
end;
thus M is Y_equal-in-column
proof
let n such that
n in Seg width M;
set L = Y_axis(Col(M,n));
let k,m;
assume that
A7: k in dom L and
A8: m in dom L;
A9: len L = len Col(M,n) by Def2;
k in Seg len L by A7,FINSEQ_1:def 3;
then k in {1} by A1,A9,FINSEQ_1:2,MATRIX_0:def 8;
then
A10: k = 1 by TARSKI:def 1;
m in Seg len L by A8,FINSEQ_1:def 3;
then m in {1} by A1,A9,FINSEQ_1:2,MATRIX_0:def 8;
hence L.k = L.m by A10,TARSKI:def 1;
end;
thus M is Y_increasing-in-line
proof
let n such that
n in dom M;
set L = Y_axis(Line(M,n));
let k,m;
assume that
A11: k in dom L and
A12: m in dom L and
A13: k<m;
A14: len L = len Line(M,n) by Def2;
k in Seg len L by A11,FINSEQ_1:def 3;
then k in {1} by A2,A14,FINSEQ_1:2,MATRIX_0:def 7;
then
A15: k = 1 by TARSKI:def 1;
m in Seg len L by A12,FINSEQ_1:def 3;
then m in {1} by A2,A14,FINSEQ_1:2,MATRIX_0:def 7;
hence thesis by A13,A15,TARSKI:def 1;
end;
let n such that
n in Seg width M;
set L = X_axis(Col(M,n));
let k,m;
assume that
A16: k in dom L and
A17: m in dom L and
A18: k<m;
A19: len L = len Col(M,n) by Def1;
k in Seg len L by A16,FINSEQ_1:def 3;
then k in {1} by A1,A19,FINSEQ_1:2,MATRIX_0:def 8;
then
A20: k = 1 by TARSKI:def 1;
m in Seg len L by A17,FINSEQ_1:def 3;
then m in {1} by A1,A19,FINSEQ_1:2,MATRIX_0:def 8;
hence thesis by A18,A20,TARSKI:def 1;
end;
end;
::$CT
theorem Th2:
for M being X_increasing-in-column X_equal-in-line Matrix of
TOP-REAL 2 holds for x,n,m st x in rng Line(M,n) & x in rng Line(M,m) & n in
dom M & m in dom M holds n=m
proof
let M be X_increasing-in-column X_equal-in-line Matrix of TOP-REAL 2;
assume not thesis;
then consider x,n,m such that
A1: x in rng Line(M,n) and
A2: x in rng Line(M,m) and
A3: n in dom M and
A4: m in dom M and
A5: n<>m;
A6: n < m or m < n by A5,XXREAL_0:1;
A7: X_axis(Line(M,m)) is constant by A4,Def3;
reconsider Ln = Line(M,n), Lm = Line(M,m) as FinSequence of TOP-REAL 2;
consider i being Nat such that
A8: i in dom Ln and
A9: Ln.i = x by A1,FINSEQ_2:10;
set C = X_axis(Col(M,i));
A10: len Ln = width M by MATRIX_0:def 7;
reconsider Mi = Col(M,i) as FinSequence of TOP-REAL 2;
A11: Col(M,i).n = M*(n,i) by A3,MATRIX_0:def 8;
A12: len Col(M,i) = len M by MATRIX_0:def 8;
then n in dom(Col(M,i)) by A3,FINSEQ_3:29;
then
A13: M*(n,i) = Mi/.n by A11,PARTFUN1:def 6;
A14: Col(M,i).m = M*(m,i) by A4,MATRIX_0:def 8;
A15: dom M = Seg len M by FINSEQ_1:def 3;
then m in dom(Col(M,i)) by A4,A12,FINSEQ_1:def 3;
then
A16: M*(m,i) = Mi/.m by A14,PARTFUN1:def 6;
consider j being Nat such that
A17: j in dom Lm and
A18: Lm.j = x by A2,FINSEQ_2:10;
A19: len C = len Col(M,i) & dom C=Seg len C by Def1,FINSEQ_1:def 3;
A20: Seg len Ln = dom Ln by FINSEQ_1:def 3;
then
A21: C is increasing by A8,A10,Def6;
A22: len Lm = width M by MATRIX_0:def 7;
then
A23: i in dom Lm by A8,A10,FINSEQ_3:29;
Lm.i = M*(m,i) by A8,A10,A20,MATRIX_0:def 7;
then
A24: Lm/.i = M*(m,i) by A23,PARTFUN1:def 6;
A25: dom X_axis(Lm)=Seg len X_axis(Lm) by FINSEQ_1:def 3;
Ln.i = M*(n,i) by A8,A10,A20,MATRIX_0:def 7;
then reconsider p=x as Point of TOP-REAL 2 by A9;
A26: Lm/.j = p by A17,A18,PARTFUN1:def 6;
A27: len X_axis(Lm) = len Lm by Def1;
then
A28: j in dom(X_axis(Lm)) by A17,FINSEQ_3:29;
Seg len Lm = dom Lm by FINSEQ_1:def 3;
then
A29: j in dom X_axis(Lm) by A17,A25,Def1;
i in dom(X_axis(Lm)) by A8,A10,A22,A27,FINSEQ_3:29;
then (X_axis(Lm)).i = (X_axis(Lm)).j by A7,A28;
then
A30: (M*(m,i))`1 = (X_axis(Lm)).j by A8,A25,A10,A22,A27,A20,A24,Def1
.= p`1 by A29,A26,Def1;
(M*(n,i))`1 = p`1 by A8,A9,A10,A20,MATRIX_0:def 7;
then C.n = p`1 by A3,A15,A12,A19,A13,Def1
.= C.m by A4,A15,A12,A19,A30,A16,Def1;
hence contradiction by A3,A4,A15,A21,A12,A19,A6;
end;
theorem Th3:
for M being Y_increasing-in-line Y_equal-in-column Matrix of
TOP-REAL 2 holds for x,n,m st x in rng Col(M,n) & x in rng Col(M,m) & n in Seg
width M & m in Seg width M holds n=m
proof
let M be Y_increasing-in-line Y_equal-in-column Matrix of TOP-REAL 2;
assume not thesis;
then consider x,n,m such that
A1: x in rng Col(M,n) and
A2: x in rng Col(M,m) and
A3: n in Seg width M and
A4: m in Seg width M and
A5: n<>m;
reconsider Ln = Col(M,n), Lm = Col(M,m) as FinSequence of TOP-REAL 2;
consider i being Nat such that
A6: i in dom Ln and
A7: Ln.i = x by A1,FINSEQ_2:10;
A8: len Ln=len M by MATRIX_0:def 8;
A9: len Lm=len M by MATRIX_0:def 8;
then
A10: i in dom Lm by A6,A8,FINSEQ_3:29;
set C = Y_axis(Line(M,i));
A11: Seg len Ln = dom Ln by FINSEQ_1:def 3;
A12: dom M = Seg len M by FINSEQ_1:def 3;
then
A13: C is increasing by A6,A8,A11,Def5;
Lm.i=M*(i,m) by A6,A8,A12,A11,MATRIX_0:def 8;
then
A14: Lm/.i = M*(i,m) by A10,PARTFUN1:def 6;
A15: len Y_axis(Lm) = len Lm by Def2;
consider j being Nat such that
A16: j in dom Lm and
A17: Lm.j = x by A2,FINSEQ_2:10;
A18: dom Y_axis(Lm)=Seg len Y_axis(Lm) by FINSEQ_1:def 3;
Ln.i=M*(i,n) by A6,A8,A12,A11,MATRIX_0:def 8;
then reconsider p=x as Point of TOP-REAL 2 by A7;
A19: Lm/.j = p by A16,A17,PARTFUN1:def 6;
A20: Seg len Lm = dom Lm by FINSEQ_1:def 3;
then
A21: j in dom Y_axis(Lm) by A16,A18,Def2;
Y_axis(Col(M,m)) is constant by A4,Def4;
then (Y_axis(Lm)).i = (Y_axis(Lm)).j by A6,A16,A18,A8,A9,A15,A11,A20;
then
A22: (M*(i,m))`2 = (Y_axis(Lm)).j by A6,A18,A8,A9,A15,A11,A14,Def2
.= p`2 by A21,A19,Def2;
A23: n < m or m < n by A5,XXREAL_0:1;
A24: len C = len Line(M,i) & dom C=Seg len C by Def2,FINSEQ_1:def 3;
reconsider Li = Line(M,i) as FinSequence of TOP-REAL 2;
A25: Line(M,i).m=M*(i,m) by A4,MATRIX_0:def 7;
A26: len Line(M,i) = width M by MATRIX_0:def 7;
then m in dom(Line(M,i)) by A4,FINSEQ_1:def 3;
then
A27: M*(i,m) = Li/.m by A25,PARTFUN1:def 6;
A28: Line(M,i).n=M*(i,n) by A3,MATRIX_0:def 7;
n in dom(Line(M,i)) by A3,A26,FINSEQ_1:def 3;
then
A29: M*(i,n) = Li/.n by A28,PARTFUN1:def 6;
(M*(i,n))`2 = p`2 by A6,A7,A8,A12,A11,MATRIX_0:def 8;
then C.n = p`2 by A3,A26,A24,A29,Def2
.= C.m by A4,A26,A24,A22,A27,Def2;
hence contradiction by A3,A4,A13,A26,A24,A23;
end;
begin
:: Go board
definition
mode Go-board is non empty-yielding
X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column Matrix of TOP-REAL 2;
end;
reserve G for Go-board;
theorem
x=G*(m,k) & x=G*(i,j) & [m,k] in Indices G & [i,j] in Indices G
implies m=i & k=j
proof
assume that
A1: x=G*(m,k) and
A2: x=G*(i,j) and
A3: [m,k] in Indices G and
A4: [i,j] in Indices G;
A5: len Line(G,m)=width G & dom Line(G,m)=Seg len Line(G,m) by FINSEQ_1:def 3
,MATRIX_0:def 7;
A6: Indices G=[:dom G,Seg width G:] by MATRIX_0:def 4;
then
A7: k in Seg width G by A3,ZFMISC_1:87;
then x=Line(G,m).k by A1,MATRIX_0:def 7;
then
A8: x in rng Line(G,m) by A7,A5,FUNCT_1:def 3;
A9: len Col(G,k)=len G & dom Col(G,k)=Seg len Col(G,k) by FINSEQ_1:def 3
,MATRIX_0:def 8;
A10: len Line(G,i)=width G & dom Line(G,i)=Seg len Line(G,i) by FINSEQ_1:def 3
,MATRIX_0:def 7;
A11: len Col(G,j)=len G & dom Col(G,j)=Seg len Col(G,j) by FINSEQ_1:def 3
,MATRIX_0:def 8;
A12: dom G = Seg len G by FINSEQ_1:def 3;
A13: j in Seg width G by A4,A6,ZFMISC_1:87;
then x=Line(G,i).j by A2,MATRIX_0:def 7;
then
A14: x in rng Line(G,i) by A13,A10,FUNCT_1:def 3;
A15: i in dom G by A4,A6,ZFMISC_1:87;
then x=Col(G,j).i by A2,MATRIX_0:def 8;
then
A16: x in rng Col(G,j) by A15,A12,A11,FUNCT_1:def 3;
A17: m in dom G by A3,A6,ZFMISC_1:87;
then x=Col(G,k).m by A1,MATRIX_0:def 8;
then x in rng Col(G,k) by A17,A12,A9,FUNCT_1:def 3;
hence thesis by A17,A15,A7,A13,A8,A14,A16,Th2,Th3;
end;
::$CT 3
registration
let G;
let i be Nat;
cluster DelCol(G,i) -> X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column;
coherence
proof
per cases;
suppose not i in Seg width G;
then DelCol(G,i) = G by MATRIX_0:61;
hence thesis;
end;
suppose
A1: i in Seg width G;
0 < len G & 0 < width G by MATRIX_0:44;
then consider m being Nat such that
A2: width G = m+1 by NAT_1:6;
reconsider m as Element of NAT by ORDINAL1:def 12;
set M = DelCol(G,i);
A3: width DelCol(G,i) = m by A1,A2,MATRIX_0:63;
then
A4: len M = len G & width M = m by MATRIX_0:def 13;
then
A5: dom G = dom M by FINSEQ_3:29;
then
A6: Indices M = [:dom G, Seg m:] by A4,MATRIX_0:def 4;
A7: for k,j st k in dom G & j in Seg m holds M*(k,j)=Del(Line(G,k),i).j
proof
let k,j;
assume
A8: k in dom G & j in Seg m;
then
A9: M.k=Del(Line(G,k),i) by MATRIX_0:def 13;
[k,j] in Indices M by A6,A8,ZFMISC_1:87;
then ex p being FinSequence of TOP-REAL 2 st p = M.k & M*(k,j) = p.j
by MATRIX_0:def 5;
hence thesis by A9;
end;
A10: for k,j st k in dom G & j in Seg m holds
M*(k,j)=Line(G,k).j or M*(k,j)=Line(G,k).(j+1)
proof
let k,j;
assume
A11: k in dom G & j in Seg m;
then
A12: M*(k,j)=Del(Line(G,k),i).j by A7;
A13: len Line(G,k) = m+1 by A2,MATRIX_0:def 7;
i in Seg len Line(G,k) by A1,MATRIX_0:def 7;
then i in dom Line(G,k) by FINSEQ_1:def 3;
hence thesis by A11,A12,A13,SEQM_3:44;
end;
set N=M;
A14: for k st k in Seg m holds Col(N,k)=Col(G,k) or Col(N,k)=Col(G,k+1)
proof
let k;
assume
A15: k in Seg m;
then
A16: 1<=k & k<=m by FINSEQ_1:1;
m<=m+1 & k<=k+1 by NAT_1:11;
then k<=m+1 & 1<=k+1 & k+1<=m+1 by A16,XREAL_1:6,XXREAL_0:2;
then
A17: k in Seg width G & k+1 in Seg width G by A2,A16,FINSEQ_1:1;
A18: len Col(N,k) = len N & len Col(G,k)=len G &
len Col(G,k+1) = len G by MATRIX_0:def 8;
now per cases;
suppose
A19: k<i;
now
let j be Nat;
assume 1<=j & j<=len Col(N,k);
then
A20: j in dom N by A18,FINSEQ_3:25;
hence Col(N,k).j= N*(j,k) by MATRIX_0:def 8
.= Del(Line(G,j),i).k by A7,A15,A20,A5
.= Line(G,j).k by A19,FINSEQ_3:110
.= Col(G,k).j by A17,A20,A5,MATRIX_0:42;
end;
hence thesis by A4,A18,FINSEQ_1:14;
end;
suppose
A21: k>=i;
now
let j be Nat;
assume 1<=j & j<=len Col(N,k);
then
A22: j in dom N by A18,FINSEQ_3:25;
A23: len Line(G,j) = m+1 by A2,MATRIX_0:def 7;
A24: dom Line(G,j) = Seg len Line(G,j) by FINSEQ_1:def 3;
thus Col(N,k).j= N*(j,k) by A22,MATRIX_0:def 8
.= Del(Line(G,j),i).k by A7,A15,A22,A5
.= Line(G,j).(k+1) by A2,A16,A21,A23,A24,A1,FINSEQ_3:111
.= Col(G,k+1).j by A17,A22,A5,MATRIX_0:42;
end;
hence thesis by A4,A18,FINSEQ_1:14;
end;
end;
hence thesis;
end;
thus M is X_equal-in-line
proof
let k;
assume
A25: k in dom M;
then
A26: X_axis(Line(G,k)) is constant by Def3,A5;
m<=m+1 by NAT_1:11;
then
A27: Seg m c= Seg width G by A2,FINSEQ_1:5;
reconsider L = Line(M,k), lg = Line(G,k) as FinSequence of TOP-REAL 2;
set X = X_axis(L), xg = X_axis(lg);
now
let n,j be Nat such that
A28: n in dom X & j in dom X;
A29: dom X = Seg len X & len X = len L & len L = width M &
dom xg = Seg len xg & len xg = len lg & len lg = width G
by Def1,FINSEQ_1:def 3,MATRIX_0:def 7;
then
A30: L.n = M*(k,n) & L.j=M*(k,j) & n in Seg m & j in Seg m
by A28,A3,MATRIX_0:def 7;
then
A31: (L.n=lg.n or L.n=lg.(n+1)) & (L.j=lg.j or L.j=lg.(j+1))
by A10,A25,A5;
n in dom L & j in dom L by A28,A29,FINSEQ_1:def 3;
then L.n = L/.n & L.j = L/.j by PARTFUN1:def 6;
then
A32: X.n = M*(k,n)`1 & X.j=M*(k,j)`1 by A28,A30,Def1;
1<=n & n<=m & 1<=j & j<=m by A4,A28,A29,FINSEQ_3:25;
then
A33: n<=n+1 & n+1<=m+1 & j<=j+1 & j+1<=m+1 by NAT_1:11,XREAL_1:6;
1<=n+1 & 1<=j+1 by NAT_1:11;
then
A34: n+1 in Seg width G & j+1 in Seg width G &
n in Seg width G & j in Seg width G
by A2,A4,A27,A28,A29,A33,FINSEQ_3:25;
then
A35: lg.n=G*(k,n) & lg.(n+1)=G*(k,n+1) & lg.j=G*(k,j) &
lg.(j+1)=G*(k,j+1) by MATRIX_0:def 7;
dom lg = Seg len xg by A29,FINSEQ_1:def 3;
then lg.n = lg/.n & lg.(n+1) = lg/.(n+1) &
lg.j = lg/.j & lg.(j+1) = lg/.(j+1) by A29,A34,PARTFUN1:def 6;
then xg.n=G*(k,n)`1 & xg.(n+1)=G*(k,n+1)`1 & xg.j=G*(k,j)`1 &
xg.(j+1)=G*(k,j+1)`1 by A29,A34,A35,Def1;
hence X.n = X.j by A26,A29,A30,A31,A32,A34,A35;
end;
hence X_axis(Line(M,k)) is constant;
end;
thus M is Y_equal-in-column
proof
let k;
assume
A36: k in Seg width M;
then
A37: Col(M,k)=Col(G,k) or Col(M,k)=Col(G,k+1) by A4,A14;
A38: 1<=k & k<=m by A4,A36,FINSEQ_1:1;
m<=m+1 & k<=k+1 by NAT_1:11;
then k<=m+1 & 1<=k+1 & k+1<=m+1 by A38,XREAL_1:6,XXREAL_0:2;
then k in Seg width G & k+1 in Seg width G by A2,A38,FINSEQ_1:1;
hence Y_axis(Col(M,k)) is constant by A37,Def4;
end;
thus M is Y_increasing-in-line
proof
let k;
reconsider L = Line(M,k), lg = Line(G,k) as FinSequence of TOP-REAL 2;
set X = Y_axis(L), xg = Y_axis(lg);
m<=m+1 by NAT_1:11;
then
A39: Seg m c= Seg width G by A2,FINSEQ_1:5;
assume
A40: k in dom M;
then
A41: xg is increasing by Def5,A5;
now
let n,j such that
A42: n in dom X & j in dom X & n<j;
A43: dom X = Seg len X & len X = len L & len L = width M &
dom xg = Seg len xg & len xg = len lg & len lg = width G
by Def2,FINSEQ_1:def 3,MATRIX_0:def 7;
then
A44: L.n = M*(k,n) & L.j=M*(k,j) & n in Seg m & j in Seg m
by A42,A3,MATRIX_0:def 7;
dom L = Seg len X by A43,FINSEQ_1:def 3;
then L.n = L/.n & L.j = L/.j by A42,A43,PARTFUN1:def 6;
then
A45: X.n = M*(k,n)`2 & X.j=M*(k,j)`2 by A42,A44,Def2;
A46: 1<=n & n<=m & 1<=j & j<=m by A4,A42,A43,FINSEQ_3:25;
then
A47: n<=n+1 & n+1<=m+1 & j<=j+1 & j+1<=m+1 by NAT_1:11,XREAL_1:6;
1<=n+1 & 1<=j+1 by NAT_1:11;
then
A48: n+1 in Seg width G & j+1 in Seg width G &
n in Seg width G & j in Seg width G
by A2,A4,A39,A42,A43,A47,FINSEQ_3:25;
then
A49: lg.n=G*(k,n) & lg.(n+1)=G*(k,n+1) & lg.j=G*(k,j) &
lg.(j+1)=G*(k,j+1) by MATRIX_0:def 7;
dom lg = Seg len xg by A43,FINSEQ_1:def 3;
then lg.n = lg/.n & lg.(n+1) = lg/.(n+1) &
lg.j = lg/.j & lg.(j+1) = lg/.(j+1) by A43,A48,PARTFUN1:def 6;
then
A50: xg.n=G*(k,n)`2 & xg.(n+1)=G*(k,n+1)`2 & xg.j=G*(k,j)`2 &
xg.(j+1)=G*(k,j+1)`2 by A43,A48,A49,Def2;
set r = X.n, s = X.j;
A51: dom lg = Seg len lg by FINSEQ_1:def 3;
per cases;
suppose
A52: j<i;
then
A53: n<i by A42,XXREAL_0:2;
A54: M*(k,n) = (Del(lg,i)).n by A4,A7,A40,A42,A43,A5
.= G*(k,n) by A49,A53,FINSEQ_3:110;
M*(k,j) = (Del(lg,i)).j by A4,A7,A40,A42,A43,A5
.= G*(k,j) by A49,A52,FINSEQ_3:110;
hence r < s by A4,A39,A41,A42,A43,A45,A50,A54;
end;
suppose
A55: j>=i;
A56: M*(k,j) = (Del(lg,i)).j by A4,A7,A40,A42,A43,A5
.= G*(k,j+1) by A2,A43,A46,A49,A51,A55,A1,FINSEQ_3:111;
now per cases;
suppose
A57: n<i;
j<=j+1 by NAT_1:11;
then
A58: n<j+1 by A42,XXREAL_0:2;
M*(k,n) = (Del(lg,i)).n by A4,A7,A40,A42,A43,A5
.= G*(k,n) by A49,A57,FINSEQ_3:110;
hence r < s by A41,A43,A45,A48,A50,A56,A58;
end;
suppose
A59: n>=i;
A60: n+1<j+1 by A42,XREAL_1:6;
M*(k,n) = (Del(lg,i)).n by A4,A7,A40,A42,A43,A5
.= G*(k,n+1) by A2,A43,A46,A49,A51,A59,A1,FINSEQ_3:111;
hence r < s by A41,A43,A45,A48,A50,A56,A60;
end;
end;
hence r < s;
end;
end;
hence Y_axis(Line(M,k)) is increasing;
end;
let k;
assume
A61: k in Seg width M;
then
A62: Col(M,k)=Col(G,k) or Col(M,k)=Col(G,k+1) by A4,A14;
A63: 1<=k & k<=m by A4,A61,FINSEQ_1:1;
m<=m+1 & k<=k+1 by NAT_1:11;
then k<=m+1 & 1<=k+1 & k+1<=m+1 by A63,XREAL_1:6,XXREAL_0:2;
then k in Seg width G & k+1 in Seg width G by A2,A63,FINSEQ_1:1;
hence X_axis(Col(M,k)) is increasing by A62,Def6;
end;
end;
end;
::$CT 3
theorem
i in Seg width G & width G > 1 & n in dom G & m in Seg width
DelCol(G,i) implies DelCol(G,i)*(n,m)=Del(Line(G,n),i).m by MATRIX_0:66;
theorem Th6:
i in Seg width G & width G = m+1 & m>0 & 1<=k & k<i implies Col(
DelCol(G,i),k) = Col(G,k) & k in Seg width DelCol(G,i) & k in Seg width G
by MATRIX_0:67;
theorem
i in Seg width G & width G = m+1 & m>0 & i<=k & k<=m implies Col
(DelCol(G,i),k) = Col(G,k+1) & k in Seg width DelCol(G,i) & k+1 in Seg width G
by MATRIX_0:68;
theorem Th8:
i in Seg width G & width G = m+1 & m>0 & n in dom G & 1<=k & k<i
implies DelCol(G,i)*(n,k) = G*(n,k) & k in Seg width G by MATRIX_0:69;
theorem Th9:
i in Seg width G & width G = m+1 & m>0 & n in dom G & i<=k & k<=
m implies DelCol(G,i)*(n,k) = G*(n,k+1) & k+1 in Seg width G
by MATRIX_0:70;
theorem
width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,1),k) = Col(G,k+
1) & k in Seg width DelCol(G,1) & k+1 in Seg width G by MATRIX_0:71;
theorem
width G = m+1 & m>0 & k in Seg m & n in dom G implies DelCol(G,1)*(n,k
) = G*(n,k+1) & 1 in Seg width G by MATRIX_0:72;
theorem
width G = m+1 & m>0 & k in Seg m implies Col(DelCol(G,width G),k) =
Col(G,k) & k in Seg width DelCol(G,width G) by MATRIX_0:73;
theorem Th13:
width G = m+1 & m>0 & k in Seg m & n in dom G implies k in Seg
width G & DelCol(G,width G)*(n,k) = G*(n,k) & width G in Seg width G
by MATRIX_0:74;
theorem
rng f misses rng Col(G,i) & f/.n in rng Line(G,m) & n in dom f & i in
Seg width G & m in dom G & width G>1 implies f/.n in rng Line(DelCol(G,i),m)
by MATRIX_0:75;
reserve D for set,
f for FinSequence of D,
M for Matrix of D;
definition
::$CD
let D,f,M;
pred f is_sequence_on M means
(for n st n in dom f ex i,j st [i,j] in Indices M & f/.n = M*(i,j)) &
:: rng F c= Values M
for n st n in dom f & n+1 in dom f holds
for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M &
f/.n = M*(m,k) & f/.(n+1) = M*(i,j)
holds |.m-i.|+|.k-j.| = 1;
:: zmienic na egzystencjalny, to pierwszy warunek wypadnie.
end;
theorem
(m in dom f implies 1 <= len(f|m)) &
(f is_sequence_on M implies f|m is_sequence_on M)
proof
set g=f|m;
thus m in dom f implies 1 <= len(f|m)
proof
assume m in dom f;
then 1<=m & m<=len f by FINSEQ_3:25;
hence thesis by FINSEQ_1:59;
end;
assume
A1: f is_sequence_on M;
per cases;
suppose
A2: m < 1;
m = 0 by A2,NAT_1:14;
hence thesis;
end;
suppose
m >= len f;
hence thesis by A1,FINSEQ_1:58;
end;
suppose
A3: 1 <= m & m < len f;
A4: dom g = Seg len g by FINSEQ_1:def 3;
A5: m in dom f & len g = m by A3,FINSEQ_1:59,FINSEQ_3:25;
A6: now
let n;
assume
A7: n in dom g & n+1 in dom g;
then
A8: n in dom f & n+1 in dom f by A4,A5,FINSEQ_4:71;
let i1,i2,j1,j2 be Nat;
assume
A9: [i1,i2] in Indices M & [j1,j2] in Indices M & g/.n=M*(i1,i2) &
g/.(n+ 1)=M*(j1,j2);
g/.n=f/.n & g/.(n+1)=f/.(n+1) by A4,A5,A7,FINSEQ_4:71;
hence |.i1-j1.|+|.i2-j2.| = 1 by A1,A8,A9;
end;
now
let n;
assume
A10: n in dom g;
then n in dom f by A4,A5,FINSEQ_4:71;
then consider i,j such that
A11: [i,j] in Indices M & f/.n=M*(i,j) by A1;
take i,j;
thus [i,j] in Indices M & g/.n = M*(i,j) by A4,A5,A10,A11,FINSEQ_4:71;
end;
hence thesis by A6;
end;
end;
theorem
(for n st n in dom f1 ex i,j st [i,j] in Indices M & f1/.n=M*(i,j)) &
(for n st n in dom f2 ex i,j st [i,j] in Indices M & f2/.n=M*(i,j)) implies for
n st n in dom(f1^f2) ex i,j st [i,j] in Indices M & (f1^f2)/.n=M*(i,j)
proof
assume that
A1: for n st n in dom f1 ex i,j st [i,j] in Indices M & f1/.n=M*(i,j) and
A2: for n st n in dom f2 ex i,j st [i,j] in Indices M & f2/.n=M*(i,j);
let n such that
A3: n in dom(f1^f2);
per cases by A3,FINSEQ_1:25;
suppose
A4: n in dom f1;
then consider i,j such that
A5: [i,j] in Indices M and
A6: f1/.n=M*(i,j) by A1;
take i,j;
thus [i,j] in Indices M by A5;
thus thesis by A4,A6,FINSEQ_4:68;
end;
suppose
ex m be Nat st m in dom f2 & n=len f1+m;
then consider m be Nat such that
A7: m in dom f2 and
A8: n=len f1+m;
consider i,j such that
A9: [i,j] in Indices M and
A10: f2/.m=M*(i,j) by A2,A7;
take i,j;
thus [i,j] in Indices M by A9;
thus thesis by A7,A8,A10,FINSEQ_4:69;
end;
end;
theorem
(for n st n in dom f1 & n+1 in dom f1
for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M
& f1/.n=M*(m,k) & f1/.(n+1)=M*(i,j)
holds |.m-i.|+|.k-j.|=1) &
(for n st n in dom f2 & n+1 in dom f2
for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M &
f2/.n=M*(m,k) & f2/.(n+1)=M*(i,j)
holds |.m-i.|+|.k-j.|=1) &
(for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M &
f1/.len f1=M*(m,k) & f2/.1=M*(i,j) & len f1 in dom f1 & 1 in dom f2
holds |.m-i.|+|.k-j.|=1)
implies
for n st n in dom(f1^f2) & n+1 in dom(f1^f2)
for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M &
(f1^f2)/.n =M* (m,k) & (f1^f2)/.(n+1)=M*(i,j)
holds |.m-i.|+|.k-j.|=1
proof
assume that
A1: for n st n in dom f1 & n+1 in dom f1 holds for m,k,i,j st [m,k] in
Indices M & [i,j] in Indices M & f1/.n=M*(m,k) & f1/.(n+1)=M*(i,j)
holds |.m-i.|+|.k-j.|=1 and
A2: for n st n in dom f2 & n+1 in dom f2 holds for m,k,i,j st [m,k] in
Indices M & [i,j] in Indices M & f2/.n=M*(m,k) & f2/.(n+1)=M*(i,j)
holds |.m-i.|+|.k-j.|=1 and
A3: for m,k,i,j st [m,k] in Indices M & [i,j] in Indices M & f1/.len f1=
M*(m,k) & f2/.1=M*(i,j) & len f1 in dom f1 & 1 in dom f2
holds |.m-i.|+|.k-j.|=1;
let n such that
A4: n in dom(f1^f2) and
A5: n+1 in dom(f1^f2);
let m,k,i,j such that
A6: [m,k] in Indices M & [i,j] in Indices M and
A7: (f1^f2)/.n=M*(m,k) and
A8: (f1^f2)/.(n+1)=M*(i,j);
A9: dom f1=Seg len f1 by FINSEQ_1:def 3;
per cases by A4,FINSEQ_1:25;
suppose
A10: n in dom f1;
then
A11: f1/.n=M*(m,k) by A7,FINSEQ_4:68;
now
per cases by A5,FINSEQ_1:25;
suppose
A12: n+1 in dom f1;
then f1/.(n+1)=M*(i,j) by A8,FINSEQ_4:68;
hence thesis by A1,A6,A10,A11,A12;
end;
suppose
ex m be Nat st m in dom f2 & n+1=len f1+m;
then consider mm be Nat such that
A13: mm in dom f2 and
A14: n+1=len f1+mm;
1<=mm by A13,FINSEQ_3:25;
then
A15: 0<=mm-1 by XREAL_1:48;
len f1+(mm-1)<=len f1+0 by A9,A10,A14,FINSEQ_1:1;
then
A16: mm-1=0 by A15,XREAL_1:6;
then M*(i,j)=f2/.1 & M*(m,k)=f1/.len f1 by A7,A8,A10,A13,A14,
FINSEQ_4:68,69;
hence thesis by A3,A6,A10,A13,A14,A16;
end;
end;
hence thesis;
end;
suppose
ex m be Nat st m in dom f2 & n=len f1+m;
then consider mm be Nat such that
A17: mm in dom f2 and
A18: n=len f1+mm;
A19: M*(m,k)=f2/.mm by A7,A17,A18,FINSEQ_4:69;
A20: len f1+mm+1=len f1+(mm+1);
n+1<=len(f1^f2) by A5,FINSEQ_3:25;
then len f1+mm+1<=len f1+len f2 by A18,FINSEQ_1:22;
then 1<=mm+1 & mm+1<=len f2 by A20,NAT_1:11,XREAL_1:6;
then
A21: mm+1 in dom f2 by FINSEQ_3:25;
M*(i,j)=(f1^f2)/.(len f1+(mm+1)) by A8,A18
.=f2/.(mm+1) by A21,FINSEQ_4:69;
hence thesis by A2,A6,A17,A21,A19;
end;
end;
reserve f for FinSequence of TOP-REAL 2;
theorem
f is_sequence_on G & i in Seg width G & rng f misses rng Col(G,i) &
width G > 1 implies f is_sequence_on DelCol(G,i)
proof
set D = DelCol(G,i);
assume that
A1: f is_sequence_on G and
A2: i in Seg width G and
A3: rng f misses rng Col(G,i) and
A4: width G > 1;
A5: len G = len D by MATRIX_0:def 13;
A6: Indices D = [:dom D,Seg width D:] by MATRIX_0:def 4;
A7: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
A8: dom G = Seg len G & dom D = Seg len D by FINSEQ_1:def 3;
consider M be Nat such that
A9: width G = M+1 and
A10: M>0 by A4,SEQM_3:43;
A11: width D = M by A2,A9,MATRIX_0:63;
A12: now
let n such that
A13: n in dom f & n+1 in dom f;
let i1,i2,j1,j2 be Nat;
assume that
A14: [i1,i2] in Indices D and
A15: [j1,j2] in Indices D and
A16: f/.n = D*(i1,i2) & f/.(n+1) = D*(j1,j2);
A17: i1 in dom D by A6,A14,ZFMISC_1:87;
A18: i2 in Seg width D by A6,A14,ZFMISC_1:87;
then
A19: 1<=i2 by FINSEQ_1:1;
A20: i2<=M by A11,A18,FINSEQ_1:1;
then 1<=i2+1 & i2+1<=M+1 by NAT_1:11,XREAL_1:6;
then i2+1 in Seg(M+1) by FINSEQ_1:1;
then
A21: [i1,i2+1] in Indices G by A5,A9,A8,A7,A17,ZFMISC_1:87;
A22: j1 in dom D by A6,A15,ZFMISC_1:87;
A23: j2 in Seg width D by A6,A15,ZFMISC_1:87;
then
A24: 1<=j2 by FINSEQ_1:1;
M<=M+1 by NAT_1:11;
then
A25: Seg width D c= Seg width G by A9,A11,FINSEQ_1:5;
then
A26: [j1,j2] in Indices G by A5,A8,A7,A22,A23,ZFMISC_1:87;
A27: j2<=M by A11,A23,FINSEQ_1:1;
then 1<=j2+1 & j2+1<=M+1 by NAT_1:11,XREAL_1:6;
then j2+1 in Seg(M+1) by FINSEQ_1:1;
then
A28: [j1,j2+1] in Indices G by A5,A9,A8,A7,A22,ZFMISC_1:87;
A29: [i1,i2] in Indices G by A5,A8,A7,A17,A18,A25,ZFMISC_1:87;
now
per cases;
case
i2<i & j2<i;
then f/.n=G*(i1,i2) & f/.(n+1)=G* (j1,j2) by A2,A5,A9,A10,A8,A16,A17
,A22,A19,A24,Th8;
hence |.i1-j1.|+|.i2-j2.| = 1 by A1,A13,A29,A26;
end;
case
A30: i<=i2 & j2<i;
i2<=i2+1 by NAT_1:11;
then i<=i2+1 by A30,XXREAL_0:2;
then
A31: j2<i2+1 by A30,XXREAL_0:2;
then j2+1<=i2+1 by NAT_1:13;
then
A32: 1<=i2+1-j2 by XREAL_1:19;
f/.n=G*(i1,i2+1) & f/.(n+1)=G*(j1,j2) by A2,A5,A9,A8,A16,A17,A22,A20
,A24,A30,Th8,Th9;
then
A33: 1=|.i1-j1.|+|.i2+1-j2.| by A1,A13,A26,A21;
0<i2+1-j2 by A31,XREAL_1:50;
then
A34: |.i2+1-j2.| = i2+1-j2 by ABSVALUE:def 1;
0<=|.i1-j1.| by COMPLEX1:46;
then 0+(i2+1-j2)<=1 by A33,A34,XREAL_1:7;
then i2+1-j2 = 1 by A32,XXREAL_0:1;
hence contradiction by A30;
end;
case
A35: i2<i & i<=j2;
j2<=j2+1 by NAT_1:11;
then i<=j2+1 by A35,XXREAL_0:2;
then
A36: i2<j2+1 by A35,XXREAL_0:2;
then i2+1<=j2+1 by NAT_1:13;
then
A37: 1<=j2+1-i2 by XREAL_1:19;
f/.n=G*(i1,i2) & f/.(n+1)=G*(j1,j2+1) by A2,A5,A9,A8,A16,A17,A22,A19
,A27,A35,Th8,Th9;
then
A38: 1=|.i1-j1.|+|.i2-(j2+1).| by A1,A13,A29,A28
.=|.i1-j1.|+|.-(j2+1 -i2).|
.=|.i1-j1.|+|.j2+1 -i2.| by COMPLEX1:52;
0<j2+1-i2 by A36,XREAL_1:50;
then
A39: |.j2+1-i2.| = j2+1-i2 by ABSVALUE:def 1;
0<=|.i1-j1.| by COMPLEX1:46;
then 0+(j2+1-i2)<=1 by A38,A39,XREAL_1:7;
then j2+1-i2 = 1 by A37,XXREAL_0:1;
hence contradiction by A35;
end;
case
i<=i2 & i<=j2;
then f/.n=G*(i1,i2+1) & f/.(n+1)=G*(j1,j2+1) by A2,A5,A9,A10,A8,A16,A17
,A22,A20,A27,Th9;
hence 1 = |.i1-j1.|+|.(i2+1)-(j2+1).| by A1,A13,A21,A28
.= |.i1-j1.|+|.i2-j2.|;
end;
end;
hence |.i1-j1.|+|.i2-j2.| = 1;
end;
A40: 1<=i by A2,FINSEQ_1:1;
A41: i<=width G by A2,FINSEQ_1:1;
now
let n;
assume
A42: n in dom f;
then consider m,k such that
A43: [m,k] in Indices G and
A44: f/.n=G*(m,k) by A1;
take m;
A45: m in dom G by A7,A43,ZFMISC_1:87;
A46: k in Seg width G by A7,A43,ZFMISC_1:87;
then
A47: 1<=k by FINSEQ_1:1;
A48: k<=M+1 by A9,A46,FINSEQ_1:1;
now
per cases;
suppose
A49: k<i;
take k;
k<width G by A41,A49,XXREAL_0:2;
then k<=M by A9,NAT_1:13;
then k in Seg M by A47,FINSEQ_1:1;
hence
[m,k] in Indices D & f/.n=D*(m,k) by A2,A5,A9,A10,A11,A8,A6,A44,A45,A47
,A49,Th8,ZFMISC_1:87;
end;
suppose
i<=k;
then
A50: i<k by A3,A42,A44,A45,MATRIX_0:43,XXREAL_0:1;
then k-1 in NAT by A40,INT_1:5,XXREAL_0:2;
then reconsider l = k-1 as Nat;
take l;
A51: l<=M by A48,XREAL_1:20;
i+1<=k by A50,NAT_1:13;
then
A52: i<=k-1 by XREAL_1:19;
then 1<=l by A40,XXREAL_0:2;
then
A53: l in Seg M by A51,FINSEQ_1:1;
D*(m,l)=G*(m,l+1) by A2,A9,A40,A45,A52,A51,Th9;
hence [m,l] in Indices D & f/.n=D*(m,l) by A5,A11,A8,A6,A44,A45,A53,
ZFMISC_1:87;
end;
end;
hence ex k st [m,k] in Indices D & f/.n=D*(m,k);
end;
hence thesis by A12;
end;
theorem Th19:
f is_sequence_on G & i in dom f implies ex n st n in dom G & f/.
i in rng Line(G,n)
proof
assume f is_sequence_on G & i in dom f;
then consider n,m such that
A1: [n,m] in Indices G and
A2: f/.i=G*(n,m);
set L = Line(G,n);
take n;
A3: Indices G=[:dom G,Seg width G:] by MATRIX_0:def 4;
hence n in dom G by A1,ZFMISC_1:87;
A4: m in Seg width G by A1,A3,ZFMISC_1:87;
len L = width G by MATRIX_0:def 7;
then
A5: m in dom L by A4,FINSEQ_1:def 3;
L.m = f/.i by A2,A4,MATRIX_0:def 7;
hence thesis by A5,FUNCT_1:def 3;
end;
theorem Th20:
f is_sequence_on G & i in dom f & i+1 in dom f & n in dom G & f
/.i in rng Line(G,n) implies f/.(i+1) in rng Line(G,n) or for k st f/.(i+1) in
rng Line(G,k) & k in dom G holds |.n-k.| = 1
proof
assume that
A1: f is_sequence_on G and
A2: i in dom f and
A3: i+1 in dom f and
A4: n in dom G & f/.i in rng Line(G,n);
consider j1,j2 be Nat such that
A5: [j1,j2] in Indices G and
A6: f/.(i+1)=G*(j1,j2) by A1,A3;
A7: Indices G=[:dom G,Seg width G:] by MATRIX_0:def 4;
then
A8: j1 in dom G by A5,ZFMISC_1:87;
consider i1,i2 be Nat such that
A9: [i1,i2] in Indices G and
A10: f/.i=G*(i1,i2) by A1,A2;
A11: i2 in Seg width G by A9,A7,ZFMISC_1:87;
len Line(G,i1) = width G by MATRIX_0:def 7;
then
A12: i2 in dom Line(G,i1) by A11,FINSEQ_1:def 3;
Line(G,i1).i2 = f/.i by A10,A11,MATRIX_0:def 7;
then
A13: f/.i in rng Line(G,i1) by A12,FUNCT_1:def 3;
i1 in dom G by A9,A7,ZFMISC_1:87;
then i1=n by A4,A13,Th2;
then
A14: |.n-j1.|+|.i2-j2.| = 1 by A1,A2,A3,A9,A10,A5,A6;
A15: j2 in Seg width G by A5,A7,ZFMISC_1:87;
len Line(G,j1) = width G by MATRIX_0:def 7;
then
A16: j2 in dom Line(G,j1) by A15,FINSEQ_1:def 3;
A17: Line(G,j1).j2=f/.( i+1) by A6,A15,MATRIX_0:def 7;
then
A18: f/.(i+1) in rng Line(G,j1) by A16,FUNCT_1:def 3;
now
per cases by A14,SEQM_3:42;
suppose
|.n-j1.|=1 & i2=j2;
hence thesis by A8,A18,Th2;
end;
suppose
|.i2-j2.|=1 & n=j1;
hence thesis by A17,A16,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
theorem Th21:
1<=len f & f/.len f in rng Line(G,len G) & f is_sequence_on G &
i in dom G & i+1 in dom G & m in dom f & f/.m in rng Line(G,i) & (for k st k in
dom f & f/.k in rng Line(G,i) holds k<=m) implies m+1 in dom f & f/.(m+1) in
rng Line(G,i+1)
proof
assume that
A1: 1<=len f and
A2: f/.len f in rng Line(G,len G) and
A3: f is_sequence_on G and
A4: i in dom G and
A5: i+1 in dom G and
A6: m in dom f and
A7: f/.m in rng Line(G,i) and
A8: for k st k in dom f & f/.k in rng Line(G,i) holds k<=m;
reconsider p=f/.len f, q=f/.m as Point of TOP-REAL 2;
defpred P[Nat,set] means $2 in dom G & for k st k=$2 holds f/.$1 in rng Line
(G,k);
A9: for n st n in dom f holds ex k st k in dom G & f/.n in rng Line(G,k)
proof
assume not thesis;
then consider n such that
A10: n in dom f and
A11: for k st k in dom G holds not f/.n in rng Line(G,k);
consider i,j such that
A12: [i,j] in Indices G and
A13: f/.n = G*(i,j) by A3,A10;
A14: [i,j] in [:dom G, Seg width G:] by A12,MATRIX_0:def 4;
then i in dom G by ZFMISC_1:87;
then
A15: not f/.n in rng Line(G,i) by A11;
A16: j in Seg width G by A14,ZFMISC_1:87;
then j in Seg len Line(G,i) by MATRIX_0:def 7;
then
A17: j in dom Line(G,i) by FINSEQ_1:def 3;
(Line(G,i)).j = G*(i,j) by A16,MATRIX_0:def 7;
hence contradiction by A13,A15,A17,FUNCT_1:def 3;
end;
A18: for n be Nat st n in Seg len f ex r being Element of REAL st P[n,r]
proof
let n be Nat;
assume n in Seg len f;
then n in dom f by FINSEQ_1:def 3;
then consider k such that
A19: k in dom G and
A20: f/.n in rng Line(G,k) by A9;
reconsider r=k as Element of REAL by XREAL_0:def 1;
take r;
thus r in dom G by A19;
let m;
assume m=r;
hence thesis by A20;
end;
consider v such that
A21: dom v = Seg len f and
A22: for n be Nat st n in Seg len f holds P[n,v.n] from FINSEQ_1:sch 5(A18);
A23: dom f = Seg len f by FINSEQ_1:def 3;
A24: for k st k in dom v & v.k = i holds k<=m
proof
let k;
assume that
A25: k in dom v and
A26: v.k=i;
f/.k in rng Line(G,i) by A21,A22,A25,A26;
hence thesis by A8,A21,A23,A25;
end;
A27: rng v c= dom G
proof
let x be object;
assume x in rng v;
then ex y be Nat st y in dom v & v.y=x by FINSEQ_2:10;
hence thesis by A21,A22;
end;
A28: len v = len f by A21,FINSEQ_1:def 3;
A29: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
holds |.r-s.| = 1 or r=s
proof
let k;
assume that
A30: 1<=k and
A31: k<=len v - 1;
A32: k+1<=len v by A31,XREAL_1:19;
let r,s;
assume that
A33: r = v.k and
A34: s = v.(k+1);
1<=k+1 by NAT_1:11;
then
A35: k+1 in dom f by A28,A32,FINSEQ_3:25;
then
A36: s in rng v by A21,A23,A34,FUNCT_1:def 3;
then
A37: s in dom G by A27;
k<=k+1 by NAT_1:11;
then k<=len f by A28,A32,XXREAL_0:2;
then
A38: k in dom f by A30,FINSEQ_3:25;
then
A39: r in rng v by A21,A23,A33,FUNCT_1:def 3;
then r in dom G by A27;
then reconsider n1=r, n2=s as Element of NAT by A37;
set L1 = Line(G,n1), L2 = Line(G,n2);
f/.k in rng L1 by A22,A23,A38,A33;
then consider x be Nat such that
A40: x in dom L1 and
A41: L1.x = f/.k by FINSEQ_2:10;
A42: dom L1 = Seg len L1 & len L1 = width G by FINSEQ_1:def 3,MATRIX_0:def 7;
then
A43: f/.k = G*(n1,x) by A40,A41,MATRIX_0:def 7;
f/.(k+1) in rng L2 by A22,A23,A35,A34;
then consider y be Nat such that
A44: y in dom L2 and
A45: L2.y = f/.(k+1) by FINSEQ_2:10;
reconsider x,y as Element of NAT by ORDINAL1:def 12;
[n1,x] in [:dom G,Seg width G:] by A27,A39,A40,A42,ZFMISC_1:87;
then
A46: [n1,x] in Indices G by MATRIX_0:def 4;
A47: Seg len L2 = dom L2 & len L2 = width G by FINSEQ_1:def 3,MATRIX_0:def 7;
then [n2,y] in [:dom G,Seg width G:] by A27,A36,A44,ZFMISC_1:87;
then
A48: [n2,y] in Indices G by MATRIX_0:def 4;
f/.(k+1) = G*(n2,y) by A47,A44,A45,MATRIX_0:def 7;
then |.n1-n2.|+|.x-y.|= 1 by A3,A38,A35,A43,A46,A48;
hence thesis by SEQM_3:42;
end;
A49: v.m = i
proof
A50: v.m in dom G by A6,A22,A23;
then reconsider k=v.m as Element of NAT;
assume
A51: v.m <> i;
q in rng Line(G,k) by A6,A22,A23;
hence contradiction by A4,A7,A51,A50,Th2;
end;
1<=m & m<=len f by A6,FINSEQ_3:25;
then 1<=len f by XXREAL_0:2;
then
A52: len f in dom f by FINSEQ_3:25;
A53: v.(len v) = len G
proof
0<len G by MATRIX_0:44;
then 0+1<=len G by NAT_1:13;
then
A54: len G in dom G by FINSEQ_3:25;
A55: v.(len v) in dom G by A22,A28,A23,A52;
then reconsider k=v.(len v) as Element of NAT;
assume
A56: v.(len v) <> len G;
p in rng Line(G,k) by A22,A28,A23,A52;
hence contradiction by A2,A56,A55,A54,Th2;
end;
A57: dom G = Seg len G & v<>{} by A1,A21,FINSEQ_1:def 3;
hence m+1 in dom f by A4,A5,A6,A21,A23,A27,A53,A29,A49,A24,SEQM_3:45;
m+1 in dom v & v.(m+1)=i+1 by A4,A5,A6,A21,A23,A57,A27,A53,A29,A49,A24,
SEQM_3:45;
hence thesis by A21,A22;
end;
theorem
1<=len f & f/.1 in rng Line(G,1) & f/.len f in rng Line(G,len G) &
f is_sequence_on G implies
(for i st 1<=i & i<=len G holds ex k st k in dom f & f /.k in rng Line(G,i)) &
(for i st 1<=i & i<=len G & 2<=len f holds L~f meets rng Line(G,i)) &
for i,j,k,m
st 1<=i & i<=len G & 1<=j & j<=len G & k in dom f
& m in dom f & f/.k in rng Line(G,i) &
(for n st n in dom f & f/.n in rng Line(G,i)
holds n<=k) &
k<m & f/.m in rng Line(G,j)
holds i<j
proof
assume that
A1: 1<=len f and
A2: f/.1 in rng Line(G,1) and
A3: f/.len f in rng Line(G,len G) and
A4: f is_sequence_on G;
A5: len f in dom f by A1,FINSEQ_3:25;
defpred P[Nat] means
1<=$1 & $1<= len G implies ex k st k in dom
f & f/.k in rng Line(G,$1);
A6: for k st P[k] holds P[k+1]
proof
let k;
assume
A7: 1<=k & k<= len G implies ex i st i in dom f & f/.i in rng Line(G,k );
assume that
A8: 1<=k+1 and
A9: k+1<=len G;
A10: k+1 in dom G by A8,A9,FINSEQ_3:25;
per cases;
suppose
A11: k=0;
take 1;
thus thesis by A1,A2,A11,FINSEQ_3:25;
end;
suppose
A12: k<>0;
defpred R[Nat] means $1 in dom f & f/.$1 in rng Line(G,k);
A13: for i be Nat holds R[i] implies i<=len f by FINSEQ_3:25;
A14: 0+1<=k by A12,NAT_1:13;
then
A15: ex i be Nat st R[i] by A7,A9,NAT_1:13;
consider m be Nat such that
A16: R[m] & for i be Nat st R[i] holds i<= m from NAT_1:sch 6(A13,
A15);
take m+1;
k<=len G by A9,NAT_1:13;
then
A17: k in dom G by A14,FINSEQ_3:25;
thus thesis by A1,A3,A4,A10,A17,A16,Th21;
end;
end;
A18: P[0];
thus
A19: for i holds P[i] from NAT_1:sch 2(A18,A6);
thus for i st 1<=i & i<=len G & 2<=len f holds L~f meets rng Line(G,i)
proof
let i;
assume that
A20: 1<=i & i<=len G and
A21: 2<=len f;
consider k such that
A22: k in dom f and
A23: f/.k in rng Line(G,i) by A19,A20;
f/.k in L~f by A21,A22,Th1;
then L~f /\ rng Line(G,i) <> {} by A23,XBOOLE_0:def 4;
hence thesis;
end;
let m,k,i,j;
assume that
A24: 1<=m and
A25: m<=len G and
A26: 1<=k & k<=len G and
A27: i in dom f and
A28: j in dom f and
A29: f/.i in rng Line(G,m) and
A30: for n st n in dom f & f/.n in rng Line(G,m) holds n<=i and
A31: i<j and
A32: f/.j in rng Line(G,k);
A33: i<=len f & j<=len f by A27,A28,FINSEQ_3:25;
per cases;
suppose
m = len G;
then len f<=i by A3,A5,A30;
hence thesis by A31,A33,XXREAL_0:1;
end;
suppose
m <> len G;
then m<len G by A25,XXREAL_0:1;
then 1<=m+1 & m+1<=len G by NAT_1:11,13;
then
A34: m+1 in dom G by FINSEQ_3:25;
reconsider l = j - i as Element of NAT by A31,INT_1:5;
defpred P[set] means for n,l be Nat st n=$1 & n>0 & i+n in
dom f & f/.(i+n) in rng Line(G,l) & l in dom G holds m<l;
A35: k in dom G by A26,FINSEQ_3:25;
m in dom G by A24,A25,FINSEQ_3:25;
then
A36: f/.(i+1) in rng Line(G,m+1) by A1,A3,A4,A27,A29,A30,A34,Th21;
A37: for o be Nat st P[o] holds P[o+1]
proof
let o be Nat such that
A38: P[o];
let n,l be Nat such that
A39: n=o+1 and
A40: n>0 and
A41: i+n in dom f and
A42: f/.(i+n) in rng Line(G,l) and
A43: l in dom G;
per cases;
suppose
o=0;
then l=m+1 by A34,A36,A39,A42,A43,Th2;
hence thesis by NAT_1:13;
end;
suppose
A44: o<>0;
1<=i by A27,FINSEQ_3:25;
then
A45: 1<=i+o by NAT_1:12;
i+n<=len f & i+o<=i+o+1 by A41,FINSEQ_3:25,NAT_1:12;
then i+o<=len f by A39,XXREAL_0:2;
then
A46: i+o in dom f by A45,FINSEQ_3:25;
then consider l1 be Nat such that
A47: l1 in dom G and
A48: f/.(i+o) in rng Line(G,l1) by A4,Th19;
A49: m<l1 by A38,A44,A46,A47,A48;
A50: i+n = i+o+1 by A39;
per cases by A4,A41,A50,A46,A47,A48,Th20;
suppose
f/.(i+n) in rng Line(G,l1);
hence thesis by A42,A43,A47,A49,Th2;
end;
suppose
for k st f/.(i+n) in rng Line(G,k) & k in dom G holds
|.l1-k.| = 1;
then |.l1-l.| = 1 by A42,A43;
then per cases by SEQM_3:41;
suppose
l1>l & l1=l+1;
then m<=l by A49,NAT_1:13;
then per cases by XXREAL_0:1;
suppose
m=l;
then i+n<=i by A30,A41,A42;
then n<=i-i by XREAL_1:19;
hence thesis by A40;
end;
suppose
m<l;
hence thesis;
end;
end;
suppose
l1<l & l=l1+1;
hence thesis by A49,XXREAL_0:2;
end;
end;
end;
end;
A51: P[0];
A52: for o be Nat holds P[o] from NAT_1:sch 2(A51,A37);
0< j - i & i+l = j by A31,XREAL_1:50;
hence thesis by A28,A32,A52,A35;
end;
end;
theorem Th23:
f is_sequence_on G & i in dom f implies ex n st n in Seg width G
& f/.i in rng Col(G,n)
proof
assume f is_sequence_on G & i in dom f;
then consider n,m such that
A1: [n,m] in Indices G and
A2: f/.i=G*(n,m);
set L = Col(G,m);
take m;
A3: Indices G=[:dom G,Seg width G:] by MATRIX_0:def 4;
hence m in Seg width G by A1,ZFMISC_1:87;
A4: n in dom G by A1,A3,ZFMISC_1:87;
len L = len G by MATRIX_0:def 8;
then
A5: n in dom L by A4,FINSEQ_3:29;
L.n = f/.i by A2,A4,MATRIX_0:def 8;
hence thesis by A5,FUNCT_1:def 3;
end;
theorem Th24:
f is_sequence_on G & i in dom f & i+1 in dom f & n in Seg width
G & f/.i in rng Col(G,n) implies f/.(i+1) in rng Col(G,n) or for k st f/.(i+1)
in rng Col(G,k) & k in Seg width G holds |.n-k.| = 1
proof
assume that
A1: f is_sequence_on G and
A2: i in dom f and
A3: i+1 in dom f and
A4: n in Seg width G & f/.i in rng Col(G,n);
consider j1,j2 be Nat such that
A5: [j1,j2] in Indices G and
A6: f/.(i+1)=G*(j1,j2) by A1,A3;
A7: Indices G=[:dom G,Seg width G:] by MATRIX_0:def 4;
then
A8: j1 in dom G by A5,ZFMISC_1:87;
A9: j2 in Seg width G by A5,A7,ZFMISC_1:87;
len Col(G,j2) = len G by MATRIX_0:def 8;
then
A10: j1 in dom Col(G,j2) by A8,FINSEQ_3:29;
consider i1,i2 be Nat such that
A11: [i1,i2] in Indices G and
A12: f/.i=G*(i1,i2) by A1,A2;
A13: i1 in dom G by A11,A7,ZFMISC_1:87;
len Col(G,i2) = len G by MATRIX_0:def 8;
then
A14: i1 in dom Col(G,i2) by A13,FINSEQ_3:29;
Col(G,i2).i1 = f/.i by A12,A13,MATRIX_0:def 8;
then
A15: f/.i in rng Col(G,i2) by A14,FUNCT_1:def 3;
i2 in Seg width G by A11,A7,ZFMISC_1:87;
then i2=n by A4,A15,Th3;
then
A16: |.i1-j1.|+|.n-j2.| = 1 by A1,A2,A3,A11,A12,A5,A6;
A17: Col(G,j2).j1=f/.(i+1) by A6,A8,MATRIX_0:def 8;
then
A18: f/.(i+1) in rng Col(G,j2) by A10,FUNCT_1:def 3;
now
per cases by A16,SEQM_3:42;
suppose
|.i1-j1.|=1 & n=j2;
hence thesis by A17,A10,FUNCT_1:def 3;
end;
suppose
|.n-j2.|=1 & i1=j1;
hence thesis by A9,A18,Th3;
end;
end;
hence thesis;
end;
theorem Th25:
1<=len f & f/.len f in rng Col(G,width G) & f is_sequence_on G &
i in Seg width G & i+1 in Seg width G & m in dom f & f/.m in rng Col(G,i) & (
for k st k in dom f & f/.k in rng Col(G,i) holds k<=m) implies m+1 in dom f & f
/.(m+1) in rng Col(G,i+1)
proof
assume that
A1: 1<=len f and
A2: f/.len f in rng Col(G,width G) and
A3: f is_sequence_on G and
A4: i in Seg width G and
A5: i+1 in Seg width G and
A6: m in dom f and
A7: f/.m in rng Col(G,i) and
A8: for k st k in dom f & f/.k in rng Col(G,i) holds k<=m;
defpred P[Nat,set] means $2 in Seg width G & for k st k=$2 holds f/.$1 in
rng Col(G,k);
A9: dom G = Seg len G by FINSEQ_1:def 3;
A10: for n st n in dom f ex k st k in Seg width G & f/.n in rng Col(G,k)
proof
assume not thesis;
then consider n such that
A11: n in dom f and
A12: for k st k in Seg width G holds not f/.n in rng Col(G,k);
consider i,j such that
A13: [i,j] in Indices G and
A14: f/.n = G*(i,j) by A3,A11;
A15: [i,j] in [:dom G, Seg width G:] by A13,MATRIX_0:def 4;
then j in Seg width G by ZFMISC_1:87;
then
A16: not f/.n in rng Col(G,j) by A12;
A17: i in dom G by A15,ZFMISC_1:87;
then i in Seg len Col(G,j) by A9,MATRIX_0:def 8;
then
A18: i in dom Col(G,j) by FINSEQ_1:def 3;
(Col(G,j)).i = G*(i,j) by A17,MATRIX_0:def 8;
hence contradiction by A14,A16,A18,FUNCT_1:def 3;
end;
A19: for n be Nat st n in Seg len f ex r being Element of REAL st P[n,r]
proof
let n be Nat;
assume n in Seg len f;
then n in dom f by FINSEQ_1:def 3;
then consider k such that
A20: k in Seg width G and
A21: f/.n in rng Col(G,k) by A10;
reconsider r=k as Element of REAL by XREAL_0:def 1;
take r;
thus r in Seg width G by A20;
let m;
assume m=r;
hence thesis by A21;
end;
consider v such that
A22: dom v = Seg len f and
A23: for n be Nat st n in Seg len f holds P[n,v.n] from FINSEQ_1:sch 5(A19);
A24: dom f = Seg len f by FINSEQ_1:def 3;
A25: for k st k in dom v & v.k = i holds k<=m
proof
let k;
assume that
A26: k in dom v and
A27: v.k=i;
f/.k in rng Col(G,i) by A22,A23,A26,A27;
hence thesis by A8,A22,A24,A26;
end;
A28: rng v c= Seg width G
proof
let x be object;
assume x in rng v;
then ex y be Nat st y in dom v & v.y=x by FINSEQ_2:10;
hence thesis by A22,A23;
end;
A29: len v = len f by A22,FINSEQ_1:def 3;
A30: for k st 1<=k & k<=len v - 1 holds for r,s st r = v.k & s = v.(k+1)
holds |.r-s.| = 1 or r=s
proof
let k;
assume that
A31: 1<=k and
A32: k<=len v - 1;
A33: k+1<=len v by A32,XREAL_1:19;
let r,s;
assume that
A34: r = v.k and
A35: s = v.(k+1);
1<=k+1 by NAT_1:11;
then
A36: k+1 in dom f by A29,A33,FINSEQ_3:25;
then
A37: s in rng v by A22,A24,A35,FUNCT_1:def 3;
then
A38: s in Seg width G by A28;
k<=k+1 by NAT_1:11;
then k<=len f by A29,A33,XXREAL_0:2;
then
A39: k in dom f by A31,FINSEQ_3:25;
then
A40: r in rng v by A22,A24,A34,FUNCT_1:def 3;
then r in Seg width G by A28;
then reconsider n1=r, n2=s as Element of NAT by A38;
set L1 = Col(G,n1), L2 = Col(G,n2);
f/.k in rng L1 by A23,A24,A39,A34;
then consider x be Nat such that
A41: x in dom L1 and
A42: L1.x = f/.k by FINSEQ_2:10;
A43: dom L1 = Seg len L1 & len L1 = len G by FINSEQ_1:def 3,MATRIX_0:def 8;
then
A44: f/.k = G*(x,n1) by A9,A41,A42,MATRIX_0:def 8;
f/.(k+1) in rng L2 by A23,A24,A36,A35;
then consider y be Nat such that
A45: y in dom L2 and
A46: L2.y = f/.(k+1) by FINSEQ_2:10;
reconsider x,y as Element of NAT by ORDINAL1:def 12;
[x,n1] in [:dom G,Seg width G:] by A9,A28,A40,A41,A43,ZFMISC_1:87;
then
A47: [x,n1] in Indices G by MATRIX_0:def 4;
A48: dom L2 = Seg len L2 & len L2 = len G by FINSEQ_1:def 3,MATRIX_0:def 8;
then [y,n2] in [:dom G,Seg width G:] by A9,A28,A37,A45,ZFMISC_1:87;
then
A49: [y,n2] in Indices G by MATRIX_0:def 4;
f/.(k+1) = G*(y,n2) by A9,A48,A45,A46,MATRIX_0:def 8;
then |.x-y.|+|.n1-n2.|= 1 by A3,A39,A36,A44,A47,A49;
hence thesis by SEQM_3:42;
end;
A50: v.m = i
proof
A51: v.m in Seg width G by A6,A23,A24;
then reconsider k=v.m as Element of NAT;
assume
A52: v.m <> i;
f/.m in rng Col(G,k) by A6,A23,A24;
hence contradiction by A4,A7,A52,A51,Th3;
end;
1<=m & m<=len f by A6,FINSEQ_3:25;
then 1<=len f by XXREAL_0:2;
then
A53: len f in dom f by FINSEQ_3:25;
A54: v.(len v) = width G
proof
0<width G by MATRIX_0:44;
then 0+1<=width G by NAT_1:13;
then
A55: width G in Seg width G by FINSEQ_1:1;
A56: v.(len v) in Seg width G by A23,A29,A24,A53;
then reconsider k=v.(len v) as Element of NAT;
assume
A57: v.(len v) <> width G;
f/.len f in rng Col(G,k) by A23,A29,A24,A53;
hence contradiction by A2,A57,A56,A55,Th3;
end;
A58: v<>{} by A1,A22;
hence m+1 in dom f by A4,A5,A6,A22,A24,A28,A54,A30,A50,A25,SEQM_3:45;
m+1 in dom v & v.(m+1)=i+1 by A4,A5,A6,A22,A24,A58,A28,A54,A30,A50,A25,
SEQM_3:45;
hence thesis by A22,A23;
end;
theorem Th26:
1<=len f & f/.1 in rng Col(G,1) & f/.len f in rng Col(G,width G)
& f is_sequence_on G implies (for i st 1<=i & i<=width G holds ex k st k in dom
f & f/.k in rng Col(G,i)) & (for i st 1<=i & i<=width G & 2<=len f holds L~f
meets rng Col(G,i)) & for i,j,k,m st 1<=i & i<=width G & 1<=j & j<=width G & k
in dom f & m in dom f & f/.k in rng Col(G,i) & (for n st n in dom f & f/.n in
rng Col(G,i) holds n<=k) & k<m & f/.m in rng Col(G,j) holds i<j
proof
assume that
A1: 1<=len f and
A2: f/.1 in rng Col(G,1) and
A3: f/.len f in rng Col(G,width G) and
A4: f is_sequence_on G;
A5: len f in dom f by A1,FINSEQ_3:25;
defpred P[Nat] means
1<=$1 & $1<=width G implies ex k st k in dom
f & f/.k in rng Col(G,$1);
A6: for k st P[k] holds P[k+1]
proof
let k;
assume
A7: 1<=k & k<=width G implies ex i st i in dom f & f/.i in rng Col(G,k );
assume that
A8: 1<=k+1 and
A9: k+1<=width G;
A10: k+1 in Seg width G by A8,A9,FINSEQ_1:1;
per cases;
suppose
A11: k=0;
take 1;
thus thesis by A1,A2,A11,FINSEQ_3:25;
end;
suppose
A12: k<>0;
defpred R[Nat] means $1 in dom f & f/.$1 in rng Col(G,k);
A13: for i be Nat holds R[i] implies i<=len f by FINSEQ_3:25;
A14: 0+1<=k by A12,NAT_1:13;
then
A15: ex i be Nat st R[i] by A7,A9,NAT_1:13;
consider m be Nat such that
A16: R[m] & for i be Nat st R[i] holds i<=m from NAT_1:sch 6(A13,A15
);
take m+1;
k<=width G by A9,NAT_1:13;
then
A17: k in Seg width G by A14,FINSEQ_1:1;
thus thesis by A1,A3,A4,A10,A17,A16,Th25;
end;
end;
A18: P[0];
thus
A19: for i holds P[i] from NAT_1:sch 2(A18,A6);
thus for i st 1<=i & i<=width G & 2<=len f holds L~f meets rng Col(G,i)
proof
let i;
assume that
A20: 1<=i & i<=width G and
A21: 2<=len f;
consider k such that
A22: k in dom f and
A23: f/.k in rng Col(G,i) by A19,A20;
f/.k in L~f by A21,A22,Th1;
then L~f /\ rng Col(G,i) <> {} by A23,XBOOLE_0:def 4;
hence thesis;
end;
let m,k,i,j;
assume that
A24: 1<=m and
A25: m<=width G and
A26: 1<=k & k<=width G and
A27: i in dom f and
A28: j in dom f and
A29: f/.i in rng Col(G,m) and
A30: for n st n in dom f & f/.n in rng Col(G,m) holds n<=i and
A31: i<j and
A32: f/.j in rng Col(G,k);
A33: i<=len f & j<=len f by A27,A28,FINSEQ_3:25;
now
per cases;
case
m = width G;
then len f<=i by A3,A5,A30;
hence contradiction by A31,A33,XXREAL_0:1;
end;
case
m <> width G;
then m<width G by A25,XXREAL_0:1;
then 1<=m+1 & m+1<=width G by NAT_1:11,13;
then
A34: m+1 in Seg width G by FINSEQ_1:1;
reconsider l = j - i as Element of NAT by A31,INT_1:5;
defpred P[set] means for n,l be Nat st n=$1 & n>0 & i+n in
dom f & f/.(i+n) in rng Col(G,l) & l in Seg width G holds m<l;
A35: k in Seg width G by A26,FINSEQ_1:1;
m in Seg width G by A24,A25,FINSEQ_1:1;
then
A36: f/.(i+1) in rng Col(G,m+1) by A1,A3,A4,A27,A29,A30,A34,Th25;
A37: for o be Nat st P[o] holds P[o+1]
proof
let o be Nat such that
A38: P[o];
let n,l be Nat such that
A39: n=o+1 and
A40: n>0 and
A41: i+n in dom f and
A42: f/.(i+n) in rng Col(G,l) and
A43: l in Seg width G;
now
per cases;
suppose
o=0;
then l=m+1 by A34,A36,A39,A42,A43,Th3;
hence thesis by NAT_1:13;
end;
suppose
A44: o<>0;
1<=i by A27,FINSEQ_3:25;
then
A45: 1<=i+o by NAT_1:12;
i+n<=len f & i+o<=i+o+1 by A41,FINSEQ_3:25,NAT_1:12;
then i+o<=len f by A39,XXREAL_0:2;
then
A46: i+o in dom f by A45,FINSEQ_3:25;
then consider l1 be Nat such that
A47: l1 in Seg width G and
A48: f/.(i+o) in rng Col(G,l1) by A4,Th23;
A49: m<l1 by A38,A44,A46,A47,A48;
A50: i+n = i+o+1 by A39;
now
per cases by A4,A41,A50,A46,A47,A48,Th24;
suppose
f/.(i+n) in rng Col(G,l1);
hence thesis by A42,A43,A47,A49,Th3;
end;
suppose
for k st f/.(i+n) in rng Col(G,k) & k in Seg width G
holds |.l1-k.| = 1;
then
A51: |.l1-l.| = 1 by A42,A43;
now
per cases by A51,SEQM_3:41;
suppose
l1>l & l1=l+1;
then
A52: m<=l by A49,NAT_1:13;
now
per cases by A52,XXREAL_0:1;
case
m=l;
then i+n<=i by A30,A41,A42;
then n<=i-i by XREAL_1:19;
hence contradiction by A40;
end;
case
m<l;
hence thesis;
end;
end;
hence thesis;
end;
suppose
l1<l & l=l1+1;
hence thesis by A49,XXREAL_0:2;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A53: P[0];
A54: for o be Nat holds P[o] from NAT_1:sch 2(A53,A37);
0< j - i & i+l = j by A31,XREAL_1:50;
hence thesis by A28,A32,A54,A35;
end;
end;
hence thesis;
end;
theorem Th27:
k in Seg width G & f/.1 in rng Col(G,1) & f is_sequence_on G & (
for i st i in dom f & f/.i in rng Col(G,k) holds n<=i) implies for i st i in
dom f & i<=n holds for m st m in Seg width G & f/.i in rng Col(G,m) holds m<=k
proof
assume that
A1: k in Seg width G and
A2: f/.1 in rng Col(G,1) and
A3: f is_sequence_on G and
A4: for i st i in dom f & f/.i in rng Col(G,k) holds n<=i;
defpred P[Nat] means
$1 in dom f & $1<=n implies for m st m in
Seg width G & f/.$1 in rng Col(G,m) holds m<=k;
A5: dom G = Seg len G by FINSEQ_1:def 3;
0<width G by MATRIX_0:44;
then 0+1<=width G by NAT_1:13;
then
A6: 1 in Seg width G by FINSEQ_1:1;
A7: 1<=k by A1,FINSEQ_1:1;
A8: for i st P[i] holds P[i+1]
proof
let i such that
A9: P[i];
assume that
A10: i+1 in dom f and
A11: i+1<=n;
let m such that
A12: m in Seg width G & f/.(i+1) in rng Col(G,m);
now
per cases;
suppose
i=0;
hence thesis by A2,A6,A7,A12,Th3;
end;
suppose
A13: i<>0;
i+1<=len f by A10,FINSEQ_3:25;
then
A14: i<=len f by NAT_1:13;
A15: i<n by A11,NAT_1:13;
A16: 0+1<=i by A13,NAT_1:13;
then
A17: i in dom f by A14,FINSEQ_3:25;
then consider i1,i2 be Nat such that
A18: [i1,i2] in Indices G and
A19: f/.i = G*(i1,i2) by A3;
A20: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
then
A21: i2 in Seg width G by A18,ZFMISC_1:87;
A22: dom Col(G,i2) = Seg len Col(G,i2) & len Col(G,i2)=len G by
FINSEQ_1:def 3,MATRIX_0:def 8;
A23: i1 in dom G by A18,A20,ZFMISC_1:87;
then Col(G,i2).i1 = f/.i by A19,MATRIX_0:def 8;
then
A24: f/.i in rng Col(G,i2) by A5,A23,A22,FUNCT_1:def 3;
then
A25: i2<=k by A9,A11,A16,A14,A21,FINSEQ_3:25,NAT_1:13;
now
per cases by A25,XXREAL_0:1;
case
A26: i2<k;
now
per cases by A3,A10,A17,A21,A24,Th24;
suppose
f/.(i+1) in rng Col(G,i2);
hence thesis by A12,A21,A26,Th3;
end;
suppose
for j st f/.(i+1) in rng Col(G,j) & j in Seg width G
holds |.i2-j.|=1;
then
A27: |.i2-m.|=1 by A12;
now
per cases by A27,SEQM_3:41;
suppose
i2>m & i2=m+1;
hence thesis by A26,XXREAL_0:2;
end;
suppose
i2<m & m=i2+1;
hence thesis by A26,NAT_1:13;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
case
i2=k;
hence contradiction by A4,A15,A17,A24;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A28: P[0] by FINSEQ_3:25;
thus for n holds P[n] from NAT_1:sch 2(A28,A8);
end;
theorem
f is_sequence_on G & f/.1 in rng Col(G,1) & f/.len f in rng Col(G,
width G) & width G > 1 & 1<=len f implies ex g st g/.1 in rng Col(DelCol(G,
width G),1) & g/.len g in rng Col(DelCol(G,width G),width DelCol(G,width G)) &
1<=len g & g is_sequence_on DelCol(G,width G) & rng g c= rng f
proof
set D = DelCol(G,width G);
assume that
A1: f is_sequence_on G and
A2: f/.1 in rng Col(G,1) and
A3: f/.len f in rng Col(G,width G) and
A4: width G > 1 and
A5: 1<=len f;
consider k such that
A6: width G=k+1 and
A7: k>0 by A4,SEQM_3:43;
A8: width G in Seg width G by A4,FINSEQ_1:1;
A9: len D=len G by MATRIX_0:def 13;
A10: 0+1<=k by A7,NAT_1:13;
then 1<width G by A6,NAT_1:13;
then
A11: Col(D,1)=Col(G,1) by A6,A7,A8,Th6;
A12: dom G = Seg len G by FINSEQ_1:def 3;
defpred P[Nat] means $1 in dom f & f/.$1 in rng Col(G,k);
k<=k+1 by NAT_1:11;
then ex m st P[m] by A1,A2,A3,A5,A6,A10,Th26;
then
A13: ex m be Nat st P[m];
consider m be Nat such that
A14: P[m] & for i be Nat st P[i] holds m<=i from NAT_1:sch 5(A13);
A15: width D = k by A6,A8,MATRIX_0:63;
then width D<width G by A6,NAT_1:13;
then
A16: Col(D,width D)=Col(G,width D) by A6,A10,A8,A15,Th6;
A17: dom D = Seg len D by FINSEQ_1:def 3;
A18: for i st P[i] holds m<=i by A14;
reconsider m as Element of NAT by ORDINAL1:def 12;
A19: 1<=m by A14,FINSEQ_3:25;
then
A20: 1 in Seg m by FINSEQ_1:1;
A21: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
take t = f|m;
m<=len f by A14,FINSEQ_3:25;
then
A22: len t = m by FINSEQ_1:59;
then len t in Seg m by A19,FINSEQ_1:1;
hence
t/.1 in rng Col(D,1) & t/.len t in rng Col(D,width D) & 1<=len t by A2,A14
,A15,A11,A16,A22,A20,FINSEQ_1:1,FINSEQ_4:71;
A23: dom t=Seg len t by FINSEQ_1:def 3;
A24: Indices D = [:dom D,Seg width D:] by MATRIX_0:def 4;
A25: now
k<=k+1 by NAT_1:11;
then
A26: k in Seg width G by A6,A10,FINSEQ_1:1;
let n;
assume
A27: n in dom t;
then
A28: n<=m by A22,FINSEQ_3:25;
A29: n in dom f by A14,A22,A23,A27,FINSEQ_4:71;
then consider i,j such that
A30: [i,j] in Indices G and
A31: f/.n=G*(i,j) by A1;
A32: j in Seg width G by A21,A30,ZFMISC_1:87;
then
A33: 1<=j by FINSEQ_1:1;
take i,j;
A34: len Col(G,j) = len G & dom Col(G,j)=Seg len Col(G,j) by FINSEQ_1:def 3
,MATRIX_0:def 8;
A35: i in dom G by A21,A30,ZFMISC_1:87;
then Col(G,j).i=G*(i,j) by MATRIX_0:def 8;
then f/.n in rng Col(G,j) by A12,A31,A35,A34,FUNCT_1:def 3;
then j<=k by A1,A2,A18,A29,A28,A32,A26,Th27;
then
A36: j in Seg k by A33,FINSEQ_1:1;
hence [i,j] in Indices D by A9,A12,A17,A15,A24,A35,ZFMISC_1:87;
thus t/.n = G*(i,j) by A14,A22,A23,A27,A31,FINSEQ_4:71
.= D*(i,j) by A6,A7,A35,A36,Th13;
end;
now
let n;
assume that
A37: n in dom t and
A38: n+1 in dom t;
A39: n in dom f & n+1 in dom f by A14,A22,A23,A37,A38,FINSEQ_4:71;
let i1,i2,j1,j2 be Nat;
assume that
A40: [i1,i2] in Indices D and
A41: [j1,j2] in Indices D and
A42: t/.n=D*(i1,i2) and
A43: t/.(n+1)=D*(j1,j2);
A44: i1 in dom D & i2 in Seg k by A15,A24,A40,ZFMISC_1:87;
A45: j1 in dom D & j2 in Seg k by A15,A24,A41,ZFMISC_1:87;
t/.n=f/.n by A14,A22,A23,A37,FINSEQ_4:71;
then
A46: f/.n=G*(i1,i2) by A6,A7,A9,A12,A17,A42,A44,Th13;
k<=k+1 by NAT_1:11;
then
A47: Seg k c= Seg width G by A6,FINSEQ_1:5;
then
A48: [j1,j2] in Indices G by A9,A21,A12,A17,A45,ZFMISC_1:87;
t/.(n+1)=f/.(n+1) by A14,A22,A23,A38,FINSEQ_4:71;
then
A49: f/.(n+1)=G*(j1,j2) by A6,A7,A9,A12,A17,A43,A45,Th13;
[i1,i2] in Indices G by A9,A21,A12,A17,A44,A47,ZFMISC_1:87;
hence |.i1-j1.|+|.i2-j2.| = 1 by A1,A39,A46,A49,A48;
end;
hence t is_sequence_on D by A25;
t = f|Seg m by FINSEQ_1:def 16;
hence thesis by RELAT_1:70;
end;
theorem
f is_sequence_on G & rng f /\ rng Col(G,1)<>{} & rng f /\ rng Col(G,
width G)<>{} implies ex g st rng g c= rng f & g/.1 in rng Col(G,1) & g/.len g
in rng Col(G,width G) & 1<=len g & g is_sequence_on G
proof
assume that
A1: f is_sequence_on G and
A2: rng f /\ rng Col(G,1)<>{} and
A3: rng f /\ rng Col(G,width G)<>{};
set y = the Element of rng f /\ rng Col(G,width G);
set x = the Element of rng f /\ rng Col(G,1);
A4: x in rng Col(G,1) & y in rng Col(G,width G) by A2,A3,XBOOLE_0:def 4;
y in rng f by A3,XBOOLE_0:def 4;
then consider m being Element of NAT such that
A5: m in dom f and
A6: y=f/.m by PARTFUN2:2;
A7: 1<=m by A5,FINSEQ_3:25;
A8: x in rng f by A2,XBOOLE_0:def 4;
then consider n being Element of NAT such that
A9: n in dom f and
A10: x=f/.n by PARTFUN2:2;
reconsider x as Point of TOP-REAL 2 by A10;
A11: 1<=n by A9,FINSEQ_3:25;
per cases by XXREAL_0:1;
suppose
A12: n=m;
reconsider h = <*x*> as FinSequence of TOP-REAL 2;
A13: len h=1 by FINSEQ_1:39;
A14: now
let k;
assume
A15: k in Seg 1;
then
A16: k = 1 by FINSEQ_1:2,TARSKI:def 1;
k in dom h by A15,FINSEQ_1:def 8;
hence h/.k = h.k by PARTFUN1:def 6
.= x by A16;
end;
A17: rng h c= rng f
proof
let z be object;
assume z in rng h;
then consider i being Element of NAT such that
A18: i in dom h and
A19: z=h/.i by PARTFUN2:2;
i in Seg 1 by A18,FINSEQ_1:def 8;
hence thesis by A8,A14,A19;
end;
reconsider h as FinSequence of TOP-REAL 2;
take h;
thus rng h c= rng f by A17;
1 in Seg 1 by FINSEQ_1:1;
hence h/.1 in rng Col(G,1) & h/.len h in rng Col(G,width G) by A10,A4,A6
,A12,A13,A14;
A20: dom h=Seg len h by FINSEQ_1:def 3;
A21: now
let i;
assume that
A22: i in dom h and
A23: i+1 in dom h;
i=1 by A13,A20,A22,FINSEQ_1:2,TARSKI:def 1;
hence
for i1,i2,j1,j2 be Nat st [i1,i2] in Indices G & [j1,j2]
in Indices G & h/.i=G*(i1,i2) & h/.(i+1)=G* (j1,j2) holds |.i1-j1.|+|.i2-j2.|
=1 by A13,A20,A23,FINSEQ_1:2,TARSKI:def 1;
end;
now
consider i1,i2 be Nat such that
A24: [i1,i2] in Indices G & f/.n=G*(i1,i2) by A1,A9;
let i such that
A25: i in dom h;
take i1,i2;
thus [i1,i2] in Indices G & h/.i=G*(i1,i2) by A10,A13,A14,A20,A25,A24;
end;
hence thesis by A21,FINSEQ_1:39;
end;
suppose
A26: n>m;
n<=n+1 by NAT_1:11;
then reconsider l=n+1-m as Element of NAT by A26,INT_1:5,XXREAL_0:2;
set f1=f|n;
defpred P[Nat,set] means for k st $1+k = n+1 holds $2 = f1/.k;
A27: n in Seg n by A11,FINSEQ_1:1;
A28: now
let i;
assume i in Seg l;
then
A29: i<=l by FINSEQ_1:1;
l<=n+1-0 by XREAL_1:13;
hence n+1-i is Element of NAT by A29,INT_1:5,XXREAL_0:2;
end;
A30: for i being Nat st i in Seg l ex p st P[i,p]
proof
let i be Nat;
assume i in Seg l;
then reconsider a=n+1-i as Element of NAT by A28;
take f1/.a;
let k;
assume i+k = n+1;
hence thesis;
end;
consider g such that
A31: len g = l & for i being Nat st i in Seg l holds P[i,g/.i] from
FINSEQ_4:sch 1(A30);
take g;
A32: dom g = Seg len g by FINSEQ_1:def 3;
A33: for i st i in Seg l holds n+1-i is Element of NAT & f1/.(n+1-i)=f/.(n
+1-i) & n+1-i in dom f
proof
let i;
assume
A34: i in Seg l;
then
A35: i<=l by FINSEQ_1:1;
l<=n+1-0 by XREAL_1:13;
then reconsider w=n+1-i as Element of NAT by A35,INT_1:5,XXREAL_0:2;
1<=i by A34,FINSEQ_1:1;
then
A36: n+1-i<=n+1-1 by XREAL_1:13;
n+1-l<=n+1-i by A35,XREAL_1:13;
then 1<=n+1-i by A7,XXREAL_0:2;
then w in Seg n by A36,FINSEQ_1:1;
hence thesis by A9,FINSEQ_4:71;
end;
thus rng g c= rng f
proof
let z be object;
assume z in rng g;
then consider i being Element of NAT such that
A37: i in dom g and
A38: z=g/.i by PARTFUN2:2;
reconsider yy = n+1-i as Element of NAT by A28,A31,A32,A37;
i + yy = n+1;
then
A39: z=f1/.yy by A31,A32,A37,A38;
f1/.yy=f/.yy & yy in dom f by A33,A31,A32,A37;
hence thesis by A39,PARTFUN2:2;
end;
A40: dom g=Seg len g by FINSEQ_1:def 3;
A41: now
let i;
assume that
A42: i in dom g and
A43: i+1 in dom g;
let i1,i2,j1,j2 be Nat;
assume
A44: [i1,i2] in Indices G & [j1,j2] in Indices G & g/.i=G*(i1,i2) &
g/.(i+ 1)=G*(j1,j2);
reconsider xx = n+1-(i+1) as Element of NAT by A28,A31,A40,A43;
i+1 + xx = n+1;
then g/.(i+1)=f1/.xx by A31,A32,A43;
then
A45: g/.(i+1)=f/.xx by A33,A31,A32,A43;
A46: xx+1=n+1-i;
reconsider ww = n+1-i as Element of NAT by A28,A31,A40,A42;
i + ww = n+1;
then g/.i=f1/.ww by A31,A32,A42;
then
A47: g/.i=f/.ww by A33,A31,A32,A42;
ww in dom f & xx in dom f by A33,A31,A32,A42,A43;
hence 1=|.j1-i1.|+|.j2-i2.| by A1,A47,A45,A46,A44
.= |.-(i1-j1).|+|.-(i2-j2).|
.= |.i1-j1.|+|.-(i2-j2).| by COMPLEX1:52
.= |.i1-j1.|+|.i2-j2.| by COMPLEX1:52;
end;
m+1<=n by A26,NAT_1:13;
then
A48: m+1<=n+1 by NAT_1:13;
then
A49: 1<=l by XREAL_1:19;
then 1 in Seg l by FINSEQ_1:1;
then g/.1 = f1/.n by A31
.= f/.n by A9,A27,FINSEQ_4:71;
hence g/.1 in rng Col(G,1) by A2,A10,XBOOLE_0:def 4;
A50: m in Seg n by A7,A26,FINSEQ_1:1;
reconsider ww = n+1-l as Element of NAT;
A51: l + ww = n+1;
len g in dom g by A31,A49,FINSEQ_3:25;
then g/.len g= f1/.ww by A31,A32,A51
.= f/.m by A9,A50,FINSEQ_4:71;
hence g/.len g in rng Col(G,width G) by A3,A6,XBOOLE_0:def 4;
now
let i;
assume
A52: i in dom g;
then reconsider ww=n+1-i as Element of NAT by A28,A31,A40;
ww in dom f by A33,A31,A32,A52;
then consider i1,i2 be Nat such that
A53: [i1,i2] in Indices G & f/.ww=G*(i1,i2) by A1;
take i1,i2;
i + ww = n+1;
then g/.i=f1/.ww by A31,A32,A52;
hence [i1,i2] in Indices G & g/.i=G*(i1,i2) by A33,A31,A32,A52,A53;
end;
hence thesis by A31,A48,A41,XREAL_1:19;
end;
suppose
A54: n<m;
then
A55: n in Seg m by A11,FINSEQ_1:1;
m<=m+1 by NAT_1:11;
then reconsider l=m+1-n as Element of NAT by A54,INT_1:5,XXREAL_0:2;
reconsider w=n-1 as Element of NAT by A11,INT_1:5;
set f1=f|m;
defpred P[Nat,set] means $2=f1/.(w+$1);
A56: for i being Nat st i in Seg l ex p st P[i,p];
consider g such that
A57: len g= l & for i being Nat st i in Seg l holds P[i,g/.i] from
FINSEQ_4:sch 1(A56);
reconsider ww = m+1-n as Element of NAT by A57;
A58: m in Seg m by A7,FINSEQ_1:1;
take g;
A59: dom g = Seg l by A57,FINSEQ_1:def 3;
A60: for i st i in Seg l holds n-1 is Element of NAT & f1/.(w+i)=f/.(w+i)
& n-1+i in dom f
proof
let i;
assume
A61: i in Seg l;
then i<=l by FINSEQ_1:1;
then i+n<=l+n by XREAL_1:7;
then
A62: i+n-1<=m by XREAL_1:20;
1<=i by A61,FINSEQ_1:1;
then 0+1<=w+i by XREAL_1:7;
then w+i in Seg m by A62,FINSEQ_1:1;
hence thesis by A5,FINSEQ_4:71;
end;
A63: now
let i;
assume that
A64: i in dom g and
A65: i+1 in dom g;
g/.i=f1/.(w+i) by A57,A59,A64;
then
A66: g/.i=f/.(w+i) by A60,A59,A64;
g/.(i+1)=f1/.(w+(i+1)) by A57,A59,A65;
then
A67: w+i+1 in dom f & g/.(i+1)=f/.(w+i+1) by A60,A59,A65;
let i1,i2,j1,j2 be Nat;
assume
A68: [i1,i2] in Indices G & [j1,j2] in Indices G & g/.i=G*(i1,i2) &
g/.(i+ 1)=G*(j1,j2);
w+i in dom f by A60,A59,A64;
hence |.i1-j1.|+|.i2-j2.|=1 by A1,A66,A67,A68;
end;
A69: dom g = Seg len g by FINSEQ_1:def 3;
thus rng g c= rng f
proof
let z be object;
assume z in rng g;
then consider i being Element of NAT such that
A70: i in dom g and
A71: z=g/.i by PARTFUN2:2;
A72: w+i in dom f by A60,A57,A69,A70;
z=f1/.(w+i) & f1/.(w+i)=f/.(w+i) by A60,A57,A69,A70,A71;
hence thesis by A72,PARTFUN2:2;
end;
n+1<=m by A54,NAT_1:13;
then
A73: n+1<=m+1 by NAT_1:13;
then
A74: 1<=l by XREAL_1:19;
then 1 in Seg l by FINSEQ_1:1;
then g/.1 = f1/.(n-1+1) by A57
.= f/.n by A5,A55,FINSEQ_4:71;
hence g/.1 in rng Col(G,1) by A2,A10,XBOOLE_0:def 4;
len g in dom g by A57,A74,FINSEQ_3:25;
then g/.len g= f1/.(w+ww) by A57,A59
.= f/.m by A5,A58,FINSEQ_4:71;
hence g/.len g in rng Col(G,width G) by A3,A6,XBOOLE_0:def 4;
now
let i;
assume
A75: i in dom g;
then w+i in dom f by A60,A59;
then consider i1,i2 be Nat such that
A76: [i1,i2] in Indices G & f/.(w+i)=G*(i1,i2) by A1;
take i1,i2;
g/.i=f1/.(w+i) by A57,A59,A75;
hence [i1,i2] in Indices G & g/.i=G*(i1,i2) by A60,A59,A75,A76;
end;
hence thesis by A57,A73,A63,XREAL_1:19;
end;
end;
theorem
k in dom G & f is_sequence_on G & f/.len f in rng Line(G,len G) & n in
dom f & f/.n in rng Line(G,k) implies (for i st k<=i & i<=len G ex j st j in
dom f & n<=j & f/.j in rng Line(G,i)) & for i st k<i & i<=len G ex j st j in
dom f & n<j & f/.j in rng Line(G,i)
proof
assume that
A1: k in dom G and
A2: f is_sequence_on G & f/.len f in rng Line(G,len G) and
A3: n in dom f and
A4: f/.n in rng Line(G,k);
defpred P[Nat] means
k<=$1 & $1<=len G implies ex j st j in dom f
& n<=j & f/.j in rng Line(G,$1);
A5: 1<=k by A1,FINSEQ_3:25;
A6: 1<=n & n<=len f by A3,FINSEQ_3:25;
A7: for i st P[i] holds P[i+1]
proof
let i such that
A8: P[i];
assume that
A9: k<=i+1 and
A10: i+1<=len G;
per cases by A9,XXREAL_0:1;
suppose
A11: k=i+1;
take j=n;
thus j in dom f & n<=j & f/.j in rng Line(G,i+1) by A3,A4,A11;
end;
suppose
A12: k<i+1;
then k<=i by NAT_1:13;
then
A13: 1<=i by A5,XXREAL_0:2;
i<=len G by A10,NAT_1:13;
then
A14: i in dom G by A13,FINSEQ_3:25;
1<=i+1 by A5,A12,XXREAL_0:2;
then
A15: i+1 in dom G by A10,FINSEQ_3:25;
defpred P[Nat] means $1 in dom f & n<=$1 & f/.$1 in rng Line(G,i);
A16: for j be Nat st P[j] holds j<=len f by FINSEQ_3:25;
A17: ex j be Nat st P[j] by A8,A10,A12,NAT_1:13;
consider ma be Nat such that
A18: P[ma] & for j be Nat st P[j] holds j<=ma from NAT_1:sch 6(A16
,A17 );
A19: now
let j such that
A20: j in dom f & f/.j in rng Line(G,i);
now
per cases;
suppose
j<n;
hence j<=ma by A18,XXREAL_0:2;
end;
suppose
n<=j;
hence j<=ma by A18,A20;
end;
end;
hence j<=ma;
end;
take j=ma+1;
A21: 1<=len f by A6,XXREAL_0:2;
hence j in dom f by A2,A14,A15,A18,A19,Th21;
ma<=ma+1 by NAT_1:11;
hence n<=j & f/.j in rng Line(G,i+1) by A2,A14,A15,A18,A21,A19,Th21,
XXREAL_0:2;
end;
end;
A22: P[0] by A1,FINSEQ_3:25;
thus
A23: for i holds P[i] from NAT_1:sch 2(A22,A7);
let i;
assume that
A24: k<i and
A25: i<=len G;
consider j such that
A26: j in dom f and
A27: n<=j and
A28: f/.j in rng Line(G,i) by A23,A24,A25;
take j;
thus j in dom f by A26;
1<=i by A5,A24,XXREAL_0:2;
then i in dom G by A25,FINSEQ_3:25;
then n<>j by A1,A4,A24,A28,Th2;
hence thesis by A27,A28,XXREAL_0:1;
end;