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


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 13;

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

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

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

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

theorem :: FINSEQ_2:6
for i being Nat holds
( min 0 ,i = 0 & min i,0 = 0 & max 0 ,i = i & max i,0 = i ) by XXREAL_0:def 10, XXREAL_0:def 9;

theorem :: FINSEQ_2:7
canceled;

theorem :: FINSEQ_2:8
for i, l being Nat holds
( not i in Seg (l + 1) or i in Seg l or i = l + 1 )
proof end;

theorem :: FINSEQ_2:9
for i, l, j being Nat st i in Seg l holds
i in Seg (l + j)
proof end;

theorem :: FINSEQ_2:10
for p, q being FinSequence st len p = len q & ( for j being Nat st j in dom p holds
p . j = q . j ) holds
p = q
proof end;

theorem Th11: :: FINSEQ_2:11
for b being set
for p being FinSequence st b in rng p holds
ex i being Nat st
( i in dom p & p . i = b )
proof end;

theorem :: FINSEQ_2:12
canceled;

theorem Th13: :: FINSEQ_2:13
for i being Nat
for D being set
for p being FinSequence of D st i in dom p holds
p . i in D
proof end;

theorem Th14: :: FINSEQ_2:14
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
proof end;

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

theorem Th15: :: FINSEQ_2:15
for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> is FinSequence of D
proof end;

Lm3: for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3}
proof end;

theorem Th16: :: FINSEQ_2:16
for D being non empty set
for d1, d2, d3 being Element of D holds <*d1,d2,d3*> is FinSequence of D
proof end;

theorem :: FINSEQ_2:17
canceled;

theorem Th18: :: FINSEQ_2:18
for i being Nat
for p, q being FinSequence st i in dom p holds
i in dom (p ^ q)
proof end;

theorem Th19: :: FINSEQ_2:19
for a being set
for p being FinSequence holds len (p ^ <*a*>) = (len p) + 1
proof end;

theorem :: FINSEQ_2:20
for a, b being set
for p, q being FinSequence st p ^ <*a*> = q ^ <*b*> holds
( p = q & a = b )
proof end;

theorem :: FINSEQ_2:21
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 FINSEQ_1:63, CARD_1:47;

theorem Th22: :: FINSEQ_2:22
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*>
proof end;

theorem Th23: :: FINSEQ_2:23
for i being Nat
for q, p being FinSequence st q = p | (Seg i) & len p <= i holds
p = q
proof end;

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

theorem Th25: :: FINSEQ_2:25
for i, j being Nat
for r being FinSequence st len r = i + j holds
ex p, q being FinSequence st
( len p = i & len q = j & r = p ^ q )
proof end;

theorem Th26: :: FINSEQ_2:26
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 & len q = j & r = p ^ q )
proof end;

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() & ( for j being Nat st j in dom z holds
z . j = F3(j) ) )
proof end;

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*>]
proof end;

theorem Th27: :: FINSEQ_2:27
for D being non empty set
for D' being non empty Subset of D
for p being FinSequence of D' holds p is FinSequence of D
proof end;

theorem Th28: :: FINSEQ_2:28
for i being Nat
for D being non empty set
for f being Function of Seg i,D holds f is FinSequence of D
proof end;

theorem :: FINSEQ_2:29
canceled;

theorem :: FINSEQ_2:30
for D being non empty set
for p being FinSequence of D holds p is Function of dom p,D
proof end;

theorem :: FINSEQ_2:31
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
proof end;

theorem :: FINSEQ_2:32
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
proof end;

theorem Th33: :: FINSEQ_2:33
for p, q being FinSequence
for f being Function st rng p c= dom f & q = f * p holds
len q = len p
proof end;

theorem Th34: :: FINSEQ_2:34
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
proof end;

theorem :: FINSEQ_2:35
for i being Nat
for D, D' being non empty set st D = Seg i holds
for p being FinSequence of D'
for q being FinSequence of D st i <= len p holds
p * q is FinSequence of D'
proof end;

theorem Th36: :: FINSEQ_2:36
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
proof end;

theorem Th37: :: FINSEQ_2:37
for A being set
for D' being non empty set
for q being FinSequence
for p being FinSequence of A
for f being Function of A,D' st q = f * p holds
len q = len p
proof end;

