Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

### Finite Sequences and Tuples of Elements of a Non-empty Sets

by
Czeslaw Bylinski

MML identifier: FINSEQ_2
[ Mizar article, MML identifier index ]

```environ

vocabulary ORDINAL2, ARYTM, FINSEQ_1, SQUARE_1, BOOLE, ARYTM_1, FUNCT_1,
RELAT_1, FUNCT_2, FUNCOP_1, PARTFUN1, TARSKI, FINSEQ_2;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2,
NUMBERS, XCMPLX_0, XREAL_0, DOMAIN_1, NAT_1, SQUARE_1, RELAT_1, FUNCT_1,
PARTFUN1, FUNCT_2, FUNCT_3, FINSEQ_1, BINOP_1, FUNCOP_1;
constructors DOMAIN_1, NAT_1, SQUARE_1, FUNCT_3, FINSEQ_1, BINOP_1, FUNCOP_1,
PARTFUN1, MEMBERED, RELAT_2, XBOOLE_0;
clusters SUBSET_1, FUNCT_1, FINSEQ_1, RELSET_1, XREAL_0, FUNCOP_1, FUNCT_2,
NAT_1, MEMBERED, ZFMISC_1, PARTFUN1, XBOOLE_0, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;

begin

reserve i,j,l for Nat;
reserve k for natural number;
reserve A,a,b,x,x1,x2,x3 for set;
reserve D,D',E for non empty set;
reserve d,d1,d2,d3 for Element of D;
reserve d',d1',d2',d3' for Element of D';
reserve p,q,r for FinSequence;

:: Auxiliary theorems

theorem :: FINSEQ_2:1
min(i,j) is Nat & max(i,j) is Nat;

theorem :: FINSEQ_2:2
l = min(i,j) implies Seg i /\ Seg j = Seg l;

theorem :: FINSEQ_2:3
i <= j implies max(0,i-j) = 0;

theorem :: FINSEQ_2:4
j <= i implies max(0,i-j) = i-j;

theorem :: FINSEQ_2:5
max(0,i-j) is Nat;

theorem :: FINSEQ_2:6
min(0,i) = 0 & min(i,0) = 0 & max(0,i) = i & max(i,0) = i;

:: Non-empty Segments of Natural Numbers

canceled;

theorem :: FINSEQ_2:8
i in Seg (l+1) implies i in Seg l or i = l+1;

theorem :: FINSEQ_2:9
i in Seg l implies i in Seg(l+j);

:: Additional propositions related to Finite Sequences

theorem :: FINSEQ_2:10
len p = i & len q = i & (for j st j in Seg i holds p.j = q.j)
implies p = q;

theorem :: FINSEQ_2:11
b in rng p implies ex i st i in dom p & p.i = b;

canceled;

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

theorem :: FINSEQ_2:14
for D being set holds
(for i st i in dom p holds p.i in D) implies p is FinSequence of D;

theorem :: FINSEQ_2:15
<*d1,d2*> is FinSequence of D;

theorem :: FINSEQ_2:16
<*d1,d2,d3*> is FinSequence of D;

canceled;

theorem :: FINSEQ_2:18
i in dom p implies i in dom(p^q);

theorem :: FINSEQ_2:19
len(p^<*a*>) = len p + 1;

theorem :: FINSEQ_2:20
p^<*a*> = q^<*b*> implies p = q & a = b;

theorem :: FINSEQ_2:21
len p = i + 1 implies ex q,a st p = q^<*a*>;

theorem :: FINSEQ_2:22
for p being FinSequence of D
st len p <> 0 ex q being (FinSequence of D),d st p = q^<*d*>;

theorem :: FINSEQ_2:23
q = p|(Seg i) & len p <= i implies p = q;

theorem :: FINSEQ_2:24
q = p|(Seg i) implies len q = min(i,len p);

theorem :: FINSEQ_2:25
len r = i+j implies ex p,q st len p = i & len q = j & r = p^q;

theorem :: FINSEQ_2:26
for r being FinSequence of D st len r = i+j
ex p,q being FinSequence of D st len p = i & len q = j & r = p^q;

scheme SeqLambdaD{i()->Nat,D()->non empty set,F(set)->Element of D()}:
ex z being FinSequence of D() st len z = i() &
for j st j in Seg i() holds z.j = F(j);

scheme IndSeqD{D()->non empty set, P[set]}:
for p being FinSequence of D() holds P[p]
provided
P[<*> D()] and
for p being FinSequence of D() for x being Element of D()
st P[p] holds P[p^<*x*>];

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

theorem :: FINSEQ_2:28
for f being Function of Seg i, D holds f is FinSequence of D;

canceled;

theorem :: FINSEQ_2:30
for p being FinSequence of D holds p is Function of dom p, D;

theorem :: FINSEQ_2:31
for f being Function of NAT,D holds f|(Seg i) is FinSequence of D;

theorem :: FINSEQ_2:32
for f being Function of NAT,D st q = f|(Seg i) holds len q = i;

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

theorem :: FINSEQ_2:34
D = Seg i implies
for p being FinSequence for q being FinSequence of D st i <= len p
holds p*q is FinSequence;

theorem :: FINSEQ_2:35
D = Seg i implies
for p being FinSequence of D' for q being FinSequence of D st i <= len p
holds p*q is FinSequence of D';

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

theorem :: FINSEQ_2:37
for p being FinSequence of A for f being Function of A,D'
st q = f*p holds len q = len p;

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

theorem :: FINSEQ_2:39
for p being FinSequence of D for f being Function of D,D'
st p = <*x1*> holds f*p = <*f.x1*>;

theorem :: FINSEQ_2:40
for p being FinSequence of D for f being Function of D,D'
st p = <*x1,x2*> holds f*p = <*f.x1,f.x2*>;

theorem :: FINSEQ_2:41
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*>;

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

theorem :: FINSEQ_2:43
for f being Function of Seg i,Seg i st i <= len p holds p*f is FinSequence;

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

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

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

theorem :: FINSEQ_2:47
for f being Permutation of Seg i st i <= len p & q = p*f holds len q = i;

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

theorem :: FINSEQ_2:49
for p being FinSequence of D for f being Function of Seg i,Seg j
st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence of D;

theorem :: FINSEQ_2:50
for p being FinSequence of D for f being Function of Seg i,Seg i
st i <= len p holds p*f is FinSequence of D;

theorem :: FINSEQ_2:51
for p being FinSequence of D for f being Function of dom p,dom p
holds p*f is FinSequence of D;

theorem :: FINSEQ_2:52
id Seg k is FinSequence of NAT;

definition let i be natural number;
func idseq i -> FinSequence equals
:: FINSEQ_2:def 1
id Seg i;
end;

canceled;

theorem :: FINSEQ_2:54
dom idseq k = Seg k;

theorem :: FINSEQ_2:55
len idseq k = k;

theorem :: FINSEQ_2:56
j in Seg i implies (idseq i).j = j;

theorem :: FINSEQ_2:57
i<>0 implies for k being Element of Seg i holds (idseq i).k = k;

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

theorem :: FINSEQ_2:59
idseq 1 = <*1*>;

theorem :: FINSEQ_2:60
idseq (i+1) = (idseq i) ^ <*i+1*>;

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

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

theorem :: FINSEQ_2:63
p*(idseq k) = p|(Seg k);

theorem :: FINSEQ_2:64
len p <= k implies p*(idseq k) = p;

theorem :: FINSEQ_2:65
idseq k is Permutation of Seg k;

theorem :: FINSEQ_2:66
(Seg k) --> a is FinSequence;

definition let i be natural number, a be set;
func i |-> a -> FinSequence equals
:: FINSEQ_2:def 2
Seg i --> a;
end;

canceled;

theorem :: FINSEQ_2:68
dom(k |-> a) = Seg k;

theorem :: FINSEQ_2:69
len(k |-> a) = k;

theorem :: FINSEQ_2:70
b in Seg k implies (k |-> a).b = a;

theorem :: FINSEQ_2:71
k<>0 implies for w being Element of Seg k holds (k |-> d).w = d;

theorem :: FINSEQ_2:72
0 |-> a = {};

theorem :: FINSEQ_2:73
1 |-> a = <*a*>;

theorem :: FINSEQ_2:74
(i+1) |-> a = (i |-> a) ^ <*a*>;

theorem :: FINSEQ_2:75
2 |-> a = <*a,a*>;

theorem :: FINSEQ_2:76
3 |-> a = <*a,a,a*>;

theorem :: FINSEQ_2:77
k |-> d is FinSequence of D;

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

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

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

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

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

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

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

theorem :: FINSEQ_2:85
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);

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

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

theorem :: FINSEQ_2:88
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')*>;

theorem :: FINSEQ_2:89
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')*>;

theorem :: FINSEQ_2:90
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')*>;

theorem :: FINSEQ_2:91
for F being Function of [:D,D':],E for p being FinSequence of D'
holds F[;](d,p) is FinSequence of E;

theorem :: FINSEQ_2:92
for F being Function of [:D,D':],E for p being FinSequence of D'
st r = F[;](d,p) holds len r = len p;

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

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

theorem :: FINSEQ_2:95
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')*>;

theorem :: FINSEQ_2:96
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')*>;

theorem :: FINSEQ_2:97
for F being Function of [:D,D':],E for p being FinSequence of D
holds F[:](p,d') is FinSequence of E;

theorem :: FINSEQ_2:98
for F being Function of [:D,D':],E for p being FinSequence of D
st r = F[:](p,d') holds len r = len p;

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

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

theorem :: FINSEQ_2:101
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')*>;

theorem :: FINSEQ_2:102
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')*>;

:: T u p l e s

definition let D be set;
mode FinSequenceSet of D -> set means
:: FINSEQ_2:def 3
a in it implies a is FinSequence of D;
end;

definition let D be set;
cluster non empty FinSequenceSet of D;
end;

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

canceled;

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

definition let D be set;
redefine func D* -> FinSequence-DOMAIN of D;
end;

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

definition let D be set, S be FinSequence-DOMAIN of D;
redefine mode Element of S -> FinSequence of D;
end;

canceled;

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

reserve s for Element of D*;

definition let i be natural number; let D be set;
func i-tuples_on D -> FinSequenceSet of D equals
:: FINSEQ_2:def 4
{ s where s is Element of D*: len s = i };
end;

definition let i be natural number, D;
cluster i-tuples_on D -> non empty;
end;

canceled;

theorem :: FINSEQ_2:109
for z being Element of i-tuples_on D holds len z = i;

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

theorem :: FINSEQ_2:111
i-tuples_on D = Funcs(Seg i,D);

theorem :: FINSEQ_2:112
for D being set holds 0-tuples_on D = { <*>D };

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

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

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

theorem :: FINSEQ_2:116
1-tuples_on D = { <*d*>: not contradiction };

theorem :: FINSEQ_2:117
for z being Element of 1-tuples_on D ex d st z = <*d*>;

theorem :: FINSEQ_2:118
<*d*> is Element of 1-tuples_on D;

theorem :: FINSEQ_2:119
2-tuples_on D = { <*d1,d2*>: not contradiction };

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

theorem :: FINSEQ_2:121
<*d1,d2*> is Element of 2-tuples_on D;

theorem :: FINSEQ_2:122
3-tuples_on D = { <*d1,d2,d3*>: not contradiction };

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

theorem :: FINSEQ_2:124
<*d1,d2,d3*> is Element of 3-tuples_on D;

theorem :: FINSEQ_2:125
(i+j)-tuples_on D = {z^t where z is (Element of i-tuples_on D),
t is Element of j-tuples_on D: not contradiction};

theorem :: FINSEQ_2:126
for s being Element of (i+j)-tuples_on D
ex z being (Element of i-tuples_on D), t being Element of j-tuples_on D
st s = z^t;

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

theorem :: FINSEQ_2:128
D* = union {i-tuples_on D: not contradiction};

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

theorem :: FINSEQ_2:130
i-tuples_on D = j-tuples_on D implies i = j;

theorem :: FINSEQ_2:131
idseq i is Element of i-tuples_on NAT;

theorem :: FINSEQ_2:132
i |-> d is Element of i-tuples_on D;

theorem :: FINSEQ_2:133
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';

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

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

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

theorem :: FINSEQ_2:137
for z being Element of (i+1)-tuples_on D
ex t being (Element of i-tuples_on D), d st z = t^<*d*>;

theorem :: FINSEQ_2:138
for z being Element of i-tuples_on D holds z*(idseq i) = z;

theorem :: FINSEQ_2:139
for z1,z2 being Element of i-tuples_on D
st for j st j in Seg i holds z1.j = z2.j
holds z1 = z2;

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

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

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

theorem :: FINSEQ_2:143
(i+j)|->x = (i|->x)^(j|->x);

theorem :: FINSEQ_2:144
for i, D
for x being Element of i-tuples_on D
holds dom x = Seg i;

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

theorem :: FINSEQ_2:146
for f being Function,
x, y, z being set st x in dom f & y in dom f & z in dom f holds
f*<*x,y,z*> = <*f.x,f.y,f.z*>;

theorem :: FINSEQ_2:147
rng <*x1,x2*> = {x1,x2};

theorem :: FINSEQ_2:148
rng <*x1,x2,x3*> = {x1,x2,x3};
```