:: Finite Sequences and Tuples of Elements of a Non-empty Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2017 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, XBOOLE_0, SUBSET_1, FINSEQ_1, XXREAL_0, CARD_1,
ARYTM_1, ARYTM_3, TARSKI, RELAT_1, FUNCT_1, ORDINAL4, FUNCT_2, FUNCOP_1,
ZFMISC_1, PARTFUN1, FINSEQ_2, PBOOLE, CARD_3, ORDINAL1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, DOMAIN_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCT_3, FINSEQ_1, BINOP_1, PBOOLE, FUNCOP_1, CARD_3, XXREAL_0;
constructors RELAT_2, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1,
SQUARE_1, NAT_1, FINSEQ_1, RELSET_1, PBOOLE, CARD_3, SETFAM_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2,
FUNCOP_1, XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, CARD_3;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
begin
reserve i,j,k,l for natural Number;
reserve A for set, a,b,x,x1,x2,x3 for object;
reserve D,D9,E for non empty set;
reserve d,d1,d2,d3 for Element of D;
reserve d9,d19,d29,d39 for Element of D9;
reserve p,q,r for FinSequence;
:: Auxiliary theorems
::$CT
theorem :: FINSEQ_2:2
l = min(i,j) implies Seg i /\ Seg j = Seg l;
theorem :: FINSEQ_2:3
i <= j implies max(0,i-j) = 0;
theorem :: FINSEQ_2:4
j <= i implies max(0,i-j) = i-j;
theorem :: FINSEQ_2:5
max(0,i-j) is Element of NAT;
::$CT
theorem :: FINSEQ_2:7
i in Seg (l+1) implies i in Seg l or i = l+1;
theorem :: FINSEQ_2:8
i in Seg l implies i in Seg(l+j);
:: Additional propositions related to Finite Sequences
theorem :: FINSEQ_2:9
len p = len q & (for j being Nat st j in dom p holds p.j = q.j) implies p = q
;
theorem :: FINSEQ_2:10
b in rng p implies ex i being Nat st i in dom p & p.i = b;
theorem :: FINSEQ_2:11
for D being set for p being FinSequence of D st i in dom p holds p.i in D;
theorem :: FINSEQ_2:12
for D being set holds (for i being Nat st i in dom p holds p.i in D)
implies p is FinSequence of D;
theorem :: FINSEQ_2:13
<*d1,d2*> is FinSequence of D;
theorem :: FINSEQ_2:14
<*d1,d2,d3*> is FinSequence of D;
theorem :: FINSEQ_2:15
i in dom p implies i in dom(p^q);
theorem :: FINSEQ_2:16
len(p^<*a*>) = len p + 1;
theorem :: FINSEQ_2:17
p^<*a*> = q^<*b*> implies p = q & a = b;
theorem :: FINSEQ_2:18
len p = i + 1 implies ex q,a st p = q^<*a*>;
theorem :: FINSEQ_2:19
for p being FinSequence of A st len p <> 0 ex q being
FinSequence of A, d being Element of A st p = q^<*d*>;
theorem :: FINSEQ_2:20
q = p|(Seg i) & len p <= i implies p = q;
theorem :: FINSEQ_2:21
q = p|(Seg i) implies len q = min(i,len p);
theorem :: FINSEQ_2:22
len r = i+j implies ex p,q st len p = i & len q = j & r = p^q;
theorem :: FINSEQ_2:23
for r being FinSequence of D st len r = i+j ex p,q being
FinSequence of D st len p = i & len q = j & r = p^q;
scheme :: FINSEQ_2:sch 1
SeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}: ex z being
FinSequence of D() st len z = i() & for j being Nat st j in dom z holds z.j = F
(j);
scheme :: FINSEQ_2:sch 2
IndSeqD{D()->set, P[set]}: for p being FinSequence of D() holds P[p]
provided
P[<*> D()] and
for p being FinSequence of D() for x being Element of D() st P[p]
holds P[p^<*x*>];
theorem :: FINSEQ_2:24
for D being set, D1 being Subset of D for p being FinSequence of D1
holds p is FinSequence of D;
theorem :: FINSEQ_2:25
for f being Function of Seg i, D holds f is FinSequence of D;
theorem :: FINSEQ_2:26
for p being FinSequence of D holds p is Function of dom p, D;
theorem :: FINSEQ_2:27
for f being sequence of D holds f|(Seg i) is FinSequence of D;
theorem :: FINSEQ_2:28
for f being sequence of D st q = f|(Seg i) holds len q = i;
theorem :: FINSEQ_2:29
for f being Function st rng p c= dom f & q = f*p holds len q = len p;
theorem :: FINSEQ_2:30
D = Seg i implies for p being FinSequence for q being
FinSequence of D st i <= len p holds p*q is FinSequence;
theorem :: FINSEQ_2:31
D = Seg i implies for p being FinSequence of D9 for q being
FinSequence of D st i <= len p holds p*q is FinSequence of D9;
theorem :: FINSEQ_2:32
for A,D being set for p being FinSequence of A for f being
Function of A,D holds f*p is FinSequence of D;
theorem :: FINSEQ_2:33
for p being FinSequence of A
for f being Function of A,D9 st q = f*p holds len q = len p;
theorem :: FINSEQ_2:34
for x being set, f being Function st x in dom f holds f*<*x*> = <*f.x*>;
theorem :: FINSEQ_2:35
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds f*p = <*f.x1*>;
theorem :: FINSEQ_2:36
for p being FinSequence of D for f being Function of D,D9 st p =
<*x1,x2*> holds f*p = <*f.x1,f.x2*>;
theorem :: FINSEQ_2:37
for p being FinSequence of D for f being Function of D,D9 st p =
<*x1,x2,x3*> holds f*p = <*f.x1,f.x2,f.x3*>;
theorem :: FINSEQ_2:38
for f being Function of Seg i,Seg j st (j = 0 implies i = 0) & j <= len p
holds p*f is FinSequence;
theorem :: FINSEQ_2:39
for f being Function of Seg i,Seg i st i <= len p holds p*f is
FinSequence;
theorem :: FINSEQ_2:40
for f being Function of dom p,dom p holds p*f is FinSequence;
theorem :: FINSEQ_2:41
for f being Function of Seg i,Seg i st rng f = Seg i & i <= len
p & q = p*f holds len q = i;
theorem :: FINSEQ_2:42
for f being Function of dom p,dom p st rng f = dom p & q = p*f
holds len q = len p;
theorem :: FINSEQ_2:43
for f being Permutation of Seg i st i <= len p & q = p*f holds len q = i;
theorem :: FINSEQ_2:44
for f being Permutation of dom p st q = p*f holds len q = len p;
theorem :: FINSEQ_2:45
for p being FinSequence of D for f being Function of Seg i,Seg j
st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence of D;
theorem :: FINSEQ_2:46
for p being FinSequence of D for f being Function of Seg i,Seg i st i
<= len p holds p*f is FinSequence of D;
theorem :: FINSEQ_2:47
for p being FinSequence of D for f being Function of dom p,dom p
holds p*f is FinSequence of D;
theorem :: FINSEQ_2:48
for k being natural Number holds id Seg k is FinSequence of NAT;
definition
let i be natural Number;
func idseq i -> FinSequence equals
:: FINSEQ_2:def 1
id Seg i;
end;
registration
let k be natural Number;
cluster idseq k -> k-element;
end;
registration
cluster idseq 0 -> empty;
end;
theorem :: FINSEQ_2:49
for k being Element of Seg i holds (idseq i).k = k;
theorem :: FINSEQ_2:50
idseq 1 = <*1*>;
theorem :: FINSEQ_2:51
idseq (i+1) = (idseq i) ^ <*i+1*>;
theorem :: FINSEQ_2:52
idseq 2 = <*1,2*>;
theorem :: FINSEQ_2:53
idseq 3 = <*1,2,3*>;
theorem :: FINSEQ_2:54
len p <= k implies p*(idseq k) = p;
theorem :: FINSEQ_2:55
idseq k is Permutation of Seg k;
theorem :: FINSEQ_2:56
for k being natural Number holds (Seg k) --> a is FinSequence;
registration
let i be natural Number, a be object;
cluster (Seg i) --> a -> FinSequence-like;
end;
definition
let i be natural Number, a be object;
func i |-> a -> FinSequence equals
:: FINSEQ_2:def 2
Seg i --> a;
end;
registration
let k be natural Number, a be object;
cluster k |-> a -> k-element;
end;
theorem :: FINSEQ_2:57
for d being object, w being set st w in Seg k holds (k |-> d).w = d;
theorem :: FINSEQ_2:58
for a being object holds 0 |-> a = {};
theorem :: FINSEQ_2:59
for a being object holds 1 |-> a = <*a*>;
theorem :: FINSEQ_2:60
for a being object holds (i+1) |-> a = (i |-> a) ^ <*a*>;
theorem :: FINSEQ_2:61
for a being object holds 2 |-> a = <*a,a*>;
theorem :: FINSEQ_2:62
for a being object holds 3 |-> a = <*a,a,a*>;
theorem :: FINSEQ_2:63
for k being natural Number holds k |-> d is FinSequence of D;
theorem :: FINSEQ_2:64
for F being Function st [:rng p,rng q:] c= dom F holds F.:(p,q)
is FinSequence;
theorem :: FINSEQ_2:65
for F being Function st [:rng p,rng q:] c= dom F & r = F.:(p,q)
holds len r = min(len p,len q);
theorem :: FINSEQ_2:66
for F being Function st [:{a},rng p:] c= dom F holds F[;](a,p) is FinSequence
;
theorem :: FINSEQ_2:67
for F being Function st [:{a},rng p:] c= dom F & r = F[;](a,p)
holds len r = len p;
theorem :: FINSEQ_2:68
for F being Function st [:rng p,{a}:] c= dom F holds F[:](p,a) is FinSequence
;
theorem :: FINSEQ_2:69
for F being Function st [:rng p,{a}:] c= dom F & r = F[:](p,a)
holds len r = len p;
theorem :: FINSEQ_2:70
for F being Function of [:D,D9:],E for p being FinSequence of D
for q being FinSequence of D9 holds F.:(p,q) is FinSequence of E;
theorem :: FINSEQ_2:71
for F being Function of [:D,D9:],E for p being FinSequence of D
for q being FinSequence of D9 st r = F.:(p,q) holds len r = min(len p,len q);
theorem :: FINSEQ_2:72
for F being Function of [:D,D9:],E for p being FinSequence of D
for q being FinSequence of D9 st len p = len q & r = F.:(p,q) holds len r = len
p & len r = len q;
theorem :: FINSEQ_2:73
for F being Function of [:D,D9:],E for p being FinSequence of D for p9
being FinSequence of D9 holds F.:(<*>D,p9) = <*>E & F.:(p,<*>D9) = <*>E;
theorem :: FINSEQ_2:74
for F being Function of [:D,D9:],E for p being FinSequence of D for q
being FinSequence of D9 st p = <*d1*> & q = <*d19*> holds F.:(p,q) = <*F.(d1,
d19)*>;
theorem :: FINSEQ_2:75
for F being Function of [:D,D9:],E for p being FinSequence of D for q
being FinSequence of D9 st p = <*d1,d2*> & q = <*d19,d29*> holds F.:(p,q) = <*F
.(d1,d19),F.(d2,d29)*>;
theorem :: FINSEQ_2:76
for F being Function of [:D,D9:],E for p being FinSequence of D for q
being FinSequence of D9 st p = <*d1,d2,d3*> & q = <*d19,d29,d39*> holds F.:(p,q
) = <*F.(d1,d19),F.(d2,d29),F.(d3,d39)*>;
theorem :: FINSEQ_2:77
for F being Function of [:D,D9:],E for p being FinSequence of D9
holds F[;](d,p) is FinSequence of E;
theorem :: FINSEQ_2:78
for F being Function of [:D,D9:],E for p being FinSequence of D9
st r = F[;](d,p) holds len r = len p;
theorem :: FINSEQ_2:79
for F being Function of [:D,D9:],E holds F[;](d,<*>D9) = <*>E;
theorem :: FINSEQ_2:80
for F being Function of [:D,D9:],E for p being FinSequence of D9 st p
= <*d19*> holds F[;](d,p) = <*F.(d,d19)*>;
theorem :: FINSEQ_2:81
for F being Function of [:D,D9:],E for p being FinSequence of D9 st p
= <*d19,d29*> holds F[;](d,p) = <*F.(d,d19),F.(d,d29)*>;
theorem :: FINSEQ_2:82
for F being Function of [:D,D9:],E for p being FinSequence of D9 st p
= <*d19,d29,d39*> holds F[;](d,p) = <*F.(d,d19),F.(d,d29),F.(d,d39)*>;
theorem :: FINSEQ_2:83
for F being Function of [:D,D9:],E for p being FinSequence of D
holds F[:](p,d9) is FinSequence of E;
theorem :: FINSEQ_2:84
for F being Function of [:D,D9:],E for p being FinSequence of D
st r = F[:](p,d9) holds len r = len p;
theorem :: FINSEQ_2:85
for F being Function of [:D,D9:],E holds F[:](<*>D,d9) = <*>E;
theorem :: FINSEQ_2:86
for F being Function of [:D,D9:],E for p being FinSequence of D st p =
<*d1*> holds F[:](p,d9) = <*F.(d1,d9)*>;
theorem :: FINSEQ_2:87
for F being Function of [:D,D9:],E for p being FinSequence of D st p =
<*d1,d2*> holds F[:](p,d9) = <*F.(d1,d9),F.(d2,d9)*>;
theorem :: FINSEQ_2:88
for F being Function of [:D,D9:],E for p being FinSequence of D st p =
<*d1,d2,d3*> holds F[:](p,d9) = <*F.(d1,d9),F.(d2,d9),F.(d3,d9)*>;
:: Tuples
definition
let D be set;
mode FinSequenceSet of D -> set means
:: FINSEQ_2:def 3
a in it implies a is FinSequence of D;
end;
definition
let D be set, S be FinSequenceSet of D;
redefine mode Element of S -> FinSequence of D;
end;
registration
let D be set;
cluster non empty for FinSequenceSet of D;
end;
theorem :: FINSEQ_2:89
for D being set holds D* is FinSequenceSet of D;
definition
let D be set;
redefine func D* -> FinSequenceSet of D;
end;
theorem :: FINSEQ_2:90
for D being set, D9 being FinSequenceSet of D holds D9 c= D*;
theorem :: FINSEQ_2:91
for D9 being Subset of D, S being FinSequenceSet of D9
holds S is FinSequenceSet of D;
reserve s for Element of D*;
registration
let i be natural Number, D;
cluster i-element for FinSequence of D;
end;
definition
let i be natural Number, D be non empty set;
mode Tuple of i,D is i-element FinSequence of D;
end;
definition
let i be natural Number;
let D be set;
func i-tuples_on D -> FinSequenceSet of D equals
:: FINSEQ_2:def 4
{ s where s is Element of D*: len s = i };
end;
registration
let i be natural Number, D;
cluster i-tuples_on D -> non empty;
end;
registration
let D;
let i be natural Number;
cluster -> i-element for Element of i-tuples_on D;
end;
theorem :: FINSEQ_2:92
for D be set, z being FinSequence of D holds
z is Element of (len z)-tuples_on D;
theorem :: FINSEQ_2:93
for D being set holds i-tuples_on D = Funcs(Seg i,D);
theorem :: FINSEQ_2:94
for D being set holds 0-tuples_on D = { <*>D };
theorem :: FINSEQ_2:95
for z being Tuple of 0,D for t being Tuple of i, D
holds z^t = t & t^z = t;
theorem :: FINSEQ_2:96
1-tuples_on D = the set of all <*d*>;
theorem :: FINSEQ_2:97
for z being Tuple of 1,D ex d st z = <*d*>;
theorem :: FINSEQ_2:98
<*d*> in 1-tuples_on D;
theorem :: FINSEQ_2:99
2-tuples_on D = the set of all <*d1,d2*>;
theorem :: FINSEQ_2:100
for z being Tuple of 2,D ex d1,d2 st z = <*d1,d2*>;
theorem :: FINSEQ_2:101
<*d1,d2*> in 2-tuples_on D;
theorem :: FINSEQ_2:102
3-tuples_on D = the set of all <*d1,d2,d3*>;
theorem :: FINSEQ_2:103
for z being Tuple of 3,D ex d1,d2,d3 st z = <*d1,d2,d3*>;
theorem :: FINSEQ_2:104
<*d1,d2,d3*> in 3-tuples_on D;
theorem :: FINSEQ_2:105
(i+j)-tuples_on D = the set of all z^t where z is Tuple of i,D,
t is Tuple of j,D;
theorem :: FINSEQ_2:106
for s being Tuple of i+j,D
ex z being Element of i-tuples_on D, t being Element of j-tuples_on D
st s = z^t;
theorem :: FINSEQ_2:107
for z being Tuple of i,D for t being Tuple of j,D holds
z^t is Tuple of i+j,D;
theorem :: FINSEQ_2:108
D* = union the set of all i-tuples_on D where i is Nat;
theorem :: FINSEQ_2:109
for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i-tuples_on D;
theorem :: FINSEQ_2:110
i-tuples_on D = j-tuples_on A implies i = j;
theorem :: FINSEQ_2:111
idseq i is Element of i-tuples_on NAT;
theorem :: FINSEQ_2:112
i |-> d is Element of i-tuples_on D;
theorem :: FINSEQ_2:113
for z being Tuple of i,D for f being Function of D,D9
holds f*z is Element of i-tuples_on D9;
theorem :: FINSEQ_2:114
for z being Tuple of i,D for f being Function of
Seg i,Seg i st rng f = Seg i holds z*f is Element of i-tuples_on D;
theorem :: FINSEQ_2:115
for z being Tuple of i,D for f being Permutation of Seg i
holds z*f is Tuple of i,D;
theorem :: FINSEQ_2:116
for z being Tuple of i,D for d holds (z^<*d*>).(i+1) = d;
theorem :: FINSEQ_2:117
for z being Tuple of i+1,D ex t being Element of i-tuples_on D, d
st z = t^<*d*>;
theorem :: FINSEQ_2:118
for z being Tuple of i,D holds z*(idseq i) = z;
theorem :: FINSEQ_2:119
for z1,z2 being Tuple of i,D st for j being Nat st j in Seg i holds
z1.j = z2.j holds z1 = z2;
theorem :: FINSEQ_2:120
for F being Function of [:D,D9:],E for z1 being Tuple of i,D
for z2 being Tuple of i,D9 holds F.:(z1,z2) is Element of i
-tuples_on E;
theorem :: FINSEQ_2:121
for F being Function of [:D,D9:],E for z being Tuple of i,D9
holds F[;](d,z) is Element of i-tuples_on E;
theorem :: FINSEQ_2:122
for F being Function of [:D,D9:],E for z being Tuple of i,D
holds F[:](z,d9) is Element of i-tuples_on E;
theorem :: FINSEQ_2:123
(i+j)|->x = (i|->x)^(j|->x);
:: Addendum, 2002.07.08
theorem :: FINSEQ_2:124
for i being natural Number, x being Tuple of i,D holds dom x = Seg i;
theorem :: FINSEQ_2:125
for f being Function, x, y being set st x in dom f & y in dom f holds
f*<*x,y*> = <*f.x,f.y*>;
theorem :: FINSEQ_2:126
for f being Function, x, y, z being set st x in dom f & y in dom f & z
in dom f holds f*<*x,y,z*> = <*f.x,f.y,f.z*>;
theorem :: FINSEQ_2:127
rng <*x1,x2*> = {x1,x2};
theorem :: FINSEQ_2:128
rng <*x1,x2,x3*> = {x1,x2,x3};
begin :: Addenda
:: from SCMFSA_7, 2005.11.21, A.T.
theorem :: FINSEQ_2:129
for p1,p2,q being FinSequence st p1 c= q & p2 c= q & len p1 = len p2
holds p1 = p2;
:: from MODAL_1, 2007.03.14, A.T.
reserve m,n for Nat,
s,w for FinSequence of NAT;
theorem :: FINSEQ_2:130
for D being non empty set,
s being FinSequence of D st s <> {}
ex w being FinSequence of D, n being Element of D st s = <*n*>^w;
:: Moved from AMISTD_2 by AK, 2008.02.02
registration
let D be set;
cluster -> functional for FinSequenceSet of D;
end;
:: from FINSOP_1, 2009.05.23, AT
definition
let D; let n be natural Number; let d;
redefine func n |-> d -> Element of n-tuples_on D;
end;
:: new, 2009.08.15, A.T.
theorem :: FINSEQ_2:131
for z being set holds z is Tuple of i,D iff z in i-tuples_on D;
:: from CATALG_1, 2009.09.08, A.T.
theorem :: FINSEQ_2:132
for A being set, i being (Element of NAT), p being FinSequence
holds p in i-tuples_on A iff len p = i & rng p c= A;
theorem :: FINSEQ_2:133
for A being set, i being (Element of NAT), p being FinSequence of
A holds p in i-tuples_on A iff len p = i;
theorem :: FINSEQ_2:134
for A being set, i being Element of NAT holds i-tuples_on A c= A*;
theorem :: FINSEQ_2:135
for A being set, x being object
holds x in 1-tuples_on A iff ex a being set st
a in A & x = <*a*>;
theorem :: FINSEQ_2:136
for A being set, a being object st <*a*> in 1-tuples_on A holds a in A;
theorem :: FINSEQ_2:137
for A being set, x being object holds x in 2-tuples_on A iff
ex a,b being object st a in A & b in A & x = <*a,b*>;
theorem :: FINSEQ_2:138
for A being set, a,b being object st <*a,b*> in 2-tuples_on A
holds a in A & b in A;
theorem :: FINSEQ_2:139
for A being set, x being object holds x in 3-tuples_on A iff
ex a,b,c being object st a in A & b in A & c in A & x = <*a,b,c*>;
theorem :: FINSEQ_2:140
for A being set,a,b,c being object st <*a,b,c*> in 3-tuples_on A holds
a in A & b in A & c in A;
theorem :: FINSEQ_2:141
for x being object holds
x in i-tuples_on A implies x is i-element FinSequence;
:: from MSUALG_1, 2009.09.18, A.T.
theorem :: FINSEQ_2:142
for A being non empty set, n holds n-tuples_on A c= A*;
:: from AMISTD_3, 2010.01.10, A.T.
theorem :: FINSEQ_2:143
n |-> x = m |-> x implies n = m;
:: from PBOOLE, 2011.04.17, A.T.
reserve i,j,e,u for set,
n for Nat;
definition
let I be set;
let M be ManySortedSet of I;
func M# -> ManySortedSet of I* means
:: FINSEQ_2:def 5
for i being Element of I* holds it.i = product(M*i);
end;
registration
let I be set;
let M be non-empty ManySortedSet of I;
cluster M# -> non-empty;
end;
definition
let a be set;
func *-->a -> sequence of {a}* means
:: FINSEQ_2:def 6
for n being Nat holds it.n = n |-> a;
end;
theorem :: FINSEQ_2:144
for a,b being set holds (a .--> b)*(n|->a) = n |-> b;
theorem :: FINSEQ_2:145
for a being set for M being ManySortedSet of {a} st M = a .--> D holds
(M#* *-->a).n = Funcs(Seg n, D);
registration
let i be natural Number;
cluster i |-> 0 -> empty-yielding;
end;
:: new, 2011.10.03, A.K.
registration
let D be set;
cluster -> FinSequence-membered for FinSequenceSet of D;
end;
definition
let D be set;
let F be FinSequenceSet of D, f be sequence of F, n be natural Number;
redefine func f.n -> FinSequence of D;
end;