Copyright (c) 1995 Association of Mizar Users
environ vocabulary EUCLID, FINSEQ_1, PRE_TOPC, ARYTM, MCART_1, TOPREAL1, FINSEQ_5, RELAT_1, FINSEQ_4, BOOLE, RFINSEQ, ARYTM_1, TARSKI, FUNCT_1, REALSET1, TOPREAL4, RCOMP_1, COMPTS_1, BORSUK_1, TOPS_2, ORDINAL2, SUBSET_1, SPPOL_2; notation TARSKI, XBOOLE_0, ORDINAL1, XREAL_0, STRUCT_0, REAL_1, NAT_1, FUNCT_1, FINSEQ_1, REALSET1, FINSEQ_4, RFINSEQ, PRE_TOPC, COMPTS_1, TOPS_2, EUCLID, BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5; constructors TOPMETR, REAL_1, NAT_1, REALSET1, RFINSEQ, COMPTS_1, TOPS_2, TOPREAL1, TOPREAL4, FINSEQ_4, FINSEQ_5, INT_1, MEMBERED, XBOOLE_0; clusters PRE_TOPC, FINSEQ_5, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1, INT_1, TOPREAL1, MEMBERED, ZFMISC_1, XBOOLE_0, ORDINAL2; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0; theorems TARSKI, AXIOMS, ENUMSET1, ZFMISC_1, REAL_1, NAT_1, RLVECT_1, SQUARE_1, REAL_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, TOPS_2, HEINE, TOPMETR, COMPTS_1, RFINSEQ, EUCLID, TOPREAL1, TOPREAL3, TOPREAL4, GOBOARD1, GOBOARD2, SPPOL_1, FINSEQ_5, RELAT_1, GROUP_5, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1; schemes FINSEQ_2, COMPLSP1; begin :: Segments in TOP-REAL 2 reserve P for Subset of TOP-REAL 2, f,f1,f2,g for FinSequence of TOP-REAL 2, p,p1,p2,q,q1,q2 for Point of TOP-REAL 2, r1,r2,r1',r2' for Real, i,j,k,n for Nat; theorem Th1: for r1, r2, r1', r2' being real number st |[ r1,r2 ]| = |[ r1',r2' ]| holds r1 = r1' & r2 = r2' proof let r1, r2, r1', r2' be real number; |[r1,r2]|`1=r1 & |[r1,r2]|`2=r2 & |[r1',r2']|`1=r1' & |[r1',r2']|`2=r2' by EUCLID:56; hence thesis; end; theorem Th2: i+j = len f implies LSeg(f,i) = LSeg(Rev f,j) proof assume A1: i+j = len f; per cases; suppose that A2: 1 <= i and A3: i + 1 <= len f; A4: i in dom f by A2,A3,GOBOARD2:3; A5: i+1 in dom f by A2,A3,GOBOARD2:3; A6: i+(j+1) = len f + 1 by A1,XCMPLX_1:1; then j+1 in dom Rev f by A4,FINSEQ_5:62; then A7: j+1 <= len Rev f by FINSEQ_3:27; A8: i+1+j = len f + 1 by A1,XCMPLX_1:1; then j in dom Rev f by A5,FINSEQ_5:62; then A9: 1 <= j by FINSEQ_3:27; thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A2,A3,TOPREAL1:def 5 .= LSeg((Rev f)/.(j+1),f/.(i+1)) by A4,A6,FINSEQ_5:69 .= LSeg((Rev f)/.j,(Rev f)/.(j+1)) by A5,A8,FINSEQ_5:69 .= LSeg(Rev f,j) by A7,A9,TOPREAL1:def 5; suppose A10: not 1 <= i; then i = 0 by RLVECT_1:98; then not j+1 <= len f by A1,NAT_1:38; then not j+1 <= len Rev f by FINSEQ_5:def 3; then LSeg(f,i) = {} & LSeg(Rev f,j) = {} by A10,TOPREAL1:def 5; hence thesis; suppose A11: not i+1 <= len f; then j < 1 by A1,AXIOMS:24; then LSeg(f,i) = {} & LSeg(Rev f,j) = {} by A11,TOPREAL1:def 5; hence thesis; end; theorem Th3: i+1 <= len(f|n) implies LSeg(f|n,i) = LSeg(f,i) proof assume A1: i+1 <= len(f|n); per cases; suppose i <> 0; then A2: 1 <= i by RLVECT_1:99; then A3: i in dom(f|n) by A1,GOBOARD2:3; A4: i+1 in dom(f|n) by A1,A2,GOBOARD2:3; len(f|n) <= len f by FINSEQ_5:18; then A5: i+1 <= len f by A1,AXIOMS:22; thus LSeg(f|n,i) = LSeg((f|n)/.i,(f|n)/.(i+1)) by A1,A2,TOPREAL1:def 5 .= LSeg(f/.i,(f|n)/.(i+1)) by A3,TOPREAL1:1 .= LSeg(f/.i,f/.(i+1)) by A4,TOPREAL1:1 .= LSeg(f,i) by A2,A5,TOPREAL1:def 5; suppose A6: i = 0; hence LSeg(f|n,i) = {} by TOPREAL1:def 5 .= LSeg(f,i) by A6,TOPREAL1:def 5; end; theorem Th4: n <= len f & 1 <= i implies LSeg(f/^n,i) = LSeg(f,n+i) proof assume that A1: n <= len f and A2: 1 <= i; per cases; suppose A3: i+1 <= len f - n; 1<=i+1 by NAT_1:29; then 1 <= len f - n by A3,AXIOMS:22; then A4: 1+n <= len f by REAL_1:84; n <= 1+n by NAT_1:29; then n <= len f by A4,AXIOMS:22; then A5: len(f/^n) = len f - n by RFINSEQ:def 2; then A6: i in dom(f/^n) by A2,A3,GOBOARD2:3; A7: i+1 in dom(f/^n) by A2,A3,A5,GOBOARD2:3; i <= i+n by NAT_1:29; then A8: 1 <= i+n by A2,AXIOMS:22; i+1+n <= len f by A3,REAL_1:84; then A9: i+n+1 <= len f by XCMPLX_1:1; thus LSeg(f/^n,i) = LSeg((f/^n)/.i,(f/^n)/.(i+1)) by A2,A3,A5,TOPREAL1:def 5 .= LSeg(f/.(i+n),(f/^n)/.(i+1)) by A6,FINSEQ_5:30 .= LSeg(f/.(i+n),f/.(i+1+n)) by A7,FINSEQ_5:30 .= LSeg(f/.(i+n),f/.(i+n+1)) by XCMPLX_1:1 .= LSeg(f,n+i) by A8,A9,TOPREAL1:def 5; suppose A10: i+1 > len f - n; then n+(i+1) > len f by REAL_1:84; then A11: n+i+1 > len f by XCMPLX_1:1; i+1 > len(f/^n) by A1,A10,RFINSEQ:def 2; hence LSeg(f/^n,i) = {} by TOPREAL1:def 5 .= LSeg(f,n+i) by A11,TOPREAL1:def 5; end; theorem Th5: 1 <= i & i+1 <= len f - n implies LSeg(f/^n,i) = LSeg(f,n+i) proof assume A1: 1 <= i; assume i+1 <= len f - n; then A2: i+1+n <= len f by REAL_1:84; n <= i+1+n by NAT_1:29; then n <= len f by A2,AXIOMS:22; hence thesis by A1,Th4; end; theorem Th6: i+1 <= len f implies LSeg(f^g,i) = LSeg(f,i) proof assume A1: i+1 <= len f; per cases; suppose i <> 0; then A2: 1 <= i by RLVECT_1:99; then A3: i in dom f by A1,GOBOARD2:3; A4: i+1 in dom f by A1,A2,GOBOARD2:3; len(f^g) = len f + len g by FINSEQ_1:35; then len(f^g) >= len f by NAT_1:29; then A5: i+1 <= len(f^g) by A1,AXIOMS:22; thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 5 .= LSeg((f^g)/.i,f/.(i+1)) by A3,GROUP_5:95 .= LSeg((f^g)/.i,(f^g)/.(i+1)) by A4,GROUP_5:95 .= LSeg(f^g,i) by A2,A5,TOPREAL1:def 5; suppose A6: i = 0; hence LSeg(f^g,i) = {} by TOPREAL1:def 5 .= LSeg(f,i) by A6,TOPREAL1:def 5; end; theorem Th7: 1 <= i implies LSeg(f^g,len f + i) = LSeg(g,i) proof assume A1: 1 <= i; per cases; suppose A2: i+1 <= len g; then A3: i in dom g by A1,GOBOARD2:3; A4: i+1 in dom g by A1,A2,GOBOARD2:3; i <= len f+i by NAT_1:29; then A5: 1 <= len f+i by A1,AXIOMS:22; A6: len f +(i+1) = len f+i+1 by XCMPLX_1:1; then len f +i+1 <= len f + len g by A2,AXIOMS:24; then A7: len f+i+1 <= len(f^g) by FINSEQ_1:35; thus LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A1,A2,TOPREAL1:def 5 .= LSeg((f^g)/.(len f+i),g/.(i+1)) by A3,GROUP_5:96 .= LSeg((f^g)/.(len f+i), (f^g)/.(len f + (i+1))) by A4,GROUP_5:96 .= LSeg(f^g,len f + i) by A5,A6,A7,TOPREAL1:def 5; suppose A8: i+1 > len g; then len f + (i + 1) > len f + len g by REAL_1:53; then len f + (i + 1) > len(f^g) by FINSEQ_1:35; then len f + i + 1 > len(f^g) by XCMPLX_1:1; hence LSeg(f^g,len f + i) = {} by TOPREAL1:def 5 .= LSeg(g,i) by A8,TOPREAL1:def 5; end; theorem Th8: f is non empty & g is non empty implies LSeg(f^g,len f) = LSeg(f/.len f,g/.1) proof assume that A1: f is non empty and A2: g is non empty; A3: len f in dom f by A1,FINSEQ_5:6; A4: 1 in dom g by A2,FINSEQ_5:6; A5: 1 <= len f by A3,FINSEQ_3:27; 1 <= len g by A4,FINSEQ_3:27; then len f + 1 <= len f + len g by AXIOMS:24; then len f + 1 <= len(f^g) by FINSEQ_1:35; hence LSeg(f^g,len f) = LSeg((f^g)/.(len f),(f^g)/.(len f+1)) by A5,TOPREAL1:def 5 .= LSeg(f/.len f,(f^g)/.(len f+1)) by A3,GROUP_5:95 .= LSeg(f/.len f,g/.1) by A4,GROUP_5:96; end; theorem Th9: i+1 <= len(f-:p) implies LSeg(f-:p,i) = LSeg(f,i) proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis by Th3; end; theorem Th10: p in rng f implies LSeg(f:-p,i+1) = LSeg(f,i+p..f) proof assume A1: p in rng f; A2: 1 <= i+1 by NAT_1:29; A3: i+(1+1) = i+1+1 by XCMPLX_1:1; A4: len (f:-p) = len f - p..f + 1 by A1,FINSEQ_5:53; per cases; suppose A5: i+2 <= len(f:-p); then A6: i+1 in dom(f:-p) by A2,A3,GOBOARD2:3; A7: i+1+1 in dom(f:-p) by A2,A3,A5,GOBOARD2:3; 1 <= p..f by A1,FINSEQ_4:31; then i+1 <= i+p..f by AXIOMS:24; then A8: 1 <= i+p..f by A2,AXIOMS:22; i+1 <= len f - p..f by A3,A4,A5,REAL_1:53; then i+1+p..f <= len f by REAL_1:84; then A9: i+p..f+1 <= len f by XCMPLX_1:1; thus LSeg(f:-p,i+1) = LSeg((f:-p)/.(i+1),(f:-p)/.(i+1+1)) by A2,A3,A5,TOPREAL1:def 5 .= LSeg(f/.(i+p..f),(f:-p)/.(i+1+1)) by A1,A6,FINSEQ_5:55 .= LSeg(f/.(i+p..f),f/.(i+1+p..f)) by A1,A7,FINSEQ_5:55 .= LSeg(f/.(i+p..f),f/.(i+p..f+1)) by XCMPLX_1:1 .= LSeg(f,i+p..f) by A8,A9,TOPREAL1:def 5; suppose A10: i+2 > len(f:-p); then i+1 > len f - p..f by A3,A4,AXIOMS:24; then p..f+(i+1) > len f by REAL_1:84; then i+p..f+1 > len f by XCMPLX_1:1; hence LSeg(f,i+p..f) = {} by TOPREAL1:def 5 .= LSeg(f:-p,i+1) by A3,A10,TOPREAL1:def 5; end; theorem Th11: L~<*>(the carrier of TOP-REAL 2) = {} proof len(<*>(the carrier of TOP-REAL 2)) = 0 by FINSEQ_1:32; hence thesis by TOPREAL1:28; end; theorem Th12: L~<*p*> = {} proof len <*p*> = 1 by FINSEQ_1:56; hence thesis by TOPREAL1:28; end; theorem Th13: p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f,i) proof assume A1: p in L~f; set X = { LSeg(f,i) : 1 <= i & i+1 <= len f}; L~f = union X by TOPREAL1:def 6; then consider Y being set such that A2: p in Y and A3: Y in X by A1,TARSKI:def 4; ex i st Y = LSeg(f,i) & 1 <= i & i+1 <= len f by A3; hence thesis by A2; end; theorem Th14: p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1)) proof assume p in L~f; then consider i such that A1: 1 <= i & i+1 <= len f and A2: p in LSeg(f,i) by Th13; take i; thus 1 <= i & i+1 <= len f by A1; thus thesis by A1,A2,TOPREAL1:def 5; end; theorem Th15: 1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1)) implies p in L~f proof assume that A1: 1 <= i and A2: i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)); set X = { LSeg(f,j) : 1 <= j & j+1 <= len f }; A4: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 5; LSeg(f,i) in X by A1,A2; then p in union X by A3,A4,TARSKI:def 4; hence p in L~f by TOPREAL1:def 6; end; theorem 1 <= i & i+1 <= len f implies LSeg(f/.i,f/.(i+1)) c= L~f proof assume 1 <= i & i+1 <= len f; then LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by TOPREAL1:def 5; hence thesis by TOPREAL3:26; end; theorem p in LSeg(f,i) implies p in L~f proof LSeg(f,i) c= L~f by TOPREAL3:26; hence thesis; end; theorem Th18: len f >= 2 implies rng f c= L~f proof assume A1: len f >= 2; let x be set; assume x in rng f; then consider i such that A2: i in dom f and A3: f/.i = x by PARTFUN2:4; A4: 1 <= i by A2,FINSEQ_3:27; A5: i <= len f by A2,FINSEQ_3:27; A6: f/.i in LSeg(f/.i,f/.(i+1)) by TOPREAL1:6; per cases; suppose A7: i = len f; then i <>0 by A1; then consider j such that A8: j+1 = i by NAT_1:22; A9: f/.(j+1) in LSeg(f/.j,f/.(j+1)) by TOPREAL1:6; 1+1 <= j+1 by A1,A7,A8; then 1 <= j by REAL_1:53; hence x in L~f by A3,A7,A8,A9,Th15; suppose i <> len f; then i < len f by A5,REAL_1:def 5; then i+1 <= len f by NAT_1:38; hence x in L~f by A3,A4,A6,Th15; end; theorem Th19: f is non empty implies L~(f^<*p*>) = L~f \/ LSeg(f/.len f,p) proof assume that A1: f is non empty; set fp = f^<*p*>; A2: len fp = len f + 1 by FINSEQ_2:19; 1 <= len f + 1 & len f + 1 <= len fp by FINSEQ_2:19,NAT_1:29; then A3: len f + 1 in dom fp by FINSEQ_3:27; A4: len f in dom f by A1,FINSEQ_5:6; then A5: fp/.len f = f/.len f by GROUP_5:95; A6: fp/.(len f + 1) = p by TOPREAL4:1; A7: fp|(len f + 1) = fp by A2,TOPREAL1:2; A8: dom f c= dom(fp) by FINSEQ_1:39; fp|len f = f by FINSEQ_5:26; hence thesis by A3,A4,A5,A6,A7,A8,TOPREAL3:45; end; theorem Th20: f is non empty implies L~(<*p*>^f) = LSeg(p,f/.1) \/ L~f proof assume that A1: f is non empty; set q = f/.1; A2: len f <> 0 by A1,FINSEQ_1:25; A3: len <*p*> = 1 by FINSEQ_1:56; then A4: len (<*p*>^f) = 1 + len f by FINSEQ_1:35; hereby let x be set; assume A5: x in L~(<*p*>^f); then reconsider r = x as Point of TOP-REAL 2; consider i such that A6: 1 <= i and A7: i+1 <= len (<*p*>^f) and A8: r in LSeg((<*p*>^f)/.i,(<*p*>^f)/.(i+1)) by A5,Th14; now per cases by A6,REAL_1:def 5; case A9: i = 1; then A10: p = (<*p*>^f)/.i by FINSEQ_5:16; i in dom f by A1,A9,FINSEQ_5:6; hence r in LSeg(p,q) by A3,A8,A9,A10,GROUP_5:96; case A11: i > 1; then i <> 0; then consider j such that A12: i = j + 1 by NAT_1:22; A13: 1 <= j by A11,A12,NAT_1:38; A14: j+1 <= len f by A4,A7,A12,REAL_1:53; then j in dom f by A13,GOBOARD2:3; then A15: (<*p*>^f)/.i = f/.j by A3,A12,GROUP_5:96; j+1 in dom f by A13,A14,GOBOARD2:3; then (<*p*>^f)/.(i+1) = f/.(j+1) by A3,A12,GROUP_5:96; hence r in L~f by A8,A13,A14,A15,Th15; end; hence x in LSeg(p,q) \/ L~f by XBOOLE_0:def 2; end; let x be set; assume A16: x in LSeg(p,q) \/ L~f; then reconsider r = x as Point of TOP-REAL 2; per cases by A16,XBOOLE_0:def 2; suppose A17: r in LSeg(p,q); set i = 1; i <= len f by A2,RLVECT_1:99; then A18: i+1 <= len(<*p*>^f) by A4,AXIOMS:24; A19: p = (<*p*>^f)/.i by FINSEQ_5:16; i in dom f by A1,FINSEQ_5:6; then q = (<*p*>^f)/.(i+1) by A3,GROUP_5:96; hence x in L~(<*p*>^f) by A17,A18,A19,Th15; suppose r in L~f; then consider j such that A20: 1 <= j and A21: j+1 <= len f and A22: r in LSeg(f/.j,f/.(j+1)) by Th14; set i = j + 1; A23: 1 <= i by NAT_1:37; A24: i+1 <= len (<*p*>^f) by A4,A21,AXIOMS:24; j in dom f by A20,A21,GOBOARD2:3; then A25: (<*p*>^f)/.i = f/.j by A3,GROUP_5:96; j+1 in dom f by A20,A21,GOBOARD2:3; then (<*p*>^f)/.(i+1) = f/.(j+1) by A3,GROUP_5:96; hence x in L~(<*p*>^f) by A22,A23,A24,A25,Th15; end; theorem Th21: L~<*p,q*> = LSeg(p,q) proof set f = <*p*>; A1: len f = 1 by FINSEQ_1:56; thus L~<*p,q*> = L~(f^<*q*>) by FINSEQ_1:def 9 .= L~f \/ LSeg(f/.len f,q) by Th19 .= L~f \/ LSeg(p,q) by A1,FINSEQ_4:25 .= {} \/ LSeg(p,q) by A1,TOPREAL1:28 .= LSeg(p,q); end; theorem Th22: L~f = L~(Rev f) proof defpred P[FinSequence of TOP-REAL 2] means L~$1 = L~(Rev $1); A1: P[<*>(the carrier of TOP-REAL 2)]; A2: for f,p st P[f] holds P[f^<*p*>] proof let f,p such that A3: P[f]; per cases; suppose A4: f is empty; hence L~(f^<*p*>) = L~<*p*> by FINSEQ_1:47 .= L~(Rev <*p*>) by FINSEQ_5:63 .= L~(Rev(f^<*p*>)) by A4,FINSEQ_1:47; suppose A5: f is non empty; then A6: len f <> 0 by FINSEQ_1:25; set q = f/.len f; A7: len f = len Rev f by FINSEQ_5:def 3; set q' = (Rev f)/.1; A8: q = q' by A5,FINSEQ_5:68; A9: Rev f is non empty by A6,A7,FINSEQ_1:25; thus L~(f^<*p*>) = LSeg(p,q') \/ L~(Rev f) by A3,A5,A8,Th19 .= L~(<*p*>^(Rev f)) by A9,Th20 .= L~(Rev(f^<*p*>)) by FINSEQ_5:66; end; for f holds P[f] from IndSeqD(A1,A2); hence thesis; end; theorem Th23: f1 is non empty & f2 is non empty implies L~(f1^f2) = L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 proof set p = f1/.len f1, q = f2/.1; assume A1: f1 is non empty; assume f2 is non empty; then A2: f2 = <*q*>^(f2/^1) by FINSEQ_5:32; defpred P[FinSequence of TOP-REAL 2] means L~(f1^<*q*>^$1) = L~f1 \/ LSeg(p,q) \/ L~(<*q*>^$1); A3: P[<*>(the carrier of TOP-REAL 2)] proof set O = <*>(the carrier of TOP-REAL 2); thus L~(f1^<*q*>^O) = L~(f1^<*q*>) by FINSEQ_1:47 .= L~f1 \/ LSeg(p,q) \/ {} by A1,Th19 .= L~f1 \/ LSeg(p,q) \/ L~<*q*> by Th12 .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^O) by FINSEQ_1:47; end; A4: for f for o being Point of TOP-REAL 2 st P[f] holds P[f^<*o*>] proof let f; let o be Point of TOP-REAL 2 such that A5: P[f]; A6: f1^<*q*> is non empty by FINSEQ_1:48; per cases; suppose f is empty; then A7: (f^<*o*>) = <*o*> by FINSEQ_1:47; len(f1^<*q*>) = len f1 + 1 by FINSEQ_2:19; then (f1^<*q*>)/.len(f1^<*q*>) = q by TOPREAL4:1; hence L~(f1^<*q*>^(f^<*o*>)) = L~(f1^<*q*>) \/ LSeg(q,o) by A6,A7,Th19 .= L~f1 \/ LSeg(p,q) \/ LSeg(q,o) by A1,Th19 .= L~f1 \/ LSeg(p,q) \/ L~<*q,o*> by Th21 .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A7,FINSEQ_1:def 9; suppose A8: f is non empty; set g = f1^<*q*>^f, h = <*q*>^f; A9: g is non empty by A6,FINSEQ_1:48; A10: h is non empty by FINSEQ_1:48; len f <> 0 by A8,FINSEQ_1:25; then consider f' being FinSequence of TOP-REAL 2, d being Point of TOP-REAL 2 such that A11: f = f'^<*d*> by FINSEQ_2:22; A12: g = f1^<*q*>^f'^<*d*> & h = <*q*>^f'^<*d*> by A11,FINSEQ_1:45; then len g = len(f1^<*q*>^f')+1 & len h = len(<*q*>^f')+1 by FINSEQ_2:19; then g/.len g = d & h/.len h = d by A12,TOPREAL4:1; then A13: L~h \/ LSeg(g/.len g,o) = L~(h^<*o*>) by A10,Th19 .= L~(<*q*>^(f^<*o*>)) by FINSEQ_1:45; thus L~(f1^<*q*>^(f^<*o*>)) = L~(g^<*o*>) by FINSEQ_1:45 .= L~g \/ LSeg(g/.len g,o) by A9,Th19 .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A5,A13,XBOOLE_1:4; end; for f holds P[f] from IndSeqD(A3,A4); then L~(f1^<*q*>^(f2/^1)) = L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f2/^1)); hence L~(f1^f2) = L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 by A2,FINSEQ_1:45; end; Lm1: L~(f|n) c= L~f proof now per cases; suppose A1: n = 0; f|0 is empty; hence thesis by A1,Th11,XBOOLE_1:2; suppose A2: n <> 0; now per cases; suppose A3: n < len f; then len(f|n) = n by TOPREAL1:3; then A4: f|n is non empty by A2,FINSEQ_1:25; len(f/^n) = len f - n by A3,RFINSEQ:def 2; then len(f/^n) <> 0 by A3,XCMPLX_1:15; then A5: f/^n is non empty by FINSEQ_1:25; (f|n)^(f/^n) = f by RFINSEQ:21; then L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n) by A4,A5,Th23 .= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)) by XBOOLE_1:4; hence thesis by XBOOLE_1:7; suppose n >= len f; hence thesis by TOPREAL1:2; end; hence thesis; end; hence thesis; end; canceled; theorem Th25: q in rng f implies L~f = L~(f-:q) \/ L~(f:-q) proof assume A1: q in rng f; set n = q..f; A2: n <> 0 by A1,FINSEQ_4:31; A3: n <= len f by A1,FINSEQ_4:31; per cases by A3,REAL_1:def 5; suppose A4: n < len f; then A5: len(f|n) = n by TOPREAL1:3; then A6: f|n is non empty by A2,FINSEQ_1:25; f|n = f-:q by FINSEQ_5:def 1; then A7: (f|n)/.len(f|n) = q by A1,A5,FINSEQ_5:48; len(f/^n) = len f - n by A4,RFINSEQ:def 2; then len(f/^n) <> 0 by A4,XCMPLX_1:15; then A8: f/^n is non empty by FINSEQ_1:25; (f|n)^(f/^n) = f by RFINSEQ:21; hence L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n) by A6,A8,Th23 .= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)) by XBOOLE_1:4 .= L~(f|n) \/ L~(<*(f|n)/.len(f|n)*>^(f/^n)) by A8,Th20 .= L~(f|n) \/ L~(f:-q) by A7,FINSEQ_5:def 2 .= L~(f-:q) \/ L~(f:-q) by FINSEQ_5:def 1; suppose A9: n = len f; then A10: L~f = L~(f|n) by TOPREAL1:2 .= L~(f-:q) by FINSEQ_5:def 1; len(f/^n) = len f - n by A9,RFINSEQ:def 2 .= 0 by A9,XCMPLX_1:14; then A11: f/^n is empty by FINSEQ_1:25; f:-q = <*q*>^(f/^n) by FINSEQ_5:def 2 .= <*q*> by A11,FINSEQ_1:47; then L~(f:-q) is empty by Th12; hence thesis by A10; end; theorem Th26: p in LSeg(f,n) implies L~f = L~Ins(f,n,p) proof assume A1: p in LSeg(f,n); set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A2: g1 is non empty by FINSEQ_1:48; A3: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:19 .= p by TOPREAL4:1; A4: 1 <= n & n+1 <= len f by A1,TOPREAL1:def 5; n <= n+1 by NAT_1:29; then A5: n <= len f by A4,AXIOMS:22; then A6: len f1 = n by TOPREAL1:3; then A7: n in dom f1 by A4,FINSEQ_3:27; A8: f1 is non empty by A4,A6,FINSEQ_3:27,RELAT_1:60; 1 <= len f - n by A4,REAL_1:84; then 1 <= len f2 by A5,RFINSEQ:def 2; then A9: 1 in dom f2 by FINSEQ_3:27; A10: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A4,TOPREAL1:def 5 .= LSeg(f1/.len f1,f/.(n+1)) by A6,A7,TOPREAL1:1 .= LSeg(f1/.len f1,f2/.1) by A9,FINSEQ_5:30; thus L~Ins(f,n,p) = L~(g1^f2) by FINSEQ_5:def 4 .= L~g1 \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A2,A9,Th23,RELAT_1:60 .= L~f1 \/ LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A7,Th19,RELAT_1:60 .= L~f1 \/ (LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1)) \/ L~f2 by XBOOLE_1:4 .= L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 by A1,A3,A10,TOPREAL1:11 .= L~(f1^f2) by A8,A9,Th23,RELAT_1:60 .= L~f by RFINSEQ:21; end; begin definition cluster being_S-Seq FinSequence of TOP-REAL 2; existence proof set p = |[ 0,0 ]|, q = |[ 1,1 ]|; p`1 = 0 & p`2 = 0 & q`1 = 1 & q`2 = 1 by EUCLID:56; then <* p,|[p`1,q`2]|,q *> is_S-Seq by TOPREAL3:41; hence thesis; end; cluster being_S-Seq -> one-to-one unfolded s.n.c. special non trivial FinSequence of TOP-REAL 2; coherence proof let f; assume A1: f is being_S-Seq; then len f >= 2 by TOPREAL1:def 10; hence thesis by A1,SPPOL_1:2,TOPREAL1:def 10; end; cluster one-to-one unfolded s.n.c. special non trivial -> being_S-Seq FinSequence of TOP-REAL 2; coherence proof let f; assume A2: f is one-to-one unfolded s.n.c. special; assume f is non trivial; then len f >= 2 by SPPOL_1:2; hence thesis by A2,TOPREAL1:def 10; end; cluster being_S-Seq -> non empty FinSequence of TOP-REAL 2; coherence proof let f; assume f is being_S-Seq; then len f <> 0 by TOPREAL1:def 10; hence thesis by FINSEQ_1:25; end; end; definition cluster one-to-one unfolded s.n.c. special non trivial FinSequence of TOP-REAL 2; existence proof consider f being being_S-Seq FinSequence of TOP-REAL 2; f is one-to-one unfolded s.n.c. special non trivial; hence thesis; end; end; theorem Th27: len f <= 2 implies f is unfolded proof assume A1: len f <= 2; let i such that A2: 1 <= i; assume i+2 <= len f; then i+2 <= 2 by A1,AXIOMS:22; then i <= 2-2 by REAL_1:84; hence LSeg(f,i) /\ LSeg(f,i+1) = {f/.(i+1)} by A2,AXIOMS:22; end; Lm2: <*p,q*> is unfolded proof len <*p,q*> = 2 by FINSEQ_1:61; hence thesis by Th27; end; Lm3: f is unfolded implies f|n is unfolded proof assume A1: f is unfolded; set h = f|n; let i such that A2: 1 <= i and A3: i + 2 <= len h; A4: i+1+1 = i+(1+1) by XCMPLX_1:1; len h <= len f by FINSEQ_5:18; then A5: i+2 <= len f by A3,AXIOMS:22; A6: i+1 in dom h by A2,A3,GOBOARD2:4; i+1 <= i+2 by AXIOMS:24; then i+1 <= len h by A3,AXIOMS:22; hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,i) /\ LSeg(h,i+1) by Th3 .= LSeg(f,i) /\ LSeg(f,i+1) by A3,A4,Th3 .= {f/.(i+1)} by A1,A2,A5,TOPREAL1:def 8 .= {h/.(i+1)} by A6,TOPREAL1:1; end; Lm4: f is unfolded implies f/^n is unfolded proof assume A1: f is unfolded; per cases; suppose A2: n <= len f; set h = f/^n; let i such that A3: 1 <= i and A4: i + 2 <= len h; A5: 1 <= i+1 by NAT_1:29; A6: i+1+1 = i+(1+1) by XCMPLX_1:1; A7: len h = len f - n by A2,RFINSEQ:def 2; then n+(i+2) <= len f by A4,REAL_1:84; then A8: n+i+2 <= len f by XCMPLX_1:1; A9: i+1 in dom h by A3,A4,GOBOARD2:4; i <= n+i by NAT_1:29; then A10: 1 <= n+i by A3,AXIOMS:22; i+1 <= i+2 by AXIOMS:24; then i+1 <= len h by A4,AXIOMS:22; hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,n+i) /\ LSeg(h,i+1) by A3,A7,Th5 .= LSeg(f,n+i) /\ LSeg(f,n+(i+1)) by A4,A5,A6,A7,Th5 .= LSeg(f,n+i) /\ LSeg(f,n+i+1) by XCMPLX_1:1 .= {f/.(n+i+1)} by A1,A8,A10,TOPREAL1:def 8 .= {f/.(n+(i+1))} by XCMPLX_1:1 .= {h/.(i+1)} by A9,FINSEQ_5:30; suppose n > len f; then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 2; then len(f/^n) = 0 by FINSEQ_1:25; hence thesis by Th27; end; definition let f be unfolded FinSequence of TOP-REAL 2, n; cluster f|n -> unfolded; coherence by Lm3; cluster f/^n -> unfolded; coherence by Lm4; end; theorem Th28: p in rng f & f is unfolded implies f:-p is unfolded proof assume p in rng f; then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:52; hence thesis by Lm4; end; Lm5: f is unfolded implies f-:p is unfolded proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis by Lm3; end; definition let f be unfolded FinSequence of TOP-REAL 2, p; cluster f-:p -> unfolded; coherence by Lm5; end; theorem Th29: f is unfolded implies Rev f is unfolded proof assume A1: f is unfolded; let i such that A2: 1 <= i and A3: i + 2 <= len Rev f; A4: len Rev f = len f by FINSEQ_5:def 3; i <= i+2 by NAT_1:29; then i <= len f by A3,A4,AXIOMS:22; then reconsider j = len f - i as Nat by INT_1:18; A5: j+i = len f by XCMPLX_1:27; i+1 <= i+1+1 by NAT_1:29; then i+1 <= i+(1+1) by XCMPLX_1:1; then i+1 <= len f by A3,A4,AXIOMS:22; then reconsider j' = len f - (i+1) as Nat by INT_1:18; A6: j'+1 = len f - i - 1 + 1 by XCMPLX_1:36 .= j by XCMPLX_1:27; A7: j'+(i+1) = len f by XCMPLX_1:27; A8: j + (i+1) = len f + 1 by A5,XCMPLX_1:1; A9: dom f = Seg len f by FINSEQ_1:def 3; i+(1+1) = i+1+1 by XCMPLX_1:1; then A10: 1 <= j' by A3,A4,REAL_1:84; i in dom f by A2,A3,A4,GOBOARD2:4; then j + 1 in dom f by A9,FINSEQ_5:2; then j' + (1+1) in dom f by A6,XCMPLX_1:1; then A11: j'+2 <= len f by FINSEQ_3:27; i+1 in dom f by A2,A3,A4,GOBOARD2:4; then A12: j'+1 in dom f by A9,FINSEQ_5:2; thus LSeg(Rev f,i) /\ LSeg(Rev f,i+1) = LSeg(f,j) /\ LSeg(Rev f,i+1) by A5,Th2 .= LSeg(f,j'+1) /\ LSeg(f,j') by A6,A7,Th2 .= {f/.(j'+1)} by A1,A10,A11,TOPREAL1:def 8 .= {(Rev f)/.(i+1)} by A6,A8,A12,FINSEQ_5:69; end; theorem Th30: g is unfolded & LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1} implies <*p*>^g is unfolded proof set f = <*p*>; A1: len f = 1 by FINSEQ_1:56; assume that A2: g is unfolded and A3: LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1}; A4: f/.1 = p by FINSEQ_4:25; let i such that A5: 1 <= i and A6: i + 2 <= len(f^g); A7: len(f^g) = len f + len g by FINSEQ_1:35; A8: i+(1+1) = i+1+1 by XCMPLX_1:1; per cases; suppose A9: i = len f; now assume A10: len g = 0; i <= i+1 by NAT_1:29; then i < i+(1+1) by A8,NAT_1:38; hence contradiction by A1,A5,A6,A7,A10,AXIOMS:22; end; then 1 <= len g by RLVECT_1:99; then A11: 1 in dom g by FINSEQ_3:27; then A12: LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A9,Th8,RELAT_1:60; LSeg(f^g,i+1) = LSeg(g,1) by A9,Th7; hence thesis by A1,A3,A4,A9,A11,A12,GROUP_5:96; suppose i <> len f; then A13: i > len f by A1,A5,REAL_1:def 5; reconsider j = i - len f as Nat by A1,A5,INT_1:18; A14: len f + j = i by XCMPLX_1:27; then A15: len f + (j+1) = i+1 by XCMPLX_1:1; len f + 1 <= i by A13,NAT_1:38; then A16: 1 <= j by REAL_1:84; i+2-len f <= len g by A6,A7,REAL_1:86; then A17: j+(1+1) <= len g by XCMPLX_1:29; then A18: j+1+1 <= len g by XCMPLX_1:1; j+1 <= j+1+1 by NAT_1:29; then A19: j+1 <= len g by A18,AXIOMS:22; A20: 1 <= j+1 by NAT_1:29; A21: j+1 in dom g by A16,A19,GOBOARD2:3; thus LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(g,j) /\ LSeg(f^g,i+1) by A14,A16,Th7 .= LSeg(g,j) /\ LSeg(g,j+1) by A15,A20,Th7 .= {g/.(j+1)} by A2,A16,A17,TOPREAL1:def 8 .= {(f^g)/.(i+1)} by A15,A21,GROUP_5:96; end; theorem Th31: f is unfolded & k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,p) = {f/.len f} implies f^<*p*> is unfolded proof set g = <*p*>; assume that A1: f is unfolded and A2: k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,p) = {f/.len f}; A3: len g = 1 by FINSEQ_1:56; A4: g/.1 = p by FINSEQ_4:25; let i such that A5: 1 <= i and A6: i + 2 <= len(f^g); A7: len(f^g) = len f + len g by FINSEQ_1:35; A8: i+(1+1) = i+1+1 by XCMPLX_1:1; per cases; suppose A9: i+2 <= len f; then A10: i+1 in dom f by A5,GOBOARD2:4; i+1 <= i+1+1 by NAT_1:29; then i+1 <= len f by A8,A9,AXIOMS:22; hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(f,i) /\ LSeg(f^g,i+1) by Th6 .= LSeg(f,i) /\ LSeg(f,i+1) by A8,A9,Th6 .= {f/.(i+1)} by A1,A5,A9,TOPREAL1:def 8 .= {(f^g)/.(i+1)} by A10,GROUP_5:95; suppose A11: i + 2 > len f; A12: i+1 <= len f by A3,A6,A7,A8,REAL_1:53; then A13: f is non empty by A5,GOBOARD2:3,RELAT_1:60; len f <= i+1 by A8,A11,NAT_1:38; then A14: i+1 = len f by A12,AXIOMS:21; then k = i by A2,XCMPLX_1:2; then A15: LSeg(f^g,i) = LSeg(f,k) by A12,Th6; A16: LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A13,A14,Th8; len f in dom f by A13,FINSEQ_5:6; hence thesis by A2,A4,A14,A15,A16,GROUP_5:95; end; theorem Th32: f is unfolded & g is unfolded & k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} & LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1} implies f^g is unfolded proof assume that A1: f is unfolded and A2: g is unfolded and A3: k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} and A4: LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1}; let i such that A5: 1 <= i and A6: i + 2 <= len(f^g); A7: len(f^g) = len f + len g by FINSEQ_1:35; per cases; suppose A8: i+2 <= len f; then A9: i+1 in dom f by A5,GOBOARD2:4; A10: i+(1+1) = i+1+1 by XCMPLX_1:1; i+1 <= i+1+1 by NAT_1:29; then i+1 <= len f by A8,A10,AXIOMS:22; hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(f,i) /\ LSeg(f^g,i+1) by Th6 .= LSeg(f,i) /\ LSeg(f,i+1) by A8,A10,Th6 .= {f/.(i+1)} by A1,A5,A8,TOPREAL1:def 8 .= {(f^g)/.(i+1)} by A9,GROUP_5:95; suppose A11: i + 2 > len f; A12: i+(1+1) = i+1+1 by XCMPLX_1:1; now per cases; suppose A13: i <= len f; then A14: f is non empty by A5,FINSEQ_3:27,RELAT_1:60; len g <> 0 by A6,A7,A11; then 1 <= len g by RLVECT_1:99; then A15: 1 in dom g by FINSEQ_3:27; now per cases; suppose A16: i = len f; then A17: LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A14,A15,Th8,RELAT_1:60; LSeg(f^g,i+1) = LSeg(g,1) by A16,Th7; hence thesis by A4,A15,A16,A17,GROUP_5:96; suppose i <> len f; then i < len f by A13,REAL_1:def 5; then A18: i+1 <= len f by NAT_1:38; len f <= i+1 by A11,A12,NAT_1:38; then A19: i+1 = len f by A18,AXIOMS:21; then k = i by A3,XCMPLX_1:2; then A20: LSeg(f^g,i) = LSeg(f,k) by A18,Th6; A21: LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A14,A15,A19,Th8,RELAT_1:60; len f in dom f by A14,FINSEQ_5:6; hence thesis by A3,A19,A20,A21,GROUP_5:95; end; hence thesis; suppose A22: i > len f; then reconsider j = i - len f as Nat by INT_1:18; A23: len f + j = i by XCMPLX_1:27; then A24: len f + (j+1) = i+1 by XCMPLX_1:1; len f + 1 <= i by A22,NAT_1:38; then A25: 1 <= j by REAL_1:84; i+2-len f <= len g by A6,A7,REAL_1:86; then A26: j+(1+1) <= len g by XCMPLX_1:29; then A27: j+1+1 <= len g by XCMPLX_1:1; j+1 <= j+1+1 by NAT_1:29; then A28: j+1 <= len g by A27,AXIOMS:22; A29: 1 <= j+1 by NAT_1:29; A30: j+1 in dom g by A25,A28,GOBOARD2:3; thus LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(g,j) /\ LSeg(f^g,i+1) by A23,A25,Th7 .= LSeg(g,j) /\ LSeg(g,j+1) by A24,A29,Th7 .= {g/.(j+1)} by A2,A25,A26,TOPREAL1:def 8 .= {(f^g)/.(i+1)} by A24,A30,GROUP_5:96; end; hence thesis; end; theorem Th33: f is unfolded & p in LSeg(f,n) implies Ins(f,n,p) is unfolded proof assume that A1: f is unfolded and A2: p in LSeg(f,n); set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A3: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:19 .= p by TOPREAL4:1; A4: 1 <= n & n+1 <= len f by A2,TOPREAL1:def 5; n <= n+1 by NAT_1:29; then A5: n <= len f by A4,AXIOMS:22; then A6: len f1 = n by TOPREAL1:3; then A7: n in dom f1 by A4,FINSEQ_3:27; 1 <= len f - n by A4,REAL_1:84; then A8: 1 <= len f2 by A5,RFINSEQ:def 2; then A9: 1 in dom f2 by FINSEQ_3:27; A10: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A4,TOPREAL1:def 5; A11: f/.n = f1/.len f1 by A6,A7,TOPREAL1:1; A12: f/.(n+1) = f2/.1 by A9,FINSEQ_5:30; then A13: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) = LSeg(f1/.len f1,f2/.1) by A2,A3,A10,A11,TOPREAL1:11; A14: now len f1 <> 0 by A2,A6,TOPREAL1:def 5; then consider k such that A15: k+1 = len f1 by NAT_1:22; A16: k+(1+1) <= len f by A4,A6,A15,XCMPLX_1:1; A17: f1 is unfolded by A1,Lm3; per cases; suppose k <> 0; then A18: 1 <= k by RLVECT_1:98; LSeg(f1,k) = LSeg(f,k) by A15,Th3; then A19: LSeg(f1,k) /\ LSeg(f,n) = {f/.n} by A1,A6,A15,A16,A18,TOPREAL1:def 8; now let x be set; hereby assume x in LSeg(f1,k) /\ LSeg(f1/.len f1,p); then A20: x in LSeg(f1,k) & x in LSeg(f1/.len f1,p) by XBOOLE_0:def 3; then x in LSeg(f,n) by A10,A11,A12,A13,XBOOLE_0:def 2; then x in LSeg(f1,k) /\ LSeg(f,n) by A20,XBOOLE_0:def 3; hence x = f/.n by A19,TARSKI:def 1; end; assume A21: x = f/.n; then x in LSeg(f1,k) /\ LSeg(f,n) by A19,TARSKI:def 1; then A22: x in LSeg(f1,k) by XBOOLE_0:def 3; x in LSeg(f1/.len f1,p) by A11,A21,TOPREAL1:6; hence x in LSeg(f1,k) /\ LSeg(f1/.len f1,p) by A22,XBOOLE_0:def 3; end; then LSeg(f1,k) /\ LSeg(f1/.len f1,p) = {f1/.len f1} by A11,TARSKI:def 1 ; hence g1 is unfolded by A15,A17,Th31; suppose k = 0; then len g1 = 1+1 by A15,FINSEQ_2:19; hence g1 is unfolded by Th27; end; A23: n+1 = len g1 by A6,FINSEQ_2:19; f1/.len f1 = g1/.n by A6,A7,GROUP_5:95; then LSeg(g1,n) = LSeg(f1/.len f1,g1/.len g1) by A4,A23,TOPREAL1:def 5; then A24: LSeg(g1,n) /\ LSeg(g1/.len g1,f2/.1) = {g1/.len g1} by A2,A3,A10,A11,A12,TOPREAL1:14; now per cases; suppose len f2 = 1; then f2 = <*f2/.1*> by FINSEQ_5:15; hence g1^f2 is unfolded by A14,A23,A24,Th31; suppose len f2 <> 1; then len f2 > 1 by A8,REAL_1:def 5; then A25: 1+1 <= len f2 by NAT_1:38; then LSeg(f2,1) = LSeg(f2/.1,f2/.(1+1)) by TOPREAL1:def 5; then A26: f2/.1 in LSeg(f2,1) by TOPREAL1:6; A27: 1+1 <= len f - n by A5,A25,RFINSEQ:def 2; then n+(1+1) <= len f by REAL_1:84; then A28: {f/.(n+1)} = LSeg(f,n) /\ LSeg(f,n+1) by A1,A4,TOPREAL1:def 8 .= LSeg(f,n) /\ LSeg(f2,1) by A27,Th5; now let x be set; hereby assume x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1); then A29: x in LSeg(g1/.len g1,f2/.1) & x in LSeg(f2,1) by XBOOLE_0:def 3; then x in LSeg(f,n) by A10,A11,A12,A13,XBOOLE_0:def 2; then x in LSeg(f,n) /\ LSeg(f2,1) by A29,XBOOLE_0:def 3; hence x = f2/.1 by A12,A28,TARSKI:def 1; end; assume A30: x = f2/.1; then x in LSeg(g1/.len g1,f2/.1) by TOPREAL1:6; hence x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) by A26,A30,XBOOLE_0:def 3; end; then A31: LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) = {f2/.1} by TARSKI:def 1; f2 is unfolded by A1,Lm4; hence g1^f2 is unfolded by A14,A23,A24,A31,Th32; end; hence thesis by FINSEQ_5:def 4; end; theorem Th34: len f <= 2 implies f is s.n.c. proof assume A1: len f <= 2; let i,j such that A2: i+1 < j; now assume that A3: 1 <= i and A4: i+1 <= len f and A5: 1 <= j and A6: j+1 <= len f; i+1 <= 1+1 & j+1 <= 1+1 by A1,A4,A6,AXIOMS:22; then i <= 1 & j <= 1 by REAL_1:53; then i = 1 & j = 1 by A3,A5,AXIOMS:21; hence contradiction by A2; end; then LSeg(f,i) = {} or LSeg(f,j) = {} by TOPREAL1:def 5; hence LSeg(f,i) /\ LSeg(f,j) = {}; end; Lm6: <*p,q*> is s.n.c. proof len <*p,q*> = 2 by FINSEQ_1:61; hence thesis by Th34; end; Lm7: f is s.n.c. implies f|n is s.n.c. proof assume A1: f is s.n.c.; let i,j such that A2: i+1 < j; per cases; suppose A3: i = 0 or j+1 > len(f|n); now per cases by A3; case i = 0; hence LSeg(f|n,i) = {} by TOPREAL1:def 5; case j+1 > len(f|n); hence LSeg(f|n,j) = {} by TOPREAL1:def 5; end; then LSeg(f|n,i) /\ LSeg(f|n,j) = {}; hence LSeg(f|n,i) misses LSeg(f|n,j) by XBOOLE_0:def 7; suppose that i <> 0 and A4: j+1 <= len(f|n); A5: LSeg(f,i) misses LSeg(f,j) by A1,A2,TOPREAL1:def 9; j <= j+1 by NAT_1:29; then i+1 < j+1 by A2,AXIOMS:22; then i+1 <= len(f|n) by A4,AXIOMS:22; then LSeg(f|n,i) /\ LSeg(f|n,j) = LSeg(f,i) /\ LSeg(f|n,j) by Th3 .= LSeg(f,i) /\ LSeg(f,j) by A4,Th3 .= {} by A5,XBOOLE_0:def 7; hence LSeg(f|n,i) misses LSeg(f|n,j) by XBOOLE_0:def 7; end; Lm8: f is s.n.c. implies f/^n is s.n.c. proof assume A1: f is s.n.c.; per cases; suppose A2: n <= len f; let i,j such that A3: i+1 < j; now per cases; suppose A4: i = 0 or j+1 > len(f/^n); now per cases by A4; case i = 0; hence LSeg(f/^n,i) = {} by TOPREAL1:def 5; case j+1 > len(f/^n); hence LSeg(f/^n,j) = {} by TOPREAL1:def 5; end; then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {}; hence thesis by XBOOLE_0:def 7; suppose that A5: i <> 0 and A6: j+1 <= len(f/^n); A7: len(f/^n) = len f - n by A2,RFINSEQ:def 2; A8: 1 <= i by A5,RLVECT_1:99; i <= j by A3,NAT_1:38; then A9: 1 <= j by A8,AXIOMS:22; n+(i+1) < n+j by A3,REAL_1:53; then n+i+1 < n+j by XCMPLX_1:1; then A10: LSeg(f,n+i) misses LSeg(f,n+j) by A1,TOPREAL1:def 9; j <= j+1 by NAT_1:29; then i+1 < j+1 by A3,AXIOMS:22; then i+1 <= len(f/^n) by A6,AXIOMS:22; then LSeg(f/^n,i) /\ LSeg(f/^n,j) = LSeg(f,n+i) /\ LSeg(f/^n,j) by A7,A8,Th5 .= LSeg(f,n+i) /\ LSeg(f,n+j) by A6,A7,A9,Th5 .= {} by A10,XBOOLE_0:def 7; hence thesis by XBOOLE_0:def 7; end; hence thesis; suppose n > len f; then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 2; then len(f/^n) = 0 by FINSEQ_1:25; hence thesis by Th34; end; definition let f be s.n.c. FinSequence of TOP-REAL 2, n; cluster f|n -> s.n.c.; coherence by Lm7; cluster f/^n -> s.n.c.; coherence by Lm8; end; Lm9: f is s.n.c. implies f-:p is s.n.c. proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis by Lm7; end; definition let f be s.n.c. FinSequence of TOP-REAL 2, p; cluster f-:p -> s.n.c.; coherence by Lm9; end; theorem Th35: p in rng f & f is s.n.c. implies f:-p is s.n.c. proof assume p in rng f; then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:52; hence thesis by Lm8; end; theorem Th36: f is s.n.c. implies Rev f is s.n.c. proof assume A1: f is s.n.c.; let i,j such that A2: i+1 < j; per cases; suppose A3: i = 0 or j+1 > len(Rev f); now per cases by A3; case i = 0; hence LSeg(Rev f,i) = {} by TOPREAL1:def 5; case j+1 > len(Rev f); hence LSeg(Rev f,j) = {} by TOPREAL1:def 5; end; then LSeg(Rev f,i) /\ LSeg(Rev f,j) = {}; hence thesis by XBOOLE_0:def 7; suppose that i <> 0 and A4: j+1 <= len(Rev f); A5: len Rev f = len f by FINSEQ_5:def 3; j <= j+1 by NAT_1:29; then A6: j <= len f by A4,A5,AXIOMS:22; then reconsider j' = len f - j as Nat by INT_1:18; i <= i+1 by NAT_1:29; then i < j by A2,AXIOMS:22; then i <= len f by A6,AXIOMS:22; then reconsider i' = len f - i as Nat by INT_1:18; A7: j'+j = len f by XCMPLX_1:27; len f - (i+1) > j' by A2,REAL_2:105; then i' - 1 > j' by XCMPLX_1:36; then i' - 1 + 1 > j'+1 by REAL_1:53; then j'+1 < i' by XCMPLX_1:27; then A8: LSeg(f,i') misses LSeg(f,j') by A1,TOPREAL1:def 9; i'+i = len f by XCMPLX_1:27; hence LSeg(Rev f,i) /\ LSeg(Rev f,j) = LSeg(f,i') /\ LSeg(Rev f,j) by Th2 .= LSeg(f,i') /\ LSeg(f,j') by A7,Th2 .= {} by A8,XBOOLE_0:def 7; end; theorem Th37: f is s.n.c. & g is s.n.c. & L~f misses L~g & (for i st 1<=i & i+2 <= len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1)) & (for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g/.1)) implies f^g is s.n.c. proof assume that A1: f is s.n.c. and A2: g is s.n.c. and A3: L~f /\ L~g = {} and A4: for i st 1<=i & i+2<= len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1) and A5: for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g/.1); let i,j such that A6: i+1 < j; per cases; suppose A7: i = 0 or j+1 > len(f^g); now per cases by A7; case i = 0; hence LSeg(f^g,i) = {} by TOPREAL1:def 5; case j+1 > len(f^g); hence LSeg(f^g,j) = {} by TOPREAL1:def 5; end; then LSeg(f^g,i) /\ LSeg(f^g,j) = {}; hence thesis by XBOOLE_0:def 7; suppose that A8: i <> 0 and A9: j+1 <= len(f^g); A10: len(f^g) = len f + len g by FINSEQ_1:35; A11: 1 <= i by A8,RLVECT_1:99; i <= i+1 by NAT_1:29; then A12: i < j by A6,AXIOMS:22; now per cases; suppose A13: j+1 <= len f; j <= j+1 by NAT_1:29; then i < j+1 by A12,AXIOMS:22; then i < len f by A13,AXIOMS:22; then i+1 <= len f by NAT_1:38; then A14: LSeg(f^g,i) = LSeg(f,i) by Th6; LSeg(f^g,j) = LSeg(f,j) by A13,Th6; hence thesis by A1,A6,A14,TOPREAL1:def 9; suppose j+1 > len f; then A15: len f <= j by NAT_1:38; then reconsider j' = j - len f as Nat by INT_1:18; A16: len f + j' = j by XCMPLX_1:27; j+1-len f <= len g by A9,A10,REAL_1:86; then A17: j'+1 <= len g by XCMPLX_1:29; now per cases; suppose A18: i <= len f; then A19: f is non empty by A11,FINSEQ_3:27,RELAT_1:60; now per cases; suppose A20: i = len f; then len f +1+1 <= j by A6,NAT_1:38; then len f +(1+1) <= j by XCMPLX_1:1; then A21: 1+1 <= j' by REAL_1:84; then A22: 1 <= j' by AXIOMS:22; then A23: LSeg(f^g,j) = LSeg(g,j') by A16,Th7; g is non empty by A17,A22,GOBOARD2:3,RELAT_1:60; then LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A19,A20,Th8; hence thesis by A5,A17,A21,A23; suppose i <> len f; then i < len f by A18,REAL_1:def 5; then i+1 <= len f by NAT_1:38; then A24: LSeg(f^g,i) = LSeg(f,i) by Th6; now per cases; suppose A25: j = len f; then i+1+1 <= len f by A6,NAT_1:38; then A26: i+(1+1) <= len f by XCMPLX_1:1; 1 <= len g by A9,A10,A25,REAL_1:53; then g is non empty by FINSEQ_3:27,RELAT_1:60; then LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A19,A25,Th8; hence thesis by A4,A11,A24,A26; suppose j <> len f; then len f < j by A15,REAL_1:def 5; then len f+1 <= j by NAT_1:38; then 1 <= j' by REAL_1:84; then LSeg(f^g,len f+j') = LSeg(g,j') by Th7; then A27: LSeg(f^g,j) c= L~g by A16,TOPREAL3:26; LSeg(f^g,i) c= L~f by A24,TOPREAL3:26; then LSeg(f^g,i) /\ LSeg(f^g,j) c= L~f /\ L~g by A27,XBOOLE_1:27; then LSeg(f^g,i) /\ LSeg(f^g,j) = {} by A3,XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; end; hence thesis; end; hence thesis; suppose A28: i > len f; then reconsider i' = i - len f as Nat by INT_1:18; A29: len f + i' = i by XCMPLX_1:27; len f + 1 <= i by A28,NAT_1:38; then 1 <= i' by REAL_1:84; then A30: LSeg(f^g,len f+i') = LSeg(g,i') by Th7; i+1-len f < j' by A6,REAL_1:54; then A31: i'+1 < j' by XCMPLX_1:29; j <> len f by A6,A28,NAT_1:38; then len f < j by A15,REAL_1:def 5; then len f+1 <= j by NAT_1:38; then 1 <= j' by REAL_1:84; then LSeg(f^g,len f+j') = LSeg(g,j') by Th7; hence thesis by A2,A16,A29,A30,A31,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; theorem Th38: f is unfolded s.n.c. & p in LSeg(f,n) & not p in rng f implies Ins(f,n,p) is s.n.c. proof assume that A1: f is unfolded and A2: f is s.n.c. and A3: p in LSeg(f,n) and A4: not p in rng f; let i,j such that A5: i+1 < j; set fp = Ins(f,n,p); per cases; suppose A6: i = 0 or j+1 > len fp; now per cases by A6; case i = 0; hence LSeg(fp,i) = {} by TOPREAL1:def 5; case j+1 > len fp; hence LSeg(fp,j) = {} by TOPREAL1:def 5; end; then LSeg(fp,i) /\ LSeg(fp,j) = {}; hence thesis by XBOOLE_0:def 7; suppose that A7: i <> 0 and A8: j+1 <= len fp; set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A9: fp = g1^f2 by FINSEQ_5:def 4; A10: 1 <= i by A7,RLVECT_1:99; i <= i+1 by NAT_1:29; then A11: i < j by A5,AXIOMS:22; A12: len fp = len f + 1 by FINSEQ_5:72; A13: len g1 = len f1 + 1 by FINSEQ_2:19; then A14: g1/.len g1 = p by TOPREAL4:1; A15: 1 <= n & n+1 <= len f by A3,TOPREAL1:def 5; A16: n <= n+1 by NAT_1:29; then A17: n <= len f by A15,AXIOMS:22; then A18: len f1 = n by TOPREAL1:3; i+1+1 <= j by A5,NAT_1:38; then i+1+1+1 <= j+1 by AXIOMS:24; then i+1+1+1 <= len f + 1 by A8,A12,AXIOMS:22; then A19: i+1+1 <= len f by REAL_1:53; i+1 <= i+1+1 by NAT_1:29; then A20: i+1 <= len f by A19,AXIOMS:22; now per cases; suppose A21: j+1 <= n; then A22: j+1 <= len g1 by A13,A16,A18,AXIOMS:22; j <= j+1 by NAT_1:29; then i < j+1 by A11,AXIOMS:22; then i < n by A21,AXIOMS:22; then A23: i+1 <= n by NAT_1:38; then i+1 <= len g1 by A13,A16,A18,AXIOMS:22; then A24: LSeg(fp,i) = LSeg(g1,i) by A9,Th6 .= LSeg(f1,i) by A18,A23,Th6 .= LSeg(f,i) by A18,A23,Th3; LSeg(fp,j) = LSeg(g1,j) by A9,A22,Th6 .= LSeg(f1,j) by A18,A21,Th6 .= LSeg(f,j) by A18,A21,Th3; hence thesis by A2,A5,A24,TOPREAL1:def 9; suppose j+1 > n; then A25: n <= j by NAT_1:38; now per cases; suppose A26: i <= n+1; A27: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A15,TOPREAL1:def 5; A28: n in dom f1 by A15,A18,FINSEQ_3:27; then A29: f/.n = f1/.len f1 by A18,TOPREAL1:1; 1 <= len f - n by A15,REAL_1:84; then 1 <= len f2 by A17,RFINSEQ:def 2; then 1 in dom f2 by FINSEQ_3:27; then A30: f/.(n+1) = f2/.1 by FINSEQ_5:30; then A31: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) = LSeg(f1/.len f1,f2/.1) by A3,A14,A27,A29,TOPREAL1:11; A32: f1/.len f1 = g1/.len f1 by A18,A28,GROUP_5:95; A33: LSeg(fp,n) = LSeg(g1,n) by A9,A13,A18,Th6 .= LSeg(f1/.len f1,p) by A13,A14,A15,A18,A32,TOPREAL1:def 5; A34: fp/.(n+1+1) = f/.(n+1) by A15,FINSEQ_5:77; A35: 1 <= n+1 by NAT_1:29; A36: n+1+1 <= len fp by A12,A15,AXIOMS:24; g1 is non empty by FINSEQ_1:48; then len g1 in dom g1 by FINSEQ_5:6; then fp/.(n+1) = g1/.len g1 by A9,A13,A18,GROUP_5:95; then A37: LSeg(fp,n+1) = LSeg(p,f2/.1) by A14,A30,A34,A35,A36,TOPREAL1:def 5; A38: LSeg(f1/.len f1,p) /\ LSeg(p,f2/.1) = {p} by A3,A27,A29,A30,TOPREAL1:14; A39: LSeg(fp,n) c= LSeg(f,n) by A27,A29,A30,A31,A33,XBOOLE_1:7; A40: LSeg(fp,n+1) c= LSeg(f,n) by A14,A27,A29,A30,A31,A37,XBOOLE_1:7; now per cases by REAL_1:def 5; suppose i < n; then A41: i+1 <= n by NAT_1:38; then i+1 <= len g1 by A13,A16,A18,AXIOMS:22; then A42: LSeg(fp,i) = LSeg(g1,i) by A9,Th6 .= LSeg(f1,i) by A18,A41,Th6 .= LSeg(f,i) by A18,A41,Th3; now per cases; suppose A43: j = n; then A44: LSeg(f,i) misses LSeg(f,n) by A2,A5,TOPREAL1:def 9; LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,n) by A39,A42,A43,XBOOLE_1:26; then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A44,XBOOLE_0:def 7; then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; suppose j <> n; then n < j by A25,REAL_1:def 5; then A45: n+1 <= j by NAT_1:38; now per cases; suppose A46: j = n+1; now per cases; suppose A47: i+1 = n; then i+1 <= len g1 by A13,A18,NAT_1:29; then A48: LSeg(fp,i) = LSeg(g1,i) by A9,Th6 .= LSeg(f1,i) by A18,A47,Th6 .= LSeg(f,i) by A18,A47,Th3; i+(1+1) <= len f by A19,XCMPLX_1:1; then A49: LSeg(fp,i) /\ LSeg(f,n) = {f/.n} by A1,A10,A47,A48,TOPREAL1:def 8; assume not thesis; then consider x being set such that A50: x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4; A51: n in dom f by A15,GOBOARD2:3; A52: x in LSeg(fp,i) by A50,XBOOLE_0:def 3; A53: x in LSeg(fp,j) by A50,XBOOLE_0:def 3; then x in LSeg(f,n) by A14,A27,A29,A30,A31,A37,A46,XBOOLE_0:def 2; then x in {f/.n} by A49,A52,XBOOLE_0:def 3; then A54: x = f/.n by TARSKI:def 1; then x in LSeg(fp,n) by A29,A33,TOPREAL1:6; then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A46,A53,XBOOLE_0:def 3; then p = f/.n by A33,A37,A38,A54,TARSKI:def 1; hence contradiction by A4,A51,PARTFUN2:4; suppose i+1 <> n; then i+1 < n by A41,REAL_1:def 5; then A55: LSeg(f,i) misses LSeg(f,n) by A2,TOPREAL1:def 9; LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,n) by A40,A42,A46,XBOOLE_1:26; then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A55,XBOOLE_0:def 7; then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; end; hence thesis; suppose j <> n+1; then A56: n+1 < j by A45,REAL_1:def 5; then A57: n+1+1 <= j by NAT_1:38; 1 < j by A10,A11,AXIOMS:22; then reconsider j' = j - 1 as Nat by INT_1:18; reconsider nj = j-(n+1) as Nat by A45,INT_1:18; A58: j = nj+(n+1) by XCMPLX_1:27; A59: 1 <= nj by A57,REAL_1:84; A60: n+nj = n+j-(n+1) by XCMPLX_1:29 .= n+j-n-1 by XCMPLX_1:36 .= j' by XCMPLX_1:26; i+1+1 <= n+1 by A41,AXIOMS:24; then i+1+1 < j by A56,AXIOMS:22; then A61: i+1 < j' by REAL_1:86; LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A58,A59,Th7 .= LSeg(f,j') by A17,A59,A60,Th4; hence thesis by A2,A42,A61,TOPREAL1:def 9; end; hence thesis; end; hence thesis; suppose A62: i = n; then A63: n+1+1 <= j by A5,NAT_1:38; 1 < j by A10,A11,AXIOMS:22; then reconsider j' = j - 1 as Nat by INT_1:18; reconsider nj = j-(n+1) as Nat by A5,A62,INT_1:18; A64: j = nj+(n+1) by XCMPLX_1:27; A65: 1 <= nj by A63,REAL_1:84; A66: n+nj = n+j-(n+1) by XCMPLX_1:29 .= n+j-n-1 by XCMPLX_1:36 .= j' by XCMPLX_1:26; A67: LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A64,A65,Th7 .= LSeg(f,j') by A17,A65,A66,Th4; now per cases; suppose j <> n+1+1; then n+1+1 < j by A63,REAL_1:def 5; then i+1 < j' by A62,REAL_1:86; then A68: LSeg(f,i) misses LSeg(f,j') by A2,TOPREAL1:def 9; LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,j') by A39,A62,A67,XBOOLE_1:26; then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A68,XBOOLE_0:def 7; then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; suppose A69: j = n+1+1; then A70: j' = n+1 by XCMPLX_1:26; j <= len f by A8,A12,REAL_1:53; then n+(1+1) <= len f by A69,XCMPLX_1:1; then A71: LSeg(f,n) /\ LSeg(f,j') = {f/.j'} by A1,A15,A70,TOPREAL1:def 8; assume not thesis; then consider x being set such that A72: x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4; A73: n+1 in dom f by A15,GOBOARD2:3; A74: x in LSeg(fp,j) by A72,XBOOLE_0:def 3; A75: x in LSeg(fp,i) by A72,XBOOLE_0:def 3; then x in LSeg(f,n) by A27,A29,A30,A31,A33,A62,XBOOLE_0:def 2; then x in {f/.(n+1)} by A67,A70,A71,A74,XBOOLE_0:def 3; then A76: x = f/.(n+1) by TARSKI:def 1; then x in LSeg(fp,n+1) by A30,A37,TOPREAL1:6; then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A62,A75,XBOOLE_0:def 3; then p = f/.(n+1) by A33,A37,A38,A76,TARSKI:def 1; hence contradiction by A4,A73,PARTFUN2:4; end; hence thesis; suppose i>n; then i>=n+1 by NAT_1:38; then A77: i = n+1 by A26,AXIOMS:21; 1 < j by A10,A11,AXIOMS:22; then reconsider j' = j - 1 as Nat by INT_1:18; n+1 <= n+1+1 by NAT_1:29; then n+1 < j by A5,A77,AXIOMS:22; then reconsider nj = j-(n+1) as Nat by INT_1:18; A78: j = nj+(n+1) by XCMPLX_1:27; A79: 1 <= nj by A5,A77,REAL_1:84; A80: n+nj = n+j-(n+1) by XCMPLX_1:29 .= n+j-n-1 by XCMPLX_1:36 .= j' by XCMPLX_1:26; A81: LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A78,A79,Th7 .= LSeg(f,j') by A17,A79,A80,Th4; n+1 < j' by A5,A77,REAL_1:86; then A82: LSeg(f,n) misses LSeg(f,j') by A2,TOPREAL1:def 9; LSeg(fp,n+1) c= LSeg(f,n) by A14,A27,A29,A30,A31,A37,XBOOLE_1:7; then LSeg(fp,n+1) /\ LSeg(fp,j) c= LSeg(f,n) /\ LSeg(f,j') by A81,XBOOLE_1:26; then LSeg(fp,n+1) /\ LSeg(fp,j) c= {} by A82,XBOOLE_0:def 7; then LSeg(fp,n+1) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by A77,XBOOLE_0:def 7; end; hence thesis; suppose A83: i > n+1; then A84: n+1+1 <= i by NAT_1:38; reconsider ni = i - (n+1) as Nat by A83,INT_1:18; A85: i = ni+(n+1) by XCMPLX_1:27; reconsider i' = i - 1 as Nat by A10,INT_1:18; A86: 1 <= ni by A84,REAL_1:84; len f <= len f+1 by NAT_1:29; then i+1 <= len f+1 by A20,AXIOMS:22; then i+1-(n+1) <= len f+1- (n+1) by REAL_1:49; then i+1-(n+1) <= len f+1-1-n by XCMPLX_1:36; then i+1-(n+1) <= len f - n by XCMPLX_1:26; then A87: ni+1 <= len f - n by XCMPLX_1:29; A88: n+ni = n+i-(n+1) by XCMPLX_1:29 .= n+i-n-1 by XCMPLX_1:36 .= i' by XCMPLX_1:26; A89: LSeg(fp,i) = LSeg(f2,ni) by A9,A13,A18,A85,A86,Th7 .= LSeg(f,i') by A86,A87,A88,Th5; 1 < j by A10,A11,AXIOMS:22; then reconsider j' = j - 1 as Nat by INT_1:18; A90: n+1 < j by A11,A83,AXIOMS:22; then reconsider nj = j-(n+1) as Nat by INT_1:18; A91: j = nj+(n+1) by XCMPLX_1:27; n+1+1 <= j by A90,NAT_1:38; then A92: 1 <= nj by REAL_1:84; A93: n+nj = n+j-(n+1) by XCMPLX_1:29 .= n+j-n-1 by XCMPLX_1:36 .= j' by XCMPLX_1:26; i+1-1 < j' by A5,REAL_1:54; then A94: i'+1 < j' by XCMPLX_1:29; LSeg(fp,j) = LSeg(f2,nj) by A9,A13,A18,A91,A92,Th7 .= LSeg(f,j') by A17,A92,A93,Th4; hence thesis by A2,A89,A94,TOPREAL1:def 9; end; hence thesis; end; hence thesis; end; Lm10: <*>(the carrier of TOP-REAL 2) is special proof set f = <*>(the carrier of TOP-REAL 2); let i such that A1: 1 <= i and A2: i+1 <= len f; i <= i+1 by NAT_1:29; then i <= len f by A2,AXIOMS:22; then i <= 0 by FINSEQ_1:25; hence thesis by A1,AXIOMS:22; end; definition cluster <*>(the carrier of TOP-REAL 2) -> special; coherence by Lm10; end; theorem Th39: <*p*> is special proof set f = <*p*>; let i such that A1: 1 <= i and A2: i+1 <= len f; len f = 0+1 by FINSEQ_1:56; then i <= 0 by A2,REAL_1:53; hence thesis by A1,AXIOMS:22; end; theorem Th40: p`1 = q`1 or p`2 = q`2 implies <*p,q*> is special proof assume A1: p`1 = q`1 or p`2 = q`2; set f = <*p,q*>; A2: len f = 1+1 by FINSEQ_1:61; let i such that A3: 1 <= i and A4: i+1 <= len f; i <= 1 by A2,A4,REAL_1:53; then i = 1 by A3,AXIOMS:21; then f/.i = p & f/.(i+1) = q by FINSEQ_4:26; hence thesis by A1; end; Lm11: f is special implies f|n is special proof assume A1: f is special; let i such that A2: 1 <= i and A3: i+1 <= len(f|n); i in dom(f|n) by A2,A3,GOBOARD2:3; then A4: (f|n)/.i = f/.i by TOPREAL1:1; i+1 in dom(f|n) by A2,A3,GOBOARD2:3; then A5: (f|n)/.(i+1) = f/.(i+1) by TOPREAL1:1; len(f|n) <= len f by FINSEQ_5:18; then i+1 <= len f by A3,AXIOMS:22; hence thesis by A1,A2,A4,A5,TOPREAL1:def 7; end; Lm12: f is special implies f/^n is special proof assume A1: f is special; per cases; suppose A2: n <= len f; let i such that A3: 1 <= i and A4: i+1 <= len(f/^n); A5: len(f/^n) = len f - n by A2,RFINSEQ:def 2; i in dom(f/^n) by A3,A4,GOBOARD2:3; then A6: (f/^n)/.i = f/.(n+i) by FINSEQ_5:30; i+1 in dom(f/^n) by A3,A4,GOBOARD2:3; then A7: (f/^n)/.(i+1) = f/.(n+(i+1)) by FINSEQ_5:30 .= f/.(n+i+1) by XCMPLX_1:1; i <= n+i by NAT_1:29; then A8: 1 <= n+i by A3,AXIOMS:22; n+(i+1) <= len f by A4,A5,REAL_1:84; then n+i+1 <= len f by XCMPLX_1:1; hence thesis by A1,A6,A7,A8,TOPREAL1:def 7; suppose n > len f; then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 2; hence thesis; end; definition let f be special FinSequence of TOP-REAL 2, n; cluster f|n -> special; coherence by Lm11; cluster f/^n -> special; coherence by Lm12; end; theorem Th41: p in rng f & f is special implies f:-p is special proof assume p in rng f; then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:52; hence thesis by Lm12; end; Lm13: f is special implies f-:p is special proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis by Lm11; end; definition let f be special FinSequence of TOP-REAL 2, p; cluster f-:p -> special; coherence by Lm13; end; theorem Th42: f is special implies Rev f is special proof assume A1: f is special; let i such that A2: 1 <= i and A3: i+1 <= len(Rev f); A4: len Rev f = len f by FINSEQ_5:def 3; i <= i+1 by NAT_1:29; then i <= len f by A3,A4,AXIOMS:22; then reconsider j = len f - i as Nat by INT_1:18; j <= len f - 1 by A2,REAL_2:106; then j+1 <= len f - 1 + 1 by AXIOMS:24; then A5: j+1 <= len f by XCMPLX_1:27; i+1-i <= j by A3,A4,REAL_1:49; then A6: 1 <= j by XCMPLX_1:26; A7: i+j = len f by XCMPLX_1:27; then A8: i+(j+1) = len f + 1 by XCMPLX_1:1; j+1 in dom f by A5,A6,GOBOARD2:3; then A9: (Rev f)/.i = f/.(j+1) by A8,FINSEQ_5:69; A10: 1+i+j = len f + 1 by A7,XCMPLX_1:1; j in dom f by A5,A6,GOBOARD2:3; then (Rev f)/.(i+1) = f/.j by A10,FINSEQ_5:69; hence thesis by A1,A5,A6,A9,TOPREAL1:def 7; end; Lm14: f is special & g is special & ((f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2) implies f^g is special proof assume that A1: f is special and A2: g is special and A3: (f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2; let i such that A4: 1 <= i and A5: i+1 <= len(f^g); A6: len(f^g) = len f + len g by FINSEQ_1:35; per cases by REAL_1:def 5; suppose i < len f; then A7: i+1 <= len f by NAT_1:38; then i in dom f by A4,GOBOARD2:3; then A8: (f^g)/.i=f/.i by GROUP_5:95; i+1 in dom f by A4,A7,GOBOARD2:3; then (f^g)/.(i+1)=f/.(i+1) by GROUP_5:95; hence thesis by A1,A4,A7,A8,TOPREAL1:def 7; suppose A9: i = len f; then i in dom f by A4,FINSEQ_3:27; then A10: (f^g)/.i = f/.i by GROUP_5:95; 1 <= len g by A5,A6,A9,REAL_1:53; then 1 in dom g by FINSEQ_3:27; hence thesis by A3,A9,A10,GROUP_5:96; suppose A11: i > len f; then reconsider j = i - len f as Nat by INT_1:18; A12: len f + j = i by XCMPLX_1:27; then A13: len f + (j+1) = i+1 by XCMPLX_1:1; len f + 1 <= i by A11,NAT_1:38; then A14: 1 <= j by REAL_1:84; i+1-len f <= len g by A5,A6,REAL_1:86; then A15: j+1 <= len g by XCMPLX_1:29; then j in dom g by A14,GOBOARD2:3; then A16: (f^g)/.i= g/.j by A12,GROUP_5:96; j+1 in dom g by A14,A15,GOBOARD2:3; then (f^g)/.(i+1)= g/.(j+1) by A13,GROUP_5:96; hence thesis by A2,A14,A15,A16,TOPREAL1:def 7; end; canceled; theorem Th44: f is special & p in LSeg(f,n) implies Ins(f,n,p) is special proof assume that A1: f is special and A2: p in LSeg(f,n); set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A3: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:19 .= p by TOPREAL4:1; A4: 1 <= n & n+1 <= len f by A2,TOPREAL1:def 5; n <= n+1 by NAT_1:29; then A5: n <= len f by A4,AXIOMS:22; then A6: len f1 = n by TOPREAL1:3; then A7: n in dom f1 by A4,FINSEQ_3:27; 1 <= len f - n by A4,REAL_1:84; then 1 <= len f2 by A5,RFINSEQ:def 2; then A8: 1 in dom f2 by FINSEQ_3:27; A9: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A4,TOPREAL1:def 5; A10: f/.n = f1/.len f1 by A6,A7,TOPREAL1:1; A11: f/.(n+1) = f2/.1 by A8,FINSEQ_5:30; A12: f1 is special by A1,Lm11; set p1 = f1/.len f1, p2 = f2/.1; A13: p1`1 = p2`1 or p1`2 = p2`2 by A1,A4,A10,A11,TOPREAL1:def 7; A14: p1 = |[p1`1, p1`2]| by EUCLID:57; A15: p2 = |[p2`1, p2`2]| by EUCLID:57; <*p*>/.1 = p by FINSEQ_4:25; then A16: p1`1 = (<*p*>/.1)`1 or p1`2 = (<*p*>/.1)`2 by A2,A9,A10,A11,A13,A14,A15,TOPREAL3:17,18; <*p*> is special by Th39; then A17: g1 is special by A12,A16,Lm14; set q1 = g1/.len g1; A18: q1`1 = p2`1 or q1`2 = p2`2 by A2,A3,A9,A10,A11,A13,A14,A15,TOPREAL3:17,18; f2 is special by A1,Lm12; then g1^f2 is special by A17,A18,Lm14; hence thesis by FINSEQ_5:def 4; end; theorem Th45: q in rng f & 1<>q..f & q..f<>len f & f is unfolded s.n.c. implies L~(f-:q) /\ L~(f:-q) = {q} proof assume that A1: q in rng f and A2: 1 <> q..f and A3: q..f <> len f and A4: f is unfolded and A5: f is s.n.c.; A6: len(f-:q) = q..f by A1,FINSEQ_5:45; f-:q is non empty by A1,FINSEQ_5:50; then A7: len(f-:q) in dom(f-:q) by FINSEQ_5:6; A8: (f-:q)/.(q..f) = q by A1,FINSEQ_5:48; A9: 1 in dom(f:-q) by FINSEQ_5:6; A10: (f:-q)/.1 = q by FINSEQ_5:56; A11: len(f:-q) = len f - q..f + 1 by A1,FINSEQ_5:53; thus L~(f-:q) /\ L~(f:-q) c= {q} proof let x be set; assume A12: x in L~(f-:q) /\ L~(f:-q); then reconsider p = x as Point of TOP-REAL 2; p in L~(f-:q) by A12,XBOOLE_0:def 3; then consider i such that A13: 1 <= i and A14: i+1 <= len(f-:q) and A15: p in LSeg((f-:q),i) by Th13; p in L~(f:-q) by A12,XBOOLE_0:def 3; then consider j such that A16: 1 <= j and j+1 <= len(f:-q) and A17: p in LSeg((f:-q),j) by Th13; A18: LSeg(f-:q,i) = LSeg(f,i) by A14,Th9; j <> 0 by A16; then consider j' being Nat such that A19: j=j'+1 by NAT_1:22; A20: LSeg(f:-q,j) = LSeg(f,j'+q..f) by A1,A19,Th10; per cases; suppose that A21: i+1 = len(f-:q) and A22: j' = 0; q..f <= len f by A1,FINSEQ_4:31; then q..f < len f by A3,REAL_1:def 5; then i+1+1 <= len f by A6,A21,NAT_1:38; then i+(1+1) <= len f by XCMPLX_1:1; then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {f/.(q..f)} by A4,A6,A13,A18,A20,A21,A22,TOPREAL1:def 8 .= {q} by A1,FINSEQ_5:41; hence x in {q} by A15,A17,XBOOLE_0:def 3; suppose that A23: i+1 = len(f-:q) and A24: j' <> 0; 1 <= j' by A24,RLVECT_1:99; then i+1+1 <= j'+q..f by A6,A23,REAL_1:55; then i+1 < j'+q..f by NAT_1:38; then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A18,A20,TOPREAL1:def 9; then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {} by XBOOLE_0:def 7; hence thesis by A15,A17,XBOOLE_0:def 3; suppose i+1 <> len(f-:q); then A25: i+1 < q..f by A6,A14,REAL_1:def 5; q..f <= j'+q..f by NAT_1:29; then i+1 < j'+q..f by A25,AXIOMS:22; then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A18,A20,TOPREAL1:def 9; then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {} by XBOOLE_0:def 7; hence thesis by A15,A17,XBOOLE_0:def 3; end; A26: q in rng(f-:q) by A6,A7,A8,PARTFUN2:4; 1 <= q..f by A1,FINSEQ_4:31; then 1 < q..f by A2,REAL_1:def 5; then 1+1 <= q..f by NAT_1:38; then A27: rng(f-:q) c= L~(f-:q) by A6,Th18; A28: q in rng(f:-q) by A9,A10,PARTFUN2:4; q..f <= len f by A1,FINSEQ_4:31; then q..f < len f by A3,REAL_1:def 5; then q..f+1 <= len f by NAT_1:38; then 1 <= len f - q..f by REAL_1:84; then 1+1<=len(f:-q) by A11,AXIOMS:24; then rng(f:-q) c= L~(f:-q) by Th18; then q in L~(f-:q) /\ L~(f:-q) by A26,A27,A28,XBOOLE_0:def 3; hence {q} c= L~(f-:q) /\ L~(f:-q) by ZFMISC_1:37; end; theorem Th46: p <> q & (p`1 = q`1 or p`2 = q`2) implies <*p,q*> is being_S-Seq proof assume that A1: p <> q and A2: p`1 = q`1 or p`2 = q`2; set f = <*p,q*>; thus f is one-to-one by A1,FINSEQ_3:103; thus len f >= 2 by FINSEQ_1:61; thus thesis by A2,Lm2,Lm6,Th40; end; definition mode S-Sequence_in_R2 is being_S-Seq FinSequence of TOP-REAL 2; end; theorem Th47: for f being S-Sequence_in_R2 holds Rev f is being_S-Seq proof let f be S-Sequence_in_R2; set g = Rev f; thus g is one-to-one; len g = len f by FINSEQ_5:def 3; hence len g >= 2 by TOPREAL1:def 10; thus thesis by Th29,Th36,Th42; end; theorem for f being S-Sequence_in_R2 st i in dom f holds f/.i in L~f proof let f be S-Sequence_in_R2; len f >= 2 by TOPREAL1:def 10; hence thesis by GOBOARD1:16; end; theorem p <> q & (p`1 = q`1 or p`2 = q`2) implies LSeg(p,q) is being_S-P_arc proof assume A1: p <> q & (p`1 = q`1 or p`2 = q`2); take f = <*p,q*>; thus f is_S-Seq by A1,Th46; thus L~f = LSeg(p,q) by Th21; end; Lm15: p in rng f implies L~(f-:p) c= L~f proof assume p in rng f; then L~f = L~(f-:p) \/ L~(f:-p) by Th25; hence thesis by XBOOLE_1:7; end; Lm16: p in rng f implies L~(f:-p) c= L~f proof assume p in rng f; then L~f = L~(f-:p) \/ L~(f:-p) by Th25; hence thesis by XBOOLE_1:7; end; theorem Th50: for f being S-Sequence_in_R2 st p in rng f & p..f <> 1 holds f-:p is being_S-Seq proof let f be S-Sequence_in_R2 such that A1: p in rng f and A2: p..f <> 1; thus f-:p is one-to-one; 1 <= p..f by A1,FINSEQ_4:31; then 1 < p..f by A2,REAL_1:def 5; then 1+1 <= p..f by NAT_1:38; hence len(f-:p) >= 2 by A1,FINSEQ_5:45; thus thesis; end; theorem for f being S-Sequence_in_R2 st p in rng f & p..f <> len f holds f:-p is being_S-Seq proof let f be S-Sequence_in_R2 such that A1: p in rng f and A2: p..f <> len f; thus f:-p is one-to-one by A1,FINSEQ_5:59; hereby assume A3: len(f:-p) < 2; p..f <= len f by A1,FINSEQ_4:31; then p..f < len f by A2,REAL_1:def 5; then 1 + p..f <= len f by NAT_1:38; then A4: len f - p..f >= 1 by REAL_1:84; len f - p..f + 1 < 1 + 1 by A1,A3,FINSEQ_5:53; hence contradiction by A4,AXIOMS:24; end; thus thesis by A1,Th28,Th35,Th41; end; theorem Th52: for f being S-Sequence_in_R2 st p in LSeg(f,i) & not p in rng f holds Ins(f,i,p) is being_S-Seq proof let f be S-Sequence_in_R2 such that A1: p in LSeg(f,i) and A2: not p in rng f; set g = Ins(f,i,p); thus g is one-to-one by A2,FINSEQ_5:79; A3: len f >= 2 by TOPREAL1:def 10; len g = len f + 1 by FINSEQ_5:72; then len g >= len f by NAT_1:29; hence len g >= 2 by A3,AXIOMS:22; thus g is unfolded by A1,Th33; thus g is s.n.c. by A1,A2,Th38; thus g is special by A1,Th44; end; begin :: Special Polygons in TOP-REAL 2 definition cluster being_S-P_arc Subset of TOP-REAL 2; existence proof set p = |[ 0,0 ]|, q = |[ 1,1 ]|, f = <* p,|[p`1,q`2]|,q *>; 0 <> 1 & p`1 = 0 & p`2 = 0 & q`1 = 1 & q`2 = 1 by EUCLID:56; then f is_S-Seq by TOPREAL3:41; then L~f is_S-P_arc by TOPREAL1:def 11; hence thesis; end; end; theorem P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1 proof given f such that A1: f is_S-Seq and A2: P = L~f and A3: p1=f/.1 & p2 = f/.len f; take g = Rev f; thus g is_S-Seq & P = L~g by A1,A2,Th22,Th47; len f <> 0 by A1,TOPREAL1:def 10; then f is non empty & len g = len f by FINSEQ_1:25,FINSEQ_5:def 3; hence thesis by A3,FINSEQ_5:68; end; definition let p1,p2; let P be Subset of TOP-REAL 2; pred p1,p2 split P means :Def1: p1 <> p2 & ex f1,f2 being S-Sequence_in_R2 st p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2; end; theorem Th54: p1,p2 split P implies p2,p1 split P proof assume A1: p1 <> p2; given f1,f2 being S-Sequence_in_R2 such that A2: p1 = f1/.1 & p1 = f2/.1 and A3: p2 = f1/.len f1 & p2 = f2/.len f2 and A4: L~f1 /\ L~f2 = {p1,p2} and A5: P = L~f1 \/ L~f2; thus p2 <> p1 by A1; reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2 by Th47; take g1, g2; len g1 = len f1 & len g2 = len f2 by FINSEQ_5:def 3; hence p2 = g1/.1 & p2 = g2/.1 & p1 = g1/.len g1 & p1 = g2/.len g2 by A2,A3,FINSEQ_5:68; L~g1 = L~f1 & L~g2 = L~f2 by Th22; hence thesis by A4,A5; end; Lm17: for f1,f2 being S-Sequence_in_R2 st p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 & q <> p1 & q in rng f1 ex g1,g2 being S-Sequence_in_R2 st p1 = g1/.1 & p1 = g2/.1 & q = g1/.len g1 & q = g2/.len g2 & L~g1 /\ L~g2 = {p1,q} & P = L~g1 \/ L~g2 proof let f1,f2 be S-Sequence_in_R2 such that A1: p1 = f1/.1 and A2: p1 = f2/.1 and A3: p2 = f1/.len f1 and A4: p2 = f2/.len f2 and A5: L~f1 /\ L~f2 = {p1,p2} and A6: P = L~f1 \/ L~f2 and A7: q <> p1 and A8: q in rng f1; A9: len f2 in dom f2 by FINSEQ_5:6; A10: now assume 1 = q..f1; then f1.1 = q & 1 in dom f1 by A8,FINSEQ_4:29,30; hence contradiction by A1,A7,FINSEQ_4:def 4; end; then reconsider g1 = f1-:q as S-Sequence_in_R2 by A8,Th50; set f1' = Rev(f1:-q); 1 in dom f2 by FINSEQ_5:6; then 1 <= len f2 by FINSEQ_3:27; then reconsider l = len f2 - 1 as Nat by INT_1:18; set f2' = f2|l; set g2 = f2'^f1'; set Z = rng f2' /\ rng f1'; A11: l < len f2 by SQUARE_1:29; then A12: len f2' = l by TOPREAL1:3; reconsider f1q = f1:-q as one-to-one FinSequence of TOP-REAL 2 by A8, FINSEQ_5:59; A13: 1 in dom f1 by FINSEQ_5:6; now assume A14: p1 in rng(f1:-q); set l = p1..(f1:-q); A15: l in dom(f1:-q) by A14,FINSEQ_4:30; (f1:-q).l = p1 by A14,FINSEQ_4:29; then A16: (f1:-q)/.l = p1 by A15,FINSEQ_4:def 4; l <> 0 by A14,FINSEQ_4:31; then consider j such that A17: l = j+1 by NAT_1:22; A18: (f1:-q)/.l = f1/.(j+q..f1) by A8,A15,A17,FINSEQ_5:55; j+q..f1 in dom f1 by A8,A15,A17,FINSEQ_5:54; then j+q..f1 = 1 by A1,A13,A16,A18,PARTFUN2:17; then 1 <= q..f1 & q..f1 <= 1 by A8,FINSEQ_4:31,NAT_1:29; hence contradiction by A10,AXIOMS:21; end; then not p1 in rng f1' by FINSEQ_5:60; then A19: not p1 in Z by XBOOLE_0:def 3; A20: p2..f2 = len f2 by A4,A9,FINSEQ_5:44; now assume A21: p2 in rng f2'; then p2..f2' = p2..f2 by FINSEQ_5:43; hence contradiction by A11,A12,A20,A21,FINSEQ_4:31; end; then not p2 in Z by XBOOLE_0:def 3; then A22: Z <> {p1} & Z <> {p2} & Z <> {p1,p2} by A19,TARSKI:def 1,def 2; rng f1' = rng(f1:-q) by FINSEQ_5:60; then rng f2' c= rng f2 & rng f1' c= rng f1 by A8,FINSEQ_5:21,58; then A23: Z c= rng f2 /\ rng f1 by XBOOLE_1:27; len f1 >= 2 & len f2 >= 2 by TOPREAL1:def 10; then rng f1 c= L~f1 & rng f2 c= L~f2 by Th18; then rng f2 /\ rng f1 c= L~f1 /\ L~f2 by XBOOLE_1:27; then Z c= {p1,p2} by A5,A23,XBOOLE_1:1; then Z = {} by A22,ZFMISC_1:42; then A24: rng f2' misses rng f1' by XBOOLE_0:def 7; Rev f1q is one-to-one; then A25: g2 is one-to-one by A24,FINSEQ_3:98; A26: 1 <= q..f1 by A8,FINSEQ_4:31; len(f1:-q) <> 0 by FINSEQ_1:25; then len(f1:-q) >= 1 by RLVECT_1:99; then A27: len f1' >= 1 by FINSEQ_5:def 3; then A28: len f1' in dom f1' by FINSEQ_3:27; len f2 >= 2 by TOPREAL1:def 10; then A29: len f2 - 1 >= 1+1-1 by REAL_1:49; then A30: len f2' >= 1 by A11,TOPREAL1:3; len f2' + len f1' >= 1+1 by A12,A27,A29,REAL_1:55; then A31: len g2 >= 2 by FINSEQ_1:35; A32: 1 in dom f2' by A12,A29,FINSEQ_3:27; A33: f2' is non empty by A30,FINSEQ_3:27,RELAT_1:60; f1:-q is unfolded by A8,Th28; then A34: f1' is unfolded by Th29; A35: l+1 = len f2 by XCMPLX_1:27; A36: l in dom f2' by A12,A29,FINSEQ_3:27; then A37: f2'/.len f2' = f2/.l by A12,TOPREAL1:1; A38: f1'/.1 = (f1:-q)/.len(f1:-q) by FINSEQ_5:68 .= f2/.len f2 by A3,A4,A8,FINSEQ_5:57; dom f2 = Seg len f2 & dom f2' = Seg len f2' by FINSEQ_1:def 3; then A39: len f2' in dom f2 by A12,A35,A36,FINSEQ_2:9; A40: now assume p1 in L~f1'; then A41: p1 in L~(f1:-q) by Th22; then consider i such that A42: 1 <= i and i+1 <= len(f1:-q) and A43: p1 in LSeg(f1:-q,i) by Th13; A44: 1 + 1 <= len f1 by TOPREAL1:def 10; p1 in LSeg(f1/.1,f1/.(1+1)) by A1,TOPREAL1:6; then A45: p1 in LSeg(f1,1) by A44,TOPREAL1:def 5; i <> 0 by A42; then consider j such that A46: i = j+1 by NAT_1:22; A47: LSeg(f1:-q,i) = LSeg(f1,j+q..f1) by A8,A46,Th10; then p1 in LSeg(f1,1) /\ LSeg(f1,j+q..f1) by A43,A45,XBOOLE_0:def 3; then A48: LSeg(f1,1) meets LSeg(f1,j+q..f1) by XBOOLE_0:4; A49: 1 < q..f1 by A10,A26,REAL_1:def 5; per cases; suppose A50: j = 0; A51: 1+1 <= q..f1 by A49,NAT_1:38; now per cases by A51,REAL_1:def 5; suppose A52: q..f1 = 2; A53: q..f1 <= len f1 by A8,FINSEQ_4:31; now per cases by A52,A53,REAL_1:def 5; suppose len f1 = 2; then len(f1:-q) = len f1 - len f1 + 1 by A8,A52,FINSEQ_5:53; then len(f1:-q) = 0+1 by XCMPLX_1:14; hence contradiction by A41,TOPREAL1:28; suppose len f1 > 2; then 1+2 <= len f1 by NAT_1:38; then LSeg(f1,1) /\ LSeg(f1,1+1) = {f1/.(1+1)} by TOPREAL1:def 8; then p1 in {f1/.2} by A43,A45,A47,A50,A52,XBOOLE_0:def 3; then A54: p1 = f1/.2 by TARSKI:def 1; 1 <> 2 & 2 in dom f1 by A8,A52,FINSEQ_4:30; hence contradiction by A1,A13,A54,PARTFUN2:17; end; hence contradiction; suppose q..f1 > 2; then 1+1 < j+q..f1 by A50; hence contradiction by A48,TOPREAL1:def 9; end; hence contradiction; suppose j <> 0; then 1 <= j by RLVECT_1:99; then 1+1 < j+q..f1 by A49,REAL_1:67; hence contradiction by A48,TOPREAL1:def 9; end; A55: LSeg(f2'/.len f2',f1'/.1) = LSeg(f2,l) by A29,A35,A37,A38,TOPREAL1:def 5; A56: now assume len f1' <> 1; then 1 < len f1' by A27,REAL_1:def 5; then A57: 1+1 <= len f1' by NAT_1:38; now let x be set; hereby assume A58: x in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1); A59: LSeg(f2'/.len f2',f1'/.1) c=L~f2 by A55,TOPREAL3:26; reconsider m = len f1'-2 as Nat by A57,INT_1:18; m+1+1 = m+(1+1) by XCMPLX_1:1; then m+1+1 = len f1' by XCMPLX_1:27 .= len(f1:-q) by FINSEQ_5:def 3; then LSeg(f1',1) = LSeg(f1:-q,m+1) by Th2 .= LSeg(f1,m+q..f1) by A8,Th10; then LSeg(f1',1) c= L~f1 by TOPREAL3:26; then A60: LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1) c= {p1,p2} by A5,A59,XBOOLE_1:27; LSeg(f1',1) c= L~f1' by TOPREAL3:26; then not p1 in LSeg(f1',1) by A40; then not p1 in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1) by XBOOLE_0:def 3; hence x = f1'/.1 by A4,A38,A58,A60,TARSKI:def 2; end; assume A61: x = f1'/.1; then x in LSeg(f1'/.1,f1'/.(1+1)) by TOPREAL1:6; then A62: x in LSeg(f1',1) by A57,TOPREAL1:def 5; x in LSeg(f2'/.len f2',f1'/.1) by A61,TOPREAL1:6; hence x in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1) by A62,XBOOLE_0:def 3; end; hence LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',1) = {f1'/.1} by TARSKI:def 1; end; A63: now per cases; suppose len f2' = 1 & len f1' = 1; then len g2 = 1+1 by FINSEQ_1:35; hence g2 is unfolded by Th27; suppose that A64: len f2' <> 1 and A65: len f1' = 1; A66: len f2' > 1 by A12,A29,A64,REAL_1:def 5; len f2' <> 0 by A30; then consider k such that A67: k+1 = len f2' by NAT_1:22; A68: 1 <= k by A66,A67,NAT_1:38; l+1 <= len f2 by A11,NAT_1:38; then A69: k+(1+1) <= len f2 by A12,A67,XCMPLX_1:1; LSeg(f2',k) = LSeg(f2,k) by A67,Th3; then A70: LSeg(f2',k) /\ LSeg(f2'/.len f2',f1'/.1) = {f2'/.len f2'} by A12,A37,A55,A67,A68,A69,TOPREAL1:def 8; f1' = <*f1'/.1*> by A65,FINSEQ_5:15; hence g2 is unfolded by A67,A70,Th31; suppose that A71: len f2' = 1 and A72: len f1' <> 1; f2' = <*f2'/.len f2'*> by A71,FINSEQ_5:15; hence g2 is unfolded by A34,A56,A72,Th30; suppose that A73: len f2' <> 1 and A74: len f1' <> 1; A75: len f2' > 1 by A12,A29,A73,REAL_1:def 5; len f2' <> 0 by A30; then consider k such that A76: k+1 = len f2' by NAT_1:22; A77: 1 <= k by A75,A76,NAT_1:38; l+1 <= len f2 by A11,NAT_1:38; then A78: k+(1+1) <= len f2 by A12,A76,XCMPLX_1:1; LSeg(f2',k) = LSeg(f2,k) by A76,Th3; then LSeg(f2',k) /\ LSeg(f2'/.len f2',f1'/.1) = {f2'/.len f2'} by A12,A37,A55,A76,A77,A78,TOPREAL1:def 8; hence g2 is unfolded by A34,A56,A74,A76,Th32; end; f1:-q is s.n.c. by A8,Th35; then A79: f1' is s.n.c. by Th36; L~(f1:-q) c= L~f1 by A8,Lm16; then A80: L~f1' c= L~f1 by Th22; L~f2' c= L~f2 by Lm1; then L~f2' /\ L~f1' c= {p1,p2} by A5,A80,XBOOLE_1:27; then A81: L~f2' /\ L~f1' = {} or L~f2' /\ L~f1' = {p1} or L~f2' /\ L~f1' = {p2} or L~f2' /\ L~f1' = {p1,p2} by ZFMISC_1:42; A82: now let i such that 1<=i and A83: i+2<=len f2'; i+(1+1) <= len f2' by A83; then i+1+1 <= len f2' by XCMPLX_1:1; then A84: i+1 < len f2' by NAT_1:38; then LSeg(f2',i) = LSeg(f2,i) by Th3; hence LSeg(f2',i) misses LSeg(f2'/.len f2',f1'/.1) by A12,A55,A84,TOPREAL1:def 9; end; A85: now let i such that A86: 2<=i and A87: i+1 <= len f1'; LSeg(f1',i) c= L~f1' by TOPREAL3:26; then A88: not p1 in LSeg(f1',i) by A40; A89: LSeg(f2'/.len f2',f1'/.1) c=L~f2 by A55,TOPREAL3:26; reconsider m = len f1'-(i+1) as Nat by A87,INT_1:18; m+1+i = m+(i+1) by XCMPLX_1:1; then m+1+i = len f1' by XCMPLX_1:27 .= len(f1:-q) by FINSEQ_5:def 3; then A90: LSeg(f1',i) = LSeg(f1:-q,m+1) by Th2 .= LSeg(f1,m+q..f1) by A8,Th10; A91: now A92: len f1 >= 1+1 by TOPREAL1:def 10; then len f1 >= 1 by AXIOMS:22; then reconsider k = len f1 - 1 as Nat by INT_1:18; A93: k+1 = len f1 by XCMPLX_1:27; then A94: 1 <= k by A92,REAL_1:53; p2 in LSeg(f1/.k,f1/.len f1) by A3,TOPREAL1:6; then A95: p2 in LSeg(f1,k) by A93,A94,TOPREAL1:def 5; A96: len f1' = len(f1:-q) by FINSEQ_5:def 3; A97: len f1 - i = len f1 - q..f1 + q..f1 - i by XCMPLX_1:27 .= len f1 - q..f1 + 1 - 1 + q..f1 - i by XCMPLX_1:26 .= len f1' - 1 + q..f1 - i by A8,A96,FINSEQ_5:53 .= len f1' - 1 - i + q..f1 by XCMPLX_1:29 .= m + q..f1 by XCMPLX_1:36; per cases; suppose i = 1+1; then A98: m + q..f1 + 1 = len f1 - 1 - 1 + 1 by A97,XCMPLX_1:36 .= k by XCMPLX_1:27; A99: 1 <= q..f1 by A8,FINSEQ_4:31; q..f1 <= m+q..f1 by NAT_1:29; then A100: 1 <= m + q..f1 by A99,AXIOMS:22; m+q..f1+(1+1) = len f1 by A93,A98,XCMPLX_1:1; then A101: LSeg(f1,m + q..f1) /\ LSeg(f1,k) = {f1/.k} by A98,A100,TOPREAL1:def 8; A102: 1 <= k by A92,REAL_1:84; k <= len f1 by A93,NAT_1:29; then A103: k in dom f1 by A102,FINSEQ_3:27; A104: len f1 in dom f1 by FINSEQ_5:6; p2 in LSeg(f1/.k,f1/.(k+1)) by A3,A93,TOPREAL1:6; then A105: p2 in LSeg(f1,k) by A93,A102,TOPREAL1:def 5; assume p2 in LSeg(f1',i); then p2 in {f1/.k} by A90,A101,A105,XBOOLE_0:def 3; then f1/.len f1 = f1/.k by A3,TARSKI:def 1; then len f1 - k = len f1 - len f1 by A103,A104,PARTFUN2:17 .= 0 by XCMPLX_1:14; then 0 = len f1 - len f1 + 1 by XCMPLX_1:37 .= 0 + 1 by XCMPLX_1:14; hence contradiction; suppose i <> 2; then 2 < i by A86,REAL_1:def 5; then 2+1 <= i by NAT_1:38; then len f1 - i <= len f1 - (1+2) by REAL_2:106; then len f1 - i <= len f1 - 1 - 2 by XCMPLX_1:36; then A106: len f1 - i + (1+1) <= k by REAL_1:84; len f1 - i + (1+1) = m + q..f1 + 1 + 1 by A97,XCMPLX_1:1; then m+q..f1 +1 < k by A106,NAT_1:38; then LSeg(f1,k) misses LSeg(f1,m+q..f1) by TOPREAL1:def 9; then LSeg(f1,k) /\ LSeg(f1,m+q..f1) = {} by XBOOLE_0:def 7; hence not p2 in LSeg(f1',i) by A90,A95,XBOOLE_0:def 3; end; LSeg(f1',i) c= L~f1 by A90,TOPREAL3:26; then A107: LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',i) c= {p1,p2} by A5,A89,XBOOLE_1:27; now given x being set such that A108: x in LSeg(f2'/.len f2',f1'/.1) /\ LSeg(f1',i); x = p1 or x = p2 by A107,A108,TARSKI:def 2; hence contradiction by A88,A91,A108,XBOOLE_0:def 3; end; then LSeg(f1',i) /\ LSeg(f2'/.len f2',f1'/.1) = {} by XBOOLE_0:def 1; hence LSeg(f1',i) misses LSeg(f2'/.len f2',f1'/.1) by XBOOLE_0:def 7; end; now assume p2 in L~f2'; then consider i such that A109: 1 <= i and A110: i+1 <= len(f2') and A111: p2 in LSeg(f2',i) by Th13; A112: LSeg(f2',i) = LSeg(f2,i) by A110,Th3; p2 in LSeg(f2/.len f2',p2) by TOPREAL1:6; then p2 in LSeg(f2,len f2') by A4,A12,A29,A35,TOPREAL1:def 5; then A113: p2 in LSeg(f2,i) /\ LSeg(f2,len f2') by A111,A112,XBOOLE_0:def 3 ; then A114: LSeg(f2,i) meets LSeg(f2,len f2') by XBOOLE_0:4; A115: len f2 <> len f2' by A11,TOPREAL1:3; per cases; suppose A116: i+1 = len(f2'); then i + (1+1) = len f2 by A12,A35,XCMPLX_1:1; then LSeg(f2,i) /\ LSeg(f2,len f2') = {f2/.len f2'} by A109,A116,TOPREAL1:def 8; then p2 = f2/.len f2' by A113,TARSKI:def 1; hence contradiction by A4,A9,A39,A115,PARTFUN2:17; suppose i+1 <> len(f2'); then i+1 < len(f2') by A110,REAL_1:def 5; hence contradiction by A114,TOPREAL1:def 9; end; then not p1 in L~f2' /\ L~f1' & not p2 in L~f2' /\ L~f1' by A40,XBOOLE_0:def 3; then L~f2' misses L~f1' by A81,TARSKI:def 1,def 2,XBOOLE_0:def 7; then A117: f2'^f1' is s.n.c. by A79,A82,A85,Th37; f1:-q is special by A8,Th41; then A118: f1' is special by Th42; (f2'/.len f2')`1 = (f1'/.1)`1 or (f2'/.len f2')`2 = (f1'/.1)`2 by A29,A35,A37,A38,TOPREAL1:def 7; then g2 is special by A118,Lm14; then reconsider g2 as S-Sequence_in_R2 by A25,A31,A63,A117,TOPREAL1:def 10; take g1,g2; thus A119: p1 = g1/.1 by A1,A8,FINSEQ_5:47; A120: 1 in dom g2 by FINSEQ_5:6; hence A121: g2/.1 = g2.1 by FINSEQ_4:def 4 .= f2'.1 by A32,FINSEQ_1:def 7 .= f2'/.1 by A32,FINSEQ_4:def 4 .= p1 by A2,A32,TOPREAL1:1; thus A122: q = g1/.(q..f1) by A8,FINSEQ_5:48 .= g1/.len g1 by A8,FINSEQ_5:45; A123: 1 in dom(f1:-q) by FINSEQ_5:6; A124: len g2 in dom g2 by FINSEQ_5:6; hence A125: g2/.len g2 = g2.(len g2) by FINSEQ_4:def 4 .= g2.(len f2' + len f1') by FINSEQ_1:35 .= f1'.(len f1') by A28,FINSEQ_1:def 7 .= f1'.(len (f1:-q)) by FINSEQ_5:def 3 .= (f1:-q).1 by FINSEQ_5:65 .= (f1:-q)/.1 by A123,FINSEQ_4:def 4 .= q by FINSEQ_5:56; len g1 >= 2 & len g2 >= 2 by TOPREAL1:def 10; then A126: rng g1 c= L~g1 & rng g2 c= L~g2 by Th18; A127: len g1 in dom g1 by FINSEQ_5:6; A128: 1 in dom g1 by FINSEQ_5:6; A129: L~f2 \/ L~f1' = L~(f2'^<*p2*>) \/ L~f1' by A4,A35,FINSEQ_5:24 .= L~f2' \/ LSeg(f2'/.len f2',f1'/.1) \/ L~f1' by A4,A32,A38,Th19,RELAT_1:60 .= L~g2 by A28,A33,Th23,RELAT_1:60; thus {p1,q} = L~g1 /\ L~g2 proof hereby let x be set; assume A130: x in {p1,q}; per cases by A130,TARSKI:def 2; suppose A131: x = p1; p1 in rng g1 & p1 in rng g2 by A119,A120,A121,A128,PARTFUN2:4; hence x in L~g1 /\ L~g2 by A126,A131,XBOOLE_0:def 3; suppose A132: x = q; q in rng g1 & q in rng g2 by A122,A124,A125,A127,PARTFUN2:4; hence x in L~g1 /\ L~g2 by A126,A132,XBOOLE_0:def 3; end; A133: L~g1 /\ L~g2 = L~g1 /\ L~f2 \/ L~g1 /\ L~f1' by A129,XBOOLE_1:23; A134: len g1 = q..f1 by A8,FINSEQ_5:45; A135: q..f1 in dom f1 by A8,FINSEQ_4:30; A136: len f1 in dom f1 by FINSEQ_5:6; A137: q = f1.(q..f1) by A8,FINSEQ_4:29 .= f1/.(q..f1) by A135,FINSEQ_4:def 4; per cases; suppose A138: q <> p2; now assume p2 in L~g1; then consider i such that A139: 1 <= i and A140: i+1 <= len g1 and A141: p2 in LSeg(g1,i) by Th13; A142: p2 in LSeg(f1,i) by A140,A141,Th9; A143: q..f1 <= len f1 by A8,FINSEQ_4:31; then 1 <= len f1 by A26,AXIOMS:22; then reconsider j = len f1 - 1 as Nat by INT_1:18; A144: j+1 = len f1 by XCMPLX_1:27; 1 < q..f1 by A10,A26,REAL_1:def 5; then 1 < len f1 by A143,AXIOMS:22; then A145: 1 <= j by A144,NAT_1:38; p2 in LSeg(f1/.j,f1/.(j+1)) by A3,A144,TOPREAL1:6; then A146: p2 in LSeg(f1,j) by A144,A145,TOPREAL1:def 5; q..f1 < len f1 by A3,A137,A138,A143,REAL_1:def 5; then A147: q..f1 <= j by A144,NAT_1:38; then A148: i+1 <= j by A134,A140,AXIOMS:22; per cases; suppose A149: i+1 = j; then i+(1+1) = j+1 by XCMPLX_1:1; then LSeg(f1,i) /\ LSeg(f1,i+1) = {f1/.(i+1)} by A139,A144,TOPREAL1:def 8; then p2 in {f1/.(i+1)} by A142,A146,A149,XBOOLE_0:def 3; then p2 = f1/.(i+1) by TARSKI:def 1; hence contradiction by A134,A137,A138,A140,A147,A149,AXIOMS:21; suppose i+1 <> j; then i+1 < j by A148,REAL_1:def 5; then LSeg(f1,i) misses LSeg(f1,j) by TOPREAL1:def 9; then LSeg(f1,i) /\ LSeg(f1,j) = {} by XBOOLE_0:def 7; hence contradiction by A142,A146,XBOOLE_0:def 3; end; then A150: not p2 in L~g1 /\ L~f2 by XBOOLE_0:def 3; A151: L~g1 /\ L~f1' = L~g1 /\ L~(f1:-q) by Th22 .= {q} by A3,A8,A10,A137,A138,Th45; L~g1 c= L~f1 by A8,Lm15; then L~g1 /\ L~f2 c= {p1,p2} by A5,XBOOLE_1:26; then L~g1 /\ L~f2 = {} or L~g1 /\ L~f2 = {p1} or L~g1 /\ L~f2 = {p2} or L~g1 /\ L~f2 = {p1,p2} by ZFMISC_1:42; then L~g1 /\ L~f2 c= {p1} by A150,TARSKI:def 1,def 2,ZFMISC_1:39; then L~g1 /\ L~g2 c= {p1} \/ {q} by A133,A151,XBOOLE_1:9; hence L~g1 /\ L~g2 c= {p1,q} by ENUMSET1:41; suppose A152: q = p2; p2..f1 = len f1 by A3,A136,FINSEQ_5:44; then A153: len(f1:-q) = len f1 - len f1 + 1 by A8,A152,FINSEQ_5:53 .= 0+1 by XCMPLX_1:14; A154: L~g1 /\ L~f1' = L~g1 /\ L~(f1:-q) by Th22 .= L~g1 /\ {} by A153,TOPREAL1:28 .= {}; L~g1 c= L~f1 by A8,Lm15; hence L~g1 /\ L~g2 c= {p1,q} by A5,A133,A152,A154,XBOOLE_1:26; end; thus P = L~(f1-:q) \/ L~(f1:-q) \/ L~f2 by A6,A8,Th25 .= L~g1 \/ (L~f2 \/ L~(f1:-q)) by XBOOLE_1:4 .= L~g1 \/ L~g2 by A129,Th22; end; theorem Th55: p1,p2 split P & q in P & q <> p1 implies p1,q split P proof assume p1 <> p2; given f1,f2 being S-Sequence_in_R2 such that A1: p1 = f1/.1 and A2: p1 = f2/.1 and A3: p2 = f1/.len f1 and A4: p2 = f2/.len f2 and A5: L~f1 /\ L~f2 = {p1,p2} and A6: P = L~f1 \/ L~f2; assume A7: q in P; assume A8: q <> p1; hence p1 <> q; per cases by A6,A7,XBOOLE_0:def 2; suppose A9: q in L~f1; now per cases; suppose q in rng f1; hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm17; suppose A10: not q in rng f1; consider i such that A11: 1 <= i and A12: i+1 <= len f1 and A13: q in LSeg(f1,i) by A9,Th13; reconsider f1' = Ins(f1,i,q) as S-Sequence_in_R2 by A10,A13,Th52; A14: q in rng f1' by FINSEQ_5:74; A15: p1 = f1'/.1 by A1,A11,FINSEQ_5:78; len f1' = len f1 + 1 by FINSEQ_5:72; then A16: p2 = f1'/.len f1' by A3,A12,FINSEQ_5:77; L~f1' = L~f1 by A13,Th26; hence thesis by A2,A4,A5,A6,A8,A14,A15,A16,Lm17; end; hence thesis; suppose A17: q in L~f2; now per cases; suppose q in rng f2; hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm17; suppose A18: not q in rng f2; consider i such that A19: 1 <= i and A20: i+1 <= len f2 and A21: q in LSeg(f2,i) by A17,Th13; reconsider f2' = Ins(f2,i,q) as S-Sequence_in_R2 by A18,A21,Th52; A22: q in rng f2' by FINSEQ_5:74; A23: p1 = f2'/.1 by A2,A19,FINSEQ_5:78; len f2' = len f2 + 1 by FINSEQ_5:72; then A24: p2 = f2'/.len f2' by A4,A20,FINSEQ_5:77; L~f2' = L~f2 by A21,Th26; hence thesis by A1,A3,A5,A6,A8,A22,A23,A24,Lm17; end; hence thesis; end; theorem Th56: p1,p2 split P & q in P & q <> p2 implies q,p2 split P proof assume that A1: p1,p2 split P and A2: q in P & q <> p2; p2,p1 split P by A1,Th54; then p2,q split P by A2,Th55; hence thesis by Th54; end; theorem Th57: p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P proof assume that A1: p1,p2 split P and A2: q1 in P and A3: q2 in P and A4: q1 <> q2; A5: p2,p1 split P by A1,Th54; per cases; suppose p1 = q1; hence thesis by A1,A3,A4,Th55; suppose p1 = q2; hence thesis by A2,A4,A5,Th56; suppose p1 <> q1; then p1,q1 split P by A1,A2,Th55; then q2,q1 split P by A3,A4,Th56; hence thesis by Th54; suppose p2 <> q1; then q1,p2 split P by A1,A2,Th56; hence thesis by A3,A4,Th55; end; definition let P be Subset of TOP-REAL 2; redefine attr P is being_special_polygon means :Def2: ex p1,p2 st p1,p2 split P; compatibility proof thus P is being_special_polygon implies ex p1,p2 st p1,p2 split P proof given p1,p2 being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2 such that A1: p1 <> p2 and p1 in P & p2 in P and A2: P1 is_S-P_arc_joining p1,p2 and A3: P2 is_S-P_arc_joining p1,p2 and A4: P1 /\ P2 = {p1,p2} & P = P1 \/ P2; take p1,p2; thus p1 <> p2 by A1; consider f1 such that A5: f1 is_S-Seq and A6: P1 = L~f1 & p1=f1/.1 & p2=f1/.len f1 by A2,TOPREAL4:def 1; consider f2 such that A7: f2 is_S-Seq and A8: P2 = L~f2 & p1=f2/.1 & p2=f2/.len f2 by A3,TOPREAL4:def 1; reconsider f1,f2 as S-Sequence_in_R2 by A5,A7; take f1,f2; thus p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 by A4,A6,A8; end; given p1,p2 such that A9: p1,p2 split P; consider f1,f2 being S-Sequence_in_R2 such that A10: p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 and A11: L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 by A9,Def1; take p1,p2, P1=L~f1, P2=L~f2; thus p1 <> p2 by A9,Def1; A12: {p1,p2} c= P by A11,XBOOLE_1:29; p1 in {p1,p2} & p2 in {p1,p2} by TARSKI:def 2; hence p1 in P & p2 in P by A12; thus ex f st f is_S-Seq & P1 = L~f & p1=f/.1 & p2=f/.len f by A10; thus ex f st f is_S-Seq & P2 = L~f & p1=f/.1 & p2=f/.len f by A10; thus thesis by A11; end; synonym P is special_polygonal; end; Lm18: for P being Subset of TOP-REAL 2 holds P is_special_polygon implies ex p1,p2 st p1 <> p2 & p1 in P & p2 in P proof let P be Subset of TOP-REAL 2; assume P is_special_polygon; then ex p1,p2 being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2 st p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 by TOPREAL4:def 2; hence thesis; end; definition let r1,r2,r1',r2'; func [.r1,r2,r1',r2'.] -> Subset of TOP-REAL 2 equals :Def3: { p: p`1 = r1 & p`2 <= r2' & p`2 >= r1' or p`1 <= r2 & p`1 >= r1 & p`2 = r2' or p`1 <= r2 & p`1 >= r1 & p`2 = r1' or p`1 = r2 & p`2 <= r2' & p`2 >= r1'}; coherence proof defpred X[Element of TOP-REAL 2] means $1`1 = r1 & $1`2 <= r2' & $1`2 >= r1' or $1`1 <= r2 & $1`1 >= r1 & $1`2 = r2' or $1`1 <= r2 & $1`1 >= r1 & $1`2 = r1' or $1`1 = r2 & $1`2 <= r2' & $1`2 >= r1'; deffunc U(Element of TOP-REAL 2) = $1; set P = { U(p): X[p] }; P is Subset of TOP-REAL 2 from SubsetFD; hence thesis; end; end; theorem Th58: r1<r2 & r1'<r2' implies [.r1,r2,r1',r2'.] = ( LSeg(|[r1,r1']|,|[r1,r2']|) \/ LSeg(|[r1,r2']|,|[r2,r2']|) ) \/ ( LSeg(|[r2,r2']|,|[r2,r1']|) \/ LSeg(|[r2,r1']|,|[r1,r1']|) ) proof assume that A1: r1<r2 and A2: r1'<r2'; set P = { p: p`1 = r1 & p`2 <= r2' & p`2 >= r1' or p`1 <= r2 & p`1 >= r1 & p`2 = r2' or p`1 <= r2 & p`1 >= r1 & p`2 = r1' or p`1 = r2 & p`2 <= r2' & p`2 >= r1'}; set P1 = { p: p`1 = r1 & r1'<= p`2 & p`2 <= r2'}; set P2 = { p: p`2 = r2'& r1 <= p`1 & p`1 <= r2 }; set P3 = { p: p`1 = r2 & r1'<= p`2 & p`2 <= r2'}; set P4 = { p: p`2 = r1'& r1 <= p`1 & p`1 <= r2 }; set p1 = |[r1,r1']|, p2 = |[r1,r2']| , p3 = |[r2,r2']|, p4 = |[r2,r1']|; P = P1 \/ P2 \/ (P3 \/ P4) proof hereby let x be set; assume x in P; then consider p such that A3: x = p and A4: p`1 = r1 & p`2 <= r2' & p`2 >= r1' or p`1 <= r2 & p`1 >= r1 & p`2 = r2' or p`1 <= r2 & p`1 >= r1 & p`2 = r1' or p`1 = r2 & p`2 <= r2' & p`2 >= r1'; x in P1 or x in P2 or x in P3 or x in P4 by A3,A4; then x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2; hence x in P1 \/ P2 \/ (P3 \/ P4) by XBOOLE_0:def 2; end; let x be set; assume x in P1 \/ P2 \/ (P3 \/ P4); then A5: x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 2; per cases by A5,XBOOLE_0:def 2; suppose x in P1; then ex p st x = p & p`1 = r1 & r1'<= p`2 & p`2 <= r2'; hence x in P; suppose x in P2; then ex p st x = p & p`2 = r2'& r1 <= p`1 & p`1 <= r2; hence x in P; suppose x in P3; then ex p st x = p & p`1 = r2 & r1'<= p`2 & p`2 <= r2'; hence x in P; suppose x in P4; then ex p st x = p & p`2 = r1'& r1 <= p`1 & p`1 <= r2; hence x in P; end; hence [.r1,r2,r1',r2'.] = P1 \/ P2 \/ (P3 \/ P4) by Def3 .= LSeg(p1,p2) \/ P2 \/ (P3 \/ P4) by A2,TOPREAL3:15 .= LSeg(p1,p2) \/ LSeg(p2,p3) \/ (P3 \/ P4) by A1,TOPREAL3:16 .= LSeg(p1,p2) \/ LSeg(p2,p3) \/ (LSeg(p3,p4) \/ P4) by A2,TOPREAL3:15 .= LSeg(p1,p2) \/ LSeg(p2,p3) \/ (LSeg(p3,p4) \/ LSeg(p4,p1)) by A1, TOPREAL3:16; end; theorem Th59: r1<r2 & r1'<r2' implies [.r1,r2,r1',r2'.] is special_polygonal proof assume that A1: r1<r2 and A2: r1'<r2'; set p1 = |[r1,r1']|, p2 = |[r1,r2']| , p3 = |[r2,r2']|, p4 = |[r2,r1']|; take p1,p3; thus p1 <> p3 by A1,Th1; A3: p1`1 = r1 & p1`2 = r1' & p2`1 = r1 & p2`2 = r2' & p3`1 = r2 & p3`2 = r2' & p4`1 = r2 & p4`2 = r1' by EUCLID:56; set f1 = <* p1,p2,p3 *>, f2 = <* p1,p4,p3 *>; A4: len f1 = 3 & len f2 = 3 by FINSEQ_1:62; reconsider f1,f2 as S-Sequence_in_R2 by A1,A2,A3,TOPREAL3:41,42; take f1,f2; thus p1 = f1/.1 & p1 = f2/.1 & p3 = f1/.len f1 & p3 = f2/.len f2 by A4,FINSEQ_4:27; A5: L~f1 = LSeg(p1,p2) \/ LSeg(p2,p3) by TOPREAL3:23; A6: L~f2 = LSeg(p3,p4) \/ LSeg(p4,p1) by TOPREAL3:23; hence L~f1 /\ L~f2 = ((LSeg(p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p3,p4)) \/ ((LSeg(p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p4,p1)) by A5,XBOOLE_1:23 .= ((LSeg(p2,p1) \/ LSeg(p3,p2)) /\ LSeg(p4,p3)) \/ {p1} by A2,A3,TOPREAL3:34 .= {p3} \/ {p1} by A1,A3,TOPREAL3:35 .= {p1,p3} by ENUMSET1:41; thus L~f1 \/ L~f2 = [.r1,r2,r1',r2'.] by A1,A2,A5,A6,Th58; end; theorem Th60: R^2-unit_square = [.0,1,0,1.] by Def3,TOPREAL1:def 3; definition cluster special_polygonal Subset of TOP-REAL 2; existence proof take A = [.0,1,0,1.]; thus A is special_polygonal by Th59; end; end; theorem Th61: R^2-unit_square is special_polygonal by Th59,Th60; definition cluster special_polygonal Subset of TOP-REAL 2; existence by Th61; cluster special_polygonal -> non empty Subset of TOP-REAL 2; coherence proof let P be Subset of TOP-REAL 2; assume P is special_polygonal; then ex p1,p2 st p1 <> p2 & p1 in P & p2 in P by Lm18; hence P is non empty; end; cluster special_polygonal -> non trivial Subset of TOP-REAL 2; coherence proof let P be Subset of TOP-REAL 2; assume P is special_polygonal; then ex p1,p2 st p1 <> p2 & p1 in P & p2 in P by Lm18; hence P is non trivial by SPPOL_1:4; end; end; definition mode Special_polygon_in_R2 is special_polygonal Subset of TOP-REAL 2; end; theorem Th62: P is being_S-P_arc implies P is compact proof assume P is being_S-P_arc; then reconsider P as being_S-P_arc Subset of TOP-REAL 2; consider f being map of I[01], (TOP-REAL 2)|P such that A1: f is_homeomorphism by TOPREAL1:36; A2: f is continuous by A1,TOPS_2:def 5; A3: I[01] is compact by HEINE:11,TOPMETR:27; rng f = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5; then (TOP-REAL 2)|P is compact by A2,A3,COMPTS_1:23; hence thesis by COMPTS_1:12; end; theorem for G being Special_polygon_in_R2 holds G is compact proof let G be Special_polygon_in_R2; consider p,q being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2 such that p<>q & p in G & q in G and A1: P1 is_S-P_arc_joining p,q & P2 is_S-P_arc_joining p,q and P1 /\ P2 = {p,q} and A2: G = P1 \/ P2 by TOPREAL4:def 2; reconsider P1,P2 as Subset of TOP-REAL 2; P1 is_S-P_arc & P2 is_S-P_arc by A1,TOPREAL4:2; then P1 is compact & P2 is compact by Th62; hence thesis by A2,COMPTS_1:19; end; theorem Th64: P is special_polygonal implies for p1,p2 st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P proof assume P is special_polygonal; then ex q1,q2 st q1,q2 split P by Def2; hence thesis by Th57; end; theorem P is special_polygonal implies for p1,p2 st p1 <> p2 & p1 in P & p2 in P ex P1,P2 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 proof assume A1: P is special_polygonal; let p1,p2; assume p1 <> p2 & p1 in P & p2 in P; then p1,p2 split P by A1,Th64; then consider f1,f2 being S-Sequence_in_R2 such that A2: p1 = f1/.1 and A3: p1 = f2/.1 and A4: p2 = f1/.len f1 and A5: p2 = f2/.len f2 and A6: L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 by Def1; take P1 = L~f1, P2 = L~f2; thus P1 is_S-P_arc_joining p1,p2 by A2,A4,TOPREAL4:def 1; thus P2 is_S-P_arc_joining p1,p2 by A3,A5,TOPREAL4:def 1; thus P1 /\ P2 = {p1,p2} & P = P1 \/ P2 by A6; end;