Copyright (c) 1990 Association of Mizar Users
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;
definitions TARSKI, FINSEQ_1;
theorems TARSKI, ZFMISC_1, ENUMSET1, REAL_1, NAT_1, SQUARE_1, FUNCT_1,
FUNCT_2, FUNCT_3, FINSEQ_1, FUNCOP_1, EQREL_1, TREES_1, RELAT_1,
RELSET_1, ORDINAL2, XBOOLE_1, XCMPLX_1;
schemes FINSEQ_1, NAT_1;
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
min(i,j) is Nat & max(i,j) is Nat by SQUARE_1:38,49;
theorem Th2:
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:9;
hence thesis by SQUARE_1:def 1;
end;
theorem Th3:
i <= j implies max(0,i-j) = 0
proof assume i <= j;
then i-i <= j-i by REAL_1:49;
then 0 <= (j-i) by XCMPLX_1:14;
then -(j-i) <= -0 by REAL_1:50;
then i-j <= 0 by XCMPLX_1:143;
hence max(0,i-j) = 0 by SQUARE_1:def 2;
end;
theorem Th4:
j <= i implies max(0,i-j) = i-j
proof assume j <= i;
then j-j <= i-j by REAL_1:49;
then 0 <= i-j by XCMPLX_1:14;
hence max(0,i-j) = i-j by SQUARE_1:def 2;
end;
theorem
max(0,i-j) is Nat
proof
per cases;
suppose i <= j;
hence thesis by Th3;
suppose
A1: j <= i;
then i = j or j < i by REAL_1:def 5;
then i - j is Nat by EQREL_1:1,XCMPLX_1:14;
hence max(0,i-j) is Nat by A1,Th4;
end;
Lm1: Seg 3 = Seg(2+1) .= Seg 2 \/ {3} by FINSEQ_1:11
.= {1,2,3} by ENUMSET1:43,FINSEQ_1:4;
theorem Th6:
min(0,i) = 0 & min(i,0) = 0 & max(0,i) = i & max(i,0) = i
proof 0 <= i by NAT_1:18;
hence thesis by SQUARE_1:def 1,def 2;
end;
:: Non-empty Segments of Natural Numbers
canceled;
theorem
i in Seg (l+1) implies i in Seg l or i = l+1
proof assume i in Seg(l+1);
then 1 <= i & i <= l+1 by FINSEQ_1:3;
then 1 <= i & i <= l or i = l+1 by NAT_1:26;
hence i in Seg l or i = l+1 by FINSEQ_1:3;
end;
theorem
i in Seg l implies i in Seg(l+j)
proof l <= l+j by NAT_1:29; then Seg l c= Seg(l+j) by FINSEQ_1:7;
hence thesis;
end;
:: Additional propositions related to Finite Sequences
theorem Th10:
len p = i & len q = i & (for j st j in Seg i holds p.j = q.j)
implies p = q
proof assume that
A1: len p = i & len q = i and
A2: for j st j in Seg i holds p.j = q.j;
dom p = Seg i & dom q = Seg i by A1,FINSEQ_1:def 3;
hence thesis by A2,FINSEQ_1:17;
end;
theorem Th11:
b in rng p implies ex i st i in dom p & p.i = b
proof assume b in rng p;
then ex a st a in dom p & b = p.a by FUNCT_1:def 5;
hence thesis;
end;
canceled;
theorem Th13:
for D being set
for p being FinSequence of D st i in dom p holds p.i in D
proof let D be set;
let p be FinSequence of D;
assume i in dom p;
then p.i in rng p & rng p c= D by FINSEQ_1:def 4,FUNCT_1:def 5;
hence p.i in D;
end;
Lm2:
now let k such that
A1: k <> 0;
let w be Element of Seg k;
reconsider z=k as Nat by ORDINAL2:def 21;
Seg z is non empty Subset of NAT by A1,FINSEQ_1:5;
hence w in Seg k;
end;
theorem Th14:
for D being set holds
(for i 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 st i in dom p holds p.i in D;
let b; assume b in rng p;
then ex i st i in dom p & p.i = b by Th11;
hence thesis by A1;
end;
Lm3:
rng <*x1,x2*> = {x1,x2}
proof
thus rng<* x1,x2 *> = rng(<* x1 *> ^ <* x2 *>) by FINSEQ_1:def 9
.= rng<* x1 *> \/ rng <* x2 *> by FINSEQ_1:44
.= rng<* x1 *> \/ {x2} by FINSEQ_1:55
.= {x1} \/ {x2} by FINSEQ_1:56
.= {x1,x2} by ENUMSET1:41;
end;
theorem Th15:
<*d1,d2*> is FinSequence of D
proof rng <*d1,d2*> = {d1,d2} & d1 in D & d2 in D by Lm3;
hence thesis by FINSEQ_1:def 4;
end;
Lm4:
rng <*x1,x2,x3*> = {x1,x2,x3}
proof
thus rng <* x1,x2,x3 *> = rng(<* x1 *> ^ <* x2,x3 *>) by FINSEQ_1:60
.= rng<* x1 *> \/ rng <* x2,x3 *> by FINSEQ_1:44
.= {x1} \/ rng<* x2,x3 *> by FINSEQ_1:55
.= {x1} \/ {x2,x3} by Lm3
.= {x1,x2,x3} by ENUMSET1:42;
end;
theorem Th16:
<*d1,d2,d3*> is FinSequence of D
proof rng <*d1,d2,d3*> = {d1,d2,d3} & {d1,d2,d3} c= D by Lm4;
hence thesis by FINSEQ_1:def 4;
end;
canceled;
theorem Th18:
i in dom p implies i in dom(p^q)
proof assume i in dom p;
then i in dom p & dom p c= dom(p^q) by FINSEQ_1:39;
hence thesis;
end;
theorem Th19:
len(p^<*a*>) = len p + 1
proof len(p^<*a*>) = len p + len <*a*> by FINSEQ_1:35;
hence thesis by FINSEQ_1:56;
end;
theorem
p^<*a*> = q^<*b*> implies p = q & a = b
proof assume
A1: p^<*a*> = q^<*b*>;
len(p^<*a*>) = len p + 1 & len(q^<*b*>) = len q + 1 by Th19;
then len p = len q & (p^<*a*>).(len p + 1) = a & (q^<*b*>).(len q + 1) = b
by A1,FINSEQ_1:59,XCMPLX_1:2;
hence thesis by A1,FINSEQ_1:46;
end;
theorem Th21:
len p = i + 1 implies ex q,a st p = q^<*a*>
proof assume len p = i + 1; then p <> {} by FINSEQ_1:25;
hence thesis by FINSEQ_1:63;
end;
theorem Th22:
for p being FinSequence of D
st len p <> 0 ex q being (FinSequence of D),d st p = q^<*d*>
proof let p be FinSequence of D;
assume
A1: len p <> 0;
then p <> {} by FINSEQ_1:25;
then consider q being FinSequence,d being set such that
A2: p = q^<*d*> by FINSEQ_1:63;
A3: for i st i in dom q holds q.i in D
proof let i; assume i in dom q;
then p.i = q.i & i in dom p by A2,Th18,FINSEQ_1:def 7;
hence thesis by Th13;
end;
A4: len p in Seg len p by A1,FINSEQ_1:5;
len p = len q + 1 by A2,Th19;
then len p in dom p & p.(len p) = d by A2,A4,FINSEQ_1:59,def 3;
then d is Element of D & q is FinSequence of D by A3,Th13,Th14;
hence thesis by A2;
end;
theorem Th23:
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:7;
then dom p c= Seg i by FINSEQ_1:def 3;
hence p = q by A1,RELAT_1:97;
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:21;
case not i <= len p;
hence len q = len p by A1,Th23;
end;
hence thesis by SQUARE_1:def 1;
end;
theorem Th25:
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 p = r|(Seg i) as FinSequence by FINSEQ_1:19;
consider q being FinSequence such that
A2: r = p^q by TREES_1:3;
take p,q;
i <= len r by A1,NAT_1:29;
hence len p = i by FINSEQ_1:21;
then len(p^q) = i + len q by FINSEQ_1:35;
hence len q = j by A1,A2,XCMPLX_1:2;
thus thesis by A2;
end;
theorem Th26:
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
proof let r be FinSequence of D;
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 Th25;
p is FinSequence of D & q is FinSequence of D by A2,FINSEQ_1:50;
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 st j in Seg i() holds z.j = F(j)
proof
deffunc G(Nat) = F($1);
consider z being FinSequence such that
A1: len z = i() and
A2: for i st i in Seg i() holds z.i = G(i) from SeqLambda;
A3: Seg i() = dom z by A1,FINSEQ_1:def 3;
for j st j in Seg i() holds z.j in D()
proof let j; assume j in Seg i(); then z.j = F(j) by A2;
hence z.j in D();
end;
then z is FinSequence of D() by A3,Th14;
hence thesis by A1,A2;
end;
scheme IndSeqD{D()->non empty 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: R[0] by A1,FINSEQ_1:32;
A4: for i st R[i] holds R[i+1]
proof let i such that
A5: for p being FinSequence of D() st len p = i holds P[p];
let p be FinSequence of D();
assume
A6: len p = i + 1;
then consider q being (FinSequence of D()), x being Element of D() such
that
A7: p = q^<*x*> by Th22;
len p = len q + 1 by A7,Th19;
then len q = i by A6,XCMPLX_1:2;
then P[q] by A5;
hence thesis by A2,A7;
end;
A8: for i holds R[i] from Ind(A3,A4);
let p be FinSequence of D();
len p = len p; hence thesis by A8;
end;
theorem Th27:
for D' being non empty Subset of D for p being FinSequence of D'
holds p is FinSequence of D
proof let D' be non empty Subset of D; let p be FinSequence of D';
rng p c= D' & D' c= D by FINSEQ_1:def 4;
hence rng p c= D by XBOOLE_1:1;
end;
theorem Th28:
for f being Function of Seg i, D holds f is FinSequence of D
proof let f be Function of Seg i, D;
dom f = Seg i by FUNCT_2:def 1;
then f is FinSequence & rng f c= D by FINSEQ_1:def 2,RELSET_1:12;
hence thesis by FINSEQ_1:def 4;
end;
canceled;
theorem
for p being FinSequence of D holds p is Function of dom p, D
proof let p be FinSequence of D;
dom p = dom p & rng p c= D by FINSEQ_1:def 4;
hence thesis by FUNCT_2:4;
end;
theorem
for f being Function of NAT,D holds f|(Seg i) is FinSequence of D
proof let f be Function of NAT,D;
f|(Seg i) is Function of Seg i, D by FUNCT_2:38;
hence thesis by Th28;
end;
theorem
for f being Function of NAT,D st q = f|(Seg i) holds len q = i
proof let f be Function of NAT,D;
f|(Seg i) is Function of Seg i, D by FUNCT_2:38;
then dom(f|(Seg i)) = Seg i by FUNCT_2:def 1;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th33:
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:46;
then dom(f*p) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th34:
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:7;
then rng q c= Seg i & Seg i c= dom p by A1,FINSEQ_1:def 3,def 4;
then rng q c= dom p by XBOOLE_1:1;
then dom (p*q) = dom q by RELAT_1:46;
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 D' for q being FinSequence of D st i <= len p
holds p*q is FinSequence of D'
proof assume
A1: D = Seg i;
let p be FinSequence of D'; let q be FinSequence of D;
assume i <= len p;
then reconsider pq = p*q as FinSequence by A1,Th34;
rng pq c= rng p & rng p c= D' by FINSEQ_1:def 4,RELAT_1:45;
then rng pq c= D' by XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th36:
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 = {} by RELSET_1:27;
then f*p = {} by RELAT_1:62;
then f*p =<*>D;
hence thesis;
suppose D <> {};
then dom f = A & rng p c= A & rng f c= D & rng(f*p) c= rng f
by FUNCT_2:def 1,RELAT_1:45,RELSET_1:12;
then f*p is FinSequence & rng(f*p) c= D by FINSEQ_1:20,XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th37:
for p being FinSequence of A for f being Function of A,D'
st q = f*p holds len q = len p
proof let p be FinSequence of A; let f be Function of A,D';
dom f = A & rng p c= A by FINSEQ_1:def 4,FUNCT_2:def 1;
hence thesis by Th33;
end;
theorem
for f being Function of A,D' holds f*(<*>A) = <*>D'
proof let f be Function of A,D';
reconsider q = f*(<*>A) as FinSequence of D' by Th36;
len(<*>A) = 0 by FINSEQ_1:32; then len q = 0 by Th37;
hence thesis by FINSEQ_1:32;
end;
theorem
for p being FinSequence of D for f being Function of D,D'
st p = <*x1*> holds f*p = <*f.x1*>
proof let p be FinSequence of D; let f be Function of D,D' such that
A1: p = <*x1*>;
reconsider q = f*p as FinSequence of D' by Th36;
len p = 1 by A1,FINSEQ_1:56;
then A2: len q = 1 by Th37;
then 1 in Seg len q by FINSEQ_1:4,TARSKI:def 1;
then 1 in dom q & p.1 = x1 by A1,FINSEQ_1:57,def 3;
then q.1 = f.x1 by FUNCT_1:22;
hence f*p = <*f.x1*> by A2,FINSEQ_1:57;
end;
theorem Th40:
for p being FinSequence of D for f being Function of D,D'
st p = <*x1,x2*> holds f*p = <*f.x1,f.x2*>
proof let p be FinSequence of D; let f be Function of D,D' such that
A1: p = <*x1,x2*>;
reconsider q = f*p as FinSequence of D' by Th36;
len p = 2 by A1,FINSEQ_1:61;
then A2: len q = 2 by Th37;
then 1 in Seg len q & 2 in Seg len q by FINSEQ_1:4,TARSKI:def 2;
then 1 in dom q & 2 in dom q & p.1 = x1 & p.2 = x2
by A1,FINSEQ_1:61,def 3;
then q.1 = f.x1 & q.2 = f.x2 by FUNCT_1:22;
hence f*p = <*f.x1,f.x2*> by A2,FINSEQ_1:61;
end;
theorem Th41:
for p being FinSequence of D for f being Function of D,D'
st p = <*x1,x2,x3*> holds f*p = <*f.x1,f.x2,f.x3*>
proof let p be FinSequence of D; let f be Function of D,D' such that
A1: p = <*x1,x2,x3*>;
reconsider q = f*p as FinSequence of D' by Th36;
len p = 3 by A1,FINSEQ_1:62;
then A2: len q = 3 by Th37;
then 1 in Seg len q & 2 in Seg len q & 3 in Seg len q by Lm1,ENUMSET1:14;
then 1 in dom q & 2 in dom q & 3 in dom q & p.1 = x1 & p.2 = x2 & p.3 = x3
by A1,FINSEQ_1:62,def 3;
then q.1 = f.x1 & q.2 = f.x2 & q.3 = f.x3 by FUNCT_1:22;
hence f*p = <*f.x1,f.x2,f.x3*> by A2,FINSEQ_1:62;
end;
theorem Th42:
for f being Function of Seg i,Seg j
st (j = 0 implies i = 0) & j <= len p holds p*f is FinSequence
proof let f be Function of Seg i,Seg j; assume
j = 0 implies i = 0;
then A1: Seg j = {} implies Seg i = {} by FINSEQ_1:5;
assume j <= len p;
then rng f c= Seg j & Seg j c= Seg len p by FINSEQ_1:7,RELSET_1:12;
then rng f c= Seg len p by XBOOLE_1:1;
then rng f c= dom p by FINSEQ_1:def 3;
then dom(p*f) = dom f & dom f = Seg i by A1,FUNCT_2:def 1,RELAT_1:46;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th43:
for f being Function of Seg i,Seg i st i <= len p holds p*f is FinSequence
proof let f be Function of Seg i,Seg i;
i = 0 implies i = 0; hence thesis by Th42;
end;
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 Th43;
end;
theorem Th45:
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:7;
then rng f c= dom p by FINSEQ_1:def 3;
then dom(p*f) = dom f & dom f = Seg i by FUNCT_2:67,RELAT_1:46;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th46:
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 Th45;
end;
theorem Th47:
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 Th45;
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 Th47;
end;
theorem Th49:
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:45;
then q is FinSequence & rng q c= D by A1,Th42,XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th50:
for p being FinSequence of D for f being Function of Seg i,Seg i
st i <= len p holds p*f is FinSequence of D
proof let p be FinSequence of D; let f be Function of Seg i,Seg i;
i = 0 implies i = 0; hence thesis by Th49;
end;
theorem Th51:
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 Th50;
end;
theorem Th52:
id Seg k is FinSequence of NAT
proof set I = id Seg k;
reconsider k as Nat by ORDINAL2:def 21;
dom I = Seg k & rng I = Seg k by RELAT_1:71;
then I is FinSequence & rng I c= NAT by FINSEQ_1:def 2;
hence thesis by FINSEQ_1:def 4;
end;
definition let i be natural number;
func idseq i -> FinSequence equals
:Def1: id Seg i;
coherence by Th52;
end;
canceled;
theorem Th54:
dom idseq k = Seg k
proof idseq k = id Seg k by Def1; hence thesis by RELAT_1:71; end;
theorem Th55:
len idseq k = k
proof
reconsider k as Nat by ORDINAL2:def 21;
dom idseq k = Seg k by Th54;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th56:
j in Seg i implies (idseq i).j = j
proof idseq i = id Seg i by Def1; hence thesis by FUNCT_1:35; end;
theorem
i<>0 implies for k being Element of Seg i holds (idseq i).k = k
proof assume
A1: i<>0;
let k be Element of Seg i;
k in Seg i by A1,Lm2;
hence thesis by Th56;
end;
theorem
idseq 0 = {}
proof len idseq 0 = 0 by Th55; hence thesis by FINSEQ_1:25; end;
theorem Th59:
idseq 1 = <*1*>
proof 1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
then len idseq 1 = 1 & (idseq 1).1 = 1 by Th55,Th56;
hence thesis by FINSEQ_1:57;
end;
theorem Th60:
idseq (i+1) = (idseq i) ^ <*i+1*>
proof set p = idseq (i+1);
A1: len p = i + 1 by Th55;
then consider q being FinSequence , a being set such that
A2: p = q^<*a*> by Th21;
A3: len p = len q + 1 by A2,Th19;
then A4: len q = i by A1,XCMPLX_1:2;
i+1 in Seg(i + 1) by FINSEQ_1:6;
then p.(i+1) = i+1 by Th56;
then A5: a = i+1 by A1,A2,A3,FINSEQ_1:59;
A6: dom q = Seg len q by FINSEQ_1:def 3;
for a st a in Seg i holds q.a = a
proof let a; assume
A7: a in Seg i;
then reconsider j = a as Nat;
i <= i+1 by NAT_1:29;
then Seg i c= Seg (i+1) by FINSEQ_1:7;
then j in Seg(i+1) & p.j = q.j by A2,A4,A6,A7,FINSEQ_1:def 7;
hence thesis by Th56;
end;
then q = id Seg i by A4,A6,FUNCT_1:34;
hence thesis by A2,A5,Def1;
end;
theorem Th61:
idseq 2 = <*1,2*>
proof
thus idseq 2 = idseq(1+1)
.= <*1*>^<*2*> by Th59,Th60
.= <*1,2*> by FINSEQ_1:def 9;
end;
theorem
idseq 3 = <*1,2,3*>
proof
thus idseq 3 = idseq(2+1)
.= <*1,2*>^<*3*> by Th60,Th61
.= <*1,2,3*> by FINSEQ_1:60;
end;
theorem
p*(idseq k) = p|(Seg k)
proof idseq k = id Seg k by Def1; hence thesis by RELAT_1:94; end;
theorem Th64:
len p <= k implies p*(idseq k) = p
proof assume
A1: len p <= k;
reconsider k as Nat by ORDINAL2:def 21;
dom p = Seg len p by FINSEQ_1:def 3;
then dom p c= Seg k & idseq k = id Seg k by A1,Def1,FINSEQ_1:7;
hence thesis by RELAT_1:77;
end;
theorem
idseq k is Permutation of Seg k
proof
id Seg k = idseq k by Def1;
hence thesis;
end;
theorem Th66:
(Seg k) --> a is FinSequence
proof set p = Seg k --> a;
reconsider k as Nat by ORDINAL2:def 21;
dom p = Seg k by FUNCOP_1:19;
hence p is FinSequence by FINSEQ_1:def 2;
end;
definition let i be natural number, a be set;
func i |-> a -> FinSequence equals
:Def2: Seg i --> a;
coherence by Th66;
end;
canceled;
theorem Th68:
dom(k |-> a) = Seg k
proof k |-> a = Seg k --> a by Def2;
hence dom(k |-> a) = Seg k by FUNCOP_1:19;
end;
theorem Th69:
len(k |-> a) = k
proof reconsider k as Nat by ORDINAL2:def 21;
dom(k |-> a) = Seg k by Th68; hence thesis by FINSEQ_1:def 3; end;
theorem Th70:
b in Seg k implies (k |-> a).b = a
proof k |-> a = Seg k --> a by Def2; hence thesis by FUNCOP_1:13; end;
theorem
k<>0 implies for w being Element of Seg k holds (k |-> d).w = d
proof assume
A1: k <> 0;
let w be Element of Seg k;
w in Seg k by A1,Lm2;
hence thesis by Th70;
end;
theorem Th72:
0 |-> a = {}
proof len(0 |-> a) = 0 by Th69; hence thesis by FINSEQ_1:25; end;
theorem Th73:
1 |-> a = <*a*>
proof 1 in Seg 1 by FINSEQ_1:5;
then len(1 |-> a) = 1 & (1 |-> a).1 = a by Th69,Th70;
hence thesis by FINSEQ_1:57;
end;
theorem Th74:
(i+1) |-> a = (i |-> a) ^ <*a*>
proof set p = (i+1) |-> a;
A1: len p = i + 1 by Th69;
then consider q being FinSequence , x being set such that
A2: p = q^<*x*> by Th21;
A3: len p = len q + 1 by A2,Th19;
then A4: len q = i by A1,XCMPLX_1:2;
i+1 in Seg(i + 1) by FINSEQ_1:6;
then A5: p.(i+1) = a by Th70;
now per cases;
suppose i = 0;
then q = {} & len (i |-> a) = 0 by A4,Th69,FINSEQ_1:25;
hence q = i |-> a by FINSEQ_1:25;
suppose
A6: i <> 0;
A7: dom q = Seg len q by FINSEQ_1:def 3;
then i in dom q by A4,A6,FINSEQ_1:5;
then q.i in rng q & Seg(i + 1) <> {} & p = Seg(i + 1) --> a
by Def2,FINSEQ_1:6,FUNCT_1:def 5;
then rng q <> {} & rng q c= rng p & rng p = {a}
by A2,FINSEQ_1:42,FUNCOP_1:14;
then rng q = {a} by ZFMISC_1:39;
then q = Seg i --> a by A4,A7,FUNCOP_1:15;
hence q = i |-> a by Def2;
end;
hence thesis by A1,A2,A3,A5,FINSEQ_1:59;
end;
theorem Th75:
2 |-> a = <*a,a*>
proof
thus 2 |-> a = (1+1) |-> a
.= (1|->a)^<*a*> by Th74
.= <*a*>^<*a*> by Th73
.= <*a,a*> by FINSEQ_1:def 9;
end;
theorem
3 |-> a = <*a,a,a*>
proof
thus 3 |-> a = (2+1) |-> a
.= (2|->a)^<*a*> by Th74
.= <*a,a*>^<*a*> by Th75
.= <*a,a,a*> by FINSEQ_1:60;
end;
theorem Th77:
k |-> d is FinSequence of D
proof set s = k |-> d;
s = Seg k --> d & d in D by Def2;
then rng s c= {d} & {d} c= D by FUNCOP_1:19;
then rng s c= D by XBOOLE_1:1;
hence s is FinSequence of D by FINSEQ_1:def 4;
end;
Lm5:
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);
dom p = Seg len p & dom q = Seg len q & rng <:p,q:> c= [:rng p,rng q:]
by FINSEQ_1:def 3,FUNCT_3:71;
then dom <:p,q:> = dom p /\ dom q & dom p /\ dom q = Seg i &
F.:(p,q) = F*<:p,q:> & rng <:p,q:> c= dom F
by A1,A2,Th2,FUNCOP_1:def 3,FUNCT_3:def 8,XBOOLE_1:1;
hence dom(F.:(p,q)) = Seg i by RELAT_1:46;
end;
theorem Th78:
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 Nat by SQUARE_1:38;
assume [:rng p,rng q:] c= dom F;
then dom(F.:(p,q)) = Seg k by Lm5;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th79:
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 Nat by SQUARE_1:38;
assume [:rng p,rng q:] c= dom F;
then dom(F.:(p,q)) = Seg k by Lm5;
hence thesis by FINSEQ_1:def 3;
end;
Lm6:
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;
rng q c= {a} by FUNCOP_1:19;
then rng <:q,p:> c= [:rng q,rng p:] & [:rng q,rng p:] c= [:{a},rng p:]
by FUNCT_3:71,ZFMISC_1:118;
then dom p = dom p & dom q = dom p & rng <:q,p:> c= [:{a},rng p:]
by FUNCOP_1:19,XBOOLE_1:1;
then dom <:q,p:> = dom p & F[;](a,p) = F*<:q,p:> & rng <:q,p:> c= dom F
by A1,FUNCOP_1:def 5,FUNCT_3:70,XBOOLE_1:1;
hence dom(F[;](a,p)) = dom p by RELAT_1:46;
end;
theorem Th80:
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 Lm6;
then dom(F[;](a,p)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th81:
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 Lm6;
then dom(F[;](a,p)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
Lm7:
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;
rng q c= {a} by FUNCOP_1:19;
then rng <:p,q:> c= [:rng p,rng q:] & [:rng p,rng q:] c= [:rng p,{a}:]
by FUNCT_3:71,ZFMISC_1:118;
then dom p = dom p & dom q = dom p & rng <:p,q:> c= [:rng p,{a}:]
by FUNCOP_1:19,XBOOLE_1:1;
then dom <:p,q:> = dom p & F[:](p,a) = F*<:p,q:> & rng <:p,q:> c= dom F
by A1,FUNCOP_1:def 4,FUNCT_3:70,XBOOLE_1:1;
hence dom(F[:](p,a)) = dom p by RELAT_1:46;
end;
theorem Th82:
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 Lm7;
then dom(F[:](p,a)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 2;
end;
theorem Th83:
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 Lm7;
then dom(F[:](p,a)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
theorem Th84:
for F being Function of [:D,D':],E
for p being FinSequence of D for q being FinSequence of D'
holds F.:(p,q) is FinSequence of E
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let q be FinSequence of D';
rng p c= D & rng q c= D' by FINSEQ_1:def 4;
then [:rng p,rng q:] c= [:D,D':] & F.:(p,q) = F*<:p,q:>
by FUNCOP_1:def 3,ZFMISC_1:119;
then [:rng p,rng q:] c= dom F & rng(F.:(p,q)) c= rng F & rng F c= E
by FUNCT_2:def 1,RELAT_1:45,RELSET_1:12;
then F.:(p,q) is FinSequence & rng(F.:(p,q)) c= E by Th78,XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th85:
for F being Function of [:D,D':],E
for p being FinSequence of D for q being FinSequence of D'
st r = F.:(p,q) holds len r = min(len p,len q)
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let q be FinSequence of D';
rng p c= D & rng q c= D' by FINSEQ_1:def 4;
then [:rng p,rng q:] c= [:D,D':] by ZFMISC_1:119;
then [:rng p,rng q:] c= dom F by FUNCT_2:def 1;
hence thesis by Th79;
end;
theorem Th86:
for F being Function of [:D,D':],E
for p being FinSequence of D for q being FinSequence of D'
st len p = len q & r = F.:(p,q) holds len r = len p & len r = len q
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let q be FinSequence of D';
assume
A1: len p = len q & r = F.:(p,q);
then len r = min(len p,len q) by Th85;
hence thesis by A1;
end;
theorem
for F being Function of [:D,D':],E
for p being FinSequence of D for p' being FinSequence of D'
holds F.:(<*>D,p') = <*>E & F.:(p,<*>D') = <*>E
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let p' be FinSequence of D';
reconsider r = F.:(<*>D,p'),r' = F.:(p,<*>D') as FinSequence of E by Th84;
len(<*>D) = 0 & len(<*>D') = 0 by FINSEQ_1:32;
then len r = min(0,len p') & len r' = min(len p,0) by Th85;
then len r = 0 & len r' = 0 by Th6;
hence thesis by FINSEQ_1:32;
end;
theorem
for F being Function of [:D,D':],E
for p being FinSequence of D for q being FinSequence of D'
st p = <*d1*> & q = <*d1'*> holds F.:(p,q) = <*F.(d1,d1')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let q be FinSequence of D' such that
A1: p = <*d1*> & q = <*d1'*>;
reconsider r = F.:(p,q) as FinSequence of E by Th84;
len p = 1 & len q = 1 by A1,FINSEQ_1:56;
then A2: len r = 1 by Th86;
then 1 in Seg len r by FINSEQ_1:4,TARSKI:def 1;
then 1 in dom r & p.1 = d1 & q.1 = d1' by A1,FINSEQ_1:57,def 3;
then r.1 = F.(d1,d1') by FUNCOP_1:28;
hence F.:(p,q) = <*F.(d1,d1')*> by A2,FINSEQ_1:57;
end;
theorem
for F being Function of [:D,D':],E
for p being FinSequence of D for q being FinSequence of D'
st p = <*d1,d2*> & q = <*d1',d2'*>
holds F.:(p,q) = <*F.(d1,d1'),F.(d2,d2')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let q be FinSequence of D' such that
A1: p = <*d1,d2*> & q = <*d1',d2'*>;
reconsider r = F.:(p,q) as FinSequence of E by Th84;
len p = 2 & len q = 2 by A1,FINSEQ_1:61;
then A2: len r = 2 by Th86;
then 1 in Seg len r & 2 in Seg len r by FINSEQ_1:4,TARSKI:def 2;
then 1 in dom r & 2 in dom r & p.1 = d1 & q.1 = d1' & p.2 = d2 & q.2 = d2'
by A1,FINSEQ_1:61,def 3;
then r.1 = F.(d1,d1') & r.2 = F.(d2,d2') by FUNCOP_1:28;
hence F.:(p,q) = <*F.(d1,d1'),F.(d2,d2')*> by A2,FINSEQ_1:61;
end;
theorem
for F being Function of [:D,D':],E
for p being FinSequence of D for q being FinSequence of D'
st p = <*d1,d2,d3*> & q = <*d1',d2',d3'*>
holds F.:(p,q) = <*F.(d1,d1'),F.(d2,d2'),F.(d3,d3')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D; let q be FinSequence of D' such that
A1: p = <*d1,d2,d3*> & q = <*d1',d2',d3'*>;
reconsider r = F.:(p,q) as FinSequence of E by Th84;
len p = 3 & len q = 3 by A1,FINSEQ_1:62;
then A2: len r = 3 by Th86;
then 1 in Seg len r & 2 in Seg len r & 3 in Seg len r by Lm1,ENUMSET1:14;
then 1 in dom r & 2 in dom r & 3 in dom r &
p.1 = d1 & q.1 = d1' & p.2 = d2 & q.2 = d2' & p.3 = d3 & q.3 = d3'
by A1,FINSEQ_1:62,def 3;
then r.1 = F.(d1,d1') & r.2 = F.(d2,d2') & r.3 = F.(d3,d3') by FUNCOP_1:28;
hence F.:(p,q) = <*F.(d1,d1'),F.(d2,d2'),F.(d3,d3')*> by A2,FINSEQ_1:62;
end;
theorem Th91:
for F being Function of [:D,D':],E for p being FinSequence of D'
holds F[;](d,p) is FinSequence of E
proof let F be Function of [:D,D':],E; let p be FinSequence of D';
{d} c= D & rng p c= D' by FINSEQ_1:def 4;
then [:{d},rng p:] c= [:D,D':] & F[;](d,p) = F * <:dom p --> d, p:>
by FUNCOP_1:def 5,ZFMISC_1:119;
then [:{d},rng p:] c= dom F & rng(F[;](d,p)) c= rng F & rng F c= E
by FUNCT_2:def 1,RELAT_1:45,RELSET_1:12;
then F[;](d,p) is FinSequence & rng(F[;](d,p)) c= E by Th80,XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th92:
for F being Function of [:D,D':],E for p being FinSequence of D'
st r = F[;](d,p) holds len r = len p
proof let F be Function of [:D,D':],E; let p be FinSequence of D';
{d} c= D & rng p c= D' by FINSEQ_1:def 4;
then [:{d},rng p:] c= [:D,D':] by ZFMISC_1:119;
then [:{d},rng p:] c= dom F by FUNCT_2:def 1;
hence thesis by Th81;
end;
theorem
for F being Function of [:D,D':],E holds F[;](d,<*>D') = <*>E
proof let F be Function of [:D,D':],E;
reconsider r = F[;](d,<*>D') as FinSequence of E by Th91;
len(<*>D') = 0 by FINSEQ_1:32;
then len r = 0 by Th92;
hence thesis by FINSEQ_1:32;
end;
theorem
for F being Function of [:D,D':],E for p being FinSequence of D'
st p = <*d1'*> holds F[;](d,p) = <*F.(d,d1')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D' such that
A1: p = <*d1'*>;
reconsider r = F[;](d,p) as FinSequence of E by Th91;
len p = 1 by A1,FINSEQ_1:56;
then A2: len r = 1 by Th92;
then 1 in Seg len r by FINSEQ_1:4,TARSKI:def 1;
then 1 in dom r & p.1 = d1' by A1,FINSEQ_1:57,def 3;
then r.1 = F.(d,d1') by FUNCOP_1:42;
hence thesis by A2,FINSEQ_1:57;
end;
theorem
for F being Function of [:D,D':],E for p being FinSequence of D'
st p = <*d1',d2'*> holds F[;](d,p) = <*F.(d,d1'),F.(d,d2')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D' such that
A1: p = <*d1',d2'*>;
reconsider r = F[;](d,p) as FinSequence of E by Th91;
len p = 2 by A1,FINSEQ_1:61;
then A2: len r = 2 by Th92;
then 1 in Seg len r & 2 in Seg len r by FINSEQ_1:4,TARSKI:def 2;
then 1 in dom r & 2 in dom r & p.1 = d1' & p.2 = d2'
by A1,FINSEQ_1:61,def 3;
then r.1 = F.(d,d1') & r.2 = F.(d,d2') by FUNCOP_1:42;
hence thesis by A2,FINSEQ_1:61;
end;
theorem
for F being Function of [:D,D':],E for p being FinSequence of D'
st p = <*d1',d2',d3'*>
holds F[;](d,p) = <*F.(d,d1'),F.(d,d2'),F.(d,d3')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D' such that
A1: p = <*d1',d2',d3'*>;
reconsider r = F[;](d,p) as FinSequence of E by Th91;
len p = 3 by A1,FINSEQ_1:62;
then A2: len r = 3 by Th92;
then 1 in Seg len r & 2 in Seg len r & 3 in Seg len r by Lm1,ENUMSET1:14;
then 1 in dom r & 2 in dom r & 3 in dom r & p.1 = d1' & p.2 = d2' & p.3 =
d3'
by A1,FINSEQ_1:62,def 3;
then r.1 = F.(d,d1') & r.2 = F.(d,d2') & r.3 = F.(d,d3') by FUNCOP_1:42;
hence thesis by A2,FINSEQ_1:62;
end;
theorem Th97:
for F being Function of [:D,D':],E for p being FinSequence of D
holds F[:](p,d') is FinSequence of E
proof let F be Function of [:D,D':],E; let p be FinSequence of D;
{d'} c= D' & rng p c= D by FINSEQ_1:def 4;
then [:rng p,{d'}:] c= [:D,D':] & F[:](p,d') = F * <:p,dom p --> d':>
by FUNCOP_1:def 4,ZFMISC_1:119;
then [:rng p,{d'}:] c= dom F & rng(F[:](p,d')) c= rng F & rng F c= E
by FUNCT_2:def 1,RELAT_1:45,RELSET_1:12;
then F[:](p,d') is FinSequence & rng(F[:](p,d')) c= E by Th82,XBOOLE_1:1;
hence thesis by FINSEQ_1:def 4;
end;
theorem Th98:
for F being Function of [:D,D':],E for p being FinSequence of D
st r = F[:](p,d') holds len r = len p
proof let F be Function of [:D,D':],E; let p be FinSequence of D;
{d'} c= D' & rng p c= D by FINSEQ_1:def 4;
then [:rng p,{d'}:] c= [:D,D':] by ZFMISC_1:119;
then [:rng p,{d'}:] c= dom F by FUNCT_2:def 1;
hence thesis by Th83;
end;
theorem
for F being Function of [:D,D':],E holds F[:](<*>D,d') = <*>E
proof let F be Function of [:D,D':],E;
reconsider r = F[:](<*>D,d') as FinSequence of E by Th97;
len(<*>D) = 0 by FINSEQ_1:32;
then len r = 0 by Th98;
hence thesis by FINSEQ_1:32;
end;
theorem
for F being Function of [:D,D':],E for p being FinSequence of D
st p = <*d1*> holds F[:](p,d') = <*F.(d1,d')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D such that
A1: p = <*d1*>;
reconsider r = F[:](p,d') as FinSequence of E by Th97;
len p = 1 by A1,FINSEQ_1:56;
then A2: len r = 1 by Th98;
then 1 in Seg len r by FINSEQ_1:4,TARSKI:def 1;
then 1 in dom r & p.1 = d1 by A1,FINSEQ_1:57,def 3;
then r.1 = F.(d1,d') by FUNCOP_1:35;
hence thesis by A2,FINSEQ_1:57;
end;
theorem
for F being Function of [:D,D':],E for p being FinSequence of D
st p = <*d1,d2*> holds F[:](p,d') = <*F.(d1,d'),F.(d2,d')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D such that
A1: p = <*d1,d2*>;
reconsider r = F[:](p,d') as FinSequence of E by Th97;
len p = 2 by A1,FINSEQ_1:61;
then A2: len r = 2 by Th98;
then 1 in Seg len r & 2 in Seg len r by FINSEQ_1:4,TARSKI:def 2;
then 1 in dom r & 2 in dom r & p.1 = d1 & p.2 = d2
by A1,FINSEQ_1:61,def 3;
then r.1 = F.(d1,d') & r.2 = F.(d2,d') by FUNCOP_1:35;
hence thesis by A2,FINSEQ_1:61;
end;
theorem
for F being Function of [:D,D':],E for p being FinSequence of D
st p = <*d1,d2,d3*> holds F[:](p,d') = <*F.(d1,d'),F.(d2,d'),F.(d3,d')*>
proof let F be Function of [:D,D':],E;
let p be FinSequence of D such that
A1: p = <*d1,d2,d3*>;
reconsider r = F[:](p,d') as FinSequence of E by Th97;
len p = 3 by A1,FINSEQ_1:62;
then A2: len r = 3 by Th98;
then 1 in Seg len r & 2 in Seg len r & 3 in Seg len r by Lm1,ENUMSET1:14;
then 1 in dom r & 2 in dom r & 3 in dom r & p.1 = d1 & p.2 = d2 & p.3 = d3
by A1,FINSEQ_1:62,def 3;
then r.1 = F.(d1,d') & r.2 = F.(d2,d') & r.3 = F.(d3,d') by FUNCOP_1:35;
hence thesis by A2,FINSEQ_1:62;
end;
:: T u p l e s
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;
cluster non empty FinSequenceSet of D;
existence
proof
{<*>D} is FinSequenceSet of D
proof let a;
thus thesis by TARSKI:def 1;
end;
hence thesis;
end;
end;
definition let D be set;
mode FinSequence-DOMAIN of D is non empty FinSequenceSet of D;
end;
canceled;
theorem Th104:
for D being set holds D* is FinSequence-DOMAIN 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* -> FinSequence-DOMAIN of D;
coherence by Th104;
end;
theorem
for D being set, D' being FinSequence-DOMAIN of D holds D' c= D*
proof let D be set, D' be FinSequence-DOMAIN of D;
let a; assume a in D';
then a is FinSequence of D by Def3;
hence a in D* by FINSEQ_1:def 11;
end;
definition let D be set, S be FinSequence-DOMAIN of D;
redefine mode Element of S -> FinSequence of D;
coherence by Def3;
end;
canceled;
theorem
for D' being non empty Subset of D, S being FinSequence-DOMAIN of D'
holds S is FinSequence-DOMAIN of D
proof let D' be non empty Subset of D, S be FinSequence-DOMAIN of D';
S is FinSequenceSet of D
proof
let a;
assume a in S;
then reconsider p = a as FinSequence of D' by Def3;
rng p c= D' & D' c= D by FINSEQ_1:def 4;
then rng p c= D by XBOOLE_1:1;
hence a is FinSequence of D by FINSEQ_1:def 4;
end;
hence thesis;
end;
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
:Def4: { 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;
definition let i be natural number, D;
cluster i-tuples_on D -> non empty;
coherence
proof consider d being Element of D;
i |-> d is FinSequence of D by Th77;
then reconsider S = i |-> d as Element of D* by FINSEQ_1:def 11;
len S = i by Th69;
then S in { s : len s = i };
hence thesis by Def4;
end;
end;
canceled;
theorem Th109:
for z being Element of i-tuples_on D holds len z = i
proof let z be Element of i-tuples_on D;
z in i-tuples_on D;
then z in { p' where p' is Element of D*: len p' = i } by Def4;
then ex p' being Element of D* st p' = z & len p' = i;
hence thesis;
end;
theorem Th110:
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 { z' where z' is Element of D*: len z' = len z};
hence thesis by Def4;
end;
theorem
i-tuples_on D = Funcs(Seg i,D)
proof
now let z be set;
thus z in i-tuples_on D implies z in Funcs(Seg i,D)
proof assume z in i-tuples_on D;
then z in { s : len s = i } by Def4;
then consider s such that
A1: z = s and
A2: len s = i;
dom s = Seg i & rng s c= D by A2,FINSEQ_1:def 3,def 4;
hence z in Funcs(Seg i,D) by A1,FUNCT_2:def 2;
end;
assume z in Funcs(Seg i,D);
then consider p being Function such that
A3: z = p and
A4: dom p = Seg i and
A5: rng p c= D by FUNCT_2:def 2;
p is FinSequence by A4,FINSEQ_1:def 2;
then p is FinSequence of D by A5,FINSEQ_1:def 4;
then reconsider p as Element of D* by FINSEQ_1:def 11;
len p = i & { s : len s = i } = i-tuples_on D by A4,Def4,FINSEQ_1:def 3;
hence z in i-tuples_on D by A3;
end;
hence thesis by TARSKI:2;
end;
theorem Th112:
for D being set holds 0-tuples_on D = { <*>D }
proof
let D be set;
now let z be set;
thus z in 0-tuples_on D implies z = <*>D
proof assume z in 0-tuples_on D;
then z in { s where s is Element of D*: len s = 0 } by Def4;
then ex s being Element of D* st z = s & len s = 0;
hence z = <*>D by FINSEQ_1:32;
end;
<*>D is Element of D* & len <*>D = 0 by FINSEQ_1:32,def 11;
then <*>D in { s where s is Element of D*: len s = 0 };
hence z = <*>D implies z in 0-tuples_on D by Def4;
end;
hence 0-tuples_on D = { <*>D } by TARSKI:def 1;
end;
theorem Th113:
for D be set, z being Element of 0-tuples_on D holds z = <*>D
proof let D be set, z be Element of 0-tuples_on D;
0-tuples_on D = { <*>D } by Th112;
hence z = <*>D by TARSKI:def 1;
end;
theorem
for D be set holds <*>D is Element of 0-tuples_on D
proof let D be set;
<*>D in { <*>D } by TARSKI:def 1;
hence thesis by Th112;
end;
theorem
for z being Element of 0-tuples_on D
for t being Element of i-tuples_on D holds z^t = t & t^z = t
proof let z be Element of 0-tuples_on D;
let t be Element of i-tuples_on D;
z = <*>D by Th113;
hence thesis by FINSEQ_1:47;
end;
theorem Th116:
1-tuples_on D = { <*d*>: not contradiction }
proof
A1: 1-tuples_on D = { s : len s = 1 } by Def4;
now let x be set;
thus x in 1-tuples_on D implies x in { <*d*>: not contradiction }
proof assume x in 1-tuples_on D;
then consider s such that
A2: x = s and
A3: len s = 1 by A1; 1 in Seg 1 by FINSEQ_1:5;
then 1 in dom s by A3,FINSEQ_1:def 3;
then reconsider d1 = s.1 as Element of D by Th13;
s = <*d1*> by A3,FINSEQ_1:57;
hence x in { <*d*>: not contradiction } by A2;
end;
assume x in { <*d*>: not contradiction };
then consider d such that
A4: x = <*d*>;
len <*d*> = 1 & <*d*> is Element of D* by FINSEQ_1:57,def 11;
hence x in 1-tuples_on D by A1,A4;
end;
hence thesis by TARSKI:2;
end;
theorem Th117:
for z being Element of 1-tuples_on D ex d st z = <*d*>
proof let z be Element of 1-tuples_on D;
z in 1-tuples_on D;
then z in { <*d*>: not contradiction } by Th116;
hence thesis;
end;
theorem
<*d*> is Element of 1-tuples_on D
proof <*d*> in { <*d1*>: not contradiction };
hence thesis by Th116;
end;
theorem Th119:
2-tuples_on D = { <*d1,d2*>: not contradiction }
proof
A1: 2-tuples_on D = { s : len s = 2 } by Def4;
now let x be set;
thus x in 2-tuples_on D implies x in { <*d1,d2*>: not contradiction }
proof assume x in 2-tuples_on D;
then consider s such that
A2: x = s and
A3: len s = 2 by A1;
1 in Seg 2 & 2 in Seg 2 by FINSEQ_1:4,TARSKI:def 2;
then 1 in dom s & 2 in dom s by A3,FINSEQ_1:def 3;
then reconsider d1' = s.1, d2' = s.2 as Element of D by Th13;
s = <*d1',d2'*> by A3,FINSEQ_1:61;
hence x in { <*d1,d2*>: not contradiction } by A2;
end;
assume x in { <*d1,d2*>: not contradiction };
then consider d1,d2 such that
A4: x = <*d1,d2*>;
<*d1,d2*> is FinSequence of D by Th15;
then len <*d1,d2*> = 2 & <*d1,d2*> is Element of D*
by FINSEQ_1:61,def 11;
hence x in 2-tuples_on D by A1,A4;
end;
hence thesis by TARSKI:2;
end;
theorem
for z being Element of 2-tuples_on D ex d1,d2 st z = <*d1,d2*>
proof let z be Element of 2-tuples_on D;
z in 2-tuples_on D;
then z in { <*d1,d2*>: not contradiction } by Th119;
hence thesis;
end;
theorem
<*d1,d2*> is Element of 2-tuples_on D
proof
<*d1,d2*> in
{ <*c1,c2*> where c1 is (Element of D), c2 is Element of D:
not contradiction };
hence thesis by Th119;
end;
theorem Th122:
3-tuples_on D = { <*d1,d2,d3*>: not contradiction }
proof
A1: 3-tuples_on D = { s : len s = 3 } by Def4;
now let x be set;
thus x in 3-tuples_on D implies x in { <*d1,d2,d3*>: not contradiction }
proof assume x in 3-tuples_on D;
then consider s such that
A2: x = s and
A3: len s = 3 by A1;
1 in Seg(3) & 2 in Seg(3) & 3 in Seg(3) by FINSEQ_1:3;
then 1 in dom s & 2 in dom s & 3 in dom s by A3,FINSEQ_1:def 3;
then reconsider d1' = s.1, d2' = s.2, d3' = s.3 as Element of D by Th13;
s = <*d1',d2',d3'*> by A3,FINSEQ_1:62;
hence x in { <*d1,d2,d3*>: not contradiction } by A2;
end;
assume x in { <*d1,d2,d3*>: not contradiction };
then consider d1,d2,d3 such that
A4: x = <*d1,d2,d3*>;
<*d1,d2,d3*> is FinSequence of D by Th16;
then len <*d1,d2,d3*> = 3 & <*d1,d2,d3*> is Element of D*
by FINSEQ_1:62,def 11;
hence x in 3-tuples_on D by A1,A4;
end;
hence thesis by TARSKI:2;
end;
theorem
for z being Element of 3-tuples_on D ex d1,d2,d3 st z = <*d1,d2,d3*>
proof let z be Element of 3-tuples_on D;
z in 3-tuples_on D;
then z in { <*d1,d2,d3*>: not contradiction } by Th122;
hence thesis;
end;
theorem
<*d1,d2,d3*> is Element of 3-tuples_on D
proof
<*d1,d2,d3*> in
{ <*c1,c2,c3*>
where c1 is (Element of D),c2 is (Element of D),c3 is Element of D
: not contradiction };
hence thesis by Th122;
end;
theorem Th125:
(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}
proof
A1: (i+j)-tuples_on D = { s : len s = i+j } by Def4;
set T = {z^t where z is (Element of i-tuples_on D),
t is Element of j-tuples_on D: not contradiction};
now let x be set;
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
A2: x = s and
A3: len s = i + j by A1;
consider z,t being FinSequence of D such that
A4: len z = i & len t = j and
A5: s = z^t by A3,Th26;
z is Element of i-tuples_on D & t is Element of j-tuples_on D
by A4,Th110;
hence x in T by A2,A5;
end;
assume x in T;
then consider z being (Element of i-tuples_on D),
t being Element of j-tuples_on D such that
A6: x = z^t;
len z = i & len t = j & z^t in D* by Th109,FINSEQ_1:def 11;
then len(z^t) = i+j & z^t is Element of D* by FINSEQ_1:35;
hence x in (i+j)-tuples_on D by A1,A6;
end;
hence thesis by TARSKI:2;
end;
theorem Th126:
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
proof let s be Element of (i+j)-tuples_on D;
s in (i+j)-tuples_on D;
then s in {z^t where z is (Element of i-tuples_on D),
t is Element of j-tuples_on D: not contradiction}
by Th125;
hence thesis;
end;
theorem
for z being Element of i-tuples_on D for t being Element of j-tuples_on D
holds z^t is Element of (i+j)-tuples_on D
proof let z be Element of i-tuples_on D; let t be Element of j-tuples_on D;
z^t in {z'^t' where z' is (Element of i-tuples_on D),
t' is Element of j-tuples_on D: not contradiction};
hence thesis by Th125;
end;
theorem
D* = union {i-tuples_on D: not contradiction}
proof
a in D* iff a in union {i-tuples_on D: not contradiction}
proof
thus a in D* implies a in union {i-tuples_on D: not contradiction}
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 by Th110;
then (len a)-tuples_on D in {i-tuples_on D: not contradiction} &
a in (len a)-tuples_on D;
hence thesis by TARSKI:def 4;
end;
assume a in union {i-tuples_on D: not contradiction};
then consider Z being set such that
A1: a in Z and
A2: Z in {i-tuples_on D: not contradiction} by TARSKI:def 4;
consider i such that
A3: Z = i-tuples_on D by A2;
a is Element of i-tuples_on D by A1,A3;
hence thesis by FINSEQ_1:def 11;
end;
hence thesis by TARSKI:2;
end;
theorem
for D' being non empty Subset of D for z being Element of i-tuples_on D'
holds z is Element of i-tuples_on D
proof let D' be non empty Subset of D; let z be Element of i-tuples_on D';
z is FinSequence of D & len z = i by Th27,Th109;
hence thesis by Th110;
end;
theorem
i-tuples_on D = j-tuples_on D implies i = j
proof consider d;
i |-> d is FinSequence of D & len(i |-> d) = i by Th69,Th77;
then reconsider i_d = i |-> d as Element of i-tuples_on D by Th110;
assume i-tuples_on D = j-tuples_on D;
then len(i_d) = i & len(i_d) = j by Th109;
hence thesis;
end;
theorem
idseq i is Element of i-tuples_on NAT
proof idseq i = id Seg i by Def1;
then idseq i is FinSequence of NAT & len idseq i = i by Th52,Th55;
hence idseq i is Element of i-tuples_on NAT by Th110;
end;
theorem
i |-> d is Element of i-tuples_on D
proof i |-> d is FinSequence of D & len(i |-> d) = i by Th69,Th77;
hence thesis by Th110;
end;
theorem
for z being Element of i-tuples_on D for f being Function of D,D'
holds f*z is Element of i-tuples_on D'
proof let z be Element of i-tuples_on D; let f be Function of D,D';
reconsider s = f*z as FinSequence of D' by Th36;
len z = i by Th109; then len s = i by Th37;
hence thesis by Th110;
end;
theorem Th134:
for z being Element of i-tuples_on D for f being Function of Seg i,Seg i
st rng f = Seg i holds z*f is Element of i-tuples_on D
proof let z be Element of i-tuples_on D; let f be Function of Seg i,Seg i;
assume
A1: rng f = Seg i;
A2: len z = i by Th109;
then A3: Seg i = dom z by FINSEQ_1:def 3;
then reconsider t = z*f as FinSequence of D by Th51;
len t = len z by A1,A3,Th46;
hence thesis by A2,Th110;
end;
theorem
for z being Element of i-tuples_on D for f being Permutation of Seg i
holds z*f is Element of i-tuples_on D
proof let z be Element of i-tuples_on D; let f be Permutation of Seg i;
rng f = Seg i by FUNCT_2:def 3; hence thesis by Th134;
end;
theorem
for z being Element of i-tuples_on D for d holds (z^<*d*>).(i+1) = d
proof let z be Element of i-tuples_on D; let d;
len z = i by Th109;
hence (z^<*d*>).(i+1) = d by FINSEQ_1:59;
end;
theorem
for z being Element of (i+1)-tuples_on D
ex t being (Element of i-tuples_on D), d st z = t^<*d*>
proof let z be Element of (i+1)-tuples_on 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 Th126;
ex d st s = <*d*> by Th117;
hence thesis by A1;
end;
theorem
for z being Element of i-tuples_on D holds z*(idseq i) = z
proof let z be Element of i-tuples_on D;
len z = i by Th109;
hence thesis by Th64;
end;
theorem
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
proof let z1,z2 be Element of i-tuples_on D;
len z1 = i & len z2 = i by Th109;
hence thesis by Th10;
end;
theorem
for F being Function of [:D,D':],E
for z1 being Element of i-tuples_on D
for z2 being Element of i-tuples_on D'
holds F.:(z1,z2) is Element of i-tuples_on E
proof let F be Function of [:D,D':],E;
let z1 be Element of i-tuples_on D; let z2 be Element of i-tuples_on D';
reconsider r = F.:(z1,z2) as FinSequence of E by Th84;
len z1 = i & len z2 = i by Th109;
then len r = i by Th86;
hence thesis by Th110;
end;
theorem
for F being Function of [:D,D':],E for z being Element of i-tuples_on D'
holds F[;](d,z) is Element of i-tuples_on E
proof let F be Function of [:D,D':],E; let z be Element of i-tuples_on D';
reconsider r = F[;](d,z) as FinSequence of E by Th91;
len z = i by Th109;
then len r = i by Th92;
hence thesis by Th110;
end;
theorem
for F being Function of [:D,D':],E for z being Element of i-tuples_on D
holds F[:](z,d') is Element of i-tuples_on E
proof let F be Function of [:D,D':],E; let z be Element of i-tuples_on D;
reconsider r = F[:](z,d') as FinSequence of E by Th97;
len z = i by Th109;
then len r = i by Th98;
hence thesis by Th110;
end;
theorem
(i+j)|->x = (i|->x)^(j|->x)
proof
defpred P[Nat] means (i+$1)|->x = (i|->x)^($1|->x);
(i+0)|->x = (i|->x)^{} by FINSEQ_1:47
.= (i|->x)^(0|->x) by Th72; then
A1: P[0];
A2: for j st P[j] holds P[j+1]
proof let j such that
A3: (i+j)|->x = (i|->x)^(j|->x);
thus (i+(j+1))|->x = (i+j+1)|->x by XCMPLX_1:1
.= ((i+j)|->x) ^ <*x*> by Th74
.= (i|->x)^((j|->x) ^ <*x*>) by A3,FINSEQ_1:45
.= (i|->x)^((j+1)|->x) by Th74;
end;
for j holds P[j] from Ind(A1,A2);
hence thesis;
end;
:: Addendum, 2002.07.08
theorem
for i, D
for x being Element of i-tuples_on D
holds dom x = Seg i
proof let i, D;
let x be Element of i-tuples_on D;
len x = i by Th109;
hence dom x = Seg i 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
A1: x in dom f & y in dom f;
then reconsider D = dom f, E = rng f as non empty set by FUNCT_1:12;
reconsider g = f as Function of D,E by FUNCT_2:def 1,RELSET_1:11;
rng <*x,y*> = {x,y} by Lm3;
then rng <*x,y*> c= D by A1,ZFMISC_1:38;
then reconsider p = <*x,y*> as FinSequence of D by FINSEQ_1:def 4;
thus f*<*x,y*> = g*p .= <*f.x,f.y*> by Th40;
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
A1: x in dom f & y in dom f & z in dom f;
then reconsider D = dom f, E = rng f as non empty set by FUNCT_1:12;
reconsider g = f as Function of D,E by FUNCT_2:def 1,RELSET_1:11;
rng <*x,y,z*> = {x,y,z} by Lm4;
then rng <*x,y,z*> = {x,y} \/ {z} & {x,y} c= D & {z} c= D
by A1,ENUMSET1:43,ZFMISC_1:37,38;
then rng <*x,y,z*> c= D by XBOOLE_1:8;
then reconsider p = <*x,y,z*> as FinSequence of D by FINSEQ_1:def 4;
thus f*<*x,y,z*> = g*p .= <*f.x,f.y,f.z*> by Th41;
end;
theorem
rng <*x1,x2*> = {x1,x2} by Lm3;
theorem
rng <*x1,x2,x3*> = {x1,x2,x3} by Lm4;