theorem :: FINSEQ_2:38
for A being set
for D' being non empty set
for f being Function of A,D' holds f * (<*> A) = <*> D' ;

theorem :: FINSEQ_2:39
for x1 being set
for D, D' being non empty set
for p being FinSequence of D
for f being Function of D,D' st p = <*x1*> holds
f * p = <*(f . x1)*>
proof end;

theorem Th40: :: FINSEQ_2:40
for x1, x2 being set
for D, D' being non empty set
for p being FinSequence of D
for f being Function of D,D' st p = <*x1,x2*> holds
f * p = <*(f . x1),(f . x2)*>
proof end;

theorem Th41: :: FINSEQ_2:41
for x1, x2, x3 being set
for D, D' being non empty set
for p being FinSequence of D
for f being Function of D,D' st p = <*x1,x2,x3*> holds
f * p = <*(f . x1),(f . x2),(f . x3)*>
proof end;

theorem Th42: :: FINSEQ_2:42
for i, j being Nat
for p being FinSequence
for f being Function of Seg i, Seg j st ( j = 0 implies i = 0 ) & j <= len p holds
p * f is FinSequence
proof end;

theorem :: FINSEQ_2:43
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 Th42;

theorem :: FINSEQ_2:44
for p being FinSequence
for f being Function of dom p, dom p holds p * f is FinSequence
proof end;

theorem Th45: :: FINSEQ_2:45
for i being Nat
for p, q being FinSequence
for f being Function of Seg i, Seg i st rng f = Seg i & i <= len p & q = p * f holds
len q = i
proof end;

theorem Th46: :: FINSEQ_2:46
for p, q being FinSequence
for f being Function of dom p, dom p st rng f = dom p & q = p * f holds
len q = len p
proof end;

theorem Th47: :: FINSEQ_2:47
for i being Nat
for p, q being FinSequence
for f being Permutation of Seg i st i <= len p & q = p * f holds
len q = i
proof end;

theorem :: FINSEQ_2:48
for p, q being FinSequence
for f being Permutation of dom p st q = p * f holds
len q = len p
proof end;

theorem Th49: :: FINSEQ_2:49
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 ) & j <= len p holds
p * f is FinSequence of D
proof end;

theorem :: FINSEQ_2:50
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 Th49;

theorem Th51: :: FINSEQ_2:51
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
proof end;

theorem Th52: :: FINSEQ_2:52
for k being Nat holds id (Seg k) is FinSequence of NAT
proof end;

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

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

theorem :: FINSEQ_2:53
canceled;

theorem :: FINSEQ_2:54
canceled;

theorem Th55: :: FINSEQ_2:55
for k being Nat holds len (idseq k) = k
proof end;

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

theorem :: FINSEQ_2:56
canceled;

theorem :: FINSEQ_2:57
for i being Nat
for k being Element of Seg i holds (idseq i) . k = k
proof end;

theorem :: FINSEQ_2:58
idseq 0 = {} ;

theorem Th59: :: FINSEQ_2:59
idseq 1 = <*1*>
proof end;

theorem Th60: :: FINSEQ_2:60
for i being Nat holds idseq (i + 1) = (idseq i) ^ <*(i + 1)*>
proof end;

theorem Th61: :: FINSEQ_2:61
idseq 2 = <*1,2*>
proof end;

theorem :: FINSEQ_2:62
idseq 3 = <*1,2,3*>
proof end;

theorem :: FINSEQ_2:63
canceled;

theorem Th64: :: FINSEQ_2:64
for k being Nat
for p being FinSequence st len p <= k holds
p * (idseq k) = p
proof end;

theorem :: FINSEQ_2:65
for k being Nat holds idseq k is Permutation of Seg k ;

theorem Th66: :: FINSEQ_2:66
for k being Nat
for a being set holds (Seg k) --> a is FinSequence
proof end;

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

definition
let i be Nat;
let a be set ;
func i |-> 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;

theorem :: FINSEQ_2:67
canceled;

theorem :: FINSEQ_2:68
canceled;

theorem Th69: :: FINSEQ_2:69
for k being Nat
for a being set holds len (k |-> a) = k
proof end;

theorem :: FINSEQ_2:70
canceled;

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

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

theorem Th73: :: FINSEQ_2:73
for a being set holds 1 |-> a = <*a*>
proof end;

