:: Finite Sequences and Tuples of Elements of a Non-empty Sets
::  by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: 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, 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;