:: Finite Sequences and Tuples of Elements of a Non-empty Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

:: Auxiliary theorems
theorem :: FINSEQ_2:1
for i, j being Nat holds
( min (i,j) is Element of NAT & max (i,j) is Element of NAT ) by ORDINAL1:def_12;

theorem Th2: :: FINSEQ_2:2
for l, i, j being Nat st l = min (i,j) holds
(Seg i) /\ (Seg j) = Seg l
proofend;

theorem Th3: :: FINSEQ_2:3
for i, j being Nat st i <= j holds
max (0,(i - j)) = 0
proofend;

theorem Th4: :: FINSEQ_2:4
for j, i being Nat st j <= i holds
max (0,(i - j)) = i - j
proofend;

theorem :: FINSEQ_2:5
for i, j being Nat holds max (0,(i - j)) is Element of NAT
proofend;

theorem :: FINSEQ_2:6
for i being Nat holds
( min (0,i) = 0 &amp; min (i,0) = 0 &amp; max (0,i) = i &amp; max (i,0) = i ) by XXREAL_0:def_9, XXREAL_0:def_10;

:: Non-empty Segments of Natural Numbers
theorem :: FINSEQ_2:7
for i, l being Nat holds
( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
proofend;

theorem :: FINSEQ_2:8
for i, l, j being Nat st i in Seg l holds
i in Seg (l + j)
proofend;

:: Additional propositions related to Finite Sequences
theorem :: FINSEQ_2:9
for p, q being FinSequence st len p = len q &amp; ( for j being Nat st j in dom p holds
p . j = q . j ) holds
p = q
proofend;

theorem Th10: :: FINSEQ_2:10
for b being set
for p being FinSequence st b in rng p holds
ex i being Nat st
( i in dom p &amp; p . i = b )
proofend;

theorem Th11: :: FINSEQ_2:11
for i being Nat
for D being set
for p being FinSequence of D st i in dom p holds
p . i in D
proofend;

theorem Th12: :: FINSEQ_2:12
for p being FinSequence
for D being set st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D
proofend;

Lm1:  for x1, x2 being set holds rng <*x1,x2*> = {x1,x2}
proofend;

theorem Th13: :: FINSEQ_2:13
for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> is FinSequence of D
proofend;

Lm2:  for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3}
proofend;

theorem Th14: :: FINSEQ_2:14
for D being non empty set
for d1, d2, d3 being Element of D holds <*d1,d2,d3*> is FinSequence of D
proofend;

theorem Th15: :: FINSEQ_2:15
for i being Nat
for p, q being FinSequence st i in dom p holds
i in dom (p ^ q)
proofend;

theorem Th16: :: FINSEQ_2:16
for a being set
for p being FinSequence holds len (p ^ <*a*>) = (len p) + 1
proofend;

theorem :: FINSEQ_2:17
for a, b being set
for p, q being FinSequence st p ^ <*a*> = q ^ <*b*> holds
( p = q &amp; a = b )
proofend;

theorem :: FINSEQ_2:18
for i being Nat
for p being FinSequence st len p = i + 1 holds
ex q being FinSequence ex a being set st p = q ^ <*a*> by CARD_1:27, FINSEQ_1:46;

theorem Th19: :: FINSEQ_2:19
for A being set
for p being FinSequence of A st len p <> 0 holds
ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>
proofend;

theorem Th20: :: FINSEQ_2:20
for i being Nat
for q, p being FinSequence st q = p | (Seg i) &amp; len p <= i holds
p = q
proofend;

theorem :: FINSEQ_2:21
for i being Nat
for q, p being FinSequence st q = p | (Seg i) holds
len q = min (i,(len p))
proofend;

theorem Th22: :: FINSEQ_2:22
for i, j being Nat
for r being FinSequence st len r = i + j holds
ex p, q being FinSequence st
( len p = i &amp; len q = j &amp; r = p ^ q )
proofend;

theorem Th23: :: FINSEQ_2:23
for i, j being Nat
for D being non empty set
for r being FinSequence of D st len r = i + j holds
ex p, q being FinSequence of D st
( len p = i &amp; len q = j &amp; r = p ^ q )
proofend;

scheme :: FINSEQ_2:sch 1
SeqLambdaD{ F1() ->  Nat, F2() ->  non empty set , F3( set ) ->  Element of F2() } :
 ex z being FinSequence of F2() st