theorem Th74: :: FINSEQ_2:74
for i being Nat
for a being set holds (i + 1) |-> a = (i |-> a) ^ <*a*>
proof end;

theorem Th75: :: FINSEQ_2:75
for a being set holds 2 |-> a = <*a,a*>
proof end;

theorem :: FINSEQ_2:76
for a being set holds 3 |-> a = <*a,a,a*>
proof end;

theorem Th77: :: FINSEQ_2:77
for k being Nat
for D being non empty set
for d being Element of D holds k |-> d is FinSequence of D
proof end;

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

theorem Th78: :: FINSEQ_2:78
for p, q being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F holds
F .: p,q is FinSequence
proof end;

theorem Th79: :: FINSEQ_2:79
for p, q, r being FinSequence
for F being Function st [:(rng p),(rng q):] c= dom F & r = F .: p,q holds
len r = min (len p),(len q)
proof end;

Lm5: 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
proof end;

theorem Th80: :: FINSEQ_2:80
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
proof end;

theorem Th81: :: FINSEQ_2:81
for a being set
for p, r being FinSequence
for F being Function st [:{a},(rng p):] c= dom F & r = F [;] a,p holds
len r = len p
proof end;

Lm6: 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
proof end;

theorem Th82: :: FINSEQ_2:82
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
proof end;

theorem Th83: :: FINSEQ_2:83
for a being set
for p, r being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] p,a holds
len r = len p
proof end;

theorem Th84: :: FINSEQ_2:84
for D, D', E being non empty set
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' holds F .: p,q is FinSequence of E
proof end;

theorem Th85: :: FINSEQ_2:85
for D, D', E being non empty set
for r being FinSequence
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st r = F .: p,q holds
len r = min (len p),(len q)
proof end;

theorem Th86: :: FINSEQ_2:86
for D, D', E being non empty set
for r being FinSequence
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st len p = len q & r = F .: p,q holds
( len r = len p & len r = len q )
proof end;

theorem :: FINSEQ_2:87
for D, D', E being non empty set
for F being Function of [:D,D':],E
for p being FinSequence of D
for p' being FinSequence of D' holds
( F .: (<*> D),p' = <*> E & F .: p,(<*> D') = <*> E )
proof end;

