### The Mizar article:

### Introduction to Go-Board --- Part II

**by****Jaroslaw Kotowicz, and****Yatsuka Nakamura**

- Received August 24, 1992
Copyright (c) 1992 Association of Mizar Users

- MML identifier: GOBOARD2
- [ MML identifier index ]

environ vocabulary PRE_TOPC, EUCLID, FINSEQ_1, GOBOARD1, RELAT_1, FUNCT_1, FINSET_1, BOOLE, CARD_1, SEQ_2, SEQ_4, LATTICES, ARYTM_1, SQUARE_1, TOPREAL1, TARSKI, MCART_1, MATRIX_1, INCSP_1, TREES_1, ORDINAL2, SEQM_3, ABSVALUE, GOBOARD2, FINSEQ_4, ARYTM; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, FINSET_1, STRUCT_0, PRE_TOPC, ABSVALUE, CARD_1, SQUARE_1, SEQ_4, FINSEQ_4, MATRIX_1, EUCLID, TOPREAL1, GOBOARD1; constructors SEQM_3, REAL_1, NAT_1, ABSVALUE, SQUARE_1, SEQ_4, TOPREAL1, GOBOARD1, FINSEQ_4, INT_1, MEMBERED, XBOOLE_0; clusters FUNCT_1, GOBOARD1, FINSET_1, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1, INT_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM; definitions TARSKI, TOPREAL1, GOBOARD1, XBOOLE_0; theorems AXIOMS, TARSKI, REAL_1, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, CARD_1, SQUARE_1, SEQ_4, FINSEQ_2, CARD_2, REAL_2, MATRIX_1, EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, FINSEQ_4, RLVECT_1, FINSEQ_3, PROB_1, RELAT_1, PARTFUN2, GROUP_5, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes NAT_1, FINSEQ_2, MATRIX_1, GOBOARD1; 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, v,v1,v2 for FinSequence of REAL, n,m,i,j,k for Nat, G for Go-board, x for set; scheme PiLambdaD{D()-> non empty set, l()->Nat, F(set)-> Element of D()}: ex g being FinSequence of D() st len g=l() & for n st n in dom g holds g/.n=F(n) proof deffunc G(Nat) = F($1); consider g being FinSequence of D() such that A1: len g=l() & for n st n in Seg l() holds g.n=G(n) from SeqLambdaD; take g; thus len g=l() by A1; let n; assume A2: n in dom g; then n in Seg l() by A1,FINSEQ_1:def 3; then g.n = F(n) by A1; hence thesis by A2,FINSEQ_4:def 4; end; defpred P[Nat] means for R being finite Subset of REAL st R <> {} & card R = $1 holds R is bounded_above & upper_bound(R) in R & R is bounded_below & lower_bound(R) in R; Lm1: P[0] by CARD_2:59; Lm2: for n st P[n] holds P[n+1] proof let n such that A1: P[n]; let R be finite Subset of REAL such that A2: R <> {} & card R = n+1; now per cases; suppose n=0; then consider x such that A3: R={x} by A2,CARD_2:60; x in R by A3,TARSKI:def 1; then reconsider r=x as Real; r in R & R={r} by A3,TARSKI:def 1; then A4: R is bounded by SEQ_4:15; hence R is bounded_above by SEQ_4:def 3; upper_bound R = r by A3,SEQ_4:22; hence upper_bound R in R by A3,TARSKI:def 1; thus R is bounded_below by A4,SEQ_4:def 3; lower_bound R = r by A3,SEQ_4:22; hence lower_bound R in R by A3,TARSKI:def 1; suppose A5: n<>0; consider x being Element of R; reconsider x as Real by A2,TARSKI:def 3; reconsider X = R \ {x} as finite Subset of REAL; {x} c= R by A2,ZFMISC_1:37; then card (R\{x}) = card R - card {x} by CARD_2:63; then card X = n+1-1 by A2,CARD_1:79 .=n by XCMPLX_1:26; then A6: X is bounded_above & upper_bound X in X & X is bounded_below & lower_bound X in X by A1,A5,CARD_1:78; set u = upper_bound X, m = max(x,u), l = lower_bound X, mi = min(x,l); A7: x<=m & u<=m & mi<=x & mi<=l by SQUARE_1:35,46; A8: now let s be real number such that A9: s in R; now per cases; suppose s=x; hence s<=m by SQUARE_1:46; suppose s<>x; then not s in {x} by TARSKI:def 1; then s in X by A9,XBOOLE_0:def 4; then s<=u by A6,SEQ_4:def 4; hence s<=m by A7,AXIOMS:22; end; hence s<=m; end; hence A10: R is bounded_above by SEQ_4:def 1; A11: now let r be real number such that A12: 0<r; reconsider s = m as real number; take s; now per cases by SQUARE_1:49; suppose m=x; hence s in R by A2; thus m-r<s by A12,SQUARE_1:29; suppose m=u; hence s in R by A6,XBOOLE_0:def 4; thus m-r<s by A12,SQUARE_1:29; end; hence s in R & m-r<s; end; now per cases by SQUARE_1:49; suppose m=x; hence m in R by A2; suppose m=u; hence m in R by A6,XBOOLE_0:def 4; end; hence upper_bound R in R by A8,A10,A11,SEQ_4:def 4; A13: now let s be real number such that A14: s in R; now per cases; suppose s=x; hence mi<=s by SQUARE_1:35; suppose s<>x; then not s in {x} by TARSKI:def 1; then s in X by A14,XBOOLE_0:def 4; then l<=s by A6,SEQ_4:def 5; hence mi<=s by A7,AXIOMS:22; end; hence mi<=s; end; hence A15: R is bounded_below by SEQ_4:def 2; A16: now let r be real number such that A17: 0<r; reconsider s = mi as real number; take s; now per cases by SQUARE_1:38; suppose mi=x; hence s in R by A2; thus s<mi+r by A17,REAL_2:174; suppose mi=l; hence s in R by A6,XBOOLE_0:def 4; thus s<mi+r by A17,REAL_2:174; end; hence s in R & s<mi+r; end; now per cases by SQUARE_1:38; suppose mi=x; hence mi in R by A2; suppose mi=l; hence mi in R by A6,XBOOLE_0:def 4; end; hence lower_bound R in R by A13,A15,A16,SEQ_4:def 5; end; hence thesis; end; Lm3: for n holds P[n] from Ind(Lm1,Lm2); ::::::::::::::::::::::::::::: :: Real numbers prelimineries ::::::::::::::::::::::::::::: theorem Th1: for R being finite Subset of REAL holds R <> {} implies R is bounded_above & upper_bound(R) in R & R is bounded_below & lower_bound(R) in R proof let R be finite Subset of REAL; assume A1: R <> {}; P[card R] by Lm3; hence thesis by A1; end; begin canceled; theorem Th3: for f being FinSequence holds 1 <= n & n+1 <= len f iff n in dom f & n+1 in dom f proof let f be FinSequence; thus 1<=n & n+1 <= len f implies n in dom f & n+1 in dom f proof assume A1: 1<=n & n+1 <= len f; n<=n+1 by NAT_1:29; then 1<=n+1 & n<=len f by A1,AXIOMS:22; hence thesis by A1,FINSEQ_3:27; end; assume n in dom f & n+1 in dom f; hence thesis by FINSEQ_3:27; end; theorem Th4: for f being FinSequence holds 1 <= n & n+2 <= len f iff n in dom f & n+1 in dom f & n+2 in dom f proof let f be FinSequence; thus 1<=n & n+2 <= len f implies n in dom f & n+1 in dom f & n+2 in dom f proof assume A1: 1<=n & n+2 <= len f; then n<=n+1 & n<=n+2 & n+1<=n+1+1 & n+1+1=n+(1+1) & n+2<=len f by NAT_1:29,XCMPLX_1:1; then 1<=n+1 & 1<=n+2 & n+1<=len f & n<=len f by A1,AXIOMS:22; hence thesis by A1,FINSEQ_3:27; end; assume n in dom f & n+1 in dom f & n+2 in dom f; hence thesis by FINSEQ_3:27; end; theorem Th5: for D being non empty set, f1,f2 being FinSequence of D, n st 1 <= n & n <= len f2 holds (f1^f2)/.(n + len f1) = f2/.n proof let D be non empty set, f1,f2 be FinSequence of D, n such that A1: 1 <= n and A2: n <= len f2; A3: len f1 < n + len f1 by A1,RLVECT_1:103; len(f1^f2) = len f1 + len f2 by FINSEQ_1:35; then A4: n + len f1 <= len(f1^f2) by A2,AXIOMS:24; n + len f1 >= n by NAT_1:29; then n + len f1 >= 1 by A1,AXIOMS:22; hence (f1^f2)/.(n + len f1) = (f1^f2).(n + len f1) by A4,FINSEQ_4:24 .= f2.(n + len f1 - len f1) by A3,A4,FINSEQ_1:37 .= f2.n by XCMPLX_1:26 .= f2/.n by A1,A2,FINSEQ_4:24; end; 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 such that A2: m>n+1; A3: n <= n+1 & m <= m+1 by NAT_1:29; 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; 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:27; then not(1 <= n & n+1 <= len f & 1 <= m & m+1 <= len f) by A3,AXIOMS:22; then LSeg(f,m)={} or LSeg(f,n)={} by TOPREAL1:def 5; hence thesis by XBOOLE_1:65; 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 & f/.len f in LSeg(f,i) & i in dom f & i+1 in dom f and A4: i+1<>len f; A5: 1<=i & i<=len f & 1<=i+1 & i+1<=len f by A3,FINSEQ_3:27; then i+1<len f by A4,REAL_1:def 5; then A6: i+1+1<=len f & i+1+1=i+(1+1) by NAT_1:38,XCMPLX_1:1; then A7: i+1<=len f - 1 & 1<=len f & i+2 <= len f by A5,AXIOMS:22,REAL_1:84; then reconsider l=len f - 1 as Nat by INT_1:18; i<=l & 0<=1 by A5,REAL_1:84; then A8: 1<=l & l<=len f & l+1=len f by A5,AXIOMS:22,PROB_1:2,XCMPLX_1:27; then A9: l in dom f & l+1 in dom f by A7,FINSEQ_3:27; A10: f/.(l+1) in LSeg(f,l) by A8,TOPREAL1:27; l<>l+1 by NAT_1:38; then A11: f/.l<>f/.(l+1) by A3,A9,PARTFUN2:17; A12: LSeg(f,i)/\ LSeg(f,i+1)={f/.(i+1)} & i+2 in dom f by A1,A5,A6,Th4,TOPREAL1:def 8; A13: f/.(i+2) in LSeg(f,i+1) by A5,A6,TOPREAL1:27; now per cases; suppose A14: l=i+1; then f/.len f in LSeg(f,i) /\ LSeg(f,i+1) by A3,A6,A8,A13,XBOOLE_0:def 3; hence contradiction by A8,A11,A12,A14,TARSKI:def 1; suppose l<>i+1; then i+1<l by A7,REAL_1:def 5; then LSeg(f,i) misses LSeg(f,l) by A2,TOPREAL1:def 9; then LSeg(f,i) /\ LSeg(f,l) = {} by XBOOLE_0:def 7; hence contradiction by A3,A8,A10,XBOOLE_0:def 3; end; hence contradiction; end; theorem Th8: k<>0 & len f = k+1 implies L~f = L~(f|k) \/ LSeg(f,k) proof assume A1: k<>0 & len f = k+1; then A2: 0<k & k<=k+1 by NAT_1:19,29; then A3: 0+1<=k & k<=len f by A1,NAT_1:38; then A4: k in Seg k & k in dom f & len(f|k)=k & dom(f|k) = dom(f|k) & dom f=Seg len f by FINSEQ_1:3,def 3,FINSEQ_3:27,TOPREAL1:3; set f1 = f|k, lf = {LSeg(f,i): 1<=i & i+1 <= len f}, l1 = {LSeg(f1,j): 1<=j & j+1 <= len f1}; thus L~f c= L~(f|k) \/ LSeg(f,k) proof let x; assume x in L~f; then x in union lf by TOPREAL1:def 6; then consider X be set such that A5: x in X & X in lf by TARSKI:def 4; consider n such that A6: X=LSeg(f,n) & 1<=n & n+1 <= len f by A5; now per cases; suppose n+1 = len f; then n=k by A1,XCMPLX_1:2; hence thesis by A5,A6,XBOOLE_0:def 2; suppose n+1 <> len f; then A7: n+1 < len f by A6,REAL_1:def 5; then A8: n+1<=k & n<=k & n<=n+1 by A1,AXIOMS:24,NAT_1:38; n+1 <= k & 1<=n+1 by A1,A6,A7,NAT_1:38; then n in dom f1 & n+1 in dom f1 by A4,A6,A8,FINSEQ_3:27; then X=LSeg(f1,n) by A4,A6,TOPREAL3:24; then X in l1 by A4,A6,A8; then x in union l1 by A5,TARSKI:def 4; then x in L~f1 by TOPREAL1:def 6; hence thesis by XBOOLE_0:def 2; end; hence thesis; end; let x such that A9: x in L~f1 \/ LSeg(f,k); now per cases by A9,XBOOLE_0:def 2; suppose x in L~f1; then x in union l1 by TOPREAL1:def 6; then consider X be set such that A10: x in X & X in l1 by TARSKI:def 4; consider n such that A11: X=LSeg(f1,n) & 1<=n & n+1 <= len f1 by A10; n<=n+1 & n+1<=len f1 by A11,NAT_1:29; then A12: 1<=n+1 & n<=len f1 & n+1<=len f by A1,A2,A4,A11,AXIOMS:22; then n in dom f1 & n+1 in dom f1 & n+1 <= len f by A11,FINSEQ_3:27; then X=LSeg(f,n) by A4,A11,TOPREAL3:24; then X in lf by A11,A12; then x in union lf by A10,TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose A13: x in LSeg(f,k); LSeg(f,k) in lf by A1,A3; then x in union lf by A13,TARSKI:def 4; hence thesis by TOPREAL1:def 6; 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 & len f = k+1 and A2: f is unfolded and A3: f is s.n.c.; set f1 = f|k; A4: 1<=k & dom f=Seg len f & dom f1=Seg len f1 & k<=k+1 by A1,FINSEQ_1:def 3,NAT_1:29; then A5: k in dom f & k in Seg k by A1,FINSEQ_1:3; reconsider k1=k-1 as Nat by A1,INT_1:18; set f2 = f1|k1, l2 = {LSeg(f2,m): 1<=m & m+1<=len f2}; 1+1<=k & 0<=1 & 0<1 by A1,NAT_1:38; then A6: 1<=k1 & k1<=k & k1<k & k1<=k1+1 by NAT_1:29,REAL_1:84,SQUARE_1:29; then A7: 0+1<=k1 & k1+1<=k & 1<=k1+1 & Seg k1 c= Seg k & dom f2=Seg len f2 by FINSEQ_1:7,def 3,NAT_1:38; then A8: 0<k1 & k1 in Seg k & k1+1 in Seg k & len f1=k by A1,A4,A6,FINSEQ_1:3,NAT_1:38,TOPREAL1:3; then A9: k1+1=k & 0<>k1 & len f2 = k1 by A6,TOPREAL1:3,XCMPLX_1:27; then A10: L~f1=L~f2 \/ LSeg(f1,k1) & k+1=k1+(1+1) by A8,Th8,XCMPLX_1:1; L~f2 misses LSeg(f,k) proof assume not thesis; then consider x be set such that A11: x in L~f2 & x in LSeg(f,k) by XBOOLE_0:3; x in union l2 by A11,TOPREAL1:def 6; then consider X be set such that A12: x in X & X in l2 by TARSKI:def 4; consider n such that A13: X=LSeg(f2,n) & 1<=n & n+1<=len f2 by A12; A14: n+1<k by A6,A9,A13,AXIOMS:22; then n in dom f2 & n+1 in dom f2 & 1<k-n by A13,Th3,REAL_1:86; then LSeg(f2,n)=LSeg(f1,n) & n in dom f1 & n+1 in dom f1 by A4,A7,A8,A9,TOPREAL3:24; then LSeg(f2,n)=LSeg(f,n) by A5,TOPREAL3:24; then LSeg(f,n) meets LSeg(f,k) & LSeg(f,n) misses LSeg(f,k) by A3,A11,A12,A13,A14,TOPREAL1:def 9,XBOOLE_0:3; hence contradiction; end; then L~f2 /\ LSeg(f,k) = {} by XBOOLE_0:def 7; hence L~f1 /\ LSeg(f,k) = {} \/ LSeg(f1,k1) /\ LSeg(f,k) by A10,XBOOLE_1:23 .= LSeg(f,k1) /\ LSeg(f,k1+1) by A4,A5,A8,A9,TOPREAL3:24 .= {f/.k} by A1,A2,A6,A9,A10,TOPREAL1:def 8; 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 A1: len f1 < n & n+1 <= len f & m+len f1 = n; then A2: 1<=m & n<=len f & len f1 <n+1 by NAT_1:38,RLVECT_1:103; A3: n+1 <= len f & len f=len f1+len f2 by A1,FINSEQ_1:35; A4: n = m + len f1 & n+1 = m+1+len f1 by A1,XCMPLX_1:1; then A5: m+1<=len f2 by A3,REAL_1:53; m <= m + 1 by NAT_1:29; then m <= len f2 & m+1 >= 1 by A5,AXIOMS:22,NAT_1:29; then A6: f/.n=f2/.m & f/.(n+1)=f2/.(m+1) by A2,A4,A5,Th5; 0<=len f1 by NAT_1:18; then A7: 0+1<=n by A1,NAT_1:38; reconsider p=f/.n, q=f/.(n+1) as Point of TOP-REAL 2; thus LSeg(f,n)=LSeg(p,q) by A1,A7,TOPREAL1:def 5 .=LSeg(f2,m) by A2,A5,A6,TOPREAL1:def 5; end; theorem Th11: 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; assume x in L~f; then x in union lf by TOPREAL1:def 6; then consider X be set such that A1: x in X & X in lf by TARSKI:def 4; consider n such that A2: X=LSeg(f,n) & 1<=n & n+1 <= len f by A1; A3: dom f = Seg len f & len f1=len f +len g by FINSEQ_1:35,def 3; n<=n+1 & n+1<=len f & 0<=len g by A2,NAT_1:18,29; then 1<=n+1 & n<=len f & len f<=len f1 by A2,A3,AXIOMS:22,REAL_2:173; then n in dom f & n+1 in dom f & len f <= len f1 by A2,FINSEQ_3:27; then X=LSeg(f1,n) & n+1 <= len f1 by A2,AXIOMS:22,TOPREAL3:25; then X in l1 by A2; then x in union l1 by A1,TARSKI:def 4; hence thesis by TOPREAL1:def 6; 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; A2: dom f=Seg len f & dom f1=Seg len f1 & f1=f|(Seg i) & 0<=i by FINSEQ_1:def 3,NAT_1:18,TOPREAL1:def 1; per cases; suppose len f<i; then Seg len f c= Seg i by FINSEQ_1:7; hence thesis by A1,A2,RELAT_1:97; suppose A3: i<=len f; let n,m; assume m>n+1; then A4: LSeg(f,n) misses LSeg(f,m) & dom f1=dom f /\ Seg i by A1,A2,FUNCT_1:68,TOPREAL1:def 9; then A5: LSeg(f,n) /\ LSeg(f,m) = {} & dom f1=dom f /\ Seg i by XBOOLE_0: def 7; now per cases; suppose i=0; then not(1 <= n+1 & n+1<= len f1) by A4,FINSEQ_1:4,FINSEQ_3:27; then LSeg(f1,n)={} by NAT_1:29,TOPREAL1:def 5; hence thesis by XBOOLE_1:65; suppose i<>0; then 0+1<=i by A2,NAT_1:38; then A6: i in dom f by A3,FINSEQ_3:27; A7: n <= n+1 & m <= m+1 by NAT_1:29; now per cases; suppose A8: n in dom f1; now per cases; suppose n+1 in dom f1; then A9: LSeg(f,n)=LSeg(f1,n) by A6,A8,TOPREAL3:24; now per cases; suppose A10: m in dom f1; now per cases; suppose m+1 in dom f1; hence LSeg(f1,n) /\ LSeg(f1,m) = {} by A5,A6,A9,A10,TOPREAL3:24; suppose not m+1 in dom f1; then not(1 <= m+1 & m+1<= len f1) by FINSEQ_3:27; then LSeg(f1,m)={} by NAT_1:29,TOPREAL1:def 5; hence LSeg(f1,n) /\ LSeg(f1,m) = {}; end; hence thesis by XBOOLE_0:def 7; suppose not m in dom f1; then not(1 <= m & m <= len f1) by FINSEQ_3:27; then not(1 <= m & m+1 <= len f1) by A7,AXIOMS:22; then LSeg(f1,m)={} by TOPREAL1:def 5; hence thesis by XBOOLE_1:65; end; hence thesis; suppose not n+1 in dom f1; then not(1 <= n+1 & n+1<= len f1) by FINSEQ_3:27; then LSeg(f1,n)={} by NAT_1:29,TOPREAL1:def 5; hence thesis by XBOOLE_1:65; end; hence thesis; suppose not n in dom f1; then not(1 <= n & n <= len f1) by FINSEQ_3:27; then not(1 <= n & n+1 <= len f1) by A7,AXIOMS:22; then LSeg(f1,n)={} by TOPREAL1:def 5; hence thesis by XBOOLE_1:65; 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; set f = f1^f2; let n; set p =f/.n, q =f/.(n+1); assume that A4: 1 <= n & n+1 <= len f; A5: dom f1=Seg len f1 & dom f2=Seg len f2 & len f=len f1+len f2 & n+1-len f1=n-len f1+1 by FINSEQ_1:35,def 3,XCMPLX_1:29; per cases; suppose A6: n+1 <= len f1; then n in dom f1 & n+1 in dom f1 by A4,Th3; then f1/.n=p & f1/.(n+1)=q by GROUP_5:95; hence p`1=q`1 or p`2=q`2 by A1,A4,A6,TOPREAL1:def 7; suppose len f1 < n+1; then A7: len f1<=n by NAT_1:38; then reconsider n1=n-len f1 as Nat by INT_1:18; now per cases; suppose A8: n=len f1; then n in dom f1 by A4,FINSEQ_3:27; then A9: p=f1/.n by GROUP_5:95; len f2 >= 1 by A4,A5,A8,REAL_1:53; hence p`1=q`1 or p`2=q`2 by A3,A8,A9,Th5; suppose n<>len f1; then A10: len f1<n & n<=n+1 by A7,NAT_1:29,REAL_1:def 5; then len f1+1<=n & len f1<n+1 & n+1<=len f by A4,NAT_1:38; then A11: 1<=n1 & n<=len f by A10,AXIOMS:22,REAL_1:84; A12: n = n1 + len f1 by XCMPLX_1:27; then A13: n+1 = n1 + 1 + len f1 by XCMPLX_1:1; then A14: n1+1<=len f2 by A4,A5,REAL_1:53; n1 + 1 >= n1 by NAT_1:29; then n1 <= len f2 by A14,AXIOMS:22; then A15: f2/.n1=p by A11,A12,Th5; n1 + 1 >= 1 by NAT_1:29; then f2/.(n1+1)=q by A13,A14,Th5; hence p`1=q`1 or p`2=q`2 by A2,A11,A14,A15,TOPREAL1:def 7; end; hence thesis; end; theorem Th14: f <> {} implies X_axis(f) <> {} proof assume f <> {} & X_axis(f) = {}; then len X_axis(f) = len f & len f <> 0 & len X_axis(f) = 0 by FINSEQ_1:25,GOBOARD1:def 3; hence contradiction; end; theorem Th15: f <> {} implies Y_axis(f) <> {} proof assume f <> {} & Y_axis(f) = {}; then len Y_axis(f) = len f & len f <> 0 & len Y_axis(f) = 0 by FINSEQ_1:25,GOBOARD1:def 4; hence contradiction; end; definition let f be non empty FinSequence of TOP-REAL 2; cluster X_axis f -> non empty; coherence by Th14; cluster Y_axis f -> non empty; coherence by Th15; end; theorem Th16: f is special implies for n st n in dom f & n+1 in dom f holds for i,j,m,k 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 such that A2: n in dom f & n+1 in dom f; let i,j,m,k such that A3: [i,j] in Indices G & [m,k] in Indices G & f/.n=G*(i,j) & f/.(n+1)=G*(m,k); assume A4: i<>m & k<>j; 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); Indices G = [:dom G,Seg width G:] by MATRIX_1:def 5; then A5: i in dom G & j in Seg width G & m in dom G & k in Seg width G & len cj=len G & len xj=len cj & dom xj=Seg len xj & len lm=width G & len xm=len lm & dom xm=Seg len xm & len yj=len cj & dom yj=Seg len yj & len ym=len lm & dom ym=Seg len ym by A3,FINSEQ_1:def 3,GOBOARD1:def 3,def 4,MATRIX_1:def 8,def 9,ZFMISC_1:106 ; then A6: dom cj = dom G & dom lm = Seg width G & dom xj = dom cj & dom xm = dom lm & dom yj = dom cj & dom ym = dom lm by FINSEQ_3:31; then cj/.i = cj.i & cj/.m = cj.m & lm/.j = lm.j & lm/.k = lm.k by A5,FINSEQ_4:def 4; then G*(i,j)=cj/.i & G*(m,j)=cj/.m & G*(m,j)=lm/.j & G*(m,k)=lm/.k by A5,MATRIX_1:def 8,def 9; then A7: xj is increasing & xj.i=G*(i,j)`1 & xj.m=G*(m,j)`1 & xm is constant & xm.j=G*(m,j)`1 & xm.k=G*(m,k)`1 & ym is increasing & ym.j=G*(m,j)`2 & ym.k=G*(m,k)`2 & yj is constant & yj.i=G*(i,j)`2 & yj.m=G*(m,j)`2 by A5,A6,GOBOARD1:def 3,def 4,def 6,def 7,def 8,def 9; A8: 1 <= n & n +1 <= len f by A2,FINSEQ_3:27; now per cases by A1,A3,A8,TOPREAL1:def 7; suppose A9: G*(i,j)`1=G*(m,k)`1; now per cases by A4,AXIOMS:21; suppose i>m; then G*(m,j)`1<G*(i,j)`1 by A5,A6,A7,GOBOARD1:def 1; hence contradiction by A5,A7,A9,GOBOARD1:def 2; suppose i<m; then G*(m,j)`1>G*(i,j)`1 by A5,A6,A7,GOBOARD1:def 1; hence contradiction by A5,A7,A9,GOBOARD1:def 2; end; hence contradiction; suppose A10: G*(i,j)`2=G*(m,k)`2; now per cases by A4,AXIOMS:21; suppose k>j; then G*(m,j)`2<G*(m,k)`2 by A5,A7,GOBOARD1:def 1; hence contradiction by A5,A6,A7,A10,GOBOARD1:def 2; suppose k<j; then G*(m,j)`2>G*(m,k)`2 by A5,A7,GOBOARD1:def 1; hence contradiction by A5,A6,A7,A10,GOBOARD1:def 2; end; hence contradiction; end; hence contradiction; end; theorem (for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) & f is special & (for n 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 st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) & f is special & for n 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: P[0] proof let f such that A2: len f=0 & (for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) & f is special & for n st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1); take g=f; f={} by A2,FINSEQ_1:25; then for n holds n in dom g & n+1 in dom g implies ( for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1) by FINSEQ_1:26; hence g is_sequence_on G & L~f = L~g & g/.1=f/.1 & g/.len g=f/.len f & len f<=len g by A2,GOBOARD1:def 11; end; A3: for k st P[k] holds P[k+1] proof let k such that A4: P[k]; let f such that A5: len f=k+1 and A6: for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j) and A7: f is special and A8: for n st n in dom f & n+1 in dom f holds f/.n <> f/.(n+1); A9: dom f = Seg len f by FINSEQ_1:def 3; now per cases; suppose k=0; then A10: dom f = {1} by A5,FINSEQ_1:4,def 3; take g=f; now let n; assume n in dom g & n+1 in dom g; then n=1 & n+1=1 by 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 abs(i1-j1)+abs(i2-j2)=1; end; hence g is_sequence_on G & L~f=L~g & g/.1=f/.1 & g/.len g=f/.len f & len f<=len g by A6,GOBOARD1:def 11; suppose A11: k<>0; then A12: 0<k & k<=k+1 by NAT_1:19,29; then A13: 0+1<=k & k<=len f & k+1 <= len f by A5,NAT_1:38; then A14: k in dom f & len (f|k)=k & dom(f|k)=Seg len(f|k) & k in Seg k & 1 in Seg k by A9,FINSEQ_1:3,def 3,TOPREAL1:3; set f1=f|k; A15: now let n; assume A16: n in dom f1; then f1/.n=f/.n & n in dom f by A14,GOBOARD1:10; then consider i,j such that A17: [i,j] in Indices G & f/.n=G*(i,j) by A6; take i,j; thus [i,j] in Indices G & f1/.n=G*(i,j) by A14,A16,A17,GOBOARD1:10; end; A18: f1 is special proof let n; set p =f1/.n, q =f1/.(n+1); assume A19: 1 <= n & n+1 <= len f1; n <= n+1 by NAT_1:29; then 1 <= n+1 & n <= len f1 by A19,AXIOMS:22; then n in dom f1 & n+1 in dom f1 by A19,FINSEQ_3:27; then A20: f1/.n=f/.n & f1/.(n+1)=f/.(n+1) by A14,GOBOARD1:10; n+1 <= len f by A5,A12,A14,A19,AXIOMS:22; hence p`1=q`1 or p`2=q`2 by A7,A19,A20,TOPREAL1:def 7; end; now let n; assume A21: n in dom f1 & n+1 in dom f1; then A22: n in dom f & n+1 in dom f by A14,GOBOARD1:10; f1/.n=f/.n & f1/.(n+1)=f/.(n+1) by A14,A21,GOBOARD1:10; hence f1/.n <> f1/.(n+1) by A8,A22; end; then consider g1 such that A23: g1 is_sequence_on G & L~g1=L~f1 & g1/.1=f1/.1 & g1/.len g1=f1/.len f1 & len f1<=len g1 by A4,A14,A15,A18; consider i1,i2 be Nat such that A24: [i1,i2] in Indices G & f/.k=G*(i1,i2) by A6,A14; 1<=len f by A13,AXIOMS:22; then A25: k+1 in dom f by A5,FINSEQ_3:27; then consider j1,j2 be Nat such that A26: [j1,j2] in Indices G & f/.(k+1)=G*(j1,j2) by A6; A27: Indices G = [:dom G,Seg width G:] by MATRIX_1:def 5; then A28: i1 in dom G & i2 in Seg width G & j1 in dom G & j2 in Seg width G by A24,A26,ZFMISC_1:106; A29: (for n st n in dom g1 ex m,k st [m,k] in Indices G & g1/.n=G*(m,k)) & for n st n in dom g1 & n+1 in dom g1 holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & g1/.n = G*(m,k) & g1/.(n+1) = G*(i,j) holds abs(m-i)+abs(k-j) = 1 by A23,GOBOARD1:def 11; A30: dom g1 = Seg len g1 by FINSEQ_1:def 3; 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); A31: x1 is constant by A28,GOBOARD1:def 6; A32: y1 is increasing by A28,GOBOARD1:def 8; A33: x2 is increasing by A28,GOBOARD1:def 9; A34: y2 is constant by A28,GOBOARD1:def 7; A35: dom x1=Seg len x1 by FINSEQ_1:def 3; A36: dom y1=Seg len y1 by FINSEQ_1:def 3; A37: len y1=len l1 by GOBOARD1:def 4; A38: len x1=len l1 by GOBOARD1:def 3; A39: len l1=width G by MATRIX_1:def 8; A40: len x2=len c1 by GOBOARD1:def 3; A41: len y2=len c1 by GOBOARD1:def 4; len c1 = len G by MATRIX_1:def 9; then A42: dom c1 = dom G by FINSEQ_3:31; A43: dom y1 = dom l1 & dom x1 = dom l1 & dom x2 = dom c1 & dom y2 = dom c1 by A37,A38,A40,A41,FINSEQ_3:31; now per cases by A7,A14,A24,A25,A26,Th16; suppose A44: i1=j1; set ppi = G*(i1,i2), pj = G*(i1,j2); now per cases by AXIOMS:21; case A45: i2>j2; then reconsider l=i2-j2 as Nat by INT_1:18; A46: now let n; assume n in Seg l; then A47: 1<=n & n<=l & 0<=j2 by FINSEQ_1:3,NAT_1:18; then l<=i2 by PROB_1:2; then n<=i2 by A47,AXIOMS:22; then reconsider w=i2-n as Nat by INT_1:18; 0<=n & i2-l<=i2-n by A47,AXIOMS:22,REAL_1:92; then i2-n<=i2 & i2<=width G & j2<=w & 1<=j2 by A28,FINSEQ_1:3,PROB_1:2,XCMPLX_1:18; then 1<=w & w<=width G by AXIOMS:22; then w in Seg width G by FINSEQ_1:3; hence i2-n is Nat & [i1,i2-n] in Indices G & i2-n in Seg width G by A27,A28,ZFMISC_1:106; end; defpred P1[Nat,set] means for m st m=i2-$1 holds $2=G*(i1,m); A48: now let n; assume n in Seg l; then reconsider m=i2-n as Nat by A46; take p=G*(i1,m); thus P1[n,p]; end; consider g2 such that A49: len g2 = l & for n st n in Seg l holds P1[n,g2/.n] from FinSeqDChoice(A48); A50: dom g2 = Seg l by A49,FINSEQ_1:def 3; take g=g1^g2; now let n; assume A51: n in dom g2; then reconsider m=i2-n as Nat by A46,A50; take k=i1,m; thus [k,m] in Indices G & g2/.n=G*(k,m) by A46,A49,A50,A51; end; then A52: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A29,GOBOARD1:39; A53: now let n; assume A54: n in dom g2 & n+1 in dom g2; then A55: i2-n is Nat & [i1,i2-n] in Indices G & P1[n,g2/.n] & i2-(n+1) is Nat & [i1,i2-(n+1)] in Indices G & P1[n+1,g2/.(n+1)] by A46,A49,A50; reconsider m1=i2-n ,m2=i2-(n+1) as Nat by A46,A50,A54; A56: g2/.n=G*(i1,m1) & g2/.(n+1)=G*(i1,m2) by A49,A50,A54; let l1,l2,l3,l4 be Nat; assume [l1,l2] in Indices G & [l3,l4] in Indices G & g2/.n=G*(l1,l2) & g2/.(n+1)=G*(l3,l4); then l1=i1 & l2=m1 & l3=i1 & l4=m2 & 0<=1 by A55,A56,GOBOARD1:21; hence abs(l1-l3)+abs(l2-l4)=abs(0)+abs(i2-n-(i2-(n+1))) by XCMPLX_1:14 .= 0+abs(i2-n-(i2-(n+1))) by ABSVALUE:7 .= abs(i2-n-(i2-n-1)) by XCMPLX_1:36 .= abs(1) by XCMPLX_1:18 .= 1 by ABSVALUE:def 1; end; A57: now let l1,l2,l3,l4 be Nat; assume A58: [l1,l2] in Indices G & [l3,l4] in Indices G & g1/.len g1=G*(l1,l2) & g2/.1=G*(l3,l4) & len g1 in dom g1 & 1 in dom g2; then A59: i2-1 is Nat & [i1,i2-1] in Indices G & P1[1,g2/.1] & f1/.len f1=f/.k by A14,A46,A49,A50,GOBOARD1:10; reconsider m1=i2-1 as Nat by A46,A50,A58; g2/.1=G*(i1,m1) by A49,A50,A58; then l1=i1 & l2=i2 & l3=i1 & l4=m1 & 0<=1 by A23,A24,A58,A59, GOBOARD1:21; hence abs(l1-l3)+abs(l2-l4)=abs(0)+abs(i2-(i2-1)) by XCMPLX_1:14 .=0+abs(i2-(i2-1)) by ABSVALUE:7 .=abs(1) by XCMPLX_1:18 .=1 by ABSVALUE:def 1; end; then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by A29,A53,GOBOARD1:40; hence g is_sequence_on G by A52,GOBOARD1:def 11; set lk={w where w is Point of TOP-REAL 2: w`1=ppi`1 & pj`2<=w`2 & w`2<=ppi`2}; i2 in dom l1 & j2 in dom l1 by A28,A39,FINSEQ_1:def 3; then l1/.i2 = l1.i2 & l1/.j2 = l1.j2 by FINSEQ_4:def 4; then A60: l1/.i2=ppi & l1/.j2=pj by A28,MATRIX_1:def 8; then A61: y1.i2=ppi`2 & y1.j2=pj`2 & x1.i2=ppi`1 & x1.j2=pj`1 by A28,A35,A36,A37,A38,A39,GOBOARD1:def 3,def 4; then A62: pj`2<ppi`2 & ppi`1=pj`1 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj`2]| by A28,A31,A32,A35,A36,A37,A38,A39,A45,EUCLID:57,GOBOARD1:def 1,def 2; A63: LSeg(f,k)=LSeg(pj,ppi) by A13,A24,A26,A44,TOPREAL1:def 5 .= lk by A62,TOPREAL3:15; 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}; A64: len g = len g1 + len g2 by FINSEQ_1:35; A65: now let j; assume A66: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A67: p=g/.j; A68: dom l1 = Seg len l1 by FINSEQ_1:def 3; now per cases; suppose A69: j=len g1; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A70: g/.len g1 = f1/.len f1 by A23,GROUP_5:95 .= G*(i1,i2) by A14,A24,GOBOARD1:10; hence p`1=G*(i1,i2)`1 by A67,A69; thus G*(i1,j2)`2<=p`2 & p`2<=G*(i1,i2)`2 by A28,A32,A36,A37,A39, A45,A61,A67,A69,A70,GOBOARD1:def 1; thus p in rng l1 by A28,A39,A60,A67,A68,A69,A70,PARTFUN2:4; suppose A71: j<>len g1; then A72: len g1 < j by A66,REAL_1:def 5; j - len g1 <> 0 by A71,XCMPLX_1:15; then A73: w >= 1 by RLVECT_1:99; A74: w + len g1 = j by XCMPLX_1:27; then A75: w <= len g2 by A64,A66,REAL_1:53; then A76: len g1 + 1<=j & g/.j=g2/.w by A72,A73,A74,Th5,NAT_1:38; A77: w in dom g2 by A73,A75,FINSEQ_3:27; then A78: i2-w is Nat & i2-w in Seg width G & P1[w,g2/.w] by A46,A49,A50; reconsider u=i2-w as Nat by A46,A50,A77; u in dom l1 by A39,A78,FINSEQ_1:def 3; then g2/.w = g2.w & l1/.u = l1.u by A77,FINSEQ_4:def 4; then A79: g2/.w=G*(i1,u) & l1/.u=G*(i1,u) by A78,MATRIX_1:def 8; then A80: x1.i2=ppi`1 & x1.u=G*(i1,u)`1 & y1.i2=ppi`2 & y1.u=G*(i1,u)`2 & y1.j2=pj`2 by A28,A35,A36,A37,A38,A39,A60,A78,GOBOARD1:def 3,def 4; hence p`1=G*(i1,i2)`1 by A28,A31,A35,A38,A39,A67,A76,A78,A79,GOBOARD1:def 2; now per cases; suppose u=j2; hence G*(i1,j2)`2<=p`2 by A67,A73,A74,A75,A79,Th5; suppose A81: u<>j2; i2-len g2<=u & len g2=l by A49,A75,REAL_1:92; then j2<=u by XCMPLX_1:18; then j2<u by A81,REAL_1:def 5; hence G*(i1,j2)`2<= p`2 by A28,A32,A36,A37,A39,A67,A76,A78,A79,A80,GOBOARD1:def 1; end; hence G*(i1,j2)`2<=p`2; u<=i2-1 & i2-1<i2 by A73,REAL_1:92,SQUARE_1:29; then u<i2 by AXIOMS:22; hence p`2<= G*(i1,i2)`2 by A28,A32,A36,A37,A39,A67,A76,A78,A79,A80,GOBOARD1:def 1; thus p in rng l1 by A39,A67,A68,A76,A78,A79,PARTFUN2:4; 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; assume x in L~g; then x in union lg by TOPREAL1:def 6; then consider X be set such that A82: x in X & X in lg by TARSKI:def 4; consider i such that A83: X=LSeg(g,i) & 1<=i & i+1<=len g by A82; now per cases; suppose A84: i+1 <= len g1; then i<=i+1 & i+1<=len g1 by NAT_1:29; then 1<=i & i<=len g1 & 1<=i+1 & i+1<=len g1 by A83,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A83,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A83,A84; then x in union {LSeg(g1,j): 1<=j & j+1<=len g1} by A82,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A23,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A85: i+1 > len g1; then A86: len g1<=i & i<=i+1 & i+1<=len g by A83,NAT_1:38; A87: 1<=i+1 & len g1<=i+1 & i<=len g by A83,A85,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A88: q1`1=ppi`1 & pj`2<=q1`2 & q1`2<=ppi`2 & q2`1=ppi`1 & pj`2<= q2`2 & q2`2<=ppi`2 by A65,A86,A87; then A89: q1=|[q1`1,q1`2]| & q2=|[q1`1,q2`2]| by EUCLID:57; A90: LSeg(g,i)=LSeg(q2,q1) by A83,TOPREAL1:def 5; now per cases by AXIOMS:21; suppose q1`2>q2`2; then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1`2} by A89,A90,TOPREAL3:15; then consider p2 such that A91: p2=x & p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1`2 by A82,A83; pj`2<=p2`2 & p2`2<=ppi`2 by A88,A91,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A63,A88,A91; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`2=q2`2; then LSeg(g,i)={q1} by A89,A90,TOPREAL1:7; then x=q1 by A82,A83,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A63,A88; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`2<q2`2; then LSeg(g,i)= {p1: p1`1=q1`1 & q1`2<=p1`2 & p1`2<=q2`2} by A89,A90,TOPREAL3:15; then consider p2 such that A92: p2=x & p2`1=q1`1 & q1`2<=p2`2 & p2`2<=q2`2 by A82,A83; pj`2<=p2`2 & p2`2<=ppi`2 by A88,A92,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A63,A88,A92; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; hence thesis; end; let x; assume x in L~f; then A93: x in L~f1 \/ LSeg(f,k) by A5,A11,Th8; now per cases by A93,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A23,Th11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A94: p1=x & p1`1=ppi`1 & pj`2<=p1`2 & p1`2<=ppi`2 by A63; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`2>=p1`2; A95: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A64,REAL_2:173; let q such that A96: q=g/.n; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A23,A96,GROUP_5:95 .=G*(i1,i2) by A14,A24,GOBOARD1:10; hence p1`2<=q`2 by A94; end; end; A97: for n holds P2[n] implies n<=len g; consider ma be Nat such that A98: P2[ma] & for n st P2[n] holds n<=ma from Max(A97,A95); now per cases; suppose A99: ma=len g; j2+1<=i2 by A45,NAT_1:38; then A100: 1<=l & l=len g2 by A49,REAL_1:84; then A101: l in dom g2 & i2-l=j2 by A50,FINSEQ_1:3,XCMPLX_1:18; then A102: g/.ma=g2/.l by A49,A64,A99,GROUP_5:96 .= pj by A49,A50,A101; then p1`2<=pj`2 by A98; then A103: p1`2=pj`2 & p1=|[p1`1,p1`2]| by A94,AXIOMS:21,EUCLID: 57; A104: ma <= len g + 1 & len g1+1<=ma & ma <= len g by A64,A99,A100,NAT_1:29,REAL_1:55; 1 <= len g1 + 1 by NAT_1:29; then A105: 0+1<=ma by A104,AXIOMS:22; then A106: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A105,INT_1:18; A107: ma in dom g by A99,A106,FINSEQ_1:def 3; A108: m1 + 1 = ma by XCMPLX_1:27; then A109: m1 >= len g1 by A104,REAL_1:53; 1<=len g1 by A13,A14,A23,AXIOMS:22; then A110: 1<=m1 by A109,AXIOMS:22; A111: m1 <= len g by A99,A108,NAT_1:29; then A112: m1 in dom g by A110,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A113: q`1=ppi`1 by A65,A109,A111; A114: pj`2<=q`2 by A65,A109,A111; A115: q=|[q`1,q`2]| by EUCLID:57; A116: LSeg(g,m1)=LSeg(pj,q) by A99,A102,A108,A110,TOPREAL1:def 5; set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1 & pj`2<=e`2 & e`2<=q`2}; now assume q`2=pj`2; then 1=abs(i1-i1)+abs(j2-j2) by A26,A29,A44,A53,A57,A62,A102,A107,A108,A112,A113,A115, GOBOARD1:40 .=abs(0)+abs(j2-j2) by XCMPLX_1:14 .=abs(0)+abs(0) by XCMPLX_1:14 .=abs(0)+0 by ABSVALUE:7 .=0 by ABSVALUE:7; hence contradiction; end; then pj`2<q`2 by A114,REAL_1:def 5; then LSeg(g,m1)=lq by A62,A113,A115,A116,TOPREAL3:15; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A94,A99,A103,A108,A110,A114; then x in union lg by A94,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A98,REAL_1:def 5; then ma+1<=len g & k<=ma & ma<=ma+1 by A14,A23,A98,AXIOMS:22,NAT_1:38; then A117: 1<=ma & ma+1 <= len g & len g1<=ma+1 by A13,A98,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A118: p1`2<=qa`2 by A98; A119: now assume p1`2<=qa1`2; then for q holds q=g/.(ma+1) implies p1`2<=q`2; then ma+1<=ma by A98,A117; hence contradiction by REAL_2:174; end; then A120: qa1`2<qa`2 & qa1`2<=p1`2 & p1`2<=qa`2 & qa`1=ppi`1 & qa1 `1 = ppi`1 by A65,A98,A117,A118,AXIOMS:22; set lma = {p2: p2`1=ppi`1 & qa1`2<=p2`2 & p2`2<=qa`2}; A121: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa1,qa) by A117,TOPREAL1:def 5 .= lma by A120,A121,TOPREAL3:15; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A94,A117,A118,A119; then x in union lg by TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; end; hence x in L~g; end; hence x in L~g; end; 1<=len g1 by A13,A14,A23,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A23,GROUP_5:95 .=f/.1 by A14,GOBOARD1:10; j2+1<=i2 by A45,NAT_1:38; then A122: 1<=l by REAL_1:84; then A123: l in dom g2 & len g=len g1 + len g2 & len g2 = l by A50,FINSEQ_1:3,35,def 3; then reconsider m1=i2-l as Nat by A46,A50; thus g/.len g=g2/.l by A123,GROUP_5:96 .=G*(i1,m1) by A49,A50,A123 .=f/.len f by A5,A26,A44,XCMPLX_1:18; thus len f<=len g by A5,A14,A23,A122,A123,REAL_1:55; case i2=j2; hence contradiction by A8,A14,A24,A25,A26,A44; case A124: i2<j2; then reconsider l=j2-i2 as Nat by INT_1:18; deffunc F(Nat) = G*(i1,i2+$1); consider g2 such that A125: len g2=l & for n st n in dom g2 holds g2/.n=F(n) from PiLambdaD; A126: dom g2 = Seg l by A125,FINSEQ_1:def 3; take g=g1^g2; A127: now let n; assume n in Seg l; then A128: 1<=n & n<=l by FINSEQ_1:3; then n<=n+i2 & i2+n<=l+i2 by NAT_1:29,REAL_1:55; then n<=i2+n & i2+n<=j2 & j2<=width G by A28,FINSEQ_1:3,XCMPLX_1:27; then 1<=i2+n & i2+n<=width G by A128,AXIOMS:22; hence i2+n in Seg width G by FINSEQ_1:3; hence [i1,i2+n] in Indices G by A27,A28,ZFMISC_1:106; end; A129: dom g2 = Seg len g2 by FINSEQ_1:def 3; now let n such that A130: n in dom g2; take m=i1,k=i2+n; thus [m,k] in Indices G & g2/.n=G*(m,k) by A125,A127,A129,A130; end; then A131: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A29,GOBOARD1:39; A132: now let n; assume n in dom g2 & n+1 in dom g2; then A133: g2/.n=G*(i1,i2+n) & [i1,i2+n] in Indices G & g2/.(n+1)=G*(i1,i2+(n+1)) & [i1,i2+(n+1)] in Indices G by A125,A127,A129; let l1,l2,l3,l4 be Nat; assume [l1,l2] in Indices G & [l3,l4] in Indices G & g2/.n=G*(l1,l2) & g2/.(n+1)=G*(l3,l4); then l1=i1 & l2=i2+n & l3=i1 & l4=i2+(n+1) & 0<=1 by A133,GOBOARD1: 21; hence abs(l1-l3)+abs(l2-l4)=abs(0)+abs(i2+n-(i2+(n+1))) by XCMPLX_1: 14 .= 0+abs(i2+n-(i2+(n+1))) by ABSVALUE:7 .= abs(i2+n-(i2+n+1)) by XCMPLX_1:1 .= abs(i2+n-(i2+n)-1) by XCMPLX_1:36 .= abs(i2+n-(i2+n)+-1) by XCMPLX_0:def 8 .= abs(-1) by XCMPLX_1:25 .= abs(1) by ABSVALUE:17 .= 1 by ABSVALUE:def 1; end; A134: now let l1,l2,l3,l4 be Nat; assume A135: [l1,l2] in Indices G & [l3,l4] in Indices G & g1/.len g1=G*(l1, l2) & g2/.1=G*(l3,l4) & len g1 in dom g1 & 1 in dom g2; then g2/.1=G* (i1,i2+1) & [i1,i2+1] in Indices G & f1/.len f1=f/.k by A14,A125,A127,A129,GOBOARD1:10; then l1=i1 & l2=i2 & l3=i1 & l4=i2+1 & 0<=1 by A23,A24,A135,GOBOARD1 :21; hence abs(l1-l3)+abs(l2-l4)=abs(0)+abs(i2-(i2+1)) by XCMPLX_1:14 .=0+abs(i2-(i2+1)) by ABSVALUE:7 .=abs(i2-i2-1) by XCMPLX_1:36 .=abs(i2-i2+-1) by XCMPLX_0:def 8 .=abs(-1) by XCMPLX_1:25 .=abs(1) by ABSVALUE:17 .=1 by ABSVALUE:def 1; end; then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by A29,A132,GOBOARD1:40; hence g is_sequence_on G by A131,GOBOARD1:def 11; set lk={w where w is Point of TOP-REAL 2: w`1=ppi`1 & ppi`2<=w`2 & w`2<= pj`2}; i2 in dom l1 & j2 in dom l1 by A28,A39,FINSEQ_1:def 3; then l1/.i2 = l1.i2 & l1/.j2 = l1.j2 by FINSEQ_4:def 4; then A136: l1/.i2=ppi & l1/.j2=pj by A28,MATRIX_1:def 8; then A137: y1.i2=ppi`2 & y1.j2=pj`2 & x1.i2=ppi`1 & x1.j2=pj`1 by A28,A35,A36,A37,A38,A39,GOBOARD1:def 3,def 4; then A138: ppi`2<pj`2 & ppi`1=pj`1 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj`2]| by A28,A31,A32,A35,A36,A37,A38,A39,A124,EUCLID:57,GOBOARD1:def 1,def 2; A139: LSeg(f,k)=LSeg(ppi,pj) by A13,A24,A26,A44,TOPREAL1:def 5 .= lk by A138,TOPREAL3:15; 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}; A140: len g = len g1 + len g2 by FINSEQ_1:35; A141: now let j; assume A142: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A143: p=g/.j; set u=i2+w; A144: dom l1 = Seg len l1 by FINSEQ_1:def 3; now per cases; suppose A145: j=len g1; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A146: g/.len g1 = f1/.len f1 by A23,GROUP_5:95 .= G*(i1,i2) by A14,A24,GOBOARD1:10; hence p`1=G*(i1,i2)`1 by A143,A145; thus G*(i1,i2)`2<=p`2 & p`2<=G* (i1,j2)`2 by A28,A32,A36,A37,A39,A124,A137,A143,A145,A146,GOBOARD1:def 1; thus p in rng l1 by A28,A39,A136,A143,A144,A145,A146,PARTFUN2:4; suppose A147: j<>len g1; then A148: len g1 < j by A142,REAL_1:def 5; A149: j - len g1 <> 0 by A147,XCMPLX_1:15; then A150: w >= 1 by RLVECT_1:99; A151: w + len g1 = j by XCMPLX_1:27; then A152: w <= len g2 by A140,A142,REAL_1:53; then A153: len g1 + 1<=j & g/.j=g2/.w by A148,A150,A151,Th5,NAT_1 :38; A154: w in dom g2 by A150,A152,FINSEQ_3:27; then u in Seg width G by A126,A127; then u in dom l1 by A39,FINSEQ_1:def 3; then A155: g2/.w = g2.w & l1/.u = l1.u by A154,FINSEQ_4:def 4; A156: g2/.w=G* (i1,u) & u in Seg width G by A125,A126,A127,A154; then A157: l1/.u=G*(i1,u) by A155,MATRIX_1:def 8; then A158: x1.i2=ppi`1 & x1.u=G*(i1,u)`1 & y1.i2=ppi`2 & y1.u=G*(i1,u) `2 & y1.j2=pj`2 by A28,A35,A36,A37,A38,A39,A136,A156,GOBOARD1:def 3,def 4; hence p`1=G*(i1,i2)`1 by A28,A31,A35,A38,A39,A143,A153,A156,GOBOARD1:def 2; 0+1<=w by A149,RLVECT_1:99; then 0<w by NAT_1:38; then i2<u by REAL_2:174; hence G*(i1,i2)`2<= p`2 by A28,A32,A36,A37,A39,A143,A153,A156,A158,GOBOARD1:def 1; now per cases; suppose u=j2; hence p`2<=G*(i1,j2)`2 by A143,A150,A151,A152,A156,Th5; suppose A159: u<>j2; u<=i2+l by A125,A152,REAL_1:55; then u<=j2 by XCMPLX_1:27; then u<j2 by A159,REAL_1:def 5; hence p`2<=G*(i1,j2)`2 by A28,A32,A36,A37,A39,A143,A153,A156, A158,GOBOARD1:def 1; end; hence p`2<=G*(i1,j2)`2; thus p in rng l1 by A39,A143,A144,A153,A156,A157,PARTFUN2:4; 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; assume x in L~g; then x in union lg by TOPREAL1:def 6; then consider X be set such that A160: x in X & X in lg by TARSKI:def 4; consider i such that A161: X=LSeg(g,i) & 1<=i & i+1 <= len g by A160; now per cases; suppose A162: i+1 <= len g1; then i<=i+1 & i+1<=len g1 by NAT_1:29; then 1<=i & i<=len g1 & 1<=i+1 & i+1<=len g1 by A161,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A161,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A161,A162; then x in union {LSeg(g1,j): 1<=j & j+1<=len g1} by A160,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A23,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A163: i+1 > len g1; then A164: len g1<=i & i<=i+1 & i+1<=len g by A161,NAT_1:38; A165: 1<=i+1 & len g1<=i+1 & i<=len g by A161,A163,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A166: q1`1=ppi`1 & ppi`2<=q1`2 & q1`2<=pj`2 & q2`1=ppi`1 & ppi`2<= q2`2 & q2`2<=pj`2 by A141,A164,A165; then A167: q1=|[q1`1,q1`2]| & q2=|[q1`1,q2`2]| by EUCLID:57; A168: LSeg(g,i)=LSeg(q2,q1) by A161,TOPREAL1:def 5; now per cases by AXIOMS:21; suppose q1`2>q2`2; then LSeg(g,i)={p2: p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1`2} by A167,A168,TOPREAL3:15; then consider p2 such that A169: p2=x & p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1`2 by A160,A161; ppi`2<=p2`2 & p2`2<=pj`2 by A166,A169,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A139,A166,A169; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`2=q2`2; then LSeg(g,i)={q1} by A167,A168,TOPREAL1:7; then x=q1 by A160,A161,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A139,A166; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`2<q2`2; then LSeg(g,i)= {p1: p1`1=q1`1 & q1`2<=p1`2 & p1`2<=q2`2} by A167,A168,TOPREAL3:15; then consider p2 such that A170: p2=x & p2`1=q1`1 & q1`2<=p2`2 & p2`2<=q2`2 by A160,A161; ppi`2<=p2`2 & p2`2<=pj`2 by A166,A170,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A139,A166,A170; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; hence thesis; end; let x; assume x in L~f; then A171: x in L~f1 \/ LSeg(f,k) by A5,A11,Th8; now per cases by A171,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A23,Th11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A172: p1=x & p1`1=ppi`1 & ppi`2<=p1`2 & p1`2<=pj`2 by A139; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`2<=p1`2; A173: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A140,REAL_2:173; let q such that A174: q=g/.n; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A23,A174,GROUP_5:95 .=G*(i1,i2) by A14,A24,GOBOARD1:10; hence q`2<=p1`2 by A172; end; end; A175: for n holds P2[n] implies n<=len g; consider ma be Nat such that A176: P2[ma] & for n st P2[n] holds n<=ma from Max(A175,A173); now per cases; suppose A177: ma=len g; i2+1<=j2 by A124,NAT_1:38; then A178: 1<=l by REAL_1:84; then A179: l in dom g2 & i2+l=j2 by A125,FINSEQ_3:27,XCMPLX_1:27; then A180: g/.ma=g2/.l by A125,A140,A177,GROUP_5:96 .= pj by A125,A179; then pj`2<=p1`2 by A176; then A181: p1`2=pj`2 & p1=|[p1`1,p1`2]| by A172,AXIOMS:21,EUCLID: 57; A182: ma <= len g + 1 & len g1+1<=ma & ma <= len g by A125,A140,A177,A178,NAT_1:29,REAL_1:55; 1 <= len g1 + 1 by NAT_1:29; then A183: 0+1<=ma by A182,AXIOMS:22; then A184: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A183,INT_1:18; A185: ma in dom g by A177,A184,FINSEQ_1:def 3; A186: m1 + 1 = ma by XCMPLX_1:27; then A187: m1 >= len g1 by A182,REAL_1:53; 1<=len g1 by A13,A14,A23,AXIOMS:22; then A188: 1<=m1 by A187,AXIOMS:22; A189: m1 <= len g by A177,A186,NAT_1:29; then A190: m1 in dom g by A188,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A191: q`1=ppi`1 by A141,A187,A189; A192: q`2<=pj`2 by A141,A187,A189; A193: q=|[q`1,q`2]| by EUCLID:57; A194: LSeg(g,m1)=LSeg(pj,q) by A177,A180,A186,A188,TOPREAL1:def 5; set lq={e where e is Point of TOP-REAL 2: e`1=ppi`1 & q`2<=e`2 & e`2<=pj`2}; now assume q`2=pj`2; then 1=abs(i1-i1)+abs(j2-j2) by A26,A29,A44,A132,A134,A138,A180,A185,A186,A190,A191,A193, GOBOARD1:40 .=abs(0)+abs(j2-j2) by XCMPLX_1:14 .=abs(0)+abs(0) by XCMPLX_1:14 .=abs(0)+0 by ABSVALUE:7 .=0 by ABSVALUE:7; hence contradiction; end; then q`2<pj`2 by A192,REAL_1:def 5; then LSeg(g,m1)=lq by A138,A191,A193,A194,TOPREAL3:15; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A172,A177,A181,A186,A188,A192; then x in union lg by A172,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A176,REAL_1:def 5; then ma+1<=len g & k<=ma & ma<=ma+1 by A14,A23,A176,AXIOMS:22,NAT_1:38; then A195: 1<=ma & ma+1 <= len g & len g1<=ma+1 by A13,A176,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A196: qa`2<=p1`2 by A176; A197: now assume qa1`2<=p1`2; then for q holds q=g/.(ma+1) implies q`2<=p1`2; then ma+1<=ma by A176,A195; hence contradiction by REAL_2:174; end; then A198: qa`2<qa1`2 & qa`2<=p1`2 & p1`2<=qa1`2 & qa`1=ppi`1 & qa1 `1 = ppi`1 by A141,A176,A195,A196,AXIOMS:22; set lma = {p2: p2`1=ppi`1 & qa`2<=p2`2 & p2`2<=qa1`2}; A199: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa,qa1) by A195,TOPREAL1:def 5 .= lma by A198,A199,TOPREAL3:15; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A172,A195,A196,A197; then x in union lg by TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; end; hence x in L~g; end; hence x in L~g; end; 1<=len g1 by A13,A14,A23,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A23,GROUP_5:95 .=f/.1 by A14,GOBOARD1:10; i2+1<=j2 by A124,NAT_1:38; then A200: 1<=l by REAL_1:84; then A201: l in dom g2 & len g=len g1 + l by A125,A129,FINSEQ_1:3,35; hence g/.len g=g2/.l by GROUP_5:96 .=G*(i1,i2+l) by A125,A201 .=f/.len f by A5,A26,A44,XCMPLX_1:27; thus len f<=len g by A5,A14,A23,A200,A201,REAL_1:55; end; hence thesis; suppose A202: i2=j2; set ppi = G*(i1,i2), pj = G*(j1,i2); now per cases by AXIOMS:21; case A203: i1>j1; then reconsider l=i1-j1 as Nat by INT_1:18; A204: now let n; assume n in Seg l; then A205: 1<=n & n<=l & 0<=j1 by FINSEQ_1:3,NAT_1:18; then l<=i1 by PROB_1:2; then n<=i1 by A205,AXIOMS:22; then reconsider w=i1-n as Nat by INT_1:18; 0<=n & i1-l<=i1-n by A205,AXIOMS:22,REAL_1:92; then i1-n<=i1 & i1<=len G & j1<=w & 1<=j1 by A28,FINSEQ_3:27,PROB_1:2,XCMPLX_1:18; then 1<=w & w<=len G by AXIOMS:22; then w in dom G by FINSEQ_3:27; hence i1-n is Nat & [i1-n,i2] in Indices G & i1-n in dom G by A27,A28,ZFMISC_1:106; end; defpred P1[Nat,set] means for m st m=i1-$1 holds $2=G*(m,i2); A206: now let n; assume n in Seg l; then reconsider m=i1-n as Nat by A204; take p=G*(m,i2); thus P1[n,p]; end; consider g2 such that A207: len g2= l & for n st n in Seg l holds P1[n,g2/.n] from FinSeqDChoice(A206); A208: dom g2 = Seg l by A207,FINSEQ_1:def 3; take g=g1^g2; now let n; assume A209: n in dom g2; then reconsider m=i1-n as Nat by A204,A208; take m,k=i2; thus [m,k] in Indices G & g2/.n=G*(m,k) by A204,A207,A208,A209; end; then A210: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A29,GOBOARD1:39; A211: now let n; assume A212: n in dom g2 & n+1 in dom g2; then A213: i1-n is Nat & [i1-n,i2] in Indices G & P1[n,g2/.n] & i1-(n+1) is Nat & [i1-(n+1),i2] in Indices G & P1[n+1,g2/.(n+1)] by A204,A207,A208; reconsider m1=i1-n ,m2=i1-(n+1) as Nat by A204,A208,A212; A214: g2/.n=G*(m1,i2) & g2/.(n+1)=G*(m2,i2) by A207,A208,A212; let l1,l2,l3,l4 be Nat; assume [l1,l2] in Indices G & [l3,l4] in Indices G & g2/.n=G*(l1,l2) & g2/.(n+1)=G*(l3,l4); then l1=m1 & l2=i2 & l3=m2 & l4=i2 & 0<=1 by A213,A214,GOBOARD1:21; hence abs(l1-l3)+abs(l2-l4)=abs(i1-n-(i1-(n+1)))+abs(0) by XCMPLX_1: 14 .= abs(i1-n-(i1-(n+1)))+0 by ABSVALUE:7 .= abs(i1-n-(i1-n-1)) by XCMPLX_1:36 .= abs(1) by XCMPLX_1:18 .= 1 by ABSVALUE:def 1; end; A215: now let l1,l2,l3,l4 be Nat; assume A216: [l1,l2] in Indices G & [l3,l4] in Indices G & g1/.len g1=G*(l1, l2) & g2/.1=G*(l3,l4) & len g1 in dom g1 & 1 in dom g2; then A217: i1-1 is Nat & [i1-1,i2] in Indices G & P1[1,g2/.1] & f1/.len f1=f/.k by A14,A204,A207,A208,GOBOARD1:10; reconsider m1=i1-1 as Nat by A204,A208,A216; g2/.1=G*(m1,i2) by A207,A208,A216; then l1=i1 & l2=i2 & l3=m1 & l4=i2 & 0<=1 by A23,A24,A216,A217, GOBOARD1:21; hence abs(l1-l3)+abs(l2-l4)=abs(i1-(i1-1))+abs(0) by XCMPLX_1:14 .=abs(i1-(i1-1))+0 by ABSVALUE:7 .=abs(1) by XCMPLX_1:18 .=1 by ABSVALUE:def 1; end; then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by A29,A211,GOBOARD1:40; hence g is_sequence_on G by A210,GOBOARD1:def 11; set lk={w where w is Point of TOP-REAL 2: w`2=ppi`2 & pj`1<=w`1 & w`1<= ppi`1}; c1/.i1 = c1.i1 & c1/.j1 = c1.j1 by A28,A42,FINSEQ_4:def 4; then A218: c1/.i1=ppi & c1/.j1=pj by A28,MATRIX_1:def 9; then A219: y2.i1=ppi`2 & y2.j1=pj`2 & x2.i1=ppi`1 & x2.j1=pj`1 by A28,A42,A43,GOBOARD1:def 3,def 4; then A220: pj`1<ppi`1 & ppi`2=pj`2 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj`2]| by A28,A33,A34,A42,A43,A203,EUCLID:57,GOBOARD1:def 1,def 2; A221: LSeg(f,k)=LSeg(pj,ppi) by A13,A24,A26,A202,TOPREAL1:def 5 .= lk by A220,TOPREAL3:16; 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}; A222: len g = len g1 + len g2 by FINSEQ_1:35; A223: now let j; assume A224: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A225: p=g/.j; now per cases; suppose A226: j=len g1; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A227: g/.len g1 = f1/.len f1 by A23,GROUP_5:95 .= G*(i1,i2) by A14,A24,GOBOARD1:10; hence p`2=G*(i1,i2)`2 by A225,A226; thus G*(j1,i2)`1<=p`1 & p`1<=G*(i1,i2)`1 by A28,A33,A42,A43,A203,A219,A225,A226,A227,GOBOARD1:def 1; thus p in rng c1 by A28,A42,A218,A225,A226,A227,PARTFUN2:4; suppose A228: j<>len g1; then A229: len g1 < j by A224,REAL_1:def 5; j - len g1 <> 0 by A228,XCMPLX_1:15; then A230: w >= 1 by RLVECT_1:99; A231: w + len g1 = j by XCMPLX_1:27; then A232: w <= len g2 by A222,A224,REAL_1:53; then A233: len g1 + 1<=j & g/.j=g2/.w by A229,A230,A231,Th5,NAT_1 :38; A234: w in dom g2 by A230,A232,FINSEQ_3:27; then A235: i1-w is Nat & i1-w in dom G & P1[w,g2/.w] by A204,A207,A208; reconsider u=i1-w as Nat by A204,A208,A234; g2/.w = g2.w & c1/.u =c1.u by A42,A234,A235,FINSEQ_4:def 4; then A236: g2/.w=G*(u,i2) & c1/.u=G*(u,i2) by A235,MATRIX_1:def 9 ; then A237: x2.i1=G*(i1,i2)`1 & x2.u=G*(u,i2)`1 & x2.j1=G*(j1,i2) `1 & y2.i1=G*(i1,i2)`2 & y2.u=G*(u,i2)`2 & y2.j1=G*(j1,i2)`2 by A28,A42,A43,A218,A235,GOBOARD1:def 3,def 4; hence p`2=G*(i1,i2)`2 by A28,A34,A42,A43,A225,A233,A235,A236,GOBOARD1:def 2; now per cases; suppose u=j1; hence G*(j1,i2)`1<=p`1 by A225,A230,A231,A232,A236,Th5; suppose A238: u<>j1; i1-len g2<=u & len g2=l by A207,A232,REAL_1:92; then j1<=u by XCMPLX_1:18; then j1<u by A238,REAL_1:def 5; hence G*(j1,i2)`1<=p`1 by A28,A33,A42,A43,A225,A233,A235,A236, A237,GOBOARD1:def 1; end; hence G*(j1,i2)`1<=p`1; u<=i1-1 & i1-1<i1 by A230,REAL_1:92,SQUARE_1:29; then u<i1 by AXIOMS:22; hence p`1<=G*(i1,i2)`1 by A28,A33,A42,A43,A225,A233,A235,A236, A237,GOBOARD1:def 1; thus p in rng c1 by A42,A225,A233,A235,A236,PARTFUN2:4; 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; assume x in L~g; then x in union lg by TOPREAL1:def 6; then consider X be set such that A239: x in X & X in lg by TARSKI:def 4; consider i such that A240: X=LSeg(g,i) & 1<=i & i+1 <= len g by A239; now per cases; suppose A241: i+1 <= len g1; then i<=i+1 & i+1<=len g1 by NAT_1:29; then 1<=i & i<=len g1 & 1<=i+1 & i+1<=len g1 by A240,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A240,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A240,A241; then x in union {LSeg(g1,j): 1<=j & j+1<=len g1} by A239,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A23,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A242: i+1 > len g1; then A243: len g1<=i & i<=i+1 & i+1<=len g by A240,NAT_1:38; A244: 1<=i+1 & len g1<=i+1 & i<=len g by A240,A242,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A245: q1`2=ppi`2 & pj`1<=q1`1 & q1`1<=ppi`1 & q2`2=ppi`2 & pj`1<= q2`1 & q2`1<=ppi`1 by A223,A243,A244; then A246: q1=|[q1`1,q1`2]| & q2=|[q2`1,q1`2]| by EUCLID:57; A247: LSeg(g,i)=LSeg(q2,q1) by A240,TOPREAL1:def 5; now per cases by AXIOMS:21; suppose q1`1>q2`1; then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1<=q1`1} by A246,A247,TOPREAL3:16; then consider p2 such that A248: p2=x & p2`2=q1`2 & q2`1<=p2`1 & p2`1<=q1`1 by A239,A240; pj`1<=p2`1 & p2`1<=ppi`1 by A245,A248,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A221,A245,A248; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`1=q2`1; then LSeg(g,i)={q1} by A246,A247,TOPREAL1:7; then x=q1 by A239,A240,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A221,A245; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`1<q2`1; then LSeg(g,i)= {p1: p1`2=q1`2 & q1`1<=p1`1 & p1`1<=q2`1} by A246,A247,TOPREAL3:16; then consider p2 such that A249: p2=x & p2`2=q1`2 & q1`1<=p2`1 & p2`1<=q2`1 by A239,A240; pj`1<=p2`1 & p2`1<=ppi`1 by A245,A249,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A221,A245,A249; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; hence thesis; end; let x; assume x in L~f; then A250: x in L~f1 \/ LSeg(f,k) by A5,A11,Th8; now per cases by A250,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A23,Th11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A251: p1=x & p1`2=ppi`2 & pj`1<=p1`1 & p1`1<=ppi`1 by A221; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`1>=p1`1; A252: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A222,REAL_2:173; let q such that A253: q=g/.n; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A23,A253,GROUP_5:95 .=G*(i1,i2) by A14,A24,GOBOARD1:10; hence p1`1<=q`1 by A251; end; end; A254: for n holds P2[n] implies n<=len g; consider ma be Nat such that A255: P2[ma] & for n st P2[n] holds n<=ma from Max(A254,A252); now per cases; suppose A256: ma=len g; j1+1<=i1 by A203,NAT_1:38; then A257: 1<=l & l=len g2 by A207,REAL_1:84; then A258: l in dom g2 & i1-l=j1 by A208,FINSEQ_1:3,XCMPLX_1:18; then A259: g/.ma=g2/.l by A207,A222,A256,GROUP_5:96 .= pj by A207,A208,A258; then p1`1<=pj`1 by A255; then A260: p1`1=pj`1 & p1=|[p1`1,p1`2]| by A251,AXIOMS:21,EUCLID: 57; A261: ma <= len g + 1 & len g1+1<=ma & ma <= len g by A222,A256,A257,NAT_1:29,REAL_1:55; 1 <= len g1 + 1 by NAT_1:29; then A262: 0+1<=ma by A261,AXIOMS:22; then A263: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A262,INT_1:18; A264: ma in dom g by A256,A263,FINSEQ_1:def 3; A265: m1 + 1 = ma by XCMPLX_1:27; then A266: m1 >= len g1 by A261,REAL_1:53; 1<=len g1 by A13,A14,A23,AXIOMS:22; then A267: 1<=m1 by A266,AXIOMS:22; A268: m1 <= len g by A256,A265,NAT_1:29; then A269: m1 in dom g by A267,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A270: q`2=ppi`2 by A223,A266,A268; A271: pj`1<=q`1 by A223,A266,A268; A272: q=|[q`1,q`2]| by EUCLID:57; A273: LSeg(g,m1)=LSeg(pj,q) by A256,A259,A265,A267,TOPREAL1:def 5 ; set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2 & pj`1<=e`1 & e`1<=q`1}; now assume q`1=pj`1; then 1=abs(j1-j1)+abs(i2-i2) by A26,A29,A202,A211,A215,A220,A259,A264,A265,A269,A270,A272, GOBOARD1:40 .=abs(0)+abs(i2-i2) by XCMPLX_1:14 .=abs(0)+abs(0) by XCMPLX_1:14 .=abs(0)+0 by ABSVALUE:7 .=0 by ABSVALUE:7; hence contradiction; end; then pj`1<q`1 by A271,REAL_1:def 5; then LSeg(g,m1)=lq by A220,A270,A272,A273,TOPREAL3:16; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A251,A256,A260,A265,A267,A271; then x in union lg by A251,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A255,REAL_1:def 5; then ma+1<=len g & k<=ma & ma<=ma+1 by A14,A23,A255,AXIOMS:22,NAT_1:38; then A274: 1<=ma & ma+1 <= len g & len g1<=ma+1 by A13,A255,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A275: p1`1<=qa`1 by A255; A276: now assume p1`1<=qa1`1; then for q holds q=g/.(ma+1) implies p1`1<=q`1; then ma+1<=ma by A255,A274; hence contradiction by REAL_2:174; end; then A277: qa1`1<qa`1 & qa1`1<=p1`1 & p1`1<=qa`1 & qa`2=ppi`2 & qa1 `2 = ppi`2 by A223,A255,A274,A275,AXIOMS:22; set lma = {p2: p2`2=ppi`2 & qa1`1<=p2`1 & p2`1<=qa`1}; A278: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa1,qa) by A274,TOPREAL1:def 5 .= lma by A277,A278,TOPREAL3:16; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A251,A274,A275,A276; then x in union lg by TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; end; hence x in L~g; end; hence x in L~g; end; 1<=len g1 by A13,A14,A23,AXIOMS:22; then 1 in dom g1 by A30,FINSEQ_1:3; hence g/.1=f1/.1 by A23,GROUP_5:95 .=f/.1 by A14,GOBOARD1:10; j1+1<=i1 by A203,NAT_1:38; then A279: 1<=l by REAL_1:84; then A280: l in dom g2 & len g=len g1 + len g2 & len g2 = l by A208,FINSEQ_1:3,35,def 3; then reconsider m1=i1-l as Nat by A204,A208; thus g/.len g=g2/.l by A280,GROUP_5:96 .=G*(m1,i2) by A207,A208,A280 .=f/.len f by A5,A26,A202,XCMPLX_1:18; thus len f<=len g by A5,A14,A23,A279,A280,REAL_1:55; case i1=j1; hence contradiction by A8,A14,A24,A25,A26,A202; case A281: i1<j1; then reconsider l=j1-i1 as Nat by INT_1:18; deffunc F(Nat) = G*(i1+$1,i2); consider g2 such that A282: len g2 = l & for n st n in dom g2 holds g2/.n = F(n) from PiLambdaD; A283: dom g2 = Seg l by A282,FINSEQ_1:def 3; take g=g1^g2; A284: now let n; assume n in Seg l; then A285: 1<=n & n<=l by FINSEQ_1:3; then n<=n+i1 & i1+n<=l+i1 by NAT_1:29,REAL_1:55; then n<=i1+n & i1+n<=j1 & j1<=len G by A28,FINSEQ_3:27,XCMPLX_1:27; then 1<=i1+n & i1+n<=len G by A285,AXIOMS:22; hence i1+n in dom G by FINSEQ_3:27; hence [i1+n,i2] in Indices G by A27,A28,ZFMISC_1:106; end; A286: dom g2 = Seg len g2 by FINSEQ_1:def 3; now let n such that A287: n in dom g2; take m=i1+n,k=i2; thus [m,k] in Indices G & g2/.n=G*(m,k) by A282,A284,A286,A287; end; then A288: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A29,GOBOARD1:39; A289: now let n; assume n in dom g2 & n+1 in dom g2; then A290: g2/.n=G*(i1+n,i2) & [i1+n,i2] in Indices G & g2/.(n+1)=G*(i1+(n+1),i2) & [i1+(n+1),i2] in Indices G by A282,A284,A286; let l1,l2,l3,l4 be Nat; assume [l1,l2] in Indices G & [l3,l4] in Indices G & g2/.n=G*(l1,l2) & g2/.(n+1)=G*(l3,l4); then l1=i1+n & l2=i2 & l3=i1+(n+1) & l4=i2 & 0<=1 by A290,GOBOARD1: 21; hence abs(l1-l3)+abs(l2-l4)=abs(i1+n-(i1+(n+1)))+abs(0) by XCMPLX_1: 14 .= abs(i1+n-(i1+(n+1)))+0 by ABSVALUE:7 .= abs(i1+n-(i1+n+1)) by XCMPLX_1:1 .= abs(i1+n-(i1+n)-1) by XCMPLX_1:36 .= abs(i1+n-(i1+n)+-1) by XCMPLX_0:def 8 .= abs(-1) by XCMPLX_1:25 .= abs(1) by ABSVALUE:17 .= 1 by ABSVALUE:def 1; end; A291: now let l1,l2,l3,l4 be Nat; assume A292: [l1,l2] in Indices G & [l3,l4] in Indices G & g1/.len g1=G*(l1,l2) & g2/.1=G*(l3,l4) & len g1 in dom g1 & 1 in dom g2; then g2/.1=G*(i1+1,i2) & [i1+1,i2] in Indices G & f1/.len f1=f/.k by A14,A282,A284,A286,GOBOARD1:10; then l1=i1 & l2=i2 & l3=i1+1 & l4=i2 & 0<=1 by A23,A24,A292,GOBOARD1 :21; hence abs(l1-l3)+abs(l2-l4)=abs(i1-(i1+1))+abs(0) by XCMPLX_1:14 .=abs(i1-(i1+1))+0 by ABSVALUE:7 .=abs(i1-i1-1) by XCMPLX_1:36 .=abs(i1-i1+-1) by XCMPLX_0:def 8 .=abs(-1) by XCMPLX_1:25 .=abs(1) by ABSVALUE:17 .=1 by ABSVALUE:def 1; end; then for n st n in dom g & n+1 in dom g holds for m,k,i,j st [m,k] in Indices G & [i,j] in Indices G & g/.n=G*(m,k) & g/.(n+1)=G*(i,j) holds abs(m-i)+abs(k-j)=1 by A29,A289,GOBOARD1:40; hence g is_sequence_on G by A288,GOBOARD1:def 11; set lk={w where w is Point of TOP-REAL 2: w`2=ppi`2 & ppi`1<=w`1 & w`1<= pj`1}; c1/.i1 = c1.i1 & c1/.j1 = c1.j1 by A28,A42,FINSEQ_4:def 4; then A293: c1/.i1=ppi & c1/.j1=pj by A28,MATRIX_1:def 9; then A294: y2.i1=ppi`2 & y2.j1=pj`2 & x2.i1=ppi`1 & x2.j1=pj`1 by A28,A42,A43,GOBOARD1:def 3,def 4; then A295: ppi`1<pj`1 & ppi`2=pj`2 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj`2]| by A28,A33,A34,A42,A43,A281,EUCLID:57,GOBOARD1:def 1,def 2; A296: LSeg(f,k)=LSeg(ppi,pj) by A13,A24,A26,A202,TOPREAL1:def 5 .= lk by A295,TOPREAL3:16; 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}; A297: len g = len g1 + len g2 by FINSEQ_1:35; A298: now let j; assume A299: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A300: p=g/.j; set u=i1+w; now per cases; suppose A301: j=len g1; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A302: g/.len g1 = f1/.len f1 by A23,GROUP_5:95 .= G*(i1,i2) by A14,A24,GOBOARD1:10; hence p`2=G*(i1,i2)`2 by A300,A301; thus G*(i1,i2)`1<=p`1 & p`1<=G* (j1,i2)`1 by A28,A33,A42,A43,A281,A294,A300,A301,A302,GOBOARD1:def 1; thus p in rng c1 by A28,A42,A293,A300,A301,A302,PARTFUN2:4; suppose A303: j<>len g1; then A304: len g1 < j by A299,REAL_1:def 5; A305: j - len g1 <> 0 by A303,XCMPLX_1:15; then A306: w >= 1 by RLVECT_1:99; A307: w + len g1 = j by XCMPLX_1:27; then A308: w <= len g2 by A297,A299,REAL_1:53; then A309: len g1 + 1<=j & g/.j=g2/.w by A304,A306,A307,Th5,NAT_1 :38; w in dom g2 by A306,A308,FINSEQ_3:27; then A310: g2/.w=G*(u,i2) & u in dom G by A282,A283,A284; then c1/.u = c1.u by A42,FINSEQ_4:def 4; then A311: c1/.u=G*(u,i2) by A310,MATRIX_1:def 9; then A312: x2.i1=G*(i1,i2)`1 & x2.u=G*(u,i2)`1 & x2.j1=G* (j1,i2)`1 & y2.i1=G*(i1,i2)`2 & y2.u=G*(u,i2)`2 & y2.j1=G*(j1,i2)`2 by A28,A42,A43,A293,A310,GOBOARD1:def 3,def 4; hence p`2=G*(i1,i2)`2 by A28,A34,A42,A43,A300,A309,A310,GOBOARD1:def 2; 0+1<=w by A305,RLVECT_1:99; then 0<w by NAT_1:38; then i1<u by REAL_2:174; hence G*(i1,i2)`1<=p`1 by A28,A33,A42,A43,A300,A309,A310,A312, GOBOARD1:def 1; now per cases; suppose u=j1; hence p`1<=G*(j1,i2)`1 by A300,A306,A307,A308,A310,Th5; suppose A313: u<>j1; u<=i1+l by A282,A308,REAL_1:55; then u<=j1 by XCMPLX_1:27; then u<j1 by A313,REAL_1:def 5; hence p`1<=G*(j1,i2)`1 by A28,A33,A42,A43,A300,A309,A310,A312, GOBOARD1:def 1; end; hence p`1<=G*(j1,i2)`1; thus p in rng c1 by A42,A300,A309,A310,A311,PARTFUN2:4; 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; assume x in L~g; then x in union lg by TOPREAL1:def 6; then consider X be set such that A314: x in X & X in lg by TARSKI:def 4; consider i such that A315: X=LSeg(g,i) & 1<=i & i+1 <= len g by A314; now per cases; suppose A316: i+1 <= len g1; then i<=i+1 & i+1<=len g1 by NAT_1:29; then 1<=i & i<=len g1 & 1<=i+1 & i+1<=len g1 by A315,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A315,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1<=len g1} by A315,A316; then x in union {LSeg(g1,j): 1<=j & j+1<=len g1} by A314,TARSKI: def 4; then x in L~f1 & L~f1 c= L~f by A23,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A317: i+1 > len g1; then A318: len g1<=i & i<=i+1 & i+1<=len g by A315,NAT_1:38; A319: 1<=i+1 & len g1<=i+1 & i<=len g by A315,A317,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A320: q1`2=ppi`2 & ppi`1<=q1`1 & q1`1<=pj`1 & q2`2=ppi`2 & ppi`1<= q2`1 & q2`1<=pj`1 by A298,A318,A319; then A321: q1=|[q1`1,q1`2]| & q2=|[q2`1,q1`2]| by EUCLID:57; A322: LSeg(g,i)=LSeg(q2,q1) by A315,TOPREAL1:def 5; now per cases by AXIOMS:21; suppose q1`1>q2`1; then LSeg(g,i)={p2: p2`2=q1`2 & q2`1<=p2`1 & p2`1<=q1`1} by A321,A322,TOPREAL3:16; then consider p2 such that A323: p2=x & p2`2=q1`2 & q2`1<=p2`1 & p2`1<=q1`1 by A314,A315; ppi`1<=p2`1 & p2`1<=pj`1 by A320,A323,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A296,A320,A323; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`1=q2`1; then LSeg(g,i)={q1} by A321,A322,TOPREAL1:7; then x=q1 by A314,A315,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A296,A320; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; suppose q1`1<q2`1; then LSeg(g,i)= {p1: p1`2=q1`2 & q1`1<=p1`1 & p1`1<=q2`1} by A321,A322,TOPREAL3:16; then consider p2 such that A324: p2=x & p2`2=q1`2 & q1`1<=p2`1 & p2`1<=q2`1 by A314,A315; ppi`1<=p2`1 & p2`1<=pj`1 by A320,A324,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A13,A296,A320,A324; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; hence thesis; end; let x; assume x in L~f; then A325: x in L~f1 \/ LSeg(f,k) by A5,A11,Th8; now per cases by A325,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A23,Th11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A326: p1=x & p1`2=ppi`2 & ppi`1<=p1`1 & p1`1<=pj`1 by A296; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`1<=p1`1; A327: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A297,REAL_2:173; let q such that A328: q=g/.n; 1<=len g1 by A13,A14,A23,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A23,A328,GROUP_5:95 .=G*(i1,i2) by A14,A24,GOBOARD1:10; hence q`1<=p1`1 by A326; end; end; A329: for n holds P2[n] implies n<=len g; consider ma be Nat such that A330: P2[ma] & for n st P2[n] holds n<=ma from Max(A329,A327); now per cases; suppose A331: ma=len g; i1+1<=j1 by A281,NAT_1:38; then A332: 1<=l by REAL_1:84; then A333: l in dom g2 & i1+l=j1 by A282,FINSEQ_3:27,XCMPLX_1:27; then A334: g/.ma=g2/.l by A282,A297,A331,GROUP_5:96 .= pj by A282,A333; then pj`1<=p1`1 by A330; then A335: p1`1=pj`1 & p1=|[p1`1,p1`2]| by A326,AXIOMS:21,EUCLID: 57; A336: ma <= len g + 1 & len g1+1<=ma & ma <= len g by A282,A297,A331,A332,NAT_1:29,REAL_1:55; 1 <= len g1 + 1 by NAT_1:29; then A337: 0+1<=ma by A336,AXIOMS:22; then A338: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A337,INT_1:18; A339: ma in dom g by A331,A338,FINSEQ_1:def 3; A340: m1 + 1 = ma by XCMPLX_1:27; then A341: m1 >= len g1 by A336,REAL_1:53; 1<=len g1 by A13,A14,A23,AXIOMS:22; then A342: 1<=m1 by A341,AXIOMS:22; A343: m1 <= len g by A331,A340,NAT_1:29; then A344: m1 in dom g by A342,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A345: q`2=ppi`2 by A298,A341,A343; A346: q`1<=pj`1 by A298,A341,A343; A347: q=|[q`1,q`2]| by EUCLID:57; A348: LSeg(g,m1)=LSeg(pj,q) by A331,A334,A340,A342,TOPREAL1:def 5; set lq={e where e is Point of TOP-REAL 2: e`2=ppi`2 & q`1<=e`1 & e`1<=pj`1}; now assume q`1=pj`1; then 1=abs(j1-j1)+abs(i2-i2) by A26,A29,A202,A289,A291,A295,A334,A339,A340,A344,A345,A347, GOBOARD1:40 .=abs(0)+abs(i2-i2) by XCMPLX_1:14 .=abs(0)+abs(0) by XCMPLX_1:14 .=abs(0)+0 by ABSVALUE:7 .=0 by ABSVALUE:7; hence contradiction; end; then q`1<pj`1 by A346,REAL_1:def 5; then LSeg(g,m1)=lq by A295,A345,A347,A348,TOPREAL3:16; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A326,A331,A335,A340,A342,A346; then x in union lg by A326,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A330,REAL_1:def 5; then ma+1<=len g & k<=ma & ma<=ma+1 by A14,A23,A330,AXIOMS:22,NAT_1:38; then A349: 1<=ma & ma+1 <= len g & len g1<=ma+1 by A13,A330,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A350: qa`1<=p1`1 by A330; A351: now assume qa1`1<=p1`1; then for q holds q=g/.(ma+1) implies q`1<=p1`1; then ma+1<=ma by A330,A349; hence contradiction by REAL_2:174; end; then A352: qa`1<qa1`1 & qa`1<=p1`1 & p1`1<=qa1`1 & qa`2=ppi`2 & qa1 `2 = ppi`2 by A298,A330,A349,A350,AXIOMS:22; set lma = {p2: p2`2=ppi`2 & qa`1<=p2`1 & p2`1<=qa1`1}; A353: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa,qa1) by A349,TOPREAL1:def 5 .= lma by A352,A353,TOPREAL3:16; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A326,A349,A350,A351; then x in union lg by TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; end; hence x in L~g; end; hence x in L~g; end; 1<=len g1 by A13,A14,A23,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A23,GROUP_5:95 .=f/.1 by A14,GOBOARD1:10; i1+1<=j1 by A281,NAT_1:38; then A354: 1<=l by REAL_1:84; then A355: l in dom g2 & len g=len g1 + l by A282,A286,FINSEQ_1:3,35; hence g/.len g=g2/.l by GROUP_5:96 .=G*(i1+l,i2) by A282,A355 .=f/.len f by A5,A26,A202,XCMPLX_1:27; thus len f<=len g by A5,A14,A23,A354,A355,REAL_1:55; end; hence thesis; end; hence thesis; end; hence thesis; end; for n holds P[n] from Ind(A1,A3); hence thesis; end; theorem v is increasing implies for n,m st n in dom v & m in dom v & n<=m holds v.n <= v.m proof assume A1: v is increasing; let n,m such that A2: n in dom v & m in dom v & n<=m; set r=v.n, s=v.m; now per cases; suppose n=m; hence r<=s; suppose n<>m; then n<m by A2,REAL_1:def 5; hence r<=s by A1,A2,GOBOARD1:def 1; end; hence thesis; end; theorem Th19: v is increasing implies for n,m st n in dom v & m in dom v & n<>m holds v.n<>v.m proof assume A1: v is increasing; let n,m; assume A2: n in dom v & m in dom v & n<>m; now per cases by A2,REAL_1:def 5; suppose n<m; hence v.n<>v.m by A1,A2,GOBOARD1:def 1; suppose n>m; hence v.n<>v.m by A1,A2,GOBOARD1:def 1; end; hence thesis; end; theorem Th20: v is increasing & v1 = v|Seg n implies v1 is increasing proof assume A1: v is increasing & v1 = v|Seg n; now per cases; suppose n<=len v; then Seg n c= Seg len v by FINSEQ_1:7; then A2: Seg n c= dom v by FINSEQ_1:def 3; then Seg n = dom v /\ Seg n by XBOOLE_1:28; then A3: dom v1 = Seg n by A1,FUNCT_1:68; now let m,k such that A4: m in dom v1 & k in dom v1 & m<k; set r=v1.m, s=v1.k; r=v.m & s=v.k & m in dom v & k in dom v by A1,A2,A3,A4,FUNCT_1:68; hence r<s by A1,A4,GOBOARD1:def 1; end; hence v1 is increasing by GOBOARD1:def 1; suppose len v<=n; hence v1 is increasing by A1,FINSEQ_2:23; end; hence thesis; end; defpred P1[Nat] means for v st card rng v = $1 holds ex v1 st rng v1 = rng v & len v1 = card rng v & v1 is increasing; Lm4: P1[0] proof let v; assume card rng v = 0; then A1: rng v = {} by CARD_2:59; then A2: v = {} by FINSEQ_1:27; take v1 = v; thus rng v1 = rng v; thus len v1 = card rng v by A1,FINSEQ_1:27; for n,m holds n in dom v1 & m in dom v1 & n<m implies v1.n < v1.m by A2,FINSEQ_1:26; hence v1 is increasing by GOBOARD1:def 1; end; Lm5: for n st P1[n] holds P1[n+1] proof let n such that A1: P1[n]; let v such that A2: card rng v = n+1; now reconsider R = rng v as finite Subset of REAL by FINSEQ_1:def 4; A3: R is bounded_above & upper_bound(R) in R by A2,Th1,CARD_1:78; set u = upper_bound(R), X = R \ {u}; reconsider f = X|v as FinSubsequence by FINSEQ_1:69; A4: X c= R by XBOOLE_1:36; X c= REAL & Seq f=f*Sgm(dom f) & rng Sgm(dom f)=dom f by FINSEQ_1:71,def 14; then A5: rng Seq f = rng f by RELAT_1:47 .= X by A4,RELAT_1:120; then reconsider f1 = Seq f as FinSequence of REAL by FINSEQ_1:def 4; reconsider X as finite set; A6: {u} c= R by A3,ZFMISC_1:37; then card X = card R - card {u} & card {u}=1 by CARD_1:79,CARD_2:63; then A7: card X = n by A2,XCMPLX_1:26; then consider v2 such that A8: rng v2 = rng f1 & len v2 = card rng f1 & v2 is increasing by A1,A5; take v1 = v2 ^ <* u *>; thus rng v1 = X \/ rng <*u*> by A5,A8,FINSEQ_1:44 .= (rng v \ {u}) \/ {u} by FINSEQ_1:56 .= rng v \/ {u} by XBOOLE_1:39 .= rng v by A6,XBOOLE_1:12; thus A9: len v1 = n+ len <*u*> by A5,A7,A8,FINSEQ_1:35 .= card rng v by A2,FINSEQ_1:56; now let k,m; assume A10: k in dom v1 & m in dom v1 & k<m; then A11: 1<=k & k<=len v1 & 1<=m & m<=len v1 by FINSEQ_3:27; set r=v1.k, s=v1.m; now per cases; suppose m=len v1; then A12: s=u by A2,A5,A7,A8,A9,FINSEQ_1:59; k<len v1 by A10,A11,AXIOMS:22; then k<=len v2 by A2,A5,A7,A8,A9,NAT_1:38; then A13: k in dom v2 by A11,FINSEQ_3:27; then r=v2.k by FINSEQ_1:def 7; then r in rng v2 by A13,FUNCT_1:def 5; then r in R & not r in {u} by A5,A8,XBOOLE_0:def 4; then r<=u & r<>u by A3,SEQ_4:def 4,TARSKI:def 1; hence r<s by A12,REAL_1:def 5; suppose m <>len v1; then m<len v1 & k<len v1 by A10,A11,REAL_1:def 5; then k<=len v2 & m<=len v2 by A2,A5,A7,A8,A9,NAT_1:38; then A14: k in dom v2 & m in dom v2 by A11,FINSEQ_3:27; then r=v2.k & s=v2.m by FINSEQ_1:def 7; hence r<s by A8,A10,A14,GOBOARD1:def 1; end; hence r<s; end; hence v1 is increasing by GOBOARD1:def 1; end; hence thesis; end; Lm6: for n holds P1[n] from Ind(Lm4,Lm5); theorem for v holds ex v1 st rng v1 = rng v & len v1 = card rng v & v1 is increasing by Lm6; defpred P3[Nat] means for v1,v2 st len v1=$1 & len v2=$1 & rng v1=rng v2 & v1 is increasing & v2 is increasing holds v1=v2; Lm7: P3[0] proof let v1,v2; assume len v1=0 & len v2=0 & rng v1=rng v2 & v1 is increasing & v2 is increasing; then v1={} & v2={} by FINSEQ_1:25; hence v1=v2; end; Lm8: for n st P3[n] holds P3[n+1] proof let n such that A1: P3[n]; let v1,v2 such that A2: len v1=n+1 & len v2=n+1 & rng v1=rng v2 & v1 is increasing & v2 is increasing; A3: dom v1 = Seg len v1 & dom v2=Seg len v2 & rng v1 c= REAL by FINSEQ_1:def 3,def 4; reconsider X = rng v1 as Subset of REAL by FINSEQ_1:def 4; now assume X={}; then v1={} by FINSEQ_1:27; hence contradiction by A2,FINSEQ_1:25; end; then A4: X is bounded_above & upper_bound(X) in X by Th1; set u = upper_bound(X); consider k such that A5: k in dom v1 & v1.k=u by A4,FINSEQ_2:11; A6: 1<=k & k<=len v1 by A5,FINSEQ_3:27; A7: now assume k<>len v1; then k<len v1 & k<=k+1 by A6,NAT_1:29,REAL_1:def 5; then 1<=k+1 & k+1<=len v1 by A6,NAT_1:38; then A8: k+1 in dom v1 by FINSEQ_3:27; then A9: v1.(k+1) in rng v1 by FUNCT_1:def 5; reconsider s=v1.(k+1) as Real; A10: s<=u by A4,A9,SEQ_4:def 4; k<k+1 by NAT_1:38; hence contradiction by A2,A5,A8,A10,GOBOARD1:def 1; end; consider m such that A11: m in dom v2 & v2.m=u by A2,A4,FINSEQ_2:11; A12: 1<=m & m<=len v2 by A11,FINSEQ_3:27; A13: now assume m<>len v2; then m<len v2 & m<=m+1 by A12,NAT_1:29,REAL_1:def 5; then 1<=m+1 & m+1<=len v2 by A12,NAT_1:38; then A14: m+1 in dom v2 by FINSEQ_3:27; then A15: v2.(m+1) in rng v2 by FUNCT_1:def 5; reconsider s=v2.(m+1) as Real; A16: s<=u by A2,A4,A15,SEQ_4:def 4; m<m+1 by NAT_1:38; hence contradiction by A2,A11,A14,A16,GOBOARD1:def 1; end; A17: n<=n+1 by NAT_1:29; then Seg n c= Seg(n+1) by FINSEQ_1:7; then Seg n = Seg(n+1) /\ Seg n by XBOOLE_1:28; then A18: dom (v1|Seg n) = Seg n & dom (v2|Seg n) =Seg n by A2,A3,FUNCT_1:68; then reconsider f1 = v1|Seg n, f2 = v2|Seg n as FinSequence by FINSEQ_1:def 2 ; rng f1 c= rng v1 & rng f2 c= rng v2 by FUNCT_1:76; then rng f1 c= REAL & rng f2 c= REAL by A2,A3,XBOOLE_1:1; then reconsider f1, f2 as FinSequence of REAL by FINSEQ_1:def 4; A19: len f1 = n & len f2 = n by A18,FINSEQ_1:def 3; then A20: dom f1 c= dom v1 by A2,A17,FINSEQ_3:32; A21: rng f1 = rng v1 \ {u} proof thus rng f1 c= rng v1 \ {u} proof let x; assume x in rng f1; then consider i such that A22: i in dom f1 & f1.i=x by FINSEQ_2:11; A23: 1<=i & i<=n & x=v1.i by A18,A22,FINSEQ_1:3,FUNCT_1:68; then i<>n+1 & i in dom v1 & n+1 in Seg len v1 by A2,A20,A22,FINSEQ_1:6,NAT_1:38; then x<>u by A2,A5,A7,A23,Th19; then not x in {u} & v1.i in rng v1 by A20,A22,FUNCT_1:def 5,TARSKI:def 1 ; hence x in rng v1 \ {u} by A23,XBOOLE_0:def 4; end; let x; assume x in rng v1 \ {u}; then A24: x in rng v1 & not x in {u} by XBOOLE_0:def 4; then consider i such that A25: i in dom v1 & v1.i=x by FINSEQ_2:11; A26: i <> len v1 by A5,A7,A24,A25,TARSKI:def 1; A27: 1<=i & i<=len v1 by A25,FINSEQ_3:27; then i<len v1 by A26,REAL_1:def 5; then i<=len f1 by A2,A19,NAT_1:38; then i in dom f1 by A27,FINSEQ_3:27; then f1.i in rng f1 & f1.i=v1.i by FUNCT_1:68,def 5; hence x in rng f1 by A25; end; A28: dom f2 c= dom v2 by A2,A17,A19,FINSEQ_3:32; A29: rng f2 = rng v2 \ {u} proof thus rng f2 c= rng v2 \ {u} proof let x; assume x in rng f2; then consider i such that A30: i in dom f2 & f2.i=x by FINSEQ_2:11; A31: 1<=i & i<=n & x=v2.i by A18,A30,FINSEQ_1:3,FUNCT_1:68; then i<>n+1 & i in dom v2 & n+1 in Seg len v2 by A2,A28,A30,FINSEQ_1:6,NAT_1:38; then x<>u by A2,A11,A13,A31,Th19; then not x in {u} & v2.i in rng v2 by A28,A30,FUNCT_1:def 5,TARSKI:def 1 ; hence x in rng v2 \ {u} by A31,XBOOLE_0:def 4; end; let x; assume x in rng v2 \ {u}; then A32: x in rng v2 & not x in {u} by XBOOLE_0:def 4; then consider i such that A33: i in dom v2 & v2.i=x by FINSEQ_2:11; A34: i <> len v2 by A11,A13,A32,A33,TARSKI:def 1; A35: 1<=i & i<=len v2 by A33,FINSEQ_3:27; then i<len v2 by A34,REAL_1:def 5; then i<=len f2 by A2,A19,NAT_1:38; then i in dom f2 by A35,FINSEQ_3:27; then f2.i in rng f2 & f2.i=v2.i by FUNCT_1:68,def 5; hence x in rng f2 by A33; end; f1 is increasing & f2 is increasing by A2,Th20; then A36: f1=f2 by A1,A2,A19,A21,A29; A37: len (f1^<*u*>) = n + len <*u*> by A19,FINSEQ_1:35 .= len v1 by A2,FINSEQ_1:56; now let i; assume i in Seg len v1; then A38: 1<=i & i<=len f1+1 by A2,A19,FINSEQ_1:3; now per cases; suppose i=len f1+1; hence (f1^<*u*>).i=v1.i by A2,A5,A7,A19,FINSEQ_1:59; suppose i<>len f1+1; then i < len f1+1 by A38,REAL_1:def 5; then i<=len f1 by NAT_1:38; then A39: i in dom f1 by A18,A19,A38,FINSEQ_1:3; hence (f1^<*u*>).i=f1.i by FINSEQ_1:def 7 .= v1.i by A39,FUNCT_1:68; end; hence (f1^<*u*>).i=v1.i; end; then A40: v1=f1^<*u*> by A37,FINSEQ_2:10; A41: len (f2^<*u*>) = n + len <*u*> by A19,FINSEQ_1:35 .= len v2 by A2,FINSEQ_1:56; now let i; assume i in Seg len v2; then A42: 1<=i & i<=len f2+1 by A2,A19,FINSEQ_1:3; now per cases; suppose i=len f2+1; hence (f2^<*u*>).i=v2.i by A2,A11,A13,A19,FINSEQ_1:59; suppose i<>len f2+1; then i < len f2+1 by A42,REAL_1:def 5; then i<=len f2 by NAT_1:38; then A43: i in dom f2 by A18,A19,A42,FINSEQ_1:3; hence (f2^<*u*>).i=f2.i by FINSEQ_1:def 7 .= v2.i by A43,FUNCT_1:68; end; hence (f2^<*u*>).i=v2.i; end; hence v1=v2 by A36,A40,A41,FINSEQ_2:10; end; Lm9: for n holds P3[n] from Ind(Lm7,Lm8); theorem for v1,v2 st len v1 = len v2 & rng v1 = rng v2 & v1 is increasing & v2 is increasing holds v1 = v2 by Lm9; begin :::::::::::::::::::::::: :: Proper text :::::::::::::::::::::::: definition let v1,v2 be increasing FinSequence of REAL; assume A1: v1 <> {} & v2 <> {}; func GoB(v1,v2) -> Matrix of TOP-REAL 2 means :Def1: len it = len v1 & width it = len v2 & for n,m 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 & dom v2 = Seg len v2 by FINSEQ_1:def 3; A3: for i,j st [i,j] in [:Seg len v1,Seg len v2:] holds for p1,p2 st P[i,j,p1] & P[i,j,p2] holds p1=p2 proof let i,j; assume [i,j] in [:Seg len v1,Seg len v2:]; reconsider s1=v1.i, s2=v2.j as Real; let p1,p2; assume P[i,j,p1] & P[i,j,p2]; then p1=|[s1,s2]| & p2=|[s1,s2]|; hence thesis; end; A4: for i,j st [i,j] in [:Seg len v1,Seg len v2:] ex p st P[i,j,p] proof let i,j; assume A5: [i,j] in [:Seg len v1,Seg len v2:]; reconsider s1=v1.i, s2=v2.j as Real; take |[s1,s2]|; thus [i,j] in [:dom v1,dom v2:] by A2,A5; 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 A6: for i,j st [i,j] in Indices M holds P[i,j,M* (i,j)] from MatrixEx(A3,A4); len v1 <>0 & len v2 <> 0 by A1,FINSEQ_1:25; then A7: 0 < len v1 & 0 < len v2 by NAT_1:19; reconsider M as Matrix of the carrier of TOP-REAL 2; take M; thus len M=len v1 & width M=len v2 by A7,MATRIX_1:24; let n,m; assume [n,m] in Indices M; hence M*(n,m) = |[v1.n,v2.m]| by A6; end; uniqueness proof let G1,G2 be Matrix of TOP-REAL 2; assume that A8: len G1 = len v1 & width G1 = len v2 & for n,m st [n,m] in Indices G1 holds G1*(n,m) = |[v1.n,v2.m]| and A9: len G2 = len v1 & width G2 = len v2 & for n,m 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_1:def 5; now let n,m; assume A11: [n,m] in Indices G1; A12: dom G1 = Seg len G1 & dom G2 = Seg len G2 by FINSEQ_1:def 3; reconsider r=v1.n, s=v2.m as Real; G1*(n,m)=|[r,s]| & G2*(n,m)=|[r,s]| by A8,A9,A10,A11,A12; hence G1*(n,m)=G2*(n,m); end; hence thesis by A8,A9,MATRIX_1:21; end; end; definition let v1,v2 be non empty increasing FinSequence of REAL; cluster GoB(v1,v2) -> non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column; coherence proof set M = GoB(v1,v2); A1: rng v1 c= REAL & rng v2 c= REAL & dom v1=Seg len v1 & dom v2=Seg len v2 by FINSEQ_1:def 3,def 4; A2: len v1 <>0 & len v2 <> 0 by FINSEQ_1:25; A3: len M=len v1 & width M=len v2 by Def1; then A4: dom M = dom v1 & width M=len v2 by FINSEQ_3:31; then A5: Indices M=[:dom v1,Seg len v2:] by MATRIX_1:def 5; thus M is non empty-yielding by A2,A3,GOBOARD1:def 5; thus M is X_equal-in-line proof let n; reconsider l = Line(M,n) as FinSequence of TOP-REAL 2; set x = X_axis(l); assume A6: n in dom M; A7: len x = len l & len l = width M & dom x = Seg len x by FINSEQ_1:def 3,GOBOARD1:def 3,MATRIX_1:def 8; then A8: dom x = dom l by FINSEQ_3:31; now let i,j; assume A9: i in dom x & j in dom x; then A10: [n,i] in Indices M & [n,j] in Indices M by A4,A5,A6,A7,ZFMISC_1:106 ; reconsider r=v1.n, s1=v2.i, s2=v2.j as Real; M*(n,i)=|[r,s1]| & M*(n,j)=|[r,s2]| by A10,Def1; then A11: M*(n,i)`1 = r & M*(n,j)`1 = r by EUCLID:56; l/.i = l.i & l/.j = l.j by A8,A9,FINSEQ_4:def 4; then l/.i=M*(n,i) & l/.j=M*(n,j) by A7,A9,MATRIX_1:def 8; then x.i=r & x.j=r by A9,A11,GOBOARD1:def 3; hence x.i=x.j; end; hence X_axis(Line(M,n)) is constant by GOBOARD1:def 2; end; thus M is Y_equal-in-column proof let n; reconsider c = Col(M,n) as FinSequence of TOP-REAL 2; set y = Y_axis(c); assume A12: n in Seg width M; len y = len c & len c = len M & dom y = Seg len y by FINSEQ_1:def 3,GOBOARD1:def 4,MATRIX_1:def 9; then A13: dom y = dom c & dom c = dom M by FINSEQ_3:31; now let i,j; assume A14: i in dom y & j in dom y; then A15: [i,n] in Indices M & [j,n] in Indices M by A4,A5,A12,A13,ZFMISC_1:106 ; reconsider r=v2.n, s1=v1.i, s2=v1.j as Real; M*(i,n)=|[s1,r]| & M*(j,n)=|[s2,r]| by A15,Def1; then A16: M*(i,n)`2 = r & M*(j,n)`2 = r by EUCLID:56; c/.i = c.i & c/.j = c.j by A13,A14,FINSEQ_4:def 4; then c/.i=M*(i,n) & c/.j=M*(j,n) by A13,A14,MATRIX_1:def 9; then y.i=r & y.j=r by A14,A16,GOBOARD1:def 4; hence y.i=y.j; end; hence Y_axis(Col(M,n)) is constant by GOBOARD1:def 2; end; thus M is Y_increasing-in-line proof let n; reconsider l = Line(M,n) as FinSequence of TOP-REAL 2; set y = Y_axis(l); assume A17: n in dom M; A18: len y = len l & len l = width M & dom y = Seg len y by FINSEQ_1:def 3,GOBOARD1:def 4,MATRIX_1:def 8; then A19: dom y = dom l by FINSEQ_3:31; now let i,j; assume A20: i in dom y & j in dom y & i<j; then A21: [n,i] in Indices M & [n,j] in Indices M by A4,A5,A17,A18,ZFMISC_1:106; reconsider r=v1.n, s1=v2.i, s2=v2.j as Real; M*(n,i)=|[r,s1]| & M*(n,j)=|[r,s2]| by A21,Def1; then A22: M*(n,i)`2 = s1 & M*(n,j)`2 = s2 by EUCLID:56; l/.i = l.i & l/.j = l.j by A19,A20,FINSEQ_4:def 4; then l/.i=M*(n,i) & l/.j=M*(n,j) by A18,A20,MATRIX_1:def 8; then y.i=s1 & y.j=s2 & s1<s2 by A1,A3,A18,A20,A22,GOBOARD1:def 1,def 4; hence y.i<y.j; end; hence Y_axis(Line(M,n)) is increasing by GOBOARD1:def 1; end; thus M is X_increasing-in-column proof let n; reconsider c = Col(M,n) as FinSequence of TOP-REAL 2; set x = X_axis(c); assume A23: n in Seg width M; A24: len x = len c & len c = len M & dom x = Seg len x by FINSEQ_1:def 3,GOBOARD1:def 3,MATRIX_1:def 9; then A25: dom x = dom c & dom c = dom M by FINSEQ_3:31; now let i,j; assume A26: i in dom x & j in dom x & i<j; then A27: [i,n] in Indices M & [j,n] in Indices M by A4,A5,A23,A25,ZFMISC_1:106 ; reconsider r=v2.n, s1=v1.i, s2=v1.j as Real; M*(i,n)=|[s1,r]| & M*(j,n)=|[s2,r]| by A27,Def1; then A28: M*(i,n)`1 = s1 & M*(j,n)`1 = s2 by EUCLID:56; c/.i = c.i & c/.j = c.j by A25,A26,FINSEQ_4:def 4; then c/.i=M*(i,n) & c/.j=M*(j,n) by A25,A26,MATRIX_1:def 9; then x.i=s1 & x.j=s2 & s1<s2 by A1,A3,A24,A26,A28,GOBOARD1:def 1,def 3; hence x.i<x.j; end; hence X_axis(Col(M,n)) is increasing by GOBOARD1:def 1; end; end; end; definition let v; func Incr(v) ->increasing FinSequence of REAL means :Def2: rng it = rng v & len it = card rng v; existence proof consider v1 such that A1: rng v1 = rng v & len v1 = card rng v & v1 is increasing by Lm6; reconsider v1 as increasing FinSequence of REAL by A1; take v1; thus thesis by A1; end; uniqueness by Lm9; end; definition let f be non empty FinSequence of TOP-REAL 2; func GoB(f) -> Matrix of TOP-REAL 2 equals :Def3: GoB(Incr(X_axis(f)),Incr(Y_axis(f))); correctness; end; theorem Th23: v <> {} implies Incr(v) <> {} proof assume A1: v <> {}; assume Incr(v) = {}; then len Incr(v) = 0 & len Incr(v)=card rng v & rng v is finite by Def2,FINSEQ_1:25; then rng v = {} & rng v <> {} by A1,CARD_2:59,FINSEQ_1:27; hence contradiction; end; definition let v be non empty FinSequence of REAL; cluster Incr v -> non empty; coherence by Th23; end; definition 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 proof reconsider w1 = X_axis f, w2 = Y_axis f as non empty FinSequence of REAL; reconsider v1 = Incr w1, v2 = Incr w2 as non empty increasing FinSequence of REAL; GoB(f) = GoB(v1,v2) by Def3; hence thesis; end; end; reserve f for non empty FinSequence of TOP-REAL 2; theorem Th24: 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); A1: x<>{} & y<>{} & GoB(f)=GoB(Incr(x),Incr(y)) by Def3; Incr(x) <> {} & Incr(y) <> {} & len Incr(x)=card rng x & len Incr(y)=card rng y by Def2; hence thesis by A1,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); A1: len GoB(f)=card rng x & width GoB(f)=card rng y & GoB(f)=GoB(Incr(x),Incr(y)) & x<>{} & y<>{} by Def3,Th24; A2: Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & Incr(x) <> {} & Incr(y) <> {} by MATRIX_1:def 5; let n such that A3: n in dom f; A4: dom f = Seg len f & dom x = Seg len x & dom y = Seg len y & rng f c= the carrier of TOP-REAL 2 by FINSEQ_1:def 3,def 4; reconsider p=f/.n as Point of TOP-REAL 2; len x = len f & len y = len f by GOBOARD1:def 3,def 4; then A5: x.n=p`1 & y.n=p`2 & x.n in rng x & y.n in rng y by A3,A4,FUNCT_1:def 5,GOBOARD1:def 3,def 4; A6: rng Incr(x) = rng x & rng Incr(y) = rng y & len Incr(x) = card rng x & len Incr(y) = card rng y by Def2; then consider i such that A7: i in dom Incr(x) & Incr(x).i=p`1 by A5,FINSEQ_2:11; consider j such that A8: j in dom Incr(y) & Incr(y).j=p`2 by A5,A6,FINSEQ_2:11; take i,j; dom GoB(f) = dom Incr(x) & Seg width GoB(f) = dom Incr(y) by A1,A6,FINSEQ_1:def 3,FINSEQ_3:31; hence [i,j] in Indices GoB(f) by A2,A7,A8,ZFMISC_1:106; then GoB(f)*(i,j) = |[p`1,p`2]| & p=|[p`1,p`2]| by A1,A7,A8,Def1,EUCLID:57; hence thesis; 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 A1: n in dom f & for m st m in dom f holds r <= x.m; A2: GoB(f)=GoB(Incr(x),Incr(y)) & x<>{} & y<>{} & len GoB(f)=card rng x & width GoB(f) = card rng y by Def3,Th24; A3: Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & Incr(x)<>{} & Incr(y)<>{} by MATRIX_1:def 5; A4: dom f = Seg len f & dom x = Seg len x & dom y = Seg len y & rng f c= the carrier of TOP-REAL 2 by FINSEQ_1:def 3,def 4; reconsider p=f/.n as Point of TOP-REAL 2; A5: len x = len f & len y = len f by GOBOARD1:def 3,def 4; then A6: x.n=p`1 & y.n=p`2 & x.n in rng x & y.n in rng y by A1,A4,FUNCT_1:def 5,GOBOARD1:def 3,def 4; A7: rng Incr(x) = rng x & rng Incr(y) = rng y & len Incr(x) = card rng x & len Incr(y) = card rng y by Def2; then consider i such that A8: i in dom Incr(x) & Incr(x).i=p`1 by A6,FINSEQ_2:11; consider j such that A9: j in dom Incr(y) & Incr(y).j=p`2 by A6,A7,FINSEQ_2:11; A10: 1<=i & i<=len Incr(x) & dom Incr(x)=dom Incr(x) & rng Incr(x) c= REAL by A8,FINSEQ_1:def 4,FINSEQ_3:27; then reconsider i1=i-1 as Nat by INT_1:18; A11: dom Incr(x) = dom GoB(f) by A2,A7,FINSEQ_3:31; A12: dom Incr(y) = Seg width GoB(f) by A2,A7,FINSEQ_1:def 3; A13: now assume i <> 1; then 1<i & 0<=1 & 0<1 by A10,REAL_1:def 5; then A14: 1+1<=i & i1<=i & i1<i by NAT_1:38,SQUARE_1:29; then 1<=i1 & i1<=len Incr(x) by A10,AXIOMS:22,REAL_1:84; then A15: i1 in dom Incr(x) by FINSEQ_3:27; then A16: Incr(x).i1 in rng Incr(x) by FUNCT_1:def 5; reconsider s=Incr(x).i1 as Real; A17: s<r by A6,A8,A14,A15,GOBOARD1:def 1; ex m st m in dom x & x.m=s by A7,A16,FINSEQ_2:11; hence contradiction by A1,A4,A5,A17; end; then [1,j] in Indices GoB(f) by A3,A8,A9,A11,A12,ZFMISC_1:106; then GoB(f)*(1,j) = |[p`1,p`2]| & p=|[p`1,p`2]| by A2,A8,A9,A13,Def1,EUCLID:57; then (Line(GoB(f),1)).j = f/.n & len Line(GoB(f),1) = width GoB(f) by A9,A12,MATRIX_1:def 8; then (Line(GoB(f),1)).j = f/.n & dom Line(GoB(f),1) = Seg width GoB(f) by FINSEQ_1:def 3; hence f/.n in rng Line(GoB(f),1) by A9,A12,FUNCT_1:def 5; 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 A1: n in dom f & for m st m in dom f holds x.m <= r; A2: GoB(f)=GoB(Incr(x),Incr(y)) & x<>{} & y<>{} & len GoB(f)=card rng x & width GoB(f) = card rng y by Def3,Th24; A3: Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & Incr(x)<>{} & Incr(y)<>{} by MATRIX_1:def 5; A4: dom f = Seg len f & dom x = Seg len x & dom y = Seg len y & rng f c= the carrier of TOP-REAL 2 by FINSEQ_1:def 3,def 4; reconsider p=f/.n as Point of TOP-REAL 2; A5: len x = len f & len y = len f by GOBOARD1:def 3,def 4; then A6: x.n=p`1 & y.n=p`2 & x.n in rng x & y.n in rng y by A1,A4,FUNCT_1:def 5,GOBOARD1:def 3,def 4; A7: rng Incr(x) = rng x & rng Incr(y) = rng y & len Incr(x) = card rng x & len Incr(y) = card rng y by Def2; then consider i such that A8: i in dom Incr(x) & Incr(x).i=p`1 by A6,FINSEQ_2:11; consider j such that A9: j in dom Incr(y) & Incr(y).j=p`2 by A6,A7,FINSEQ_2:11; A10: 1<=i & i<=len Incr(x) & dom Incr(x)=dom Incr(x) & rng Incr(x) c= REAL by A8,FINSEQ_1:def 4,FINSEQ_3:27; A11: dom Incr(x) = dom GoB(f) by A2,A7,FINSEQ_3:31; A12: dom Incr(y) = Seg width GoB(f) by A2,A7,FINSEQ_1:def 3; A13: now assume i <> len Incr(x); then i<len Incr(x) & i<=i+1 by A10,NAT_1:29,REAL_1:def 5; then 1<=i+1 & i+1<=len Incr(x) by A10,NAT_1:38; then A14: i+1 in dom Incr(x) & i<i+1 by FINSEQ_3:27,NAT_1:38; then A15: Incr(x).(i+1) in rng Incr(x) by FUNCT_1:def 5; reconsider s=Incr(x).(i+1) as Real; A16: r<s by A6,A8,A14,GOBOARD1:def 1; ex m st m in dom x & x.m=s by A7,A15,FINSEQ_2:11; hence contradiction by A1,A4,A5,A16; end; then [len GoB(f),j] in Indices GoB(f) by A2,A3,A7,A8,A9,A11,A12,ZFMISC_1:106; then GoB(f)*(len GoB(f),j) = |[p`1,p`2]| & p=|[p`1,p`2]| by A2,A7,A8,A9,A13,Def1,EUCLID:57; then (Line(GoB(f),len GoB(f))).j = f/.n & len Line(GoB(f),len GoB(f))=width GoB(f) by A9,A12,MATRIX_1:def 8; then (Line(GoB(f),len GoB(f))).j = f/.n & dom Line(GoB(f),len GoB(f))= Seg width GoB(f) by FINSEQ_1:def 3; hence f/.n in rng Line(GoB(f),len GoB(f)) by A9,A12,FUNCT_1:def 5; 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 A1: n in dom f & for m st m in dom f holds r <= y.m; A2: GoB(f)=GoB(Incr(x),Incr(y)) & x<>{} & y<>{} & len GoB(f)=card rng x & width GoB(f) = card rng y by Def3,Th24; A3: Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & Incr(x)<>{} & Incr(y)<>{} by MATRIX_1:def 5; A4: dom f = Seg len f & dom x = Seg len x & dom y = Seg len y & rng f c= the carrier of TOP-REAL 2 by FINSEQ_1:def 3,def 4; reconsider p=f/.n as Point of TOP-REAL 2; A5: len x = len f & len y = len f by GOBOARD1:def 3,def 4; then A6: x.n=p`1 & y.n=p`2 & x.n in rng x & y.n in rng y by A1,A4,FUNCT_1:def 5,GOBOARD1:def 3,def 4; A7: rng Incr(x) = rng x & rng Incr(y) = rng y & len Incr(x) = card rng x & len Incr(y) = card rng y by Def2; then consider i such that A8: i in dom Incr(x) & Incr(x).i=p`1 by A6,FINSEQ_2:11; consider j such that A9: j in dom Incr(y) & Incr(y).j=p`2 by A6,A7,FINSEQ_2:11; A10: 1<=j & j<=len Incr(y) & dom Incr(y)=dom Incr(y) & rng Incr(y) c= REAL by A9,FINSEQ_1:def 4,FINSEQ_3:27; then reconsider j1=j-1 as Nat by INT_1:18; A11: dom Incr(x) = dom GoB(f) & dom Incr(y) = Seg width GoB(f) by A2,A7,FINSEQ_1:def 3,FINSEQ_3:31; A12: now assume j <> 1; then 1<j & 0<=1 & 0<1 by A10,REAL_1:def 5; then A13: 1+1<=j & j1<=j & j1<j by NAT_1:38,SQUARE_1:29; then 1<=j1 & j1<=len Incr(y) by A10,AXIOMS:22,REAL_1:84; then A14: j1 in dom Incr(y) by FINSEQ_3:27; then A15: Incr(y).j1 in rng Incr(y) by FUNCT_1:def 5; reconsider s=Incr(y).j1 as Real; A16: s<r by A6,A9,A13,A14,GOBOARD1:def 1; ex m st m in dom y & y.m=s by A7,A15,FINSEQ_2:11; hence contradiction by A1,A4,A5,A16; end; then [i,1] in Indices GoB(f) by A3,A8,A9,A11,ZFMISC_1:106; then GoB(f)*(i,1) = |[p`1,p`2]| & p=|[p`1,p`2]| by A2,A8,A9,A12,Def1,EUCLID:57; then (Col(GoB(f),1)).i = f/.n & len Col(GoB(f),1) = len GoB(f) by A8,A11,MATRIX_1:def 9; then (Col(GoB(f),1)).i = f/.n & dom Col(GoB(f),1) = dom GoB(f) by FINSEQ_3:31 ; hence f/.n in rng Col(GoB(f),1) by A8,A11,FUNCT_1:def 5; 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 A1: n in dom f & for m st m in dom f holds y.m <= r; A2: GoB(f)=GoB(Incr(x),Incr(y)) & x<>{} & y<>{} & len GoB(f)=card rng x & width GoB(f) = card rng y by Def3,Th24; A3: Indices GoB(f) = [:dom GoB(f), Seg width GoB(f):] & Incr(x)<>{} & Incr(y)<>{} by MATRIX_1:def 5; A4: dom f = Seg len f & dom x = Seg len x & dom y = Seg len y & rng f c= the carrier of TOP-REAL 2 by FINSEQ_1:def 3,def 4; reconsider p=f/.n as Point of TOP-REAL 2; A5: len x = len f & len y = len f by GOBOARD1:def 3,def 4; then A6: x.n=p`1 & y.n=p`2 & x.n in rng x & y.n in rng y by A1,A4,FUNCT_1:def 5,GOBOARD1:def 3,def 4; A7: rng Incr(x) = rng x & rng Incr(y) = rng y & len Incr(x) = card rng x & len Incr(y) = card rng y by Def2; then consider i such that A8: i in dom Incr(x) & Incr(x).i=p`1 by A6,FINSEQ_2:11; consider j such that A9: j in dom Incr(y) & Incr(y).j=p`2 by A6,A7,FINSEQ_2:11; A10: 1<=j & j<=len Incr(y) & dom Incr(y)=dom Incr(y) & rng Incr(y) c= REAL by A9,FINSEQ_1:def 4,FINSEQ_3:27; A11: dom Incr(x) = dom GoB(f) & dom Incr(y) = Seg width GoB(f) by A2,A7,FINSEQ_1:def 3,FINSEQ_3:31; A12: now assume j <> len Incr(y); then j<len Incr(y) & j<=j+1 by A10,NAT_1:29,REAL_1:def 5; then 1<=j+1 & j+1<=len Incr(y) by A10,NAT_1:38; then A13: j+1 in dom Incr(y) & j<j+1 by FINSEQ_3:27,NAT_1:38; then A14: Incr(y).(j+1) in rng Incr(y) by FUNCT_1:def 5; reconsider s=Incr(y).(j+1) as Real; A15: r<s by A6,A9,A13,GOBOARD1:def 1; ex m st m in dom y & y.m=s by A7,A14,FINSEQ_2:11; hence contradiction by A1,A4,A5,A15; end; then [i,width GoB(f)] in Indices GoB(f) by A2,A3,A7,A8,A9,A11,ZFMISC_1:106; then GoB(f)*(i,width GoB(f)) = |[p`1,p`2]| & p=|[p`1,p`2]| by A2,A7,A8,A9,A12,Def1,EUCLID:57; then (Col(GoB(f),width GoB(f))).i = f/.n & len Col(GoB(f),width GoB(f))=len GoB(f) by A8,A11,MATRIX_1:def 9; then (Col(GoB(f),width GoB(f))).i = f/.n & dom Col(GoB(f),width GoB(f))=dom GoB(f) by FINSEQ_3:31; hence f/.n in rng Col(GoB(f),width GoB(f)) by A8,A11,FUNCT_1:def 5; end;

Back to top