( len z = F1() &amp; ( for j being Nat st j in dom z holds
z . j = F3(j) ) )
proofend;

scheme :: FINSEQ_2:sch 2
IndSeqD{ F1() ->  set , P1[ set ] } :
 for p being FinSequence of F1() holds P1[p]
provided
A1: P1[ <*> F1()] and
A2: for p being FinSequence of F1()
for x being Element of F1() st P1[p] holds
P1[p ^ <*x*>]
proofend;

theorem Th24: :: FINSEQ_2:24
for D being set
for D1 being Subset of D
for p being FinSequence of D1 holds p is FinSequence of D
proofend;

theorem Th25: :: FINSEQ_2:25
for i being Nat
for D being non empty set
for f being Function of (Seg i),D holds f is FinSequence of D
proofend;

theorem :: FINSEQ_2:26
for D being non empty set
for p being FinSequence of D holds p is Function of (dom p),D
proofend;

theorem :: FINSEQ_2:27
for i being Nat
for D being non empty set
for f being Function of NAT,D holds f | (Seg i) is FinSequence of D
proofend;

theorem :: FINSEQ_2:28
for i being Nat
for D being non empty set
for q being FinSequence
for f being Function of NAT,D st q = f | (Seg i) holds
len q = i
proofend;

theorem Th29: :: FINSEQ_2:29
for p, q being FinSequence
for f being Function st rng p c= dom f &amp; q = f * p holds
len q = len p
proofend;

theorem Th30: :: FINSEQ_2:30
for i being Nat
for D being non empty set st D = Seg i holds
for p being FinSequence
for q being FinSequence of D st i <= len p holds
p * q is FinSequence
proofend;

theorem :: FINSEQ_2:31
for i being Nat
for D, D9 being non empty set st D = Seg i holds
for p being FinSequence of D9
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D9
proofend;

theorem Th32: :: 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
proofend;

theorem Th33: :: FINSEQ_2:33
for A being set
for D9 being non empty set
for q being FinSequence
for p being FinSequence of A
for f being Function of A,D9 st q = f * p holds
len q = len p
proofend;

theorem :: FINSEQ_2:34
for x being set
for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>
proofend;

theorem :: FINSEQ_2:35
for x1 being set
for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds
f * p = <*(f . x1)*>
proofend;

theorem Th36: :: FINSEQ_2:36
for x1, x2 being set
for D, D9 being non empty set
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1,x2*> holds
f * p = <*(f . x1),(f . x2)*>
proofend;

theorem Th37: :: FINSEQ_2:37
for x1, x2, x3 being set
for D, D9 being non empty set
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)*>
proofend;

theorem Th38: :: FINSEQ_2:38
for i, j being Nat
for p being FinSequence
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) &amp; j <= len p holds
p * f is FinSequence
proofend;

theorem :: FINSEQ_2:39
for i being Nat
for p being FinSequence
for f being Function of (Seg i),(Seg i) st i <= len p holds
p * f is FinSequence by Th38;

theorem :: FINSEQ_2:40
for p being FinSequence
for f being Function of (dom p),(dom p) holds p * f is FinSequence
proofend;

theorem Th41: :: FINSEQ_2:41
for i being Nat
for p, q being FinSequence
for f being Function of (Seg i),(Seg i) st rng f = Seg i &amp; i <= len p &amp; q = p * f holds
len q = i
proofend;

theorem Th42: :: FINSEQ_2:42
for p, q being FinSequence
for f being Function of (dom p),(dom p) st rng f = dom p &amp; q = p * f holds
len q = len p
proofend;

theorem Th43: :: FINSEQ_2:43
for i being Nat
for p, q being FinSequence
for f being Permutation of (Seg i) st i <= len p &amp; q = p * f holds
len q = i
proofend;

theorem :: FINSEQ_2:44
for p, q being FinSequence
for f being Permutation of (dom p) st q = p * f holds
len q = len p
proofend;

theorem Th45: :: FINSEQ_2:45
for i, j being Nat
for D being non empty set
for p being FinSequence of D
for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) &amp; j <= len p holds
p * f is FinSequence of D
proofend;

theorem :: FINSEQ_2:46
for i being Nat
for D being non empty set
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 by Th45;

theorem Th47: :: FINSEQ_2:47
for D being non empty set
for p being FinSequence of D
for f being Function of (dom p),(dom p) holds p * f is FinSequence of D
proofend;

