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;