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

begin

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 9, XXREAL_0:def 10;

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;

Lm1: 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;

Lm2: 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 CARD_1:47, FINSEQ_1:63;

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{ 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 dom z holds
z . j = F₃(j) ) )

proof end;

scheme :: FINSEQ_2:sch 2
IndSeqD{ F₁() -> 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 set
for D1 being Subset of D
for p being FinSequence of D1 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, 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

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

proof end;

theorem :: FINSEQ_2:38

for x being set
for f being Function st x in dom f holds
f * <*x*> = <*(f . x)*>

proof end;

theorem :: FINSEQ_2:39

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)*>

proof end;

theorem Th40: :: FINSEQ_2:40

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)*>

proof end;

theorem Th41: :: FINSEQ_2:41

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)*>

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

registration

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

proof end;

end;

registration

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

end;

theorem :: FINSEQ_2:53

canceled;

theorem :: FINSEQ_2:54

canceled;

theorem :: FINSEQ_2:55

canceled;

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

canceled;

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*> by Th59, Th60;

theorem :: FINSEQ_2:62

idseq 3 = <*1,2,3*> by Th60, Th61;

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;

registration

let k be Nat;
let a be set ;
cluster k |-> a -> k -element ;
coherence
k |-> a is k -element

proof end;

end;

theorem :: FINSEQ_2:67

canceled;

theorem :: FINSEQ_2:68

canceled;

theorem :: FINSEQ_2:69

canceled;

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;

Lm3: 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;

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

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;

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

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, 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

proof end;

theorem Th85: :: FINSEQ_2:85

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))

proof end;

theorem Th86: :: FINSEQ_2:86

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 & r = F .: (p,q) holds
( len r = len p & len r = len q )

proof end;

theorem :: FINSEQ_2:87

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 & F .: (p,(<*> D9)) = <*> E )

proof end;

theorem :: FINSEQ_2:88

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*> & q = <*d19*> holds
F .: (p,q) = <*(F . (d1,d19))*>

proof end;

theorem :: FINSEQ_2:89

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*> & q = <*d19,d29*> holds
F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*>

proof end;

theorem :: FINSEQ_2:90

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*> & q = <*d19,d29,d39*> holds
F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*>

proof end;

theorem Th91: :: FINSEQ_2:91

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

proof end;

theorem Th92: :: FINSEQ_2:92

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

proof end;

theorem :: FINSEQ_2:93

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

proof end;

theorem :: FINSEQ_2:94

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))*>

proof end;

theorem :: FINSEQ_2:95

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))*>

proof end;

theorem :: FINSEQ_2:96

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))*>

proof end;

theorem Th97: :: FINSEQ_2:97

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

proof end;

theorem Th98: :: FINSEQ_2:98

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

proof end;

theorem :: FINSEQ_2:99

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

proof end;

theorem :: FINSEQ_2:100

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))*>

proof end;

theorem :: FINSEQ_2:101

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))*>

proof end;

theorem :: FINSEQ_2:102

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))*>

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 b₁ being set st
for a being set st a in b₁ holds
a is FinSequence of D

proof end;

end;

:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def 3 :
for D, b₂ being set holds
( b₂ is FinSequenceSet of D iff for a being set st a in b₂ holds
a is FinSequence of D );

registration

let D be set ;
cluster non empty FinSequenceSet of D;
existence
not for b₁ being FinSequenceSet of D holds b₁ 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 D9 being FinSequence-DOMAIN of D holds D9 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 b₁ being Element of S holds b₁ is FinSequence of D by Def3;

end;

theorem :: FINSEQ_2:106

canceled;

theorem :: FINSEQ_2:107

for D being non empty set
for D9 being non empty Subset of D
for S being FinSequence-DOMAIN of D9 holds S is FinSequence-DOMAIN of D

proof end;

registration

let i be Nat;
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like V42() i -element FinSequence-like FinSubsequence-like FinSequence of D;
existence
ex b₁ being FinSequence of D st b₁ is i -element

proof end;

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

registration

let D be non empty set ;
let i be Nat;
cluster -> i -element Element of i -tuples_on D;
coherence
for b₁ being Element of i -tuples_on D holds b₁ is i -element