theorem Th48: :: FINSEQ_2:48
for k being Nat holds id (Seg k) is FinSequence of NAT
proofend;

definition
let i be Nat;
func idseq i ->  FinSequence equals :: FINSEQ_2:def 1
 id (Seg i);
coherence
 id (Seg i) is FinSequence by Th48;
end;

:: deftheorem  defines idseq FINSEQ_2:def_1_:_
 for i being Nat holds idseq i = id (Seg i);

registration
let k be Nat;
cluster idseq k -> k -element ;
coherence
 idseq k is k -element
proofend;
end;

registration
cluster idseq 0 ->  empty ;
coherence
 idseq 0 is empty ;
end;

theorem :: FINSEQ_2:49
for i being Nat
for k being Element of Seg i holds (idseq i) . k = k
proofend;

theorem Th50: :: FINSEQ_2:50
idseq 1 = <*1*>
proofend;

theorem Th51: :: FINSEQ_2:51
for i being Nat holds idseq (i + 1) = (idseq i) ^ <*(i + 1)*>
proofend;

theorem Th52: :: FINSEQ_2:52
idseq 2 = <*1,2*> by Th50, Th51;

theorem :: FINSEQ_2:53
idseq 3 = <*1,2,3*> by Th51, Th52;

theorem Th54: :: FINSEQ_2:54
for k being Nat
for p being FinSequence st len p <= k holds
p * (idseq k) = p
proofend;

theorem :: FINSEQ_2:55
for k being Nat holds idseq k is Permutation of (Seg k) ;

theorem Th56: :: FINSEQ_2:56
for k being Nat
for a being set holds (Seg k) --> a is FinSequence
proofend;

registration
let k be Nat;
let a be set ;
cluster(Seg k) --> a ->  FinSequence-like ;
coherence
 (Seg k) --> a is FinSequence-like by Th56;
end;

definition
let i be Nat;
let a be set ;
funci |-> a ->  FinSequence equals :: FINSEQ_2:def 2
(Seg i) --> a;
coherence
 (Seg i) --> a is FinSequence ;
end;

:: deftheorem  defines |-> FINSEQ_2:def_2_:_
 for i being Nat
for a being set holds i |-> a = (Seg i) --> a;

registration
let k be Nat;
let a be set ;
clusterk |-> a -> k -element ;
coherence
 k |-> a is k -element
proofend;
end;

theorem Th57: :: FINSEQ_2:57
for k being Nat
for d, w being set st w in Seg k holds
(k |-> d) . w = d by FUNCOP_1:7;

theorem :: FINSEQ_2:58
for a being set holds 0 |-> a = {} ;

theorem Th59: :: FINSEQ_2:59
for a being set holds 1 |-> a = <*a*>
proofend;

theorem Th60: :: FINSEQ_2:60
for i being Nat
for a being set holds (i + 1) |-> a = (i |-> a) ^ <*a*>
proofend;

theorem Th61: :: FINSEQ_2:61
for a being set holds 2 |-> a = <*a,a*>
proofend;

theorem :: FINSEQ_2:62
for a being set holds 3 |-> a = <*a,a,a*>
proofend;

theorem Th63: :: FINSEQ_2:63
for k being Nat
for D being non empty set
for d being Element of D holds k |-> d is FinSequence of D
proofend;

Lm3:  for i being Nat
for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F &amp; i = min ((len p),(len q)) holds
dom (F .: (p,q)) = Seg i
proofend;

theorem Th64: :: FINSEQ_2:64
for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F holds
F .: (p,q) is FinSequence
proofend;

theorem Th65: :: FINSEQ_2:65
for p, q, r being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F &amp; r = F .: (p,q) holds
len r = min ((len p),(len q))
proofend;

Lm4:  for a being set
for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] (a,p)) = dom p
proofend;

theorem Th66: :: FINSEQ_2:66
for a being set
for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
F [;] (a,p) is FinSequence
proofend;

theorem Th67: :: FINSEQ_2:67
for a being set
for p, r being FinSequence
for F being Function st [:{a},(rng p):] c= dom F &amp; r = F [;] (a,p) holds
len r = len p
proofend;

Lm5:  for a being set
for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] (p,a)) = dom p
proofend;

theorem Th68: :: FINSEQ_2:68
for a being set
for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
F [:] (p,a) is FinSequence
proofend;

theorem Th69: :: FINSEQ_2:69
for a being set
for p, r being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F &amp; r = F [:] (p,a) holds
len r = len p
proofend;

