:: Finite Sequences and Tuples of Elements of a Non-empty Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, XXREAL_0, CARD_1,
ARYTM_1, ARYTM_3, TARSKI, RELAT_1, FUNCT_1, ORDINAL4, FUNCT_2, FUNCOP_1,
ZFMISC_1, PARTFUN1, FINSEQ_2, PBOOLE, CARD_3, ORDINAL1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1,
NUMBERS, XCMPLX_0, DOMAIN_1, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2,
FUNCT_3, FINSEQ_1, BINOP_1, PBOOLE, FUNCOP_1, CARD_3, XXREAL_0;
constructors RELAT_2, PARTFUN1, BINOP_1, DOMAIN_1, FUNCT_3, FUNCOP_1,
SQUARE_1, NAT_1, FINSEQ_1, RELSET_1, PBOOLE, CARD_3, SETFAM_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, PARTFUN1, FUNCT_2,
FUNCOP_1, XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, CARD_3;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FINSEQ_1, CARD_1, PBOOLE;
equalities FINSEQ_1, FUNCOP_1, ORDINAL1;
expansions TARSKI, FUNCT_1, CARD_1, PBOOLE;
theorems TARSKI, ZFMISC_1, ENUMSET1, NAT_1, FUNCT_1, FUNCT_2, FUNCT_3,
FINSEQ_1, FUNCOP_1, RELAT_1, RELSET_1, XBOOLE_1, XREAL_1, GRFUNC_1,
XXREAL_0, ORDINAL1, CARD_1, SUBSET_1, CARD_3;
schemes FINSEQ_1, NAT_1, FRAENKEL, PBOOLE, FUNCT_2;
begin
reserve i,j,k,l for natural Number;
reserve A for set, a,b,x,x1,x2,x3 for object;
reserve D,D9,E for non empty set;
reserve d,d1,d2,d3 for Element of D;
reserve d9,d19,d29,d39 for Element of D9;
reserve p,q,r for FinSequence;
:: Auxiliary theorems
::$CT
theorem Th1:
l = min(i,j) implies Seg i /\ Seg j = Seg l
proof
i <= j or j <= i;
then i <= j & Seg i /\ Seg j = Seg i or j <= i & Seg i /\ Seg j = Seg j by
FINSEQ_1:7;
hence thesis by XXREAL_0:def 9;
end;
theorem Th2:
i <= j implies max(0,i-j) = 0
proof
assume i <= j;
then i-i <= j-i by XREAL_1:9;
then -(j-i) <= -0;
hence thesis by XXREAL_0:def 10;
end;
theorem Th3:
j <= i implies max(0,i-j) = i-j
proof
assume j <= i;
then j-j <= i-j by XREAL_1:9;
hence thesis by XXREAL_0:def 10;
end;
theorem
max(0,i-j) is Element of NAT
proof
per cases;
suppose
i <= j;
hence thesis by Th2;
end;
suppose
A1: j <= i;
then i - j is Element of NAT by NAT_1:21;
hence thesis by A1,Th3;
end;
end;
::$CT
theorem
i in Seg (l+1) implies i in Seg l or i = l+1
proof
A0: i is Nat by TARSKI:1;
assume
A1: i in Seg(l+1);
then i <= l+1 by FINSEQ_1:1;
then 1 <= i & i <= l or i = l+1 by A1,FINSEQ_1:1,NAT_1:8;
hence thesis by A0;
end;
theorem
i in Seg l implies i in Seg(l+j)
proof
l <= l+j by NAT_1:11;
then Seg l c= Seg(l+j) by FINSEQ_1:5;
hence thesis;
end;
:: Additional propositions related to Finite Sequences
theorem
len p = len q & (for j being Nat st j in dom p holds p.j = q.j) implies p = q
proof
assume that
A1: len p = len q and
A2: for j being Nat st j in dom p holds p.j = q.j;
dom p = Seg len p & dom q = Seg len p by A1,FINSEQ_1:def 3;
hence thesis by A2;
end;
theorem Th8:
b in rng p implies ex i being Nat st i in dom p & p.i = b
proof
assume b in rng p;
then ex a being object st a in dom p & b = p.a by FUNCT_1:def 3;
hence thesis;
end;
theorem Th9:
for D being set for p being D-valued FinSequence st i in dom p holds p.i in D
proof
let D be set;
let p be D-valued FinSequence;
assume i in dom p;
then
A1: p.i in rng p by FUNCT_1:def 3;
rng p c= D by RELAT_1:def 19;
hence thesis by A1;
end;
theorem Th10:
for D being set holds (for i being Nat st i in dom p holds p.i in D)
implies p is FinSequence of D
proof
let D be set;
assume
A1: for i being Nat st i in dom p holds p.i in D;
let b be object;
assume b in rng p;
then ex i being Nat st i in dom p & p.i = b by Th8;
hence thesis by A1;
end;
Lm1: rng <*x1,x2*> = {x1,x2}
proof
thus rng<* x1,x2 *> = rng<* x1 *> \/ rng <* x2 *> by FINSEQ_1:31
.= rng<* x1 *> \/ {x2} by FINSEQ_1:38
.= {x1} \/ {x2} by FINSEQ_1:39
.= {x1,x2} by ENUMSET1:1;
end;
theorem Th11:
<*d1,d2*> is FinSequence of D
proof
rng <*d1,d2*> = {d1,d2} by Lm1;
hence thesis by FINSEQ_1:def 4;
end;
Lm2: rng <*x1,x2,x3*> = {x1,x2,x3}
proof
thus rng <* x1,x2,x3 *> = rng(<* x1 *> ^ <* x2,x3 *>) by FINSEQ_1:43
.= rng<* x1 *> \/ rng <* x2,x3 *> by FINSEQ_1:31
.= {x1} \/ rng<* x2,x3 *> by FINSEQ_1:38
.= {x1} \/ {x2,x3} by Lm1
.= {x1,x2,x3} by ENUMSET1:2;
end;
theorem Th12:
<*d1,d2,d3*> is FinSequence of D
proof
rng <*d1,d2,d3*> = {d1,d2,d3} by Lm2;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th13:
i in dom p implies i in dom(p^q)
proof
A1: dom p c= dom(p^q) by FINSEQ_1:26;
assume i in dom p;
hence thesis by A1;
end;
theorem Th14:
len(p^<*a*>) = len p + 1
proof
len(p^<*a*>) = len p + len <*a*> by FINSEQ_1:22;
hence thesis by FINSEQ_1:39;
end;
theorem
p^<*a*> = q^<*b*> implies p = q & a = b
proof
assume
A1: p^<*a*> = q^<*b*>;
A2: (p^<*a*>).(len p + 1) = a & (q^<*b*>).(len q + 1) = b by FINSEQ_1:42;
len(p^<*a*>) = len p + 1 & len(q^<*b*>) = len q + 1 by Th14;
hence thesis by A1,A2,FINSEQ_1:33;
end;
theorem
len p = i + 1 implies ex q,a st p = q^<*a*> by CARD_1:27,FINSEQ_1:46;
theorem Th17:
for p being FinSequence of A st len p <> 0 ex q being
FinSequence of A, d being Element of A st p = q^<*d*>
proof
let p be FinSequence of A;
assume
A1: len p <> 0;
then p <> {};
then consider q being FinSequence,d being object such that
A2: p = q^<*d*> by FINSEQ_1:46;
for i be Nat st i in dom q holds q.i in A
proof
let i be Nat;
assume i in dom q;
then p.i = q.i & i in dom p by A2,Th13,FINSEQ_1:def 7;
hence thesis by Th9;
end;
then
A3: q is FinSequence of A by Th10;
len p in Seg len p by A1,FINSEQ_1:3;
then
A4: len p in dom p by FINSEQ_1:def 3;
len p = len q + 1 by A2,Th14;
then p.(len p) = d by A2,FINSEQ_1:42;
then d is Element of A by A4,Th9;
hence thesis by A2,A3;
end;
theorem Th18:
q = p|(Seg i) & len p <= i implies p = q
proof
assume
A1: q = p|(Seg i);
assume len p <= i;
then Seg len p c= Seg i by FINSEQ_1:5;
then dom p c= Seg i by FINSEQ_1:def 3;
hence thesis by A1,RELAT_1:68;
end;
theorem
q = p|(Seg i) implies len q = min(i,len p)
proof
assume
A1: q = p|(Seg i);
now
per cases;
case
i <= len p;
hence len q = i by A1,FINSEQ_1:17;
end;
case
not i <= len p;
hence len q = len p by A1,Th18;
end;
end;
hence thesis by XXREAL_0:def 9;
end;
theorem Th20:
len r = i+j implies ex p,q st len p = i & len q = j & r = p^q
proof
assume
A1: len r = i+j;
reconsider z=i as Element of NAT by ORDINAL1:def 12;
reconsider p = r|(Seg z) as FinSequence by FINSEQ_1:15;
consider q being FinSequence such that
A2: r = p^q by FINSEQ_1:80;
take p,q;
i <= len r by A1,NAT_1:11;
hence len p = i by FINSEQ_1:17;
then len(p^q) = i + len q by FINSEQ_1:22;
hence len q = j by A1,A2;
thus thesis by A2;
end;
theorem Th21:
for r being D-valued FinSequence st len r = i+j
ex p,q being FinSequence of D st len p = i & len q = j & r = p^q
proof
let r be D-valued FinSequence;
assume len r = i+j;
then consider p,q being FinSequence such that
A1: len p = i & len q = j and
A2: r = p^q by Th20;
p is FinSequence of D & q is FinSequence of D by A2,FINSEQ_1:36;
hence thesis by A1,A2;
end;
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 being Nat st j in dom z holds z.j = F(j)
proof
consider z being FinSequence such that
A1: len z = i() and
A2: for i being Nat st i in dom z holds z.i = F(i) from FINSEQ_1:sch 2;
A3: Seg i() = dom z by A1,FINSEQ_1:def 3;
for j be Nat st j in Seg i() holds z.j in D()
proof
let j be Nat;
assume j in Seg i();
then z.j = F(j) by A2,A3;
hence thesis;
end;
then reconsider z as FinSequence of D() by A3,Th10;
take z;
thus len z = i() by A1;
let j be Nat;
thus thesis by A2;
end;
scheme
IndSeqD{D()->set, P[set]}: for p being FinSequence of D() holds P[p]
provided
A1: P[<*> D()] and
A2: for p being FinSequence of D() for x being Element of D() st P[p]
holds P[p^<*x*>]
proof
defpred R[set] means for p being FinSequence of D() st len p = $1 holds P[p];
A3: for i be Nat st R[i] holds R[i+1]
proof
let i be Nat such that
A4: for p being FinSequence of D() st len p = i holds P[p];
let p be FinSequence of D();
assume
A5: len p = i + 1;
then consider q being FinSequence of D(), x being Element of D() such that
A6: p = q^<*x*> by Th17;
len p = len q + 1 by A6,Th14;
hence thesis by A2,A4,A5,A6;
end;
let p be FinSequence of D();
A7: len p = len p;
A8: R[0] proof let p be FinSequence of D();
assume len p = 0;
then p = <*>D();
hence thesis by A1;
end;
for i be Nat holds R[i] from NAT_1:sch 2(A8,A3);
hence thesis by A7;
end;
theorem Th22:
for D being set, D1 being Subset of D for p being FinSequence of D1
holds p is FinSequence of D
proof
let D be set, D1 be Subset of D;
let p be FinSequence of D1;
rng p c= D1 by FINSEQ_1:def 4;
hence rng p c= D by XBOOLE_1:1;
end;
theorem Th23:
for f being Function of Seg i, D holds f is FinSequence of D
proof
let f be Function of Seg i, D;
reconsider i as Element of NAT by ORDINAL1:def 12;
dom f = Seg i by FUNCT_2:def 1;
then
A1: f is FinSequence by FINSEQ_1:def 2;
rng f c= D by RELAT_1:def 19;
hence thesis by A1,FINSEQ_1:def 4;
end;
theorem
for p being FinSequence of D holds p is Function of dom p, D
proof
let p be FinSequence of D;
rng p c= D by FINSEQ_1:def 4;
hence thesis by FUNCT_2:2;
end;
theorem
for f being sequence of D holds f|(Seg i) is FinSequence of D
proof
reconsider i as Nat by TARSKI:1;
for f being sequence of D holds f|(Seg i) is FinSequence of D by Th23;
hence thesis;
end;
theorem
for f being sequence of D st q = f|(Seg i) holds len q = i
proof
let f be sequence of D;
reconsider i as Element of NAT by ORDINAL1:def 12;
dom(f|(Seg i)) = Seg i by FUNCT_2:def 1;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th27:
for f being Function st rng p c= dom f & q = f*p holds len q = len p
proof
let f be Function;
assume rng p c= dom f;
then dom(f*p) = dom p by RELAT_1:27;
then dom(f*p) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th28:
D = Seg i implies for p being FinSequence for q being
FinSequence of D st i <= len p holds p*q is FinSequence
proof
assume
A1: D = Seg i;
let p be FinSequence;
let q be FinSequence of D;
assume i <= len p;
then Seg i c= Seg len p by FINSEQ_1:5;
then
A2: Seg i c= dom p by FINSEQ_1:def 3;
rng q c= Seg i by A1,FINSEQ_1:def 4;
then dom (p*q) = dom q by A2,RELAT_1:27,XBOOLE_1:1;
then dom (p*q) = Seg len q by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
theorem
D = Seg i implies for p being FinSequence of D9 for q being
FinSequence of D st i <= len p holds p*q is FinSequence of D9
proof
assume
A1: D = Seg i;
let p be FinSequence of D9;
let q be FinSequence of D;
assume i <= len p;
then reconsider pq = p*q as FinSequence by A1,Th28;
rng pq c= rng p & rng p c= D9 by FINSEQ_1:def 4,RELAT_1:26;
then rng pq c= D9;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th30:
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
let A,D be set;
let p be FinSequence of A;
let f be Function of A,D;
per cases;
suppose D = {};
then f*p = <*>D;
hence thesis;
end;
suppose
A1: D <> {};
A2: rng p c= A by RELAT_1:def 19;
A3: rng(f*p) c= D by RELAT_1:def 19;
dom f = A by A1,FUNCT_2:def 1;
then f*p is FinSequence by A2,FINSEQ_1:16;
hence thesis by A3,FINSEQ_1:def 4;
end;
end;
theorem Th31:
for p being FinSequence of A
for f being Function of A,D9 st q = f*p holds len q = len p
proof
let p be FinSequence of A;
let f be Function of A,D9;
dom f = A & rng p c= A by FINSEQ_1:def 4,FUNCT_2:def 1;
hence thesis by Th27;
end;
theorem
for x being set, f being Function st x in dom f holds f*<*x*> = <*f.x*>
proof
let x be set, f be Function;
assume A1: x in dom f;
then reconsider D = dom f, E = rng f as non empty set by FUNCT_1:3;
rng <*x*> = {x} by FINSEQ_1:38;
then rng <*x*> c= D by A1,ZFMISC_1:31;
then reconsider p = <*x*> as FinSequence of D by FINSEQ_1:def 4;
reconsider f as Function of D, E by FUNCT_2:def 1,RELSET_1:4;
reconsider q = f*p as FinSequence of E by Th30;
A2: p.1 = x;
A3: len q = len p by Th31 .= 1 by FINSEQ_1:39;
then 1 in Seg len q;
then 1 in dom q by FINSEQ_1:def 3;
then q.1 = f.x by A2,FUNCT_1:12;
hence thesis by A3,FINSEQ_1:40;
end;
theorem
for p being FinSequence of D
for f being Function of D,D9 st p = <*x1*> holds f*p = <*f.x1*>
proof
let p be FinSequence of D;
let f be Function of D,D9 such that
A1: p = <*x1*>;
A2: p.1 = x1 by A1;
reconsider q = f*p as FinSequence of D9 by Th30;
len p = 1 by A1,FINSEQ_1:39;
then
A3: len q = 1 by Th31;
then 1 in Seg len q;
then 1 in dom q by FINSEQ_1:def 3;
then q.1 = f.x1 by A2,FUNCT_1:12;
hence thesis by A3,FINSEQ_1:40;
end;
theorem Th34:
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
let p be FinSequence of D;
let f be Function of D,D9 such that
A1: p = <*x1,x2*>;
A2: p.2 = x2 by A1;
reconsider q = f*p as FinSequence of D9 by Th30;
len p = 2 by A1,FINSEQ_1:44;
then
A3: len q = 2 by Th31;
then 2 in Seg len q;
then 2 in dom q by FINSEQ_1:def 3;
then
A4: q.2 = f.x2 by A2,FUNCT_1:12;
1 in Seg len q by A3;
then
A5: 1 in dom q by FINSEQ_1:def 3;
p.1 = x1 by A1;
then q.1 = f.x1 by A5,FUNCT_1:12;
hence thesis by A3,A4,FINSEQ_1:44;
end;
theorem Th35:
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
let p be FinSequence of D;
let f be Function of D,D9 such that
A1: p = <*x1,x2,x3*>;
A2: p.2 = x2 by A1;
reconsider q = f*p as FinSequence of D9 by Th30;
len p = 3 by A1,FINSEQ_1:45;
then
A3: len q = 3 by Th31;
then 2 in Seg len q;
then 2 in dom q by FINSEQ_1:def 3;
then
A4: q.2 = f.x2 by A2,FUNCT_1:12;
A5: p.3 = x3 by A1;
A6: p.1 = x1 by A1;
3 in Seg len q by A3;
then 3 in dom q by FINSEQ_1:def 3;
then
A7: q.3 = f.x3 by A5,FUNCT_1:12;
1 in Seg len q by A3;
then 1 in dom q by FINSEQ_1:def 3;
then q.1 = f.x1 by A6,FUNCT_1:12;
hence thesis by A3,A4,A7,FINSEQ_1:45;
end;
theorem Th36:
for f being Function of Seg i,Seg j st (j = 0 implies i = 0) & j <= len p
holds p*f is FinSequence
proof
A0: i is Nat by TARSKI:1;
let f be Function of Seg i,Seg j;
assume j = 0 implies i = 0;
then Seg j = {} implies Seg i = {};
then
A1: dom f = Seg i by FUNCT_2:def 1;
assume j <= len p;
then rng f c= Seg j & Seg j c= Seg len p by FINSEQ_1:5,RELAT_1:def 19;
then rng f c= Seg len p;
then rng f c= dom p by FINSEQ_1:def 3;
then dom(p*f) = dom f by RELAT_1:27;
hence thesis by A0,A1,FINSEQ_1:def 2;
end;
theorem
for f being Function of Seg i,Seg i st i <= len p holds p*f is
FinSequence by Th36;
theorem
for f being Function of dom p,dom p holds p*f is FinSequence
proof
dom p = Seg len p by FINSEQ_1:def 3;
hence thesis by Th36;
end;
theorem Th39:
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
let f be Function of Seg i,Seg i;
assume rng f = Seg i & i <= len p;
then rng f c= Seg len p by FINSEQ_1:5;
then rng f c= dom p by FINSEQ_1:def 3;
then
A1: dom(p*f) = dom f by RELAT_1:27;
i is Element of NAT & dom f = Seg i by FUNCT_2:52,ORDINAL1:def 12;
hence thesis by A1,FINSEQ_1:def 3;
end;
theorem Th40:
for f being Function of dom p,dom p st rng f = dom p & q = p*f
holds len q = len p
proof
Seg len p = dom p by FINSEQ_1:def 3;
hence thesis by Th39;
end;
theorem Th41:
for f being Permutation of Seg i st i <= len p & q = p*f holds len q = i
proof
let f be Permutation of Seg i;
rng f = Seg i by FUNCT_2:def 3;
hence thesis by Th39;
end;
theorem
for f being Permutation of dom p st q = p*f holds len q = len p
proof
Seg len p = dom p by FINSEQ_1:def 3;
hence thesis by Th41;
end;
theorem Th43:
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
let p be FinSequence of D;
let f be Function of Seg i,Seg j such that
A1: ( j = 0 implies i = 0)& j <= len p;
set q = p*f;
rng p c= D & rng q c= rng p by FINSEQ_1:def 4,RELAT_1:26;
then
A2: rng q c= D;
q is FinSequence by A1,Th36;
hence thesis by A2,FINSEQ_1:def 4;
end;
theorem
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 Th43;
theorem Th45:
for p being FinSequence of D for f being Function of dom p,dom p
holds p*f is FinSequence of D
proof
let p be FinSequence of D;
Seg len p = dom p by FINSEQ_1:def 3;
hence thesis by Th43;
end;
theorem Th46:
for k being natural Number holds id Seg k is FinSequence of NAT
proof
let k be natural Number;
set I = id Seg k;
reconsider k as Element of NAT by ORDINAL1:def 12;
dom I = Seg k;
then rng I = Seg k & I is FinSequence by FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 4;
end;
definition
let i be natural Number;
func idseq i -> FinSequence equals
id Seg i;
coherence by Th46;
end;
registration
let k be natural Number;
cluster idseq k -> k-element;
coherence
proof
k in NAT & dom idseq k = Seg k by ORDINAL1:def 12;
hence len idseq k = k by FINSEQ_1:def 3;
end;
end;
registration
cluster idseq 0 -> empty;
coherence;
end;
theorem
for k being Element of Seg i holds (idseq i).k = k;
theorem Th48:
idseq 1 = <*1*>
proof
1 in Seg 1;
then len idseq 1 = 1 & (idseq 1).1 = 1 by CARD_1:def 7,FUNCT_1:18;
hence thesis by FINSEQ_1:40;
end;
theorem Th49:
idseq (i+1) = (idseq i) ^ <*i+1*>
proof
set p = idseq (i+1);
consider q being FinSequence , a being object such that
A1: p = q^<*a*> by FINSEQ_1:46;
A2: len p = i + 1 & len p = len q + 1 by A1,Th14,CARD_1:def 7;
A3: dom q = Seg len q by FINSEQ_1:def 3;
A4: for a being object st a in Seg i holds q.a = a
proof
i <= i+1 by NAT_1:11;
then
A5: Seg i c= Seg (i+1) by FINSEQ_1:5;
let a be object;
assume
A6: a in Seg i;
then ex j be Nat st a = j & 1 <= j & j <= i;
then reconsider j = a as Nat;
p.j = q.j by A1,A2,A3,A6,FINSEQ_1:def 7;
hence thesis by A6,A5,FUNCT_1:18;
end;
p.(i+1) = i+1 by FINSEQ_1:4,FUNCT_1:18;
then a = i+1 by A1,A2,FINSEQ_1:42;
hence thesis by A1,A2,A3,A4,FUNCT_1:17;
end;
theorem Th50:
idseq 2 = <*1,2*> by Th48,Th49;
theorem
idseq 3 = <*1,2,3*> by Th49,Th50;
theorem Th52:
len p <= k implies p*(idseq k) = p
proof
assume
A1: len p <= k;
reconsider k as Element of NAT by ORDINAL1:def 12;
dom p = Seg len p by FINSEQ_1:def 3;
then dom p c= Seg k by A1,FINSEQ_1:5;
hence thesis by RELAT_1:51;
end;
theorem
idseq k is Permutation of Seg k;
theorem Th54:
for k being natural Number holds (Seg k) --> a is FinSequence
proof
let k be natural Number;
reconsider k as Element of NAT by ORDINAL1:def 12;
dom(Seg k --> a) = Seg k;
hence thesis by FINSEQ_1:def 2;
end;
registration
let i be natural Number, a be object;
cluster (Seg i) --> a -> FinSequence-like;
coherence by Th54;
end;
definition
let i be natural Number, a be object;
func i |-> a -> FinSequence equals
Seg i --> a;
coherence;
end;
registration
let k be natural Number, a be object;
cluster k |-> a -> k-element;
coherence
proof
k in NAT & dom(k |-> a) = Seg k by ORDINAL1:def 12;
hence len(k |-> a) = k by FINSEQ_1:def 3;
end;
end;
theorem
for d being object, w being set st w in Seg k holds (k |-> d).w = d
by FUNCOP_1:7;
theorem
for a being object holds 0 |-> a = {};
theorem Th57:
for a being object holds 1 |-> a = <*a*>
proof let a be object;
1 in Seg 1;
then len(1 |-> a) = 1 & (1 |-> a).1 = a by CARD_1:def 7,FUNCOP_1:7;
hence thesis by FINSEQ_1:40;
end;
theorem Th58:
for a being object holds (i+1) |-> a = (i |-> a) ^ <*a*>
proof let a be object;
set p = (i+1) |-> a;
consider q being FinSequence , x being object such that
A1: p = q^<*x*> by FINSEQ_1:46;
A2: len p = i + 1 & len p = len q + 1 by A1,Th14,CARD_1:def 7;
A3: now
per cases;
suppose
A4: i = 0;
then q = {} by A2;
hence q = i |-> a by A4;
end;
suppose
A5: i <> 0;
A6: rng q c= rng p & rng p = {a} by A1,FINSEQ_1:29,FUNCOP_1:8;
A7: dom q = Seg len q by FINSEQ_1:def 3;
then i in dom q by A2,A5,FINSEQ_1:3;
then q.i in rng q by FUNCT_1:def 3;
then rng q = {a} by A6,ZFMISC_1:33;
hence q = i |-> a by A2,A7,FUNCOP_1:9;
end;
end;
p.(i+1) = a by FINSEQ_1:4,FUNCOP_1:7;
hence thesis by A1,A2,A3,FINSEQ_1:42;
end;
theorem Th59:
for a being object holds 2 |-> a = <*a,a*>
proof let a be object;
thus 2 |-> a = (1+1) |-> a .= (1|->a)^<*a*> by Th58
.= <*a,a*> by Th57;
end;
theorem
for a being object holds 3 |-> a = <*a,a,a*>
proof let a be object;
thus 3 |-> a = (2+1) |-> a .= (2|->a)^<*a*> by Th58
.= <*a,a*>^<*a*> by Th59
.= <*a,a,a*>;
end;
theorem Th61:
for k being natural Number holds k |-> d is FinSequence of D
proof
let k be natural Number;
set s = k |-> d;
rng s c= {d} by FUNCOP_1:13;
then rng s c= D by XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
Lm3: 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
let F be Function such that
A1: [:rng p,rng q:] c= dom F and
A2: i = min(len p,len q);
A3: rng <:p,q:> c= [:rng p,rng q:] & dom <:p,q:> = dom p /\ dom q by FUNCT_3:51
,def 7;
dom p = Seg len p & dom q = Seg len q by FINSEQ_1:def 3;
then dom p /\ dom q = Seg i by A2,Th1;
hence thesis by A1,A3,RELAT_1:27,XBOOLE_1:1;
end;
theorem Th62:
for F being Function st [:rng p,rng q:] c= dom F holds F.:(p,q)
is FinSequence
proof
let F be Function;
reconsider k = min(len p,len q) as Element of NAT by XXREAL_0:15;
assume [:rng p,rng q:] c= dom F;
then dom(F.:(p,q)) = Seg k by Lm3;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th63:
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
let F be Function;
reconsider k = min(len p,len q) as Element of NAT by XXREAL_0:15;
assume [:rng p,rng q:] c= dom F;
then dom(F.:(p,q)) = Seg k by Lm3;
hence thesis by FINSEQ_1:def 3;
end;
Lm4: for F being Function st [:{a},rng p:] c= dom F holds dom(F[;](a,p)) = dom
p
proof
let F be Function such that
A1: [:{a},rng p:] c= dom F;
set q = dom p --> a;
dom q = dom p;
then
A2: dom <:q,p:> = dom p by FUNCT_3:50;
rng q c= {a} by FUNCOP_1:13;
then rng <:q,p:> c= [:rng q,rng p:] & [:rng q,rng p:] c= [:{a},rng p:] by
FUNCT_3:51,ZFMISC_1:95;
then
A3: rng <:q,p:> c= [:{a},rng p:];
thus thesis by A1,A3,A2,RELAT_1:27,XBOOLE_1:1;
end;
theorem Th64:
for F being Function st [:{a},rng p:] c= dom F holds F[;](a,p) is FinSequence
proof
let F be Function;
assume [:{a},rng p:] c= dom F;
then dom(F[;](a,p)) = dom p by Lm4;
then dom(F[;](a,p)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th65:
for F being Function st [:{a},rng p:] c= dom F & r = F[;](a,p)
holds len r = len p
proof
let F be Function;
assume [:{a},rng p:] c= dom F;
then dom(F[;](a,p)) = dom p by Lm4;
then dom(F[;](a,p)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
Lm5: for F being Function st [:rng p,{a}:] c= dom F holds dom(F[:](p,a)) = dom
p
proof
let F be Function such that
A1: [:rng p,{a}:] c= dom F;
set q = dom p --> a;
dom q = dom p;
then
A2: dom <:p,q:> = dom p by FUNCT_3:50;
rng q c= {a} by FUNCOP_1:13;
then rng <:p,q:> c= [:rng p,rng q:] & [:rng p,rng q:] c= [:rng p,{a}:] by
FUNCT_3:51,ZFMISC_1:95;
then
A3: rng <:p,q:> c= [:rng p,{a}:];
thus thesis by A1,A3,A2,RELAT_1:27,XBOOLE_1:1;
end;
theorem Th66:
for F being Function st [:rng p,{a}:] c= dom F holds F[:](p,a) is FinSequence
proof
let F be Function;
assume [:rng p,{a}:] c= dom F;
then dom(F[:](p,a)) = dom p by Lm5;
then dom(F[:](p,a)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th67:
for F being Function st [:rng p,{a}:] c= dom F & r = F[:](p,a)
holds len r = len p
proof
let F be Function;
assume [:rng p,{a}:] c= dom F;
then dom(F[:](p,a)) = dom p by Lm5;
then dom(F[:](p,a)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th68:
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let q be FinSequence of D9;
A1: rng(F.:(p,q)) c= rng F by RELAT_1:26;
rng p c= D & rng q c= D9 by FINSEQ_1:def 4;
then [:rng p,rng q:] c= [:D,D9:] by ZFMISC_1:96;
then [:rng p,rng q:] c= dom F by FUNCT_2:def 1;
then
A2: F.:(p,q) is FinSequence by Th62;
rng F c= E by RELAT_1:def 19;
then rng(F.:(p,q)) c= E by A1;
hence thesis by A2,FINSEQ_1:def 4;
end;
theorem Th69:
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let q be FinSequence of D9;
rng p c= D & rng q c= D9 by FINSEQ_1:def 4;
then [:rng p,rng q:] c= [:D,D9:] by ZFMISC_1:96;
then [:rng p,rng q:] c= dom F by FUNCT_2:def 1;
hence thesis by Th63;
end;
theorem Th70:
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let q be FinSequence of D9;
assume that
A1: len p = len q and
A2: r = F.:(p,q);
len r = min(len p,len q) by A2,Th69;
hence thesis by A1;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let p9 be FinSequence of D9;
reconsider r = F.:(<*>D,p9),r9 = F.:(p,<*>D9) as FinSequence of E by Th68;
len(<*>D) = 0;
then len r = min(0,len p9) & len r9 = min(len p,0) by Th69;
hence thesis by XXREAL_0:def 9;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let q be FinSequence of D9 such that
A1: p = <*d1*> & q = <*d19*>;
A2: p.1 = d1 & q.1 = d19 by A1;
reconsider r = F.:(p,q) as FinSequence of E by Th68;
len p = 1 & len q = 1 by A1,FINSEQ_1:39;
then
A3: len r = 1 by Th70;
then 1 in Seg len r;
then 1 in dom r by FINSEQ_1:def 3;
then r.1 = F.(d1,d19) by A2,FUNCOP_1:22;
hence thesis by A3,FINSEQ_1:40;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let q be FinSequence of D9 such that
A1: p = <*d1,d2*> & q = <*d19,d29*>;
A2: p.2 = d2 & q.2 = d29 by A1;
reconsider r = F.:(p,q) as FinSequence of E by Th68;
len p = 2 & len q = 2 by A1,FINSEQ_1:44;
then
A3: len r = 2 by Th70;
then 2 in Seg len r;
then 2 in dom r by FINSEQ_1:def 3;
then
A4: r.2 = F.(d2,d29) by A2,FUNCOP_1:22;
1 in Seg len r by A3;
then
A5: 1 in dom r by FINSEQ_1:def 3;
p.1 = d1 & q.1 = d19 by A1;
then r.1 = F.(d1,d19) by A5,FUNCOP_1:22;
hence thesis by A3,A4,FINSEQ_1:44;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
let q be FinSequence of D9 such that
A1: p = <*d1,d2,d3*> & q = <*d19,d29,d39*>;
A2: p.2 = d2 & q.2 = d29 by A1;
reconsider r = F.:(p,q) as FinSequence of E by Th68;
len p = 3 & len q = 3 by A1,FINSEQ_1:45;
then
A3: len r = 3 by Th70;
then 2 in Seg len r;
then 2 in dom r by FINSEQ_1:def 3;
then
A4: r.2 = F.(d2,d29) by A2,FUNCOP_1:22;
A5: p.3 = d3 & q.3 = d39 by A1;
A6: p.1 = d1 & q.1 = d19 by A1;
3 in Seg len r by A3;
then 3 in dom r by FINSEQ_1:def 3;
then
A7: r.3 = F.(d3,d39) by A5,FUNCOP_1:22;
1 in Seg len r by A3;
then 1 in dom r by FINSEQ_1:def 3;
then r.1 = F.(d1,d19) by A6,FUNCOP_1:22;
hence thesis by A3,A4,A7,FINSEQ_1:45;
end;
theorem Th75:
for F being Function of [:D,D9:],E for p being FinSequence of D9
holds F[;](d,p) is FinSequence of E
proof
let F be Function of [:D,D9:],E;
let p be FinSequence of D9;
A1: rng(F[;](d,p)) c= rng F by RELAT_1:26;
rng p c= D9 by FINSEQ_1:def 4;
then [:{d},rng p:] c= [:D,D9:] by ZFMISC_1:96;
then [:{d},rng p:] c= dom F by FUNCT_2:def 1;
then
A2: F[;](d,p) is FinSequence by Th64;
rng F c= E by RELAT_1:def 19;
then rng(F[;](d,p)) c= E by A1;
hence thesis by A2,FINSEQ_1:def 4;
end;
theorem Th76:
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D9;
rng p c= D9 by FINSEQ_1:def 4;
then [:{d},rng p:] c= [:D,D9:] by ZFMISC_1:96;
then [:{d},rng p:] c= dom F by FUNCT_2:def 1;
hence thesis by Th65;
end;
theorem
for F being Function of [:D,D9:],E holds F[;](d,<*>D9) = <*>E
proof
let F be Function of [:D,D9:],E;
reconsider r = F[;](d,<*>D9) as FinSequence of E by Th75;
len(<*>D9) = 0;
then len r = 0 by Th76;
hence thesis;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D9 such that
A1: p = <*d19*>;
A2: p.1 = d19 by A1;
reconsider r = F[;](d,p) as FinSequence of E by Th75;
len p = 1 by A1,FINSEQ_1:39;
then
A3: len r = 1 by Th76;
then 1 in Seg len r;
then 1 in dom r by FINSEQ_1:def 3;
then r.1 = F.(d,d19) by A2,FUNCOP_1:32;
hence thesis by A3,FINSEQ_1:40;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D9 such that
A1: p = <*d19,d29*>;
A2: p.2 = d29 by A1;
reconsider r = F[;](d,p) as FinSequence of E by Th75;
len p = 2 by A1,FINSEQ_1:44;
then
A3: len r = 2 by Th76;
then 2 in Seg len r;
then 2 in dom r by FINSEQ_1:def 3;
then
A4: r.2 = F.(d,d29) by A2,FUNCOP_1:32;
1 in Seg len r by A3;
then
A5: 1 in dom r by FINSEQ_1:def 3;
p.1 = d19 by A1;
then r.1 = F.(d,d19) by A5,FUNCOP_1:32;
hence thesis by A3,A4,FINSEQ_1:44;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D9 such that
A1: p = <*d19,d29,d39*>;
A2: p.2 = d29 by A1;
reconsider r = F[;](d,p) as FinSequence of E by Th75;
len p = 3 by A1,FINSEQ_1:45;
then
A3: len r = 3 by Th76;
then 2 in Seg len r;
then 2 in dom r by FINSEQ_1:def 3;
then
A4: r.2 = F.(d,d29) by A2,FUNCOP_1:32;
A5: p.3 = d39 by A1;
A6: p.1 = d19 by A1;
3 in Seg len r by A3;
then 3 in dom r by FINSEQ_1:def 3;
then
A7: r.3 = F.(d,d39) by A5,FUNCOP_1:32;
1 in Seg len r by A3;
then 1 in dom r by FINSEQ_1:def 3;
then r.1 = F.(d,d19) by A6,FUNCOP_1:32;
hence thesis by A3,A4,A7,FINSEQ_1:45;
end;
theorem Th81:
for F being Function of [:D,D9:],E for p being FinSequence of D
holds F[:](p,d9) is FinSequence of E
proof
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
A1: rng(F[:](p,d9)) c= rng F by RELAT_1:26;
rng p c= D by FINSEQ_1:def 4;
then [:rng p,{d9}:] c= [:D,D9:] by ZFMISC_1:96;
then [:rng p,{d9}:] c= dom F by FUNCT_2:def 1;
then
A2: F[:](p,d9) is FinSequence by Th66;
rng F c= E by RELAT_1:def 19;
then rng(F[:](p,d9)) c= E by A1;
hence thesis by A2,FINSEQ_1:def 4;
end;
theorem Th82:
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D;
rng p c= D by FINSEQ_1:def 4;
then [:rng p,{d9}:] c= [:D,D9:] by ZFMISC_1:96;
then [:rng p,{d9}:] c= dom F by FUNCT_2:def 1;
hence thesis by Th67;
end;
theorem
for F being Function of [:D,D9:],E holds F[:](<*>D,d9) = <*>E
proof
let F be Function of [:D,D9:],E;
reconsider r = F[:](<*>D,d9) as FinSequence of E by Th81;
len(<*>D) = 0;
then len r = 0 by Th82;
hence thesis;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D such that
A1: p = <*d1*>;
A2: p.1 = d1 by A1;
reconsider r = F[:](p,d9) as FinSequence of E by Th81;
len p = 1 by A1,FINSEQ_1:39;
then
A3: len r = 1 by Th82;
then 1 in Seg len r;
then 1 in dom r by FINSEQ_1:def 3;
then r.1 = F.(d1,d9) by A2,FUNCOP_1:27;
hence thesis by A3,FINSEQ_1:40;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D such that
A1: p = <*d1,d2*>;
A2: p.2 = d2 by A1;
reconsider r = F[:](p,d9) as FinSequence of E by Th81;
len p = 2 by A1,FINSEQ_1:44;
then
A3: len r = 2 by Th82;
then 2 in Seg len r;
then 2 in dom r by FINSEQ_1:def 3;
then
A4: r.2 = F.(d2,d9) by A2,FUNCOP_1:27;
1 in Seg len r by A3;
then
A5: 1 in dom r by FINSEQ_1:def 3;
p.1 = d1 by A1;
then r.1 = F.(d1,d9) by A5,FUNCOP_1:27;
hence thesis by A3,A4,FINSEQ_1:44;
end;
theorem
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
let F be Function of [:D,D9:],E;
let p be FinSequence of D such that
A1: p = <*d1,d2,d3*>;
A2: p.2 = d2 by A1;
reconsider r = F[:](p,d9) as FinSequence of E by Th81;
len p = 3 by A1,FINSEQ_1:45;
then
A3: len r = 3 by Th82;
then 2 in Seg len r;
then 2 in dom r by FINSEQ_1:def 3;
then
A4: r.2 = F.(d2,d9) by A2,FUNCOP_1:27;
A5: p.3 = d3 by A1;
A6: p.1 = d1 by A1;
3 in Seg len r by A3;
then 3 in dom r by FINSEQ_1:def 3;
then
A7: r.3 = F.(d3,d9) by A5,FUNCOP_1:27;
1 in Seg len r by A3;
then 1 in dom r by FINSEQ_1:def 3;
then r.1 = F.(d1,d9) by A6,FUNCOP_1:27;
hence thesis by A3,A4,A7,FINSEQ_1:45;
end;
:: Tuples
definition
let D be set;
mode FinSequenceSet of D -> set means
:Def3:
a in it implies a is FinSequence of D;
existence
proof
take D*;
thus thesis by FINSEQ_1:def 11;
end;
end;
definition
let D be set, S be FinSequenceSet of D;
redefine mode Element of S -> FinSequence of D; :: redefines Element (SUBSET_1, definition)
coherence
proof
per cases;
suppose S is non empty;
hence thesis by Def3;
end;
suppose S is empty;
then S = <*>D;
hence thesis by SUBSET_1:def 1;
end;
end;
end;
registration
let D be set;
cluster non empty for FinSequenceSet of D;
existence
proof
{<*>D} is FinSequenceSet of D
proof
let a;
thus thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
theorem Th87:
for D being set holds D* is FinSequenceSet of D
proof
let D be set;
D* is FinSequenceSet of D
proof
let a;
thus thesis by FINSEQ_1:def 11;
end;
hence thesis;
end;
definition
let D be set;
redefine func D* -> FinSequenceSet of D; :: redefines * (FINSEQ_1, definition)
coherence by Th87;
end;
theorem
for D being set, D9 being FinSequenceSet of D holds D9 c= D*
proof
let D be set, D9 be FinSequenceSet of D;
let a be object;
assume a in D9;
then a is FinSequence of D by Def3;
hence thesis by FINSEQ_1:def 11;
end;
theorem
for D9 being Subset of D, S being FinSequenceSet of D9
holds S is FinSequenceSet of D
proof
let D9 be Subset of D, S be FinSequenceSet of D9;
S is FinSequenceSet of D
proof
let a;
assume a in S;
then reconsider p = a as FinSequence of D9 by Def3;
rng p c= D9 by FINSEQ_1:def 4;
then rng p c= D by XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
hence thesis;
end;
reserve s for Element of D*;
registration
let i be natural Number, D;
cluster i-element for FinSequence of D;
existence
proof
take i |-> the Element of D;
thus thesis by Th61;
end;
end;
definition
let i be natural Number, D be non empty set;
mode Tuple of i,D is i-element FinSequence of D;
end;
definition
let i be natural Number;
let D be set;
func i-tuples_on D -> FinSequenceSet of D equals
{ s where s is Element of D*: len s = i };
coherence
proof
now
let a;
assume a in { s where s is Element of D*: len s = i };
then ex s being Element of D* st s = a & len s = i;
hence a is FinSequence of D;
end;
hence thesis by Def3;
end;
end;
registration
let i be natural Number, D;
cluster i-tuples_on D -> non empty;
coherence
proof
set d = the Element of D;
i |-> d is FinSequence of D by Th61;
then reconsider S = i |-> d as Element of D* by FINSEQ_1:def 11;
len S = i by CARD_1:def 7;
then S in { s : len s = i };
hence thesis;
end;
end;
registration
let D;
let i be natural Number;
cluster -> i-element for Element of i-tuples_on D;
coherence
proof
let z be Element of i-tuples_on D;
z in { p9 where p9 is Element of D*: len p9 = i };
then ex p9 being Element of D* st p9 = z & len p9 = i;
hence len z = i;
end;
end;
theorem Th90:
for D be set, z being FinSequence of D holds
z is Element of (len z)-tuples_on D
proof
let D be set, z be FinSequence of D;
z is Element of D* by FINSEQ_1:def 11;
then z in { z9 where z9 is Element of D*: len z9 = len z};
hence thesis;
end;
theorem
for D being set holds i-tuples_on D = Funcs(Seg i,D)
proof let D be set;
now
reconsider j=i as Element of NAT by ORDINAL1:def 12;
let z be object;
thus z in i-tuples_on D implies z in Funcs(Seg i,D)
proof
assume z in i-tuples_on D;
then consider s being Element of D* such that
A1: z = s and
A2: len s = i;
A3: rng s c= D by FINSEQ_1:def 4;
dom s = Seg i by A2,FINSEQ_1:def 3;
hence thesis by A1,A3,FUNCT_2:def 2;
end;
assume z in Funcs(Seg i,D);
then consider p being Function such that
A4: z = p and
A5: dom p = Seg j and
A6: rng p c= D by FUNCT_2:def 2;
p is FinSequence by A5,FINSEQ_1:def 2;
then p is FinSequence of D by A6,FINSEQ_1:def 4;
then reconsider p as Element of D* by FINSEQ_1:def 11;
len p = i by A5,FINSEQ_1:def 3;
hence z in i-tuples_on D by A4;
end;
hence thesis by TARSKI:2;
end;
theorem
for D being set holds 0-tuples_on D = { <*>D }
proof
let D be set;
now
let z be object;
thus z in 0-tuples_on D implies z = <*>D
proof
assume z in 0-tuples_on D;
then ex s being Element of D* st z = s & len s = 0;
hence thesis;
end;
<*>D is Element of D* & len <*>D = 0 by FINSEQ_1:def 11;
hence z = <*>D implies z in 0-tuples_on D;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for z being Tuple of 0,D for t being Tuple of i, D
holds z^t = t & t^z = t by FINSEQ_1:34;
theorem Th94:
1-tuples_on D = the set of all <*d*>
proof
now
let x be object;
thus x in 1-tuples_on D implies x in the set of all <*d*>
proof
assume x in 1-tuples_on D;
then consider s such that
A1: x = s and
A2: len s = 1;
1 in Seg 1;
then 1 in dom s by A2,FINSEQ_1:def 3;
then reconsider d1 = s.1 as Element of D by Th9;
s = <*d1*> by A2,FINSEQ_1:40;
hence thesis by A1;
end;
assume x in the set of all <*d*>;
then consider d such that
A3: x = <*d*>;
len <*d*> = 1 & <*d*> is Element of D* by FINSEQ_1:40,def 11;
hence x in 1-tuples_on D by A3;
end;
hence thesis by TARSKI:2;
end;
Lm6:
for z being Tuple of i,D holds z in i-tuples_on D proof let z be Tuple of i,D;
A1: z is Element of D* by FINSEQ_1:def 11;
len z = i by CARD_1:def 7;
hence z in i-tuples_on D by A1;
end;
theorem Th95:
for z being Tuple of 1,D ex d st z = <*d*>
proof
let z be Tuple of 1,D;
z in 1-tuples_on D by Lm6;
then z in the set of all <*d*> by Th94;
hence thesis;
end;
theorem Th96:
<*d*> in 1-tuples_on D
proof
<*d*> in the set of all <*d1*>;
hence thesis by Th94;
end;
theorem Th97:
2-tuples_on D = the set of all <*d1,d2*>
proof
now
let x be object;
thus x in 2-tuples_on D implies x in the set of all <*d1,d2*>
proof
assume x in 2-tuples_on D;
then consider s such that
A1: x = s and
A2: len s = 2;
2 in Seg 2;
then
A3: 2 in dom s by A2,FINSEQ_1:def 3;
1 in Seg 2;
then 1 in dom s by A2,FINSEQ_1:def 3;
then reconsider d19 = s.1, d29 = s.2 as Element of D by A3,Th9;
s = <*d19,d29*> by A2,FINSEQ_1:44;
hence thesis by A1;
end;
assume x in the set of all <*d1,d2*>;
then consider d1,d2 such that
A4: x = <*d1,d2*>;
<*d1,d2*> is FinSequence of D by Th11;
then len <*d1,d2*> = 2 & <*d1,d2*> is Element of D* by FINSEQ_1:44,def 11;
hence x in 2-tuples_on D by A4;
end;
hence thesis by TARSKI:2;
end;
theorem
for z being Tuple of 2,D ex d1,d2 st z = <*d1,d2*>
proof
let z be Tuple of 2,D;
A1: z is Element of D* by FINSEQ_1:def 11;
len z = 2 by CARD_1:def 7;
then z in 2-tuples_on D by A1;
then z in the set of all <*d1,d2*> by Th97;
hence thesis;
end;
theorem Th99:
<*d1,d2*> in 2-tuples_on D
proof
<*d1,d2*> in the set of all
<*c1,c2*> where c1 is (Element of D), c2 is Element of D;
hence thesis by Th97;
end;
theorem Th100:
3-tuples_on D = the set of all <*d1,d2,d3*>
proof
now
let x be object;
thus x in 3-tuples_on D implies x in the set of all <*d1,d2,d3*>
proof
assume x in 3-tuples_on D;
then consider s such that
A1: x = s and
A2: len s = 3;
2 in Seg(3);
then
A3: 2 in dom s by A2,FINSEQ_1:def 3;
3 in Seg(3);
then
A4: 3 in dom s by A2,FINSEQ_1:def 3;
1 in Seg(3);
then 1 in dom s by A2,FINSEQ_1:def 3;
then reconsider d19 = s.1, d29 = s.2, d39 = s.3 as Element of D by A3,A4
,Th9;
s = <*d19,d29,d39*> by A2,FINSEQ_1:45;
hence thesis by A1;
end;
assume x in the set of all <*d1,d2,d3*>;
then consider d1,d2,d3 such that
A5: x = <*d1,d2,d3*>;
<*d1,d2,d3*> is FinSequence of D by Th12;
then len <*d1,d2,d3*> = 3 & <*d1,d2,d3*> is Element of D* by FINSEQ_1:45
,def 11;
hence x in 3-tuples_on D by A5;
end;
hence thesis by TARSKI:2;
end;
theorem
for z being Tuple of 3,D ex d1,d2,d3 st z = <*d1,d2,d3*>
proof
let z be Tuple of 3,D;
A1: z is Element of D* by FINSEQ_1:def 11;
len z = 3 by CARD_1:def 7;
then z in 3-tuples_on D by A1;
then z in the set of all <*d1,d2,d3*> by Th100;
hence thesis;
end;
theorem Th102:
<*d1,d2,d3*> in 3-tuples_on D
proof
<*d1,d2,d3*> in the set of all
<*c1,c2,c3*> where c1 is (Element of D),c2 is (Element
of D),c3 is Element of D ;
hence thesis by Th100;
end;
theorem Th103:
(i+j)-tuples_on D = the set of all z^t where z is Tuple of i,D,
t is Tuple of j,D
proof
set T = the set of all z^t where z is Tuple of i,D, t is Tuple of j,D;
now
let x be object;
thus x in (i+j)-tuples_on D implies x in T
proof
assume x in (i+j)-tuples_on D;
then consider s such that
A1: x = s and
A2: len s = i + j;
consider z,t being FinSequence of D such that
A3: len z = i & len t = j and
A4: s = z^t by A2,Th21;
z is Tuple of i,D & t is Tuple of j,D by A3,CARD_1:def 7;
hence thesis by A1,A4;
end;
assume x in T;
then consider z being Tuple of i,D, t being Tuple of j,D such that
A5: x = z^t;
len z = i & len t = j by CARD_1:def 7;
then
A6: len(z^t) = i+j by FINSEQ_1:22;
z^t is Element of D* by FINSEQ_1:def 11;
hence x in (i+j)-tuples_on D by A5,A6;
end;
hence thesis by TARSKI:2;
end;
theorem Th104:
for s being Tuple of i+j,D
ex z being Element of i-tuples_on D, t being Element of j-tuples_on D
st s = z^t
proof
let s be Tuple of i+j,D;
A1: s is Element of D* by FINSEQ_1:def 11;
len s = i+j by CARD_1:def 7;
then s in (i+j)-tuples_on D by A1;
then s in the set of all z^t where z is Tuple of i,D, t is Tuple of j,D
by Th103;
then consider z being Tuple of i,D, t being Tuple of j,D such that
A2: s = z^t;
reconsider z as Element of i-tuples_on D by Lm6;
reconsider t as Element of j-tuples_on D by Lm6;
s = z^t by A2;
hence thesis;
end;
theorem
for z being Tuple of i,D for t being Tuple of j,D holds
z^t is Tuple of i+j,D;
theorem
D* = union the set of all i-tuples_on D where i is Nat
proof
for a being object
holds a in D* iff a in union the set of all i-tuples_on D where i is Nat
proof let a be object;
thus a in D* implies a in union the set of all
i-tuples_on D where i is Nat
proof
assume a in D*;
then reconsider a as FinSequence of D by FINSEQ_1:def 11;
a is Element of (len a)-tuples_on D & (len a)-tuples_on D in the set of
all i
-tuples_on D where i is Nat by Th90;
hence thesis by TARSKI:def 4;
end;
assume a in union the set of all i-tuples_on D where i is Nat;
then consider Z being set such that
A1: a in Z and
A2: Z in the set of all i-tuples_on D where i is Nat
by TARSKI:def 4;
consider i being Nat such that
A3: Z = i-tuples_on D by A2;
ex s being Element of D* st s = a & len s = i by A1,A3;
hence thesis;
end;
hence thesis by TARSKI:2;
end;
theorem
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 let D9 be non empty Subset of D;
let z being Tuple of i,D9;
z is Tuple of i, D by Th22;
hence thesis by Lm6;
end;
Lm7:
for x being object holds
x in i-tuples_on A implies x is i-element FinSequence
proof let x be object;
assume x in i-tuples_on A;
then x in { s where s is Element of A*: len s = i };
then ex s being Element of A* st x = s & len s = i;
hence thesis by CARD_1:def 7;
end;
theorem
i-tuples_on D = j-tuples_on A implies i = j
proof
set f = i |-> the Element of D;
f is Tuple of i,D by Th61;
then
A1: f in i-tuples_on D by Lm6;
assume i-tuples_on D = j-tuples_on A;
then f in j-tuples_on A by A1;
then f is j-element by Lm7;
then len f = j;
hence thesis by CARD_1:def 7;
end;
theorem
idseq i is Element of i-tuples_on NAT
proof
idseq i is FinSequence of NAT & len idseq i = i by Th46,CARD_1:def 7;
hence thesis by Th90;
end;
theorem Th110:
i |-> d is Element of i-tuples_on D
proof
i |-> d is FinSequence of D & len(i |-> d) = i by Th61,CARD_1:def 7;
hence thesis by Lm6;
end;
theorem
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
let z be Tuple of i,D;
let f be Function of D,D9;
reconsider s = f*z as FinSequence of D9 by Th30;
len z = i by CARD_1:def 7;
then len s = i by Th31;
hence thesis by Th90;
end;
theorem Th112:
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
let z be Tuple of i,D;
let f be Function of Seg i,Seg i;
A1: len z = i by CARD_1:def 7;
then
A2: Seg i = dom z by FINSEQ_1:def 3;
then reconsider t = z*f as FinSequence of D by Th45;
assume rng f = Seg i;
then len t = len z by A2,Th40;
hence thesis by A1,Th90;
end;
theorem
for z being Tuple of i,D for f being Permutation of Seg i
holds z*f is Tuple of i,D
proof
let z be Tuple of i,D;
let f be Permutation of Seg i;
rng f = Seg i by FUNCT_2:def 3;
hence thesis by Th112;
end;
theorem
for z being Tuple of i,D for d holds (z^<*d*>).(i+1) = d
proof
let z be Tuple of i,D;
let d;
len z = i by CARD_1:def 7;
hence thesis by FINSEQ_1:42;
end;
theorem
for z being Tuple of i+1,D ex t being Element of i-tuples_on D, d
st z = t^<*d*>
proof
let z be Tuple of i+1,D;
consider t being Element of i-tuples_on D, s being Element of 1-tuples_on D
such that
A1: z = t^s by Th104;
ex d st s = <*d*> by Th95;
hence thesis by A1;
end;
theorem
for z being Tuple of i,D holds z*(idseq i) = z
proof
let z be Tuple of i,D;
len z = i by CARD_1:def 7;
hence thesis by Th52;
end;
theorem
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
let z1,z2 be Tuple of i,D;
len z2 = i by CARD_1:def 7;
then
A1: dom z2 = Seg i by FINSEQ_1:def 3;
len z1 = i by CARD_1:def 7;
then dom z1 = Seg i by FINSEQ_1:def 3;
hence thesis by A1;
end;
theorem
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
let F be Function of [:D,D9:],E;
let z1 be Tuple of i,D;
let z2 be Tuple of i,D9;
reconsider r = F.:(z1,z2) as FinSequence of E by Th68;
len z1 = i & len z2 = i by CARD_1:def 7;
then len r = i by Th70;
hence thesis by Th90;
end;
theorem
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
let F be Function of [:D,D9:],E;
let z be Tuple of i,D9;
reconsider r = F[;](d,z) as FinSequence of E by Th75;
len z = i by CARD_1:def 7;
then len r = i by Th76;
hence thesis by Th90;
end;
theorem
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
let F be Function of [:D,D9:],E;
let z be Tuple of i,D;
reconsider r = F[:](z,d9) as FinSequence of E by Th81;
len z = i by CARD_1:def 7;
then len r = i by Th82;
hence thesis by Th90;
end;
theorem
(i+j)|->x = (i|->x)^(j|->x)
proof
A0: j is Nat by TARSKI:1;
defpred P[Nat] means (i+$1)|->x = (i|->x)^($1|->x);
A1: for j be Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A2: (i+j)|->x = (i|->x)^(j|->x);
thus (i+(j+1))|->x = (i+j+1)|->x .= ((i+j)|->x) ^ <*x*> by Th58
.= (i|->x)^((j|->x) ^ <*x*>) by A2,FINSEQ_1:32
.= (i|->x)^((j+1)|->x) by Th58;
end;
(i+0)|->x = (i|->x)^{} by FINSEQ_1:34
.= (i|->x)^(0|->x);
then
A3: P[0];
for j be Nat holds P[j] from NAT_1:sch 2(A3,A1);
hence thesis by A0;
end;
:: Addendum, 2002.07.08
theorem
for i being natural Number, x being Tuple of i,D holds dom x = Seg i
proof
let i be natural Number;
let x be Tuple of i,D;
len x = i by CARD_1:def 7;
hence thesis by FINSEQ_1:def 3;
end;
theorem
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*>
proof
let f be Function;
let x,y be set;
assume that
A1: x in dom f and
A2: y in dom f;
reconsider D = dom f, E = rng f as non empty set by A1,FUNCT_1:3;
rng <*x,y*> = {x,y} by Lm1;
then rng <*x,y*> c= D by A1,A2,ZFMISC_1:32;
then reconsider p = <*x,y*> as FinSequence of D by FINSEQ_1:def 4;
reconsider g = f as Function of D,E by FUNCT_2:def 1,RELSET_1:4;
thus f*<*x,y*> = g*p .= <*f.x,f.y*> by Th34;
end;
theorem
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*>
proof
let f be Function;
let x,y,z be set;
assume that
A1: x in dom f and
A2: y in dom f & z in dom f;
reconsider D = dom f, E = rng f as non empty set by A1,FUNCT_1:3;
rng <*x,y,z*> = {x,y,z} by Lm2;
then
A3: rng <*x,y,z*> = {x,y} \/ {z} by ENUMSET1:3;
{x,y} c= D & {z} c= D by A1,A2,ZFMISC_1:31,32;
then rng <*x,y,z*> c= D by A3,XBOOLE_1:8;
then reconsider p = <*x,y,z*> as FinSequence of D by FINSEQ_1:def 4;
reconsider g = f as Function of D,E by FUNCT_2:def 1,RELSET_1:4;
thus f*<*x,y,z*> = g*p .= <*f.x,f.y,f.z*> by Th35;
end;
theorem
rng <*x1,x2*> = {x1,x2} by Lm1;
theorem
rng <*x1,x2,x3*> = {x1,x2,x3} by Lm2;
begin :: Addenda
:: from SCMFSA_7, 2005.11.21, A.T.
theorem
for p1,p2,q being FinSequence st p1 c= q & p2 c= q & len p1 = len p2
holds p1 = p2
proof
let p1,p2,q be FinSequence;
assume that
A1: p1 c= q and
A2: p2 c= q and
A3: len p1 = len p2;
reconsider i = len p1 as Element of NAT;
A4: dom p1 = Seg i & dom p2 = Seg i by A3,FINSEQ_1:def 3;
now
let j be Nat;
assume
A5: j in dom p1;
hence p1.j = q.j by A1,GRFUNC_1:2
.= p2.j by A2,A4,A5,GRFUNC_1:2;
end;
hence thesis by A4;
end;
:: from MODAL_1, 2007.03.14, A.T.
reserve m,n for Nat,
s,w for FinSequence of NAT;
theorem
for D being non empty set,
s being FinSequence of D st s <> {}
ex w being FinSequence of D, n being Element of D st s = <*n*>^w
proof
let D be non empty set,
s be FinSequence of D;
defpred P[FinSequence of D] means
$1 <> {} implies ex w being FinSequence of D,
n being Element of D st $1 = <*n*>^w;
A1: for s being FinSequence of D
for m being Element of D st P[s] holds P[s^<*m*>]
proof
let s be FinSequence of D;
let m be Element of D such that
A2: s <> {} implies ex w being FinSequence of D,
n be Element of D st s = <*n*>^w;
assume s^<*m*> <> {};
per cases;
suppose
A3: s = {};
reconsider w = <*> D as FinSequence of D;
take w, n = m;
thus s^<*m*> = <*m*> by A3,FINSEQ_1:34
.= <*n*>^w by FINSEQ_1:34;
end;
suppose
s <> {};
then consider w be FinSequence of D,
n be Element of D such that
A4: s = <*n*>^w by A2;
take w^<*m*>,n;
thus thesis by A4,FINSEQ_1:32;
end;
end;
A5: P[<*> D];
for p being FinSequence of D holds P[p] from IndSeqD(A5,A1);
hence thesis;
end;
:: Moved from AMISTD_2 by AK, 2008.02.02
registration
let D be set;
cluster -> functional for FinSequenceSet of D;
coherence by Def3;
end;
:: from FINSOP_1, 2009.05.23, AT
definition
let D; let n be natural Number; let d;
redefine func n |-> d -> Element of n-tuples_on D; :: redefines |-> (FINSEQ_2, definition)
coherence by Th110;
end;
:: new, 2009.08.15, A.T.
theorem
for z being set holds z is Tuple of i,D iff z in i-tuples_on D
proof let z be set;
thus z is Tuple of i,D implies z in i-tuples_on D by Lm6;
assume z in i-tuples_on D;
then ex s being Element of D* st z = s & len s = i;
hence z is Tuple of i,D by CARD_1:def 7;
end;
:: from CATALG_1, 2009.09.08, A.T.
theorem Th130:
for A being set, i being Nat, p being FinSequence
holds p in i-tuples_on A iff len p = i & rng p c= A
proof
let A be set, i be Nat, p be FinSequence;
hereby
assume p in i-tuples_on A;
then ex q being Element of A* st p = q & len q = i;
hence len p = i & rng p c= A by FINSEQ_1:def 4;
end;
assume
A1: len p = i;
assume rng p c= A;
then p is FinSequence of A by FINSEQ_1:def 4;
then p in A* by FINSEQ_1:def 11;
hence thesis by A1;
end;
theorem
for A being set, i being Nat, p being FinSequence of
A holds p in i-tuples_on A iff len p = i
proof
let A be set, i be Nat, p be FinSequence of A;
rng p c= A by RELAT_1:def 19;
hence thesis by Th130;
end;
theorem
for A being set, i being Nat holds i-tuples_on A c= A*
proof
let A be set, i be Nat, x be object;
assume x in i-tuples_on A;
then x is FinSequence of A by Def3;
hence thesis by FINSEQ_1:def 11;
end;
theorem Th133:
for A being set, x being object holds
x in 1-tuples_on A iff ex a being set st a in A & x = <*a*>
proof
let A be set, x be object;
hereby
assume x in 1-tuples_on A;
then x in {s where s is Element of A*: len s = 1};
then consider s being Element of A* such that
A1: x = s and
A2: len s = 1;
take a = s.1;
A3: rng <*a*> = {a} & a in {a} by FINSEQ_1:39,TARSKI:def 1;
A4: rng s c= A by RELAT_1:def 19;
x = <*a*> by A1,A2,FINSEQ_1:40;
hence a in A & x = <*a*> by A1,A3,A4;
end;
given a being set such that
A5: a in A and
A6: x = <*a*>;
reconsider A as non empty set by A5;
reconsider a as Element of A by A5;
<*a*> is Element of 1-tuples_on A by Th96;
hence thesis by A6;
end;
theorem
for A being set, a being object st <*a*> in 1-tuples_on A holds a in A
proof
let A be set, a be object;
assume <*a*> in 1-tuples_on A;
then
A1: ex a9 being set st a9 in A & <*a*> = <*a9*> by Th133;
<*a*>.1 = a;
hence thesis by A1,FINSEQ_1:40;
end;
theorem Th135:
for A being set, x being object holds x in 2-tuples_on A iff
ex a,b being object st a in A & b in A & x = <*a,b*>
proof
let A be set, x be object;
hereby
assume x in 2-tuples_on A;
then x in {s where s is Element of A*: len s = 2};
then consider s being Element of A* such that
A1: x = s and
A2: len s = 2;
reconsider a = s.1, b = s.2 as object;
take a,b;
A3: rng <*a,b*> = {a,b} & a in {a,b} by Lm1,TARSKI:def 2;
A4: b in {a,b} & rng s c= A by RELAT_1:def 19,TARSKI:def 2;
x = <*a,b*> by A1,A2,FINSEQ_1:44;
hence a in A & b in A & x = <*a,b*> by A1,A3,A4;
end;
given a,b being object such that
A5: a in A and
A6: b in A and
A7: x = <*a,b*>;
reconsider A as non empty set by A5;
reconsider a,b as Element of A by A5,A6;
<*a,b*> is Element of 2-tuples_on A by Th99;
hence thesis by A7;
end;
theorem
for A being set, a,b being object st <*a,b*> in 2-tuples_on A
holds a in A & b in A
proof
let A be set, a,b be object;
assume <*a,b*> in 2-tuples_on A;
then
A1: ex a9,b9 being object st a9 in A & b9 in A & <*a,b*> = <*a9,b9*> by Th135;
<*a,b*>.1 = a & <*a,b*>.2 = b;
hence thesis by A1,FINSEQ_1:44;
end;
theorem Th137:
for A being set, x being object holds x in 3-tuples_on A iff
ex a,b,c being object st a in A & b in A & c in A & x = <*a,b,c*>
proof
let A be set, x be object;
hereby
assume x in 3-tuples_on A;
then x in {s where s is Element of A*: len s = 3};
then consider s being Element of A* such that
A1: x = s and
A2: len s = 3;
reconsider a = s.1, b = s.2, c = s.3 as object;
take a,b,c;
A3: rng <*a,b,c*> = {a,b,c} & a in {a,b,c} by Lm2,ENUMSET1:def 1;
A4: rng s c= A by RELAT_1:def 19;
A5: b in {a,b,c} & c in {a,b,c} by ENUMSET1:def 1;
x = <*a,b,c*> by A1,A2,FINSEQ_1:45;
hence a in A & b in A & c in A & x = <*a,b,c*> by A1,A3,A5,A4;
end;
given a,b,c being object such that
A6: a in A and
A7: b in A & c in A and
A8: x = <*a,b,c*>;
reconsider A as non empty set by A6;
reconsider a,b,c as Element of A by A6,A7;
<*a,b,c*> is Element of 3-tuples_on A by Th102;
hence thesis by A8;
end;
theorem
for A being set,a,b,c being object st <*a,b,c*> in 3-tuples_on A holds
a in A & b in A & c in A
proof
let A be set,a,b,c be object;
A1: <*a,b,c*>.3 = c;
assume <*a,b,c*> in 3-tuples_on A;
then
A2: ex a9,b9,c9 being object
st a9 in A & b9 in A & c9 in A & <*a,b,c*> = <*a9,
b9,c9*> by Th137;
<*a,b,c*>.1 = a & <*a,b,c*>.2 = b;
hence thesis by A2,A1,FINSEQ_1:45;
end;
theorem
for x being object holds
x in i-tuples_on A implies x is i-element FinSequence by Lm7;
:: from MSUALG_1, 2009.09.18, A.T.
theorem
for A being non empty set, n holds n-tuples_on A c= A*
proof
let A be non empty set, n;
defpred P[Element of A*] means len $1 = n;
{ s where s is Element of A*: P[s] } c= A* from FRAENKEL:sch 10;
hence thesis;
end;
:: from AMISTD_3, 2010.01.10, A.T.
theorem
n |-> x = m |-> x implies n = m
proof
len(n |-> x) = n by CARD_1:def 7;
hence thesis by CARD_1:def 7;
end;
:: from PBOOLE, 2011.04.17, A.T.
reserve i,j,e,u for set,
n for Nat;
definition
let I be set;
let M be ManySortedSet of I;
func M# -> ManySortedSet of I* means
:Def5:
for i being Element of I* holds it.i = product(M*i);
existence
proof
defpred P[object,object] means
ex j being Element of I* st j = $1 & $2 = product
(M*j);
A1: for i being object st i in I* ex j being object st P[i,j]
proof
let i be object;
assume i in I*;
then reconsider j = i as Element of I*;
reconsider e = product(M*j) as set;
take e,j;
thus thesis;
end;
consider f being ManySortedSet of I* such that
A2: for i being object st i in I* holds P[i,f.i] from PBOOLE:sch 3(A1);
take f;
let i be Element of I*;
ex j being Element of I* st j = i & f.i = product(M*j) by A2;
hence thesis;
end;
uniqueness
proof
let N1,N2 be ManySortedSet of I* such that
A3: for i being Element of I* holds N1.i = product(M*i) and
A4: for i being Element of I* holds N2.i = product(M*i);
now
let i be object;
assume i in I*;
then reconsider e = i as Element of I*;
thus N1.i = product(M*e) by A3
.= N2.i by A4;
end;
hence thesis;
end;
end;
registration
let I be set;
let M be non-empty ManySortedSet of I;
cluster M# -> non-empty;
coherence
proof
M# is non-empty
proof
let i be object;
assume i in I*;
then reconsider f = i as Element of I*;
product(M*f) <> {};
hence thesis by Def5;
end;
hence thesis;
end;
end;
definition
let a be set;
func *-->a -> sequence of {a}* means
:Def6:
for n being Nat holds it.n = n |-> a;
existence
proof
defpred P[Element of NAT,set] means $2 = $1 |-> a;
A1: for x being Element of NAT ex y being Element of {a}* st P[x,y]
proof
let n be Element of NAT;
a is Element of {a} by TARSKI:def 1;
then n |-> a is FinSequence of {a} by Th61;
then reconsider u = n |-> a as Element of {a}* by FINSEQ_1:def 11;
take u;
thus thesis;
end;
consider f being sequence of {a}* such that
A2: for x being Element of NAT holds P[x,f.x] from FUNCT_2:sch 3(A1);
take f;
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
P[nn,f.nn] by A2;
hence thesis;
end;
uniqueness
proof
let f1,f2 be sequence of {a}* such that
A3: for n being Nat holds f1.n = n |-> a and
A4: for n being Nat holds f2.n = n |-> a;
now
let k be Element of NAT;
thus f1.k = k |-> a by A3
.= f2.k by A4;
end;
hence f1 = f2;
end;
end;
theorem Th142:
for a,b being set holds (a .--> b)*(n|->a) = n |-> b
proof
let a,b be set;
A1: now
let x be object;
hereby
assume x in dom (n |-> b);
then
A2: x in Seg n;
hence x in dom(n|->a);
dom(a .--> b) = {a} & (n|->a).x = a by A2,FUNCOP_1:7;
hence (n|->a).x in dom(a .--> b) by TARSKI:def 1;
end;
assume that
A3: x in dom(n|->a) and
(n|->a).x in dom(a .--> b);
x in Seg n by A3;
hence x in dom (n |-> b);
end;
now
let x be object;
A4: a in {a} by TARSKI:def 1;
assume x in dom (n |-> b);
then
A5: x in Seg n;
hence (n |-> b).x = b by FUNCOP_1:7
.= (a .--> b).a by A4,FUNCOP_1:7
.= (a .--> b).((n|->a).x) by A5,FUNCOP_1:7;
end;
hence thesis by A1,FUNCT_1:10;
end;
theorem
for a being set for M being ManySortedSet of {a} st M = a .--> D holds
(M#* *-->a).n = Funcs(Seg n, D)
proof
let a be set;
let M be ManySortedSet of {a} such that
A1: M = a .--> D;
a is Element of {a} by TARSKI:def 1;
then n |-> a is FinSequence of {a} by Th61;
then
A2: n |-> a in {a}* by FINSEQ_1:def 11;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
dom(*-->a) = NAT by FUNCT_2:def 1;
hence (M#* *-->a).n = M#.((*-->a).nn) by FUNCT_1:13
.= M#.(nn|->a) by Def6
.= product((a .--> D)*(n|->a)) by A1,A2,Def5
.= product(n |-> D) by Th142
.= Funcs(Seg n, D) by CARD_3:11;
end;
registration
let i be natural Number;
cluster i |-> 0 -> empty-yielding;
coherence;
end;
:: new, 2011.10.03, A.K.
registration
let D be set;
cluster -> FinSequence-membered for FinSequenceSet of D;
coherence
proof
let A be FinSequenceSet of D;
let x be object;
thus thesis by Def3;
end;
end;
definition
let D be set;
let F be FinSequenceSet of D, f be sequence of F, n be natural Number;
redefine func f.n -> FinSequence of D; :: redefines . (FUNCT_1, definition)
coherence
proof reconsider n as Element of NAT by ORDINAL1:def 12;
f.n is Element of F;
hence thesis;
end;
end;