proof end;

end;

theorem :: FINSEQ_2:108

canceled;

theorem :: FINSEQ_2:109

canceled;

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 :: FINSEQ_2:112

for D being set holds 0 -tuples_on D = {(<*> D)}

proof end;

theorem :: FINSEQ_2:113

canceled;

theorem :: FINSEQ_2:114

canceled;

theorem :: FINSEQ_2:115

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 & t ^ z = t ) by FINSEQ_1:47;

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;

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

proof end;

theorem Th117: :: FINSEQ_2:117

for D being non empty set
for z being Tuple of 1,D ex d being Element of D st z = <*d*>

proof end;

theorem Th118: :: 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 Tuple of 2,D ex d1, d2 being Element of D st z = <*d1,d2*>

proof end;

theorem Th121: :: 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 Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>

proof end;

theorem Th124: :: 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 Tuple of i,D, t is Tuple of j,D : verum }

proof end;

theorem Th126: :: FINSEQ_2:126

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

proof end;

theorem :: FINSEQ_2:127

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

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 D9 being non empty Subset of D
for z being Tuple of i,D9 holds z is Element of i -tuples_on D

proof end;

Lm7: for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b₁ -element FinSequence

proof end;

theorem :: FINSEQ_2:130

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

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, 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

proof end;

theorem Th134: :: FINSEQ_2:134

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

proof end;

theorem :: FINSEQ_2:135

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

proof end;

theorem :: FINSEQ_2:136

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

proof end;

theorem :: FINSEQ_2:137

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

proof end;

theorem :: FINSEQ_2:138

for i being Nat
for D being non empty set
for z being Tuple of i,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 Tuple of i,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, 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

proof end;

theorem :: FINSEQ_2:141

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

proof end;

theorem :: FINSEQ_2:142

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

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 Tuple of i,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 Lm1;

theorem :: FINSEQ_2:148

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

begin

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

proof end;

registration

let D be set ;
cluster -> functional FinSequenceSet of D;
coherence
for b₁ being FinSequenceSet of D holds b₁ is functional

proof end;

end;

definition

let D be non empty set ;
let n be Nat;
let d be Element of D;
:: original: |->
redefine func n |-> d -> FinSequence of D;
coherence
n |-> d is FinSequence of D by Th77;

end;

theorem :: FINSEQ_2:151

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 )

proof end;

theorem Th152: :: FINSEQ_2:152

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 & rng p c= A ) )

proof end;

theorem :: FINSEQ_2:153

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 )

proof end;

theorem :: FINSEQ_2:154

for A being set
for i being Element of NAT holds i -tuples_on A c= A *

proof end;

theorem Th155: :: FINSEQ_2:155

for A, x being set holds
( x in 1 -tuples_on A iff ex a being set st
( a in A & x = <*a*> ) )

proof end;

theorem :: FINSEQ_2:156

for A, a being set st <*a*> in 1 -tuples_on A holds
a in A

proof end;

theorem Th157: :: FINSEQ_2:157

for A, x being set holds
( x in 2 -tuples_on A iff ex a, b being set st
( a in A & b in A & x = <*a,b*> ) )

proof end;

theorem :: FINSEQ_2:158

for A, a, b being set st <*a,b*> in 2 -tuples_on A holds
( a in A & b in A )

proof end;

theorem Th159: :: FINSEQ_2:159

for A, x being set holds
( x in 3 -tuples_on A iff ex a, b, c being set st
( a in A & b in A & c in A & x = <*a,b,c*> ) )

proof end;

theorem :: FINSEQ_2:160

for A, a, b, c being set st <*a,b,c*> in 3 -tuples_on A holds
( a in A & b in A & c in A )

proof end;

theorem :: FINSEQ_2:161

for i being Nat
for x, A being set st x in i -tuples_on A holds
x is b₁ -element FinSequence by Lm7;

theorem :: FINSEQ_2:162

for A being non empty set
for n being Nat holds n -tuples_on A c= A *

proof end;

theorem :: FINSEQ_2:163

for x being set
for n, m being Nat st n |-> x = m |-> x holds
n = m

proof end;