:: Introduction to Go-Board - Part II.
:: Go-Board Determined by Finite Sequence of point from ${\calE}^2_{\rm T}$
:: 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, GOBOARD1,
NAT_1, XBOOLE_0, CARD_1, ARYTM_3, XXREAL_0, TARSKI, ARYTM_1, RELAT_1,
ORDINAL4, PARTFUN1, FUNCT_1, RLTOPSP1, TOPREAL1, MCART_1, MATRIX_1,
INCSP_1, ZFMISC_1, TREES_1, ORDINAL2, COMPLEX1, STRUCT_0, GOBOARD2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1,
FINSEQ_1, VALUED_0, STRUCT_0, PRE_TOPC, SEQ_4, MATRIX_0, MATRIX_1,
RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, XXREAL_0;
constructors PARTFUN1, SQUARE_1, NAT_1, COMPLEX1, SEQ_4, TOPREAL1, GOBOARD1,
XXREAL_2, SEQM_3, RELSET_1, DOMAIN_1, BINOP_2, RVSUM_1, REAL_1;
registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, EUCLID,
VALUED_0, CARD_1, SEQM_3, SEQ_4, INT_1, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, TOPREAL1, GOBOARD1, XBOOLE_0;
equalities TOPREAL1, XBOOLE_0;
expansions TOPREAL1, GOBOARD1, XBOOLE_0;
theorems TARSKI, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, SEQ_4,
FINSEQ_2, MATRIX_0, EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, FINSEQ_4,
FINSEQ_3, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, COMPLEX1,
XXREAL_0, ORDINAL1, PARTFUN1, SEQM_3, RLTOPSP1;
schemes NAT_1, MATRIX_0, FINSEQ_4;
begin
reserve p,p1,p2,q for Point of TOP-REAL 2,
f,f1,f2,g,g1,g2 for FinSequence of TOP-REAL 2,
r,s for Real,
n,m,i,j,k for Nat,
G for Go-board,
x for set;
theorem
(for n,m st m>n+1 & n in dom f & n+1 in dom f & m in dom f & m+1 in
dom f holds LSeg(f,n) misses LSeg(f,m)) implies f is s.n.c.
proof
assume
A1: for n,m st m>n+1 & n in dom f & n+1 in dom f & m in dom f & m+1 in
dom f holds LSeg(f,n) misses LSeg(f,m);
let n,m be Nat such that
A2: m>n+1;
A3: n <= n+1 & m <= m+1 by NAT_1:11;
per cases;
suppose
n in dom f & n+1 in dom f & m in dom f & m+1 in dom f;
hence thesis by A1,A2;
end;
suppose
not(n in dom f & n+1 in dom f & m in dom f & m+1 in dom f);
then
not(1 <= n & n <= len f & 1 <= n+1 & n+1<= len f & 1 <= m & m <= len f
& 1 <= m+1 & m+1<= len f) by FINSEQ_3:25;
then not(1 <= n & n+1 <= len f & 1 <= m & m+1 <= len f) by A3,XXREAL_0:2;
then LSeg(f,m)={} or LSeg(f,n)={} by TOPREAL1:def 3;
hence thesis;
end;
end;
theorem
f is unfolded s.n.c. one-to-one & f/.len f in LSeg(f,i) & i in dom f &
i+1 in dom f implies i+1=len f
proof
assume that
A1: f is unfolded and
A2: f is s.n.c. and
A3: f is one-to-one and
A4: f/.len f in LSeg(f,i) and
A5: i in dom f and
A6: i+1 in dom f and
A7: i+1<>len f;
A8: 1<=i by A5,FINSEQ_3:25;
A9: i<=len f by A5,FINSEQ_3:25;
then reconsider l=len f - 1 as Element of NAT by A8,INT_1:5,XXREAL_0:2;
1<=len f by A8,A9,XXREAL_0:2;
then
A10: l+1 in dom f by FINSEQ_3:25;
A11: i+1<=len f by A6,FINSEQ_3:25;
then i+1<len f by A7,XXREAL_0:1;
then
A12: i+1+1<=len f by NAT_1:13;
then
A13: i+1<=len f - 1 by XREAL_1:19;
i<=l by A11,XREAL_1:19;
then
A14: 1<=l by A8,XXREAL_0:2;
then
A15: f/.(l+1) in LSeg(f,l) by TOPREAL1:21;
1<=i+1 by A6,FINSEQ_3:25;
then
A16: f/.(i+2) in LSeg(f,i+1) by A12,TOPREAL1:21;
l<=len f by XREAL_1:43;
then
A17: l in dom f by A14,FINSEQ_3:25;
l<>l+1;
then
A18: f/.l<>f/.(l+1) by A3,A17,A10,PARTFUN2:10;
i+1+1=i+(1+1);
then
A19: LSeg(f,i)/\ LSeg(f,i+1)={f/.(i+1)} by A1,A8,A12;
now
per cases;
suppose
A20: l=i+1;
then f/.len f in LSeg(f,i) /\ LSeg(f,i+1) by A4,A16,XBOOLE_0:def 4;
hence contradiction by A18,A19,A20,TARSKI:def 1;
end;
suppose
l<>i+1;
then i+1<l by A13,XXREAL_0:1;
then LSeg(f,i) misses LSeg(f,l) by A2;
then LSeg(f,i) /\ LSeg(f,l) = {};
hence contradiction by A4,A15,XBOOLE_0:def 4;
end;
end;
hence contradiction;
end;
theorem Th3:
k<>0 & len f = k+1 implies L~f = L~(f|k) \/ LSeg(f,k)
proof
assume that
A1: k<>0 and
A2: len f = k+1;
A3: 0+1<=k by A1,NAT_1:13;
set f1 = f|k, lf = {LSeg(f,i): 1<=i & i+1 <= len f}, l1 = {LSeg(f1,j): 1<=j
& j+1 <= len f1};
k<=len f by A2,NAT_1:13;
then
A4: len(f|k)=k by FINSEQ_1:59;
thus L~f c= L~(f|k) \/ LSeg(f,k)
proof
let x be object;
assume x in L~f;
then consider X be set such that
A5: x in X and
A6: X in lf by TARSKI:def 4;
consider n such that
A7: X=LSeg(f,n) and
A8: 1<=n and
A9: n+1 <= len f by A6;
now
per cases;
suppose
n+1 = len f;
hence thesis by A2,A5,A7,XBOOLE_0:def 3;
end;
suppose
A10: n+1 <> len f;
A11: 1<=n+1 by A8,NAT_1:13;
n<=k by A2,A9,XREAL_1:6;
then
A12: n in dom f1 by A4,A8,FINSEQ_3:25;
A13: n+1 < len f by A9,A10,XXREAL_0:1;
then n+1 <= k by A2,NAT_1:13;
then n+1 in dom f1 by A4,A11,FINSEQ_3:25;
then
A14: X=LSeg(f1,n) by A7,A12,TOPREAL3:17;
n+1<=k by A2,A13,NAT_1:13;
then X in l1 by A4,A8,A14;
then x in union l1 by A5,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
A15: k<=k+1 by NAT_1:11;
let x be object such that
A16: x in L~f1 \/ LSeg(f,k);
now
per cases by A16,XBOOLE_0:def 3;
suppose
x in L~f1;
then consider X be set such that
A17: x in X and
A18: X in l1 by TARSKI:def 4;
consider n such that
A19: X=LSeg(f1,n) and
A20: 1<=n and
A21: n+1 <= len f1 by A18;
n<=n+1 by NAT_1:11;
then n<=len f1 by A21,XXREAL_0:2;
then
A22: n in dom f1 by A20,FINSEQ_3:25;
1<=n+1 by NAT_1:11;
then n+1 in dom f1 by A21,FINSEQ_3:25;
then
A23: X=LSeg(f,n) by A19,A22,TOPREAL3:17;
n+1<=len f by A2,A15,A4,A21,XXREAL_0:2;
then X in lf by A20,A23;
hence thesis by A17,TARSKI:def 4;
end;
suppose
A24: x in LSeg(f,k);
LSeg(f,k) in lf by A2,A3;
hence thesis by A24,TARSKI:def 4;
end;
end;
hence thesis;
end;
theorem
1 < k & len f = k+1 & f is unfolded s.n.c. implies L~(f|k) /\ LSeg(f,k
) = {f/.k}
proof
assume that
A1: 1<k and
A2: len f = k+1 and
A3: f is unfolded and
A4: f is s.n.c.;
set f1 = f|k;
A5: len f1=k by A2,FINSEQ_1:59,NAT_1:11;
reconsider k1=k-1 as Element of NAT by A1,INT_1:5;
set f2 = f1|k1, l2 = {LSeg(f2,m): 1<=m & m+1<=len f2};
A6: dom f1=Seg len f1 by FINSEQ_1:def 3;
A7: k in Seg k by A1,FINSEQ_1:1;
A8: dom f2=Seg len f2 by FINSEQ_1:def 3;
A9: k1<k by XREAL_1:44;
A10: k1<=k by XREAL_1:44;
then
A11: len f2 = k1 by A5,FINSEQ_1:59;
A12: Seg k1 c= Seg k by A10,FINSEQ_1:5;
L~f2 misses LSeg(f,k)
proof
assume not thesis;
then consider x be object such that
A13: x in L~f2 and
A14: x in LSeg(f,k) by XBOOLE_0:3;
consider X be set such that
A15: x in X and
A16: X in l2 by A13,TARSKI:def 4;
consider n such that
A17: X=LSeg(f2,n) and
A18: 1<=n and
A19: n+1<=len f2 by A16;
A20: n in dom f2 & n+1 in dom f2 by A18,A19,SEQ_4:134;
then LSeg(f2,n)=LSeg(f1,n) by TOPREAL3:17;
then LSeg(f2,n)=LSeg(f,n) by A6,A12,A8,A5,A11,A20,TOPREAL3:17;
then
A21: LSeg(f,n) meets LSeg(f,k) by A14,A15,A17,XBOOLE_0:3;
n+1<k by A9,A11,A19,XXREAL_0:2;
hence contradiction by A4,A21;
end;
then
A22: L~f2 /\ LSeg(f,k) = {};
A23: k+1=k1+(1+1);
1+1<=k by A1,NAT_1:13;
then
A24: 1<=k1 by XREAL_1:19;
then
A25: k1 in Seg k by A10,FINSEQ_1:1;
k1+1 in Seg k by A1,FINSEQ_1:1;
then L~f1=L~f2 \/ LSeg(f1,k1) by A24,A5,Th3;
hence L~f1 /\ LSeg(f,k) = {} \/ LSeg(f1,k1) /\ LSeg(f,k) by A22,XBOOLE_1:23
.= LSeg(f,k1) /\ LSeg(f,k1+1) by A6,A7,A25,A5,TOPREAL3:17
.= {f/.k} by A2,A3,A24,A23;
end;
theorem
len f1 < n & n+1 <= len (f1^f2) & m+len f1 = n implies LSeg(f1^f2,n) =
LSeg(f2,m)
proof
set f = f1^f2;
assume that
A1: len f1 < n and
A2: n+1 <= len f and
A3: m+len f1 = n;
A4: 1<=m by A1,A3,NAT_1:19;
reconsider p=f/.n, q=f/.(n+1) as Point of TOP-REAL 2;
A5: n+1 = m+1+len f1 by A3;
len f=len f1+len f2 by FINSEQ_1:22;
then
A6: m+1<=len f2 by A2,A5,XREAL_1:6;
then
A7: f/.(n+1)=f2/.(m+1) by A5,NAT_1:11,SEQ_4:136;
m <= m + 1 by NAT_1:11;
then m <= len f2 by A6,XXREAL_0:2;
then
A8: f/.n=f2/.m by A3,A4,SEQ_4:136;
0+1<=n by A1,NAT_1:13;
hence LSeg(f,n)=LSeg(p,q) by A2,TOPREAL1:def 3
.=LSeg(f2,m) by A4,A6,A8,A7,TOPREAL1:def 3;
end;
theorem Th6:
L~f c= L~(f^g)
proof
set f1 = f^g, lf = {LSeg(f,i): 1<=i & i+1 <= len f}, l1 = {LSeg(f1,j): 1<=j
& j+1 <= len f1};
let x be object;
assume x in L~f;
then consider X be set such that
A1: x in X and
A2: X in lf by TARSKI:def 4;
consider n such that
A3: X=LSeg(f,n) and
A4: 1<=n and
A5: n+1 <= len f by A2;
n<=n+1 by NAT_1:11;
then n<=len f by A5,XXREAL_0:2;
then
A6: n in dom f by A4,FINSEQ_3:25;
len f1=len f +len g by FINSEQ_1:22;
then len f <= len f1 by XREAL_1:31;
then
A7: n+1 <= len f1 by A5,XXREAL_0:2;
1<=n+1 by XREAL_1:31;
then n+1 in dom f by A5,FINSEQ_3:25;
then X=LSeg(f1,n) by A3,A6,TOPREAL3:18;
then X in l1 by A4,A7;
hence thesis by A1,TARSKI:def 4;
end;
theorem
f is s.n.c. implies f|i is s.n.c.
proof
assume
A1: f is s.n.c.;
set f1 = f|i;
let n,m be Nat;
assume m>n+1;
then LSeg(f,n) misses LSeg(f,m) by A1;
then
A2: LSeg(f,n) /\ LSeg(f,m) = {};
now
A3: m <= m+1 by NAT_1:11;
A4: n <= n+1 by NAT_1:11;
now
per cases;
suppose
A5: n in dom f1;
now
per cases;
suppose
n+1 in dom f1;
then
A6: LSeg(f,n)=LSeg(f1,n) by A5,TOPREAL3:17;
now
per cases;
suppose
A7: m in dom f1;
now
per cases;
suppose
m+1 in dom f1;
hence LSeg(f1,n) /\ LSeg(f1,m) = {} by A2,A6,A7,
TOPREAL3:17;
end;
suppose
not m+1 in dom f1;
then not(1 <= m+1 & m+1<= len f1) by FINSEQ_3:25;
then LSeg(f1,m)={} by NAT_1:11,TOPREAL1:def 3;
hence LSeg(f1,n) /\ LSeg(f1,m) = {};
end;
end;
hence thesis;
end;
suppose
not m in dom f1;
then not(1 <= m & m <= len f1) by FINSEQ_3:25;
then not(1 <= m & m+1 <= len f1) by A3,XXREAL_0:2;
then LSeg(f1,m)={} by TOPREAL1:def 3;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not n+1 in dom f1;
then not(1 <= n+1 & n+1<= len f1) by FINSEQ_3:25;
then LSeg(f1,n)={} by NAT_1:11,TOPREAL1:def 3;
hence thesis;
end;
end;
hence thesis;
end;
suppose
not n in dom f1;
then not(1 <= n & n <= len f1) by FINSEQ_3:25;
then not(1 <= n & n+1 <= len f1) by A4,XXREAL_0:2;
then LSeg(f1,n)={} by TOPREAL1:def 3;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
f1 is special & f2 is special & ((f1/.len f1)`1=(f2/.1)`1 or (f1/.len
f1)`2=(f2/.1)`2) implies f1^f2 is special
proof
assume that
A1: f1 is special and
A2: f2 is special and
A3: (f1/.len f1)`1=(f2/.1)`1 or (f1/.len f1)`2=(f2/.1)`2;
let n be Nat;
set f = f1^f2;
assume that
A4: 1 <= n and
A5: n+1 <= len f;
reconsider n as Element of NAT by ORDINAL1:def 12;
set p =f/.n, q =f/.(n+1);
A6: len f=len f1+len f2 by FINSEQ_1:22;
per cases;
suppose
A7: n+1 <= len f1;
then n+1 in dom f1 by A4,SEQ_4:134;
then
A8: f1/.(n+1)=q by FINSEQ_4:68;
n in dom f1 by A4,A7,SEQ_4:134;
then f1/.n=p by FINSEQ_4:68;
hence thesis by A1,A4,A7,A8;
end;
suppose
len f1 < n+1;
then
A9: len f1<=n by NAT_1:13;
then reconsider n1=n-len f1 as Element of NAT by INT_1:5;
now
per cases;
suppose
A10: n=len f1;
then n in dom f1 by A4,FINSEQ_3:25;
then
A11: p=f1/.n by FINSEQ_4:68;
len f2 >= 1 by A5,A6,A10,XREAL_1:6;
hence p`1=q`1 or p`2=q`2 by A3,A10,A11,SEQ_4:136;
end;
suppose
n<>len f1;
then len f1<n by A9,XXREAL_0:1;
then len f1+1<=n by NAT_1:13;
then
A12: 1<=n1 by XREAL_1:19;
A13: n+1 = n1 + 1 + len f1;
then
A14: n1+1<=len f2 by A5,A6,XREAL_1:6;
then
A15: f2/.(n1+1)=q by A13,NAT_1:11,SEQ_4:136;
n1 + 1 >= n1 by NAT_1:11;
then n = n1 + len f1 & n1 <= len f2 by A14,XXREAL_0:2;
then f2/.n1=p by A12,SEQ_4:136;
hence p`1=q`1 or p`2=q`2 by A2,A12,A14,A15;
end;
end;
hence thesis;
end;
end;
theorem Th9:
f <> {} implies X_axis(f) <> {}
proof
A1: len X_axis(f) = len f by GOBOARD1:def 1;
assume f <> {} & X_axis(f) = {};
hence contradiction by A1;
end;
theorem Th10:
f <> {} implies Y_axis(f) <> {}
proof
A1: len Y_axis(f) = len f by GOBOARD1:def 2;
assume f <> {} & Y_axis(f) = {};
hence contradiction by A1;
end;
registration
let f be non empty FinSequence of TOP-REAL 2;
cluster X_axis f -> non empty;
coherence by Th9;
cluster Y_axis f -> non empty;
coherence by Th10;
end;
theorem Th11:
f is special implies
for n being Nat st n in dom f & n+1 in dom f
for i,j,m,k being Nat
st [i,j] in Indices G & [m,k] in Indices G & f/.n=G*(i,j) & f/.(n+1
)=G*(m,k) holds i=m or k=j
proof
assume
A1: f is special;
let n be Nat;
assume n in dom f & n+1 in dom f;
then
A2: 1 <= n & n +1 <= len f by FINSEQ_3:25;
let i,j,m,k be Nat such that
A3: [i,j] in Indices G and
A4: [m,k] in Indices G and
A5: f/.n=G*(i,j) & f/.(n+1)=G*(m,k);
reconsider cj = Col(G,j), lm = Line(G,m) as FinSequence of TOP-REAL 2;
set xj = X_axis(cj), yj = Y_axis(cj), xm = X_axis(lm), ym = Y_axis(lm);
len cj=len G by MATRIX_0:def 8;
then
A6: dom cj = dom G by FINSEQ_3:29;
assume that
A7: i<>m and
A8: k<>j;
A9: len xm=len lm & dom xm=Seg len xm by FINSEQ_1:def 3,GOBOARD1:def 1;
A10: len xj=len cj by GOBOARD1:def 1;
then
A11: dom xj = dom cj by FINSEQ_3:29;
A12: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
then
A13: i in dom G by A3,ZFMISC_1:87;
then cj/.i = cj.i by A6,PARTFUN1:def 6;
then
A14: G*(i,j)=cj/.i by A13,MATRIX_0:def 8;
then
A15: xj.i=G*(i,j)`1 by A13,A6,A11,GOBOARD1:def 1;
A16: m in dom G by A4,A12,ZFMISC_1:87;
then cj/.m = cj.m by A6,PARTFUN1:def 6;
then
A17: G*(m,j)=cj/.m by A16,MATRIX_0:def 8;
then
A18: xj.m=G*(m,j)`1 by A16,A6,A11,GOBOARD1:def 1;
A19: ym is increasing by A16,GOBOARD1:def 6;
A20: xm is constant by A16,GOBOARD1:def 4;
A21: dom yj=Seg len yj by FINSEQ_1:def 3;
A22: dom xj=Seg len xj & len yj=len cj by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A23: yj.m=G*(m,j)`2 by A16,A10,A21,A6,A11,A17,GOBOARD1:def 2;
A24: j in Seg width G by A3,A12,ZFMISC_1:87;
then
A25: xj is increasing by GOBOARD1:def 7;
A26: len lm=width G by MATRIX_0:def 7;
then
A27: dom lm = Seg width G by FINSEQ_1:def 3;
then lm/.j = lm.j by A24,PARTFUN1:def 6;
then
A28: G*(m,j)=lm/.j by A24,MATRIX_0:def 7;
then
A29: xm.j=G*(m,j)`1 by A24,A26,A9,GOBOARD1:def 1;
A30: k in Seg width G by A4,A12,ZFMISC_1:87;
then lm/.k = lm.k by A27,PARTFUN1:def 6;
then
A31: G*(m,k)=lm/.k by A30,MATRIX_0:def 7;
then
A32: xm.k=G*(m,k)`1 by A30,A26,A9,GOBOARD1:def 1;
A33: yj is constant by A24,GOBOARD1:def 5;
A34: len ym=len lm & dom ym=Seg len ym by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A35: ym.j=G*(m,j)`2 by A24,A26,A28,GOBOARD1:def 2;
A36: ym.k=G*(m,k)`2 by A30,A26,A34,A31,GOBOARD1:def 2;
A37: yj.i=G*(i,j)`2 by A13,A10,A22,A21,A6,A11,A14,GOBOARD1:def 2;
now
per cases by A1,A5,A2;
suppose
A38: G*(i,j)`1=G*(m,k)`1;
now
per cases by A7,XXREAL_0:1;
suppose
i>m;
then G*(m,j)`1<G*(i,j)`1 by A13,A16,A6,A11,A25,A15,A18,SEQM_3:def 1;
hence contradiction by A24,A30,A26,A9,A20,A29,A32,A38,SEQM_3:def 10;
end;
suppose
i<m;
then G*(m,j)`1>G*(i,j)`1 by A13,A16,A6,A11,A25,A15,A18,SEQM_3:def 1;
hence contradiction by A24,A30,A26,A9,A20,A29,A32,A38,SEQM_3:def 10;
end;
end;
hence contradiction;
end;
suppose
A39: G*(i,j)`2=G*(m,k)`2;
now
per cases by A8,XXREAL_0:1;
suppose
k>j;
then G*(m,j)`2<G*(m,k)`2 by A24,A30,A26,A34,A19,A35,A36,SEQM_3:def 1;
hence contradiction by A13,A16,A10,A22,A21,A6,A11,A33,A37,A23,A39,
SEQM_3:def 10;
end;
suppose
k<j;
then G*(m,j)`2>G*(m,k)`2 by A24,A30,A26,A34,A19,A35,A36,SEQM_3:def 1;
hence contradiction by A13,A16,A10,A22,A21,A6,A11,A33,A37,A23,A39,
SEQM_3:def 10;
end;
end;
hence contradiction;
end;
end;
hence contradiction;
end;
theorem
(for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)) & f
is special &
(for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1))
implies ex g st g is_sequence_on G & L~f = L~g & g/.1=f/.1 & g/.len g=f/.len f
& len f<=len g
proof
defpred P[Nat] means for f st len f=$1 &
(for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)) & f is special &
(for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1))
ex g st g is_sequence_on G & L~f = L~g &
g/.1=f/.1 & g/.len g=f/.len f & len f<=len g;
A1: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
let f such that
A3: len f=k+1 and
A4: for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j)
and
A5: f is special and
A6: for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1);
A7: dom f = Seg len f by FINSEQ_1:def 3;
now
per cases;
suppose
A8: k=0;
take g=f;
A9: dom f = {1} by A3,A8,FINSEQ_1:2,def 3;
now
let n be Nat;
assume that
A10: n in dom g and
A11: n+1 in dom g;
n=1 by A9,A10,TARSKI:def 1;
hence
for i1,i2,j1,j2 be Nat st [i1,i2] in Indices G & [j1
,j2] in Indices G & g/.n=G*(i1,i2) & g/.(n+1)=G*(j1,j2)
holds |.i1-j1.|+|.i2-j2.|=1 by A9,A11,TARSKI:def 1;
end;
hence g is_sequence_on G by A4;
thus L~f=L~g & g/.1=f/.1 & g/.len g=f/.len f & len f<=len g;
end;
suppose
A12: k<>0;
then
A13: 0+1<=k by NAT_1:13;
then
A14: k in Seg k by FINSEQ_1:1;
A15: 1 in Seg k by A13,FINSEQ_1:1;
A16: k<=k+1 by NAT_1:11;
then
A17: k in dom f by A3,A7,A13,FINSEQ_1:1;
then consider i1,i2 be Nat such that
A18: [i1,i2] in Indices G and
A19: f/.k=G*(i1,i2) by A4;
reconsider l1 = Line(G,i1), c1 = Col(G,i2) as FinSequence of TOP-REAL
2;
set x1 = X_axis(l1), y1 = Y_axis(l1), x2 = X_axis(c1), y2 = Y_axis(c1);
A20: dom y1=Seg len y1 & len y1=len l1 by FINSEQ_1:def 3,GOBOARD1:def 2;
len y2=len c1 by GOBOARD1:def 2;
then
A21: dom y2 = dom c1 by FINSEQ_3:29;
len x2=len c1 by GOBOARD1:def 1;
then
A22: dom x2 = dom c1 by FINSEQ_3:29;
set f1=f|k;
A23: len (f|k)=k by A3,FINSEQ_1:59,NAT_1:11;
A24: dom(f|k)=Seg len(f|k) by FINSEQ_1:def 3;
A25: now
let n be Nat;
assume
A26: n in dom f1;
then n in dom f by A17,A23,A24,FINSEQ_4:71;
then consider i,j being Nat such that
A27: [i,j] in Indices G & f/.n=G*(i,j) by A4;
take i,j;
thus [i,j] in Indices G & f1/.n=G*(i,j) by A17,A23,A24,A26,A27,
FINSEQ_4:71;
end;
A28: f1 is special
proof
let n be Nat;
assume that
A29: 1 <= n and
A30: n+1 <= len f1;
n <= n+1 by NAT_1:11;
then n <= len f1 by A30,XXREAL_0:2;
then n in dom f1 by A29,FINSEQ_3:25;
then
A31: f1/.n=f/.n by A17,A23,A24,FINSEQ_4:71;
1 <= n+1 by NAT_1:11;
then n+1 in dom f1 by A30,FINSEQ_3:25;
then
A32: f1/.(n+1)=f/.(n+1) by A17,A23,A24,FINSEQ_4:71;
n+1 <= len f by A3,A16,A23,A30,XXREAL_0:2;
hence thesis by A5,A29,A31,A32;
end;
now
let n be Nat;
assume
A33: n in dom f1 & n+1 in dom f1;
then
A34: f1/.n=f/.n & f1/.(n+1)=f/.(n+1) by A17,A23,A24,FINSEQ_4:71;
n in dom f & n+1 in dom f by A17,A23,A24,A33,FINSEQ_4:71;
hence f1/.n <> f1/.(n+1) by A6,A34;
end;
then consider g1 such that
A35: g1 is_sequence_on G and
A36: L~g1=L~f1 and
A37: g1/.1=f1/.1 and
A38: g1/.len g1=f1/.len f1 and
A39: len f1<=len g1 by A2,A23,A25,A28;
A40: for n being Nat st n in dom g1
ex m,k being Nat st [m,k] in Indices G & g1/.n=G*(m,k)
by A35;
A41: for n being Nat st n in dom g1 & n+1 in dom g1
for m,k,i,j being Nat st [m,k]
in Indices G & [i,j] in Indices G & g1/.n = G*(m,k) & g1/.(n+1) = G*(i,j) holds
|.m-i.|+|.k-j.| = 1 by A35;
A42: dom x1=Seg len x1 & len x1=len l1 by FINSEQ_1:def 3,GOBOARD1:def 1;
len c1 = len G by MATRIX_0:def 8;
then
A43: dom c1 = dom G by FINSEQ_3:29;
1<=len f by A3,NAT_1:11;
then
A44: k+1 in dom f by A3,FINSEQ_3:25;
then consider j1,j2 be Nat such that
A45: [j1,j2] in Indices G and
A46: f/.(k+1)=G*(j1,j2) by A4;
A47: Indices G = [:dom G,Seg width G:] by MATRIX_0:def 4;
then
A48: j1 in dom G by A45,ZFMISC_1:87;
A49: i1 in dom G by A18,A47,ZFMISC_1:87;
then
A50: x1 is constant by GOBOARD1:def 4;
A51: i2 in Seg width G by A18,A47,ZFMISC_1:87;
then
A52: x2 is increasing by GOBOARD1:def 7;
A53: y2 is constant by A51,GOBOARD1:def 5;
A54: y1 is increasing by A49,GOBOARD1:def 6;
A55: len l1=width G by MATRIX_0:def 7;
A56: j2 in Seg width G by A45,A47,ZFMISC_1:87;
A57: dom g1 = Seg len g1 by FINSEQ_1:def 3;
now
per cases by A5,A17,A18,A19,A44,A45,A46,Th11;
suppose
A58: i1=j1;
set ppi = G*(i1,i2), pj = G*(i1,j2);
now
per cases by XXREAL_0:1;
case
A59: i2>j2;
j2 in dom l1 by A56,A55,FINSEQ_1:def 3;
then l1/.j2 = l1.j2 by PARTFUN1:def 6;
then
A60: l1/.j2=pj by A56,MATRIX_0:def 7;
then
A61: y1.j2=pj`2 by A56,A20,A55,GOBOARD1:def 2;
i2 in dom l1 by A51,A55,FINSEQ_1:def 3;
then l1/.i2 = l1.i2 by PARTFUN1:def 6;
then
A62: l1/.i2=ppi by A51,MATRIX_0:def 7;
then
A63: y1.i2=ppi`2 by A51,A20,A55,GOBOARD1:def 2;
then
A64: pj`2<ppi`2 by A51,A56,A54,A20,A55,A59,A61,SEQM_3:def 1;
A65: x1.j2=pj`1 by A56,A42,A55,A60,GOBOARD1:def 1;
x1.i2=ppi`1 by A51,A42,A55,A62,GOBOARD1:def 1;
then
A66: ppi`1=pj`1 by A51,A56,A50,A42,A55,A65,SEQM_3:def 10;
reconsider l=i2-j2 as Element of NAT by A59,INT_1:5;
defpred P1[Nat,set] means for m st m=i2-$1 holds $2=G*(i1,m);
set lk={w where w is Point of TOP-REAL 2: w`1=ppi`1 & pj`2<=w
`2 & w`2<=ppi`2};
A67: ppi=|[ppi`1,ppi `2]| by EUCLID:53;
A68: now
let n;
assume n in Seg l;
then
A69: n<=l by FINSEQ_1:1;
l<=i2 by XREAL_1:43;
then reconsider w=i2-n as Element of NAT by A69,INT_1:5
,XXREAL_0:2;
i2-n<=i2 & i2<=width G by A51,FINSEQ_1:1,XREAL_1:43;
then
A70: w<=width G by XXREAL_0:2;
A71: 1<=j2 by A56,FINSEQ_1:1;
i2-l<=i2-n by A69,XREAL_1:13;
then 1<=w by A71,XXREAL_0:2;
then w in Seg width G by A70,FINSEQ_1:1;
hence i2-n is Element of NAT & [i1,i2-n] in Indices G & i2-n
in Seg width G by A47,A49,ZFMISC_1:87;
end;
A72: now
let n be Nat;
assume n in Seg l;
then reconsider m=i2-n as Element of NAT by A68;
take p=G*(i1,m);
thus P1[n,p];
end;
consider g2 such that
A73: len g2 = l & for n being Nat st n in Seg l holds P1[n
,g2/.n] from FINSEQ_4:sch 1(A72);
take g=g1^g2;
A74: dom g2 = Seg l by A73,FINSEQ_1:def 3;
A75: now
let n be Nat;
assume that
A76: n in dom g2 and
A77: n+1 in dom g2;
reconsider m1=i2-n,m2=i2-(n+1) as Element of NAT by A68,A74
,A76,A77;
let l1,l2,l3,l4 be Nat;
assume that
A78: [l1,l2] in Indices G and
A79: [l3,l4] in Indices G and
A80: g2/.n=G*(l1,l2) and
A81: g2/.(n+1)=G*(l3,l4);
[i1,i2-(n+1)] in Indices G & g2/.(n+1)=G*(i1,m2) by A68,A73
,A74,A77;
then
A82: l3=i1 & l4=m2 by A79,A81,GOBOARD1:5;
[i1,i2-n] in Indices G & g2/.n=G*(i1,m1) by A68,A73,A74,A76;
then l1=i1 & l2=m1 by A78,A80,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= 0+|.i2-n-(i2-(n+1)).| by A82,
ABSVALUE:2
.= 1 by ABSVALUE:def 1;
end;
now
let n be Nat;
assume
A83: n in dom g2;
then reconsider m=i2-n as Element of NAT by A68,A74;
reconsider k=i1,m as Nat;
take k,m;
thus [k,m] in Indices G & g2/.n=G*(k,m) by A68,A73,A74,A83;
end;
then
A84: for n being Nat st n in dom g
ex i,j being Nat st [i,j] in Indices G & g/.n=G
*(i, j) by A40,GOBOARD1:23;
now
let l1,l2,l3,l4 be Nat;
assume that
A85: [l1,l2] in Indices G and
A86: [l3,l4] in Indices G and
A87: g1/.len g1=G*(l1,l2) and
A88: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A89: 1 in dom g2;
reconsider m1=i2-1 as Element of NAT by A68,A74,A89;
[i1,i2-1] in Indices G & g2/.1=G*(i1,m1) by A68,A73,A74,A89;
then
A90: l3=i1 & l4=m1 by A86,A88,GOBOARD1:5;
f1/.len f1=f/.k by A17,A23,A14,FINSEQ_4:71;
then l1=i1 & l2=i2 by A38,A18,A19,A85,A87,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=0+|.i2-(i2-1).| by A90,
ABSVALUE:2
.=1 by ABSVALUE:def 1;
end;
then for n being Nat
st n in dom g & n+1 in dom g
for m,k,i,j being Nat st
[m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A41,A75,GOBOARD1:24;
hence g is_sequence_on G by A84;
reconsider m1=i2-l as Element of NAT by ORDINAL1:def 12;
A91: pj=|[pj`1,pj`2]| by EUCLID:53;
A92: LSeg(f,k)=LSeg(pj,ppi) by A3,A13,A19,A46,A58,TOPREAL1:def 3
.= lk by A64,A66,A67,A91,TOPREAL3:9;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1<=len g}, lf = {LSeg(f,j): 1
<=j & j+1<=len f};
A93: len g = len g1 + len g2 by FINSEQ_1:22;
A94: now
let j;
assume that
A95: len g1<=j and
A96: j<=len g;
reconsider w = j-len g1 as Element of NAT by A95,INT_1:5;
let p such that
A97: p=g/.j;
A98: dom l1 = Seg len l1 by FINSEQ_1:def 3;
now
per cases;
suppose
A99: j=len g1;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A100: g/.len g1 = f1/.len f1 by A38,FINSEQ_4:68
.= G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence p`1=G*(i1,i2)`1 by A97,A99;
thus G*(i1,j2)`2<=p`2 & p`2<=G*(i1,i2)`2 by A51,A56,A54
,A20,A55,A59,A63,A61,A97,A99,A100,SEQM_3:def 1;
thus p in rng l1 by A51,A55,A62,A97,A98,A99,A100,
PARTFUN2:2;
end;
suppose
A101: j<>len g1;
A102: w + len g1 = j;
then
A103: w <= len g2 by A93,A96,XREAL_1:6;
A104: j - len g1 <> 0 by A101;
then
A105: w >= 1 by NAT_1:14;
then
A106: w in dom g2 by A103,FINSEQ_3:25;
then reconsider u=i2-w as Element of NAT by A68,A74;
A107: g/.j=g2/.w by A105,A102,A103,SEQ_4:136;
A108: x1.i2=ppi`1 by A51,A42,A55,A62,GOBOARD1:def 1;
A109: u<i2 by A104,XREAL_1:44;
A110: g2/.w=G*(i1,u) by A73,A74,A106;
A111: i2-w in Seg width G by A68,A74,A106;
then u in dom l1 by A55,FINSEQ_1:def 3;
then l1/.u = l1.u by PARTFUN1:def 6;
then
A112: l1/.u=G*( i1,u) by A111,MATRIX_0:def 7;
then
A113: y1.u=G*(i1,u)`2 by A20,A55,A111,GOBOARD1:def 2;
x1.u=G*(i1,u )`1 by A42,A55,A111,A112,GOBOARD1:def 1;
hence
p`1=G*(i1,i2)`1 by A51,A50,A42,A55,A97,A107,A111,A110
,A108,SEQM_3:def 10;
A114: y1.j2=pj`2 by A56,A20,A55,A60,GOBOARD1:def 2;
now
per cases;
suppose
u=j2;
hence G*(i1,j2)`2<=p`2 by A97,A105,A102,A103,A110,
SEQ_4:136;
end;
suppose
A115: u<>j2;
i2-len g2<=u by A103,XREAL_1:13;
then j2<u by A73,A115,XXREAL_0:1;
hence G*(i1,j2)`2<= p`2 by A56,A54,A20,A55,A97,A107
,A111,A110,A113,A114,SEQM_3:def 1;
end;
end;
hence G*(i1,j2)`2<=p`2;
y1.i2=ppi`2 by A51,A20,A55,A62,GOBOARD1:def 2;
hence p`2<= G*(i1,i2)`2 by A51,A54,A20,A55,A97,A107
,A111,A110,A113,A109,SEQM_3:def 1;
thus p in rng l1 by A55,A97,A98,A107,A111,A110,A112,
PARTFUN2:2;
end;
end;
hence p`1=ppi`1 & pj`2<=p`2 & p`2<=ppi`2 & p in rng l1;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A116: x in X and
A117: X in lg by TARSKI:def 4;
consider i such that
A118: X=LSeg(g,i) and
A119: 1<=i and
A120: i+1<=len g by A117;
now
per cases;
suppose
A121: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A121,XXREAL_0:2;
then
A122: i in dom g1 by A119,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A121,FINSEQ_3:25;
then X=LSeg(g1,i) by A118,A122,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A119,A121
;
then
A123: x in L~f1 by A36,A116,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A123;
end;
suppose
A124: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A125: i<=len g by A120,NAT_1:13;
A126: len g1<=i by A124,NAT_1:13;
then
A127: q1 `1=ppi`1 by A94,A125;
A128: q1`2<=ppi`2 by A94,A126,A125;
A129: pj`2<=q1`2 by A94,A126,A125;
q2`1=ppi`1 by A94,A120,A124;
then
A130: q2=|[q1 `1,q2`2]| by A127,EUCLID:53;
A131: q2`2<=ppi`2 by A94,A120,A124;
A132: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A119,A120,
EUCLID:53,TOPREAL1:def 3;
A133: pj`2<= q2`2 by A94,A120,A124;
now
per cases by XXREAL_0:1;
suppose
q1`2>q2`2;
then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2
<=q1`2} by A130,A132,TOPREAL3:9;
then consider p2 such that
A134: p2 =x & p2`1=q1`1 and
A135: q2`2<=p2`2 & p2`2<=q1`2 by A116,A118;
pj`2<=p2`2 & p2`2<=ppi`2 by A128,A133,A135,
XXREAL_0:2;
then
A136: x in LSeg(f,k) by A92,A127,A134;
LSeg(f,k) in lf by A3,A13;
hence thesis by A136,TARSKI:def 4;
end;
suppose
q1`2=q2`2;
then LSeg(g,i)={q1} by A130,A132,RLTOPSP1:70;
then x=q1 by A116,A118,TARSKI:def 1;
then
A137: x in LSeg(f,k) by A92,A127,A129,A128;
LSeg(f,k) in lf by A3,A13;
hence thesis by A137,TARSKI:def 4;
end;
suppose
q1`2<q2`2;
then LSeg(g,i)= {p1: p1`1=q1`1 & q1`2<=p1`2 & p1
`2<=q2`2} by A130,A132,TOPREAL3:9;
then consider p2 such that
A138: p2 =x & p2`1=q1`1 and
A139: q1`2<=p2`2 & p2`2<=q2`2 by A116,A118;
pj`2<=p2`2 & p2`2<=ppi`2 by A129,A131,A139,
XXREAL_0:2;
then
A140: x in LSeg(f,k) by A92,A127,A138;
LSeg(f,k) in lf by A3,A13;
hence thesis by A140,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let x be object;
assume x in L~f;
then
A141: x in L~f1 \/ LSeg(f,k) by A3,A12,Th3;
now
per cases by A141,XBOOLE_0:def 3;
suppose
A142: x in L~f1;
L~g1 c= L~g by Th6;
hence thesis by A36,A142;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A143: p1=x and
A144: p1`1=ppi`1 and
A145: pj`2<=p1`2 and
A146: p1`2<=ppi`2 by A92;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st
q=g/.$1 holds q`2>=p1`2;
A147: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A93,XREAL_1:31;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A148: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A38,A148,FINSEQ_4:68
.=G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence thesis by A146;
end;
end;
A149: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A150: P2[ma] & for n be Nat st P2[n] holds n<=ma
from NAT_1:sch 6(A149,A147);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A151: ma=len g;
j2+1<=i2 by A59,NAT_1:13;
then
A152: 1<=l by XREAL_1:19;
then 0+1<=ma by A73,A93,A151,XREAL_1:7;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
A153: m1 + 1 = ma;
len g1+1<=ma by A73,A93,A151,A152,XREAL_1:7;
then
A154: m1 >= len g1 by A153,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1
& pj`2<=e`2 & e`2<=q`2};
A155: i2-l=j2;
A156: l in dom g2 by A74,A152,FINSEQ_1:1;
then
A157: g/.ma=g2/.l by A73,A93,A151,FINSEQ_4:69
.= pj by A73,A74,A156,A155;
then p1`2<=pj`2 by A150;
then
A158: p1`2=pj`2 by A145,XXREAL_0:1;
A159: m1 <= len g by A151,A153,NAT_1:11;
then
A160: q`1=ppi`1 by A94,A154;
A161: pj`2<=q`2 by A94,A154,A159;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A162: 1<=m1 by A154,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg (g,m1)=LSeg(pj,q) by A151
,A157,A153,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A66,A91,A160,A161,TOPREAL3:9;
then
A163: p1 in LSeg(g,m1) by A144,A158,A161;
LSeg(g,m1) in lg by A151,A153,A162;
hence thesis by A143,A163,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A150,XXREAL_0:1;
then
A164: ma+1 <= len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of
TOP-REAL 2;
set lma = {p2: p2`1=ppi`1 & qa1`2<=p2`2 & p2`2<=qa`2
};
A165: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A166: p1`2<=qa`2 by A150;
A167: len g1<=ma+1 by A150,NAT_1:13;
then
A168: qa1 `1 = ppi`1 by A94,A164;
A169: now
assume p1`2<=qa1`2;
then for q holds q=g/.(ma+1) implies p1`2<=q`2;
then ma+1<=ma by A150,A164,A167;
hence contradiction by XREAL_1:29;
end;
A170: qa`1=ppi`1 & qa =|[qa`1,qa`2]| by A94,A150,EUCLID:53;
A171: 1<=ma by A13,A23,A39,A150,NAT_1:13;
then LSeg(g,ma)=LSeg(qa1,qa) by A164,TOPREAL1:def 3
.= lma by A166,A169,A168,A170,A165,TOPREAL3:9
,XXREAL_0:2;
then
A172: x in LSeg(g,ma) by A143,A144,A166,A169;
LSeg(g,ma) in lg by A171,A164;
hence thesis by A172,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A37,FINSEQ_4:68
.=f/.1 by A17,A15,FINSEQ_4:71;
A173: len g=len g1 + len g2 by FINSEQ_1:22;
j2+1<=i2 by A59,NAT_1:13;
then
A174: 1<=l by XREAL_1:19;
then
A175: l in dom g2 by A74,FINSEQ_1:1;
hence g/.len g=g2/.l by A73,A173,FINSEQ_4:69
.=G*(i1,m1) by A73,A74,A175
.=f/.len f by A3,A46,A58;
thus len f<=len g by A3,A23,A39,A73,A174,A173,XREAL_1:7;
end;
case
i2=j2;
hence contradiction by A6,A17,A19,A44,A46,A58;
end;
case
A176: i2<j2;
set lk={w where w is Point of TOP-REAL 2: w`1=ppi`1 & ppi`2<=w
`2 & w`2<= pj`2};
A177: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
reconsider l=j2-i2 as Element of NAT by A176,INT_1:5;
deffunc F(Nat) = G*(i1,i2+$1);
consider g2 such that
A178: len g2=l & for n being Nat st n in dom g2 holds g2/.
n=F(n) from FINSEQ_4:sch 2;
take g=g1^g2;
A179: now
let n;
A180: n<=i2+n by NAT_1:11;
assume
A181: n in Seg l;
then n<=l by FINSEQ_1:1;
then
A182: i2+n<=l+i2 by XREAL_1:7;
j2<=width G by A56,FINSEQ_1:1;
then
A183: i2+n<=width G by A182,XXREAL_0:2;
1<=n by A181,FINSEQ_1:1;
then 1<=i2+n by A180,XXREAL_0:2;
hence i2+n in Seg width G by A183,FINSEQ_1:1;
hence [i1,i2+n] in Indices G by A47,A49,ZFMISC_1:87;
end;
A184: dom g2 = Seg len g2 by FINSEQ_1:def 3;
now
let n be Nat such that
A185: n in dom g2;
take m=i1,k=i2+n;
thus [m,k] in Indices G & g2/.n=G*(m,k) by A178,A179,A184
,A185;
end;
then
A186: for n being Nat st n in dom g
ex i,j being Nat st [i,j] in Indices G & g/.n=
G*(i,j) by A40,GOBOARD1:23;
A187: now
let n be Nat;
assume that
A188: n in dom g2 and
A189: n+1 in dom g2;
let l1,l2,l3,l4 be Nat;
assume that
A190: [l1,l2] in Indices G and
A191: [l3,l4] in Indices G and
A192: g2/.n=G*(l1,l2) and
A193: g2/.(n+1)=G*(l3,l4);
g2/.(n+1)=G*(i1,i2+(n+1)) & [i1,i2+(n+1)] in Indices G
by A178,A179,A184,A189;
then
A194: l3=i1 & l4=i2+(n+1) by A191,A193,GOBOARD1:5;
g2/.n=G*(i1,i2+n) & [i1,i2+n] in Indices G by A178,A179,A184
,A188;
then l1=i1 & l2=i2+n by A190,A192,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= 0+|.i2+n-(i2+(n+1)).| by A194,
ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
now
let l1,l2,l3,l4 be Nat;
assume that
A195: [ l1,l2] in Indices G and
A196: [l3,l4] in Indices G and
A197: g1/.len g1=G*(l1, l2) and
A198: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A199: 1 in dom g2;
g2/.1=G* (i1,i2+1) & [i1,i2+1] in Indices G by A178,A179,A184
,A199;
then
A200: l3=i1 & l4=i2+1 by A196,A198,GOBOARD1:5;
f1/.len f1=f/.k by A17,A23,A14,FINSEQ_4:71;
then l1=i1 & l2=i2 by A38,A18,A19,A195,A197,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=0+|.i2-(i2+1).| by A200,
ABSVALUE:2
.=|.i2-i2+-1.|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
then for n being Nat st n in dom g & n+1 in dom g
for m,k,i,j being Nat st
[m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A41,A187,GOBOARD1:24;
hence g is_sequence_on G by A186;
A201: pj=|[pj`1,pj`2]| by EUCLID:53;
j2 in dom l1 by A56,A55,FINSEQ_1:def 3;
then l1/.j2 = l1.j2 by PARTFUN1:def 6;
then
A202: l1/.j2=pj by A56,MATRIX_0:def 7;
then
A203: y1.j2=pj`2 by A56,A20,A55,GOBOARD1:def 2;
i2 in dom l1 by A51,A55,FINSEQ_1:def 3;
then l1/.i2 = l1.i2 by PARTFUN1:def 6;
then
A204: l1/.i2=ppi by A51,MATRIX_0:def 7;
then
A205: y1.i2=ppi`2 by A51,A20,A55,GOBOARD1:def 2;
then
A206: ppi `2<pj`2 by A51,A56,A54,A20,A55,A176,A203,SEQM_3:def 1;
A207: x1.j2=pj`1 by A56,A42,A55,A202,GOBOARD1:def 1;
x1.i2=ppi`1 by A51,A42,A55,A204,GOBOARD1:def 1;
then
A208: ppi`1=pj`1 by A51,A56,A50,A42,A55,A207,SEQM_3:def 10;
A209: LSeg(f,k)=LSeg(ppi,pj) by A3,A13,A19,A46,A58,TOPREAL1:def 3
.= lk by A206,A208,A177,A201,TOPREAL3:9;
A210: dom g2 = Seg l by A178,FINSEQ_1:def 3;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1<=len g}, lf = {LSeg(f,j): 1
<=j & j+1<=len f};
A211: len g = len g1 + len g2 by FINSEQ_1:22;
A212: now
let j;
assume that
A213: len g1<=j and
A214: j<=len g;
reconsider w = j-len g1 as Element of NAT by A213,INT_1:5;
let p such that
A215: p=g/.j;
set u=i2+w;
A216: dom l1 = Seg len l1 by FINSEQ_1:def 3;
now
per cases;
suppose
A217: j=len g1;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A218: g/.len g1 = f1/.len f1 by A38,FINSEQ_4:68
.= G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence p`1=G*(i1,i2)`1 by A215,A217;
thus G*(i1,i2)`2<=p`2 & p`2<=G* (i1,j2)`2 by A51,A56
,A54,A20,A55,A176,A205,A203,A215,A217,A218,SEQM_3:def 1;
thus p in rng l1 by A51,A55,A204,A215,A216,A217,A218,
PARTFUN2:2;
end;
suppose
A219: j<>len g1;
A220: w + len g1 = j;
then
A221: w <= len g2 by A211,A214,XREAL_1:6;
A222: x1 .i2=ppi`1 by A51,A42,A55,A204,GOBOARD1:def 1;
A223: j - len g1 <> 0 by A219;
then
A224: w >= 1 by NAT_1:14;
then
A225: g/.j=g2/.w by A220,A221,SEQ_4:136;
A226: i2<u by A223,XREAL_1:29;
A227: w in dom g2 by A224,A221,FINSEQ_3:25;
then
A228: u in Seg width G by A210,A179;
u in Seg width G by A210,A179,A227;
then u in dom l1 by A55,FINSEQ_1:def 3;
then l1/.u = l1. u by PARTFUN1:def 6;
then
A229: l1/.u=G*(i1,u) by A228,MATRIX_0:def 7;
then
A230: y1.u=G*(i1,u) `2 by A20,A55,A228,GOBOARD1:def 2;
A231: g2/.w=G* (i1,u) by A178,A227;
x1.u=G*(i1,u)`1 by A42,A55,A228,A229,GOBOARD1:def 1;
hence
p`1=G*(i1,i2)`1 by A51,A50,A42,A55,A215,A225,A231,A228
,A222,SEQM_3:def 10;
y1.i2=ppi`2 by A51,A20,A55,A204,GOBOARD1:def 2;
hence G*(i1,i2)`2<= p`2 by A51,A54,A20,A55,A215,A225
,A231,A228,A230,A226,SEQM_3:def 1;
A232: y1.j2=pj`2 by A56,A20,A55,A202,GOBOARD1:def 2;
now
per cases;
suppose
u=j2;
hence
p`2<=G*(i1,j2)`2
by A215,A224,A220,A221,A231,SEQ_4:136;
end;
suppose
A233: u<>j2;
u<=i2+l by A178,A221,XREAL_1:7;
then u<j2 by A233,XXREAL_0:1;
hence
p`2<=G*(i1,j2)`2 by A56,A54,A20,A55,A215,A225,A231
,A228,A230,A232,SEQM_3:def 1;
end;
end;
hence p`2<=G*(i1,j2)`2;
thus p in rng l1 by A55,A215,A216,A225,A231,A228,A229,
PARTFUN2:2;
end;
end;
hence p`1=ppi`1 & ppi`2<=p`2 & p`2<=pj`2 & p in rng l1;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A234: x in X and
A235: X in lg by TARSKI:def 4;
consider i such that
A236: X=LSeg(g,i) and
A237: 1<=i and
A238: i+1 <= len g by A235;
now
per cases;
suppose
A239: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A239,XXREAL_0:2;
then
A240: i in dom g1 by A237,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A239,FINSEQ_3:25;
then X=LSeg(g1,i) by A236,A240,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A237,A239
;
then
A241: x in L~f1 by A36,A234,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A241;
end;
suppose
A242: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A243: i<=len g by A238,NAT_1:13;
A244: len g1<=i by A242,NAT_1:13;
then
A245: q1 `1=ppi`1 by A212,A243;
A246: q1`2<=pj`2 by A212,A244,A243;
A247: ppi`2<=q1`2 by A212,A244,A243;
q2`1=ppi`1 by A212,A238,A242;
then
A248: q2=|[q1 `1,q2`2]| by A245,EUCLID:53;
A249: q2`2<=pj`2 by A212,A238,A242;
A250: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A237,A238,
EUCLID:53,TOPREAL1:def 3;
A251: ppi`2<= q2`2 by A212,A238,A242;
now
per cases by XXREAL_0:1;
suppose
q1`2>q2`2;
then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2
<=q1`2} by A248,A250,TOPREAL3:9;
then consider p2 such that
A252: p2 =x & p2`1=q1`1 and
A253: q2`2<=p2`2 & p2`2<=q1`2 by A234,A236;
ppi`2<=p2`2 & p2`2<=pj`2 by A246,A251,A253,
XXREAL_0:2;
then
A254: x in LSeg(f,k) by A209,A245,A252;
LSeg(f,k) in lf by A3,A13;
hence thesis by A254,TARSKI:def 4;
end;
suppose
q1`2=q2`2;
then LSeg(g,i)={q1} by A248,A250,RLTOPSP1:70;
then x=q1 by A234,A236,TARSKI:def 1;
then
A255: x in LSeg(f,k) by A209,A245,A247,A246;
LSeg(f,k) in lf by A3,A13;
hence thesis by A255,TARSKI:def 4;
end;
suppose
q1`2<q2`2;
then LSeg(g,i)= {p1: p1`1=q1`1 & q1`2<=p1`2 & p1
`2<=q2`2} by A248,A250,TOPREAL3:9;
then consider p2 such that
A256: p2 =x & p2`1=q1`1 and
A257: q1`2<=p2`2 & p2`2<=q2`2 by A234,A236;
ppi`2<=p2`2 & p2`2<=pj`2 by A247,A249,A257,
XXREAL_0:2;
then
A258: x in LSeg(f,k) by A209,A245,A256;
LSeg(f,k) in lf by A3,A13;
hence thesis by A258,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let x be object;
assume x in L~f;
then
A259: x in L~f1 \/ LSeg(f,k) by A3,A12,Th3;
now
per cases by A259,XBOOLE_0:def 3;
suppose
A260: x in L~f1;
L~g1 c= L~g by Th6;
hence thesis by A36,A260;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A261: p1=x and
A262: p1`1=ppi`1 and
A263: ppi`2<=p1`2 and
A264: p1`2<=pj`2 by A209;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st
q=g/.$1 holds q`2<=p1`2;
A265: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A211,XREAL_1:31;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A266: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A38,A266,FINSEQ_4:68
.=G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence thesis by A263;
end;
end;
A267: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A268: P2 [ma] & for n be Nat st P2[n] holds n<=ma
from NAT_1:sch 6 (A267,A265);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A269: ma=len g;
i2+1<=j2 by A176,NAT_1:13;
then
A270: 1<=l by XREAL_1:19;
then 0+1<=ma by A178,A211,A269,XREAL_1:7;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
A271: m1 + 1 = ma;
len g1+1<=ma by A178,A211,A269,A270,XREAL_1:7;
then
A272: m1 >= len g1 by A271,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1
& q`2<=e`2 & e`2<=pj`2};
A273: i2+l=j2;
A274: l in dom g2 by A178,A270,FINSEQ_3:25;
then
A275: g/.ma=g2/.l by A178,A211,A269,FINSEQ_4:69
.= pj by A178,A274,A273;
then pj`2<=p1`2 by A268;
then
A276: p1`2=pj`2 by A264,XXREAL_0:1;
A277: m1 <= len g by A269,A271,NAT_1:11;
then
A278: q`1=ppi`1 by A212,A272;
A279: q`2<=pj`2 by A212,A272,A277;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A280: 1<=m1 by A272,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg (g,m1)=LSeg(pj,q) by A269
,A275,A271,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A208,A201,A278,A279,TOPREAL3:9;
then
A281: p1 in LSeg(g,m1) by A262,A276,A279;
LSeg(g,m1) in lg by A269,A271,A280;
hence thesis by A261,A281,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A268,XXREAL_0:1;
then
A282: ma+1 <= len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of
TOP-REAL 2;
set lma = {p2: p2`1=ppi`1 & qa`2<=p2`2 & p2`2<=qa1`2
};
A283: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A284: qa`2<=p1`2 by A268;
A285: len g1<=ma+1 by A268,NAT_1:13;
then
A286: qa1 `1 = ppi`1 by A212,A282;
A287: now
assume qa1`2<=p1`2;
then for q holds q=g/.(ma+1) implies q`2<=p1`2;
then ma+1<=ma by A268,A282,A285;
hence contradiction by XREAL_1:29;
end;
A288: qa`1=ppi`1 & qa =|[qa`1,qa`2]| by A212,A268,EUCLID:53
;
A289: 1<=ma by A13,A23,A39,A268,NAT_1:13;
then LSeg(g,ma)=LSeg(qa,qa1) by A282,TOPREAL1:def 3
.= lma by A284,A287,A286,A288,A283,TOPREAL3:9
,XXREAL_0:2;
then
A290: x in LSeg(g,ma) by A261,A262,A284,A287;
LSeg(g,ma) in lg by A289,A282;
hence thesis by A290,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A37,FINSEQ_4:68
.=f/.1 by A17,A15,FINSEQ_4:71;
A291: len g=len g1 + l by A178,FINSEQ_1:22;
i2+1<=j2 by A176,NAT_1:13;
then
A292: 1<=l by XREAL_1:19;
then
A293: l in dom g2 by A178,A184,FINSEQ_1:1;
hence g/.len g=g2/.l by A291,FINSEQ_4:69
.=G*(i1,i2+l) by A178,A293
.=f/.len f by A3,A46,A58;
thus len f<=len g by A3,A23,A39,A292,A291,XREAL_1:7;
end;
end;
hence thesis;
end;
suppose
A294: i2=j2;
set ppi = G*(i1,i2), pj = G*(j1,i2);
now
per cases by XXREAL_0:1;
case
A295: i1>j1;
c1/.j1 = c1.j1 by A48,A43,PARTFUN1:def 6;
then
A296: c1/.j1=pj by A48,MATRIX_0:def 8;
then
A297: x2.j1=pj`1 by A48,A43,A22,GOBOARD1:def 1;
c1/.i1 = c1.i1 by A49,A43,PARTFUN1:def 6;
then
A298: c1/.i1=ppi by A49,MATRIX_0:def 8;
then
A299: x2.i1=ppi`1 by A49,A43,A22,GOBOARD1:def 1;
then
A300: pj `1<ppi`1 by A49,A48,A52,A43,A22,A295,A297,SEQM_3:def 1;
A301: y2.j1=pj`2 by A48,A43,A21,A296,GOBOARD1:def 2;
y2.i1=ppi`2 by A49,A43,A21,A298,GOBOARD1:def 2;
then
A302: ppi`2=pj`2 by A49,A48,A53,A43,A21,A301,SEQM_3:def 10;
reconsider l=i1-j1 as Element of NAT by A295,INT_1:5;
defpred P1[Nat,set] means for m st m=i1-$1 holds $2=G*(m,i2);
set lk={w where w is Point of TOP-REAL 2: w`2=ppi`2 & pj`1<=w
`1 & w`1<= ppi`1};
A303: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
A304: now
let n;
assume n in Seg l;
then
A305: n<=l by FINSEQ_1:1;
l<=i1 by XREAL_1:43;
then reconsider w=i1-n as Element of NAT by A305,INT_1:5
,XXREAL_0:2;
i1-n<=i1 & i1<=len G by A49,FINSEQ_3:25,XREAL_1:43;
then
A306: w<=len G by XXREAL_0:2;
A307: 1<=j1 by A48,FINSEQ_3:25;
i1-l<=i1-n by A305,XREAL_1:13;
then 1<=w by A307,XXREAL_0:2;
then w in dom G by A306,FINSEQ_3:25;
hence i1-n is Element of NAT & [i1-n,i2] in Indices G & i1-n
in dom G by A47,A51,ZFMISC_1:87;
end;
A308: now
let n be Nat;
assume n in Seg l;
then reconsider m=i1-n as Element of NAT by A304;
take p=G*(m,i2);
thus P1[n,p];
end;
consider g2 such that
A309: len g2= l & for n being Nat st n in Seg l holds P1[n
,g2/.n] from FINSEQ_4:sch 1(A308);
take g=g1^g2;
A310: dom g2 = Seg l by A309,FINSEQ_1:def 3;
A311: now
let n be Nat;
assume that
A312: n in dom g2 and
A313: n+1 in dom g2;
reconsider m1=i1-n,m2=i1-(n+1) as Element of NAT by A304,A310
,A312,A313;
let l1,l2,l3,l4 be Nat;
assume that
A314: [l1,l2] in Indices G and
A315: [l3,l4] in Indices G and
A316: g2/.n=G*(l1,l2) and
A317: g2/.(n+1)=G*(l3,l4);
[i1-(n+1),i2] in Indices G & g2/.(n+1)=G*(m2,i2) by A304,A309
,A310,A313;
then
A318: l3=m2 & l4=i2 by A315,A317,GOBOARD1:5;
[i1-n,i2] in Indices G & g2/.n=G*(m1,i2) by A304,A309,A310
,A312;
then l1=m1 & l2=i2 by A314,A316,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= |.i1-n-(i1-(n+1)).|+0 by A318,
ABSVALUE:2
.= 1 by ABSVALUE:def 1;
end;
now
let n be Nat;
assume
A319: n in dom g2;
then reconsider m=i1-n as Element of NAT by A304,A310;
reconsider m,k=i2 as Nat;
take m,k;
thus [m,k] in Indices G & g2/.n=G*(m,k) by A304,A309,A310
,A319;
end;
then
A320: for n being Nat st n in dom g
ex i,j being Nat st [i,j] in Indices G & g/.n=
G*(i,j) by A40,GOBOARD1:23;
now
let l1,l2,l3,l4 be Nat;
assume that
A321: [ l1,l2] in Indices G and
A322: [l3,l4] in Indices G and
A323: g1/.len g1=G*(l1, l2) and
A324: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A325: 1 in dom g2;
reconsider m1=i1-1 as Element of NAT by A304,A310,A325;
[i1-1,i2] in Indices G & g2/.1=G*(m1,i2) by A304,A309,A310
,A325;
then
A326: l3=m1 & l4=i2 by A322,A324,GOBOARD1:5;
f1/.len f1=f/.k by A17,A23,A14,FINSEQ_4:71;
then l1=i1 & l2=i2 by A38,A18,A19,A321,A323,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=|.i1-(i1-1).|+0 by A326,
ABSVALUE:2
.=1 by ABSVALUE:def 1;
end;
then for n being Nat st n in dom g & n+1 in dom g
for m,k,i,j being Nat st
[m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A41,A311,GOBOARD1:24;
hence g is_sequence_on G by A320;
reconsider m1=i1-l as Element of NAT by ORDINAL1:def 12;
A327: pj=|[pj`1,pj`2]| by EUCLID:53;
A328: LSeg(f,k)=LSeg(pj,ppi) by A3,A13,A19,A46,A294,TOPREAL1:def 3
.= lk by A300,A302,A303,A327,TOPREAL3:10;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1<=len g}, lf = {LSeg(f,j): 1
<=j & j+1<=len f};
A329: len g = len g1 + len g2 by FINSEQ_1:22;
A330: now
let j;
assume that
A331: len g1<=j and
A332: j<=len g;
reconsider w = j-len g1 as Element of NAT by A331,INT_1:5;
let p such that
A333: p=g/.j;
now
per cases;
suppose
A334: j=len g1;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A335: g/.len g1 = f1/.len f1 by A38,FINSEQ_4:68
.= G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence p`2=G*(i1,i2)`2 by A333,A334;
thus G*(j1,i2)`1<=p`1 & p`1<=G*(i1,i2)`1 by A49,A48,A52
,A43,A22,A295,A299,A297,A333,A334,A335,SEQM_3:def 1;
thus p in rng c1 by A49,A43,A298,A333,A334,A335,
PARTFUN2:2;
end;
suppose
A336: j<>len g1;
A337: w + len g1 = j;
then
A338: w <= len g2 by A329,A332,XREAL_1:6;
A339: j - len g1 <> 0 by A336;
then
A340: w >= 1 by NAT_1:14;
then
A341: w in dom g2 by A338,FINSEQ_3:25;
then reconsider u=i1-w as Element of NAT by A304,A310;
A342: g/.j=g2/.w by A340,A337,A338,SEQ_4:136;
A343: u<i1 by A339,XREAL_1:44;
A344: g2/.w=G*(u,i2) by A309,A310,A341;
A345: y2.i1=G*(i1,i2)`2 by A49,A43,A21,A298,GOBOARD1:def 2;
A346: i1-w in dom G by A304,A310,A341;
c1/.u =c1.u by A43,A304,A310,A341,PARTFUN1:def 6;
then
A347: c1/.u=G*( u,i2) by A346,MATRIX_0:def 8;
then
A348: x2.u=G *(u,i2)`1 by A43,A22,A346,GOBOARD1:def 1;
y2.u=G*(u,i2)`2 by A43,A21,A346,A347,GOBOARD1:def 2;
hence
p`2=G*(i1,i2)`2 by A49,A53,A43,A21,A333,A342,A346,A344
,A345,SEQM_3:def 10;
A349: x2.j1=G*(j1,i2) `1 by A48,A43,A22,A296,GOBOARD1:def 1;
now
per cases;
suppose
u=j1;
hence
G*(j1,i2)`1<=p`1
by A333,A340,A337,A338,A344,SEQ_4:136;
end;
suppose
A350: u<>j1;
i1-len g2<=u by A338,XREAL_1:13;
then j1<u by A309,A350,XXREAL_0:1;
hence
G*(j1,i2)`1<=p`1 by A48,A52,A43,A22,A333,A342,A346
,A344,A348,A349,SEQM_3:def 1;
end;
end;
hence G*(j1,i2)`1<=p`1;
x2.i1=G*(i1,i2)`1 by A49,A43,A22,A298,GOBOARD1:def 1;
hence p`1<=G*(i1,i2)`1 by A49,A52,A43,A22,A333,A342
,A346,A344,A348,A343,SEQM_3:def 1;
thus p in rng c1 by A43,A333,A342,A346,A344,A347,
PARTFUN2:2;
end;
end;
hence p`2=ppi`2 & pj`1<=p`1 & p`1<=ppi`1 & p in rng c1;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A351: x in X and
A352: X in lg by TARSKI:def 4;
consider i such that
A353: X=LSeg(g,i) and
A354: 1<=i and
A355: i+1 <= len g by A352;
now
per cases;
suppose
A356: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A356,XXREAL_0:2;
then
A357: i in dom g1 by A354,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A356,FINSEQ_3:25;
then X=LSeg(g1,i) by A353,A357,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A354,A356
;
then
A358: x in L~f1 by A36,A351,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A358;
end;
suppose
A359: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A360: i<=len g by A355,NAT_1:13;
A361: len g1<=i by A359,NAT_1:13;
then
A362: q1 `2=ppi`2 by A330,A360;
A363: q1`1<=ppi`1 by A330,A361,A360;
A364: pj`1<=q1`1 by A330,A361,A360;
q2`2=ppi`2 by A330,A355,A359;
then
A365: q2=|[q2 `1,q1`2]| by A362,EUCLID:53;
A366: q2`1<=ppi`1 by A330,A355,A359;
A367: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A354,A355,
EUCLID:53,TOPREAL1:def 3;
A368: pj`1<= q2`1 by A330,A355,A359;
now
per cases by XXREAL_0:1;
suppose
q1`1>q2`1;
then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1
<=q1`1} by A365,A367,TOPREAL3:10;
then consider p2 such that
A369: p2 =x & p2`2=q1`2 and
A370: q2`1<=p2`1 & p2`1<=q1`1 by A351,A353;
pj`1<=p2`1 & p2`1<=ppi`1 by A363,A368,A370,
XXREAL_0:2;
then
A371: x in LSeg(f,k) by A328,A362,A369;
LSeg(f,k) in lf by A3,A13;
hence thesis by A371,TARSKI:def 4;
end;
suppose
q1`1=q2`1;
then LSeg(g,i)={q1} by A365,A367,RLTOPSP1:70;
then x=q1 by A351,A353,TARSKI:def 1;
then
A372: x in LSeg(f,k) by A328,A362,A364,A363;
LSeg(f,k) in lf by A3,A13;
hence thesis by A372,TARSKI:def 4;
end;
suppose
q1`1<q2`1;
then LSeg(g,i)= {p1: p1`2=q1`2 & q1`1<=p1`1 & p1
`1<=q2`1} by A365,A367,TOPREAL3:10;
then consider p2 such that
A373: p2 =x & p2`2=q1`2 and
A374: q1`1<=p2`1 & p2`1<=q2`1 by A351,A353;
pj`1<=p2`1 & p2`1<=ppi`1 by A364,A366,A374,
XXREAL_0:2;
then
A375: x in LSeg(f,k) by A328,A362,A373;
LSeg(f,k) in lf by A3,A13;
hence thesis by A375,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let x be object;
assume x in L~f;
then
A376: x in L~f1 \/ LSeg(f,k) by A3,A12,Th3;
now
per cases by A376,XBOOLE_0:def 3;
suppose
A377: x in L~f1;
L~g1 c= L~g by Th6;
hence thesis by A36,A377;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A378: p1=x and
A379: p1`2=ppi`2 and
A380: pj`1<=p1`1 and
A381: p1`1<=ppi`1 by A328;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st
q=g/.$1 holds q`1>=p1`1;
A382: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A329,XREAL_1:31;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A383: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A38,A383,FINSEQ_4:68
.=G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence thesis by A381;
end;
end;
A384: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A385: P2 [ma] & for n be Nat st P2[n] holds n<=ma
from NAT_1:sch 6 (A384,A382);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A386: ma=len g;
j1+1<=i1 by A295,NAT_1:13;
then
A387: 1<=l by XREAL_1:19;
then 0+1<=ma by A309,A329,A386,XREAL_1:7;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
A388: m1 + 1 = ma;
len g1+1<=ma by A309,A329,A386,A387,XREAL_1:7;
then
A389: m1 >= len g1 by A388,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2
& pj`1<=e`1 & e`1<=q`1};
A390: i1-l=j1;
A391: l in dom g2 by A310,A387,FINSEQ_1:1;
then
A392: g/.ma=g2/.l by A309,A329,A386,FINSEQ_4:69
.= pj by A309,A310,A391,A390;
then p1`1<=pj`1 by A385;
then
A393: p1`1=pj`1 by A380,XXREAL_0:1;
A394: m1 <= len g by A386,A388,NAT_1:11;
then
A395: q`2=ppi`2 by A330,A389;
A396: pj`1<=q`1 by A330,A389,A394;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A397: 1<=m1 by A389,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg (g,m1)=LSeg(pj,q) by A386
,A392,A388,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A302,A327,A395,A396,TOPREAL3:10
;
then
A398: p1 in LSeg(g,m1) by A379,A393,A396;
LSeg(g,m1) in lg by A386,A388,A397;
hence thesis by A378,A398,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A385,XXREAL_0:1;
then
A399: ma+1 <= len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of
TOP-REAL 2;
set lma = {p2: p2`2=ppi`2 & qa1`1<=p2`1 & p2`1<=qa`1
};
A400: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A401: p1`1<=qa`1 by A385;
A402: len g1<=ma+1 by A385,NAT_1:13;
then
A403: qa1 `2 = ppi`2 by A330,A399;
A404: now
assume p1`1<=qa1`1;
then for q holds q=g/.(ma+1) implies p1`1<=q`1;
then ma+1<=ma by A385,A399,A402;
hence contradiction by XREAL_1:29;
end;
A405: qa`2=ppi`2 & qa =|[qa`1,qa`2]| by A330,A385,EUCLID:53
;
A406: 1<=ma by A13,A23,A39,A385,NAT_1:13;
then LSeg(g,ma)=LSeg(qa1,qa) by A399,TOPREAL1:def 3
.= lma by A401,A404,A403,A405,A400,TOPREAL3:10
,XXREAL_0:2;
then
A407: x in LSeg(g,ma) by A378,A379,A401,A404;
LSeg(g,ma) in lg by A406,A399;
hence thesis by A407,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then 1 in dom g1 by A57,FINSEQ_1:1;
hence g/.1=f1/.1 by A37,FINSEQ_4:68
.=f/.1 by A17,A15,FINSEQ_4:71;
A408: len g=len g1 + len g2 by FINSEQ_1:22;
j1+1<=i1 by A295,NAT_1:13;
then
A409: 1<=l by XREAL_1:19;
then
A410: l in dom g2 by A310,FINSEQ_1:1;
hence g/.len g=g2/.l by A309,A408,FINSEQ_4:69
.=G*(m1,i2) by A309,A310,A410
.=f/.len f by A3,A46,A294;
thus len f<=len g by A3,A23,A39,A309,A409,A408,XREAL_1:7;
end;
case
i1=j1;
hence contradiction by A6,A17,A19,A44,A46,A294;
end;
case
A411: i1<j1;
set lk={w where w is Point of TOP-REAL 2: w`2=ppi`2 & ppi`1<=w
`1 & w`1<= pj`1};
A412: ppi=|[ppi`1,ppi`2]| by EUCLID:53;
reconsider l=j1-i1 as Element of NAT by A411,INT_1:5;
deffunc F(Nat) = G*(i1+$1,i2);
consider g2 such that
A413: len g2 = l & for n being Nat st n in dom g2 holds g2
/.n = F(n) from FINSEQ_4:sch 2;
take g=g1^g2;
A414: now
let n;
A415: n<=i1+n by NAT_1:11;
assume
A416: n in Seg l;
then n<=l by FINSEQ_1:1;
then
A417: i1+n<=l+i1 by XREAL_1:7;
j1<=len G by A48,FINSEQ_3:25;
then
A418: i1+n<=len G by A417,XXREAL_0:2;
1<=n by A416,FINSEQ_1:1;
then 1<=i1+n by A415,XXREAL_0:2;
hence i1+n in dom G by A418,FINSEQ_3:25;
hence [i1+n,i2] in Indices G by A47,A51,ZFMISC_1:87;
end;
A419: dom g2 = Seg len g2 by FINSEQ_1:def 3;
now
let n be Nat such that
A420: n in dom g2;
reconsider m=i1+n,k=i2 as Nat;
take m,k;
thus [m,k] in Indices G & g2/.n=G*(m,k) by A413,A414,A419
,A420;
end;
then
A421: for n being Nat st n in dom g
ex i,j being Nat st [i,j] in Indices G & g/.n=
G*(i,j) by A40,GOBOARD1:23;
A422: now
let n be Nat;
assume that
A423: n in dom g2 and
A424: n+1 in dom g2;
let l1,l2,l3,l4 be Nat;
assume that
A425: [l1,l2] in Indices G and
A426: [l3,l4] in Indices G and
A427: g2/.n=G*(l1,l2) and
A428: g2/.(n+1)=G*(l3,l4);
g2/.(n+1)=G*(i1+(n+1),i2) & [i1+(n+1),i2] in Indices G
by A413,A414,A419,A424;
then
A429: l3=i1+(n+1) & l4=i2 by A426,A428,GOBOARD1:5;
g2/.n=G*(i1+n,i2) & [i1+n,i2] in Indices G by A413,A414,A419
,A423;
then l1=i1+n & l2=i2 by A425,A427,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|= |.i1+n-(i1+(n+1)).|+0 by A429,
ABSVALUE:2
.= |.-1.|
.= |.1.| by COMPLEX1:52
.= 1 by ABSVALUE:def 1;
end;
now
let l1,l2,l3,l4 be Nat;
assume that
A430: [ l1,l2] in Indices G and
A431: [l3,l4] in Indices G and
A432: g1/.len g1=G*(l1,l2) and
A433: g2/.1=G*(l3,l4) and
len g1 in dom g1 and
A434: 1 in dom g2;
g2/.1=G*(i1+1,i2) & [i1+1,i2] in Indices G by A413,A414,A419
,A434;
then
A435: l3=i1+1 & l4=i2 by A431,A433,GOBOARD1:5;
f1/.len f1=f/.k by A17,A23,A14,FINSEQ_4:71;
then l1=i1 & l2=i2 by A38,A18,A19,A430,A432,GOBOARD1:5;
hence |.l1-l3.|+|.l2-l4.|=|.i1-(i1+1).|+0 by A435,
ABSVALUE:2
.=|.i1-i1+-1.|
.=|.1.| by COMPLEX1:52
.=1 by ABSVALUE:def 1;
end;
then for n being Nat st n in dom g & n+1 in dom g
for m,k,i,j being Nat st
[m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds
|.m-i.|+|.k-j.|=1 by A41,A422,GOBOARD1:24;
hence g is_sequence_on G by A421;
A436: pj=|[pj`1,pj`2]| by EUCLID:53;
c1/.j1 = c1.j1 by A48,A43,PARTFUN1:def 6;
then
A437: c1/.j1=pj by A48,MATRIX_0:def 8;
then
A438: x2.j1=pj`1 by A48,A43,A22,GOBOARD1:def 1;
c1/.i1 = c1.i1 by A49,A43,PARTFUN1:def 6;
then
A439: c1/.i1=ppi by A49,MATRIX_0:def 8;
then
A440: x2.i1=ppi`1 by A49,A43,A22,GOBOARD1:def 1;
then
A441: ppi `1<pj`1 by A49,A48,A52,A43,A22,A411,A438,SEQM_3:def 1;
A442: y2.j1=pj`2 by A48,A43,A21,A437,GOBOARD1:def 2;
y2.i1=ppi`2 by A49,A43,A21,A439,GOBOARD1:def 2;
then
A443: ppi`2=pj`2 by A49,A48,A53,A43,A21,A442,SEQM_3:def 10;
A444: LSeg(f,k)=LSeg(ppi,pj) by A3,A13,A19,A46,A294,TOPREAL1:def 3
.= lk by A441,A443,A412,A436,TOPREAL3:10;
A445: dom g2 = Seg l by A413,FINSEQ_1:def 3;
thus L~g=L~f
proof
set lg = {LSeg(g,i): 1<=i & i+1<=len g}, lf = {LSeg(f,j): 1
<=j & j+1<=len f};
A446: len g = len g1 + len g2 by FINSEQ_1:22;
A447: now
let j;
assume that
A448: len g1<=j and
A449: j<=len g;
reconsider w = j-len g1 as Element of NAT by A448,INT_1:5;
set u=i1+w;
let p such that
A450: p=g/.j;
now
per cases;
suppose
A451: j=len g1;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then len g1 in dom g1 by FINSEQ_3:25;
then
A452: g/.len g1 = f1/.len f1 by A38,FINSEQ_4:68
.= G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence p`2=G*(i1,i2)`2 by A450,A451;
thus G*(i1,i2)`1<=p`1 & p`1<=G* (j1,i2)`1 by A49,A48
,A52,A43,A22,A411,A440,A438,A450,A451,A452,SEQM_3:def 1;
thus p in rng c1 by A49,A43,A439,A450,A451,A452,
PARTFUN2:2;
end;
suppose
A453: j<>len g1;
A454: w + len g1 = j;
then
A455: w <= len g2 by A446,A449,XREAL_1:6;
A456: y2.i1=G*(i1,i2)`2 by A49,A43,A21,A439,GOBOARD1:def 2;
A457: j - len g1 <> 0 by A453;
then
A458: w >= 1 by NAT_1:14;
then
A459: g/.j=g2/.w by A454,A455,SEQ_4:136;
A460: i1<u by A457,XREAL_1:29;
A461: w in dom g2 by A458,A455,FINSEQ_3:25;
then
A462: u in dom G by A445,A414;
c1/.u = c1.u by A43,A445,A414,A461,PARTFUN1:def 6;
then
A463: c1/.u=G*(u,i2) by A462,MATRIX_0:def 8;
then
A464: x2.u=G *(u,i2)`1 by A43,A22,A462,GOBOARD1:def 1;
A465: g2/.w=G*(u,i2) by A413,A461;
y2.u=G*(u,i2)`2 by A43,A21,A462,A463,GOBOARD1:def 2;
hence
p`2=G*(i1,i2)`2 by A49,A53,A43,A21,A450,A459,A465,A462
,A456,SEQM_3:def 10;
x2.i1=G*(i1,i2)`1 by A49,A43,A22,A439,GOBOARD1:def 1;
hence G*(i1,i2)`1<=p`1 by A49,A52,A43,A22,A450,A459
,A465,A462,A464,A460,SEQM_3:def 1;
A466: x2.j1=G* (j1,i2)`1 by A48,A43,A22,A437,GOBOARD1:def 1;
now
per cases;
suppose
u=j1;
hence
p`1<=G*(j1,i2)`1
by A450,A458,A454,A455,A465,SEQ_4:136;
end;
suppose
A467: u<>j1;
u<=i1+l by A413,A455,XREAL_1:7;
then u<j1 by A467,XXREAL_0:1;
hence
p`1<=G*(j1,i2)`1 by A48,A52,A43,A22,A450,A459,A465
,A462,A464,A466,SEQM_3:def 1;
end;
end;
hence p`1<=G*(j1,i2)`1;
thus p in rng c1 by A43,A450,A459,A465,A462,A463,
PARTFUN2:2;
end;
end;
hence p`2=ppi`2 & ppi`1<=p`1 & p`1<=pj`1 & p in rng c1;
end;
thus L~g c= L~f
proof
let x be object;
assume x in L~g;
then consider X be set such that
A468: x in X and
A469: X in lg by TARSKI:def 4;
consider i such that
A470: X=LSeg(g,i) and
A471: 1<=i and
A472: i+1 <= len g by A469;
now
per cases;
suppose
A473: i+1 <= len g1;
i<=i+1 by NAT_1:11;
then i<=len g1 by A473,XXREAL_0:2;
then
A474: i in dom g1 by A471,FINSEQ_3:25;
1<=i+1 by NAT_1:11;
then i+1 in dom g1 by A473,FINSEQ_3:25;
then X=LSeg(g1,i) by A470,A474,TOPREAL3:18;
then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A471,A473
;
then
A475: x in L~f1 by A36,A468,TARSKI:def 4;
L~f1 c= L~f by TOPREAL3:20;
hence thesis by A475;
end;
suppose
A476: i+1 > len g1;
reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2;
A477: i<=len g by A472,NAT_1:13;
A478: len g1<=i by A476,NAT_1:13;
then
A479: q1 `2=ppi`2 by A447,A477;
A480: q1`1<=pj`1 by A447,A478,A477;
A481: ppi`1<=q1`1 by A447,A478,A477;
q2`2=ppi`2 by A447,A472,A476;
then
A482: q2=|[q2 `1,q1`2]| by A479,EUCLID:53;
A483: q2`1<=pj`1 by A447,A472,A476;
A484: q1=|[q1`1,q1`2]| & LSeg(g,i)=LSeg(q2,q1) by A471,A472,
EUCLID:53,TOPREAL1:def 3;
A485: ppi`1<= q2`1 by A447,A472,A476;
now
per cases by XXREAL_0:1;
suppose
q1`1>q2`1;
then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1
<=q1`1} by A482,A484,TOPREAL3:10;
then consider p2 such that
A486: p2 =x & p2`2=q1`2 and
A487: q2`1<=p2`1 & p2`1<=q1`1 by A468,A470;
ppi`1<=p2`1 & p2`1<=pj`1 by A480,A485,A487,
XXREAL_0:2;
then
A488: x in LSeg(f,k) by A444,A479,A486;
LSeg(f,k) in lf by A3,A13;
hence thesis by A488,TARSKI:def 4;
end;
suppose
q1`1=q2`1;
then LSeg(g,i)={q1} by A482,A484,RLTOPSP1:70;
then x=q1 by A468,A470,TARSKI:def 1;
then
A489: x in LSeg(f,k) by A444,A479,A481,A480;
LSeg(f,k) in lf by A3,A13;
hence thesis by A489,TARSKI:def 4;
end;
suppose
q1`1<q2`1;
then LSeg(g,i)= {p1: p1`2=q1`2 & q1`1<=p1`1 & p1
`1<=q2`1} by A482,A484,TOPREAL3:10;
then consider p2 such that
A490: p2 =x & p2`2=q1`2 and
A491: q1`1<=p2`1 & p2`1<=q2`1 by A468,A470;
ppi`1<=p2`1 & p2`1<=pj`1 by A481,A483,A491,
XXREAL_0:2;
then
A492: x in LSeg(f,k) by A444,A479,A490;
LSeg(f,k) in lf by A3,A13;
hence thesis by A492,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let x be object;
assume x in L~f;
then
A493: x in L~f1 \/ LSeg(f,k) by A3,A12,Th3;
now
per cases by A493,XBOOLE_0:def 3;
suppose
A494: x in L~f1;
L~g1 c= L~g by Th6;
hence thesis by A36,A494;
end;
suppose
x in LSeg(f,k);
then consider p1 such that
A495: p1=x and
A496: p1`2=ppi`2 and
A497: ppi`1<=p1`1 and
A498: p1`1<=pj`1 by A444;
defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st
q=g/.$1 holds q`1<=p1`1;
A499: now
reconsider n=len g1 as Nat;
take n;
thus P2[n]
proof
thus len g1<=n & n<=len g by A446,XREAL_1:31;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A500: len g1 in dom g1 by FINSEQ_3:25;
let q;
assume q=g/.n;
then q=f1/.len f1 by A38,A500,FINSEQ_4:68
.=G*(i1,i2) by A17,A23,A14,A19,FINSEQ_4:71;
hence thesis by A497;
end;
end;
A501: for n be Nat holds P2[n] implies n<=len g;
consider ma be Nat such that
A502: P2 [ma] & for n be Nat st P2[n] holds n<=ma
from NAT_1:sch 6 (A501,A499);
reconsider ma as Element of NAT by ORDINAL1:def 12;
now
per cases;
suppose
A503: ma=len g;
i1+1<=j1 by A411,NAT_1:13;
then
A504: 1<=l by XREAL_1:19;
then 0+1<=ma by A413,A446,A503,XREAL_1:7;
then reconsider m1=ma-1 as Element of NAT by INT_1:5;
A505: m1 + 1 = ma;
len g1+1<=ma by A413,A446,A503,A504,XREAL_1:7;
then
A506: m1 >= len g1 by A505,XREAL_1:6;
reconsider q=g/.m1 as Point of TOP-REAL 2;
set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2
& q`1<=e`1 & e`1<=pj`1};
A507: i1+l=j1;
A508: l in dom g2 by A413,A504,FINSEQ_3:25;
then
A509: g/.ma=g2/.l by A413,A446,A503,FINSEQ_4:69
.= pj by A413,A508,A507;
then pj`1<=p1`1 by A502;
then
A510: p1`1=pj`1 by A498,XXREAL_0:1;
A511: m1 <= len g by A503,A505,NAT_1:11;
then
A512: q`2=ppi`2 by A447,A506;
A513: q`1<=pj`1 by A447,A506,A511;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then
A514: 1<=m1 by A506,XXREAL_0:2;
then q=|[q`1,q`2]| & LSeg(g,m1)=LSeg(pj,q) by A503
,A509,A505,EUCLID:53,TOPREAL1:def 3;
then LSeg(g,m1)=lq by A443,A436,A512,A513,TOPREAL3:10
;
then
A515: p1 in LSeg(g,m1) by A496,A510,A513;
LSeg(g,m1) in lg by A503,A505,A514;
hence thesis by A495,A515,TARSKI:def 4;
end;
suppose
ma<>len g;
then ma<len g by A502,XXREAL_0:1;
then
A516: ma+1 <= len g by NAT_1:13;
reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of
TOP-REAL 2;
set lma = {p2: p2`2=ppi`2 & qa`1<=p2`1 & p2`1<=qa1`1
};
A517: qa1=|[qa1 `1, qa1 `2]| by EUCLID:53;
A518: qa`1<=p1`1 by A502;
A519: len g1<=ma+1 by A502,NAT_1:13;
then
A520: qa1 `2 = ppi`2 by A447,A516;
A521: now
assume qa1`1<=p1`1;
then for q holds q=g/.(ma+1) implies q`1<=p1`1;
then ma+1<=ma by A502,A516,A519;
hence contradiction by XREAL_1:29;
end;
A522: qa`2=ppi`2 & qa =|[qa`1,qa`2]| by A447,A502,EUCLID:53
;
A523: 1<=ma by A13,A23,A39,A502,NAT_1:13;
then LSeg(g,ma)=LSeg(qa,qa1) by A516,TOPREAL1:def 3
.= lma by A518,A521,A520,A522,A517,TOPREAL3:10
,XXREAL_0:2;
then
A524: x in LSeg(g,ma) by A495,A496,A518,A521;
LSeg(g,ma) in lg by A523,A516;
hence thesis by A524,TARSKI:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
1<=len g1 by A13,A23,A39,XXREAL_0:2;
then 1 in dom g1 by FINSEQ_3:25;
hence g/.1=f1/.1 by A37,FINSEQ_4:68
.=f/.1 by A17,A15,FINSEQ_4:71;
A525: len g=len g1 + l by A413,FINSEQ_1:22;
i1+1<=j1 by A411,NAT_1:13;
then
A526: 1<=l by XREAL_1:19;
then
A527: l in dom g2 by A413,A419,FINSEQ_1:1;
hence g/.len g=g2/.l by A525,FINSEQ_4:69
.=G*(i1+l,i2) by A413,A527
.=f/.len f by A3,A46,A294;
thus len f<=len g by A3,A23,A39,A526,A525,XREAL_1:7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
A528: P[0]
proof
let f such that
A529: len f=0 and
A530: for n being Nat st n in dom f
ex i,j being Nat st [i,j] in Indices G & f/.n=G*(i,j) and
f is special and
for n being Nat st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1);
take g=f;
f={} by A529;
then
for n being Nat holds n in dom g & n+1 in dom g implies
for m,k,i,j being Nat st [m,k] in
Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds |.m-i.|
+|.k-j.|=1;
hence thesis by A530;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A528,A1);
hence thesis;
end;
definition
let v1,v2 be FinSequence of REAL;
assume
A1: v1 <> {};
func GoB(v1,v2) -> Matrix of TOP-REAL 2 means
:Def1:
len it = len v1 & width
it = len v2 &
for n,m being Nat st [n,m] in Indices it holds it*(n,m) = |[v1.n,v2.m]|;
existence
proof
defpred P[Nat,Nat,Point of TOP-REAL 2] means [$1,$2] in [:dom v1,dom v2:]
& for r,s st v1.$1=r & v2.$2=s holds $3=|[r,s]|;
A2: dom v1 = Seg len v1 by FINSEQ_1:def 3;
A3: for i,j being Nat st [i,j] in [:Seg len v1,Seg len v2:] ex p st P[i,j, p]
proof
let i,j be Nat;
assume
A4: [i,j] in [:Seg len v1,Seg len v2:];
reconsider i9=i, j9=j as Element of NAT by ORDINAL1:def 12;
reconsider s1=v1.i9, s2=v2.j9 as Real;
take |[s1,s2]|;
thus [i,j] in [:dom v1,dom v2:] by A2,A4,FINSEQ_1:def 3;
let r,s;
assume r=v1.i & s=v2.j;
hence thesis;
end;
consider M be Matrix of len v1,len v2,the carrier of TOP-REAL 2 such that
A5: for i,j being Nat st [i,j] in Indices M holds P[i,j,M*(i,j)] from
MATRIX_0:sch 2(A3);
reconsider M as Matrix of the carrier of TOP-REAL 2;
take M;
thus len M=len v1 & width M=len v2 by A1,MATRIX_0:23;
let n,m be Nat;
assume [n,m] in Indices M;
hence thesis by A5;
end;
uniqueness
proof
let G1,G2 be Matrix of TOP-REAL 2;
assume that
A6: len G1 = len v1 & width G1 = len v2 and
A7: for n,m being Nat st [n,m] in Indices G1 holds G1*(n,m) = |[v1.n,v2.m]| and
A8: len G2 = len v1 & width G2 = len v2 and
A9: for n,m being Nat st [n,m] in Indices G2 holds G2*(n,m) = |[v1.n,v2.m]|;
A10: Indices G1 = [:dom G1,Seg width G1:] & Indices G2 = [:dom G2,Seg
width G2:] by MATRIX_0:def 4;
now
let n,m be Nat;
reconsider m9=m, n9=n as Element of NAT by ORDINAL1:def 12;
A11: dom G1 = Seg len G1 & dom G2 = Seg len G2 by FINSEQ_1:def 3;
reconsider r=v1.n9, s=v2.m9 as Real;
assume
A12: [n,m] in Indices G1;
then G1*(n,m)=|[r,s]| by A7;
hence G1*(n,m)=G2*(n,m) by A6,A8,A9,A10,A12,A11;
end;
hence thesis by A6,A8,MATRIX_0:21;
end;
end;
registration
let v1,v2 be non empty FinSequence of REAL;
cluster GoB(v1,v2) -> non empty-yielding X_equal-in-line Y_equal-in-column;
coherence
proof
set M = GoB(v1,v2);
A1: len M=len v1 by Def1;
then
A2: dom M = dom v1 by FINSEQ_3:29;
A3: width M=len v2 by Def1;
hence M is non empty-yielding by A1,MATRIX_0:def 10;
A4: Indices M=[:dom v1,Seg len v2:] by A3,A2,MATRIX_0:def 4;
thus M is X_equal-in-line
proof
let n be Nat;
reconsider l = Line(M,n) as FinSequence of TOP-REAL 2;
set x = X_axis(l);
assume
A5: n in dom M;
A6: len l = width M & dom x = Seg len x by FINSEQ_1:def 3,MATRIX_0:def 7;
A7: len x = len l by GOBOARD1:def 1;
then
A8: dom x = dom l by FINSEQ_3:29;
now
let i,j be Nat;
assume that
A9: i in dom x and
A10: j in dom x;
reconsider r=v1.n, s1=v2.i, s2=v2.j as Real;
[n,i] in Indices M by A3,A2,A4,A5,A7,A6,A9,ZFMISC_1:87;
then M*(n,i)=|[r,s1]| by Def1;
then
A11: M*(n,i)`1 = r by EUCLID:52;
l/.i = l.i by A8,A9,PARTFUN1:def 6;
then l/.i=M*(n,i) by A7,A6,A9,MATRIX_0:def 7;
then
A12: x.i=r by A9,A11,GOBOARD1:def 1;
[n,j] in Indices M by A3,A2,A4,A5,A7,A6,A10,ZFMISC_1:87;
then M*(n,j)=|[r,s2]| by Def1;
then
A13: M*(n,j)`1 = r by EUCLID:52;
l/.j = l.j by A8,A10,PARTFUN1:def 6;
then l/.j=M*(n,j) by A7,A6,A10,MATRIX_0:def 7;
hence x.i=x.j by A10,A13,A12,GOBOARD1:def 1;
end;
hence thesis by SEQM_3:def 10;
end;
thus M is Y_equal-in-column
proof
let n be Nat;
reconsider c = Col(M,n) as FinSequence of TOP-REAL 2;
set y = Y_axis(c);
len y = len c by GOBOARD1:def 2;
then
A14: dom y = dom c by FINSEQ_3:29;
len c = len M by MATRIX_0:def 8;
then
A15: dom c = dom M by FINSEQ_3:29;
assume
A16: n in Seg width M;
now
let i,j be Nat;
assume that
A17: i in dom y and
A18: j in dom y;
reconsider r=v2.n, s1=v1.i, s2=v1.j as Real;
[i,n] in Indices M by A3,A2,A4,A16,A14,A15,A17,ZFMISC_1:87;
then M*(i,n)=|[s1,r]| by Def1;
then
A19: M*(i,n)`2 = r by EUCLID:52;
c/.i = c.i by A14,A17,PARTFUN1:def 6;
then c/.i=M*(i,n) by A14,A15,A17,MATRIX_0:def 8;
then
A20: y.i=r by A17,A19,GOBOARD1:def 2;
[j,n] in Indices M by A3,A2,A4,A16,A14,A15,A18,ZFMISC_1:87;
then M*(j,n)=|[s2,r]| by Def1;
then
A21: M*(j,n)`2 = r by EUCLID:52;
c/.j = c.j by A14,A18,PARTFUN1:def 6;
then c/.j=M*(j,n) by A14,A15,A18,MATRIX_0:def 8;
hence y.i=y.j by A18,A21,A20,GOBOARD1:def 2;
end;
hence thesis by SEQM_3:def 10;
end;
end;
end;
registration
let v1,v2 be non empty increasing FinSequence of REAL;
cluster GoB(v1,v2) -> Y_increasing-in-line X_increasing-in-column;
coherence
proof
set M = GoB(v1,v2);
A1: width M=len v2 by Def1;
A2: len M=len v1 by Def1;
then
A3: dom M = dom v1 by FINSEQ_3:29;
then
A4: Indices M=[:dom v1,Seg len v2:] by A1,MATRIX_0:def 4;
A5: dom v2=Seg len v2 by FINSEQ_1:def 3;
thus M is Y_increasing-in-line
proof
let n be Nat;
reconsider l = Line(M,n) as FinSequence of TOP-REAL 2;
set y = Y_axis(l);
assume
A6: n in dom M;
A7: len l = width M & dom y = Seg len y by FINSEQ_1:def 3,MATRIX_0:def 7;
A8: len y = len l by GOBOARD1:def 2;
then
A9: dom y = dom l by FINSEQ_3:29;
now
let i,j be Nat;
assume that
A10: i in dom y and
A11: j in dom y and
A12: i<j;
reconsider r=v1.n, s1=v2.i, s2=v2.j as Real;
[n,j] in Indices M by A1,A3,A4,A6,A8,A7,A11,ZFMISC_1:87;
then M*(n,j)=|[r,s2]| by Def1;
then
A13: M*(n,j)`2 = s2 by EUCLID:52;
l/.j = l.j by A9,A11,PARTFUN1:def 6;
then l/.j=M*(n,j) by A8,A7,A11,MATRIX_0:def 7;
then
A14: y.j=s2 by A11,A13,GOBOARD1:def 2;
[n,i] in Indices M by A1,A3,A4,A6,A8,A7,A10,ZFMISC_1:87;
then M*(n,i)=|[r,s1]| by Def1;
then
A15: M*(n,i)`2 = s1 by EUCLID:52;
l/.i = l.i by A9,A10,PARTFUN1:def 6;
then l/.i=M*(n,i) by A8,A7,A10,MATRIX_0:def 7;
then y.i=s1 by A10,A15,GOBOARD1:def 2;
hence y.i<y.j by A5,A1,A8,A7,A10,A11,A12,A14,SEQM_3:def 1;
end;
hence thesis by SEQM_3:def 1;
end;
A16: dom v1=Seg len v1 by FINSEQ_1:def 3;
thus M is X_increasing-in-column
proof
let n be Nat;
reconsider c = Col(M,n) as FinSequence of TOP-REAL 2;
set x = X_axis(c);
assume
A17: n in Seg width M;
A18: len x = len c by GOBOARD1:def 1;
then
A19: dom x = dom c by FINSEQ_3:29;
A20: len c = len M by MATRIX_0:def 8;
then
A21: dom c = dom M by FINSEQ_3:29;
A22: dom x = Seg len x by FINSEQ_1:def 3;
now
let i,j be Nat;
assume that
A23: i in dom x and
A24: j in dom x and
A25: i<j;
reconsider r=v2.n, s1=v1.i, s2=v1.j as Real;
[j,n] in Indices M by A1,A3,A4,A17,A19,A21,A24,ZFMISC_1:87;
then M*(j,n)=|[s2,r]| by Def1;
then
A26: M*(j,n)`1 = s2 by EUCLID:52;
c/.j = c.j by A19,A24,PARTFUN1:def 6;
then c/.j=M*(j,n) by A19,A21,A24,MATRIX_0:def 8;
then
A27: x.j=s2 by A24,A26,GOBOARD1:def 1;
[i,n] in Indices M by A1,A3,A4,A17,A19,A21,A23,ZFMISC_1:87;
then M*(i,n)=|[s1,r]| by Def1;
then
A28: M*(i,n)`1 = s1 by EUCLID:52;
c/.i = c.i by A19,A23,PARTFUN1:def 6;
then c/.i=M*(i,n) by A19,A21,A23,MATRIX_0:def 8;
then x.i=s1 by A23,A28,GOBOARD1:def 1;
hence x.i<x.j by A16,A2,A18,A20,A22,A23,A24,A25,A27,SEQM_3:def 1;
end;
hence thesis by SEQM_3:def 1;
end;
end;
end;
definition
let f be non empty FinSequence of TOP-REAL 2;
func GoB(f) -> Matrix of TOP-REAL 2 equals
GoB(Incr(X_axis(f)),Incr(Y_axis(f)));
correctness;
end;
registration
let f be non empty FinSequence of TOP-REAL 2;
cluster GoB(f) -> non empty-yielding X_equal-in-line Y_equal-in-column
Y_increasing-in-line X_increasing-in-column;
coherence;
end;
reserve f for non empty FinSequence of TOP-REAL 2;
theorem Th13:
len GoB(f) = card rng X_axis(f) & width GoB(f) = card rng Y_axis (f)
proof
set x = X_axis(f), y = Y_axis(f);
len Incr(x)=card rng x & len Incr(y)=card rng y by SEQ_4:def 21;
hence thesis by Def1;
end;
theorem
for n st n in dom f holds ex i,j st [i,j] in Indices GoB(f) & f/.n =
GoB(f)*(i,j)
proof
set x = X_axis(f), y = Y_axis(f);
let n such that
A1: n in dom f;
A2: rng Incr(y) = rng y by SEQ_4:def 21;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
dom y = Seg len y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
then y.n=p`2 & y.n in rng y by A1,A3,FUNCT_1:def 3,GOBOARD1:def 2;
then consider j being Nat such that
A4: j in dom Incr(y) and
A5: Incr(y).j=p`2 by A2,FINSEQ_2:10;
A6: rng Incr(x) = rng x by SEQ_4:def 21;
dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then x.n=p`1 & x.n in rng x by A1,A3,FUNCT_1:def 3,GOBOARD1:def 1;
then consider i being Nat such that
A7: i in dom Incr(x) and
A8: Incr(x).i=p`1 by A6,FINSEQ_2:10;
width GoB(f)=card rng y & len Incr(y) = card rng y by Th13,SEQ_4:def 21;
then
A9: Seg width GoB(f) = dom Incr(y) by FINSEQ_1:def 3;
reconsider i,j as Element of NAT by ORDINAL1:def 12;
take i,j;
len GoB(f)=card rng x & len Incr(x) = card rng x by Th13,SEQ_4:def 21;
then Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & dom GoB(f) = dom
Incr(x) by FINSEQ_3:29,MATRIX_0:def 4;
hence [i,j] in Indices GoB(f) by A7,A4,A9,ZFMISC_1:87;
then GoB(f)*(i,j) = |[p`1,p`2]| by A8,A5,Def1;
hence thesis by EUCLID:53;
end;
theorem
n in dom f & (for m st m in dom f holds (X_axis(f)).n <= (X_axis(f)).m
) implies f/.n in rng Line(GoB(f),1)
proof
set x = X_axis(f), y = Y_axis(f), r = x.n;
assume that
A1: n in dom f and
A2: for m st m in dom f holds r <= x.m;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then
A5: x.n=p`1 by A1,A3,GOBOARD1:def 1;
A6: rng Incr(x) = rng x by SEQ_4:def 21;
x.n in rng x by A1,A3,A4,FUNCT_1:def 3;
then consider i being Nat such that
A7: i in dom Incr(x) and
A8: Incr(x).i=p`1 by A5,A6,FINSEQ_2:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
A9: 1<=i by A7,FINSEQ_3:25;
then reconsider i1=i-1 as Element of NAT by INT_1:5;
A10: i<=len Incr(x) by A7,FINSEQ_3:25;
A11: now
reconsider s=Incr(x).i1 as Real;
assume i <> 1;
then 1<i by A9,XXREAL_0:1;
then 1+1<=i by NAT_1:13;
then
A12: 1<=i1 by XREAL_1:19;
i1<=i by XREAL_1:44;
then i1<=len Incr(x) by A10,XXREAL_0:2;
then
A13: i1 in dom Incr(x) by A12,FINSEQ_3:25;
then Incr(x).i1 in rng Incr(x) by FUNCT_1:def 3;
then
A14: ex m being Nat st m in dom x & x.m=s by A6,FINSEQ_2:10;
i1<i by XREAL_1:44;
then s<r by A5,A7,A8,A13,SEQM_3:def 1;
hence contradiction by A2,A3,A4,A14;
end;
A15: rng Incr(y) = rng y by SEQ_4:def 21;
dom y = Seg len y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
then y.n=p`2 & y.n in rng y by A1,A3,FUNCT_1:def 3,GOBOARD1:def 2;
then consider j being Nat such that
A16: j in dom Incr(y) and
A17: Incr(y).j=p`2 by A15,FINSEQ_2:10;
A18: p=|[p`1,p`2]| by EUCLID:53;
len Line(GoB(f),1) = width GoB(f) by MATRIX_0:def 7;
then
A19: dom Line(GoB(f),1) = Seg width GoB(f) by FINSEQ_1:def 3;
width GoB(f) = card rng y & len Incr(y) = card rng y by Th13,SEQ_4:def 21;
then
A20: dom Incr(y) = Seg width GoB(f) by FINSEQ_1:def 3;
len GoB(f)=card rng x & len Incr(x) = card rng x by Th13,SEQ_4:def 21;
then Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & dom Incr(x) = dom
GoB(f) by FINSEQ_3:29,MATRIX_0:def 4;
then [1,j] in Indices GoB(f) by A7,A16,A20,A11,ZFMISC_1:87;
then GoB(f)*(1,j) = |[p`1,p`2]| by A8,A17,A11,Def1;
then (Line(GoB(f),1)).j = f/.n by A16,A20,A18,MATRIX_0:def 7;
hence thesis by A16,A20,A19,FUNCT_1:def 3;
end;
theorem
n in dom f & (for m st m in dom f holds (X_axis(f)).m <= (X_axis(f)).n
) implies f/.n in rng Line(GoB(f),len GoB(f))
proof
set x = X_axis(f), y = Y_axis(f), r = x.n;
assume that
A1: n in dom f and
A2: for m st m in dom f holds x.m <= r;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then
A5: x.n=p`1 by A1,A3,GOBOARD1:def 1;
A6: rng Incr(x) = rng x by SEQ_4:def 21;
x.n in rng x by A1,A3,A4,FUNCT_1:def 3;
then consider i being Nat such that
A7: i in dom Incr(x) and
A8: Incr(x).i=p`1 by A5,A6,FINSEQ_2:10;
reconsider i as Element of NAT by ORDINAL1:def 12;
A9: i<=len Incr(x) by A7,FINSEQ_3:25;
A10: 1<=i by A7,FINSEQ_3:25;
A11: now
reconsider s=Incr(x).(i+1) as Real;
assume i <> len Incr(x);
then i<len Incr(x) by A9,XXREAL_0:1;
then
A12: i+1<=len Incr(x) by NAT_1:13;
1<=i+1 by A10,NAT_1:13;
then
A13: i+1 in dom Incr(x) by A12,FINSEQ_3:25;
then Incr(x).(i+1) in rng Incr(x) by FUNCT_1:def 3;
then
A14: ex m being Nat st m in dom x & x.m=s by A6,FINSEQ_2:10;
i<i+1 by NAT_1:13;
then r<s by A5,A7,A8,A13,SEQM_3:def 1;
hence contradiction by A2,A3,A4,A14;
end;
A15: rng Incr(y) = rng y by SEQ_4:def 21;
dom y = Seg len y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
then y.n=p`2 & y.n in rng y by A1,A3,FUNCT_1:def 3,GOBOARD1:def 2;
then consider j being Nat such that
A16: j in dom Incr(y) and
A17: Incr(y).j=p`2 by A15,FINSEQ_2:10;
A18: p=|[p`1,p`2]| by EUCLID:53;
len Line(GoB(f),len GoB(f))=width GoB(f) by MATRIX_0:def 7;
then
A19: dom Line(GoB(f),len GoB(f))= Seg width GoB(f) by FINSEQ_1:def 3;
width GoB(f) = card rng y & len Incr(y) = card rng y by Th13,SEQ_4:def 21;
then
A20: dom Incr(y) = Seg width GoB(f) by FINSEQ_1:def 3;
A21: len GoB(f)=card rng x & len Incr(x) = card rng x by Th13,SEQ_4:def 21;
then Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & dom Incr(x) = dom
GoB(f) by FINSEQ_3:29,MATRIX_0:def 4;
then [len GoB(f),j] in Indices GoB(f) by A21,A7,A16,A20,A11,ZFMISC_1:87;
then GoB(f)*(len GoB(f),j) = |[p`1,p`2]| by A21,A8,A17,A11,Def1;
then (Line(GoB(f),len GoB(f))).j = f/.n by A16,A20,A18,MATRIX_0:def 7;
hence thesis by A16,A20,A19,FUNCT_1:def 3;
end;
theorem
n in dom f & (for m st m in dom f holds (Y_axis(f)).n <= (Y_axis(f)).m
) implies f/.n in rng Col(GoB(f),1)
proof
set x = X_axis(f), y = Y_axis(f), r = y.n;
assume that
A1: n in dom f and
A2: for m st m in dom f holds r <= y.m;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: dom y = Seg len y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A5: y.n=p`2 by A1,A3,GOBOARD1:def 2;
A6: rng Incr(y) = rng y by SEQ_4:def 21;
y.n in rng y by A1,A3,A4,FUNCT_1:def 3;
then consider j being Nat such that
A7: j in dom Incr(y) and
A8: Incr(y).j=p`2 by A5,A6,FINSEQ_2:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
A9: 1<=j by A7,FINSEQ_3:25;
then reconsider j1=j-1 as Element of NAT by INT_1:5;
A10: j<=len Incr(y) by A7,FINSEQ_3:25;
A11: now
reconsider s=Incr(y).j1 as Real;
assume j <> 1;
then 1<j by A9,XXREAL_0:1;
then 1+1<=j by NAT_1:13;
then
A12: 1<=j1 by XREAL_1:19;
j1<=j by XREAL_1:44;
then j1<=len Incr(y) by A10,XXREAL_0:2;
then
A13: j1 in dom Incr(y) by A12,FINSEQ_3:25;
then Incr(y).j1 in rng Incr(y) by FUNCT_1:def 3;
then
A14: ex m being Nat st m in dom y & y.m=s by A6,FINSEQ_2:10;
j1<j by XREAL_1:44;
then s<r by A5,A7,A8,A13,SEQM_3:def 1;
hence contradiction by A2,A3,A4,A14;
end;
A15: rng Incr(x) = rng x by SEQ_4:def 21;
dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then x.n=p`1 & x.n in rng x by A1,A3,FUNCT_1:def 3,GOBOARD1:def 1;
then consider i being Nat such that
A16: i in dom Incr(x) and
A17: Incr(x).i=p`1 by A15,FINSEQ_2:10;
A18: p=|[p`1,p`2]| by EUCLID:53;
len Col(GoB(f),1) = len GoB(f) by MATRIX_0:def 8;
then
A19: dom Col(GoB(f),1) = dom GoB(f) by FINSEQ_3:29;
len GoB(f)=card rng x & len Incr(x) = card rng x by Th13,SEQ_4:def 21;
then
A20: dom Incr(x) = dom GoB(f) by FINSEQ_3:29;
width GoB(f) = card rng y & len Incr(y) = card rng y by Th13,SEQ_4:def 21;
then Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & dom Incr(y) = Seg
width GoB(f) by FINSEQ_1:def 3,MATRIX_0:def 4;
then [i,1] in Indices GoB(f) by A16,A7,A20,A11,ZFMISC_1:87;
then GoB(f)*(i,1) = |[p`1,p`2]| by A17,A8,A11,Def1;
then (Col(GoB(f),1)).i = f/.n by A16,A20,A18,MATRIX_0:def 8;
hence thesis by A16,A20,A19,FUNCT_1:def 3;
end;
theorem
n in dom f & (for m st m in dom f holds (Y_axis(f)).m <= (Y_axis(f)).n
) implies f/.n in rng Col(GoB(f),width GoB(f))
proof
set x = X_axis(f), y = Y_axis(f), r = y.n;
assume that
A1: n in dom f and
A2: for m st m in dom f holds y.m <= r;
reconsider p=f/.n as Point of TOP-REAL 2;
A3: dom f = Seg len f by FINSEQ_1:def 3;
A4: dom y = Seg len y & len y = len f by FINSEQ_1:def 3,GOBOARD1:def 2;
then
A5: y.n=p`2 by A1,A3,GOBOARD1:def 2;
A6: rng Incr(y) = rng y by SEQ_4:def 21;
y.n in rng y by A1,A3,A4,FUNCT_1:def 3;
then consider j being Nat such that
A7: j in dom Incr(y) and
A8: Incr(y).j=p`2 by A5,A6,FINSEQ_2:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
A9: j<=len Incr(y) by A7,FINSEQ_3:25;
A10: 1<=j by A7,FINSEQ_3:25;
A11: now
reconsider s=Incr(y).(j+1) as Real;
assume j <> len Incr(y);
then j<len Incr(y) by A9,XXREAL_0:1;
then
A12: j+1<=len Incr(y) by NAT_1:13;
1<=j+1 by A10,NAT_1:13;
then
A13: j+1 in dom Incr(y) by A12,FINSEQ_3:25;
then Incr(y).(j+1) in rng Incr(y) by FUNCT_1:def 3;
then
A14: ex m being Nat st m in dom y & y.m=s by A6,FINSEQ_2:10;
j<j+1 by NAT_1:13;
then r<s by A5,A7,A8,A13,SEQM_3:def 1;
hence contradiction by A2,A3,A4,A14;
end;
A15: rng Incr(x) = rng x by SEQ_4:def 21;
dom x = Seg len x & len x = len f by FINSEQ_1:def 3,GOBOARD1:def 1;
then x.n=p`1 & x.n in rng x by A1,A3,FUNCT_1:def 3,GOBOARD1:def 1;
then consider i being Nat such that
A16: i in dom Incr(x) and
A17: Incr(x).i=p`1 by A15,FINSEQ_2:10;
A18: p=|[p`1,p`2]| by EUCLID:53;
len Col(GoB(f),width GoB(f))=len GoB(f) by MATRIX_0:def 8;
then
A19: dom Col(GoB(f),width GoB(f))=dom GoB(f) by FINSEQ_3:29;
len GoB(f)=card rng x & len Incr(x) = card rng x by Th13,SEQ_4:def 21;
then
A20: dom Incr(x) = dom GoB(f) by FINSEQ_3:29;
A21: width GoB(f) = card rng y & len Incr(y) = card rng y by Th13,SEQ_4:def 21;
then Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & dom Incr(y) = Seg
width GoB(f) by FINSEQ_1:def 3,MATRIX_0:def 4;
then [i,width GoB(f)] in Indices GoB(f) by A21,A16,A7,A20,A11,ZFMISC_1:87;
then GoB(f)*(i,width GoB(f)) = |[p`1,p`2]| by A21,A17,A8,A11,Def1;
then (Col(GoB(f),width GoB(f))).i = f/.n by A16,A20,A18,MATRIX_0:def 8;
hence thesis by A16,A20,A19,FUNCT_1:def 3;
end;