theorem Th70: :: FINSEQ_2:70
for D, D9, E being non empty set
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
proofend;

theorem Th71: :: FINSEQ_2:71
for D, D9, E being non empty set
for r being FinSequence
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))
proofend;

theorem Th72: :: FINSEQ_2:72
for D, D9, E being non empty set
for r being FinSequence
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 &amp; r = F .: (p,q) holds
( len r = len p &amp; len r = len q )
proofend;

theorem :: FINSEQ_2:73
for D, D9, E being non empty set
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 &amp; F .: (p,(<*> D9)) = <*> E )
proofend;

theorem :: FINSEQ_2:74
for D, D9, E being non empty set
for d1 being Element of D
for d19 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st p = <*d1*> &amp; q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>
proofend;

theorem :: FINSEQ_2:75
for D, D9, E being non empty set
for d1, d2 being Element of D
for d19, d29 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D
for q being FinSequence of D9 st p = <*d1,d2*> &amp; q = <*d19,d29*> holds
F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*>
proofend;

theorem :: FINSEQ_2:76
for D, D9, E being non empty set
for d1, d2, d3 being Element of D
for d19, d29, d39 being Element of D9
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*> &amp; q = <*d19,d29,d39*> holds
F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*>
proofend;

theorem Th77: :: FINSEQ_2:77
for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E
for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E
proofend;

theorem Th78: :: FINSEQ_2:78
for D, D9, E being non empty set
for d being Element of D
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st r = F [;] (d,p) holds
len r = len p
proofend;

theorem :: FINSEQ_2:79
for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E holds F [;] (d,(<*> D9)) = <*> E
proofend;

theorem :: FINSEQ_2:80
for D, D9, E being non empty set
for d being Element of D
for d19 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D9 st p = <*d19*> holds
F [;] (d,p) = <*(F . (d,d19))*>
proofend;

theorem :: FINSEQ_2:81
for D, D9, E being non empty set
for d being Element of D
for d19, d29 being Element of D9
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))*>
proofend;

theorem :: FINSEQ_2:82
for D, D9, E being non empty set
for d being Element of D
for d19, d29, d39 being Element of D9
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))*>
proofend;

theorem Th83: :: FINSEQ_2:83
for D, D9, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E
proofend;

theorem Th84: :: FINSEQ_2:84
for D, D9, E being non empty set
for d9 being Element of D9
for r being FinSequence
for F being Function of [:D,D9:],E
for p being FinSequence of D st r = F [:] (p,d9) holds
len r = len p
proofend;

theorem :: FINSEQ_2:85
for D, D9, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E holds F [:] ((<*> D),d9) = <*> E
proofend;

theorem :: FINSEQ_2:86
for D, D9, E being non empty set
for d1 being Element of D
for d9 being Element of D9
for F being Function of [:D,D9:],E
for p being FinSequence of D st p = <*d1*> holds
F [:] (p,d9) = <*(F . (d1,d9))*>
proofend;

theorem :: FINSEQ_2:87
for D, D9, E being non empty set
for d1, d2 being Element of D
for d9 being Element of D9
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))*>
proofend;

theorem :: FINSEQ_2:88
for D, D9, E being non empty set
for d1, d2, d3 being Element of D
for d9 being Element of D9
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))*>
proofend;

:: Tuples
definition
let D be set ;
mode FinSequenceSet of D ->  set  means :Def3: :: FINSEQ_2:def 3
 for a being set st a in it holds
a is FinSequence of D;
existence
 ex b1 being set st
for a being set st a in b1 holds
a is FinSequence of D
proofend;
end;

:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def_3_:_
 for D, b2 being set holds
( b2 is FinSequenceSet of D iff for a being set st a in b2 holds
a is FinSequence of D );

definition
let D be set ;
let S be FinSequenceSet of D;
:: original:Element
redefine mode Element of S ->  FinSequence of D;
coherence
 for b1 being Element of S holds b1 is FinSequence of D
proofend;
end;

registration
let D be set ;
cluster non empty for FinSequenceSet of D;
existence
 not for b1 being FinSequenceSet of D holds b1 is empty
proofend;
end;

theorem Th89: :: FINSEQ_2:89
for D being set holds D * is FinSequenceSet of D
proofend;

definition
let D be set ;
:: original:*
redefine funcD *  ->  FinSequenceSet of D;
coherence
 D * is FinSequenceSet of D by Th89;
