let k be natural number ; :: thesis:
assume A1: k <> 0 ; :: thesis:
let w be Element of Seg k; :: thesis:
reconsider z = k as Nat by ORDINAL2:def 21;
Seg z is non empty Subset of NAT by A1, FINSEQ_1:5;
hence w in Seg k ; :: thesis:

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 Th21: :: 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*>

proof end;

theorem Th22: :: FINSEQ_2:22

for D being non empty set
for p being FinSequence of D st len p <> 0 holds
ex q being FinSequence of D ex d being Element of D 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{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

ex z being FinSequence of F₂() st
( len z = F₁() & ( for j being Nat st j in Seg F₁() holds
z . j = F₃(j) ) )

proof end;

scheme :: FINSEQ_2:sch 2
IndSeqD{ F₁() -> non empty set , P₁[ set ] } :

for p being FinSequence of F₁() holds P₁[p]

provided

A1: P₁[ <*> F₁()] and
A2: for p being FinSequence of F₁()
for x being Element of F₁() st P₁[p] holds
P₁[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'

proof end;

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 Th43: :: 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

proof end;

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 Th50: :: 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

proof end;

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 natural number holds id (Seg k) is FinSequence of NAT

proof end;

definition

let i be natural number ;
func idseq i -> FinSequence equals :: FINSEQ_2:def 1
id (Seg i);
coherence by Th52;

end;

:: deftheorem defines idseq FINSEQ_2:def 1 :

theorem :: FINSEQ_2:53

canceled;

theorem Th54: :: FINSEQ_2:54

for k being natural number holds dom (idseq k) = Seg k by RELAT_1:71;

theorem Th55: :: FINSEQ_2:55

for k being natural number holds len (idseq k) = k

proof end;

theorem Th56: :: FINSEQ_2:56

for j, i being Nat st j in Seg i holds
(idseq i) . j = j by FUNCT_1:35;

theorem :: FINSEQ_2:57

for i being Nat st i <> 0 holds
for k being Element of Seg i holds (idseq i) . k = k

proof end;

theorem :: FINSEQ_2:58

idseq 0 = {}

proof end;

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

for k being natural number
for p being FinSequence holds p * (idseq k) = p | (Seg k) by RELAT_1:94;

theorem Th64: :: FINSEQ_2:64

for k being natural number
for p being FinSequence st len p <= k holds
p * (idseq k) = p

proof end;

theorem :: FINSEQ_2:65

for k being natural number holds idseq k is Permutation of Seg k ;

theorem Th66: :: FINSEQ_2:66

for k being natural number
for a being set holds (Seg k) --> a is FinSequence

proof end;

definition

let i be natural number ;
let a be set ;
func i |-> a -> FinSequence equals :: FINSEQ_2:def 2
(Seg i) --> a;
coherence by Th66;

end;

:: deftheorem defines |-> FINSEQ_2:def 2 :

theorem :: FINSEQ_2:67

canceled;

theorem Th68: :: FINSEQ_2:68

for k being natural number
for a being set holds dom (k |-> a) = Seg k by FUNCOP_1:19;

theorem Th69: :: FINSEQ_2:69

for k being natural number
for a being set holds len (k |-> a) = k

proof end;

theorem Th70: :: FINSEQ_2:70

for k being natural number
for b, a being set st b in Seg k holds
(k |-> a) . b = a by FUNCOP_1:13;

theorem :: FINSEQ_2:71

for k being natural number
for D being non empty set
for d being Element of D st k <> 0 holds
for w being Element of Seg k holds (k |-> d) . w = d

proof end;

theorem Th72: :: FINSEQ_2:72

for a being set holds 0 |-> a = {}

proof end;

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 natural number
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

proof end;

end;

:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def 3 :

registration

let D be set ;
cluster non empty FinSequenceSet of D;
existence

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 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 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 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 } ;
coherence

proof end;

end;

:: deftheorem defines -tuples_on FINSEQ_2:def 4 :

registration

let i be natural number ;
let D be non empty set ;
cluster i -tuples_on D -> non empty ;
coherence

proof end;

end;

theorem :: FINSEQ_2:108

canceled;

theorem Th109: :: FINSEQ_2:109

for i being Nat
for D being non empty set
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*> is Element of 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*> is Element of 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*> is Element of 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 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;