theorem :: FINSEQ_2:88
for D, D', E being non empty set
for d1 being Element of D
for d1' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st p = <*d1*> & q = <*d1'*> holds
F .: p,q = <*(F . d1,d1')*>
proof end;

theorem :: FINSEQ_2:89
for D, D', E being non empty set
for d1, d2 being Element of D
for d1', d2' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st p = <*d1,d2*> & q = <*d1',d2'*> holds
F .: p,q = <*(F . d1,d1'),(F . d2,d2')*>
proof end;

theorem :: FINSEQ_2:90
for D, D', E being non empty set
for d1, d2, d3 being Element of D
for d1', d2', d3' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D
for q being FinSequence of D' st p = <*d1,d2,d3*> & q = <*d1',d2',d3'*> holds
F .: p,q = <*(F . d1,d1'),(F . d2,d2'),(F . d3,d3')*>
proof end;

theorem Th91: :: FINSEQ_2:91
for D, D', E being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for p being FinSequence of D' holds F [;] d,p is FinSequence of E
proof end;

theorem Th92: :: FINSEQ_2:92
for D, D', E being non empty set
for d being Element of D
for r being FinSequence
for F being Function of [:D,D':],E
for p being FinSequence of D' st r = F [;] d,p holds
len r = len p
proof end;

theorem :: FINSEQ_2:93
for D, D', E being non empty set
for d being Element of D
for F being Function of [:D,D':],E holds F [;] d,(<*> D') = <*> E
proof end;

theorem :: FINSEQ_2:94
for D, D', E being non empty set
for d being Element of D
for d1' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D' st p = <*d1'*> holds
F [;] d,p = <*(F . d,d1')*>
proof end;

theorem :: FINSEQ_2:95
for D, D', E being non empty set
for d being Element of D
for d1', d2' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D' st p = <*d1',d2'*> holds
F [;] d,p = <*(F . d,d1'),(F . d,d2')*>
proof end;

theorem :: FINSEQ_2:96
for D, D', E being non empty set
for d being Element of D
for d1', d2', d3' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D' st p = <*d1',d2',d3'*> holds
F [;] d,p = <*(F . d,d1'),(F . d,d2'),(F . d,d3')*>
proof end;

theorem Th97: :: FINSEQ_2:97
for D, D', E being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D holds F [:] p,d' is FinSequence of E
proof end;

theorem Th98: :: FINSEQ_2:98
for D, D', E being non empty set
for d' being Element of D'
for r being FinSequence
for F being Function of [:D,D':],E
for p being FinSequence of D st r = F [:] p,d' holds
len r = len p
proof end;

theorem :: FINSEQ_2:99
for D, D', E being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E holds F [:] (<*> D),d' = <*> E
proof end;

theorem :: FINSEQ_2:100
for D, D', E being non empty set
for d1 being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D st p = <*d1*> holds
F [:] p,d' = <*(F . d1,d')*>
proof end;

theorem :: FINSEQ_2:101
for D, D', E being non empty set
for d1, d2 being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D st p = <*d1,d2*> holds
F [:] p,d' = <*(F . d1,d'),(F . d2,d')*>
proof end;

theorem :: FINSEQ_2:102
for D, D', E being non empty set
for d1, d2, d3 being Element of D
for d' being Element of D'
for F being Function of [:D,D':],E
for p being FinSequence of D st p = <*d1,d2,d3*> holds
F [:] p,d' = <*(F . d1,d'),(F . d2,d'),(F . d3,d')*>
proof end;

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
proof end;
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 );

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

definition
let D be set ;
mode FinSequence-DOMAIN of D is non empty FinSequenceSet of D;
end;

theorem :: FINSEQ_2:103
canceled;

theorem Th104: :: FINSEQ_2:104
for D being set holds D * is FinSequence-DOMAIN of D
proof end;

definition
let D be set ;
:: original: *
redefine func D * -> FinSequence-DOMAIN of D;
coherence
D * is FinSequence-DOMAIN of D by Th104;
end;

theorem :: FINSEQ_2:105
for D being set
for D' being FinSequence-DOMAIN of D holds D' c= D *
proof end;

definition
let D be set ;
let S be FinSequence-DOMAIN 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 by Def3;
end;

theorem :: FINSEQ_2:106
canceled;

theorem :: FINSEQ_2:107
for D being non empty set
for D' being non empty Subset of D
for S being FinSequence-DOMAIN of D' holds S is FinSequence-DOMAIN of D
proof end;

definition
let i be Nat;
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 } ;
coherence
{ s where s is Element of D * : len s = i } is FinSequenceSet of D
proof end;
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 ;
cluster i -tuples_on D -> non empty ;
coherence
not i -tuples_on D is empty
proof end;
end;

theorem :: FINSEQ_2:108
canceled;

theorem Th109: :: FINSEQ_2:109
for D being non empty set
for i being Nat
for z being Element of i -tuples_on D holds len z = i
proof end;

theorem Th110: :: FINSEQ_2:110
for D being set
for z being FinSequence of D holds z is Element of (len z) -tuples_on D
proof end;

theorem :: FINSEQ_2:111
for i being Nat
for D being non empty set holds i -tuples_on D = Funcs (Seg i),D
proof end;

theorem Th112: :: FINSEQ_2:112
for D being set holds 0 -tuples_on D = {(<*> D)}
proof end;

theorem Th113: :: FINSEQ_2:113
for D being set
for z being Element of 0 -tuples_on D holds z = <*> D
proof end;

theorem :: FINSEQ_2:114
for D being set holds <*> D is Element of 0 -tuples_on D
proof end;

theorem :: FINSEQ_2:115
for i being Nat
for D being non empty set
for z being Element of 0 -tuples_on D
for t being Element of i -tuples_on D holds
( z ^ t = t & t ^ z = t )
proof end;

theorem Th116: :: FINSEQ_2:116
for D being non empty set holds 1 -tuples_on D = { <*d*> where d is Element of D : verum }
proof end;

theorem Th117: :: FINSEQ_2:117
for D being non empty set
for z being Element of 1 -tuples_on D ex d being Element of D st z = <*d*>
proof end;

theorem :: FINSEQ_2:118
for D being non empty set
for d being Element of D holds <*d*> in 1 -tuples_on D
proof end;

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

theorem :: FINSEQ_2:120
for D being non empty set
for z being Element of 2 -tuples_on D ex d1, d2 being Element of D st z = <*d1,d2*>
proof end;

theorem :: FINSEQ_2:121
for D being non empty set
for d1, d2 being Element of D holds <*d1,d2*> in 2 -tuples_on D
proof end;

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

theorem :: FINSEQ_2:123
for D being non empty set
for z being Element of 3 -tuples_on D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>
proof end;

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

theorem Th125: :: FINSEQ_2:125
for i, j being Nat
for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Element of i -tuples_on D, t is Element of j -tuples_on D : verum }
proof end;

theorem Th126: :: FINSEQ_2:126
for i, j being Nat
for D being non empty set
for s being Element of (i + j) -tuples_on D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t
proof end;

theorem :: FINSEQ_2:127
for i, j being Nat
for D being non empty set
for z being Element of i -tuples_on D
for t being Element of j -tuples_on D holds z ^ t is Element of (i + j) -tuples_on D
proof end;

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

theorem :: FINSEQ_2:129
for i being Nat
for D being non empty set
for D' being non empty Subset of D
for z being Element of i -tuples_on D' holds z is Element of i -tuples_on D
proof end;

theorem :: FINSEQ_2:130
for i, j being Nat
for D being non empty set st i -tuples_on D = j -tuples_on D holds
i = j
proof end;

theorem :: FINSEQ_2:131
for i being Nat holds idseq i is Element of i -tuples_on NAT
proof end;

theorem :: FINSEQ_2:132
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
proof end;

theorem :: FINSEQ_2:133
for i being Nat
for D, D' being non empty set
for z being Element of i -tuples_on D
for f being Function of D,D' holds f * z is Element of i -tuples_on D'
proof end;

theorem Th134: :: FINSEQ_2:134
for i being Nat
for D being non empty set
for z being Element of i -tuples_on 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
proof end;

theorem :: FINSEQ_2:135
for i being Nat
for D being non empty set
for z being Element of i -tuples_on D
for f being Permutation of Seg i holds z * f is Element of i -tuples_on D
proof end;

theorem :: FINSEQ_2:136
for i being Nat
for D being non empty set
for z being Element of i -tuples_on D
for d being Element of D holds (z ^ <*d*>) . (i + 1) = d
proof end;

theorem :: FINSEQ_2:137
for i being Nat
for D being non empty set
for z being Element of (i + 1) -tuples_on D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>
proof end;

theorem :: FINSEQ_2:138
for i being Nat
for D being non empty set
for z being Element of i -tuples_on D holds z * (idseq i) = z
proof end;

theorem :: FINSEQ_2:139
for i being Nat
for D being non empty set
for z1, z2 being Element of i -tuples_on D st ( for j being Nat st j in Seg i holds
z1 . j = z2 . j ) holds
z1 = z2
proof end;

theorem :: FINSEQ_2:140
for i being Nat
for D, D', E being non empty set
for F being Function of [:D,D':],E
for z1 being Element of i -tuples_on D
for z2 being Element of i -tuples_on D' holds F .: z1,z2 is Element of i -tuples_on E
proof end;

theorem :: FINSEQ_2:141
for i being Nat
for D, D', E being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for z being Element of i -tuples_on D' holds F [;] d,z is Element of i -tuples_on E
proof end;

theorem :: FINSEQ_2:142
for i being Nat
for D, D', E being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for z being Element of i -tuples_on D holds F [:] z,d' is Element of i -tuples_on E
proof end;

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

theorem :: FINSEQ_2:144
for i being Nat
for D being non empty set
for x being Element of i -tuples_on D holds dom x = Seg i
proof end;

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

theorem :: FINSEQ_2:146
for f being Function
for 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)*>
proof end;

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

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

theorem :: FINSEQ_2:149
for p1, p2, q being FinSequence st p1 c= q & p2 c= q & len p1 = len p2 holds
p1 = p2
proof end;

theorem :: FINSEQ_2:150
for s being FinSequence of NAT st s <> {} holds
ex w being FinSequence of NAT ex n being Nat st s = <*n*> ^ w
proof end;

registration
let D be set ;
cluster -> functional FinSequenceSet of D;
coherence
for b1 being FinSequenceSet of D holds b1 is functional
proof end;
end;