end;

theorem :: FINSEQ_2:90
for D being set
for D9 being FinSequenceSet of D holds D9 c= D *
proofend;

theorem :: FINSEQ_2:91
for D being non empty set
for D9 being Subset of D
for S being FinSequenceSet of D9 holds S is FinSequenceSet of D
proofend;

registration
let i be Nat;
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like V46() i -element FinSequence-like FinSubsequence-like countable for FinSequence of D;
existence
 ex b1 being FinSequence of D st b1 is i -element
proofend;
end;

definition
let i be Nat;
let D be non empty set ;
mode Tuple of i,D is i -element FinSequence of D;
end;

definition
let i be Nat;
let D be set ;
funci -tuples_on D ->  FinSequenceSet of D equals :: FINSEQ_2:def 4
 {  s where s is Element of D * : len s = i  }  ;
coherence
  {  s where s is Element of D * : len s = i  }  is FinSequenceSet of D
proofend;
end;

:: deftheorem  defines -tuples_on FINSEQ_2:def_4_:_
 for i being Nat
for D being set holds i -tuples_on D =  {  s where s is Element of D * : len s = i  }  ;

registration
let i be Nat;
let D be non empty set ;
clusteri -tuples_on D ->  non empty ;
coherence
 not i -tuples_on D is empty
proofend;
end;

registration
let D be non empty set ;
let i be Nat;
cluster  -> i -element for Element of i -tuples_on D;
coherence
 for b1 being Element of i -tuples_on D holds b1 is i -element
proofend;
end;

theorem Th92: :: FINSEQ_2:92
for D being set
for z being FinSequence of D holds z is Element of (len z) -tuples_on D
proofend;

theorem :: FINSEQ_2:93
for i being Nat
for D being set holds i -tuples_on D = Funcs ((Seg i),D)
proofend;

theorem :: FINSEQ_2:94
for D being set holds 0 -tuples_on D = {(<*> D)}
proofend;

theorem :: FINSEQ_2:95
for i being Nat
for D being non empty set
for z being Tuple of 0 ,D
for t being Tuple of i,D holds
( z ^ t = t &amp; t ^ z = t ) by FINSEQ_1:34;

theorem Th96: :: FINSEQ_2:96
for D being non empty set holds 1 -tuples_on D =  {  <*d*> where d is Element of D : verum  }
proofend;

Lm6:  for i being Nat
for D being non empty set
for z being Tuple of i,D holds z in i -tuples_on D
proofend;

theorem Th97: :: FINSEQ_2:97
for D being non empty set
for z being Tuple of 1,D ex d being Element of D st z = <*d*>
proofend;

theorem Th98: :: FINSEQ_2:98
for D being non empty set
for d being Element of D holds <*d*> in 1 -tuples_on D
proofend;

theorem Th99: :: FINSEQ_2:99
for D being non empty set holds 2 -tuples_on D =  {  <*d1,d2*> where d1, d2 is Element of D : verum  }
proofend;

theorem :: FINSEQ_2:100
for D being non empty set
for z being Tuple of 2,D ex d1, d2 being Element of D st z = <*d1,d2*>
proofend;

theorem Th101: :: FINSEQ_2:101
for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> in 2 -tuples_on D
proofend;

theorem Th102: :: FINSEQ_2:102
for D being non empty set holds 3 -tuples_on D =  {  <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum  }
proofend;

theorem :: FINSEQ_2:103
for D being non empty set
for z being Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
proofend;

theorem Th104: :: FINSEQ_2:104
for D being non empty set
for d1, d2, d3 being Element of D holds <*d1,d2,d3*> in 3 -tuples_on D
proofend;

