Copyright (c) 1992 Association of Mizar Users
environ vocabulary PRE_TOPC, EUCLID, FINSEQ_1, GOBOARD1, RELAT_1, TOPREAL1, FINSEQ_4, BOOLE, MATRIX_1, FUNCT_1, ABSVALUE, ARYTM_1, MCART_1, TREES_1, INCSP_1, SEQM_3, ORDINAL2, TARSKI; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, PRE_TOPC, ABSVALUE, FINSEQ_4, MATRIX_1, EUCLID, TOPREAL1, GOBOARD1; constructors SEQM_3, NAT_1, ABSVALUE, TOPREAL1, GOBOARD1, FINSEQ_4, INT_1, MEMBERED, REAL_1, XBOOLE_0; clusters RELSET_1, STRUCT_0, EUCLID, INT_1, XREAL_0, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, TOPREAL1, XBOOLE_0; theorems AXIOMS, TARSKI, REAL_1, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE, SQUARE_1, FINSEQ_3, REAL_2, MATRIX_1, EUCLID, TOPREAL1, TOPREAL3, GOBOARD1, GOBOARD2, FINSEQ_4, PROB_1, GROUP_5, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1; schemes NAT_1, GOBOARD1, GOBOARD2; begin reserve p,p1,p2,q for Point of TOP-REAL 2, f,g,g1,g2 for FinSequence of TOP-REAL 2, n,m,i,j,k for Nat, G for Go-board, x for set; Lm1: now let f,k; assume A1: len f=k+1; assume k<>0; then A2: 0<k & k<=k+1 by NAT_1:19,29; then 0+1<=k & k<=len f & k+1 <= len f by A1,NAT_1:38; then A3: k in dom f by FINSEQ_3:27; A4: len (f|k)=k by A1,A2,TOPREAL1:3; A5: dom(f|k)=Seg len(f|k) by FINSEQ_1:def 3; assume A6:f is unfolded; thus f|k is unfolded proof set f1 = f|k; let n; assume A7: 1<=n & n+2 <= len f1; then n in dom f1 & n+1 in dom f1 & n+2 in dom f1 & n+1+1=n+(1+1) by GOBOARD2:4,XCMPLX_1:1; then A8: LSeg(f1,n)=LSeg(f,n) & LSeg(f1,n+1)=LSeg(f,n+1) & f1/.(n+1)=f/.(n+1) by A3,A4,A5,GOBOARD1:10,TOPREAL3:24; len f1 <= len f by A1,A2,TOPREAL1:3; then n+2 <= len f by A7,AXIOMS:22; hence LSeg(f1,n) /\ LSeg(f1,n+1)={f1/.(n+1)} by A6,A7,A8,TOPREAL1:def 8; end; end; theorem Th1: (for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j)) & f is one-to-one unfolded s.n.c. special implies ex g st g is_sequence_on G & g is one-to-one unfolded s.n.c. special & L~f = L~g & f/.1 = g/.1 & f/.len f = g/.len g & 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 one-to-one unfolded s.n.c. special ex g st g is_sequence_on G & g is one-to-one unfolded s.n.c. special & L~f=L~g & f/.1=g/.1 & f/.len f=g/.len g & 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 one-to-one unfolded s.n.c. special; 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 thesis 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 one-to-one and A8: f is unfolded and A9: f is s.n.c. and A10: f is special; per cases; suppose k=0; then A11: 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 A11,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 by A6,GOBOARD1:def 11; thus g is one-to-one unfolded s.n.c. special & L~f=L~g & f/.1=g/.1 & f/.len f=g/.len g & len f<=len g by A7,A8,A9,A10; suppose A12: k<>0; then A13: 0<k & k<=k+1 by NAT_1:19,29; then A14: 0+1<=k & k<=len f & k+1 <= len f by A5,NAT_1:38; then A15: k in dom f by FINSEQ_3:27; A16: len (f|k)=k by A5,A13,TOPREAL1:3; A17: dom(f|k)=Seg len(f|k) by FINSEQ_1:def 3; A18: k in Seg k by A14,FINSEQ_1:3; A19: 1 in Seg k by A14,FINSEQ_1:3; set f1=f|k; A20: now let n; assume A21: n in dom f1; then n in dom f by A15,A16,A17,GOBOARD1:10; then consider i,j such that A22: [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 A15,A16,A17,A21,A22,GOBOARD1:10; end; f1 = f|Seg k by TOPREAL1:def 1; then A23: f1 is one-to-one by A7,FUNCT_1:84; A24: f1 is unfolded by A5,A8,A12,Lm1; A25: f1 is s.n.c. by A9,GOBOARD2:12; f1 is special proof let n; assume A26: 1<=n & n+1 <= len f1; then n in dom f1 & n+1 in dom f1 by GOBOARD2:3; then A27: f1/.n=f/.n & f1/.(n+1)=f/.(n+1) by A15,A16,A17,GOBOARD1:10; len f1 <=len f by A5,A13,TOPREAL1:3; then n+1 <= len f by A26,AXIOMS:22; hence (f1/.n)`1=(f1/.(n+1))`1 or (f1/.n)`2=(f1/.(n+1))`2 by A10,A26,A27,TOPREAL1:def 7; end; then consider g1 such that A28: g1 is_sequence_on G and A29: g1 is one-to-one and A30: g1 is unfolded and A31: g1 is s.n.c. and A32: g1 is special and A33: L~g1=L~f1 and A34: g1/.1=f1/.1 and A35: g1/.len g1=f1/.len f1 and A36: len f1<=len g1 by A4,A16,A20,A23,A24,A25; A37: k=1 implies L~g1={} & rng g1 = {f/.k} proof assume A38: k=1; hence L~g1={} by A16,A33,TOPREAL1:28; then A39: (len g1=1 or len g1=0) & 1<=len g1 by A5,A36,A38,TOPREAL1:3,28; then A40: len g1 in dom g1 by FINSEQ_3:27; A41: g1/.len g1=f/.k by A15,A16,A18,A35,GOBOARD1:10; then f/.k in rng g1 by A40,PARTFUN2:4; then A42: {f/.k} c= rng g1 by ZFMISC_1:37; rng g1 c= {f/.k} proof let x; assume x in rng g1; then consider n such that A43: n in dom g1 & g1/.n=x by PARTFUN2:4; n in Seg len g1 by A43,FINSEQ_1:def 3; then n=len g1 by A39,FINSEQ_1:4,TARSKI:def 1; hence x in {f/.k} by A41,A43,TARSKI:def 1; end; hence rng g1={f/.k} by A42,XBOOLE_0:def 10; end; A44: 1<k implies rng g1 c= L~f1 proof assume 1<k; then 1+1<=k by NAT_1:38; then A45: 2<=len g1 by A16,A36,AXIOMS:22; let x; assume x in rng g1; then consider n such that A46: n in dom g1 & g1/.n=x by PARTFUN2:4; thus x in L~f1 by A33,A45,A46,GOBOARD1:16; end; consider i1,i2 be Nat such that A47: [i1,i2] in Indices G & f/.k=G*(i1,i2) by A6,A15; 1<=len f by A14,AXIOMS:22; then A48: k+1 in dom f by A5,FINSEQ_3:27; then consider j1,j2 be Nat such that A49: [j1,j2] in Indices G & f/.(k+1)=G*(j1,j2) by A6; A50: Indices G = [:dom G,Seg width G:] by MATRIX_1:def 5; then A51: i1 in dom G & i2 in Seg width G & j1 in dom G & j2 in Seg width G by A47,A49,ZFMISC_1:106; A52:dom G = Seg len G by FINSEQ_1:def 3; A53: (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 A28,GOBOARD1:def 11; 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); A54: x1 is constant by A51,GOBOARD1:def 6; A55: y1 is increasing by A51,GOBOARD1:def 8; A56: x2 is increasing by A51,GOBOARD1:def 9; A57: y2 is constant by A51,GOBOARD1:def 7; A58: dom x1=Seg len x1 by FINSEQ_1:def 3; A59: dom y1=Seg len y1 by FINSEQ_1:def 3; A60: len y1=len l1 by GOBOARD1:def 4; A61: len x1=len l1 by GOBOARD1:def 3; A62: len l1=width G by MATRIX_1:def 8; then A63:Seg width G = dom l1 by FINSEQ_1:def 3; A64: dom x2= Seg len x2 by FINSEQ_1:def 3; A65: dom y2=Seg len y2 by FINSEQ_1:def 3; A66: len x2=len c1 by GOBOARD1:def 3; then A67: dom c1 = Seg len x2 by FINSEQ_1:def 3 .= dom x2 by FINSEQ_1:def 3; A68: len y2=len c1 by GOBOARD1:def 4; A69: len c1 = len G by MATRIX_1:def 9; then A70: dom c1 = Seg len G by FINSEQ_1:def 3 .= dom G by FINSEQ_1:def 3; now per cases by A10,A15,A47,A48,A49,GOBOARD2:16; suppose A71: i1=j1; set ppi = G*(i1,i2), pj = G*(i1,j2); now per cases by AXIOMS:21; case A72: i2>j2; then reconsider l=i2-j2 as Nat by INT_1:18; A73: now let n; assume n in Seg l; then A74: 1<=n & n<=l & 0<=j2 by FINSEQ_1:3,NAT_1:18; then l<=i2 by PROB_1:2; then n<=i2 by A74,AXIOMS:22; then reconsider w=i2-n as Nat by INT_1:18; 0<=n & i2-l<=i2-n by A74,AXIOMS:22,REAL_1:92; then i2-n<=i2 & i2<=width G & j2<=w & 1<=j2 by A51,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 A50,A51,ZFMISC_1:106; end; defpred P1[Nat,set] means for m st m=i2-$1 holds $2=G*(i1,m); A75: now let n; assume n in Seg l; then reconsider m=i2-n as Nat by A73; take p=G*(i1,m); thus P1[n,p]; end; consider g2 such that A76: len g2=l & for n st n in Seg l holds P1[n,g2/.n] from FinSeqDChoice(A75); A77: dom g2 = Seg l by A76,FINSEQ_1:def 3; take g=g1^g2; now let n; assume A78: n in dom g2; then reconsider m=i2-n as Nat by A73,A77; take k=i1,m; thus [k,m] in Indices G & g2/.n=G*(k,m) by A73,A76,A77,A78; end; then A79: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G* (i,j) by A53,GOBOARD1:39; A80: now let n; assume A81: n in dom g2 & n+1 in dom g2; then A82: [i1,i2-n] in Indices G & [i1,i2-(n+1)] in Indices G by A73,A77; reconsider m1=i2-n ,m2=i2-(n+1) as Nat by A73,A77,A81; A83: g2/.n=G*(i1,m1) & g2/.(n+1)=G*(i1,m2) by A76,A77,A81; 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 by A82,A83,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; A84: now let l1,l2,l3,l4 be Nat; assume A85: [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 A86: [i1,i2-1] in Indices G & f1/.len f1=f/.k by A15,A16,A18,A73,A77,GOBOARD1:10; reconsider m1=i2-1 as Nat by A73,A77,A85; g2/.1=G*(i1,m1) by A76,A77,A85; then l1=i1 & l2=i2 & l3=i1 & l4=m1 by A35,A47,A85,A86,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 A53,A80,GOBOARD1:40; hence g is_sequence_on G by A79,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}; l1/.i2=l1.i2 & l1/.j2 = l1.j2 by A51,A63,FINSEQ_4:def 4; then A87: l1/.i2=ppi & l1/.j2=pj by A51,MATRIX_1:def 8; then A88: y1.i2=ppi`2 & y1.j2=pj`2 & x1.i2=ppi`1 & x1.j2=pj`1 & l=len g2 by A51,A58,A59,A60,A61,A62,A76,GOBOARD1:def 3,def 4; then A89: pj`2<ppi`2 & ppi`1=pj`1 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj`2]| by A51,A54,A55,A58,A59,A60,A61,A62,A72,EUCLID:57,GOBOARD1:def 1,def 2; A90: LSeg(f,k)=LSeg(pj,ppi) by A14,A47,A49,A71,TOPREAL1:def 5 .= lk by A89,TOPREAL3:15; A91: LSeg(f,k)=LSeg(ppi,pj) by A14,A47,A49,A71,TOPREAL1:def 5; now let n,m; assume A92: n in dom g2 & m in dom g2 & n<>m; then A93: [i1,i2-n] in Indices G& [i1,i2-m] in Indices G by A73,A77; reconsider n1=i2-n, m1=i2-m as Nat by A73,A77,A92; A94: g2/.n=G*(i1,n1) & g2/.m=G*(i1,m1) by A76,A77,A92; assume g2/.n=g2/.m; then n1=m1 by A93,A94,GOBOARD1:21; hence contradiction by A92,XCMPLX_1:20; end; then for n,m st n in dom g2 & m in dom g2 & g2/.n = g2/.m holds n = m; then A95: g2 is one-to-one & dom g2=Seg len g2 by FINSEQ_1:def 3,PARTFUN2: 16; A96: not f/.k in rng g2 proof assume f/.k in rng g2; then consider n such that A97: n in dom g2 & g2/.n=f/.k by PARTFUN2:4; A98: [i1,i2-n] in Indices G by A73,A76,A95,A97; reconsider n1=i2-n as Nat by A73,A76,A95,A97; g2/.n=G*(i1,n1) & 0+1<=n by A76,A95,A97,FINSEQ_1:3; then n1=i2 & 0<n by A47,A97,A98,GOBOARD1:21,NAT_1:38; hence contradiction by SQUARE_1:29; end; A99: now let n,p; assume A100: n in dom g2 & g2/.n=p; then A101: P1[n,g2/.n] & 1<=n & n<=len g2& i2-n in Seg width G by A73,A76,A95,FINSEQ_3:27; reconsider n1=i2-n as Nat by A73,A77,A100; set pn = G*(i1,n1); l1/.n1=l1.n1 by A63,A101,FINSEQ_4:def 4; then A102: g2/.n=pn & l1/.n1=pn & 0<=n & i2-len g2<=n1 by A101,AXIOMS:22,MATRIX_1:def 8,REAL_1:92; then A103: x1.n1=pn`1 & x1.n1=x1.i2 & y1.n1=pn`2 & n1<=i2 & j2<=n1 by A51,A54,A58,A59,A60,A61,A62,A76,A101,GOBOARD1:def 2,def 3,def 4, REAL_2:173,XCMPLX_1:18; hence p`1=ppi`1 & pj`2<=p`2 & p`2<=ppi`2 by A51,A55,A59,A60,A62,A88,A100,A101,A102,GOBOARD2:18; dom l1 = Seg len l1 by FINSEQ_1:def 3; hence p in rng l1 by A62,A100,A101,A102,PARTFUN2:4; 0<n by A101,AXIOMS:22; then n1<i2 by SQUARE_1:29; hence p`2<ppi`2 by A51,A55,A59,A60,A62,A88,A100,A101,A102,A103, GOBOARD1:def 1; end; A104: now let n,m,p,q; assume A105: n in dom g2 & m in dom g2 & n<m & g2/.n=p & g2/.m=q; then A106: P1[n,g2/.n] & i2-n in Seg width G & P1[m,g2/.m] & i2-m in Seg width G by A73,A76,A77; reconsider n1=i2-n, m1=i2-m as Nat by A73,A77,A105; set pn = G*(i1,n1), pm = G*(i1,m1); l1/.n1=l1.n1 & l1/.m1 = l1.m1 by A63,A106,FINSEQ_4:def 4; then A107: g2/.n=pn & l1/.n1=pn & g2/.m=pm & l1/.m1=pm & m1<n1 by A105,A106,MATRIX_1:def 8,REAL_1:92; then y1.n1=pn`2 & y1.m1=pm`2 by A59,A60,A62,A106,GOBOARD1:def 4; hence q`2<p`2 by A55,A59,A60,A62,A105,A106,A107,GOBOARD1:def 1; end; A108: rng g2 c= LSeg(f,k) proof let x; assume x in rng g2; then consider n such that A109: n in dom g2 & g2/.n=x by PARTFUN2:4; reconsider n1=i2-n as Nat by A73,A76,A95,A109; set pn = G*(i1,n1); A110: g2/.n=pn by A76,A95,A109; then pn`1=ppi`1 & pj`2<=pn`2 & pn`2<=ppi`2 by A99,A109; hence x in LSeg(f,k) by A90,A109,A110; end; rng g1 /\ rng g2 = {} proof consider x being Element of rng g1 /\ rng g2; assume not thesis; then A111: x in rng g1 & x in rng g2 by XBOOLE_0:def 3; now per cases by A14,REAL_1:def 5; suppose k=1; hence contradiction by A37,A96,A111,TARSKI:def 1; suppose 1<k; then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A44,A108,A111,GOBOARD2:9,XBOOLE_0:def 3; hence contradiction by A96,A111,TARSKI:def 1; end; hence contradiction; end; then rng g1 misses rng g2 by XBOOLE_0:def 7; hence g is one-to-one by A29,A95,FINSEQ_3:98; A112: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2,n+1) = {g2/.(n+1)} proof let n; assume A113: 1<=n & n+2 <= len g2; then A114: n in dom g2 & n+1 in dom g2 & n+2 in dom g2 by GOBOARD2:4; then g2/.n in rng g2 & g2/.(n+1) in rng g2 & g2/.(n+2) in rng g2 by PARTFUN2:4; then A115: g2/.n in lk & g2/.(n+1) in lk & g2/.(n+2) in lk by A90,A108; then consider u be Point of TOP-REAL 2 such that A116: g2/.n=u & u`1=ppi`1 & pj`2<=u`2 & u`2<=ppi`2; consider u1 be Point of TOP-REAL 2 such that A117: g2/.(n+1)=u1 & u1`1=ppi`1 & pj`2<=u1`2 & u1`2<=ppi`2 by A115; consider u2 be Point of TOP-REAL 2 such that A118: g2/.(n+2)=u2 & u2`1=ppi`1 & pj`2<=u2`2 & u2`2<=ppi`2 by A115; set lg = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & u2`2<=w`2 & w`2<=u`2}; A119: n+(1+1) = n+1+1 by XCMPLX_1:1; n+1 <= n+2 by AXIOMS:24; then n+1 <= len g2 by A113,AXIOMS:22; then A120: LSeg(g2,n)=LSeg(u,u1) by A113,A116,A117,TOPREAL1:def 5; 1 <= n+1 by NAT_1:29; then A121: LSeg(g2,n+1)=LSeg(u1,u2) by A113,A117,A118,A119,TOPREAL1:def 5; n<n+1 & n+1<n+1+1 & n+1+1=n+(1+1) by NAT_1:38,XCMPLX_1:1; then A122: u2`2<u1`2 & u1`2<u`2 by A104,A114,A116,A117,A118; then A123: u2`2<=u1`2 & u1`2<=u`2 & u2`2<u`2 by AXIOMS:22; A124: u1 in lg & u=|[u`1,u`2]| & u2=|[u2`1,u2`2]| by A117,A122,EUCLID :57; then LSeg(g2/.n,g2/.(n+2))=lg by A116,A118,A123,TOPREAL3:15; hence thesis by A116,A117,A118,A120,A121,A124,TOPREAL1:14; end; thus g is unfolded proof let n; assume A125: 1<=n & n+2 <= len g; then n+(1+1)<=len g; then A126: n+1+1<=len g by XCMPLX_1:1; A127: 1 <= n+1 by NAT_1:29; A128: n<=n+1 & n+1<=n+1+1 by NAT_1:29; then A129: n+1 <= len g by A126,AXIOMS:22; A130: n+(1+1)=n+1+1 by XCMPLX_1:1; A131: len g=len g1+len g2 by FINSEQ_1:35; n+2-len g1 = n-len g1 +2 by XCMPLX_1:29; then A132: n-len g1 + 2 <= len g2 by A125,A131,REAL_1:86; A133: n+1+1 = n+(1+1) by XCMPLX_1:1; per cases; suppose A134: n+2 <= len g1; then n in dom g1 & n+1 in dom g1 & n+2 in dom g1 & n+(1+1)=n+1+1 by A125,GOBOARD2:4,XCMPLX_1:1; then LSeg(g1,n)=LSeg(g,n) & LSeg(g1,n+1)=LSeg(g,n+1) & g/.(n+1)=g1/.(n+1) by GROUP_5:95,TOPREAL3:25; hence thesis by A30,A125,A134,TOPREAL1:def 8; suppose len g1 < n+2; then len g1+1<=n+2 by NAT_1:38; then len g1<=n+2-1 by REAL_1:84; then A135: len g1<=n+(1+1-1) by XCMPLX_1:29; now per cases; suppose A136: len g1=n+1; now assume A137: k=1; 1<len g1 by A125,A136,NAT_1:38; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A137,TOPREAL1:29; end; then A138: 1<k & LSeg(g1,n) c= L~f1 by A14,A33,REAL_1:def 5,TOPREAL3:26; then A139: L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,GOBOARD2:9; 1<=n+1 by NAT_1:29; then A140: n in dom g1 & n+1 in dom g1 by A125,A128,A136,FINSEQ_3:27; then A141: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; A142: g/.(n+1)=f1/.len f1 by A35,A136,A140,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; 1<=len g-len g1 by A126,A136,REAL_1:84; then A143: 1<=len g2 by A131,XCMPLX_1:26; then A144: g/.(n+2)=g2/.1 by A130,A136,GOBOARD2:5; 1 in dom g2 by A143,FINSEQ_3:27; then A145: g2/.1 in rng g2 by PARTFUN2:4; then g2/.1 in lk by A90,A108; then consider u1 be Point of TOP-REAL 2 such that A146: g2/.1=u1 & u1`1=ppi`1 & pj`2<=u1`2 & u1`2<=ppi`2; ppi in LSeg(ppi,pj) by TOPREAL1:6; then LSeg(ppi,u1) c= LSeg(f,k) & LSeg(g,n+1)=LSeg(ppi,u1) by A91,A108,A125,A127,A133,A142,A144,A145,A146,TOPREAL1:12,def 5; then A147: LSeg(g,n) /\ LSeg(g,n+1) c= {g/.(n+1)} by A47,A138,A139,A141,A142,XBOOLE_1:27; g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1) by A125,A127,A129,A133,TOPREAL1:27; then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by XBOOLE_0:def 3; then {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:37; hence thesis by A147,XBOOLE_0:def 10; suppose len g1<>n+1; then len g1<n+1 by A135,REAL_1:def 5; then A148: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; now per cases; suppose A149: len g1=n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A150: g/.n=f1/.len f1 by A35,A149,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; 1 <= len g2 by A129,A131,A149,REAL_1:53; then A151: g/.(n+1)=g2/.1 by A149,GOBOARD2:5; 2 <= len g2 by A125,A131,A149,REAL_1:53; then A152: g/.(n+2)=g2/.2 by A149,GOBOARD2:5; A153: 0+2<=len g2 by A125,A131,A149,REAL_1:53; then 1<=len g2 by AXIOMS:22; then A154: 1 in dom g2 & 2 in dom g2 by A153,FINSEQ_3:27; then g2/.1 in rng g2 & g2/.2 in rng g2 by PARTFUN2:4; then A155: g2/.1 in lk & g2/.2 in lk by A90,A108; then consider u1 be Point of TOP-REAL 2 such that A156: g2/.1=u1 & u1`1=ppi`1 & pj`2<=u1`2 & u1`2<=ppi`2; consider u2 be Point of TOP-REAL 2 such that A157: g2/.2=u2 & u2`1=ppi`1 & pj`2<=u2`2 & u2`2<=ppi`2 by A155; A158: u2`2<u1`2 by A104,A154,A156,A157; then A159: u2`2<=u1`2 & u2`2<ppi`2 & u2=|[u2`1,u2`2]| by A156,AXIOMS:22,EUCLID:57; set lg = {w where w is Point of TOP-REAL 2 : w`1=ppi`1 & u2`2<=w`2 & w`2<=ppi`2}; A160: u1 in lg by A156,A158; A161: LSeg(g,n)=LSeg(ppi,u1) by A125,A129,A150,A151,A156,TOPREAL1:def 5; A162: LSeg(g,n+1)=LSeg(u1,u2) by A125,A127,A133,A151,A152,A156,A157,TOPREAL1:def 5; LSeg(ppi,g2/.2)=lg by A89,A157,A159,TOPREAL3:15; hence thesis by A151,A156,A157,A160,A161,A162,TOPREAL1:14; suppose len g1<>n; then A163: len g1<n by A148,REAL_1:def 5; A164: n1 + len g1 = n by XCMPLX_1:27; then A165: LSeg(g,n)=LSeg(g2,n1) by A129,A163,GOBOARD2:10; A166: len g1<n+1 by A128,A163,AXIOMS:22; A167: len g1+1<=n by A163,NAT_1:38; A168: n+1 = (n1+len g1)+1 by XCMPLX_1:27 .= n1+1+len g1 by XCMPLX_1:1; A169: 1<=n1+1 by NAT_1:29; n1 + 1 + len g1 = n + 1 by A164,XCMPLX_1:1; then A170: n1+1 <= len g2 by A129,A131,REAL_1:53; A171: LSeg(g,n+1)=LSeg(g2,n1+1) by A126,A166,A168,GOBOARD2:10; A172: g/.(n+1)=g2/.(n1+1) by A168,A169,A170,GOBOARD2:5; 1<=n1 by A167,REAL_1:84; hence thesis by A112,A132,A165,A171,A172; end; hence thesis; end; hence thesis; end; for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m) proof let n,m; assume that A173: m>n+1 and A174: n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 and A175: LSeg(g2,n) /\ LSeg(g2,m) <> {}; A176: 1 <= n & n+1 <= len g2 & 1 <= m & m+1<= len g2 by A174,FINSEQ_3:27; reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lp = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & p2`2<=w`2 & w`2<=p1`2}, lq = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & q2`2<=w`2 & w`2<=q1`2}; m<m+1 & n<n+1 by NAT_1:38; then A177: p2`2<p1`2 & q2`2<q1`2 & p1`1=ppi`1 & p2`1=ppi`1 & q1`1= ppi`1 & q2`1=ppi`1 & p1=|[p1`1,p1`2]| & q1=|[q1`1,q1`2]| & p2=|[p2`1,p2`2]| & q2=|[q2`1,q2`2]| by A99,A104,A174,EUCLID:57; A178: LSeg(g2,n) = LSeg(p2,p1) by A176,TOPREAL1:def 5 .=lp by A177,TOPREAL3:15; A179: LSeg(g2,m) = LSeg(q2,q1) by A176,TOPREAL1:def 5 .=lq by A177,TOPREAL3:15; consider x being Element of LSeg(g2,n) /\ LSeg(g2,m); A180: x in LSeg(g2,n) & x in LSeg(g2,m) by A175,XBOOLE_0:def 3; then A181: ex tn be Point of TOP-REAL 2 st tn=x & tn`1=ppi`1 & p2`2<=tn`2 & tn`2<=p1`2 by A178; A182: ex tm be Point of TOP-REAL 2 st tm=x & tm`1=ppi`1 & q2`2<=tm`2 & tm`2<=q1`2 by A179,A180; q1`2<p2`2 by A104,A173,A174; hence contradiction by A181,A182,AXIOMS:22; end; then A183: g2 is s.n.c. by GOBOARD2:6; A184: L~g2 c= LSeg(f,k) proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; let x; assume x in L~g2; then x in union ls by TOPREAL1:def 6; then consider X be set such that A185: x in X & X in ls by TARSKI:def 4; consider m such that A186: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A185; m in dom g2 & m+1 in dom g2 by A186,GOBOARD2:3; then A187: g2/.m in rng g2 & g2/.(m+1) in rng g2 by PARTFUN2:4; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; A188: LSeg(q1,q2) c= LSeg(ppi,pj) by A91,A108,A187,TOPREAL1:12; LSeg(g2,m)=LSeg(q1,q2) by A186,TOPREAL1:def 5; hence thesis by A91,A185,A186,A188; end; A189: not f/.k in L~g2 proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; assume f/.k in L~g2; then f/.k in union ls by TOPREAL1:def 6; then consider X be set such that A190: f/.k in X & X in ls by TARSKI:def 4; consider m such that A191: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A190; A192: m in dom g2 & m+1 in dom g2 & m<m+1 by A191,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lq={w where w is Point of TOP-REAL 2: w`1=ppi`1 & q2`2<=w`2 & w`2<=q1`2}; A193: q1`1=ppi`1 & q2`1=ppi`1 & q2`2<q1`2 & q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by A99,A104,A192,EUCLID:57; LSeg(g2,m)=LSeg(q2,q1) by A191,TOPREAL1:def 5 .=lq by A193,TOPREAL3:15; then ex p st p=f/.k & p`1=ppi`1 & q2`2<=p`2 & p`2<=q1`2 by A190,A191 ; hence contradiction by A47,A99,A192; end; A194: L~g1 /\ L~g2 = {} proof per cases; suppose k=1; hence thesis by A37; suppose k<>1; then 1<k by A14,REAL_1:def 5; then L~g1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A33,GOBOARD2:9; then A195: L~g1 /\ L~g2 c= {f/.k} by A184,XBOOLE_1:26; now consider x being Element of L~g1 /\ L~g2; assume L~g1 /\ L~g2 <> {}; then x in {f/.k} & x in L~g2 by A195,TARSKI:def 3,XBOOLE_0:def 3 ; hence contradiction by A189,TARSKI:def 1; end; hence thesis; end; for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g & m+1 in dom g holds LSeg(g,n) misses LSeg(g,m) proof let n,m; assume that A196: m>n+1 and A197: n in dom g & n+1 in dom g & m in dom g & m+1 in dom g; A198: 1<=n & 1<=n+1 & n+1<=len g & 1<=m & 1<=m+1 & m+1<=len g & n<=n+1 & m<=m+1 & len g=len g1+len g2 by A197,FINSEQ_1:35,FINSEQ_3:27,NAT_1:29; set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j): 1<=j & j+1 <= len g2}; A199: L~g1=union l1 & L~g2=union l2 & n+1 <= len g & m+1 <= len g by A197,FINSEQ_3:27,TOPREAL1:def 6; j2+1<=i2 by A72,NAT_1:38; then A200: 1<=l by REAL_1:84; then A201: 1 in dom g2 by A76,FINSEQ_3:27; reconsider qq=g2/.1 as Point of TOP-REAL 2; set ql={z where z is Point of TOP-REAL 2: z`1=ppi`1 & qq`2<=z`2 & z`2<=ppi`2}; A202: 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 & dom g1 c= dom g by FINSEQ_1:39,FINSEQ_3:27; then A203: g/.len g1=g1/.len g1 by GROUP_5:95 .= ppi by A15,A16,A18,A35,A47,GOBOARD1:10; A204: len g1<len g1 +1 & len g1+1<=len g by A76,A198,A200,NAT_1:38,REAL_1:55; A205: g/.(len g1+1)=qq by A76,A200,GOBOARD2:5; A206: qq`1=ppi`1 & pj`2<=qq`2 & qq`2<ppi`2 & qq=|[qq`1,qq`2]| by A99,A201,EUCLID:57; A207: LSeg(g,len g1)=LSeg(qq,ppi) by A202,A203,A204,A205,TOPREAL1:def 5 .= ql by A89,A206,TOPREAL3:15; A208: n+1<=m+1 by A196,A198,AXIOMS:22; now per cases; suppose A209: m+1<=len g1; then A210: m<=len g1 & n+1<=len g1 by A198,A208,AXIOMS:22; then n<=len g1 by A198,AXIOMS:22; then n in dom g1 & n+1 in dom g1 & m in dom g1 & m+1 in dom g1 by A198,A209,A210,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) & LSeg(g,m)=LSeg(g1,m) by TOPREAL3:25; hence thesis by A31,A196,TOPREAL1:def 9; suppose len g1<m+1; then A211: len g1<=m by NAT_1:38; then reconsider m1=m-len g1 as Nat by INT_1:18; now per cases; suppose A212: m=len g1; now assume A213: k=1; 1<len g1 by A196,A198,A212,AXIOMS:22; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A213,TOPREAL1:29; end; then 1<k by A14,REAL_1:def 5; then A214: L~f1 /\ LSeg(f,k) ={f/.k} by A5,A8,A9,GOBOARD2:9; n<=len g1 by A196,A198,A212,AXIOMS:22; then A215: n in dom g1 & n+1 in dom g1 by A196,A198,A212,FINSEQ_3:27; then A216: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A196,A198,A212; then A217: LSeg(g,n) c= L~f1 by A33,A199,ZFMISC_1:92; LSeg(g,m) c= LSeg(f,k) proof let x; assume x in LSeg(g,m); then consider px be Point of TOP-REAL 2 such that A218: px=x & px`1=ppi`1 & qq`2<=px`2 & px`2<= ppi`2 by A207,A212; pj`2<=px`2 by A206,A218,AXIOMS:22; hence thesis by A90,A218; end; then A219: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A214,A217,XBOOLE_1:27; now consider x being Element of LSeg(g,n) /\ LSeg(g,m); assume LSeg(g,n)/\ LSeg(g,m)<>{}; then A220: x in LSeg(g,n) & x in {f/.k} by A219,TARSKI:def 3,XBOOLE_0:def 3; then A221: x=f/.k by TARSKI:def 1; f/.k=g1/.len g1 by A15,A16,A18,A35,GOBOARD1:10; hence contradiction by A29,A30,A31,A196,A212,A215,A216,A220,A221,GOBOARD2:7; end; hence thesis by XBOOLE_0:def 7; suppose A222: m<>len g1; m+1 = m1+len g1+1 by XCMPLX_1:27; then A223: len g1<m & m+1 = m1+1 +len g1 by A211,A222,REAL_1:def 5,XCMPLX_1:1; m = m1+len g1 by XCMPLX_1:27; then A224: LSeg(g,m)=LSeg(g2,m1) by A198,A223,GOBOARD2:10; m1+1<=len g2 & len g1+1<= m by A198,A223,NAT_1:38,REAL_1:53; then A225: 1<=m1 & m1+1 <= len g2 by REAL_1:84; then LSeg(g,m) in l2 by A224; then A226: LSeg(g,m) c= L~g2 by A199,ZFMISC_1:92; now per cases; suppose A227: n+1<=len g1; then n<=len g1 by A198,AXIOMS:22; then n in dom g1 & n+1 in dom g1 by A198,A227,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A198,A227; then LSeg(g,n) c= L~g1 by A199,ZFMISC_1:92; then LSeg(g,n) /\ LSeg(g,m) c= {} by A194,A226,XBOOLE_1:27; then LSeg(g,n) /\ LSeg(g,m) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; suppose len g1<n+1; then A228: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; A229: n - len g1 + 1 = n + 1 - len g1 by XCMPLX_1:29; A230: n = n1 + len g1 by XCMPLX_1:27; now per cases; suppose A231: len g1=n; now consider x being Element of LSeg(g,n) /\ LSeg(g,m); assume LSeg(g,n) /\ LSeg(g,m)<>{}; then A232: x in LSeg(g,n) & x in LSeg(g,m) by XBOOLE_0:def 3; then A233: ex qx be Point of TOP-REAL 2 st qx=x & qx`1=ppi`1 & qq`2<=qx`2 & qx`2<=ppi`2 by A207,A231; A234: m1 in dom g2 & m1+1 in dom g2 & m1<m1+1 by A225,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point of TOP-REAL 2; set q1l={v where v is Point of TOP-REAL 2: v`1=ppi`1 & q2`2<=v`2 & v`2<=q1`2}; A235: q1`1=ppi`1 & q2`1=ppi`1 & q2`2<q1`2 & q1=|[q1`1,q1`2]|& q2=|[q2`1,q2`2]| by A99,A104,A234,EUCLID:57; m1 > n1 + 1 & n1 + 1 >= 1 by A196,A229,NAT_1:29,REAL_1:54; then A236: m1 > 1 by AXIOMS:22; LSeg(g2,m1)=LSeg(q2,q1) by A225,TOPREAL1:def 5 .=q1l by A235,TOPREAL3:15; then A237: ex qy be Point of TOP-REAL 2 st qy=x & qy`1=ppi`1 & q2`2<=qy`2 & qy`2<=q1`2 by A224,A232; q1`2 < qq`2 by A104,A201,A234,A236; hence contradiction by A233,A237,AXIOMS:22; end; hence thesis by XBOOLE_0:def 7; suppose n<>len g1; then len g1<n by A228,REAL_1:def 5; then LSeg(g,n)=LSeg(g2,n1) & m1>n1+1 by A196,A198,A229,A230,GOBOARD2:10,REAL_1:54; hence thesis by A183,A224,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; hence thesis; end; hence thesis; end; hence g is s.n.c. by GOBOARD2:6; A238: g2 is special proof let n; set p = g2/.n, q = g2/.(n+1); assume 1<=n & n+1 <= len g2; then n in dom g2 & n+1 in dom g2 by GOBOARD2:3; then p`1=ppi`1 & q`1=ppi`1 by A99; hence p`1=q`1 or p`2=q`2; end; now set p=g1/.len g1, q=g2/.1; j2+1<=i2 by A72,NAT_1:38; then 1<=l by REAL_1:84; then 1 in dom g2 by A77,FINSEQ_1:3; then q`1=ppi`1 by A99; hence p`1=q`1 or p`2=q`2 by A15,A16,A18,A35,A47,GOBOARD1:10; end; hence g is special by A32,A238,GOBOARD2:13; 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}; A239: len g = len g1 + len g2 by FINSEQ_1:35; A240: now let j; assume A241: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A242: p=g/.j; now per cases; suppose A243: j=len g1; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A244: g/.len g1 = f1/.len f1 by A35,GROUP_5:95 .= G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence p`1=G*(i1,i2)`1 by A242,A243; thus G*(i1,j2)`2<=p`2 & p`2<=G*(i1,i2)`2 by A51,A55,A59,A60,A62, A72,A88,A242,A243,A244,GOBOARD1:def 1; dom l1 = Seg len l1 by FINSEQ_1:def 3; hence p in rng l1 by A51,A62,A87,A242,A243,A244,PARTFUN2:4; suppose j<>len g1; then len g1 < j by A241,REAL_1:def 5; then len g1 + 1<=j by NAT_1:38; then A245: 1<=w & w<=len g2 by A239,A241,REAL_1:84,86; w + len g1 = j by XCMPLX_1:27; then A246: g/.j=g2/.w by A245,GOBOARD2:5; w in dom g2 by A245,FINSEQ_3:27; hence p`1=ppi`1 & pj`2<=p`2 & p`2<= ppi`2 & p in rng l1 by A99,A242,A246; 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 A247: x in X & X in lg by TARSKI:def 4; consider i such that A248: X=LSeg(g,i) & 1<=i & i+1 <= len g by A247; per cases; suppose A249: 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 A248,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A248,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A248,A249; then x in union {LSeg(g1,j): 1<=j & j+1 <= len g1} by A247,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A33,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A250: i+1 > len g1; then A251: len g1<=i & i<=i+1 & i+1<=len g by A248,NAT_1:38; A252: 1<=i+1 & len g1<=i+1 & i<=len g by A248,A250,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A253: 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 A240,A251,A252; then A254: q1=|[q1`1,q1`2]| & q2=|[q1`1,q2`2]| by EUCLID:57; A255: LSeg(g,i)=LSeg(q2,q1) by A248,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 A254,A255,TOPREAL3:15; then consider p2 such that A256: p2=x & p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1`2 by A247,A248; pj`2<=p2`2 & p2`2<=ppi`2 by A253,A256,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A90,A253,A256; 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 A254,A255,TOPREAL1:7; then x=q1 by A247,A248,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A90,A253; 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 A254,A255,TOPREAL3:15; then consider p2 such that A257: p2=x & p2`1=q1`1 & q1`2<=p2`2 & p2`2<=q2`2 by A247,A248; pj`2<=p2`2 & p2`2<=ppi`2 by A253,A257,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A90,A253,A257; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; let x; assume x in L~f; then A258: x in L~f1 \/ LSeg(f,k) by A5,A12,GOBOARD2:8; per cases by A258,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A33,GOBOARD2:11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A259: p1=x & p1`1=ppi`1 & pj`2<=p1`2 & p1`2<=ppi`2 by A90; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`2>=p1`2; A260: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A239,REAL_2:173; let q such that A261: q=g/.n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A35,A261,GROUP_5:95 .=G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence p1`2<=q`2 by A259; end; end; A262: for n holds P2[n] implies n<=len g; consider ma be Nat such that A263: P2[ma] & for n st P2[n] holds n<=ma from Max(A262,A260); now per cases; suppose A264: ma=len g; j2+1<=i2 by A72,NAT_1:38; then A265: 1<=l & l=len g2 by A76,REAL_1:84; then A266: l in dom g2 & i2-l=j2 by FINSEQ_3:27,XCMPLX_1:18; then A267: g/.ma=g2/.l by A76,A239,A264,GROUP_5:96 .= pj by A76,A77,A266; then p1`2<=pj`2 by A263; then A268: p1`2=pj`2 by A259,AXIOMS:21; A269: ma-1<=len g & len g1+1<=ma by A239,A264,A265,PROB_1:2,REAL_1:55; then A270: len g1<=ma-1 & 0<=len g1 by NAT_1:18,REAL_1:84; then A271: 0+1<=ma by REAL_1:84; then A272: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A271,INT_1:18; 1<=len g1 by A14,A16,A36,AXIOMS:22; then A273: 1<=m1 by A270,AXIOMS:22; then A274: m1 in dom g & dom g=Seg len g by A269,FINSEQ_1:def 3,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A275: q`1=ppi`1 & pj`2<=q`2 & q=|[q`1,q`2]| & m1+1=ma by A240,A269,A270,EUCLID:57,XCMPLX_1:27; then A276: LSeg(g,m1)=LSeg(pj,q) by A264,A267,A273,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 A49,A53,A71,A80,A84,A89,A264,A267,A272,A274,A275,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 A275,REAL_1:def 5; then LSeg(g,m1)=lq by A89,A275,A276,TOPREAL3:15; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A259,A264,A268,A273,A275; then x in union lg by A259,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A263,REAL_1:def 5; then A277: ma+1<=len g & k<=ma & ma<=ma+1 by A16,A36,A263,AXIOMS:22,NAT_1:38; then A278: 1<=ma & len g1<=ma+1 by A14,A263,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A279: p1`2<=qa`2 by A263; A280: now assume p1`2<=qa1`2; then for q holds q=g/.(ma+1) implies p1`2<=q`2; then ma+1<=ma by A263,A277,A278; hence contradiction by REAL_2:174; end; then A281: qa1`2<qa`2 & qa1`2<=p1`2 & p1`2<=qa`2 & qa`1=ppi`1 & qa1 `1 = ppi`1 by A240,A263,A277,A278,A279,AXIOMS:22; set lma = {p2: p2`1=ppi`1 & qa1`2<=p2`2 & p2`2<=qa`2}; A282: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa1,qa) by A277,A278,TOPREAL1:def 5 .= lma by A281,A282,TOPREAL3:15; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A259,A277,A278,A279, A280; 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; 1<=len g1 by A14,A16,A36,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A34,GROUP_5:95 .=f/.1 by A15,A19,GOBOARD1:10; j2+1<=i2 by A72,NAT_1:38; then A283: 1<=l by REAL_1:84; then A284: l in dom g2 & len g=len g1 + len g2 & len g2 = l by A77,FINSEQ_1:3,35,def 3; then reconsider m1=i2-l as Nat by A73,A77; thus g/.len g=g2/.l by A284,GROUP_5:96 .=G*(i1,m1) by A76,A77,A284 .=f/.len f by A5,A49,A71,XCMPLX_1:18; thus len f<=len g by A5,A16,A36,A283,A284,REAL_1:55; case A285: i2=j2; k<>k+1 by NAT_1:38; hence contradiction by A7,A15,A47,A48,A49,A71,A285,PARTFUN2:17; case A286: i2<j2; then reconsider l=j2-i2 as Nat by INT_1:18; deffunc F(Nat) = G*(i1,i2+$1); consider g2 such that A287: len g2=l & for n st n in dom g2 holds g2/.n=F(n) from PiLambdaD; take g=g1^g2; A288: now let n; assume n in Seg l; then A289: 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 A51,FINSEQ_1:3,XCMPLX_1:27; then 1<=i2+n & i2+n<=width G by A289,AXIOMS:22; hence i2+n in Seg width G by FINSEQ_1:3; hence [i1,i2+n] in Indices G by A50,A51,ZFMISC_1:106; end; A290: dom g2 = Seg len g2 by FINSEQ_1:def 3; now let n such that A291: n in dom g2; take m=i1,k=i2+n; thus [m,k] in Indices G & g2/.n=G*(m,k) by A287,A288,A290,A291; end; then A292: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A53,GOBOARD1:39; A293: now let n; assume n in dom g2 & n+1 in dom g2; then A294: 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 A287,A288,A290; 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) by A294,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; A295: now let l1,l2,l3,l4 be Nat; assume A296: [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 A15,A16,A18,A287,A288,A290,GOBOARD1:10; then l1=i1 & l2=i2 & l3=i1 & l4=i2+1 by A35,A47,A296,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 A53,A293,GOBOARD1:40; hence g is_sequence_on G by A292,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}; l1/.i2=l1.i2 & l1/.j2=l1.j2 by A51,A63,FINSEQ_4:def 4; then A297: l1/.i2=ppi & l1/.j2=pj by A51,MATRIX_1:def 8; then A298: y1.i2=ppi`2 & y1.j2=pj`2 & x1.i2=ppi`1 & x1.j2=pj`1 by A51,A58,A59,A60,A61,A62,GOBOARD1:def 3,def 4; then A299: ppi`2<pj`2 & ppi`1=pj`1 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj `2]| by A51,A54,A55,A58,A59,A60,A61,A62,A286,EUCLID:57,GOBOARD1:def 1,def 2; A300: LSeg(f,k)=LSeg(ppi,pj) by A14,A47,A49,A71,TOPREAL1:def 5 .= lk by A299,TOPREAL3:15; A301: LSeg(f,k)=LSeg(ppi,pj) by A14,A47,A49,A71,TOPREAL1:def 5; now let n,m; assume A302: n in dom g2 & m in dom g2 & n<>m; then A303: g2/.n=G*(i1,i2+n) & g2/.m=G*(i1,i2+m) & [i1,i2+n] in Indices G & [i1,i2+m] in Indices G by A287,A288,A290; assume g2/.n=g2/.m; then i2+n=i2+m by A303,GOBOARD1:21; hence contradiction by A302,XCMPLX_1:2; end; then for n,m st n in dom g2 & m in dom g2 & g2/.n = g2/.m holds n = m; then A304: g2 is one-to-one by PARTFUN2:16; A305: not f/.k in rng g2 proof assume f/.k in rng g2; then consider n such that A306: n in dom g2 & g2/.n=f/.k by PARTFUN2:4; dom g2 = Seg len g2 by FINSEQ_1:def 3; then A307: g2/.n=G*(i1,i2+n) & [i1,i2+n] in Indices G by A287,A288,A306; 0+1<=n by A306,FINSEQ_3:27; then i2+n=i2 & 0<n by A47,A306,A307,GOBOARD1:21,NAT_1:38; hence contradiction by XCMPLX_1:3; end; A308: now let n,p; assume A309: n in dom g2 & g2/.n=p; then A310: g2/.n=G*(i1,i2+n) & 1<=n & n<=len g2 & i2+n in Seg width G by A287,A288,A290,FINSEQ_1:3; set n1=i2+n; set pn = G*(i1,n1); l1/.n1=l1.n1 by A63,A310,FINSEQ_4:def 4; then A311: g2/.n=pn & l1/.n1=pn & 0<=n & n1<=i2+len g2 by A310,AXIOMS:22,MATRIX_1:def 8,REAL_1:55; then A312: x1.n1=pn`1 & x1.n1=x1.i2 & y1.n1=pn`2 & n1<=j2 & i2<=n1 by A51,A54,A58,A59,A60,A61,A62,A287,A310,GOBOARD1:def 2,def 3,def 4, REAL_2:173,XCMPLX_1:27; hence p`1=ppi`1 & ppi`2<=p`2 & p`2<=pj`2 by A51,A55,A59,A60,A62,A298,A309,A310,GOBOARD2:18; dom l1 = Seg len l1 by FINSEQ_1:def 3; hence p in rng l1 by A62,A309,A310,A311,PARTFUN2:4; 0<n by A310,AXIOMS:22; then i2<n1 by REAL_2:174; hence p`2>ppi`2 by A51,A55,A59,A60,A62,A298,A309,A310,A312,GOBOARD1: def 1; end; A313: now let n,m,p,q; assume A314: n in dom g2 & m in dom g2 & n<m & g2/.n=p & g2/.m=q; then A315: g2/.n=G*(i1,i2+n) & i2+n in Seg width G & g2/.m=G*(i1,i2+m) & i2+m in Seg width G by A287,A288,A290; set n1=i2+n, m1=i2+m; set pn = G*(i1,n1), pm = G*(i1,m1); l1/.n1=l1.n1 & l1/.m1 = l1.m1 by A63,A315,FINSEQ_4:def 4; then A316: l1/.n1=pn & l1/.m1=pm & n1<m1 by A314,A315,MATRIX_1:def 8,REAL_1:67; then y1.n1=pn`2 & y1.m1=pm`2 by A59,A60,A62,A315,GOBOARD1:def 4; hence p`2<q`2 by A55,A59,A60,A62,A314,A315,A316,GOBOARD1:def 1; end; A317: rng g2 c= LSeg(f,k) proof let x; assume x in rng g2; then consider n such that A318: n in dom g2 & g2/.n=x by PARTFUN2:4; A319: g2/.n=G*(i1,i2+n) by A287,A318; set pn = G*(i1,(i2+n)); pn`1=ppi`1 & ppi`2<=pn`2 & pn`2<=pj`2 by A308,A318,A319; hence x in LSeg(f,k) by A300,A318,A319; end; rng g1 /\ rng g2 = {} proof consider x being Element of rng g1 /\ rng g2; assume not thesis; then A320: x in rng g1 & x in rng g2 by XBOOLE_0:def 3; now per cases by A14,REAL_1:def 5; suppose k=1; hence contradiction by A37,A305,A320,TARSKI:def 1; suppose 1<k; then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A44,A317,A320,GOBOARD2:9,XBOOLE_0:def 3; hence contradiction by A305,A320,TARSKI:def 1; end; hence contradiction; end; then rng g1 misses rng g2 by XBOOLE_0:def 7; hence g is one-to-one by A29,A304,FINSEQ_3:98; A321: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2,n+1) = {g2/.(n+1)} proof let n; assume A322: 1<=n & n+2 <= len g2; then A323: n in dom g2 & n+1 in dom g2 & n+2 in dom g2 by GOBOARD2:4; then g2/.n in rng g2 & g2/.(n+1) in rng g2 & g2/.(n+2) in rng g2 by PARTFUN2:4; then A324: g2/.n in lk & g2/.(n+1) in lk & g2/.(n+2) in lk by A300,A317; then consider u be Point of TOP-REAL 2 such that A325: g2/.n=u & u`1=ppi`1 & ppi`2<=u`2 & u`2<=pj`2; consider u1 be Point of TOP-REAL 2 such that A326: g2/.(n+1)=u1 & u1`1=ppi`1 & ppi`2<=u1`2 & u1`2<=pj`2 by A324; consider u2 be Point of TOP-REAL 2 such that A327: g2/.(n+2)=u2 & u2`1=ppi`1 & ppi`2<=u2`2 & u2`2<=pj`2 by A324; set lg = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & u`2<=w`2 & w`2<=u2`2}; A328: 1<= n+1 by NAT_1:29; A329: n+1+1 = n+(1+1) by XCMPLX_1:1; n+1 <= n+2 by AXIOMS:24; then n+1 <= len g2 by A322,AXIOMS:22; then A330: LSeg(g2,n)=LSeg(u,u1) & LSeg(g2,n+1)=LSeg(u1,u2) & LSeg(g2/.n,g2/.(n+2))=LSeg(u,u2) by A322,A325,A326,A327,A328,A329,TOPREAL1:def 5; n<n+1 & n+1<n+1+1 & n+1+1=n+(1+1) by NAT_1:38,XCMPLX_1:1; then A331: u1`2<u2`2 & u`2<u1`2 by A313,A323,A325,A326,A327; then A332: u1`2<=u2`2 & u`2<=u1`2 & u`2<u2`2 by AXIOMS:22; A333: u1 in lg & u=|[u`1,u`2]| & u2=|[u2`1,u2`2]| by A326,A331,EUCLID :57; then LSeg(g2/.n,g2/.(n+2))=lg by A325,A327,A332,TOPREAL3:15; hence thesis by A326,A330,A333,TOPREAL1:14; end; thus g is unfolded proof let n; assume A334: 1<=n & n+2 <= len g; then n+(1+1)<=len g; then A335: n+1+1<=len g by XCMPLX_1:1; A336: 1<= n+1 by NAT_1:29; A337: n<=n+1 & n+1<=n+1+1 by NAT_1:29; then A338: n+1 <= len g by A335,AXIOMS:22; A339: n+(1+1)=n+1+1 by XCMPLX_1:1; A340: len g=len g1+len g2 by FINSEQ_1:35; n+2-len g1 = n-len g1 +2 by XCMPLX_1:29; then A341: n-len g1 + 2 <= len g2 by A334,A340,REAL_1:86; per cases; suppose A342: n+2 <= len g1; then n in dom g1 & n+1 in dom g1 & n+2 in dom g1 & n+(1+1)=n+1+1 by A334,GOBOARD2:4,XCMPLX_1:1; then LSeg(g1,n)=LSeg(g,n) & LSeg(g1,n+1)=LSeg(g,n+1) & g/.(n+1)=g1/.(n+1) by GROUP_5:95,TOPREAL3:25; hence thesis by A30,A334,A342,TOPREAL1:def 8; suppose len g1 < n+2; then len g1+1<=n+2 by NAT_1:38; then len g1<=n+2-1 by REAL_1:84; then A343: len g1<=n+(1+1-1) by XCMPLX_1:29; now per cases; suppose A344: len g1=n+1; now assume A345: k=1; 1<len g1 by A334,A344,NAT_1:38; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A345,TOPREAL1:29; end; then A346: 1<k & LSeg(g1,n) c= L~f1 by A14,A33,REAL_1:def 5,TOPREAL3:26; then A347: L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,GOBOARD2:9; 1<=n+1 by NAT_1:29; then A348: n in dom g1 & n+1 in dom g1 by A334,A337,A344,FINSEQ_3:27; then A349: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; A350: g/.(n+1)=f1/.len f1 by A35,A344,A348,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; 1<=len g-len g1 by A335,A344,REAL_1:84; then A351: 1 <= len g2 by A340,XCMPLX_1:26; then A352: g/.(n+2)=g2/.1 by A339,A344,GOBOARD2:5; 1 in dom g2 by A351,FINSEQ_3:27; then A353: g2/.1 in rng g2 by PARTFUN2:4; then g2/.1 in lk by A300,A317; then consider u1 be Point of TOP-REAL 2 such that A354: g2/.1=u1 & u1`1=ppi`1 & ppi`2<=u1`2 & u1`2<=pj`2; ppi in LSeg(ppi,pj) by TOPREAL1:6; then LSeg(ppi,u1) c= LSeg(f,k) & LSeg(g,n+1)=LSeg(ppi,u1) by A301,A317,A334,A336,A339,A350,A352,A353,A354,TOPREAL1:12,def 5; then A355: LSeg(g,n) /\ LSeg(g,n+1) c= {g/.(n+1)} by A47,A346,A347,A349,A350,XBOOLE_1:27; g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1) by A334,A336,A338,A339,TOPREAL1:27; then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by XBOOLE_0:def 3; then {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:37; hence thesis by A355,XBOOLE_0:def 10; suppose len g1<>n+1; then len g1<n+1 by A343,REAL_1:def 5; then A356: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; now per cases; suppose A357: len g1=n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A358: g/.n=f1/.len f1 by A35,A357,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; A359: 2 <= len g2 by A334,A340,A357,REAL_1:53; then 1 <= len g2 by AXIOMS:22; then A360: g/.(n+1)=g2/.1 by A357,GOBOARD2:5; A361: g/.(n+2)=g2/.2 by A357,A359,GOBOARD2:5; 1<=len g2 by A359,AXIOMS:22; then A362: 1 in dom g2 & 2 in dom g2 by A359,FINSEQ_3:27; then g2/.1 in rng g2 & g2/.2 in rng g2 by PARTFUN2:4; then A363: g2/.1 in lk & g2/.2 in lk by A300,A317; then consider u1 be Point of TOP-REAL 2 such that A364: g2/.1=u1 & u1`1=ppi`1 & ppi`2<=u1`2 & u1`2<=pj`2; consider u2 be Point of TOP-REAL 2 such that A365: g2/.2=u2 & u2`1=ppi`1 & ppi`2<=u2`2 & u2`2<=pj`2 by A363; A366: u1`2<u2`2 by A313,A362,A364,A365; then A367: u1`2<=u2`2 & ppi`2<u2`2 & u2=|[u2`1,u2`2]| by A364,AXIOMS:22,EUCLID:57; set lg = {w where w is Point of TOP-REAL 2 : w`1=ppi`1 & ppi`2<=w`2 & w`2<=u2`2}; A368: u1 in lg by A364,A366; A369: LSeg(g,n)=LSeg(ppi,u1) & LSeg(g,n+1)=LSeg(u1,u2) by A334,A336,A338,A339,A358,A360,A361,A364,A365,TOPREAL1:def 5; u1 in LSeg(ppi,u2) by A299,A365,A367,A368,TOPREAL3:15; hence thesis by A360,A364,A369,TOPREAL1:14; suppose len g1<>n; then A370: len g1<n by A356,REAL_1:def 5; n1 + len g1 = n by XCMPLX_1:27; then A371: LSeg(g,n)=LSeg(g2,n1) by A338,A370,GOBOARD2:10; A372: len g1<n+1 by A337,A370,AXIOMS:22; A373: len g1+1<=n by A370,NAT_1:38; A374: n1+1+len g1 = n1+len g1+1 by XCMPLX_1:1 .= n+1 by XCMPLX_1:27; A375: 1<=n1+1 by NAT_1:29; n1+1<=len g2 by A338,A340,A374,REAL_1:53; then LSeg(g,n+1)=LSeg(g2,n1+1)& g/.(n+1)=g2/.(n1+1) & 1<=n1 by A335,A372,A373,A374,A375,GOBOARD2:5,10,REAL_1:84; hence thesis by A321,A341,A371; end; hence thesis; end; hence thesis; end; for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m) proof let n,m; assume that A376: m>n+1 and A377: n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 and A378: LSeg(g2,n) /\ LSeg(g2,m) <> {}; A379: 1 <= n & n+1 <= len g2 & 1 <= m & m+1<= len g2 by A377,FINSEQ_3:27; reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lp = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & p1`2<=w`2 & w`2<=p2`2}, lq = {w where w is Point of TOP-REAL 2: w`1=ppi`1 & q1`2<=w`2 & w`2<=q2`2}; m<m+1 & n<n+1 by NAT_1:38; then A380: p1`2<p2`2 & q1`2<q2`2 & p1`1=ppi`1 & p2`1=ppi`1 & q1`1= ppi`1 & q2`1=ppi`1 & p1=|[p1`1,p1`2]| & q1=|[q1`1,q1`2]| & p2=|[p2`1,p2`2]| & q2=|[q2`1,q2`2]| by A308,A313,A377,EUCLID:57; A381: LSeg(g2,n) = LSeg(p1,p2) by A379,TOPREAL1:def 5 .=lp by A380,TOPREAL3:15; A382: LSeg(g2,m) = LSeg(q1,q2) by A379,TOPREAL1:def 5 .=lq by A380,TOPREAL3:15; consider x being Element of LSeg(g2,n) /\ LSeg(g2,m); A383: x in LSeg(g2,n) & x in LSeg(g2,m) by A378,XBOOLE_0:def 3; then A384: ex tn be Point of TOP-REAL 2 st tn=x & tn`1=ppi`1 & p1`2<=tn`2 & tn`2<=p2`2 by A381; A385: ex tm be Point of TOP-REAL 2 st tm=x & tm`1=ppi`1 & q1`2<=tm`2 & tm`2<=q2`2 by A382,A383; p2`2<q1`2 by A313,A376,A377; hence contradiction by A384,A385,AXIOMS:22; end; then A386: g2 is s.n.c. by GOBOARD2:6; A387: L~g2 c= LSeg(f,k) proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; let x; assume x in L~g2; then x in union ls by TOPREAL1:def 6; then consider X be set such that A388: x in X & X in ls by TARSKI:def 4; consider m such that A389: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A388; m in dom g2 & m+1 in dom g2 by A389,GOBOARD2:3; then A390: g2/.m in rng g2 & g2/.(m+1) in rng g2 by PARTFUN2:4; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; A391: LSeg(q1,q2) c= LSeg(ppi,pj) by A301,A317,A390,TOPREAL1:12; LSeg(g2,m)=LSeg(q1,q2) by A389,TOPREAL1:def 5; hence thesis by A301,A388,A389,A391; end; A392: not f/.k in L~g2 proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; assume f/.k in L~g2; then f/.k in union ls by TOPREAL1:def 6; then consider X be set such that A393: f/.k in X & X in ls by TARSKI:def 4; consider m such that A394: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A393; A395: m in dom g2 & m+1 in dom g2 & m<m+1 by A394,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lq={w where w is Point of TOP-REAL 2: w`1=ppi`1 & q1`2<=w`2 & w`2<=q2`2}; A396: q1`1=ppi`1 & q2`1=ppi`1 & q1`2<q2`2 & q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by A308,A313,A395,EUCLID:57; LSeg(g2,m)=LSeg(q1,q2) by A394,TOPREAL1:def 5 .=lq by A396,TOPREAL3:15; then ex p st p=f/.k & p`1=ppi`1 & q1`2<=p`2 & p`2<=q2`2 by A393,A394 ; hence contradiction by A47,A308,A395; end; A397: L~g1 /\ L~g2 = {} proof per cases; suppose k=1; hence thesis by A37; suppose k<>1; then 1<k by A14,REAL_1:def 5; then L~g1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A33,GOBOARD2:9; then A398: L~g1 /\ L~g2 c= {f/.k} by A387,XBOOLE_1:26; now consider x being Element of L~g1 /\ L~g2; assume L~g1 /\ L~g2 <> {}; then x in {f/.k} & x in L~g2 by A398,TARSKI:def 3,XBOOLE_0:def 3 ; hence contradiction by A392,TARSKI:def 1; end; hence thesis; end; for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g & m+1 in dom g holds LSeg(g,n) misses LSeg(g,m) proof let n,m; assume that A399: m>n+1 and A400: n in dom g & n+1 in dom g & m in dom g & m+1 in dom g; A401: 1<=n & 1<=n+1 & n+1<=len g & 1<=m & 1<=m+1 & m+1<=len g & n<=n+1 & m<=m+1 & len g=len g1+len g2 by A400,FINSEQ_1:35,FINSEQ_3:27,NAT_1:29; set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j): 1<=j & j+1 <= len g2}; A402: L~g1=union l1 & L~g2=union l2 & n+1 <= len g & m+1 <= len g by A400,FINSEQ_3:27,TOPREAL1:def 6; i2+1<=j2 by A286,NAT_1:38; then A403: 1<=l by REAL_1:84; then A404: 1 in dom g2 by A287,FINSEQ_3:27; reconsider qq=g2/.1 as Point of TOP-REAL 2; set ql={z where z is Point of TOP-REAL 2: z`1=ppi`1 & ppi`2<=z`2 & z`2<=qq`2}; A405: 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 & dom g1 c= dom g by FINSEQ_1:39,FINSEQ_3:27; then A406: g/.len g1=g1/.len g1 by GROUP_5:95 .= ppi by A15,A16,A18,A35,A47,GOBOARD1:10; A407: len g1<len g1 +1 & len g1+1<=len g by A287,A401,A403,NAT_1:38,REAL_1:55; A408: g/.(len g1+1)=qq by A287,A403,GOBOARD2:5; A409: qq`1=ppi`1 & qq`2<=pj`2 & qq`2>ppi`2 & qq=|[qq`1,qq`2]| by A308,A404,EUCLID:57; A410: LSeg(g,len g1)=LSeg(ppi,qq) by A405,A406,A407,A408,TOPREAL1:def 5 .= ql by A299,A409,TOPREAL3:15; A411: n+1<=m+1 by A399,A401,AXIOMS:22; now per cases; suppose A412: m+1<=len g1; then A413: m<=len g1 & n+1<=len g1 by A401,A411,AXIOMS:22; then n<=len g1 by A401,AXIOMS:22; then n in dom g1 & n+1 in dom g1 & m in dom g1 & m+1 in dom g1 by A401,A412,A413,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) & LSeg(g,m)=LSeg(g1,m) by TOPREAL3:25; hence thesis by A31,A399,TOPREAL1:def 9; suppose len g1<m+1; then A414: len g1<=m by NAT_1:38; then reconsider m1=m-len g1 as Nat by INT_1:18; now per cases; suppose A415: m=len g1; now assume A416: k=1; 1<len g1 by A399,A401,A415,AXIOMS:22; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A416,TOPREAL1:29; end; then 1<k by A14,REAL_1:def 5; then A417: L~f1 /\ LSeg(f,k) ={f/.k} by A5,A8,A9,GOBOARD2:9; n<=len g1 by A399,A401,A415,AXIOMS:22; then A418: n in dom g1 & n+1 in dom g1 by A399,A401,A415,FINSEQ_3:27; then A419: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A399,A401,A415; then A420: LSeg(g,n) c= L~f1 by A33,A402,ZFMISC_1:92; LSeg(g,m) c= LSeg(f,k) proof let x; assume x in LSeg(g,m); then consider px be Point of TOP-REAL 2 such that A421: px=x & px`1=ppi`1 & ppi`2<=px`2 & px`2<= qq`2 by A410,A415; pj`2>=px`2 by A409,A421,AXIOMS:22; hence thesis by A300,A421; end; then A422: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A417,A420,XBOOLE_1:27; now consider x being Element of LSeg(g,n)/\ LSeg(g,m); assume LSeg(g,n)/\ LSeg(g,m)<>{}; then A423: x in LSeg(g,n) & x in {f/.k} by A422,TARSKI:def 3,XBOOLE_0:def 3; then A424: x=f/.k by TARSKI:def 1; f/.k=g1/.len g1 by A15,A16,A18,A35,GOBOARD1:10; hence contradiction by A29,A30,A31,A399,A415,A418,A419,A423, A424,GOBOARD2:7; end; hence thesis by XBOOLE_0:def 7; suppose A425: m<>len g1; m+1 = m1+len g1+1 by XCMPLX_1:27; then A426: len g1<m & m+1=m1+1+len g1 by A414,A425,REAL_1:def 5,XCMPLX_1:1; m = m1+len g1 by XCMPLX_1:27; then A427: LSeg(g,m)=LSeg(g2,m1) by A401,A426,GOBOARD2:10; m1+1<=len g2 & len g1+1<= m by A401,A426,NAT_1:38,REAL_1:53; then A428: 1<=m1 & m1+1 <= len g2 by REAL_1:84; then LSeg(g,m) in l2 by A427; then A429: LSeg(g,m) c= L~g2 by A402,ZFMISC_1:92; now per cases; suppose A430: n+1<=len g1; then n<=len g1 by A401,AXIOMS:22; then n in dom g1 & n+1 in dom g1 by A401,A430,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A401,A430; then LSeg(g,n) c= L~g1 by A402,ZFMISC_1:92; then LSeg(g,n) /\ LSeg(g,m) c= {} by A397,A429,XBOOLE_1:27; then LSeg(g,n) /\ LSeg(g,m) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; suppose len g1<n+1; then A431: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; A432: n - len g1 + 1 = n + 1 - len g1 by XCMPLX_1:29; A433: n = n1 + len g1 by XCMPLX_1:27; now per cases; suppose A434: len g1=n; now consider x being Element of LSeg(g,n) /\ LSeg(g,m); assume LSeg(g,n) /\ LSeg(g,m)<>{}; then A435: x in LSeg(g,n) & x in LSeg(g,m) by XBOOLE_0:def 3; then A436: ex qx be Point of TOP-REAL 2 st qx=x & qx`1=ppi`1 & ppi`2<=qx`2 & qx`2<=qq`2 by A410,A434; A437: m1 in dom g2 & m1+1 in dom g2 & m1<m1+1 by A428,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point of TOP-REAL 2; set q1l={v where v is Point of TOP-REAL 2: v`1=ppi`1 & q1`2<=v`2 & v`2<=q2`2}; A438: q1`1=ppi`1 & q2`1=ppi`1 & q1`2<q2`2 & q1=|[q1`1,q1`2]|& q2=|[q2`1,q2`2]| by A308,A313,A437,EUCLID:57; m1 > n1 + 1 & n1 + 1 >= 1 by A399,A432,NAT_1:29,REAL_1:54; then A439: m1 > 1 by AXIOMS:22; LSeg(g2,m1)=LSeg(q1,q2) by A428,TOPREAL1:def 5 .=q1l by A438,TOPREAL3:15; then A440: ex qy be Point of TOP-REAL 2 st qy=x & qy`1=ppi`1 & q1`2<=qy`2 & qy`2<=q2`2 by A427,A435; qq`2 < q1`2 by A313,A404,A437,A439; hence contradiction by A436,A440,AXIOMS:22; end; hence thesis by XBOOLE_0:def 7; suppose n<>len g1; then len g1<n by A431,REAL_1:def 5; then LSeg(g,n)=LSeg(g2,n1) & m1>n1+1 by A399,A401,A432,A433,GOBOARD2:10,REAL_1:54; hence thesis by A386,A427,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; hence thesis; end; hence thesis; end; hence g is s.n.c. by GOBOARD2:6; A441: g2 is special proof let n; set p = g2/.n, q = g2/.(n+1); assume 1<=n & n+1 <= len g2; then n in dom g2 & n+1 in dom g2 by GOBOARD2:3; then p`1=ppi`1 & q`1=ppi`1 by A308; hence p`1=q`1 or p`2=q`2; end; now set p=g1/.len g1, q=g2/.1; i2+1<=j2 by A286,NAT_1:38; then 1<=l by REAL_1:84; then 1 in dom g2 by A287,FINSEQ_3:27; then q`1=ppi`1 by A308; hence p`1=q`1 or p`2=q`2 by A15,A16,A18,A35,A47,GOBOARD1:10; end; hence g is special by A32,A441,GOBOARD2:13; 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}; A442: len g = len g1 + len g2 by FINSEQ_1:35; A443: now let j; assume A444: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A445: p=g/.j; per cases; suppose A446: j=len g1; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A447: g/.len g1 = f1/.len f1 by A35,GROUP_5:95 .= G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence p`1=G*(i1,i2)`1 by A445,A446; thus G*(i1,i2)`2<=p`2 & p`2<=G* (i1,j2)`2 by A51,A55,A59,A60,A62,A286,A298,A445,A446,A447,GOBOARD1:def 1; dom l1 = Seg len l1 by FINSEQ_1:def 3; hence p in rng l1 by A51,A62,A297,A445,A446,A447,PARTFUN2:4; suppose j<>len g1; then A448: len g1 < j by A444,REAL_1:def 5; A449: j = w + len g1 by XCMPLX_1:27; len g1 + 1<=j by A448,NAT_1:38; then A450: 1<=w & w<=len g2 by A442,A444,REAL_1:84,86; then A451: g/.j=g2/.w by A449,GOBOARD2:5; w in dom g2 by A450,FINSEQ_3:27; hence p`1=ppi`1 & ppi`2<=p`2 & p`2<= pj`2 & p in rng l1 by A308,A445,A451; 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 A452: x in X & X in lg by TARSKI:def 4; consider i such that A453: X=LSeg(g,i) & 1<=i & i+1 <= len g by A452; per cases; suppose A454: 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 A453,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A453,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A453,A454; then x in union {LSeg(g1,j): 1<=j & j+1 <= len g1} by A452,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A33,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A455: i+1 > len g1; then A456: len g1<=i & i<=i+1 & i+1<=len g by A453,NAT_1:38; A457: 1<=i+1 & len g1<=i+1 & i<=len g by A453,A455,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A458: 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 A443,A456,A457; then A459: q1=|[q1`1,q1`2]| & q2=|[q1`1,q2`2]| by EUCLID:57; A460: LSeg(g,i)=LSeg(q2,q1) by A453,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 A459,A460,TOPREAL3:15; then consider p2 such that A461: p2=x & p2`1=q1`1 & q2`2<=p2`2 & p2`2<=q1`2 by A452,A453; ppi`2<=p2`2 & p2`2<=pj`2 by A458,A461,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A300,A458,A461; 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 A459,A460,TOPREAL1:7; then x=q1 by A452,A453,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A300,A458; 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 A459,A460,TOPREAL3:15; then consider p2 such that A462: p2=x & p2`1=q1`1 & q1`2<=p2`2 & p2`2<=q2`2 by A452,A453; ppi`2<=p2`2 & p2`2<=pj`2 by A458,A462,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A300,A458,A462; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; let x; assume x in L~f; then A463: x in L~f1 \/ LSeg(f,k) by A5,A12,GOBOARD2:8; now per cases by A463,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A33,GOBOARD2:11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A464: p1=x & p1`1=ppi`1 & ppi`2<=p1`2 & p1`2<=pj`2 by A300; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`2<=p1`2; A465: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A442,REAL_2:173; let q such that A466: q=g/.n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A35,A466,GROUP_5:95 .=G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence q`2<=p1`2 by A464; end; end; A467: for n holds P2[n] implies n<=len g; consider ma be Nat such that A468: P2[ma] & for n st P2[n] holds n<=ma from Max(A467,A465); now per cases; suppose A469: ma=len g; i2+1<=j2 by A286,NAT_1:38; then A470: 1<=l by REAL_1:84; then A471: l in dom g2 & i2+l=j2 by A287,FINSEQ_3:27,XCMPLX_1:27; then A472: g/.ma=g2/.l by A287,A442,A469,GROUP_5:96 .= pj by A287,A471; then pj`2<=p1`2 by A468; then A473: p1`2=pj`2 by A464,AXIOMS:21; A474: ma-1<=len g & len g1+1<=ma by A287,A442,A469,A470,PROB_1:2,REAL_1:55; then A475: len g1<=ma-1 & 0<=len g1 by NAT_1:18,REAL_1:84; then A476: 0+1<=ma by REAL_1:84; then A477: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A476,INT_1:18; 1<=len g1 by A14,A16,A36,AXIOMS:22; then A478: 1<=m1 by A475,AXIOMS:22; then A479: m1 in dom g & Seg len g=dom g by A474,FINSEQ_1:def 3,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A480: q`1=ppi`1 & q`2<=pj`2 & q=|[q`1,q`2]| & m1+1=ma by A443,A474,A475,EUCLID:57,XCMPLX_1:27; then A481: LSeg(g,m1)=LSeg(q,pj) by A469,A472,A478,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 A49,A53,A71,A293,A295,A299,A469,A472,A477,A479,A480, 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 A480,REAL_1:def 5; then LSeg(g,m1)=lq by A299,A480,A481,TOPREAL3:15; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A464,A469,A473,A478,A480; then x in union lg by A464,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A468,REAL_1:def 5; then A482: ma+1<=len g & k<=ma & ma<=ma+1 by A16,A36,A468,AXIOMS:22,NAT_1:38; then A483: 1<=ma & len g1<=ma+1 by A14,A468,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A484: qa`2<=p1`2 by A468; A485: now assume qa1`2<=p1`2; then for q holds q=g/.(ma+1) implies q`2<=p1`2; then ma+1<=ma by A468,A482,A483; hence contradiction by REAL_2:174; end; then A486: qa`2<qa1`2 & qa`2<=p1`2 & p1`2<=qa1`2 & qa`1=ppi`1 & qa1 `1 = ppi`1 by A443,A468,A482,A483,A484,AXIOMS:22; set lma = {p2: p2`1=ppi`1 & qa`2<=p2`2 & p2`2<=qa1`2}; A487: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa,qa1) by A482,A483,TOPREAL1:def 5 .= lma by A486,A487,TOPREAL3:15; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A464,A482,A483,A484, A485; 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 A14,A16,A36,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A34,GROUP_5:95 .=f/.1 by A15,A19,GOBOARD1:10; i2+1<=j2 by A286,NAT_1:38; then A488: 1<=l by REAL_1:84; then A489: l in dom g2 & len g=len g1 + l by A287,FINSEQ_1:35,FINSEQ_3: 27; hence g/.len g=g2/.l by GROUP_5:96 .=G*(i1,i2+l) by A287,A489 .=f/.len f by A5,A49,A71,XCMPLX_1:27; thus len f<=len g by A5,A16,A36,A488,A489,REAL_1:55; end; hence thesis; suppose A490: i2=j2; set ppi = G*(i1,i2), pj = G*(j1,i2); now per cases by AXIOMS:21; case A491: i1>j1; then reconsider l=i1-j1 as Nat by INT_1:18; A492: now let n; assume n in Seg l; then A493: 1<=n & n<=l & 0<=j1 by FINSEQ_1:3,NAT_1:18; then l<=i1 by PROB_1:2; then n<=i1 by A493,AXIOMS:22; then reconsider w=i1-n as Nat by INT_1:18; 0<=n & i1-l<=i1-n by A493,AXIOMS:22,REAL_1:92; then i1-n<=i1 & i1<=len G & j1<=w & 1<=j1 by A51,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 A50,A51,ZFMISC_1:106; end; defpred P1[Nat,set] means for m st m=i1-$1 holds $2=G*(m,i2); A494: now let n; assume n in Seg l; then reconsider m=i1-n as Nat by A492; take p=G*(m,i2); thus P1[n,p]; end; consider g2 such that A495: len g2 = l & for n st n in Seg l holds P1[n,g2/.n] from FinSeqDChoice(A494); A496: dom g2=Seg l by A495,FINSEQ_1:def 3; take g=g1^g2; now let n; assume A497: n in dom g2; then reconsider m=i1-n as Nat by A492,A496; take m,k=i2; thus [m,k] in Indices G & g2/.n=G*(m,k) by A492,A495,A496,A497; end; then A498: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A53,GOBOARD1:39; A499: now let n; assume A500: n in dom g2 & n+1 in dom g2; then A501: [i1-n,i2] in Indices G & [i1-(n+1),i2] in Indices G by A492,A496; reconsider m1=i1-n ,m2=i1-(n+1) as Nat by A492,A496,A500; A502: g2/.n=G*(m1,i2) & g2/.(n+1)=G*(m2,i2) by A495,A496,A500; 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 by A501,A502,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; A503: now let l1,l2,l3,l4 be Nat; assume A504: [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 A505: [i1-1,i2] in Indices G & f1/.len f1=f/.k by A15,A16,A18,A492,A496,GOBOARD1:10; reconsider m1=i1-1 as Nat by A492,A496,A504; g2/.1=G*(m1,i2) by A495,A496,A504; then l1=i1 & l2=i2 & l3=m1 & l4=i2 by A35,A47,A504,A505,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 A53,A499,GOBOARD1:40; hence g is_sequence_on G by A498,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 A51,A70,FINSEQ_4:def 4; then A506: c1/.i1=ppi & c1/.j1=pj by A51,MATRIX_1:def 9; then A507: y2.i1=ppi`2 & y2.j1=pj`2 & x2.i1=ppi`1 & x2.j1=pj`1 & len g2 =l by A51,A52,A64,A65,A66,A68,A69,A495,GOBOARD1:def 3,def 4; then A508: pj`1<ppi`1 & ppi`2=pj`2 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj `2]| by A51,A52,A56,A57,A64,A65,A66,A68,A69,A491,EUCLID:57,GOBOARD1:def 1, def 2; A509: LSeg(f,k)=LSeg(pj,ppi) by A14,A47,A49,A490,TOPREAL1:def 5 .= lk by A508,TOPREAL3:16; A510: LSeg(f,k)=LSeg(ppi,pj) by A14,A47,A49,A490,TOPREAL1:def 5; now let n,m; assume A511: n in dom g2 & m in dom g2 & n<>m; then A512: [i1-n,i2] in Indices G& [i1-m,i2] in Indices G by A492, A496; reconsider n1=i1-n, m1=i1-m as Nat by A492,A496,A511; A513: g2/.n=G*(n1,i2) & g2/.m=G*(m1,i2) by A495,A496,A511; assume g2/.n=g2/.m; then n1=m1 by A512,A513,GOBOARD1:21; hence contradiction by A511,XCMPLX_1:20; end; then for n,m st n in dom g2 & m in dom g2 & g2/.n = g2/.m holds n = m; then A514: g2 is one-to-one & Seg len g2=dom g2 by FINSEQ_1:def 3,PARTFUN2:16; A515: not f/.k in rng g2 proof assume f/.k in rng g2; then consider n such that A516: n in dom g2 & g2/.n=f/.k by PARTFUN2:4; A517: [i1-n,i2] in Indices G by A492,A495,A514,A516; reconsider n1=i1-n as Nat by A492,A495,A514,A516; g2/.n=G*(n1,i2) & 0+1<=n by A495,A514,A516,FINSEQ_1:3; then n1=i1 & 0<n by A47,A516,A517,GOBOARD1:21,NAT_1:38; hence contradiction by SQUARE_1:29; end; A518: now let n,p; assume A519: n in dom g2 & g2/.n=p; then A520: P1[n,g2/.n] & 1<=n & n<=len g2& i1-n in dom G by A492,A495,A514,FINSEQ_1:3; reconsider n1=i1-n as Nat by A492,A496,A519; set pn = G*(n1,i2); c1/.n1=c1.n1 by A70,A520,FINSEQ_4:def 4; then A521: g2/.n=pn & c1/.n1=pn & 0<=n & i1-len g2<=n1 by A520,AXIOMS:22,MATRIX_1:def 9,REAL_1:92; then A522: y2.n1=pn`2 & y2.n1=y2.i1 & x2.n1=pn`1 & n1<=i1 & j1<=n1 by A51,A52,A57,A64,A65,A66,A68,A69,A495,A520,GOBOARD1:def 2,def 3, def 4,REAL_2:173,XCMPLX_1:18; hence p`2=ppi`2 & pj`1<=p`1 & p`1<=ppi`1 by A51,A52,A56,A64,A66,A69,A507,A519,A520,A521,GOBOARD2:18; thus p in rng c1 by A70,A519,A520,A521,PARTFUN2:4; 0<n by A520,AXIOMS:22; then n1<i1 by SQUARE_1:29; hence p`1<ppi`1 by A51,A52,A56,A64,A66,A69,A507,A519,A520,A521,A522,GOBOARD1:def 1; end; A523: now let n,m,p,q; assume A524: n in dom g2 & m in dom g2 & n<m & g2/.n=p & g2/.m=q; then A525: P1[n,g2/.n] & i1-n in dom G & P1[m,g2/.m] & i1-m in dom G by A492,A495,A496; reconsider n1=i1-n, m1=i1-m as Nat by A492,A496,A524; set pn = G*(n1,i2), pm = G*(m1,i2); c1/.n1=c1.n1 & c1/.m1 = c1.m1 by A70,A525,FINSEQ_4:def 4; then A526: g2/.n=pn & c1/.n1=pn & g2/.m=pm & c1/.m1=pm & m1<n1 by A524,A525,MATRIX_1:def 9,REAL_1:92; then x2.n1=pn`1 & x2.m1=pm`1 by A67,A70,A525,GOBOARD1:def 3; hence q`1<p`1 by A56,A67,A70,A524,A525,A526,GOBOARD1:def 1; end; A527: rng g2 c= LSeg(f,k) proof let x; assume x in rng g2; then consider n such that A528: n in dom g2 & g2/.n=x by PARTFUN2:4; reconsider n1=i1-n as Nat by A492,A495,A514,A528; set pn = G*(n1,i2); A529: g2/.n=pn by A495,A514,A528; then pn`2=ppi`2 & pj`1<=pn`1 & pn`1<=ppi`1 by A518,A528; hence x in LSeg(f,k) by A509,A528,A529; end; rng g1 /\ rng g2 = {} proof consider x being Element of rng g1 /\ rng g2; assume not thesis; then A530: x in rng g1 & x in rng g2 by XBOOLE_0:def 3; now per cases by A14,REAL_1:def 5; suppose k=1; hence contradiction by A37,A515,A530,TARSKI:def 1; suppose 1<k; then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A44,A527,A530,GOBOARD2:9,XBOOLE_0:def 3; hence contradiction by A515,A530,TARSKI:def 1; end; hence contradiction; end; then rng g1 misses rng g2 by XBOOLE_0:def 7; hence g is one-to-one by A29,A514,FINSEQ_3:98; A531: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2,n+1) = {g2/.(n+1)} proof let n; assume A532: 1<=n & n+2 <= len g2; then A533: n in dom g2 & n+1 in dom g2 & n+2 in dom g2 by GOBOARD2:4; then g2/.n in rng g2 & g2/.(n+1) in rng g2 & g2/.(n+2) in rng g2 by PARTFUN2:4; then A534: g2/.n in lk & g2/.(n+1) in lk & g2/.(n+2) in lk by A509,A527; then consider u be Point of TOP-REAL 2 such that A535: g2/.n=u & u`2=ppi`2 & pj`1<=u`1 & u`1<=ppi`1; consider u1 be Point of TOP-REAL 2 such that A536: g2/.(n+1)=u1 & u1`2=ppi`2 & pj`1<=u1`1 & u1`1<=ppi`1 by A534; consider u2 be Point of TOP-REAL 2 such that A537: g2/.(n+2)=u2 & u2`2=ppi`2 & pj`1<=u2`1 & u2`1<=ppi`1 by A534; set lg = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & u2`1<=w`1 & w`1<=u`1}; A538: 1<= n+1 by NAT_1:29; A539: n+1+1 = n+(1+1) by XCMPLX_1:1; n+1 <= n+2 by AXIOMS:24; then n+1 <= len g2 by A532,AXIOMS:22; then A540: LSeg(g2,n)=LSeg(u,u1) & LSeg(g2,n+1)=LSeg(u1,u2) & LSeg(g2/.n,g2/.(n+2))=LSeg(u,u2) by A532,A535,A536,A537,A538,A539,TOPREAL1:def 5; n<n+1 & n+1<n+1+1 & n+1+1=n+(1+1) by NAT_1:38,XCMPLX_1:1; then A541: u2`1<u1`1 & u1`1<u`1 by A523,A533,A535,A536,A537; then A542: u2`1<=u1`1 & u1`1<=u`1 & u2`1<u`1 by AXIOMS:22; A543: u1 in lg & u=|[u`1,u`2]| & u2=|[u2`1,u2`2]| by A536,A541,EUCLID :57; then LSeg(g2/.n,g2/.(n+2))=lg by A535,A537,A542,TOPREAL3:16; hence thesis by A536,A540,A543,TOPREAL1:14; end; thus g is unfolded proof let n; assume A544: 1<=n & n+2 <= len g; then n+(1+1)<=len g; then A545: n+1+1<=len g by XCMPLX_1:1; A546: 1 <= n+1 by NAT_1:29; A547: n<=n+1 & n+1<=n+1+1 by NAT_1:29; then A548: n+1 <= len g by A545,AXIOMS:22; A549: n+(1+1)=n+1+1 by XCMPLX_1:1; A550: len g=len g1+len g2 by FINSEQ_1:35; n+2-len g1 = n-len g1 +2 by XCMPLX_1:29; then A551: n-len g1 + 2 <= len g2 by A544,A550,REAL_1:86; per cases; suppose A552: n+2 <= len g1; then n in dom g1 & n+1 in dom g1 & n+2 in dom g1 & n+(1+1)=n+1+1 by A544,GOBOARD2:4,XCMPLX_1:1; then LSeg(g1,n)=LSeg(g,n) & LSeg(g1,n+1)=LSeg(g,n+1) & g/.(n+1)=g1/.(n+1) by GROUP_5:95,TOPREAL3:25; hence thesis by A30,A544,A552,TOPREAL1:def 8; suppose len g1 < n+2; then len g1+1<=n+2 by NAT_1:38; then len g1<=n+2-1 by REAL_1:84; then A553: len g1<=n+(1+1-1) by XCMPLX_1:29; thus thesis proof per cases; suppose A554: len g1=n+1; now assume A555: k=1; 1<len g1 by A544,A554,NAT_1:38; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A555,TOPREAL1:29; end; then A556: 1<k & LSeg(g1,n) c= L~f1 by A14,A33,REAL_1:def 5,TOPREAL3:26; then A557: L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,GOBOARD2:9; 1<=n+1 by NAT_1:29; then A558: n in dom g1 & n+1 in dom g1 by A544,A547,A554,FINSEQ_3:27; then A559: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; A560: g/.(n+1)=f1/.len f1 by A35,A554,A558,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; 1 <= len g2 by A544,A549,A550,A554,REAL_1:53; then A561: g/.(n+2)=g2/.1 by A549,A554,GOBOARD2:5; 1<=len g-len g1 by A545,A554,REAL_1:84; then 1<=len g2 by A550,XCMPLX_1:26; then 1 in dom g2 by FINSEQ_3:27; then A562: g2/.1 in rng g2 by PARTFUN2:4; then g2/.1 in lk by A509,A527; then consider u1 be Point of TOP-REAL 2 such that A563: g2/.1=u1 & u1`2=ppi`2 & pj`1<=u1`1 & u1`1<=ppi`1; ppi in LSeg(ppi,pj) by TOPREAL1:6; then LSeg(ppi,u1) c= LSeg(f,k) & LSeg(g,n+1)=LSeg(ppi,u1) by A510,A527,A544,A546,A549,A560,A561,A562,A563,TOPREAL1:12,def 5; then A564: LSeg(g,n) /\ LSeg(g,n+1) c= {g/.(n+1)} by A47,A556,A557,A559,A560,XBOOLE_1:27; g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1) by A544,A546,A548,A549,TOPREAL1:27; then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by XBOOLE_0:def 3; then {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:37; hence thesis by A564,XBOOLE_0:def 10; suppose len g1<>n+1; then len g1<n+1 by A553,REAL_1:def 5; then A565: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; thus thesis proof per cases; suppose A566: len g1=n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A567: g/.n=f1/.len f1 by A35,A566,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; A568: 2 <= len g2 by A544,A550,A566,REAL_1:53; then 1<= len g2 by AXIOMS:22; then A569: g/.(n+1)=g2/.1 by A566,GOBOARD2:5; A570: g/.(n+2)=g2/.2 by A566,A568,GOBOARD2:5; 1<=len g2 by A568,AXIOMS:22; then A571: 1 in dom g2 & 2 in dom g2 by A568,FINSEQ_3:27; then g2/.1 in rng g2 & g2/.2 in rng g2 by PARTFUN2:4; then A572: g2/.1 in lk & g2/.2 in lk by A509,A527; then consider u1 be Point of TOP-REAL 2 such that A573: g2/.1=u1 & u1`2=ppi`2 & pj`1<=u1`1 & u1`1<=ppi`1; consider u2 be Point of TOP-REAL 2 such that A574: g2/.2=u2 & u2`2=ppi`2 & pj`1<=u2`1 & u2`1<=ppi`1 by A572; A575: u2`1<u1`1 by A523,A571,A573,A574; then A576: u2`1<=u1`1 & u2`1<ppi`1 & u2=|[u2`1,u2`2]| by A573,AXIOMS:22,EUCLID:57; set lg = {w where w is Point of TOP-REAL 2 : w`2=ppi`2 & u2`1<=w`1 & w`1<=ppi`1}; A577: u1 in lg by A573,A575; A578: LSeg(ppi,g2/.2)=LSeg(ppi,u2) & LSeg(g,n)=LSeg(ppi,u1) & LSeg(g,n+1)=LSeg(u1,u2) by A544,A546,A548,A549,A567,A569,A570,A573,A574,TOPREAL1:def 5; LSeg(ppi,g2/.2)=lg by A508,A574,A576,TOPREAL3:16; hence thesis by A569,A573,A577,A578,TOPREAL1:14; suppose len g1<>n; then A579: len g1<n by A565,REAL_1:def 5; n1 + len g1 = n by XCMPLX_1:27; then A580: LSeg(g,n)=LSeg(g2,n1) by A548,A579,GOBOARD2:10; A581: len g1<n+1 by A547,A579,AXIOMS:22; A582: len g1+1<=n by A579,NAT_1:38; A583: n+1 = (n1+len g1)+1 by XCMPLX_1:27 .= n1+1+len g1 by XCMPLX_1:1; A584: 1<=n1+1 by NAT_1:29; n1 + len g1 = n by XCMPLX_1:27; then n1 + 1 + len g1 = n + 1 by XCMPLX_1:1; then n1+1 <= len g2 by A548,A550,REAL_1:53; then LSeg(g,n+1)=LSeg(g2,n1+1)& g/.(n+1)=g2/.(n1+1) & 1<=n1 by A545,A581,A582,A583,A584,GOBOARD2:5,10,REAL_1:84; hence thesis by A531,A551,A580; end; end; end; for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m) proof let n,m; assume that A585: m>n+1 and A586: n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 and A587: LSeg(g2,n) /\ LSeg(g2,m) <> {}; A588: 1 <= n & n+1 <= len g2 & 1 <= m & m+1<= len g2 by A586,FINSEQ_3:27; reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lp = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & p2`1<=w`1 & w`1<=p1`1}, lq = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & q2`1<=w`1 & w`1<=q1`1}; m<m+1 & n<n+1 by NAT_1:38; then A589: p2`1<p1`1 & q2`1<q1`1 & p1`2=ppi`2 & p2`2=ppi`2 & q1`2= ppi`2 & q2`2=ppi`2 & p1=|[p1`1,p1`2]| & q1=|[q1`1,q1`2]| & p2=|[p2`1,p2`2]| & q2=|[q2`1,q2`2]| by A518,A523,A586,EUCLID:57; A590: LSeg(g2,n) = LSeg(p2,p1) by A588,TOPREAL1:def 5 .=lp by A589,TOPREAL3:16; A591: LSeg(g2,m) = LSeg(q2,q1) by A588,TOPREAL1:def 5 .=lq by A589,TOPREAL3:16; consider x being Element of LSeg(g2,n) /\ LSeg(g2,m); A592: x in LSeg(g2,n) & x in LSeg(g2,m) by A587,XBOOLE_0:def 3; then A593: ex tn be Point of TOP-REAL 2 st tn=x & tn`2=ppi`2 & p2`1<=tn`1 & tn`1<=p1`1 by A590; A594: ex tm be Point of TOP-REAL 2 st tm=x & tm`2=ppi`2 & q2`1<=tm`1 & tm`1<=q1`1 by A591,A592; q1`1<p2`1 by A523,A585,A586; hence contradiction by A593,A594,AXIOMS:22; end; then A595: g2 is s.n.c. by GOBOARD2:6; A596: L~g2 c= LSeg(f,k) proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; let x; assume x in L~g2; then x in union ls by TOPREAL1:def 6; then consider X be set such that A597: x in X & X in ls by TARSKI:def 4; consider m such that A598: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A597; m in dom g2 & m+1 in dom g2 by A598,GOBOARD2:3; then A599: g2/.m in rng g2 & g2/.(m+1) in rng g2 by PARTFUN2:4; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; A600: LSeg(q1,q2) c= LSeg(ppi,pj) by A510,A527,A599,TOPREAL1:12; LSeg(g2,m)=LSeg(q1,q2) by A598,TOPREAL1:def 5; hence thesis by A510,A597,A598,A600; end; A601: not f/.k in L~g2 proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; assume f/.k in L~g2; then f/.k in union ls by TOPREAL1:def 6; then consider X be set such that A602: f/.k in X & X in ls by TARSKI:def 4; consider m such that A603: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A602; A604: m in dom g2 & m+1 in dom g2 & m<m+1 by A603,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lq={w where w is Point of TOP-REAL 2: w`2=ppi`2 & q2`1<=w`1 & w`1<=q1`1}; A605: q1`2=ppi`2 & q2`2=ppi`2 & q2`1<q1`1 & q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by A518,A523,A604,EUCLID:57; LSeg(g2,m)=LSeg(q2,q1) by A603,TOPREAL1:def 5 .=lq by A605,TOPREAL3:16; then ex p st p=f/.k & p`2=ppi`2 & q2`1<=p`1 & p`1<=q1`1 by A602,A603 ; hence contradiction by A47,A518,A604; end; A606: L~g1 /\ L~g2 = {} proof per cases; suppose k=1; hence thesis by A37; suppose k<>1; then 1<k by A14,REAL_1:def 5; then L~g1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A33,GOBOARD2:9; then A607: L~g1 /\ L~g2 c= {f/.k} by A596,XBOOLE_1:26; now consider x being Element of L~g1 /\ L~g2; assume L~g1 /\ L~g2 <> {}; then x in {f/.k} & x in L~g2 by A607,TARSKI:def 3,XBOOLE_0:def 3 ; hence contradiction by A601,TARSKI:def 1; end; hence thesis; end; for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g & m+1 in dom g holds LSeg(g,n) misses LSeg(g,m) proof let n,m; assume that A608: m>n+1 and A609: n in dom g & n+1 in dom g & m in dom g & m+1 in dom g; A610: 1<=n & 1<=n+1 & n+1<=len g & 1<=m & 1<=m+1 & m+1<=len g & n<=n+1 & m<=m+1 & len g=len g1+len g2 by A609,FINSEQ_1:35,FINSEQ_3:27,NAT_1:29; set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j): 1<=j & j+1 <= len g2}; A611: L~g1=union l1 & L~g2=union l2 & n+1 <= len g & m+1 <= len g by A609,FINSEQ_3:27,TOPREAL1:def 6; j1+1<=i1 by A491,NAT_1:38; then A612: 1<=l by REAL_1:84; then A613: 1 in dom g2 by A495,FINSEQ_3:27; reconsider qq=g2/.1 as Point of TOP-REAL 2; set ql={z where z is Point of TOP-REAL 2: z`2=ppi`2 & qq`1<=z`1 & z`1<=ppi`1}; A614: 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 & dom g1 c= dom g by FINSEQ_1:39,FINSEQ_3:27; then A615: g/.len g1=g1/.len g1 by GROUP_5:95 .= ppi by A15,A16,A18,A35,A47,GOBOARD1:10; A616: len g1<len g1 +1 & len g1+1<=len g by A495,A610,A612,NAT_1:38,REAL_1:55; A617: g/.(len g1+1)=qq by A495,A612,GOBOARD2:5; A618: qq`2=ppi`2 & pj`1<=qq`1 & qq`1<ppi`1 & qq=|[qq`1,qq`2]| by A518,A613,EUCLID:57; A619: LSeg(g,len g1)=LSeg(qq,ppi) by A614,A615,A616,A617,TOPREAL1:def 5 .= ql by A508,A618,TOPREAL3:16; A620: n+1<=m+1 by A608,A610,AXIOMS:22; now per cases; suppose A621: m+1<=len g1; then A622: m<=len g1 & n+1<=len g1 by A610,A620,AXIOMS:22; then n<=len g1 by A610,AXIOMS:22; then n in dom g1 & n+1 in dom g1 & m in dom g1 & m+1 in dom g1 by A610,A621,A622,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) & LSeg(g,m)=LSeg(g1,m) by TOPREAL3:25; hence thesis by A31,A608,TOPREAL1:def 9; suppose len g1<m+1; then A623: len g1<=m by NAT_1:38; then reconsider m1=m-len g1 as Nat by INT_1:18; now per cases; suppose A624: m=len g1; now assume A625: k=1; 1<len g1 by A608,A610,A624,AXIOMS:22; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A625,TOPREAL1:29; end; then 1<k by A14,REAL_1:def 5; then A626: L~f1 /\ LSeg(f,k) ={f/.k} by A5,A8,A9,GOBOARD2:9; n<=len g1 by A608,A610,A624,AXIOMS:22; then A627: n in dom g1 & n+1 in dom g1 by A608,A610,A624,FINSEQ_3:27; then A628: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A608,A610,A624; then A629: LSeg(g,n) c= L~f1 by A33,A611,ZFMISC_1:92; LSeg(g,m) c= LSeg(f,k) proof let x; assume x in LSeg(g,m); then consider px be Point of TOP-REAL 2 such that A630: px=x & px`2=ppi`2 & qq`1<=px`1 & px`1<= ppi`1 by A619,A624; pj`1<=px`1 by A618,A630,AXIOMS:22; hence thesis by A509,A630; end; then A631: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A626,A629,XBOOLE_1:27; now consider x being Element of LSeg(g,n)/\ LSeg(g,m); assume LSeg(g,n)/\ LSeg(g,m)<>{}; then A632: x in LSeg(g,n) & x in {f/.k} by A631,TARSKI:def 3,XBOOLE_0:def 3; then A633: x=f/.k by TARSKI:def 1; f/.k=g1/.len g1 by A15,A16,A18,A35,GOBOARD1:10; hence contradiction by A29,A30,A31,A608,A624,A627,A628,A632,A633,GOBOARD2:7; end; hence thesis by XBOOLE_0:def 7; suppose A634: m<>len g1; m+1 = m1+len g1+1 by XCMPLX_1:27; then A635: len g1<m & m+1=m1+1+len g1 by A623,A634,REAL_1:def 5,XCMPLX_1:1; m = m1+len g1 by XCMPLX_1:27; then A636: LSeg(g,m)=LSeg(g2,m1) by A610,A635,GOBOARD2:10; m1+1<=len g2 & len g1+1<= m by A610,A635,NAT_1:38,REAL_1:53; then A637: 1<=m1 & m1+1 <= len g2 by REAL_1:84; then LSeg(g,m) in l2 by A636; then A638: LSeg(g,m) c= L~g2 by A611,ZFMISC_1:92; now per cases; suppose A639: n+1<=len g1; then n<=len g1 by A610,AXIOMS:22; then n in dom g1 & n+1 in dom g1 by A610,A639,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A610,A639; then LSeg(g,n) c= L~g1 by A611,ZFMISC_1:92; then LSeg(g,n) /\ LSeg(g,m) c= {} by A606,A638,XBOOLE_1:27; then LSeg(g,n) /\ LSeg(g,m) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; suppose len g1<n+1; then A640: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; A641: n - len g1 + 1 = n + 1 - len g1 by XCMPLX_1:29; A642: n = n1 + len g1 by XCMPLX_1:27; now per cases; suppose A643: len g1=n; now consider x being Element of LSeg(g,n) /\ LSeg(g,m); assume LSeg(g,n) /\ LSeg(g,m)<>{}; then A644: x in LSeg(g,n) & x in LSeg(g,m) by XBOOLE_0:def 3; then A645: ex qx be Point of TOP-REAL 2 st qx=x & qx`2=ppi`2 & qq`1<=qx`1 & qx`1<= ppi`1 by A619,A643; A646: m1 in dom g2 & m1+1 in dom g2 & m1<m1+1 by A637,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point of TOP-REAL 2; set q1l={v where v is Point of TOP-REAL 2: v`2=ppi`2 & q2`1<=v`1 & v`1<=q1`1}; A647: q1`2=ppi`2 & q2`2=ppi`2 & q2`1<q1`1 & q1=|[q1`1,q1`2]|& q2=|[q2`1,q2`2]| by A518,A523,A646,EUCLID:57; m1 > n1 + 1 & n1 + 1 >= 1 by A608,A641,NAT_1:29,REAL_1:54; then A648: m1 > 1 by AXIOMS:22; LSeg(g2,m1)=LSeg(q2,q1) by A637,TOPREAL1:def 5 .=q1l by A647,TOPREAL3:16; then A649: ex qy be Point of TOP-REAL 2 st qy=x & qy`2=ppi`2 & q2`1<=qy`1 & qy`1<= q1`1 by A636,A644; q1`1 < qq`1 by A523,A613,A646,A648; hence contradiction by A645,A649,AXIOMS:22; end; hence thesis by XBOOLE_0:def 7; suppose n<>len g1; then len g1<n by A640,REAL_1:def 5; then LSeg(g,n)=LSeg(g2,n1) & m1>n1+1 by A608,A610,A641,A642,GOBOARD2:10,REAL_1:54; hence thesis by A595,A636,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; hence thesis; end; hence thesis; end; hence g is s.n.c. by GOBOARD2:6; A650: g2 is special proof let n; set p = g2/.n, q = g2/.(n+1); assume 1<=n & n+1 <= len g2; then n in dom g2 & n+1 in dom g2 by GOBOARD2:3; then p`2=ppi`2 & q`2=ppi`2 by A518; hence p`1=q`1 or p`2=q`2; end; now set p=g1/.len g1, q=g2/.1; j1+1<=i1 by A491,NAT_1:38; then 1<=l by REAL_1:84; then 1 in dom g2 by A496,FINSEQ_1:3; then q`2=ppi`2 by A518; hence p`1=q`1 or p`2=q`2 by A15,A16,A18,A35,A47,GOBOARD1:10; end; hence g is special by A32,A650,GOBOARD2:13; 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}; A651: len g = len g1 + len g2 by FINSEQ_1:35; A652: now let j; assume A653: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A654: p=g/.j; per cases; suppose A655: j=len g1; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A656: g/.len g1 = f1/.len f1 by A35,GROUP_5:95 .= G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence p`2=G*(i1,i2)`2 by A654,A655; thus G*(j1,i2)`1<=p`1 & p`1<=G* (i1,i2)`1 by A51,A52,A56,A64,A66,A69,A491,A507,A654,A655,A656, GOBOARD1:def 1; Seg len c1 = dom c1 by FINSEQ_1:def 3; hence p in rng c1 by A51,A52,A69,A506,A654,A655,A656,PARTFUN2:4; suppose j<>len g1; then A657: len g1 < j by A653,REAL_1:def 5; A658: j = w + len g1 by XCMPLX_1:27; len g1 + 1<=j by A657,NAT_1:38; then A659: 1<=w & w<=len g2 by A651,A653,REAL_1:84,86; then A660: g/.j=g2/.w by A658,GOBOARD2:5; w in dom g2 by A659,FINSEQ_3:27; hence p`2=ppi`2 & pj`1<=p`1 & p`1<= ppi`1 & p in rng c1 by A518,A654,A660; 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 A661: x in X & X in lg by TARSKI:def 4; consider i such that A662: X=LSeg(g,i) & 1<=i & i+1 <= len g by A661; per cases; suppose A663: 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 A662,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A662,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A662,A663; then x in union {LSeg(g1,j): 1<=j & j+1 <= len g1} by A661,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A33,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A664: i+1 > len g1; then A665: len g1<=i & i<=i+1 & i+1<=len g by A662,NAT_1:38; A666: 1<=i+1 & len g1<=i+1 & i<=len g by A662,A664,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A667: 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 A652,A665,A666; then A668: q1=|[q1`1,q1`2]| & q2=|[q2`1,q1`2]| by EUCLID:57; A669: LSeg(g,i)=LSeg(q2,q1) by A662,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 A668,A669,TOPREAL3:16; then consider p2 such that A670: p2=x & p2`2=q1`2 & q2`1<=p2`1 & p2`1<=q1`1 by A661,A662; pj`1<=p2`1 & p2`1<=ppi`1 by A667,A670,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A509,A667,A670; 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 A668,A669,TOPREAL1:7; then x=q1 by A661,A662,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A509,A667; 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 A668,A669,TOPREAL3:16; then consider p2 such that A671: p2=x & p2`2=q1`2 & q1`1<=p2`1 & p2`1<=q2`1 by A661,A662; pj`1<=p2`1 & p2`1<=ppi`1 by A667,A671,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A509,A667,A671; then x in union lf by TARSKI:def 4; hence thesis by TOPREAL1:def 6; end; hence thesis; end; let x; assume x in L~f; then A672: x in L~f1 \/ LSeg(f,k) by A5,A12,GOBOARD2:8; per cases by A672,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A33,GOBOARD2:11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A673: p1=x & p1`2=ppi`2 & pj`1<=p1`1 & p1`1<=ppi`1 by A509; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`1>=p1`1; A674: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A651,REAL_2:173; let q such that A675: q=g/.n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A35,A675,GROUP_5:95 .=G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence p1`1<=q`1 by A673; end; end; A676: for n holds P2[n] implies n<=len g; consider ma be Nat such that A677: P2[ma] & for n st P2[n] holds n<=ma from Max(A676,A674); now per cases; suppose A678: ma=len g; j1+1<=i1 by A491,NAT_1:38; then A679: 1<=l & l=len g2 by A495,REAL_1:84; then A680: l in dom g2 & i1-l=j1 by FINSEQ_3:27,XCMPLX_1:18; then A681: g/.ma=g2/.l by A495,A651,A678,GROUP_5:96 .= pj by A495,A496,A680; then p1`1<=pj`1 by A677; then A682: p1`1=pj`1 by A673,AXIOMS:21; A683: ma-1<=len g & len g1+1<=ma by A651,A678,A679,PROB_1:2,REAL_1:55; then A684: len g1<=ma-1 & 0<=len g1 by NAT_1:18,REAL_1:84; then A685: 0+1<=ma by REAL_1:84; then A686: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A685,INT_1:18; 1<=len g1 by A14,A16,A36,AXIOMS:22; then A687: 1<=m1 by A684,AXIOMS:22; then A688: m1 in dom g & Seg len g=dom g by A683,FINSEQ_1:def 3,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A689: q`2=ppi`2 & pj`1<=q`1 & q=|[q`1,q`2]| & m1+1=ma by A652,A683,A684,EUCLID:57,XCMPLX_1:27; then A690: LSeg(g,m1)=LSeg(pj,q) by A678,A681,A687,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 A49,A53,A490,A499,A503,A508,A678,A681,A686,A688,A689, 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 A689,REAL_1:def 5; then LSeg(g,m1)=lq by A508,A689,A690,TOPREAL3:16; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A673,A678,A682,A687,A689; then x in union lg by A673,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A677,REAL_1:def 5; then A691: ma+1<=len g & k<=ma & ma<=ma+1 by A16,A36,A677,AXIOMS:22,NAT_1:38; then A692: 1<=ma & len g1<=ma+1 by A14,A677,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A693: p1`1<=qa`1 by A677; A694: now assume p1`1<=qa1`1; then for q holds q=g/.(ma+1) implies p1`1<=q`1; then ma+1<=ma by A677,A691,A692; hence contradiction by REAL_2:174; end; then A695: qa1`1<qa`1 & qa1`1<=p1`1 & p1`1<=qa`1 & qa`2=ppi`2 & qa1 `2 = ppi`2 by A652,A677,A691,A692,A693,AXIOMS:22; set lma = {p2: p2`2=ppi`2 & qa1`1<=p2`1 & p2`1<=qa`1}; A696: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa1,qa) by A691,A692,TOPREAL1:def 5 .= lma by A695,A696,TOPREAL3:16; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A673,A691,A692,A693, A694; 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; 1<=len g1 by A14,A16,A36,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A34,GROUP_5:95 .=f/.1 by A15,A19,GOBOARD1:10; j1+1<=i1 by A491,NAT_1:38; then A697: 1<=l by REAL_1:84; then A698: l in dom g2 & len g=len g1 + len g2 & len g2 = l by A496,FINSEQ_1:3,35,def 3; then reconsider m1=i1-l as Nat by A492,A496; thus g/.len g=g2/.l by A698,GROUP_5:96 .=G*(m1,i2) by A495,A496,A698 .=f/.len f by A5,A49,A490,XCMPLX_1:18; thus len f<=len g by A5,A16,A36,A697,A698,REAL_1:55; case A699: i1=j1; k<>k+1 by NAT_1:38; hence contradiction by A7,A15,A47,A48,A49,A490,A699,PARTFUN2:17; case A700: i1<j1; then reconsider l=j1-i1 as Nat by INT_1:18; deffunc F(Nat) = G*(i1+$1,i2); consider g2 such that A701: len g2 = l & for n st n in dom g2 holds g2/.n = F(n) from PiLambdaD; A702: Seg l = dom g2 by A701,FINSEQ_1:def 3; take g=g1^g2; A703: now let n; assume n in Seg l; then A704: 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 A51,FINSEQ_3:27,XCMPLX_1:27; then 1<=i1+n & i1+n<=len G by A704,AXIOMS:22; hence i1+n in dom G by FINSEQ_3:27; hence [i1+n,i2] in Indices G by A50,A51,ZFMISC_1:106; end; A705: Seg len g2 = dom g2 by FINSEQ_1:def 3; now let n such that A706: n in dom g2; take m=i1+n,k=i2; thus [m,k] in Indices G & g2/.n=G*(m,k) by A701,A703,A705,A706; end; then A707: for n st n in dom g ex i,j st [i,j] in Indices G & g/.n=G*(i,j) by A53,GOBOARD1:39; A708: now let n; assume n in dom g2 & n+1 in dom g2; then A709: 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 A701,A703,A705; 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 by A709,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; A710: now let l1,l2,l3,l4 be Nat; assume A711: [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 A15,A16,A18,A701,A703,A705,GOBOARD1:10; then l1=i1 & l2=i2 & l3=i1+1 & l4=i2 by A35,A47,A711,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 A53,A708,GOBOARD1:40; hence g is_sequence_on G by A707,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 A51,A70,FINSEQ_4:def 4; then A712: c1/.i1=ppi & c1/.j1=pj by A51,MATRIX_1:def 9; then A713: y2.i1=ppi`2 & y2.j1=pj`2 & x2.i1=ppi`1 & x2.j1=pj`1 by A51,A64,A65,A66,A67,A68,A70,GOBOARD1:def 3,def 4; then A714: ppi`1<pj`1 & ppi`2=pj`2 & ppi=|[ppi`1,ppi`2]| & pj=|[pj`1,pj`2]| by A51,A56,A57,A64,A65,A66,A67,A68,A70,A700,EUCLID:57,GOBOARD1:def 1, def 2; A715: LSeg(f,k)=LSeg(ppi,pj) by A14,A47,A49,A490,TOPREAL1:def 5 .= lk by A714,TOPREAL3:16; A716: LSeg(f,k)=LSeg(ppi,pj) by A14,A47,A49,A490,TOPREAL1:def 5; now let n,m; assume A717: n in dom g2 & m in dom g2 & n<>m; then A718: g2/.n=G*(i1+n,i2) & g2/.m=G*(i1+m,i2) & [i1+n,i2] in Indices G & [i1+m,i2] in Indices G by A701,A703,A705; assume g2/.n=g2/.m; then i1+n=i1+m by A718,GOBOARD1:21; hence contradiction by A717,XCMPLX_1:2; end; then for n,m st n in dom g2 & m in dom g2 & g2/.n = g2/.m holds n = m; then A719: g2 is one-to-one by PARTFUN2:16; A720: not f/.k in rng g2 proof assume f/.k in rng g2; then consider n such that A721: n in dom g2 & g2/.n=f/.k by PARTFUN2:4; A722: g2/.n=G*(i1+n,i2) & [i1+n,i2] in Indices G by A701,A702,A703,A721; 0+1<=n by A721,FINSEQ_3:27; then i1+n=i1 & 0<n by A47,A721,A722,GOBOARD1:21,NAT_1:38; hence contradiction by XCMPLX_1:3; end; A723: now let n,p; assume A724: n in dom g2 & g2/.n=p; then A725: g2/.n=G*(i1+n,i2) & 1<=n & n<=len g2 & i1+n in dom G by A701,A703,A705,FINSEQ_3:27; set n1=i1+n; set pn = G*(n1,i2); c1/.n1=c1.n1 by A70,A725,FINSEQ_4:def 4; then A726: g2/.n=pn & c1/.n1=pn & 0<=n & n1<=i1+len g2 by A725,AXIOMS:22,MATRIX_1:def 9,REAL_1:55; then A727: y2.n1=pn`2 & y2.n1=y2.i1 & x2.n1=pn`1 & n1<=j1 & i1<=n1 by A51,A57,A64,A65,A66,A67,A68,A70,A701,A725,GOBOARD1:def 2,def 3,def 4,REAL_2:173,XCMPLX_1:27; hence p`2=ppi`2 & ppi`1<=p`1 & p`1<=pj`1 by A51,A56,A67,A70,A713,A724,A725,GOBOARD2:18; thus p in rng c1 by A70,A724,A725,A726,PARTFUN2:4; 0<n by A725,AXIOMS:22; then i1<n1 by REAL_2:174; hence p`1>ppi`1 by A51,A56,A67,A70,A713,A724,A725,A727,GOBOARD1:def 1 ; end; A728: now let n,m,p,q; assume A729: n in dom g2 & m in dom g2 & n<m & g2/.n=p & g2/.m=q; then A730: g2/.n=G*(i1+n,i2) & i1+n in dom G & g2/.m=G*(i1+m,i2) & i1+m in dom G by A701,A703,A705; set n1=i1+n, m1=i1+m; set pn = G*(n1,i2), pm = G*(m1,i2); c1/.n1=c1.n1 & c1/.m1 = c1.m1 by A70,A730,FINSEQ_4:def 4; then A731: c1/.n1=pn & c1/.m1=pm & n1<m1 by A729,A730,MATRIX_1:def 9,REAL_1:67; then x2.n1=pn`1 & x2.m1=pm`1 by A67,A70,A730,GOBOARD1:def 3; hence p`1<q`1 by A56,A67,A70,A729,A730,A731,GOBOARD1:def 1; end; A732: rng g2 c= LSeg(f,k) proof let x; assume x in rng g2; then consider n such that A733: n in dom g2 & g2/.n=x by PARTFUN2:4; A734: g2/.n=G*(i1+n,i2) by A701,A733; set pn = G*((i1+n),i2); pn`2=ppi`2 & ppi`1<=pn`1 & pn`1<=pj`1 by A723,A733,A734; hence x in LSeg(f,k) by A715,A733,A734; end; rng g1 /\ rng g2 = {} proof consider x being Element of rng g1 /\ rng g2; assume not thesis; then A735: x in rng g1 & x in rng g2 by XBOOLE_0:def 3; now per cases by A14,REAL_1:def 5; suppose k=1; hence contradiction by A37,A720,A735,TARSKI:def 1; suppose 1<k; then x in L~f1 /\ LSeg(f,k) & L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A44,A732,A735,GOBOARD2:9,XBOOLE_0:def 3; hence contradiction by A720,A735,TARSKI:def 1; end; hence contradiction; end; then rng g1 misses rng g2 by XBOOLE_0:def 7; hence g is one-to-one by A29,A719,FINSEQ_3:98; A736: for n st 1<=n & n+2 <= len g2 holds LSeg(g2,n) /\ LSeg(g2,n+1) = {g2/.(n+1)} proof let n; assume A737:1<=n & n+2 <= len g2; then A738: n in dom g2 & n+1 in dom g2 & n+2 in dom g2 by GOBOARD2:4; then g2/.n in rng g2 & g2/.(n+1) in rng g2 & g2/.(n+2) in rng g2 by PARTFUN2:4; then A739: g2/.n in lk & g2/.(n+1) in lk & g2/.(n+2) in lk by A715,A732; then consider u be Point of TOP-REAL 2 such that A740: g2/.n=u & u`2=ppi`2 & ppi`1<=u`1 & u`1<=pj`1; consider u1 be Point of TOP-REAL 2 such that A741: g2/.(n+1)=u1 & u1`2=ppi`2 & ppi`1<=u1`1 & u1`1<=pj`1 by A739; consider u2 be Point of TOP-REAL 2 such that A742: g2/.(n+2)=u2 & u2`2=ppi`2 & ppi`1<=u2`1 & u2`1<=pj`1 by A739; set lg = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & u`1<=w`1 & w`1<=u2`1}; A743: 1<= n+1 by NAT_1:29; A744: n+1+1 = n+(1+1) by XCMPLX_1:1; n+1 <= n+2 by AXIOMS:24; then n+1 <= len g2 by A737,AXIOMS:22; then A745: LSeg(g2,n)=LSeg(u,u1) & LSeg(g2,n+1)=LSeg(u1,u2) & LSeg(g2/.n,g2/.(n+2))=LSeg(u,u2) by A737,A740,A741,A742,A743,A744,TOPREAL1:def 5; n<n+1 & n+1<n+1+1 & n+1+1=n+(1+1) by NAT_1:38,XCMPLX_1:1; then A746: u1`1<u2`1 & u`1<u1`1 by A728,A738,A740,A741,A742; then A747: u1`1<=u2`1 & u`1<=u1`1 & u`1<u2`1 by AXIOMS:22; A748: u1 in lg & u=|[u`1,u`2]| & u2=|[u2`1,u2`2]| by A741,A746,EUCLID :57; then LSeg(g2/.n,g2/.(n+2))=lg by A740,A742,A747,TOPREAL3:16; hence thesis by A741,A745,A748,TOPREAL1:14; end; thus g is unfolded proof let n; assume A749: 1<=n & n+2 <= len g; then n+(1+1)<=len g; then A750: n+1+1<=len g by XCMPLX_1:1; A751: 1<= n+1 by NAT_1:29; A752: n<=n+1 & n+1<=n+1+1 by NAT_1:29; then A753: n+1 <= len g by A750,AXIOMS:22; A754: n+(1+1)=n+1+1 by XCMPLX_1:1; A755: len g=len g1+len g2 by FINSEQ_1:35; n+2-len g1 = n-len g1 +2 by XCMPLX_1:29; then A756: n-len g1 + 2 <= len g2 by A749,A755,REAL_1:86; per cases; suppose A757: n+2 <= len g1; then n in dom g1 & n+1 in dom g1 & n+2 in dom g1 & n+(1+1)=n+1+1 by A749,GOBOARD2:4,XCMPLX_1:1; then LSeg(g1,n)=LSeg(g,n) & LSeg(g1,n+1)=LSeg(g,n+1) & g/.(n+1)=g1/.(n+1) by GROUP_5:95,TOPREAL3:25; hence thesis by A30,A749,A757,TOPREAL1:def 8; suppose len g1 < n+2; then len g1+1<=n+2 by NAT_1:38; then len g1<=n+2-1 by REAL_1:84; then A758: len g1<=n+(1+1-1) by XCMPLX_1:29; now per cases; suppose A759: len g1=n+1; now assume A760: k=1; 1<len g1 by A749,A759,NAT_1:38; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A760,TOPREAL1:29; end; then A761: 1<k & LSeg(g1,n) c= L~f1 by A14,A33,REAL_1:def 5,TOPREAL3:26; then A762: L~f1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,GOBOARD2:9; 1<=n+1 by NAT_1:29; then A763: n in dom g1 & n+1 in dom g1 by A749,A752,A759,FINSEQ_3:27; then A764: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; A765: g/.(n+1)=f1/.len f1 by A35,A759,A763,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; n+2 = 1+len g1 & 1 <= len g2 by A749,A754,A755,A759,REAL_1:53; then A766: g/.(n+2)=g2/.1 by GOBOARD2:5; 1<=len g-len g1 by A750,A759,REAL_1:84; then 1<=len g2 by A755,XCMPLX_1:26; then 1 in dom g2 by FINSEQ_3:27; then A767: g2/.1 in rng g2 by PARTFUN2:4; then g2/.1 in lk by A715,A732; then consider u1 be Point of TOP-REAL 2 such that A768: g2/.1=u1 & u1`2=ppi`2 & ppi`1<=u1`1 & u1`1<=pj`1; ppi in LSeg(ppi,pj) by TOPREAL1:6; then LSeg(ppi,u1) c= LSeg(f,k) & LSeg(g,n+1)=LSeg(ppi,u1) by A716,A732,A749,A751,A754,A765,A766,A767,A768,TOPREAL1:12,def 5; then A769: LSeg(g,n) /\ LSeg(g,n+1) c= {g/.(n+1)} by A47,A761,A762,A764,A765,XBOOLE_1:27; g/.(n+1) in LSeg(g,n) & g/.(n+1) in LSeg(g,n+1) by A749,A751,A753,A754,TOPREAL1:27; then g/.(n+1) in LSeg(g,n) /\ LSeg(g,n+1) by XBOOLE_0:def 3; then {g/.(n+1)} c= LSeg(g,n) /\ LSeg(g,n+1) by ZFMISC_1:37; hence thesis by A769,XBOOLE_0:def 10; suppose len g1<>n+1; then len g1<n+1 by A758,REAL_1:def 5; then A770: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; now per cases; suppose A771: len g1=n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A772: g/.n=f1/.len f1 by A35,A771,GROUP_5:95 .= ppi by A15,A16,A18,A47,GOBOARD1:10; A773: 2 <= len g2 by A749,A755,A771,REAL_1:53; then 1 <= len g2 by AXIOMS:22; then A774: g/.(n+1)=g2/.1 by A771,GOBOARD2:5; A775: g/.(n+2)=g2/.2 by A771,A773,GOBOARD2:5; 1<=len g2 by A773,AXIOMS:22; then A776: 1 in dom g2 & 2 in dom g2 by A773,FINSEQ_3:27; then g2/.1 in rng g2 & g2/.2 in rng g2 by PARTFUN2:4; then A777: g2/.1 in lk & g2/.2 in lk by A715,A732; then consider u1 be Point of TOP-REAL 2 such that A778: g2/.1=u1 & u1`2=ppi`2 & ppi`1<=u1`1 & u1`1<=pj`1; consider u2 be Point of TOP-REAL 2 such that A779: g2/.2=u2 & u2`2=ppi`2 & ppi`1<=u2`1 & u2`1<=pj`1 by A777; A780: u1`1<u2`1 by A728,A776,A778,A779; then A781: u1`1<=u2`1 & ppi`1<u2`1 & u2=|[u2`1,u2`2]| by A778,AXIOMS:22,EUCLID:57; set lg = {w where w is Point of TOP-REAL 2 : w`2=ppi`2 & ppi`1<=w`1 & w`1<=u2`1}; A782: u1 in lg by A778,A780; A783: LSeg(g,n)=LSeg(ppi,u1) & LSeg(g,n+1)=LSeg(u1,u2) by A749,A751,A753,A754,A772,A774,A775,A778,A779,TOPREAL1:def 5; u1 in LSeg(ppi,u2) by A714,A779,A781,A782,TOPREAL3:16; hence thesis by A774,A778,A783,TOPREAL1:14; suppose len g1<>n; then A784: len g1<n by A770,REAL_1:def 5; n1 + len g1 = n by XCMPLX_1:27; then A785: LSeg(g,n)=LSeg(g2,n1) by A753,A784,GOBOARD2:10; A786: len g1<n+1 by A752,A784,AXIOMS:22; A787: len g1+1<=n by A784,NAT_1:38; A788: n+1 = (n1+len g1)+1 by XCMPLX_1:27 .= n1+1+len g1 by XCMPLX_1:1; A789: 1<=n1+1 by NAT_1:29; n1+1<=len g2 by A753,A755,A788,REAL_1:53; then LSeg(g,n+1)=LSeg(g2,n1+1)& g/.(n+1)=g2/.(n1+1) & 1<=n1 by A750,A786,A787,A788,A789,GOBOARD2:5,10,REAL_1:84; hence thesis by A736,A756,A785; end; hence thesis; end; hence thesis; end; for n,m st m>n+1 & n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 holds LSeg(g2,n) misses LSeg(g2,m) proof let n,m; assume that A790: m>n+1 and A791: n in dom g2 & n+1 in dom g2 & m in dom g2 & m+1 in dom g2 and A792: LSeg(g2,n) /\ LSeg(g2,m) <> {}; A793: 1 <= n & n+1 <= len g2 & 1 <= m & m+1<= len g2 by A791,FINSEQ_3:27; reconsider p1=g2/.n, p2=g2/.(n+1), q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lp = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & p1`1<=w`1 & w`1<=p2`1}, lq = {w where w is Point of TOP-REAL 2: w`2=ppi`2 & q1`1<=w`1 & w`1<=q2`1}; m<m+1 & n<n+1 by NAT_1:38; then A794: p1`1<p2`1 & q1`1<q2`1 & p1`2=ppi`2 & p2`2=ppi`2 & q1`2= ppi`2 & q2`2=ppi`2 & p1=|[p1`1,p1`2]| & q1=|[q1`1,q1`2]| & p2=|[p2`1,p2`2]| & q2=|[q2`1,q2`2]| by A723,A728,A791,EUCLID:57; A795: LSeg(g2,n) = LSeg(p1,p2) by A793,TOPREAL1:def 5 .=lp by A794,TOPREAL3:16; A796: LSeg(g2,m) = LSeg(q1,q2) by A793,TOPREAL1:def 5 .=lq by A794,TOPREAL3:16; consider x being Element of LSeg(g2,n) /\ LSeg(g2,m); A797: x in LSeg(g2,n) & x in LSeg(g2,m) by A792,XBOOLE_0:def 3; then A798: ex tn be Point of TOP-REAL 2 st tn=x & tn`2=ppi`2 & p1`1<=tn`1 & tn`1<=p2`1 by A795; A799: ex tm be Point of TOP-REAL 2 st tm=x & tm`2=ppi`2 & q1`1<=tm`1 & tm`1<=q2`1 by A796,A797; p2`1<q1`1 by A728,A790,A791; hence contradiction by A798,A799,AXIOMS:22; end; then A800: g2 is s.n.c. by GOBOARD2:6; A801: L~g2 c= LSeg(f,k) proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; let x; assume x in L~g2; then x in union ls by TOPREAL1:def 6; then consider X be set such that A802: x in X & X in ls by TARSKI:def 4; consider m such that A803: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A802; m in dom g2 & m+1 in dom g2 by A803,GOBOARD2:3; then A804: g2/.m in rng g2 & g2/.(m+1) in rng g2 by PARTFUN2:4; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; A805: LSeg(q1,q2) c= LSeg(ppi,pj) by A716,A732,A804,TOPREAL1:12; LSeg(g2,m)=LSeg(q1,q2) by A803,TOPREAL1:def 5; hence thesis by A716,A802,A803,A805; end; A806: not f/.k in L~g2 proof set ls={LSeg(g2,m): 1<=m & m+1 <= len g2}; assume f/.k in L~g2; then f/.k in union ls by TOPREAL1:def 6; then consider X be set such that A807: f/.k in X & X in ls by TARSKI:def 4; consider m such that A808: X=LSeg(g2,m) & 1<=m & m+1 <= len g2 by A807; A809: m in dom g2 & m+1 in dom g2 & m<m+1 by A808,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m, q2=g2/.(m+1) as Point of TOP-REAL 2; set lq={w where w is Point of TOP-REAL 2: w`2=ppi`2 & q1`1<=w`1 & w`1<=q2`1}; A810: q1`2=ppi`2 & q2`2=ppi`2 & q1`1<q2`1 & q1=|[q1`1,q1`2]| & q2=|[q2`1,q2`2]| by A723,A728,A809,EUCLID:57; LSeg(g2,m)=LSeg(q1,q2) by A808,TOPREAL1:def 5 .=lq by A810,TOPREAL3:16; then ex p st p=f/.k & p`2=ppi`2 & q1`1<=p`1 & p`1<=q2`1 by A807,A808 ; hence contradiction by A47,A723,A809; end; A811: L~g1 /\ L~g2 = {} proof per cases; suppose k=1; hence thesis by A37; suppose k<>1; then 1<k by A14,REAL_1:def 5; then L~g1 /\ LSeg(f,k)={f/.k} by A5,A8,A9,A33,GOBOARD2:9; then A812: L~g1 /\ L~g2 c= {f/.k} by A801,XBOOLE_1:26; now consider x being Element of L~g1 /\ L~g2; assume L~g1 /\ L~g2 <> {}; then x in {f/.k} & x in L~g2 by A812,TARSKI:def 3,XBOOLE_0:def 3 ; hence contradiction by A806,TARSKI:def 1; end; hence thesis; end; for n,m st m>n+1 & n in dom g & n+1 in dom g & m in dom g & m+1 in dom g holds LSeg(g,n) misses LSeg(g,m) proof let n,m; assume that A813: m>n+1 and A814: n in dom g & n+1 in dom g & m in dom g & m+1 in dom g; A815: 1<=n & 1<=n+1 & n+1<=len g & 1<=m & 1<=m+1 & m+1<=len g & n<=n+1 & m<=m+1 & len g=len g1+len g2 by A814,FINSEQ_1:35,FINSEQ_3:27,NAT_1:29; set l1 = {LSeg(g1,i): 1<=i & i+1 <= len g1}, l2 = {LSeg(g2,j): 1<=j & j+1 <= len g2}; A816: L~g1=union l1 & L~g2=union l2 & n+1 <= len g & m+1 <= len g by A814,FINSEQ_3:27,TOPREAL1:def 6; i1+1<=j1 by A700,NAT_1:38; then A817: 1<=l by REAL_1:84; then A818: 1 in dom g2 by A701,FINSEQ_3:27; reconsider qq=g2/.1 as Point of TOP-REAL 2; set ql={z where z is Point of TOP-REAL 2: z`2=ppi`2 & ppi`1<=z`1 & z`1<=qq`1}; A819: 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 & dom g1 c= dom g by FINSEQ_1:39,FINSEQ_3:27; then A820: g/.len g1=g1/.len g1 by GROUP_5:95 .= ppi by A15,A16,A18,A35,A47,GOBOARD1:10; A821: len g1<len g1 +1 & len g1+1<=len g by A701,A815,A817,NAT_1:38,REAL_1:55; A822: g/.(len g1+1)=qq by A701,A817,GOBOARD2:5; A823: qq`2=ppi`2 & qq`1<=pj`1 & qq`1>ppi`1 & qq=|[qq`1,qq`2]| by A723,A818,EUCLID:57; A824: LSeg(g,len g1)=LSeg(ppi,qq) by A819,A820,A821,A822,TOPREAL1:def 5 .= ql by A714,A823,TOPREAL3:16; A825: n+1<=m+1 by A813,A815,AXIOMS:22; now per cases; suppose A826: m+1<=len g1; then A827: m<=len g1 & n+1<=len g1 by A815,A825,AXIOMS:22; then n<=len g1 by A815,AXIOMS:22; then n in dom g1 & n+1 in dom g1 & m in dom g1 & m+1 in dom g1 by A815,A826,A827,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) & LSeg(g,m)=LSeg(g1,m) by TOPREAL3:25; hence thesis by A31,A813,TOPREAL1:def 9; suppose len g1<m+1; then A828: len g1<=m by NAT_1:38; then reconsider m1=m-len g1 as Nat by INT_1:18; now per cases; suppose A829: m=len g1; now assume A830: k=1; 1<len g1 by A813,A815,A829,AXIOMS:22; then 1+1<=len g1 by NAT_1:38; hence contradiction by A37,A830,TOPREAL1:29; end; then 1<k by A14,REAL_1:def 5; then A831: L~f1 /\ LSeg(f,k) ={f/.k} by A5,A8,A9,GOBOARD2:9; n<=len g1 by A813,A815,A829,AXIOMS:22; then A832: n in dom g1 & n+1 in dom g1 by A813,A815,A829,FINSEQ_3:27; then A833: LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A813,A815,A829; then A834: LSeg(g,n) c= L~f1 by A33,A816,ZFMISC_1:92; LSeg(g,m) c= LSeg(f,k) proof let x; assume x in LSeg(g,m); then consider px be Point of TOP-REAL 2 such that A835: px=x & px`2=ppi`2 & ppi`1<=px`1 & px`1<=qq`1 by A824,A829; pj`1>=px`1 by A823,A835,AXIOMS:22; hence thesis by A715,A835; end; then A836: LSeg(g,n) /\ LSeg(g,m) c= {f/.k} by A831,A834,XBOOLE_1:27; now consider x being Element of LSeg(g,n)/\ LSeg(g,m); assume LSeg(g,n)/\ LSeg(g,m)<>{}; then A837: x in LSeg(g,n) & x in {f/.k} by A836,TARSKI:def 3,XBOOLE_0:def 3; then A838: x=f/.k by TARSKI:def 1; f/.k=g1/.len g1 by A15,A16,A18,A35,GOBOARD1:10; hence contradiction by A29,A30,A31,A813,A829,A832,A833,A837, A838,GOBOARD2:7; end; hence thesis by XBOOLE_0:def 7; suppose A839: m<>len g1; m+1 = m1+len g1+1 by XCMPLX_1:27; then A840: len g1<m & m+1=m1+1+len g1 by A828,A839,REAL_1:def 5,XCMPLX_1:1; m = m1+len g1 by XCMPLX_1:27; then A841: LSeg(g,m)=LSeg(g2,m1) by A815,A840,GOBOARD2:10; m1+1<=len g2 & len g1+1<= m by A815,A840,NAT_1:38,REAL_1:53; then A842: 1<=m1 & m1+1 <= len g2 by REAL_1:84; then LSeg(g,m) in l2 by A841; then A843: LSeg(g,m) c= L~g2 by A816,ZFMISC_1:92; now per cases; suppose A844: n+1<=len g1; then n<=len g1 by A815,AXIOMS:22; then n in dom g1 & n+1 in dom g1 by A815,A844,FINSEQ_3:27; then LSeg(g,n)=LSeg(g1,n) by TOPREAL3:25; then LSeg(g,n) in l1 by A815,A844; then LSeg(g,n) c= L~g1 by A816,ZFMISC_1:92; then LSeg(g,n) /\ LSeg(g,m) c= {} by A811,A843,XBOOLE_1:27; then LSeg(g,n) /\ LSeg(g,m) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; suppose len g1<n+1; then A845: len g1<=n by NAT_1:38; then reconsider n1=n-len g1 as Nat by INT_1:18; A846: n - len g1 + 1 = n + 1 - len g1 by XCMPLX_1:29; A847: n = n1 + len g1 by XCMPLX_1:27; now per cases; suppose A848: len g1=n; now consider x being Element of LSeg(g,n) /\ LSeg(g,m); assume LSeg(g,n) /\ LSeg(g,m)<>{}; then A849: x in LSeg(g,n) & x in LSeg(g,m) by XBOOLE_0:def 3; then A850: ex qx be Point of TOP-REAL 2 st qx=x & qx`2=ppi`2 & ppi`1<=qx`1 & qx`1<=qq`1 by A824,A848; A851: m1 in dom g2 & m1+1 in dom g2 & m1<m1+1 by A842,GOBOARD2:3,NAT_1:38; reconsider q1=g2/.m1, q2=g2/.(m1+1) as Point of TOP-REAL 2; set q1l={v where v is Point of TOP-REAL 2: v`2=ppi`2 & q1`1<=v`1 & v`1<=q2`1}; A852: q1`2=ppi`2 & q2`2=ppi`2 & q1`1<q2`1 & q1=|[q1`1,q1 `2]|& q2=|[q2`1,q2`2]| by A723,A728,A851,EUCLID:57; m1 > n1 + 1 & n1 + 1 >= 1 by A813,A846,NAT_1:29,REAL_1:54; then A853: m1 > 1 by AXIOMS:22; LSeg(g2,m1)=LSeg(q1,q2) by A842,TOPREAL1:def 5 .=q1l by A852,TOPREAL3:16; then A854: ex qy be Point of TOP-REAL 2 st qy=x & qy`2=ppi`2 & q1`1<=qy`1 & qy`1<=q2`1 by A841,A849; qq`1<q1`1 by A728,A818,A851,A853; hence contradiction by A850,A854,AXIOMS:22; end; hence thesis by XBOOLE_0:def 7; suppose n<>len g1; then len g1<n by A845,REAL_1:def 5; then LSeg(g,n)=LSeg(g2,n1) & m1>n1+1 by A813,A815,A846,A847,GOBOARD2:10,REAL_1:54; hence thesis by A800,A841,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; hence thesis; end; hence thesis; end; hence g is s.n.c. by GOBOARD2:6; A855: g2 is special proof let n; set p = g2/.n, q = g2/.(n+1); assume 1<=n & n+1 <= len g2; then n in dom g2 & n+1 in dom g2 by GOBOARD2:3; then p`2=ppi`2 & q`2=ppi`2 by A723; hence p`1=q`1 or p`2=q`2; end; now set p=g1/.len g1, q=g2/.1; i1+1<=j1 by A700,NAT_1:38; then 1<=l by REAL_1:84; then 1 in dom g2 by A701,FINSEQ_3:27; then q`2=ppi`2 by A723; hence p`1=q`1 or p`2=q`2 by A15,A16,A18,A35,A47,GOBOARD1:10; end; hence g is special by A32,A855,GOBOARD2:13; 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}; A856: len g = len g1 + len g2 by FINSEQ_1:35; A857: now let j; assume A858: len g1<=j & j<=len g; then reconsider w = j-len g1 as Nat by INT_1:18; let p such that A859: p=g/.j; now per cases; suppose A860: j=len g1; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then A861: g/.len g1 = f1/.len f1 by A35,GROUP_5:95 .= G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence p`2=G*(i1,i2)`2 by A859,A860; thus G*(i1,i2)`1<=p`1 & p`1<=G* (j1,i2)`1 by A51,A56,A67,A70,A700,A713,A859,A860,A861,GOBOARD1:def 1; thus p in rng c1 by A51,A70,A712,A859,A860,A861,PARTFUN2:4; suppose j<>len g1; then A862: len g1 < j by A858,REAL_1:def 5; A863: j = w + len g1 by XCMPLX_1:27; len g1 + 1 <= j by A862,NAT_1:38; then A864: 1<=w & w<=len g2 by A856,A858,REAL_1:84,86; then A865: g/.j=g2/.w by A863,GOBOARD2:5; w in dom g2 by A864,FINSEQ_3:27; hence p`2=ppi`2 & ppi`1<=p`1 & p`1<= pj`1 & p in rng c1 by A723,A859,A865; 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 A866: x in X & X in lg by TARSKI:def 4; consider i such that A867: X=LSeg(g,i) & 1<=i & i+1 <= len g by A866; now per cases; suppose A868: 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 A867,AXIOMS:22; then i in dom g1 & i+1 in dom g1 by FINSEQ_3:27; then X=LSeg(g1,i) by A867,TOPREAL3:25; then X in {LSeg(g1,j): 1<=j & j+1 <= len g1} by A867,A868; then x in union {LSeg(g1,j): 1<=j & j+1 <= len g1} by A866,TARSKI:def 4; then x in L~f1 & L~f1 c= L~f by A33,TOPREAL1:def 6,TOPREAL3:27; hence thesis; suppose A869: i+1 > len g1; then A870: len g1<=i & i<=i+1 & i+1<=len g by A867,NAT_1:38; A871: 1<=i+1 & len g1<=i+1 & i<=len g by A867,A869,NAT_1:38; reconsider q1=g/.i, q2=g/.(i+1) as Point of TOP-REAL 2; A872: 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 A857,A870,A871; then A873: q1=|[q1`1,q1`2]| & q2=|[q2`1,q1`2]| by EUCLID:57; A874: LSeg(g,i)=LSeg(q2,q1) by A867,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 A873,A874,TOPREAL3:16; then consider p2 such that A875: p2=x & p2`2=q1`2 & q2`1<=p2`1 & p2`1<=q1`1 by A866,A867; ppi`1<=p2`1 & p2`1<=pj`1 by A872,A875,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A715,A872,A875; 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 A873,A874,TOPREAL1:7; then x=q1 by A866,A867,TARSKI:def 1; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A715,A872; 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 A873,A874,TOPREAL3:16; then consider p2 such that A876: p2=x & p2`2=q1`2 & q1`1<=p2`1 & p2`1<=q2`1 by A866,A867; ppi`1<=p2`1 & p2`1<=pj`1 by A872,A876,AXIOMS:22; then x in LSeg(f,k) & LSeg(f,k) in lf by A14,A715,A872,A876; 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 A877: x in L~f1 \/ LSeg(f,k) by A5,A12,GOBOARD2:8; now per cases by A877,XBOOLE_0:def 2; suppose x in L~f1; then x in L~g1 & L~g1 c= L~g by A33,GOBOARD2:11; hence x in L~g; suppose x in LSeg(f,k); then consider p1 such that A878: p1=x & p1`2=ppi`2 & ppi`1<=p1`1 & p1`1<=pj`1 by A715; defpred P2[Nat] means len g1<=$1 & $1<=len g & for q st q=g/.$1 holds q`1<=p1`1; A879: now take n=len g1; thus P2[n] proof 0<=len g2 by NAT_1:18; hence len g1<=n & n<=len g by A856,REAL_2:173; let q such that A880: q=g/.n; 1<=len g1 by A14,A16,A36,AXIOMS:22; then len g1 in dom g1 by FINSEQ_3:27; then q=f1/.len f1 by A35,A880,GROUP_5:95 .=G*(i1,i2) by A15,A16,A18,A47,GOBOARD1:10; hence q`1<=p1`1 by A878; end; end; A881: for n holds P2[n] implies n<=len g; consider ma be Nat such that A882: P2[ma] & for n st P2[n] holds n<=ma from Max(A881,A879); now per cases; suppose A883: ma=len g; i1+1<=j1 by A700,NAT_1:38; then A884: 1<=l by REAL_1:84; then A885: l in dom g2 & i1+l=j1 by A701,FINSEQ_3:27,XCMPLX_1:27; then A886: g/.ma=g2/.l by A701,A856,A883,GROUP_5:96 .= pj by A701,A885; then pj`1<=p1`1 by A882; then A887: p1`1=pj`1 by A878,AXIOMS:21; A888: ma-1<=len g & len g1+1<=ma by A701,A856,A883,A884,PROB_1:2,REAL_1:55; then A889: len g1<=ma-1 & 0<=len g1 by NAT_1:18,REAL_1:84; then A890: 0+1<=ma by REAL_1:84; then A891: ma in Seg ma by FINSEQ_1:3; reconsider m1=ma-1 as Nat by A890,INT_1:18; 1<=len g1 by A14,A16,A36,AXIOMS:22; then A892: 1<=m1 by A889,AXIOMS:22; then A893: m1 in dom g & Seg len g=dom g by A888,FINSEQ_1:def 3,FINSEQ_3:27; reconsider q=g/.m1 as Point of TOP-REAL 2; A894: q`2=ppi`2 & q`1<=pj`1 & q=|[q`1,q`2]| & m1+1=ma by A857,A888,A889,EUCLID:57,XCMPLX_1:27; then A895: LSeg(g,m1)=LSeg(q,pj) by A883,A886,A892,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 A49,A53,A490,A708,A710,A714,A883,A886,A891,A893,A894,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 A894,REAL_1:def 5; then LSeg(g,m1)=lq by A714,A894,A895,TOPREAL3:16; then p1 in LSeg(g,m1) & LSeg(g,m1) in lg by A878,A883,A887,A892,A894; then x in union lg by A878,TARSKI:def 4; hence x in L~g by TOPREAL1:def 6; suppose ma<>len g; then ma<len g by A882,REAL_1:def 5; then A896: ma+1<=len g & k<=ma & ma<=ma+1 by A16,A36,A882,AXIOMS:22,NAT_1:38; then A897: 1<=ma & len g1<=ma+1 by A14,A882,AXIOMS:22; reconsider qa=g/.ma, qa1=g/.(ma+1) as Point of TOP-REAL 2; A898: qa`1<=p1`1 by A882; A899: now assume qa1`1<=p1`1; then for q holds q=g/.(ma+1) implies q`1<=p1`1; then ma+1<=ma by A882,A896,A897; hence contradiction by REAL_2:174; end; then A900: qa`1<qa1`1 & qa`1<=p1`1 & p1`1<=qa1`1 & qa`2=ppi`2 & qa1 `2 = ppi`2 by A857,A882,A896,A897,A898,AXIOMS:22 ; set lma = {p2: p2`2=ppi`2 & qa`1<=p2`1 & p2`1<=qa1`1}; A901: qa=|[qa`1,qa`2]| & qa1=|[qa1 `1, qa1 `2]| by EUCLID:57; LSeg(g,ma)=LSeg(qa,qa1) by A896,A897,TOPREAL1:def 5 .= lma by A900,A901,TOPREAL3:16; then x in LSeg(g,ma) & LSeg(g,ma) in lg by A878,A896,A897,A898, A899; 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 A14,A16,A36,AXIOMS:22; then 1 in dom g1 by FINSEQ_3:27; hence g/.1=f1/.1 by A34,GROUP_5:95 .=f/.1 by A15,A19,GOBOARD1:10; i1+1<=j1 by A700,NAT_1:38; then A902: 1<=l by REAL_1:84; then A903: l in dom g2 & len g=len g1 + l by A701,FINSEQ_1:35,FINSEQ_3: 27; hence g/.len g=g2/.l by GROUP_5:96 .=G*(i1+l,i2) by A701,A903 .=f/.len f by A5,A49,A490,XCMPLX_1:27; thus len f<=len g by A5,A16,A36,A902,A903,REAL_1:55; end; hence thesis; end; hence thesis; end; for k holds P[k] from Ind(A1,A3); hence thesis; 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_S-Seq implies ex g st g is_sequence_on G & g is_S-Seq & L~f = L~g & f/.1 = g/.1 & f/.len f = g/.len g & len f<=len g proof assume that A1: for n st n in dom f ex i,j st [i,j] in Indices G & f/.n=G*(i,j) and A2: f is_S-Seq; A3: f is one-to-one & 2<=len f & f is unfolded s.n.c. special by A2,TOPREAL1:def 10; then consider g such that A4: g is_sequence_on G and A5: g is one-to-one unfolded s.n.c. special & L~f = L~g & f/.1 = g/.1 & f/.len f = g/.len g & len f <= len g by A1,Th1; take g; thus g is_sequence_on G by A4; 2<=len g by A3,A5,AXIOMS:22; hence g is_S-Seq by A5,TOPREAL1:def 10; thus thesis by A5; end;