:: Segments of Natural Numbers and Finite Sequences :: by Grzegorz Bancerek and Krzysztof Hryniewiecki :: :: Received April 1, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, FUNCT_1, SUBSET_1, XXREAL_0, TARSKI, XCMPLX_0, XBOOLE_0, CARD_1, ARYTM_3, RELAT_1, FINSET_1, ZFMISC_1, ORDINAL1, PARTFUN1, FUNCOP_1, ORDINAL4, ARYTM_1, FINSEQ_1, ORDINAL2, VALUED_0, FUNCT_2, UPROOTS; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, FUNCOP_1, WELLORD2, ORDINAL1, NAT_1, CARD_1, NUMBERS, PARTFUN1, FINSET_1, XXREAL_0, FUNCT_2, INT_1, VALUED_0; constructors WELLORD2, FUNCOP_1, FUNCT_4, XXREAL_0, XREAL_0, NAT_1, CARD_1, RELSET_1, XCMPLX_0, INT_1, VALUED_0, NUMBERS; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0, XREAL_0, NAT_1, CARD_1, NUMBERS, VALUED_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve a for natural Number, k,l,m,n,k1,b,c,i for Nat, x,y,z,y1,y2 for object, X,Y for set, f,g for Function; :: Segments of Natural Numbers definition let n be natural Number; func Seg n -> set equals :: FINSEQ_1:def 1 { k where k is Nat: 1 <= k & k <= n }; end; definition let n be Nat; redefine func Seg n -> Subset of NAT; end; theorem :: FINSEQ_1:1 for a,b being natural Number holds a in Seg b iff 1 <= a & a <= b; registration let n be zero natural Number; cluster Seg n -> empty; end; theorem :: FINSEQ_1:2 Seg 1 = { 1 } & Seg 2 = { 1,2 }; theorem :: FINSEQ_1:3 for a being natural Number holds a = 0 or a in Seg a; registration let n be non zero natural Number; cluster Seg n -> non empty; end; theorem :: FINSEQ_1:4 for a being natural Number holds a+1 in Seg(a+1); theorem :: FINSEQ_1:5 for a,b being natural Number holds a <= b iff Seg a c= Seg b; theorem :: FINSEQ_1:6 for a,b being natural Number holds Seg a = Seg b implies a = b; theorem :: FINSEQ_1:7 for a,c being natural Number holds c <= a implies Seg c = Seg a /\ Seg c; theorem :: FINSEQ_1:8 for a,c being natural Number holds Seg c = Seg c /\ Seg a implies c <= a; theorem :: FINSEQ_1:9 for a being natural Number holds Seg a \/ { a+1 } = Seg (a+1); theorem :: FINSEQ_1:10 for k being natural Number holds Seg k = Seg(k + 1) \ {k + 1}; :: Finite Sequences definition let IT be Relation; attr IT is FinSequence-like means :: FINSEQ_1:def 2 ex n st dom IT = Seg n; end; registration cluster empty -> FinSequence-like for Relation; end; definition mode FinSequence is FinSequence-like Function; end; reserve p,q,r,s,t for FinSequence; registration let n be natural Number; cluster Seg n -> finite; end; registration cluster FinSequence-like -> finite for Function; end; registration let n be natural Number; cluster Seg n -> n-element; end; notation let p; synonym len p for card p; end; definition let p; redefine func len p -> Element of NAT means :: FINSEQ_1:def 3 Seg it = dom p; end; definition let p; redefine func dom p -> Subset of NAT; end; theorem :: FINSEQ_1:11 (ex k st dom f c= Seg k) implies ex p st f c= p; scheme :: FINSEQ_1:sch 1 SeqEx{A()->Nat,P[object,object]}: ex p st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k] provided for k st k in Seg A() ex x st P[k,x]; scheme :: FINSEQ_1:sch 2 SeqLambda{A()->Nat,F(object) -> object}: ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k); theorem :: FINSEQ_1:12 z in p implies ex k st k in dom p & z=[k,p.k]; theorem :: FINSEQ_1:13 dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p=q; theorem :: FINSEQ_1:14 len p = len q & (for k st 1 <= k & k <= len p holds p.k = q.k) implies p=q; theorem :: FINSEQ_1:15 p|(Seg a) is FinSequence; theorem :: FINSEQ_1:16 rng p c= dom f implies f*p is FinSequence; theorem :: FINSEQ_1:17 a <= len p & q = p|(Seg a) implies len q = a & dom q = Seg a; :: :: :: FinSequences of D :: :: :: definition let D be set; mode FinSequence of D -> FinSequence means :: FINSEQ_1:def 4 rng it c= D; end; registration let D be set; cluster -> D-valued for FinSequence of D; end; registration cluster empty -> FinSequence-like for Relation; end; registration let D be set; cluster FinSequence-like for PartFunc of NAT,D; end; definition let D be set; redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D; end; reserve D for set; theorem :: FINSEQ_1:18 for p being FinSequence of D holds p|(Seg a) is FinSequence of D; theorem :: FINSEQ_1:19 for D being non empty set ex p being FinSequence of D st len p = a; theorem :: FINSEQ_1:20 p <> {} iff len p >= 1; definition let x be object; func <*x*> -> set equals :: FINSEQ_1:def 5 { [1,x] }; end; definition let D be set; func <*>D -> FinSequence of D equals :: FINSEQ_1:def 6 {}; end; registration let D be set; cluster <*>D -> empty; end; registration let D be set; cluster empty for FinSequence of D; end; definition let p,q; func p^q -> FinSequence means :: FINSEQ_1:def 7 dom it = Seg (len p + len q) & (for k st k in dom p holds it.k=p.k) & for k st k in dom q holds it.(len p + k) = q.k; end; theorem :: FINSEQ_1:21 p = (p ^ q) | (dom p); theorem :: FINSEQ_1:22 len(p^q) = len p + len q; theorem :: FINSEQ_1:23 for k being Nat st len p + 1 <= k & k <= len p + len q holds (p^q).k=q.(k-len p); theorem :: FINSEQ_1:24 for k being Nat st len p < k & k <= len(p^q) holds (p^q).k = q.(k - len p); theorem :: FINSEQ_1:25 for k being Nat st k in dom (p^q) holds (k in dom p or ex n st n in dom q & k=len p + n ); theorem :: FINSEQ_1:26 dom p c= dom(p^q); theorem :: FINSEQ_1:27 x in dom q implies ex k st k=x & len p + k in dom(p^q); theorem :: FINSEQ_1:28 k in dom q implies len p + k in dom(p^q); theorem :: FINSEQ_1:29 rng p c= rng(p^q); theorem :: FINSEQ_1:30 rng q c= rng(p^q); theorem :: FINSEQ_1:31 rng(p^q) = rng p \/ rng q; theorem :: FINSEQ_1:32 p^q^r = p^(q^r); theorem :: FINSEQ_1:33 p^r = q^r or r^p = r^q implies p = q; theorem :: FINSEQ_1:34 p^{} = p & {}^p = p; theorem :: FINSEQ_1:35 p^q = {} implies p={} & q={}; definition let D be set; let p,q be FinSequence of D; redefine func p^q -> FinSequence of D; end; definition let x be object; redefine func <*x*> -> Function means :: FINSEQ_1:def 8 dom it = Seg 1 & it.1 = x; end; registration let x be object; cluster <*x*> -> Function-like Relation-like; end; registration let x be object; cluster <*x*> -> FinSequence-like; end; theorem :: FINSEQ_1:36 p^q is FinSequence of D implies p is FinSequence of D & q is FinSequence of D ; definition let x,y be object; func <*x,y*> -> set equals :: FINSEQ_1:def 9 <*x*>^<*y*>; let z be object; func <*x,y,z*> -> set equals :: FINSEQ_1:def 10 <*x*>^<*y*>^<*z*>; end; registration let x,y be object; cluster <*x,y*> -> Function-like Relation-like; let z be object; cluster <*x,y,z*> -> Function-like Relation-like; end; registration let x,y be object; cluster <*x,y*> -> FinSequence-like; let z be object; cluster <*x,y,z*> -> FinSequence-like; end; theorem :: FINSEQ_1:37 for x being object holds <*x*> = { [1,x] }; theorem :: FINSEQ_1:38 for x being object holds p=<*x*> iff dom p = Seg 1 & rng p = {x}; theorem :: FINSEQ_1:39 for x being object holds p=<*x*> iff len p = 1 & rng p = {x}; theorem :: FINSEQ_1:40 for x being object holds p = <*x*> iff len p = 1 & p.1 = x; theorem :: FINSEQ_1:41 for x being object holds (<*x*>^p).1 = x; theorem :: FINSEQ_1:42 for x being object holds (p^<*x*>).(len p + 1)=x; theorem :: FINSEQ_1:43 for x,y,z being object holds <*x,y,z*>=<*x*>^<*y,z*> & <*x,y,z*>=<*x,y*>^<*z*>; theorem :: FINSEQ_1:44 for x,y being object holds p = <*x,y*> iff len p = 2 & p.1=x & p.2=y; theorem :: FINSEQ_1:45 for x,y,z being object holds p = <*x,y,z*> iff len p = 3 & p.1 = x & p.2 = y & p.3 = z; theorem :: FINSEQ_1:46 p <> {} implies ex q,x st p = q^<*x*>; definition let D be non empty set; let x be Element of D; redefine func <*x*> -> FinSequence of D; end; :: scheme of induction for finite sequences :: scheme :: FINSEQ_1:sch 3 IndSeq{P[FinSequence]}: for p holds P[p] provided P[{}] and for p,x st P[p] holds P[p^<*x*>]; theorem :: FINSEQ_1:47 for p,q,r,s being FinSequence st p^q = r^s & len p <= len r ex t being FinSequence st p^t = r; registration cluster -> NAT-defined for FinSequence; end; definition let D be set; func D* -> set means :: FINSEQ_1:def 11 x in it iff x is FinSequence of D; end; registration let D be set; cluster D* -> non empty; end; theorem :: FINSEQ_1:48 rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q; theorem :: FINSEQ_1:49 {} in D*; scheme :: FINSEQ_1:sch 4 SepSeq{D()->non empty set, P[FinSequence]}: ex X st for x holds x in X iff ex p st p in D()* & P[p] & x=p; :: :: :: Subsequences :: :: :: definition let IT be Function; attr IT is FinSubsequence-like means :: FINSEQ_1:def 12 ex k st dom IT c= Seg k; end; registration cluster FinSubsequence-like for Function; end; definition mode FinSubsequence is FinSubsequence-like Function; end; registration cluster FinSequence-like -> FinSubsequence-like for Function; let p be FinSubsequence, X be set; cluster p|X -> FinSubsequence-like; cluster X|`p -> FinSubsequence-like; end; registration cluster -> NAT-defined for FinSubsequence; end; reserve p9 for FinSubsequence; definition let X; given k being Nat such that X c= Seg k; func Sgm X -> FinSequence of NAT means :: FINSEQ_1:def 13 rng it = X & for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len it & k1=it.l & k2=it.m holds k1 < k2; end; theorem :: FINSEQ_1:50 rng Sgm dom p9 = dom p9; definition let p9; func Seq p9 -> Function equals :: FINSEQ_1:def 14 p9* Sgm(dom p9); end; registration let p9; cluster Seq p9 -> FinSequence-like; end; theorem :: FINSEQ_1:51 for X st ex k st X c= Seg k holds Sgm X = {} iff X = {}; begin :: from FINSET_1, 1998 theorem :: FINSEQ_1:52 :: FINSET_1:def 1 D is finite iff ex p st D = rng p; begin :: Moved from CARD_1, 1999 theorem :: FINSEQ_1:53 Seg n,Seg m are_equipotent implies n = m; theorem :: FINSEQ_1:54 Seg n,n are_equipotent; theorem :: FINSEQ_1:55 card Seg n = card n; theorem :: FINSEQ_1:56 X is finite implies ex n st X,Seg n are_equipotent; theorem :: FINSEQ_1:57 for n being Nat holds card Seg n = n; begin :: Addenda :: from FINSEQ_5 registration let x be object; cluster <*x*> -> non empty; end; :: From SPRECT_1 registration cluster non empty for FinSequence; end; :: From FUNCT_7, actually from GOBOARD4 registration let f1 be FinSequence, f2 be non empty FinSequence; cluster f1^f2 -> non empty; cluster f2^f1 -> non empty; end; registration let x,y be object; cluster <*x,y*> -> non empty; let z be object; cluster <*x,y,z*> -> non empty; end; :: from MATRIX_2 scheme :: FINSEQ_1:sch 5 SeqDEx{D()->non empty set,A()->Nat,P[object,object]}: ex p being FinSequence of D() st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k] provided for k st k in Seg A() ex x being Element of D() st P[k,x]; :: from TOPREAL1 reserve D for set, p for FinSequence of D, m for Nat; definition let m; let p be FinSequence; func p|m -> FinSequence equals :: FINSEQ_1:def 15 p|Seg m; end; definition let D,m,p; redefine func p|m -> FinSequence of D; end; registration let f be FinSequence; cluster f|0 -> empty; end; theorem :: FINSEQ_1:58 len q <= i implies q|i = q; theorem :: FINSEQ_1:59 i <= len q implies len(q|i) = i; registration let f be non empty FinSequence; reduce len (f|1) to 1; cluster f|1 -> 1-element; end; registration let p be non empty FinSequence, n be non zero Nat; cluster p|n -> non empty; end; :: from FSM_1 theorem :: FINSEQ_1:60 i in Seg n implies i+m in Seg (n+m); theorem :: FINSEQ_1:61 i>0 & i+m in Seg (n+m) implies i in Seg n & i in Seg (n+m); :: from LANG1 definition let R be Relation; func R[*] -> Relation means :: FINSEQ_1:def 16 for x,y being object holds [x,y] in it iff x in field R & y in field R & ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y & for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R; end; theorem :: FINSEQ_1:62 for D1,D2 being set st D1 c= D2 holds D1* c= D2*; :: 2005.05.13, A.T. registration let D be set; cluster D* -> functional; end; :: from SCMFSA_7, 2005.11.21, A.T. theorem :: FINSEQ_1:63 for p,q being FinSequence st p c= q holds len p <= len q; theorem :: FINSEQ_1:64 for p,q being FinSequence, i being Nat st 1 <= i & i <= len p holds (p ^ q).i = p.i; theorem :: FINSEQ_1:65 for p,q being FinSequence, i being Nat st 1 <= i & i <= len q holds (p ^ q).(len p + i) = q.i; :: from GRAPH_2, 2006.01.09, A.T. scheme :: FINSEQ_1:sch 6 FinSegRng{n() -> Nat, F(set)->set, P[set]}: {F(i) where i is Nat: i<=n() & P[i]} is finite; theorem :: FINSEQ_1:66 for x1, x2, x3, x4 being set, p being FinSequence st p = <*x1*>^<*x2*>^<*x3*>^<*x4*> holds len p = 4 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4; theorem :: FINSEQ_1:67 for x1, x2, x3, x4, x5 being set, p being FinSequence st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*> holds len p = 5 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5; theorem :: FINSEQ_1:68 for x1, x2, x3, x4, x5, x6 being set, p being FinSequence st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*> holds len p = 6 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6; theorem :: FINSEQ_1:69 for x1, x2, x3, x4, x5, x6, x7 being set, p being FinSequence st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*> holds len p = 7 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 & p.7 = x7; theorem :: FINSEQ_1:70 for x1,x2,x3,x4, x5, x6, x7, x8 being set, p being FinSequence st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*> holds len p = 8 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 & p.7 = x7 & p.8 = x8; theorem :: FINSEQ_1:71 for x1,x2,x3,x4,x5,x6,x7, x8, x9 being set, p being FinSequence st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*> holds len p = 9 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9; :: from SCMFSA_7, 2006.03.14, A.T. theorem :: FINSEQ_1:72 for p being FinSequence holds p | Seg 0 = {}; theorem :: FINSEQ_1:73 for f,g being FinSequence holds f | Seg 0 = g | Seg 0; theorem :: FINSEQ_1:74 for D being non empty set, x being Element of D holds <* x *> is FinSequence of D; theorem :: FINSEQ_1:75 for D being set, p,q being FinSequence of D holds p ^ q is FinSequence of D; :: from GROUP_7, 2007.02.10, AK reserve a, b, c, d, e, f for object; theorem :: FINSEQ_1:76 <*a*> = <*b*> implies a = b; theorem :: FINSEQ_1:77 <*a,b*> = <*c,d*> implies a = c & b = d; theorem :: FINSEQ_1:78 <*a,b,c*> = <*d,e,f*> implies a = d & b = e & c = f; :: from PRVECT_1, 2007.03.09, A.T registration cluster non empty non-empty for FinSequence; end; theorem :: FINSEQ_1:79 for p,q being FinSequence st q = p|Seg n holds len q <= len p; theorem :: FINSEQ_1:80 for p,r being FinSequence st r = p|Seg n ex q being FinSequence st p = r^q; :: from GOBOARD1, PRALG_1, 2007.04.06, A.T registration let D be non empty set; cluster non empty for FinSequence of D; end; registration let D be non empty set; cluster non empty D-valued for FinSequence; end; :: Added by AK, 2007.11.07 definition let p,q be FinSequence; redefine pred p = q means :: FINSEQ_1:def 17 len p = len q & for k st 1 <= k & k <= len p holds p.k = q.k; end; :: from GROEB_2, 2008.10.08, A.T. theorem :: FINSEQ_1:81 for x,y,z being object holds 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*>; theorem :: FINSEQ_1:82 for p being FinSequence, n,m being Nat st m <= n holds p|n|m = p|m; :: from CARD_5, 2008.10.08, A.T. reserve m for Nat; theorem :: FINSEQ_1:83 Seg n = (n+1) \ {0}; :: from CIRCCOMB, 2009.03.27, A.T. registration let n be natural Number; cluster n-element for FinSequence; end; :: from FACIRC_1, 2009.02.16, A.T. registration let x be object; cluster <*x*> -> 1-element; let y be object; cluster <*x,y*> -> 2-element; let z be object; cluster <*x,y,z*> -> 3-element; end; :: new, 2009.08.24, A.T. definition let X be set; attr X is FinSequence-membered means :: FINSEQ_1:def 18 x in X implies x is FinSequence; end; registration cluster empty -> FinSequence-membered for set; end; registration cluster non empty FinSequence-membered for set; end; registration let X be set; cluster X* -> FinSequence-membered; end; theorem :: FINSEQ_1:84 for f being Function st f in D* & x in dom f holds f.x in D; registration cluster FinSequence-membered -> functional for set; end; theorem :: FINSEQ_1:85 for X being FinSequence-membered set ex Y being non empty set st X c= Y*; registration let X be FinSequence-membered set; cluster -> FinSequence-like for Element of X; end; registration let X be FinSequence-membered set; cluster -> FinSequence-membered for Subset of X; end; :: from TREES_1, 2009.09.09, A.T. theorem :: FINSEQ_1:86 for p,q being FinSequence st q = p|Seg n holds len q <= n; theorem :: FINSEQ_1:87 for p,q being FinSequence st p = p^q or p = q^p holds q = {}; theorem :: FINSEQ_1:88 for p,q being FinSequence st p^q = <*x*> holds p = <*x*> & q = {} or p = {} & q = <*x*>; :: missing, 2009.09.26, A.T. theorem :: FINSEQ_1:89 for f being n-element FinSequence holds dom f = Seg n; registration let n,m be natural Number; let f be n-element FinSequence, g be m-element FinSequence; cluster f^g -> (n+m)-element; end; :: from JORDAN7, 2010.02.26, A.T registration cluster increasing -> one-to-one for real-valued FinSequence; end; :: from AMI_6, 2010.04.07, A.T. theorem :: FINSEQ_1:90 for x, y being object st x in dom <*y*> holds x = 1; :: from FOMODEL0, 2011.06.12, A.T. registration let X; cluster X-valued for FinSequence; end; :: new, 2011.10.03, A.K. registration let D be FinSequence-membered set; let f be D-valued Function; let x be object; cluster f.x -> FinSequence-like; end; theorem :: FINSEQ_1:91 x in Seg n implies x = 1 or ... or x = n; theorem :: FINSEQ_1:92 dom <*x,y*> = { 1,2 }; begin :: Fixed ordering of a finite set into a finite sequence registration let A be finite set; cluster onto one-to-one for FinSequence of A; end; definition let A be finite set; func canFS A -> FinSequence equals :: FINSEQ_1:def 19 the one-to-one onto FinSequence of A; end; definition let A be finite set; redefine func canFS A -> FinSequence of A; end; registration let A be finite set; cluster canFS A -> one-to-one onto for FinSequence of A; end; theorem :: FINSEQ_1:93 for A being finite set holds len canFS A = card A; registration let A be finite non empty set; cluster canFS A -> non empty; end; theorem :: FINSEQ_1:94 for a being object holds canFS({a}) = <* a *>; theorem :: FINSEQ_1:95 for A being finite set holds (canFS A)" is Function of A, Seg card A; :: from PNPROC_1, 2012.02.20, A.T. theorem :: FINSEQ_1:96 i > 0 implies {[i,x]} is FinSubsequence; theorem :: FINSEQ_1:97 for q being FinSubsequence holds q = {} iff Seq q = {}; registration cluster -> finite for FinSubsequence; end; reserve x1,x2,y1,y2 for set; theorem :: FINSEQ_1:98 {[x1,y1], [x2,y2]} is FinSequence implies x1 = 1 & x2 = 1 & y1 = y2 or x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1; theorem :: FINSEQ_1:99 <*x1,x2*> = {[1,x1], [2,x2]}; reserve j for Nat; theorem :: FINSEQ_1:100 for q being FinSubsequence holds dom Seq q = dom Sgm dom q; theorem :: FINSEQ_1:101 for q being FinSubsequence holds rng q = rng Seq q; registration cluster one-to-one for FinSequence; end; registration let D; cluster one-to-one for FinSequence of D; end; registration cluster non empty natural-valued for FinSequence; end;