theorem Th105: :: FINSEQ_2:105
for i, j being Nat
for D being non empty set holds (i + j) -tuples_on D =  {  (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum  }
proofend;

theorem Th106: :: FINSEQ_2:106
for i, j being Nat
for D being non empty set
for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
proofend;

theorem :: FINSEQ_2:107
for i, j being Nat
for D being non empty set
for z being Tuple of i,D
for t being Tuple of j,D holds z ^ t is Tuple of i + j,D
proofend;

theorem :: FINSEQ_2:108
for D being non empty set holds D * = union  {  (i -tuples_on D) where i is Element of NAT : verum  }
proofend;

theorem :: FINSEQ_2:109
for i being Nat
for D being non empty set
for D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D
proofend;

Lm7:  for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b1 -element FinSequence
proofend;

theorem :: FINSEQ_2:110
for i, j being Nat
for A being set
for D being non empty set st i -tuples_on D = j -tuples_on A holds
i = j
proofend;

theorem :: FINSEQ_2:111
for i being Nat holds idseq i is Element of i -tuples_on NAT
proofend;

theorem Th112: :: FINSEQ_2:112
for i being Nat
for D being non empty set
for d being Element of D holds i |-> d is Element of i -tuples_on D
proofend;

theorem :: FINSEQ_2:113
for i being Nat
for D, D9 being non empty set
for z being Tuple of i,D
for f being Function of D,D9 holds f * z is Element of i -tuples_on D9
proofend;

theorem Th114: :: FINSEQ_2:114
for i being Nat
for D being non empty set
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
proofend;

theorem :: FINSEQ_2:115
for i being Nat
for D being non empty set
for z being Tuple of i,D
for f being Permutation of (Seg i) holds z * f is Tuple of i,D
proofend;

theorem :: FINSEQ_2:116
for i being Nat
for D being non empty set
for z being Tuple of i,D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
proofend;

theorem :: FINSEQ_2:117
for i being Nat
for D being non empty set
for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
proofend;

theorem :: FINSEQ_2:118
for i being Nat
for D being non empty set
for z being Tuple of i,D holds z * (idseq i) = z
proofend;

theorem :: FINSEQ_2:119
for i being Nat
for D being non empty set
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
proofend;

theorem :: FINSEQ_2:120
for i being Nat
for D, D9, E being non empty set
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
proofend;

theorem :: FINSEQ_2:121
for i being Nat
for D, D9, E being non empty set
for d being Element of D
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
proofend;

theorem :: FINSEQ_2:122
for i being Nat
for D, D9, E being non empty set
for d9 being Element of D9
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
proofend;

theorem :: FINSEQ_2:123
for i, j being Nat
for x being set holds (i + j) |-> x = (i |-> x) ^ (j |-> x)
proofend;

:: Addendum, 2002.07.08
theorem :: FINSEQ_2:124
for i being Nat
for D being non empty set
for x being Tuple of i,D holds dom x = Seg i
proofend;

theorem :: FINSEQ_2:125
for f being Function
for x, y being set st x in dom f &amp; y in dom f holds
f * <*x,y*> = <*(f . x),(f . y)*>
proofend;

theorem :: FINSEQ_2:126
for f being Function
for x, y, z being set st x in dom f &amp; y in dom f &amp; z in dom f holds
f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>
proofend;

theorem :: FINSEQ_2:127
for x1, x2 being set holds rng <*x1,x2*> = {x1,x2} by Lm1;

theorem :: FINSEQ_2:128
for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3} by Lm2;

begin

:: from SCMFSA_7, 2005.11.21, A.T.
theorem :: FINSEQ_2:129
for p1, p2, q being FinSequence st p1 c= q &amp; p2 c= q &amp; len p1 = len p2 holds
p1 = p2
proofend;

theorem :: FINSEQ_2:130
for D being non empty set
for s being FinSequence of D st s <> {} holds
ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w
proofend;

:: Moved from AMISTD_2 by AK, 2008.02.02
registration
let D be set ;
cluster  ->  functional for FinSequenceSet of D;
coherence
 for b1 being FinSequenceSet of D holds b1 is functional
proofend;
end;

:: from FINSOP_1, 2009.05.23, AT
definition
let D be non empty set ;
let n be Nat;
let d be Element of D;
:: original:|->
redefine funcn |-> d ->  Element of n -tuples_on D;
coherence
 n |-> d is Element of n -tuples_on D by Th112;
end;

:: new, 2009.08.15, A.T.
theorem :: FINSEQ_2:131
for i being Nat
for D being non empty set
for z being set holds
( z is Tuple of i,D iff z in i -tuples_on D )
proofend;

:: from CATALG_1, 2009.09.08, A.T.
theorem Th132: :: FINSEQ_2:132
for A being set
for i being Element of NAT
for p being FinSequence holds
( p in i -tuples_on A iff ( len p = i &amp; rng p c= A ) )
proofend;

theorem :: FINSEQ_2:133
for A being set
for i being Element of NAT
for p being FinSequence of A holds
( p in i -tuples_on A iff len p = i )
proofend;

theorem :: FINSEQ_2:134
for A being set
for i being Element of NAT holds i -tuples_on A c= A *
proofend;

