:: Introduction to Go-Board - Part I. Basic Notations
:: by Jaros{\l}aw Kotowicz and Yatsuka Nakamura
::
:: Received August 24, 1992
:: Copyright (c) 1992-2021 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 *>;
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: km;
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
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=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;
A60: n+1 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**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**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;
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;
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) &
k0;
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 len G;
then m0 & i+n in
dom f & f/.(i+n) in rng Line(G,l) & l in dom G holds m0 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: ml & 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 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;
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) & k0;
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 width G;
then m0 & i+n in
dom f & f/.(i+n) in rng Col(G,l) & l in Seg width G holds m0 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: ml & 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
m0;
i+1<=len f by A10,FINSEQ_3:25;
then
A14: i<=len f by NAT_1:13;
A15: im & i2=m+1;
hence thesis by A26,XXREAL_0:2;
end;
suppose
i2 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{} & 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,FINSEQ_1:40;
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: nj by A1,A4,A24,A28,Th2;
hence thesis by A27,A28,XXREAL_0:1;
end;
*