theorem Th135: :: FINSEQ_2:135
for A, x being set holds
( x in 1 -tuples_on A iff ex a being set st
( a in A &amp; x = <*a*> ) )
proofend;

theorem :: FINSEQ_2:136
for A, a being set st <*a*> in 1 -tuples_on A holds
a in A
proofend;

theorem Th137: :: FINSEQ_2:137
for A, x being set holds
( x in 2 -tuples_on A iff ex a, b being set st
( a in A &amp; b in A &amp; x = <*a,b*> ) )
proofend;

theorem :: FINSEQ_2:138
for A, a, b being set st <*a,b*> in 2 -tuples_on A holds
( a in A &amp; b in A )
proofend;

theorem Th139: :: FINSEQ_2:139
for A, x being set holds
( x in 3 -tuples_on A iff ex a, b, c being set st
( a in A &amp; b in A &amp; c in A &amp; x = <*a,b,c*> ) )
proofend;

theorem :: FINSEQ_2:140
for A, a, b, c being set st <*a,b,c*> in 3 -tuples_on A holds
( a in A &amp; b in A &amp; c in A )
proofend;

theorem :: FINSEQ_2:141
for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b1 -element FinSequence by Lm7;

:: from MSUALG_1, 2009.09.18, A.T.
theorem :: FINSEQ_2:142
for A being non empty set
for n being Nat holds n -tuples_on A c= A *
proofend;

:: from AMISTD_3, 2010.01.10, A.T.
theorem :: FINSEQ_2:143
for x being set
for n, m being Nat st n |-> x = m |-> x holds
n = m
proofend;

definition
let I be set ;
let M be ManySortedSet of I;
funcM #  ->  ManySortedSet of I *  means :Def5: :: FINSEQ_2:def 5
 for i being Element of I * holds it . i = product (M * i);
existence
 ex b1 being ManySortedSet of I * st
for i being Element of I * holds b1 . i = product (M * i)
proofend;
uniqueness
 for b1, b2 being ManySortedSet of I * st ( for i being Element of I * holds b1 . i = product (M * i) ) &amp; ( for i being Element of I * holds b2 . i = product (M * i) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines # FINSEQ_2:def_5_:_
 for I being set
for M being ManySortedSet of I
for b3 being ManySortedSet of I * holds
( b3 = M # iff for i being Element of I * holds b3 . i = product (M * i) );

registration
let I be set ;
let M be V2() ManySortedSet of I;
clusterM #  -> V2() ;
coherence
 M # is non-empty
proofend;
end;

definition
let a be set ;
func *--> a ->  Function of NAT,({a} *) means :Def6: :: FINSEQ_2:def 6
 for n being Element of NAT holds it . n = n |-> a;
existence
 ex b1 being Function of NAT,({a} *) st
for n being Element of NAT holds b1 . n = n |-> a
proofend;
uniqueness
 for b1, b2 being Function of NAT,({a} *) st ( for n being Element of NAT holds b1 . n = n |-> a ) &amp; ( for n being Element of NAT holds b2 . n = n |-> a ) holds
b1 = b2
proofend;
end;

:: deftheorem Def6 defines *--> FINSEQ_2:def_6_:_
 for a being set
for b2 being Function of NAT,({a} *) holds
( b2 = *--> a iff for n being Element of NAT holds b2 . n = n |-> a );

theorem Th144: :: FINSEQ_2:144
for n being Element of NAT
for a, b being set holds (a .--> b) * (n |-> a) = n |-> b
proofend;

theorem :: FINSEQ_2:145
for D being non empty set
for n being Element of NAT
for a being set
for M being ManySortedSet of {a} st M = a .--> D holds
((M #) * (*--> a)) . n = Funcs ((Seg n),D)
proofend;

theorem :: FINSEQ_2:146
for F being NAT -defined total Function
for p being NAT -defined Function
for n being Element of NAT st Shift (p,n) c= F holds
for i being Element of NAT st i in dom p holds
F . (n + i) = p . i
proofend;

registration
let i be Nat;
clusteri |-> 0 ->  empty-yielding ;
coherence
 i |-> 0 is empty-yielding
proofend;
end;

:: new, 2011.10.03, A.K.
registration
let D be set ;
cluster  ->  FinSequence-membered for FinSequenceSet of D;
coherence
 for b1 being FinSequenceSet of D holds b1 is FinSequence-membered
proofend;
end;