:: Segments of Natural Numbers and Finite Sequences
:: by Grzegorz Bancerek and Krzysztof Hryniewiecki
::
:: Received April 1, 1989
:: 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, FUNCT_1, SUBSET_1, XXREAL_0, TARSKI, XCMPLX_0,
XBOOLE_0, CARD_1, ARYTM_3, RELAT_1, FINSET_1, ZFMISC_1, ORDINAL1,
PARTFUN1, FUNCOP_1, ORDINAL4, ARYTM_1, FINSEQ_1, ORDINAL2, VALUED_0,
FUNCT_2, UPROOTS, INT_1, RAT_1, REAL_1, NUMBER09, MEMBERED, CARD_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1,
FUNCOP_1, WELLORD2, ORDINAL1, NAT_1, CARD_1, NUMBERS, PARTFUN1, FINSET_1,
CARD_3, XXREAL_0, XREAL_0, FUNCT_2, INT_1, VALUED_0, RAT_1, MEMBERED;
constructors WELLORD2, FUNCOP_1, FUNCT_4, XXREAL_0, XREAL_0, NAT_1, CARD_1,
RELSET_1, XCMPLX_0, INT_1, VALUED_0, NUMBERS, RAT_1, CARD_3, MEMBERED;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, CARD_1, NUMBERS, VALUED_0, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, FINSET_1, FUNCT_1, WELLORD2, XBOOLE_0, RELAT_1, CARD_1,
VALUED_0;
equalities ORDINAL1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, CARD_1;
theorems TARSKI, AXIOMS, FUNCT_1, NAT_1, ZFMISC_1, RELAT_1, RELSET_1,
WELLORD2, ORDINAL1, CARD_1, FINSET_1, XBOOLE_0, XBOOLE_1, FUNCOP_1,
XREAL_1, XXREAL_0, SETFAM_1, ORDINAL3, SUBSET_1, VALUED_0, XTUPLE_0,
FUNCT_2, CARD_2, ENUMSET1, GRFUNC_1, XREAL_0, NUMBERS, CARD_3;
schemes FUNCT_1, SUBSET_1, NAT_1, XBOOLE_0, RELAT_1, CLASSES1;
begin
reserve
a for natural Number,
k,l,m,n,k1,b,c,i for Nat,
x,y,z,y1,y2 for object,
X,Y for set,
f,g for Function;
:: Segments of Natural Numbers
definition
let n be natural Number;
func Seg n -> set equals
{ k where k is Nat: 1 <= k & k <= n };
correctness;
end;
definition
let n be Nat;
redefine func Seg n -> Subset of NAT; :: redefines Seg (FINSEQ_1, definition)
coherence
proof
set X = Seg n;
X c= NAT
proof
let x be object;
assume x in X;
then ex k being Nat st x = k & 1 <= k & k <= n;
hence thesis by ORDINAL1:def 12;
end;
hence thesis;
end;
end;
theorem Th1:
for a,b being natural Number holds a in Seg b iff 1 <= a & a <= b
proof
let a,b be natural Number;
A1: a is Nat & b is Nat by TARSKI:1;
a in { m where m is Nat: 1 <= m & m <= b } iff
ex m being Nat st a = m & 1 <= m & m <= b;
hence thesis by A1;
end;
registration let n be zero natural Number;
cluster Seg n -> empty;
coherence
proof
assume Seg n is not empty;
then consider x being object such that
A1: x in Seg n;
ex k being Nat st k = x & 1 <= k & k <= 0 by A1;
hence contradiction;
end;
end;
theorem Th2:
Seg 1 = { 1 } & Seg 2 = { 1,2 }
proof
now
let x be object;
thus x in Seg 1 implies x in { 1 }
proof
assume x in Seg 1;
then consider k being Nat such that
A1: x = k and
A2: 1 <= k & k <= 1;
k = 1 by A2,XXREAL_0:1;
hence thesis by A1,TARSKI:def 1;
end;
assume x in { 1 };
then x = 1 by TARSKI:def 1;
hence x in Seg 1;
end;
hence Seg 1 = { 1 } by TARSKI:2;
now
let x be object;
thus x in Seg 2 implies x in { 1,2 }
proof
assume x in Seg 2;
then consider k being Nat such that
A3: x = k and
A4: 1 <= k and
A5: k <= 2;
k <= 1 + 1 by A5;
then k = 1 or k = 2 by A4,NAT_1:9;
hence thesis by A3,TARSKI:def 2;
end;
assume x in { 1,2 };
then x = 1 or x = 2 by TARSKI:def 2;
hence x in Seg 2;
end;
hence thesis by TARSKI:2;
end;
theorem Th3:
for a being natural Number holds a = 0 or a in Seg a
proof
let a be natural Number;
assume a <> 0;
then ex b be Nat st a = b + 1 by NAT_1:6;
then a in NAT & 1 <= a by NAT_1:11;
hence thesis;
end;
registration let n be non zero natural Number;
cluster Seg n -> non empty;
coherence by Th3;
end;
theorem
for a being natural Number holds a+1 in Seg(a+1) by Th3;
theorem Th5:
for a,b being natural Number holds a <= b iff Seg a c= Seg b
proof
let a,b be natural Number;
thus a <= b implies Seg a c= Seg b
proof
assume
A1: a <= b;
let x be object;
assume x in Seg a;
then consider c being Nat such that
A3: x = c & 1 <= c & c <= a;
c <= b by A1,A3,XXREAL_0:2;
hence thesis by A3;
end;
assume
A4: Seg a c= Seg b;
now
assume a <> 0;
then a in Seg a by Th3;
hence thesis by A4,Th1;
end;
hence thesis;
end;
theorem Th6:
for a,b being natural Number holds Seg a = Seg b implies a = b
proof
let a,b be natural Number;
assume Seg a = Seg b;
then a <= b & b <= a by Th5;
hence thesis by XXREAL_0:1;
end;
theorem Th7:
for a,c being natural Number holds
c <= a implies Seg c = Seg a /\ Seg c by Th5,XBOOLE_1:28;
theorem
for a,c being natural Number holds
Seg c = Seg c /\ Seg a implies c <= a by Th6,Th7;
theorem Th9:
for a being natural Number holds Seg a \/ { a+1 } = Seg (a+1)
proof
let a be natural Number;
thus Seg a \/ { a+1 } c= Seg (a+1)
proof
a+0<=a+1 by XREAL_1:7;
then
A1: Seg a c= Seg(a+1) by Th5;
let x be object;
assume x in Seg a \/ { a+1 };
then x in Seg a or x in { a+1 } by XBOOLE_0:def 3;
then x in Seg (a+1) or x = a+1 by A1,TARSKI:def 1;
hence thesis by Th3;
end;
let x be object;
assume
A2: x in Seg (a+1);
then reconsider x as Element of NAT;
A3: x<=a+1 by A2,Th1;
A4: 1<=x by A2,Th1;
x<=a or x=a+1 by A3,NAT_1:8;
then x in Seg a or x in {a+1} by A4,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
theorem
for k being natural Number holds Seg k = Seg(k + 1) \ {k + 1}
proof
let k be natural Number;
A1: Seg(k + 1) = Seg k \/ {k + 1} by Th9;
Seg k misses {k + 1}
proof
assume
A2: not thesis;
set x = the Element of Seg k /\ {k + 1};
A3: x in Seg k by A2,XBOOLE_0:def 4;
x in {k + 1} by A2,XBOOLE_0:def 4;
then x = k + 1 by TARSKI:def 1;
hence thesis by A3,Th1,XREAL_1:29;
end;
hence thesis by A1,XBOOLE_1:88;
end;
:: Finite Sequences
definition
let IT be Relation;
attr IT is FinSequence-like means
:Def2:
ex n st dom IT = Seg n;
end;
registration
cluster empty -> FinSequence-like for Relation;
coherence
proof
let R be Relation;
assume
A1: R is empty;
take 0;
thus thesis by A1;
end;
end;
definition
mode FinSequence is FinSequence-like Function;
end;
reserve p,q,r,s,t for FinSequence;
defpred P[object,object] means ex k st $1 = k & $2 = k+1;
registration
let n be natural Number;
cluster Seg n -> finite;
coherence
proof
reconsider n as Nat by TARSKI:1;
Seg n is finite
proof
A1: n = { k where k is Nat: k < n } by AXIOMS:4;
A2: for x being object st x in n ex y being object st P[x,y]
proof
let x be object;
assume x in n;
then ex k being Nat st x = k & k < n by A1;
then reconsider k = x as Nat;
take k+1;
thus thesis;
end;
consider f such that
A3: dom f = n and
A4: for x being object st x in n holds P[x,f.x] from CLASSES1:sch 1(A2);
take f;
thus rng f = Seg n
proof
thus rng f c= Seg n
proof
let x be object;
assume x in rng f;
then consider y being object such that
A5: y in dom f and
A6: x = f.y by FUNCT_1:def 3;
consider k such that
A7: y = k and
A8: x = k+1 by A3,A4,A5,A6;
ex m being Nat st m = y & m < n by A1,A3,A5;
then 1 <= k+1 & k+1 <= n by A7,NAT_1:11,13;
hence thesis by A8;
end;
let x be object;
assume x in Seg n;
then consider k being Nat such that
A9: x = k and
A10: 1 <= k and
A11: k <= n;
consider i being Nat such that
A12: 1+i = k by A10,NAT_1:10;
i in NAT & i < n by A11,A12,NAT_1:13,ORDINAL1:def 12;
then
A13: i in n by A1;
then P[i,f.i] by A4;
hence thesis by A3,A9,A12,A13,FUNCT_1:def 3;
end;
thus thesis by A3,ORDINAL1:def 12;
end;
hence thesis;
end;
end;
registration
cluster FinSequence-like -> finite for Function;
coherence
proof
let f be Function;
given n such that
A1: dom f = Seg n;
rng f is finite by A1,FINSET_1:8;
then [:dom f, rng f:] is finite by A1;
hence thesis by FINSET_1:1,RELAT_1:7;
end;
end;
Lm1: Seg n,n are_equipotent
proof
defpred P[Nat] means Seg $1,$1 are_equipotent;
A1: P[0];
A2: for n st P[n] holds P[n+1]
proof
let n such that
A3: Seg n,n are_equipotent;
A4: Segm(n+1) = succ Segm n by NAT_1:38
.= n \/ { n };
A5: Seg(n+1) = Seg n \/ { n+1 } & { n+1 },{ n } are_equipotent
by Th9,CARD_1:28;
A6: now
assume n meets { n };
then consider x being object such that
A7: x in n and
A8: x in { n } by XBOOLE_0:3;
reconsider xx = x as set by TARSKI:1;
not xx in xx;
hence contradiction by A7,A8,TARSKI:def 1;
end;
now
assume Seg n meets { n+1 };
then consider x being object such that
A9: x in Seg n and
A10: x in { n+1 } by XBOOLE_0:3;
A11: x = n+1 by A10,TARSKI:def 1;
not n+1 <= n by NAT_1:13;
hence contradiction by A9,A11,Th1;
end;
hence thesis by A3,A4,A5,A6,CARD_1:31;
end;
for n holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
registration let n be natural Number;
cluster Seg n -> n-element;
coherence
proof
n is Nat by TARSKI:1;
hence thesis by Lm1,CARD_1:def 2;
end;
end;
notation
let p;
synonym len p for card p;
end;
definition
let p;
redefine func len p -> Element of NAT means :: redefines len (FINSEQ_1, synonym) → card (CARD_1, definition)
:Def3:
Seg it = dom p;
coherence
proof card p = card p;
hence thesis;
end;
compatibility
proof
let k be Element of NAT;
consider n such that
A1: dom p = Seg n by Def2;
dom p,p are_equipotent
proof
deffunc F(object) = [$1,p.$1];
consider g being Function such that
A2: dom g = dom p and
A3: for x being object st x in dom p holds g.x = F(x) from FUNCT_1:sch 3;
take g;
thus g is one-to-one
proof
let x,y be object;
assume that
A4: x in dom g and
A5: y in dom g;
assume g.x = g.y;
then [x,p.x] = g.y by A2,A3,A4
.= [y,p.y] by A2,A3,A5;
hence thesis by XTUPLE_0:1;
end;
thus dom g = dom p by A2;
thus rng g c= p
proof
let i be object;
assume i in rng g;
then consider x being object such that
A6: x in dom g and
A7: g.x = i by FUNCT_1:def 3;
g.x = [x,p.x] by A2,A3,A6;
hence thesis by A2,A6,A7,FUNCT_1:1;
end;
let x,y be object;
assume
A8: [x,y] in p; then
A9: x in dom p by FUNCT_1:1;
y = p.x by A8,FUNCT_1:1;
then g.x = [x,y] by A3,A8,FUNCT_1:1;
hence thesis by A2,A9,FUNCT_1:def 3;
end;
then
A10: card p = card dom p by CARD_1:5;
thus k = card p implies Seg k = dom p by A1,A10,Lm1,CARD_1:def 2;
assume Seg k = dom p;
hence k = card p by A10,Lm1,CARD_1:def 2;
end;
end;
definition
let p;
redefine func dom p -> Subset of NAT; :: redefines dom (RELAT_1, synonym) → proj1 (XTUPLE_0, definition)
coherence
proof dom p = Seg len p by Def3;
hence thesis;
end;
end;
theorem
(ex k st dom f c= Seg k) implies ex p st f c= p
proof
given k such that
A1: dom f c= Seg k;
deffunc F(object) = f.$1;
consider g such that
A2: dom g = Seg k &
for x being object st x in Seg k holds g.x = F(x) from FUNCT_1:sch 3;
reconsider g as FinSequence by A2,Def2;
take g;
let y,z be object;
assume
A3: [y,z] in f; then
A4: y in dom f by XTUPLE_0:def 12;
reconsider z as set by TARSKI:1;
A5: f.y = z by A3,FUNCT_1:def 2,A4;
[y,g.y] in g by A1,A2,A4,FUNCT_1:1;
hence thesis by A1,A2,A4,A5;
end;
scheme SeqEx{A()->Nat,P[object,object]}:
ex p st dom p = Seg A() & for k st k in Seg A() holds P[k,p.k]
provided
A1: for k st k in Seg A() ex x st P[k,x]
proof
A2: for x being object st x in Seg A() ex y being object st P[x,y]
by A1;
consider f being Function such that
A3: dom f = Seg A() &
for x being object st x in Seg A() holds P[x,f.x] from CLASSES1:sch 1(A2);
reconsider p=f as FinSequence by A3,Def2;
take p;
thus thesis by A3;
end;
scheme SeqLambda{A()->Nat,F(object) -> object}:
ex p being FinSequence st len p = A() & for k st k in dom p holds p.k=F(k)
proof
consider f being Function such that
A1: dom f = Seg A() &
for x being object st x in Seg A() holds f.x=F(x) from FUNCT_1:sch 3;
A2: A() in NAT by ORDINAL1:def 12;
reconsider p=f as FinSequence by A1,Def2;
take p;
thus thesis by A1,A2,Def3;
end;
theorem
z in p implies ex k st k in dom p & z = [k,p.k]
proof
assume
A1: z in p;
then consider x,y being object such that
A2: z=[x,y] by RELAT_1:def 1;
x in dom p by A1,A2,FUNCT_1:1;
then reconsider k = x as Nat;
take k;
thus thesis by A1,A2,FUNCT_1:1;
end;
theorem
dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p = q;
theorem Th14:
len p = len q & (for k st 1 <= k & k <= len p holds p.k = q.k) implies p = q
proof
assume that
A1: len p = len q and
A2: for k st 1<=k & k<=len p holds p.k = q.k;
A3: dom p = Seg len p by Def3;
now
let x be object;
assume
A5: x in dom p;
then reconsider k=x as Nat;
1 <= k & k <= len p by A3,A5,Th1;
hence p.x = q.x by A2;
end;
hence thesis by A1,A3,Def3;
end;
theorem Th15:
p|(Seg a) is FinSequence
proof
A0: a is Nat by TARSKI:1;
A1: dom(p|Seg a) = dom p /\ Seg a by RELAT_1:61
.= Seg len p /\ Seg a by Def3;
len p <= a or a <= len p;
then dom(p|Seg a) = Seg len p or dom(p|Seg a) = Seg a by A1,Th5,XBOOLE_1:28;
hence thesis by A0,Def2;
end;
theorem
rng p c= dom f implies f*p is FinSequence
proof
assume rng p c= dom f;
then dom(f*p) = dom p by RELAT_1:27
.= Seg len p by Def3;
hence thesis by Def2;
end;
theorem Th17:
a <= len p & q = p|(Seg a) implies len q = a & dom q = Seg a
proof
assume that
A1: a <= len p and
A2: q = p|(Seg a);
Seg a c= Seg len p by A1,Th5;
then Seg a c= dom p by Def3;
then a in NAT & dom q = Seg a by A2,ORDINAL1:def 12,RELAT_1:62;
hence thesis by Def3;
end;
:: ::
:: FinSequences of D ::
:: ::
definition
let D be set;
mode FinSequence of D -> FinSequence means
:Def4:
rng it c= D;
existence
proof
rng {} c= D;
hence thesis;
end;
end;
registration
let D be set;
cluster -> D-valued for FinSequence of D;
coherence
proof
let f be FinSequence of D;
thus rng f c= D by Def4;
end;
end;
Lm2: for D being set, f being FinSequence of D holds f is PartFunc of NAT,D
proof
let D be set, f be FinSequence of D;
dom f c= NAT & rng f c= D by Def4;
hence thesis by RELSET_1:4;
end;
registration
cluster empty -> FinSequence-like for Relation;
coherence;
end;
registration
let D be set;
cluster FinSequence-like for PartFunc of NAT,D;
existence
proof {} is PartFunc of NAT,D by RELSET_1:12;
hence thesis;
end;
end;
definition
let D be set;
redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D; :: redefines FinSequence (FINSEQ_1, definition)
coherence by Lm2;
end;
reserve D for set;
registration
let D;
cluster D-valued for FinSequence;
existence
proof
take the FinSequence of D;
thus thesis;
end;
end;
theorem Th18:
for p being D-valued FinSequence holds p|(Seg a) is FinSequence of D
proof
let p be D-valued FinSequence;
A1: p|(Seg a) is FinSequence by Th15;
rng(p|(Seg a)) c= rng p & rng p c= D by RELAT_1:70,def 19;
hence thesis by A1,Def4,XBOOLE_1:1;
end;
theorem
for D being non empty set ex p being FinSequence of D st len p = a
proof
let D be non empty set;
reconsider a as Element of NAT by ORDINAL1:def 12;
set y = the Element of D;
set p = Seg a --> y;
A1: dom p = Seg a by FUNCOP_1:13;
then reconsider p as FinSequence by Def2;
rng p c= {y} & {y} c= D by FUNCOP_1:13,ZFMISC_1:31;
then reconsider q=p as FinSequence of D by Def4,XBOOLE_1:1;
take q;
thus thesis by A1,Def3;
end;
:: ::
:: The Empty FinSequence ::
:: ::
Lm3: q = {} iff len q = 0;
theorem
p <> {} iff len p >= 1
proof
hereby
assume p <> {};
then len p+1 > 0+1 by XREAL_1:8;
hence len p >=1 by NAT_1:13;
end;
assume len p >= 1;
hence thesis;
end;
definition
let x be object;
func <*x*> -> set equals
{ [1,x] };
coherence;
end;
definition
let D be set;
func <*>D -> FinSequence of D equals
{};
coherence
proof
rng {} c= D;
hence thesis by Def4;
end;
end;
registration
let D be set;
cluster <*>D -> empty;
coherence;
end;
registration
let D be set;
cluster empty for FinSequence of D;
existence
proof
take <*>D;
thus thesis;
end;
end;
definition
let p,q;
func p^q -> FinSequence means
:Def7:
dom it = Seg (len p + len q) & (for k st k in dom p holds it.k = p.k) &
for k st k in dom q holds it.(len p + k) = q.k;
existence
proof
defpred P[object,object] means
(for k st k=$1 & 1 <= k & k <= len p holds $2=p.k) &
(for k st k=$1 & len p + 1 <= k & k <= len p + len q
holds $2=q.(k-len p));
A1: for x being object st x in Seg(len p + len q) ex y being object st P[x,y]
proof
let x be object;
assume x in Seg(len p + len q);
then reconsider m=x as Element of NAT;
A2: now
assume
A3: len p + 1 <= m;
set y = q.(m-len p);
A4: for k st k=x & 1 <= k & k <= len p holds y=p.k
proof
let k;
assume that
A5: k=x and 1 <= k and
A6: k <= len p;
m + (len p + 1) <= m + len p by A3,A5,A6,XREAL_1:7;
then m + len p + 1 <= m + len p + 0;
hence thesis by XREAL_1:6;
end;
for k st k=x & len p + 1 <= k & k <= len p + len q holds y=q.(k-len p);
hence thesis by A4;
end;
now
assume
A7: not len p + 1 <= m;
set y=p.m;
( for k st k=x & 1 <= k & k <= len p holds y=p.k)& for k st k=x & len p + 1 <=
k & k <= len p + len q holds y=q.(k-len p) by A7;
hence thesis;
end;
hence thesis by A2;
end;
consider f such that
A8: dom f = Seg(len p + len q) &
for x being object st x in Seg(len p + len q) holds P[x,f.x]
from CLASSES1:sch 1(A1);
A9: for k st k in dom p holds f.k=p.k
proof
let k;
assume k in dom p;
then
A10: k in Seg len p by Def3;
then
A11: 1 <= k & k <= len p by Th1;
Seg len p c= Seg(len p + len q) by Th5,NAT_1:11;
hence thesis by A8,A10,A11;
end;
A12: for n st n in dom q holds f.(len p+n)=q.n
proof
let n;
assume n in dom q; then
A13: n in Seg len q by Def3; then
1 <= n by Th1; then
A16: len p + 1 <= len p + n by XREAL_1:7;
n <= len q by A13,Th1; then
A17: len p + n <= len p + len q by XREAL_1:7;
len p + n <= len p + n + len p by NAT_1:11;
then len p + 1 <= len p + n + len p by A16,XXREAL_0:2;
then 1 <= len p + n by XREAL_1:6;
then (len p + n) in Seg (len p + len q) by A17;
then f.(len p + n)=q.(n + len p - len p) by A8,A16,A17;
hence thesis;
end;
reconsider r=f as FinSequence by A8,Def2;
take r;
thus thesis by A8,A9,A12;
end;
uniqueness
proof
let f,g be FinSequence such that
A18: dom f = Seg(len p + len q) and
A19: for k st k in dom p holds f.k=p.k and
A20: for k st k in dom q holds f.(len p + k)=q.k and
A21: dom g = Seg(len p + len q) and
A22: for k st k in dom p holds g.k=p.k and
A23: for k st k in dom q holds g.(len p + k)=q.k;
for x being object st x in Seg(len p + len q) holds f.x=g.x
proof
let x be object;
assume
A24: x in Seg(len p + len q);
then reconsider k=x as Element of NAT;
A25: 1 <= k by A24,Th1;
A26: now
assume len p + 1 <= k;
then consider m be Nat such that
A27: len p + 1 + m = k by NAT_1:10;
len p + (1 + m) <= len p + len q by A24,A27,Th1;
then 1+0<=1+m & 1 + m <= len q by XREAL_1:6;
then (1+m) in Seg len q;
then
A28: (1+m) in dom q by Def3;
then g.(len p +(1+m)) = q.(1+m) by A23;
hence thesis by A20,A27,A28;
end;
now
assume not len p + 1 <= k;
then k <= len p by NAT_1:8;
then k in Seg len p by A25;
then
A29: k in dom p by Def3;
then f.k=p.k by A19;
hence thesis by A22,A29;
end;
hence thesis by A26;
end;
hence thesis by A18,A21;
end;
end;
theorem Th21:
p = (p ^ q) | (dom p)
proof
A1: dom(p ^ q) = Seg(len p + len q) by Def7;
A2: dom p = Seg len p by Def3; then
A3: dom p = dom(p ^ q) /\ Seg len p by A1,Th7,NAT_1:12;
for x being object st x in dom p holds p.x = (p ^ q).x by Def7;
hence thesis by A2,A3,FUNCT_1:46;
end;
theorem Th22:
len(p^q) = len p + len q
proof
dom(p^q) = Seg(len p + len q) by Def7;
hence thesis by Def3;
end;
theorem Th23:
for k being Nat st
len p + 1 <= k & k <= len p + len q holds (p^q).k=q.(k-len p)
proof
let k be Nat;
assume that
A1: len p + 1 <= k and
A2: k <= len p + len q;
consider m be Nat such that
A3: (len p + 1)+m = k by A1,NAT_1:10;
A4: len p+(1+m) = k by A3;
1+m = k - len p by A3;
then
A5: 1 <= 1+m by A1,XREAL_1:19;
k-len p <= len q by A2,XREAL_1:20;
then 1+m in Seg len q by A3,A5;
then 1+m in dom q by Def3;
hence thesis by A4,Def7;
end;
theorem Th24:
for k being Nat st len p < k & k <= len(p^q) holds (p^q).k = q.(k - len p)
proof
let k be Nat;
assume len p < k & k <= len(p^q);
then len p + 1 <= k & k <= len p + len q by Th22,NAT_1:13;
hence thesis by Th23;
end;
theorem Th25:
for k being Nat st k in dom (p^q) holds
(k in dom p or ex n st n in dom q & k=len p + n )
proof
let k be Nat;
assume k in dom(p^q);
then
A1: k in Seg len (p^q) by Def3;
then
A2: k in Seg(len p + len q) by Th22;
A3: k in NAT & 1 <= k by A1,Th1;
A4: now
assume not len p+1 <= k;
then k <= len p by NAT_1:8;
then k in Seg len p by A3;
hence thesis by Def3;
end;
now
assume len p + 1 <= k;
then consider n be Nat such that
A5: k=len p + 1 + n by NAT_1:10;
len p + (1 + n) <= len p + len q by A2,A5,Th1;
then
A6: 1+n <= len q by XREAL_1:6;
1 <= 1+n by NAT_1:11;
then 1+n in Seg len q by A6;
then
A7: 1+n in dom q by Def3;
k=len p + (1+n) by A5;
hence thesis by A7;
end;
hence thesis by A4;
end;
theorem Th26:
dom p c= dom(p^q)
proof
Seg len p c= Seg(len p + len q) by Th5,NAT_1:11;
then Seg len p c= dom(p^q) by Def7;
hence thesis by Def3;
end;
theorem Th27:
x in dom q implies ex k st k=x & len p + k in dom(p^q)
proof
assume
A1: x in dom q;
then
A2: x in Seg len q by Def3;
reconsider k=x as Element of NAT by A1;
take k;
A3: 1 <= k by A2,Th1;
A4: k <= len q by A2,Th1;
k <= len p + k by NAT_1:11;
then
A5: 1 <= len p + k by A3,XXREAL_0:2;
len p + k <= len p + len q by A4,XREAL_1:7;
then len p + k in Seg(len p + len q) by A5;
hence thesis by Def7;
end;
theorem Th28:
k in dom q implies len p + k in dom(p^q)
proof
assume k in dom q;
then ex n st n=k & len p + n in dom(p^q) by Th27;
hence thesis;
end;
theorem Th29:
rng p c= rng(p^q)
proof
let x be object;
assume x in rng p;
then consider y being object such that
A1: y in dom p and
A2: x=p.y by FUNCT_1:def 3;
reconsider k=y as Element of NAT by A1;
A3: dom p c= dom(p^q) by Th26;
(p^q).k=p.k by A1,Def7;
hence x in rng(p^q) by A1,A2,A3,FUNCT_1:def 3;
end;
theorem Th30:
rng q c= rng(p^q)
proof
let x be object;
assume x in rng q;
then consider y being object such that
A1: y in dom q and
A2: x=q.y by FUNCT_1:def 3;
reconsider k=y as Element of NAT by A1;
len p + k in dom(p^q) & (p^q).(len p + k) = q.k by A1,Def7,Th28;
hence x in rng(p^q) by A2,FUNCT_1:def 3;
end;
theorem Th31:
rng(p^q) = rng p \/ rng q
proof
now
let x be object;
assume x in rng(p^q);
then consider y being object such that
A1: y in dom(p^q) and
A2: x=(p^q).y by FUNCT_1:def 3;
A3: y in Seg(len p + len q) by A1,Def7;
reconsider k=y as Element of NAT by A1;
A4: 1 <= k by A3,Th1;
A5: k <= len p + len q by A3,Th1;
A6: now
assume
A7: len p + 1 <= k;
then
A8: q.(k-len p) = x by A2,A5,Th23;
consider m be Nat such that
A9: (len p+1)+m = k by A7,NAT_1:10;
len p +(1+m) = k by A9;
then 1+0<=1+m & 1+m <= len q by A3,Th1,XREAL_1:6;
then 1+m in Seg len q;
then k-len p in dom q by A9,Def3;
hence x in rng q by A8,FUNCT_1:def 3;
end;
now
assume not len p + 1 <= k;
then k <= len p by NAT_1:8;
then k in Seg len p by A4;
then
A10: k in dom p by Def3;
then p.k = x by A2,Def7;
hence x in rng p by A10,FUNCT_1:def 3;
end;
hence x in rng p \/ rng q by A6,XBOOLE_0:def 3;
end;
then
A11: rng(p^q) c= rng p \/ rng q;
rng p c= rng(p^q) & rng q c= rng(p^q) by Th29,Th30;
hence thesis by A11,XBOOLE_1:8;
end;
theorem Th32:
p^q^r = p^(q^r)
proof
A1: dom ((p^q)^r) = Seg(len (p^q) + len r) by Def7
.= Seg(len p + len q + len r) by Th22
.= Seg(len p + (len q + len r))
.= Seg(len p + len(q^r)) by Th22;
A2: for k st k in dom p holds ((p^q)^r).k=p.k
proof
let k;
assume
A3: k in dom p;
dom p c= dom(p^q) by Th26;
hence (p^q^r).k=(p^q).k by A3,Def7
.=p.k by A3,Def7;
end;
for k st k in dom(q^r) holds ((p^q)^r).(len p + k)=(q^r).k
proof
let k;
assume
A4: k in dom(q^r);
A5: now
assume
A6: k in dom q;
then (len p + k) in dom(p^q) by Th28;
hence (p^q^r).(len p + k) = (p^q).(len p + k) by Def7
.=q.k by A6,Def7
.=(q^r).k by A6,Def7;
end;
now
assume not k in dom q;
then consider n such that
A7: n in dom r and
A8: k=len q + n by A4,Th25;
thus (p^q^r).(len p + k) =(p^q^r).(len p + len q + n) by A8
.=(p^q^r).(len(p^q) + n) by Th22
.=r.n by A7,Def7
.=(q^r).k by A7,A8,Def7;
end;
hence thesis by A5;
end;
hence thesis by A1,A2,Def7;
end;
theorem
p^r = q^r or r^p = r^q implies p = q
proof
assume
A1: p^r = q^r or r^p = r^q;
A2: now
assume
A3: p^r = q^r;
then len p + len r = len(q^r) by Th22;
then len p + len r = len q + len r by Th22;
then
A4: dom p = Seg len q by Def3
.= dom q by Def3;
for k st k in dom p holds p.k=q.k
proof
let k;
assume
A5: k in dom p;
hence p.k=(q^r).k by A3,Def7
.=q.k by A4,A5,Def7;
end;
hence thesis by A4;
end;
now
assume
A6: r^p=r^q;
then len r + len p = len(r^q) by Th22
.=len r + len q by Th22;
then
A7: dom p = Seg len q by Def3
.= dom q by Def3;
for k st k in dom p holds p.k=q.k
proof
let k;
assume
A8: k in dom p;
hence p.k = (r^q).(len r + k) by A6,Def7
.= q.k by A7,A8,Def7;
end;
hence thesis by A7;
end;
hence thesis by A1,A2;
end;
theorem Th34:
p^{} = p & {}^p = p
proof
dom(p^{}) = Seg len (p^{}) by Def3
.= Seg (len p + len {}) by Th22
.= dom p by Def3;
hence p^{} = p by Def7;
A2: dom({}^p) = Seg len ({}^p) by Def3
.= Seg (len {} + len p) by Th22
.= dom p by Def3;
for k st k in dom p holds p.k = ({}^p).k
proof
let k;
assume
A3: k in dom p;
thus ({}^p).k =({}^p).(len {} + k) .=p.k by A3,Def7;
end;
hence {}^p=p by A2;
end;
theorem Th35:
p^q = {} implies p = {} & q = {}
proof
assume p^q={};
then 0 = len (p^q) .= len p + len q by Th22;
hence thesis;
end;
definition
let D be set;
let p,q be FinSequence of D;
redefine func p^q -> FinSequence of D; :: redefines ^ (FINSEQ_1, definition)
coherence
proof
A1: rng(p^q) = rng p \/ rng q & rng p c= D by RELAT_1:def 19,Th31;
rng q c= D by RELAT_1:def 19;
hence rng(p^q) c= D by A1,XBOOLE_1:8;
end;
end;
Lm4: for x1, y1 being object holds [x,y] in {[x1,y1]} implies x = x1 & y = y1
proof
let x1, y1 be object;
assume [x,y] in {[x1,y1]};
then [x,y] = [x1,y1] by TARSKI:def 1;
hence thesis by XTUPLE_0:1;
end;
definition
let x be object;
redefine func <*x*> -> Function means :: redefines <* (FINSEQ_1, definition)
:Def8:
dom it = Seg 1 & it.1 = x;
coherence;
compatibility
proof
let f be Function;
hereby
assume
A1: f = <*x*>;
hence dom f = Seg 1 by Th2,RELAT_1:9;
[1,x] in f by A1,TARSKI:def 1;
hence f.1 = x by FUNCT_1:1;
end;
assume that
A2: dom f = Seg 1 and
A3: f.1 = x;
reconsider g = { [1,f.1] } as Function;
for y,z being object holds [y,z] in f iff [y,z] in g
proof let y,z be object;
hereby
assume
A4: [y,z] in f;
then
A5: y in {1} by A2,Th2,XTUPLE_0:def 12;
A6: z in rng f by A4,XTUPLE_0:def 13;
A7: rng f = {f.1} by A2,Th2,FUNCT_1:4;
A8: y = 1 by A5,TARSKI:def 1;
z = f.1 by A6,A7,TARSKI:def 1;
hence [y,z] in g by A8,TARSKI:def 1;
end;
assume [y,z] in g;
then
A9: y = 1 & z = f.1 by Lm4;
1 in dom f by A2;
hence thesis by A9,FUNCT_1:def 2;
end;
hence thesis by A3,RELAT_1:def 2;
end;
end;
registration
let a be object;
reduce <*a*>.1 to a;
reducibility by Def8;
end;
registration
let x be object;
cluster <*x*> -> Function-like Relation-like;
coherence;
end;
registration
let x be object;
cluster <*x*> -> FinSequence-like;
coherence by Def8;
end;
theorem Th36:
p^q is D-valued FinSequence implies
p is FinSequence of D & q is FinSequence of D
proof
assume p^q is D-valued FinSequence;
then rng(p^q) c= D by RELAT_1:def 19;
then
A1: rng p \/ rng q c= D by Th31;
rng p c= rng p \/ rng q by XBOOLE_1:7;
hence p is FinSequence of D by Def4,A1,XBOOLE_1:1;
rng q c= rng p \/ rng q by XBOOLE_1:7;
hence thesis by Def4,A1,XBOOLE_1:1;
end;
definition
let x,y be object;
func <*x,y*> -> set equals
<*x*>^<*y*>;
correctness;
let z be object;
func <*x,y,z*> -> set equals
<*x*>^<*y*>^<*z*>;
correctness;
end;
registration
let x,y be object;
cluster <*x,y*> -> Function-like Relation-like;
coherence;
let z be object;
cluster <*x,y,z*> -> Function-like Relation-like;
coherence;
end;
registration
let x,y be object;
cluster <*x,y*> -> FinSequence-like;
coherence;
let z be object;
cluster <*x,y,z*> -> FinSequence-like;
coherence;
end;
theorem
for x being object holds <*x*> = { [1,x] };
theorem Th38:
for x being object holds p=<*x*> iff dom p = Seg 1 & rng p = {x}
proof let x be object;
thus p = <*x*> implies dom p = Seg 1 & rng p = {x}
proof
assume
A1: p = <*x*>;
hence dom p = Seg 1 by Def8;
rng p = {p.1} by A1,Def8,Th2,FUNCT_1:4;
hence thesis by A1;
end;
assume that
A2: dom p = Seg 1 and
A3: rng p = {x};
1 in dom p by A2;
then p.1 in {x} by A3,FUNCT_1:def 3;
then p.1 = x by TARSKI:def 1;
hence thesis by A2,Def8;
end;
theorem Th39:
for x being object holds p=<*x*> iff len p = 1 & rng p = {x}
proof let x be object;
len p = 1 iff dom p = Seg 1 by Def3;
hence thesis by Th38;
end;
theorem Th40:
for x being object holds p = <*x*> iff len p = 1 & p.1 = x
proof let x be object;
len p = 1 iff dom p = Seg 1 by Def3;
hence thesis by Def8;
end;
theorem
for x being object holds (<*x*>^p).1 = x
proof let x be object;
1 in Seg 1;
then 1 in dom <*x*> by Def8;
then (<*x*>^p).1 = <*x*>.1 by Def7;
hence thesis;
end;
theorem Th42:
for x being object holds (p^<*x*>).(len p + 1)=x
proof let x be object;
dom <*x*> = Seg 1 by Def8;
then 1 in dom <*x*>;
hence (p^<*x*>).(len p + 1) = <*x*>.1 by Def7
.=x;
end;
theorem
for x,y,z being object
holds <*x,y,z*>=<*x*>^<*y,z*> & <*x,y,z*>=<*x,y*>^<*z*> by Th32;
theorem Th44:
for x,y being object holds p = <*x,y*> iff len p = 2 & p.1=x & p.2=y
proof let x,y be object;
thus
p = <*x,y*> implies len p = 2 & p.1=x & p.2=y
proof
assume
A1: p=<*x,y*>;
hence len p = len <*x*> + len <*y*> by Th22
.= 1 + len <*y*> by Th39
.= 1 + 1 by Th39
.=2;
A2: 1 in {1} by TARSKI:def 1;
then 1 in dom <*x*> by Def8,Th2;
hence p.1 = <*x*>.1 by A1,Def7
.= x;
A3: 1 in dom <*y*> by A2,Def8,Th2;
thus p.2 = (<*x*>^<*y*>).(1+1) by A1
.= (<*x*>^<*y*>).(len <*x*> + 1) by Th39
.= <*y*>.1 by A3,Def7
.= y;
end;
assume that
A4: len p = 2 and
A5: p.1=x and
A6: p.2=y;
A7: dom p = Seg(1+1) by A4,Def3
.= Seg(len <*x*> + 1) by Th39
.= Seg(len <*x*> + len <*y*>) by Th39;
A8: for k st k in dom <*x*> holds p.k=<*x*>.k
proof
let k;
assume k in dom <*x*>;
then k in {1} by Def8,Th2;
then k=1 by TARSKI:def 1;
hence thesis by A5;
end;
for k st k in dom <*y*> holds p.((len <*x*>)+k)=<*y*>.k
proof
let k;
assume k in dom <*y*>;
then
A9: k in {1} by Def8,Th2;
thus p.((len <*x*>) + k) = p.(1+k) by Th39
.=p.(1+1) by A9,TARSKI:def 1
.=<*y*>.1 by A6
.= <*y*>.k by A9,TARSKI:def 1;
end;
hence thesis by A7,A8,Def7;
end;
registration
let a,b be object;
reduce <*a,b*>.1 to a;
reducibility by Th44;
reduce <*a,b*>.2 to b;
reducibility by Th44;
end;
theorem Th45:
for x,y,z being object
holds p = <*x,y,z*> iff len p = 3 & p.1 = x & p.2 = y & p.3 = z
proof let x,y,z be object;
thus p = <*x,y,z*> implies len p = 3 & p.1 = x & p.2 = y & p.3 = z
proof
assume
A1: p =<*x,y,z*>;
hence len p =len <*x,y*> + len <*z*> by Th22
.=2 + len <*z*> by Th44
.=2+1 by Th39
.=3;
A2: 1 in {1} by TARSKI:def 1;
then
A3: 1 in dom <*x*> by Def8,Th2;
thus p.1 = (<*x*>^<*y,z*>).1 by A1,Th32
.=<*x*>.1 by A3,Def7
.=x;
2 in Seg 2 & len <*x,y*> = 2 by Th44;
then 2 in dom <*x,y*> by Def3;
hence p.2 =<*x,y*>.2 by A1,Def7
.=y;
A4: 1 in dom <*z*> by A2,Def8,Th2;
thus p.3 = (<*x,y*>^<*z*>).(2+1) by A1
.=(<*x,y*>^<*z*>).(len (<*x,y*>) + 1) by Th44
.= <*z*>.1 by A4,Def7
.= z;
end;
assume that
A5: len p = 3 and
A6: p.1 = x and
A7: p.2 = y and
A8: p.3 = z;
A9: dom p = Seg(2+1) by A5,Def3
.= Seg((len <*x,y*>) + 1) by Th44
.= Seg((len <*x,y*>) + len <*z*>) by Th39;
A10: for k st k in dom <*x,y*> holds p.k=<*x,y*>.k
proof
let k such that
A11: k in dom <*x,y*>;
len <*x,y*> = 2 by Th44;
then
A12: k in Seg 2 by A11,Def3;
A13: k=1 implies p.k=<*x,y*>.k by A6;
k=2 implies p.k=<*x,y*>.k by A7;
hence thesis by A12,A13,Th2,TARSKI:def 2;
end;
for k st k in dom <*z*> holds p.( (len <*x,y*>) + k) = <*z*>.k
proof
let k;
assume k in dom <*z*>;
then k in {1} by Def8,Th2;
then
A14: k = 1 by TARSKI:def 1;
hence p.( (len <*x,y*>) + k) = p.(2+1) by Th44
.=<*z*>.k by A8,A14;
end;
hence thesis by A9,A10,Def7;
end;
registration
let a,b,c be object;
reduce <*a,b,c*>.1 to a;
reducibility by Th45;
reduce <*a,b,c*>.2 to b;
reducibility by Th45;
reduce <*a,b,c*>.3 to c;
reducibility by Th45;
end;
theorem Th46:
p <> {} implies ex q,x st p = q^<*x*>
proof
assume p <> {};
then consider n be Nat such that
A1: len p = n + 1 by NAT_1:6;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider q=p|Seg n as FinSequence by Th15;
take q;
take p.(len p);
A2: dom q = dom p /\ Seg n by RELAT_1:61
.= Seg len p /\ Seg n by Def3;
Seg n c= Seg len p by Th5,A1,NAT_1:11;
then
A3: dom q = Seg n by A2,XBOOLE_1:28;
A4: dom(q^<*p.(len p)*>) = Seg len (q^<*p.(len p)*>) by Def3
.= Seg(len q + len <*p.(len p)*>) by Th22
.= Seg(len q + 1) by Th39
.= Seg len p by A1,A3,Def3
.= dom p by Def3;
for x being object st x in dom p holds p.x = (q^<*p.(len p)*>).x
proof
let x be object;
assume
A5: x in dom p;
then reconsider k = x as Element of NAT;
k in Seg(n+1) by A1,A5,Def3;
then
A6: k in Seg n \/ {n+1} by Th9;
A7: now
assume
A8: k in Seg n;
hence p.k=q.k by A3,FUNCT_1:47
.=(q^<*p.(len p)*>).k by A3,A8,Def7;
end;
now
assume
A9: k in {n+1};
1 in Seg 1;
then
A10: 1 in dom <*p.(len p)*> by Def8;
thus (q^<*p.(len p)*>).k =(q^<*p.(len p)*>).(n+1) by A9,TARSKI:def 1
.=(q^<*p.(len p)*>).(len q + 1) by A3,Def3
.=<*p.(len p)*>.1 by A10,Def7
.=p.k by A1,A9,TARSKI:def 1;
end;
hence thesis by A6,A7,XBOOLE_0:def 3;
end;
hence q^<*p.(len p)*>=p by A4;
end;
definition
let D be non empty set;
let x be Element of D;
redefine func <*x*> -> FinSequence of D; :: redefines <* (FINSEQ_1, definition)
coherence
proof
let y be object;
assume y in rng <*x*>;
then y in {x} by Th39;
then y = x by TARSKI:def 1;
hence thesis;
end;
end;
:: scheme of induction for finite sequences ::
scheme IndSeq{P[FinSequence]}: for p holds P[p]
provided
A1: P[{}] and
A2: for p,x st P[p] holds P[p^<*x*>]
proof
let p;
defpred R[set] means for p st len p = $1 holds P[p];
consider X being Subset of REAL such that
A3: for x being Element of REAL holds x in X iff R[x] from SUBSET_1:sch 3;
for k holds k in X
proof
A4: 0 in REAL by XREAL_0:def 1;
defpred S[Nat] means $1 in X;
for q st len q = 0 holds P[q] by A1,Lm3;
then
A5: S[0] by A3,A4;
now
let n such that
A6: n in X;
A7: n+1 in REAL by NUMBERS:19;
now
let q;
assume
A8: len q = n+1;
then q <> {};
then consider r,x such that
A9: q=r^<*x*> by Th46;
len q = len r + len <*x*> by A9,Th22
.= len r + 1 by Th39;
hence P[q] by A2,A9,A3,A6,A8;
end;
hence n+1 in X by A3,A7;
end;
then
A10: for n st S[n] holds S[n+1];
thus for n holds S[n] from NAT_1:sch 2(A5,A10);
end;
then len p in X;
hence thesis by A3;
end;
theorem
for p,q,r,s being FinSequence st p^q = r^s & len p <= len r
ex t being FinSequence st p^t = r
proof
defpred S[FinSequence] means
for p,q,s st p^q=$1^s & len p <= len $1 holds ex t st p^t=$1;
A1: S[{}]
proof
let p,q,s;
assume that
p^q={}^s and
A2: len p <= len {};
take {};
thus p^{} = p by Th34
.= {} by A2;
end;
A3: for r,x st S[r] holds S[r^<*x*>]
proof
let r,x;
assume
A4: for p,q,s st p^q=r^s & len p <= len r ex t st p^t=r;
let p,q,s;
assume that
A5: p^q=(r^<*x*>)^s and
A6: len p <= len (r^<*x*>);
A7: now
assume len p = len(r^<*x*>);
then
A8: dom p = Seg len(r^<*x*>) by Def3
.= dom(r^<*x*>) by Def3;
A9: for k st k in dom p holds p.k=(r^<*x*>).k
proof
let k;
assume
A10: k in dom p;
hence p.k = (r^<*x*>^s).k by A5,Def7
.=(r^<*x*>).k by A8,A10,Def7;
end;
p^{} = p by Th34
.=r^<*x*> by A8,A9;
hence thesis;
end;
now
assume len p <> len(r^<*x*>);
then len p <> len r + len <*x*> by Th22;
then
A11: len p <> len r + 1 by Th39;
len p <= len r + len <*x*> by A6,Th22;
then
A12: len p <= len r + 1 by Th39;
p^q=r^(<*x*>^s) by A5,Th32;
then consider t being FinSequence such that
A13: p^t = r by A4,A11,A12,NAT_1:8;
p^(t^<*x*>) = r^<*x*> by A13,Th32;
hence thesis;
end;
hence thesis by A7;
end;
for r holds S[r] from IndSeq(A1,A3);
hence thesis;
end;
registration
cluster -> NAT-defined for FinSequence;
coherence
proof let f be FinSequence;
thus dom f c= NAT;
end;
end;
definition
let D be set;
func D* -> set means
:Def11:
x in it iff x is FinSequence of D;
existence
proof
defpred P[object] means $1 is FinSequence of D;
consider X such that
A1: for x being object holds x in X iff x in bool [:NAT,D:] & P[x]
from XBOOLE_0:sch 1;
take X;
let x;
thus x in X implies x is FinSequence of D by A1;
assume x is FinSequence of D;
then reconsider p = x as FinSequence of D;
p c= [:NAT,D:];
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be set such that
A2: x in D1 iff x is FinSequence of D and
A3: x in D2 iff x is FinSequence of D;
now
let x be object;
thus x in D1 implies x in D2
proof
assume x in D1;
then x is FinSequence of D by A2;
hence thesis by A3;
end;
assume x in D2;
then x is FinSequence of D by A3;
hence x in D1 by A2;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let D be set;
cluster D* -> non empty;
coherence
proof
set f = the FinSequence of D;
f in D* by Def11;
hence thesis;
end;
end;
theorem
rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q
proof
defpred P[FinSequence] means $1 is one-to-one implies
for q st rng $1 = rng q & q is one-to-one holds len $1 = len q;
A1: P[{}] by RELAT_1:41;
now
let p,x;
assume
A2: p is one-to-one implies
for q st rng p = rng q & q is one-to-one holds len p = len q;
assume
A3: p ^ <* x *> is one-to-one;
let q;
assume that
A4: rng(p ^ <* x *>) = rng q and
A5: q is one-to-one;
A6: rng(p ^ <* x *>) = rng p \/ rng<* x *> by Th31
.= rng p \/ {x} by Th38;
x in {x} by TARSKI:def 1;
then x in rng q by A4,A6,XBOOLE_0:def 3;
then consider y being object such that
A7: y in dom q and
A8: x = q.y by FUNCT_1:def 3;
A9: y in Seg(len q) by A7,Def3;
reconsider y as Element of NAT by A7;
A10: 1 <= y by A9,Th1;
then consider k be Nat such that
A11: 1 + k = y by NAT_1:10;
A12: y <= len q by A9,Th1;
then consider n be Nat such that
A13: y + n = len q by NAT_1:10;
reconsider k,n as Element of NAT by ORDINAL1:def 12;
reconsider q1 = q | (Seg k) as FinSequence by Th15;
defpred P[Nat,object] means $2 = q.(y + $1);
A14: for j being Nat st j in Seg n ex x st P[j,x];
consider q2 being FinSequence such that
A15: dom q2 = Seg n and
A16: for j being Nat st j in Seg n holds P[j,q2.j] from SeqEx(A14);
A17: k <= y by A11,NAT_1:12;
then
A18: k <= len q by A12,XXREAL_0:2;
then
A19: len q1 = k by Th17;
len(q1 ^ <* x *>) + len q2 = len q1 + len<* x *> + len q2 by Th22
.= k + 1 + len q2 by A19,Th39
.= len q by A11,A13,A15,Def3;
then
A20: dom q = Seg(len(q1 ^ <* x *>) + len q2) by Def3;
A21: rng(q1 ^ q2) = rng q \ {x}
proof
thus rng(q1 ^ q2) c= rng q \ {x}
proof
let z be object;
assume z in rng(q1 ^ q2);
then
A22: z in rng q1 \/ rng q2 by Th31;
A23: now
assume
A24: z in rng q1;
A25: rng
q1 = q .: (Seg k) & q .: (Seg k) c= rng q by RELAT_1:111,115;
consider y1 being object such that
A26: y1 in dom q1 and
A27: q1.y1 = z by A24,FUNCT_1:def 3;
A28: q1.y1 = q.y1 by A26,FUNCT_1:47;
A29: y1 in Seg(len q1) by A26,Def3;
reconsider y1 as Element of NAT by A26;
A30: y1 <= k by A19,A29,Th1;
A31: k < y by A11,XREAL_1:29;
Seg k c= Seg(len q) by A17,Th5,A12,XXREAL_0:2;
then dom q1 c= Seg(len q) by A18,Th17;
then dom q1 c= dom q by Def3;
then x <> z by A5,A7,A8,A26,A27,A28,A30,A31;
then not z in {x} by TARSKI:def 1;
hence thesis by A24,A25,XBOOLE_0:def 5;
end;
now
assume z in rng q2;
then consider y1 being object such that
A32: y1 in dom q2 and
A33: q2.y1 = z by FUNCT_1:def 3;
reconsider y1 as Element of NAT by A32;
A34: q2.y1 = q.(y + y1) by A15,A16,A32;
A35: 1 <= y + y1 by A10,NAT_1:12;
y1 <= n by A15,A32,Th1;
then y + y1 <= len q by A13,XREAL_1:7;
then y + y1 in Seg(len q) by A35;
then
A36: y + y1 in dom q by Def3;
then
A37: z in rng q by A33,A34,FUNCT_1:def 3;
y1 <> 0 by A15,A32,Th1;
then y <> y + y1;
then x <> z by A5,A7,A8,A33,A34,A36;
then not z in {x} by TARSKI:def 1;
hence thesis by A37,XBOOLE_0:def 5;
end;
hence thesis by A22,A23,XBOOLE_0:def 3;
end;
let z be object;
assume
A38: z in rng q \ {x};
then consider y1 being object such that
A39: y1 in dom q and
A40: z = q.y1 by FUNCT_1:def 3;
A41: y1 in Seg(len q) by A39,Def3;
reconsider y1 as Element of NAT by A39;
not z in {x} by A38,XBOOLE_0:def 5;
then
A42: y <> y1 by A8,A40,TARSKI:def 1;
A43: now
assume
A44: y < y1;
then consider j being Nat such that
A45: y1 = y + j by NAT_1:10;
A46: 1 <= j by A44,A45,NAT_1:19;
j <= n by A13,A41,A45,Th1,XREAL_1:6;
then
A47: j in Seg n by A46;
then z = q2.j by A16,A40,A45;
hence z in rng q2 by A15,A47,FUNCT_1:def 3;
end;
now
assume
A48: y1 < y;
A49: 1 <= y1 by A41,Th1;
y1 <= k by A11,A48,NAT_1:13;
then y1 in Seg k by A49;
then
A50: y1 in dom q1 by A18,Th17;
then q1.y1 = z by A40,FUNCT_1:47;
hence z in rng q1 by A50,FUNCT_1:def 3;
end;
then z in rng q1 \/ rng q2 by A42,A43,XBOOLE_0:def 3,XXREAL_0:1;
hence thesis by Th31;
end;
A51: p = (p ^ <* x *>) | (dom p) by Th21;
A52: rng p = rng(p ^ <* x *>) \ {x}
proof
thus rng p c= rng(p ^ <* x *>) \ {x}
proof
let z be object;
assume
A53: z in rng p;
A54: rng p c= rng(p ^ <* x *>) by A51,RELAT_1:70;
consider y1 being object such that
A55: y1 in dom p and
A56: p.y1 = z by A53,FUNCT_1:def 3;
A57: y1 in Seg(len p) by A55,Def3;
reconsider y1 as Element of NAT by A55;
A58: (p ^ <* x *>).(len p + 1) = x by Th42;
A59: (p ^ <* x *>).y1 = p.y1 by A51,A55,FUNCT_1:47;
A60: y1 <= len p by A57,Th1;
A61: len p < len p +1 by XREAL_1:29;
A62: 1 <= y1 by A57,Th1;
y1 <= len p + 1 by A60,A61,XXREAL_0:2;
then
A63: y1 in Seg(len p + 1) by A62;
A64: len p + 1 in Seg(len p + 1) by Th3;
A65: y1 in Seg(len p + len<* x *>) by A63,Th40;
A66: len p + 1 in Seg(len p + len<* x *>) by A64,Th40;
A67: y1 in dom(p ^ <* x *>) by A65,Def7;
len p + 1 in dom(p ^ <* x *>) by A66,Def7;
then x <> z by A3,A56,A58,A59,A60,A61,A67;
then not z in {x} by TARSKI:def 1;
hence thesis by A53,A54,XBOOLE_0:def 5;
end;
let z be object;
assume
A68: z in rng(p ^ <* x *>) \ {x};
then
A69: z in rng(p ^ <* x *>);
A70: not z in {x} by A68,XBOOLE_0:def 5;
z in rng p \/ rng<* x *> by A69,Th31;
then z in rng p or z in rng<* x *> by XBOOLE_0:def 3;
hence thesis by A70,Th38;
end;
A71: q1 ^ q2 is one-to-one
proof
let y1,y2 be object;
assume that
A72: y1 in dom(q1 ^ q2) & y2 in dom(q1 ^ q2) and
A73: (q1 ^ q2).y1 = (q1 ^ q2).y2;
reconsider m1 = y1, m2 = y2 as Element of NAT by A72;
A74: q1 is one-to-one by A5,FUNCT_1:52;
A75: now
assume
A76: m1 in dom q1 & m2 in dom q1;
then (q1 ^ q2).m1 = q1.m1 & (q1 ^ q2).m2 = q1.m2 by Def7;
hence thesis by A73,A74,A76;
end;
A77: now
assume
A78: m1 in dom q1;
given j being Nat such that
A79: j in dom q2 and
A80: m2 = len q1 + j;
A81: (q1 ^ q2).m2 = q2.j by A79,A80,Def7;
(q1 ^ q2).m1 = q1.m1 & q1.m1 = q.m1 by A78,Def7,FUNCT_1:47;
then
A82: q.m1 = q.(y + j) by A15,A16,A73,A79,A81;
1 <= j by A15,A79,Th1;
then
A83: 1 <= y + j by NAT_1:12;
j <= n by A15,A79,Th1;
then y + j <= len q by A13,XREAL_1:7;
then y + j in Seg(len q) by A83;
then
A84: y + j in dom q by Def3;
m1 in Seg k by A18,A78,Th17;
then
A85: m1 <= k by Th1;
k < y by A11,XREAL_1:29;
then
A86: m1 < y by A85,XXREAL_0:2;
dom q1 c= dom q & y <= y + j by NAT_1:12,RELAT_1:60;
hence thesis by A5,A78,A82,A84,A86;
end;
A87: now
assume
A88: m2 in dom q1;
given j be Nat such that
A89: j in dom q2 and
A90: m1 = len q1 + j;
A91: (q1 ^ q2).m1 = q2.j by A89,A90,Def7;
(q1 ^ q2).m2 = q1.m2 & q1.m2 = q.m2 by A88,Def7,FUNCT_1:47;
then
A92: q.m2 = q.(y + j) by A15,A16,A73,A89,A91;
1 <= j by A15,A89,Th1;
then
A93: 1 <= y + j by NAT_1:12;
j <= n by A15,A89,Th1;
then y + j <= len q by A13,XREAL_1:7;
then y + j in Seg(len q) by A93;
then
A94: y + j in dom q by Def3;
m2 in Seg k by A18,A88,Th17;
then
A95: m2 <= k by Th1;
k < y by A11,XREAL_1:29;
then
A96: m2 < y by A95,XXREAL_0:2;
dom q1 c= dom q & y <= y + j by NAT_1:12,RELAT_1:60;
hence thesis by A5,A88,A92,A94,A96;
end;
now
given j1 being Nat such that
A97: j1 in dom q2 and
A98: m1 = len q1 + j1;
given j2 being Nat such that
A99: j2 in dom q2 and
A100: m2 = len q1 + j2;
A101: (q1 ^ q2).m1 = q2.j1 by A97,A98,Def7;
A102: (q1 ^ q2).m2 = q2.j2 by A99,A100,Def7;
A103: (q1 ^ q2).m1 = q.(y + j1) by A15,A16,A97,A101;
A104: (q1 ^ q2).m2 = q.(y + j2) by A15,A16,A99,A102;
A105: 1 <= j1 by A15,A97,Th1;
A106: 1 <= j2 by A15,A99,Th1;
A107: 1 <= y + j1 by A105,NAT_1:12;
A108: 1 <= y + j2 by A106,NAT_1:12;
A109: j1 <= n by A15,A97,Th1;
A110: j2 <= n by A15,A99,Th1;
A111: y + j1 <= len q by A13,A109,XREAL_1:7;
A112: y + j2 <= len q by A13,A110,XREAL_1:7;
A113: y + j1 in Seg(len q) by A107,A111;
A114: y + j2 in Seg(len q) by A108,A112;
A115: y + j1 in dom q by A113,Def3;
y + j2 in dom q by A114,Def3;
then y + j1 = y + j2 by A5,A73,A103,A104,A115;
hence thesis by A98,A100;
end;
hence thesis by A72,A75,A77,A87,Th25;
end;
A116: now
let j be Nat;
assume
A117: j in dom(q1 ^ <* x *>);
A118: now
assume
A119: j in dom q1;
then (q1 ^ <* x *>).j = q1.j by Def7;
hence q.j = (q1 ^ <* x *>).j by A119,FUNCT_1:47;
end;
now
given i be Nat such that
A120: i in dom<* x *> and
A121: j = len q1 + i;
i in {1} by A120,Th2,Th38;
then i = 1 by TARSKI:def 1;
hence q.j = (q1 ^ <* x *>).j by A8,A11,A19,A121,Th42;
end;
hence q.j = (q1 ^ <* x *>).j by A117,A118,Th25;
end;
now
let j be Nat;
assume j in dom q2;
hence q2.j = q.(len q1 + 1 + j) by A11,A15,A16,A19
.= q.(len q1 + len<* x *> + j) by Th39
.= q.(len(q1 ^ <* x *>) + j) by Th22;
end;
then q1 ^ <* x *> ^ q2 = q by A20,A116,Def7;
then
A122: len q = len(q1 ^ <* x *>) + len q2 by Th22
.= len <* x *> + len q1 + len q2 by Th22
.= 1 + len q1 + len q2 by Th40
.= 1 + (len q1 + len q2)
.= len(q1 ^ q2) + 1 by Th22;
len(p ^ <* x *>) = len p + len<* x *> by Th22
.= len p + 1 by Th40;
hence len(p ^ <* x *>) = len q by A2,A3,A4,A21,A51,A52,A71,A122,FUNCT_1:52;
end;
then
A123: for p,x st P[p] holds P[p^<*x*>];
for p holds P[p] from IndSeq(A1,A123);
hence thesis;
end;
theorem
{} in D*
proof
{} = <*>D;
hence thesis by Def11;
end;
scheme SepSeq{D()->non empty set, P[FinSequence]}:
ex X st for x holds x in X iff ex p st p in D()* & P[p] & x=p
proof
defpred R[object] means ex p st P[p] & $1=p;
consider Y such that
A1: for x being object holds x in Y iff x in D()* & R[x] from XBOOLE_0:sch 1;
take Y;
x in Y iff ex p st p in D()* & P[p] & x=p
proof
now
assume x in Y;
then x in D()* & ex p st P[p] & x=p by A1;
hence ex p st p in D()* & P[p] & x=p;
end;
hence thesis by A1;
end;
hence thesis;
end;
:: ::
:: Subsequences ::
:: ::
definition
let IT be Function;
attr IT is FinSubsequence-like means
:Def12:
ex k st dom IT c= Seg k;
end;
registration
cluster FinSubsequence-like for Function;
existence
proof
take {},len {};
thus thesis;
end;
end;
definition
mode FinSubsequence is FinSubsequence-like Function;
end;
registration
cluster FinSequence-like -> FinSubsequence-like for Function;
coherence;
let p be FinSubsequence, X be set;
cluster p|X -> FinSubsequence-like;
coherence
proof
A1: ex k st dom p c= Seg k by Def12;
dom(p|X) c= dom p by RELAT_1:60;
hence thesis by A1,XBOOLE_1:1;
end;
cluster X|`p -> FinSubsequence-like;
coherence
proof
A2: ex k st dom p c= Seg k by Def12;
dom(X|`p) c= dom p by FUNCT_1:56;
hence thesis by A2,XBOOLE_1:1;
end;
end;
registration
cluster -> NAT-defined for FinSubsequence;
coherence
proof let f be FinSubsequence;
ex n st dom f c= Seg n by Def12;
hence dom f c= NAT by XBOOLE_1:1;
end;
end;
definition
let X be set;
attr X is included_in_Seg means :DI:
ex k being Nat st X c= Seg k;
end;
registration
let n be Nat;
cluster Seg n -> included_in_Seg;
coherence;
end;
registration
cluster empty -> included_in_Seg for set;
coherence
proof
let X be set;
assume
A1: X is empty;
take 0;
thus thesis by A1;
end;
end;
registration
let n be non zero Nat;
cluster {n} -> included_in_Seg;
coherence
proof
take n;
let x be object;
assume x in {n};
then
A1: x = n by TARSKI:def 1;
0+1 <= n by NAT_1:13;
hence thesis by A1;
end;
end;
registration
cluster non empty included_in_Seg for set;
existence
proof
take {1};
thus thesis;
end;
end;
registration
cluster included_in_Seg -> finite for set;
coherence;
cluster included_in_Seg -> natural-membered for set;
coherence;
end;
registration
let f be FinSequence;
cluster dom f -> included_in_Seg;
coherence by Def12;
end;
registration
let f be FinSubsequence;
cluster dom f -> included_in_Seg;
coherence by Def12;
end;
LL1: now
let A be included_in_Seg set;
let B be set;
assume
A1: B c= A;
thus B is included_in_Seg
proof
consider k being Nat such that
A2: A c= Seg k by DI;
take k;
thus thesis by A1,A2;
end;
end;
registration
let A,B be included_in_Seg set;
cluster A \/ B -> included_in_Seg;
coherence
proof
consider k1 being Nat such that
A1: A c= Seg k1 by DI;
consider k2 being Nat such that
A2: B c= Seg k2 by DI;
take k1+k2;
A3: A \/ B c= Seg k1 \/ Seg k2 by A1,A2,XBOOLE_1:13;
k1 <= k1+k2 & k2 <= k1+k2 by NAT_1:11;
then Seg k1 c= Seg(k1+k2) & Seg k2 c= Seg(k1+k2) by Th5;
then Seg k1 \/ Seg k2 c= Seg(k1+k2) by XBOOLE_1:8;
hence thesis by A3;
end;
end;
registration
let A be included_in_Seg set;
let B be set;
cluster A \ B -> included_in_Seg;
coherence by LL1;
cluster A /\ B -> included_in_Seg;
coherence by XBOOLE_1:17, LL1;
end;
definition
let X be set;
assume
A1: X is included_in_Seg;
func Sgm X -> FinSequence of NAT means
:Def13:
rng it = X &
for m,n being Nat st 1 <= m & m < n & n <= len it holds it.m < it.n;
existence
proof
defpred P[Nat] means for X st X c= Seg $1 ex p being FinSequence of NAT st
rng p = X &
for n,m being Nat st 1 <= n & n < m & m <= len p holds p.n < p.m;
A2: P[0]
proof
let X;
assume
A3: X c= Seg 0;
take <*>(NAT);
thus rng <*>(NAT) = X by A3;
thus thesis;
end;
A4: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A5: for X st X c= Seg k holds ex p being FinSequence of NAT st
rng p = X &
for n,m be Nat st 1 <= n & n < m & m <= len p holds p.n < p.m;
let X;
assume
A6: X c= Seg(k+1);
now
assume not X c= Seg k;
then consider x being object such that
A7: x in X and
A8: not x in Seg k;
x in Seg(k+1) by A6,A7;
then reconsider n=x as Element of NAT;
A9: n=k+1
proof
assume
A10: n <> k+1;
A11: n <= k+1 by A6,A7,Th1;
A12: 1 <= n by A6,A7,Th1;
n <= k by A10,A11,NAT_1:8;
hence contradiction by A8,A12;
end;
set Y=X\{k+1};
A13: Y c= Seg k
proof
let x be object;
assume
A14: x in Y;
then
A15: x in X;
A16: not x in {k+1} by A14,XBOOLE_0:def 5;
A17: x in Seg(k+1) by A6,A14;
A18: x<>k+1 by A16,TARSKI:def 1;
reconsider m=x as Element of NAT by A17;
A19: m <= k+1 by A6,A15,Th1;
A20: 1 <= m by A6,A15,Th1;
m <= k by A18,A19,NAT_1:8;
hence thesis by A20;
end;
then consider p being FinSequence of NAT such that
A21: rng p = Y and
A22: for n,m be Nat st 1 <= n & n < m & m <= len p holds p.n < p.m by A5;
consider q such that
A23: q=p^<*k+1*>;
reconsider q as FinSequence of NAT by A23;
A24: rng q = rng p \/ rng <*k+1*> by A23,Th31
.= Y \/ {k+1} by A21,Th38
.= X \/ {k+1} by XBOOLE_1:39
.= X by A7,A9,XBOOLE_1:12,ZFMISC_1:31;
for n,m be Nat st 1 <= n & n < m & m <= len q holds q.n < q.m
proof
let l,m be Nat;
assume that
A25: 1 <= l and
A26: l < m and
A27: m <= len q;
set k2 = q.m;
set k1 = q.l;
l < len (p^<*k+1*>) by A23,A26,A27,XXREAL_0:2;
then l < len p + len <*k+1*> by Th22;
then l < len p + 1 by Th39;
then l <= len p by NAT_1:13;
then l in Seg len p by A25;
then
A30: l in dom p by Def3;
A31: 1 <= m by A25,A26,XXREAL_0:2;
A32: now
assume
A33: m=len q;
k1 = p.l by A23,A30,Def7;
then k1 in Y by A21,A30,FUNCT_1:def 3;
then
A34: k1 <= k by A13,Th1;
q.m = (p^<*k+1*>).(len p + len <*k+1*>) by A23,A33,Th22
.=(p^<*k+1*>).(len p + 1) by Th39
.= k+1 by Th42;
hence thesis by A34,NAT_1:13;
end;
now
assume m <> len q;
then m < len (p^<*k+1*>) by A23,A27,XXREAL_0:1;
then m < len p + len <*k+1*> by Th22;
then m < len p + 1 by Th39;
then
A35: m <= len p by NAT_1:13;
then m in Seg len p by A31;
then m in dom p by Def3;
then
A36: k2 = p.m by A23,Def7;
k1 = p.l by A23,A30,Def7;
hence thesis by A22,A25,A26,A35,A36;
end;
hence thesis by A32;
end;
hence thesis by A24;
end;
hence thesis by A5;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A2,A4);
hence thesis by A1;
end;
uniqueness
proof
let p,q be FinSequence of NAT such that
A37: rng p = X and
g01: for l,m being Nat st 1 <= l & l < m & m <= len p holds p.l < p.m and
g02: rng q = X and
g03: for l,m being Nat st 1 <= l & l < m & m <= len q holds q.l < q.m;
a37: for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len p &
k1 = p.l & k2 = p.m holds k1 < k2 by g01;
defpred S[FinSequence] means for X st ex k being Nat st X c= Seg k holds
($1 is FinSequence of NAT & rng $1 = X &
for l,m,k1,k2 being Nat st
(1 <= l & l < m & m <= len $1 & k1 = $1.l & k2 = $1.m)
holds k1 < k2)
implies
for q being FinSequence of NAT st rng q = X &
for l,m being Nat st ( 1 <= l & l < m & m <= len q) holds q.l < q.m holds
q=$1;
A38: S[{}];
A39: for p,x st S[p] holds S[p^<*x*>]
proof
let p,x;
assume
A40: S[p];
let X;
given k being Nat such that
A41: X c= Seg k;
assume that
A42: p^<*x*> is FinSequence of NAT and
A43: rng (p^<*x*>) = X and
A44: for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len(p^<*x*>) &
k1=(p^<*x*>).l & k2=(p^<*x*>).m holds k1 < k2;
reconsider p as FinSequence of NAT by A42,Th36;
let q be FinSequence of NAT;
assume that
A45: rng q = X and
A46: for l,m being Nat st 1 <= l & l < m & m <= len q holds q.l < q.m;
1 in Seg 1;
then
A47: 1 in dom <*x*> by Def8;
A48: ex m st m=x & for l st l in X & l <> x holds l < m
proof
<*x*> is FinSequence of NAT by A42,Th36;
then rng <*x*> c= NAT by Def4;
then {x} c= NAT by Th38;
then reconsider m=x as Element of NAT by ZFMISC_1:31;
take m;
thus m=x;
thus for l st l in X & l <> x holds l < m
proof
let l;
assume that
A49: l in X and
A50: l <> x;
consider y being object such that
A51: y in dom (p^<*x*>) and
A52: l=(p^<*x*>).y by A43,A49,FUNCT_1:def 3;
A53: y in Seg len (p^<*x*>) by A51,Def3;
reconsider k=y as Element of NAT by A51;
k <= len (p^<*x*>) by A53,Th1;
then k <= len p + len <*x*> by Th22;
then
A54: k <= len p + 1 by Th39;
A55: k <> len p + 1
proof
assume k = len p + 1;
then (p^<*x*>).k = <*x*>.1 by A47,Def7
.= x;
hence contradiction by A50,A52;
end;
A56: 1 <= k by A53,Th1;
k < len p + 1 by A54,A55,XXREAL_0:1;
then k < len p + len <*x*> by Th39;
then
A57: k < len(p^<*x*>) by Th22;
m=(p^<*x*>).(len p + 1) by Th42
.= (p^<*x*>).(len p + len <*x*>) by Th39
.= (p^<*x*>).(len(p^<*x*>)) by Th22;
hence thesis by A44,A52,A56,A57;
end;
end;
then reconsider m = x as Nat;
len q <> 0
proof
assume len q = 0;
then p^<*x*> = {} by A43,A45,Lm3,RELAT_1:38;
then 0 = len (p^<*x*>) .= len p + len <*x*> by Th22
.= 1 + len p by Th39;
hence contradiction;
end;
then consider n be Nat such that
A58: len q = n+1 by NAT_1:6;
deffunc F(Nat) = q.$1;
ex q9 being FinSequence st len q9 = n &
for m st m in dom q9 holds q9.m = F(m) from SeqLambda;
then consider q9 being FinSequence such that
A59: len q9 = n and
A60: for m st m in dom q9 holds q9.m = q.m;
now
let x be object;
assume x in rng q9;
then consider y being object such that
A61: y in dom q9 and
A62: x=q9.y by FUNCT_1:def 3;
A63: y in Seg len q9 by A61,Def3;
reconsider y as Element of NAT by A61;
A64: y <= n by A59,A63,Th1;
A65: n <= n + 1 by NAT_1:11;
A66: 1 <= y by A63,Th1;
y <= n+1 by A64,A65,XXREAL_0:2;
then y in Seg (n+1) by A66;
then y in dom q by A58,Def3;
then
A67: q.y in rng q by FUNCT_1:def 3;
rng q c= NAT by Def4;
then q.y in NAT by A67;
hence x in NAT by A60,A61,A62;
end;
then reconsider f=q9 as FinSequence of NAT by Def4,TARSKI:def 3;
A68: dom q = Seg (n+1) by A58,Def3
.= Seg (len q9 + len <*x*>) by A59,Th39;
A69: for m st m in dom <*x*> holds q.(len q9 + m) = <*x*>.m
proof
let m;
assume m in dom <*x*>;
then
A70: m in {1} by Def8,Th2;
then
A71: m=1 by TARSKI:def 1;
q.(len q9 + m) = x
proof
assume q.(len q9 + m) <> x;
then
A72: q.len q <> x by A58,A59,A70,TARSKI:def 1;
consider d being Nat such that
A73: d=x and
A74: for l st l in X & l<>x holds l<d by A48;
x in {x} by TARSKI:def 1;
then x in rng <*x*> by Th38;
then x in rng p \/ rng <*x*> by XBOOLE_0:def 3;
then x in rng q by A43,A45,Th31;
then consider y being object such that
A75: y in dom q and
A76: x=q.y by FUNCT_1:def 3;
A77: y in Seg len q by A75,Def3;
reconsider y as Element of NAT by A75;
A78: 1 <= y by A77,Th1;
A79: y <= len q by A77,Th1;
then
A80: y < len q by A72,A76,XXREAL_0:1;
1 <= len q by A78,A79,XXREAL_0:2;
then len q in Seg len q;
then
A81: len q in dom q by Def3;
A82: q.len q in X by A45,A81,FUNCT_1:def 3;
reconsider k = q.len q as Nat;
k < d by A72,A74,A82;
hence contradiction by A46,A73,A76,A78,A80;
end;
hence thesis by A71;
end;
then
A83: q9^<*x*> = q by A60,A68,Def7;
A84: not x in rng p
proof
assume x in rng p;
then consider y being object such that
A85: y in dom p and
A86: x=p.y by FUNCT_1:def 3;
A87: y in Seg len p by A85,Def3;
reconsider y as Element of NAT by A85;
A88: y <= len p by A87,Th1;
A89: len p + 1 = len p + len <*x*> by Th39
.= len (p^<*x*>) by Th22;
A90: 1 <= y by A87,Th1;
A91: y < len p + 1 by A88,NAT_1:13;
A92: m = (p^<*x*>).y by A85,A86,Def7;
m = (p^<*x*>).(len p + 1 ) by Th42;
hence contradiction by A44,A89,A90,A91,A92;
end;
A93: X = rng p \/ rng <*x*> by A43,Th31
.= rng p \/ {x} by Th39;
A94: for z being object holds z in rng p \/ {x} \ {x} iff z in rng p
proof
let z be object;
thus z in rng p \/ {x} \ {x} implies z in rng p
proof
assume
A95: z in rng p \/ {x} \ {x};
then not z in {x} by XBOOLE_0:def 5;
hence thesis by A95,XBOOLE_0:def 3;
end;
assume z in rng p;
then
( not z in {x})& z in rng p \/ {x} by A84,TARSKI:def 1,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 5;
end;
A96: for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len p &
k1 = p.l & k2 = p.m holds k1 < k2
proof
let l,m,k1,k2 be Nat;
assume that
A97: 1 <= l and
A98: l < m and
A99: m <= len p and
A100: k1=p.l and
A101: k2=p.m;
l <= len p by A98,A99,XXREAL_0:2;
then l in Seg len p by A97;
then l in dom p by Def3;
then
A102: k1 = (p^<*x*>).l by A100,Def7;
1 <= m by A97,A98,XXREAL_0:2;
then m in Seg len p by A99;
then m in dom p by Def3;
then
A103: k2 = (p^<*x*>).m by A101,Def7;
len p <= len p + 1 by NAT_1:11;
then m <= len p + 1 by A99,XXREAL_0:2;
then m <= len p + len <*x*> by Th39;
then m <= len (p^<*x*>) by Th22;
hence thesis by A44,A97,A98,A102,A103;
end;
A105: rng p = X\{x} by A93,A94,TARSKI:2;
A106: not x in rng f
proof
assume x in rng f;
then consider y being object such that
A107: y in dom f and
A108: x=f.y by FUNCT_1:def 3;
A109: y in Seg len f by A107,Def3;
reconsider y as Element of NAT by A107;
A110: y <= len f by A109,Th1;
A111: len f + 1 = len f + len <*x*> by Th39
.= len (f^<*x*>) by Th22;
A112: 1 <= y by A109,Th1;
A113: y < len f + 1 by A110,NAT_1:13;
A114: m = q.y by A60,A107,A108;
m = q.(len f + 1) by A83,Th42;
hence contradiction by A46,A83,A111,A112,A113,A114;
end;
A115: X = rng f \/ rng <*x*> by A45,A83,Th31
.= rng f \/ {x} by Th39;
A116: for z being object holds z in rng f \/ {x} \ {x} iff z in rng f
proof
let z be object;
thus z in rng f \/ {x} \ {x} implies z in rng f
proof
assume
A117: z in rng f \/ {x} \ {x};
then not z in {x} by XBOOLE_0:def 5;
hence thesis by A117,XBOOLE_0:def 3;
end;
assume z in rng f;
then
( not z in {x})& z in rng f \/ {x} by A106,TARSKI:def 1,XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 5;
end;
A118: for l,m being Nat st 1 <= l & l < m & m <= len f holds f.l < f.m
proof
let l,m be Nat;
assume that
A119: 1 <= l and
A120: l < m and
A121: m <= len f;
set k1=f.l;
set k2=f.m;
A124: m <= len q by A58,A59,A121,NAT_1:13;
l <= n by A59,A120,A121,XXREAL_0:2;
then
A125: l in Seg n by A119;
1 <= m by A119,A120,XXREAL_0:2;
then
A126: m in Seg n by A59,A121;
A127: l in dom q9 by A59,A125,Def3;
A128: m in dom q9 by A59,A126,Def3;
A129: k1 = q.l by A60,A127;
k2 = q.m by A60,A128;
hence thesis by A46,A119,A120,A124,A129;
end;
rng f = X\{x} by A115,A116,TARSKI:2;
then q9 = p by A40,A41,A96,A105,A118,XBOOLE_1:1;
hence thesis by A60,A68,A69,Def7;
end;
for p holds S[p] from IndSeq(A38,A39);
hence thesis by A1,A37,g02,g03,a37;
end;
end;
theorem Th50:
for p being FinSubsequence holds rng Sgm dom p = dom p by Def13;
definition
let p be FinSubsequence;
func Seq p -> Function equals
p * Sgm(dom p);
coherence;
end;
registration
let p be FinSubsequence;
cluster Seq p -> FinSequence-like;
coherence
proof
rng Sgm dom p = dom p by Th50;
then dom(p*Sgm(dom p)) = dom Sgm dom p by RELAT_1:27
.=Seg len Sgm dom p by Def3;
hence thesis;
end;
end;
theorem
for X st X is included_in_Seg holds Sgm X = {} iff X = {}
proof
let X;
assume X is included_in_Seg;
then rng Sgm X = X by Def13;
hence thesis;
end;
begin :: from FINSET_1, 1998
theorem :: FINSET_1:def 1
D is finite iff ex p st D = rng p
proof
thus D is finite implies ex p st D = rng p
proof
given g being Function such that
A1: rng g = D and
A2: dom g in omega;
reconsider n = dom g as Element of NAT by A2;
defpred R[object,object] means P[$2,$1];
A3: for x being object st x in Seg n ex y being object st R[x,y]
proof
let x be object;
assume
A4: x in Seg n;
then reconsider x as Element of NAT;
x >= 1 by A4,Th1;
then ex k be Nat st x = 1+k by NAT_1:10;
hence thesis;
end;
consider f such that
A5: dom f = Seg n and
A6: for x being object st x in Seg n holds R[x,f.x] from CLASSES1:sch 1(A3);
A7: rng f = dom g
proof
A8: n = { k where k is Nat: k < n } by AXIOMS:4;
thus rng f c= dom g
proof
let x be object;
assume x in rng f;
then consider y being object such that
A9: y in dom f and
A10: x = f.y by FUNCT_1:def 3;
consider k such that
A11: x = k and
A12: y = k+1 by A5,A6,A9,A10;
k + 1 <= n by A5,A9,A12,Th1;
then k < n by NAT_1:13;
hence thesis by A8,A11;
end;
let x be object;
assume x in dom g;
then consider k being Nat such that
A13: x = k and
A14: k < n by A8;
1 <= k+1 & k+1 <= n by A14,NAT_1:11,13;
then
A15: k+1 in Seg n;
then ex k1 st f.(k+1) = k1 & k+1 = k1+1 by A6;
hence thesis by A5,A13,A15,FUNCT_1:def 3;
end;
then dom(g*f) = Seg n by A5,RELAT_1:27;
then reconsider p = g*f as FinSequence by Def2;
take p;
thus thesis by A1,A7,RELAT_1:28;
end;
given p such that
A16: D = rng p;
consider n such that
A17: dom p = Seg n by Def2;
A18: n = { k where k is Nat: k < n } by AXIOMS:4;
A19: for x being object st x in n ex y being object st P[x,y]
proof
let x be object;
assume x in n;
then ex k being Nat st x = k & k < n by A18;
then reconsider k = x as Nat;
take k+1;
thus thesis;
end;
consider f such that
A20: dom f = n and
A21: for x being object st x in n holds P[x,f.x] from CLASSES1:sch 1(A19);
take p*f;
A22: rng f = dom p
proof
thus rng f c= dom p
proof
let x be object;
assume x in rng f;
then consider y being object such that
A23: y in dom f and
A24: x = f.y by FUNCT_1:def 3;
consider k such that
A25: y = k and
A26: x = k+1 by A20,A21,A23,A24;
ex m being Nat st k = m & m < n by A18,A20,A23,A25;
then 1 <= k+1 & k+1 <= n by NAT_1:11,13;
hence thesis by A17,A26;
end;
let x be object;
assume
A27: x in dom p;
then reconsider x as Element of NAT;
1 <= x by A17,A27,Th1;
then consider m be Nat such that
A28: x = 1+m by NAT_1:10;
x <= n by A17,A27,Th1;
then m < n by A28,NAT_1:13;
then
A29: m in n by A18;
then ex k st m = k & f.m = k+1 by A21;
hence thesis by A20,A28,A29,FUNCT_1:def 3;
end;
hence rng(p*f) = D by A16,RELAT_1:28;
dom(p*f) = dom f by A22,RELAT_1:27;
hence thesis by A20,ORDINAL1:def 12;
end;
begin :: Moved from CARD_1, 1999
theorem
Seg n,Seg m are_equipotent implies n = m
proof
defpred P[Nat] means ex n st Seg n,Seg $1 are_equipotent & n <> $1;
assume Seg n,Seg m are_equipotent & n <> m;
then
A1: ex m being Nat st P[m];
consider m being Nat such that
A2: P[m] and
A3: for k being Nat st P[k] holds m <= k from NAT_1:sch 5(A1);
consider n such that
A4: Seg n,Seg m are_equipotent and
A5: n <> m by A2;
A7: now
assume m = 0;
then Seg m = {};
then Seg m = Seg n by A4,RELAT_1:42;
hence contradiction by A5,Th6;
end;
then consider m1 being Nat such that
A8: m = m1+1 by NAT_1:6;
A9: now
assume n = 0;
then Seg n = {};
then Seg m = Seg n by A4,RELAT_1:42;
hence contradiction by A5,Th6;
end;
then consider n1 being Nat such that
A10: n = n1+1 by NAT_1:6;
A11: n in Seg n by A9,Th3;
A12: m in Seg m by A7,Th3;
A13: not n1+1 <= n1 by NAT_1:13;
A14: not m1+1 <= m1 by NAT_1:13;
A15: not n in Seg n1 by A10,A13,Th1;
A16: not m in Seg m1 by A8,A14,Th1;
A17: (Seg n1) /\ { n } c= {}
proof
let x be object;
assume x in (Seg n1) /\ { n };
then x in Seg n1 & x in { n } by XBOOLE_0:def 4;
hence thesis by A15,TARSKI:def 1;
end;
A18: (Seg m1) /\ { m } c= {}
proof
let x be object;
assume x in (Seg m1) /\ { m };
then x in Seg m1 & x in { m } by XBOOLE_0:def 4;
hence thesis by A16,TARSKI:def 1;
end;
A19: Seg n = (Seg n1) \/ { n } by A10,Th9;
A20: Seg m = (Seg m1) \/ { m } by A8,Th9;
A23: (Seg n1) \ { n } = ((Seg n1) \/ { n }) \ { n } & (Seg n1) misses { n }
by A17,XBOOLE_1:40;
A24: (Seg m1) \ { m } = ((Seg m1) \/ { m }) \ { m } & (Seg m1) misses { m }
by A18,XBOOLE_1:40;
A25: (Seg n) \ { n } = Seg n1 by A19,A23,XBOOLE_1:83;
(Seg m) \ { m } = Seg m1 by A20,A24,XBOOLE_1:83;
hence contradiction by A3,A4,A5,A8,A10,A11,A12,A14,A25,CARD_1:34;
end;
theorem
Seg n,n are_equipotent by Lm1;
theorem
card Seg n = card n by Lm1,CARD_1:5;
theorem Th56:
X is finite implies ex n st X,Seg n are_equipotent
proof
assume X is finite;
then reconsider n = card X as Nat;
A1: X,n are_equipotent by CARD_1:def 2;
take n;
n,Seg n are_equipotent by Lm1;
hence thesis by A1,WELLORD2:15;
end;
theorem
for n being Nat holds card Seg n = n by Lm1,CARD_1:def 2;
begin :: Addenda
:: from FINSEQ_5
registration
let x be object;
cluster <*x*> -> non empty;
coherence;
end;
:: From SPRECT_1
registration
cluster non empty for FinSequence;
existence
proof
take <* 0 *>;
thus thesis;
end;
end;
:: From FUNCT_7, actually from GOBOARD4
registration
let f1 be FinSequence, f2 be non empty FinSequence;
cluster f1^f2 -> non empty;
coherence by Th35;
cluster f2^f1 -> non empty;
coherence by Th35;
end;
registration
let x,y be object;
cluster <*x,y*> -> non empty;
coherence;
let z be object;
cluster <*x,y,z*> -> non empty;
coherence;
end;
:: from MATRIX_2
scheme SeqDEx{D()->non empty set,A()->Nat,P[object,object]}:
ex p being FinSequence of D() st dom p = Seg A() &
for k st k in Seg A() holds P[k,p.k]
provided
A1: for k st k in Seg A() ex x being Element of D() st P[k,x]
proof
A2: for y be object st y in Seg A() ex x being object st x in D() & P[y,x]
proof
let y be object;
assume
A3: y in Seg A();
then reconsider k=y as Element of NAT;
consider x being Element of D() such that
A4: P[k,x] by A1,A3;
take x;
thus thesis by A4;
end;
consider f being Function such that
A5: dom f = Seg A() and
A6: rng f c= D() and
A7: for y be object st y in Seg A() holds P[y,f.y] from FUNCT_1:sch 6(A2);
reconsider f as FinSequence by A5,Def2;
reconsider p=f as FinSequence of D() by A6,Def4;
take p;
thus thesis by A5,A7;
end;
:: from TOPREAL1
definition
let m;
let p be FinSequence;
func p|m -> FinSequence equals
p|Seg m;
coherence by Th15;
end;
definition
let D,m;
let p be FinSequence of D;
redefine func p|m -> FinSequence of D; :: redefines | (FINSEQ_1, definition)
coherence by Th18;
end;
registration
let f be FinSequence;
cluster f|0 -> empty;
coherence;
end;
theorem Th58:
len q <= i implies q|i = q
proof
assume len q <= i;
then Seg len q c= Seg i by Th5;
then dom q c= Seg i by Def3;
hence thesis by RELAT_1:68;
end;
theorem Th59:
i <= len q implies len(q|i) = i
proof
assume i <= len q;
then Seg i c= Seg(len q) by Th5;
then Seg i c= dom q by Def3;
then i in NAT & Seg i = dom(q|i) by ORDINAL1:def 12,RELAT_1:62;
hence thesis by Def3;
end;
registration
let f be non empty FinSequence;
reduce len (f|1) to 1;
reducibility
proof
1 <= len f by NAT_1:14;
hence thesis by Th59;
end;
cluster f|1 -> 1-element;
coherence;
end;
registration
let p be non empty FinSequence, n be non zero Nat;
cluster p|n -> non empty;
coherence
proof
per cases;
suppose n <= len p;
then len(p|n) = n by Th59;
hence thesis;
end;
suppose len p <= n;
hence thesis by Th58;
end;
end;
end;
:: from FSM_1
theorem
i in Seg n implies i+m in Seg (n+m)
proof
assume
A1: i in Seg n;
then
A2: 1 <= i by Th1;
A3: i <= n by A1,Th1;
i <= i+m by NAT_1:11;
then 1 <= i+m by A2,XXREAL_0:2;
hence thesis by A3,Th1,XREAL_1:7;
end;
theorem
i > 0 & i+m in Seg (n+m) implies i in Seg n & i in Seg (n+m)
proof
assume that
A1: i > 0 and
A2: i+m in Seg (n+m);
1 = 0+1;
then
A3: 1 <= i by A1,NAT_1:13;
A4: i+m <= n+m by A2,Th1;
i <= n by A2,Th1,XREAL_1:6;
hence i in Seg n by A3;
i <= i+m by NAT_1:11;
then i <= n+m by A4,XXREAL_0:2;
hence thesis by A3;
end;
:: from LANG1
definition
let R be Relation;
func R[*] -> Relation means
for x,y being object holds [x,y] in it iff x in field R & y in field R &
ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
existence
proof
defpred X[object,object] means
ex p being FinSequence st len p >= 1 & p.1 = $1 & p.(len p) = $2 &
for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
thus ex S being Relation st for x,y being object holds
[x,y] in S iff x in field R & y in field R & X[x,y] from RELAT_1:sch 1;
end;
uniqueness
proof
let R1,R2 be Relation such that
A1: for x,y being object holds [x,y] in R1 iff x in field R & y in field R &
ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R and
A2: for x,y being object holds [x,y] in R2 iff x in field R & y in field R &
ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y &
for i being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R;
let x,y be object;
thus [x,y] in R1 implies [x,y] in R2
proof
assume
A3: [x,y] in R1;
then
A4: x in field R & y in field R by A1;
ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y & for i
being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R by A1,A3;
hence thesis by A2,A4;
end;
assume
A5: [x,y] in R2;
then
A6: x in field R & y in field R by A2;
ex p being FinSequence st len p >= 1 & p.1 = x & p.(len p) = y & for i
being Nat st i >= 1 & i < len p holds [p.i,p.(i+1)] in R by A2,A5;
hence thesis by A1,A6;
end;
end;
theorem
for D1,D2 being set st D1 c= D2 holds D1* c= D2*
proof
let D1,D2 be set such that
A1: D1 c= D2;
let x be object;
assume x in D1*;
then reconsider p = x as FinSequence of D1 by Def11;
rng p c= D1 by Def4;
then x is FinSequence of D2 by Def4,A1,XBOOLE_1:1;
hence thesis by Def11;
end;
:: 2005.05.13, A.T.
registration
let D be set;
cluster D* -> functional;
coherence by Def11;
end;
:: from SCMFSA_7, 2005.11.21, A.T.
theorem
for p,q being FinSequence st p c= q or dom p c= dom q holds len p <= len q
proof let p,q be FinSequence;
assume p c= q or dom p c= dom q;
then dom p c= dom q by RELAT_1:11;
then
A1: Segm card dom p c= Segm card dom q by CARD_1:11;
card dom p = card p & card dom q = card q by CARD_1:62;
hence thesis by A1,NAT_1:39;
end;
theorem
for p,q being FinSequence, i being Nat st
1 <= i & i <= len p holds (p ^ q).i = p.i
proof
let p,q be FinSequence, i be Nat;
assume
A1: 1 <= i & i <= len p;
i in NAT & Seg len p = dom p by Def3,ORDINAL1:def 12;
then i in dom p by A1;
hence thesis by Def7;
end;
theorem
for p,q being FinSequence, i being Nat st
1 <= i & i <= len q holds (p ^ q).(len p + i) = q.i
proof
let p,q be FinSequence, i be Nat;
assume 1 <= i & i <= len q;
then
len p + 1 <= len p + i & len p + i <= len p + len q by XREAL_1:6;
hence (p ^ q).(len p + i) = q.(len p + i - len p) by Th23
.= q.i;
end;
:: from GRAPH_2, 2006.01.09, A.T.
scheme FinSegRng{n() -> Nat, F(set)->set, P[set]}:
{F(i) where i is Nat: i<=n() & P[i]} is finite
proof
set F = {F(i) where i is Nat: i<=n() & P[i]};
deffunc G(Nat) = F($1-1);
consider f being FinSequence such that
A1: len f = n()+1 and
A2: for k st k in dom f holds f.k = G(k) from SeqLambda;
F c= rng f
proof
let x be object;
assume x in F;
then consider j being Nat such that
A3: x=F(j) and
A4: j<=n() and P[j];
1<=j+1 & j+1<=n()+1 by A4,NAT_1:11,XREAL_1:6;
then j+1 in Seg (n()+1);
then
A5: j+1 in dom f by A1,Def3;
then f.(j+1) = F(j+1-1) by A2
.= F(j);
hence thesis by A3,A5,FUNCT_1:def 3;
end;
hence thesis;
end;
Lm5: x in Seg n implies x = 1 or ... or x = n
proof assume
A1: x in Seg n;
then reconsider k = x as Nat;
1 <= k & k <= n by A1,Th1;
hence thesis;
end;
theorem Th66:
for x1, x2, x3, x4 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>
holds len p = 4 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4
proof
let x1, x2, x3, x4 be set, p be FinSequence;
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>;
set p13 = <*x1*>^<*x2*>^<*x3*>;
A2: p13 = <*x1, x2, x3*>;
then
A3: len p13 = 3 by Th45;
A4: p13.1 = x1 & p13.2 = x2 by A2;
A5: p13.3 = x3 by A2;
thus len p = len p13 + len <*x4*> by A1,Th22
.= 3 + 1 by A3,Th40
.= 4;
A6: dom p13 = Seg 3 by A3,Def3;
1 in Seg 3 & ...& 3 in Seg 3;
hence p.1 = x1 & p.2 = x2 & p.3 = x3 by A1,A4,A5,Def7,A6;
thus p.4 = p.(len p13 + 1) by A3
.= x4 by A1,Th42;
end;
theorem Th67:
for x1, x2, x3, x4, x5 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>
holds len p = 5 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5
proof
let x1, x2, x3, x4, x5 be set, p be FinSequence;
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>;
set p14 = <*x1*>^<*x2*>^<*x3*>^<*x4*>;
A2: len p14 = 4 by Th66;
A3: p14.1 = x1 & p14.2 = x2 by Th66;
A4: p14.3 = x3 & p14.4 = x4 by Th66;
thus len p = len p14 + len <*x5*> by A1,Th22
.= 4 + 1 by A2,Th40
.= 5;
A5: dom p14 = Seg 4 by A2,Def3;
1 in Seg 4 & ...& 4 in Seg 4;
hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 by A1,A3,A4,Def7,A5;
thus p.5 = p.(len p14 + 1) by A2
.= x5 by A1,Th42;
end;
theorem Th68:
for x1, x2, x3, x4, x5, x6 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>
holds len p = 6 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6
proof
let x1, x2, x3, x4, x5, x6 be set, p be FinSequence;
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>;
set p15 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>;
A2: len p15 = 5 by Th67;
A3: p15.1 = x1 & p15.2 = x2 by Th67;
A4: p15.3 = x3 & p15.4 = x4 by Th67;
A5: p15.5 = x5 by Th67;
thus len p = len p15 + len <*x6*> by A1,Th22
.= 5 + 1 by A2,Th40
.= 6;
A6: dom p15 = Seg 5 by A2,Def3;
1 in Seg 5 & ...& 5 in Seg 5;
hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5
by A1,A3,A4,A5,Def7,A6;
thus p.6 = p.(len p15 + 1) by A2
.= x6 by A1,Th42;
end;
theorem Th69:
for x1, x2, x3, x4, x5, x6, x7 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>
holds len p = 7 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7
proof
let x1, x2, x3, x4, x5, x6, x7 be set, p be FinSequence;
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>;
set p16 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>;
A2: len p16 = 6 by Th68;
A3: p16.1 = x1 & p16.2 = x2 by Th68;
A4: p16.3 = x3 & p16.4 = x4 by Th68;
A5: p16.5 = x5 & p16.6 = x6 by Th68;
thus len p = len p16 + len <*x7*> by A1,Th22
.= 6 + 1 by A2,Th40
.= 7;
A6: dom p16 = Seg 6 by A2,Def3;
1 in Seg 6 & ...& 6 in Seg 6;
hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6
by A1,A3,A4,A5,Def7,A6;
thus p.7 = p.(len p16 + 1) by A2
.= x7 by A1,Th42;
end;
theorem Th70:
for x1,x2,x3,x4, x5, x6, x7, x8 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>
holds len p = 8 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7 & p.8 = x8
proof
let x1, x2, x3, x4, x5, x6, x7, x8 be set, p be FinSequence;
thus p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>
implies len p = 8 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7 & p.8 = x8
proof
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>;
set p17 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>;
A2: len p17 = 7 by Th69;
A3: p17.1 = x1 & p17.2 = x2 by Th69;
A4: p17.3 = x3 & p17.4 = x4 by Th69;
A5: p17.5 = x5 & p17.6 = x6 by Th69;
A6: p17.7 = x7 by Th69;
thus len p = len p17 + len <*x8*> by A1,Th22
.= 7 + 1 by A2,Th40
.= 8;
A7: dom p17 = Seg 7 by A2,Def3;
1 in Seg 7 & ...& 7 in Seg 7;
hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 &
p.7 = x7 by A1,A3,A4,A5,A6,Def7,A7;
thus p.8 = p.(len p17 + 1) by A2
.= x8 by A1,Th42;
end;
end;
theorem
for x1,x2,x3,x4,x5,x6,x7, x8, x9 being set, p being FinSequence
st p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>
holds len p = 9 & p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 &
p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9
proof
let x1, x2, x3, x4, x5, x6, x7, x8, x9 be set, p be FinSequence;
thus p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>
implies len p = 9 & p.1 = x1 & p.2 = x2 & p.3 = x3&p.4 = x4&p.5 = x5 &
p.6 = x6 & p.7 = x7 & p.8 = x8 & p.9 = x9
proof
assume
A1: p = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>^<*x9*>;
set p17 = <*x1*>^<*x2*>^<*x3*>^<*x4*>^<*x5*>^<*x6*>^<*x7*>^<*x8*>;
A2: len p17 = 8 by Th70;
A3: p17.1 = x1 & p17.2 = x2 by Th70;
A4: p17.3 = x3 & p17.4 = x4 by Th70;
A5: p17.5 = x5 & p17.6 = x6 by Th70;
A6: p17.7 = x7 & p17.8 = x8 by Th70;
thus len p = len p17 + len <*x9*> by A1,Th22
.= 8 + 1 by A2,Th40
.= 9;
A7: dom p17 = Seg 8 by A2,Def3;
1 in Seg 8 & ...& 8 in Seg 8;
hence p.1 = x1 & p.2 = x2 & p.3 = x3 & p.4 = x4 & p.5 = x5 & p.6 = x6 &
p.7 = x7 & p.8 = x8 by A1,A3,A4,A5,A6,Def7,A7;
thus p.9 = p.(len p17 + 1) by A2
.= x9 by A1,Th42;
end;
end;
:: from SCMFSA_7, 2006.03.14, A.T.
theorem
for p being FinSequence holds p | Seg 0 = {};
theorem
for f,g being FinSequence holds f | Seg 0 = g | Seg 0;
theorem
for D being non empty set, x being Element of D holds
<* x *> is FinSequence of D;
LL:
for f being D-valued FinSequence holds f is FinSequence of D
proof
let f be D-valued FinSequence;
thus rng f c= D by RELAT_1:def 19;
end;
theorem
for D being set, p,q being D-valued FinSequence holds p^q is FinSequence of D
proof
let D be set, p,q be D-valued FinSequence;
reconsider p,q as FinSequence of D by LL;
p^q is FinSequence of D;
hence thesis;
end;
:: from GROUP_7, 2007.02.10, AK
reserve a, b, c, d, e, f for object;
theorem
<*a*> = <*b*> implies a = b
proof
assume
A1: <*a*> = <*b*>;
thus a = <*a*>.1
.= b by A1,Def8;
end;
theorem
<*a,b*> = <*c,d*> implies a = c & b = d
proof
assume
A1: <*a,b*> = <*c,d*>;
thus a = <*a,b*>.1
.= c by A1,Th44;
thus b = <*a,b*>.2
.= d by A1,Th44;
end;
theorem
<*a,b,c*> = <*d,e,f*> implies a = d & b = e & c = f
proof
assume
A1: <*a,b,c*> = <*d,e,f*>;
thus a = <*a,b,c*>.1
.= d by A1,Th45;
thus b = <*a,b,c*>.2
.= e by A1,Th45;
thus c = <*a,b,c*>.3
.= f by A1,Th45;
end;
:: from PRVECT_1, 2007.03.09, A.T
registration
cluster non empty non-empty for FinSequence;
existence
proof
take <*{{}}*>;
thus <*{{}}*> is non empty;
assume {} in rng <*{{}}*>;
then {} in {{{}}} by Th38;
hence contradiction by TARSKI:def 1;
end;
end;
theorem Th79:
for p,q being FinSequence st q = p|Seg n holds len q <= len p
proof
let p,q be FinSequence;
assume q = p|Seg n;
then
A1: dom q = dom p /\ Seg n by RELAT_1:61;
Seg len q = dom q & Seg len p = dom p by Def3;
hence thesis by Th5,A1,XBOOLE_1:17;
end;
theorem
for p,r being FinSequence st r = p|Seg n ex q being FinSequence st p = r^q
proof
let p,r be FinSequence;
assume
A1: r = p|Seg n;
then consider m be Nat such that
A2: len p = len r + m by Th79,NAT_1:10;
deffunc U(Nat) = p.(len r + $1);
consider q being FinSequence such that
A3: len q = m & for k st k in dom q holds q.k = U(k) from SeqLambda;
take q;
A4: len p = len(r^q) by A2,A3,Th22;
now
let k such that
A5: 1 <= k and
A6: k <= len p;
A7: now
assume k <= len r;
then
A8: k in Seg len r by A5;
A9: dom r = Seg len r by Def3;
then (r^q).k = r.k by A8,Def7;
hence p.k = (r^q).k by A1,A8,A9,FUNCT_1:47;
end;
now
assume
A10: not k <= len r;
then consider j being Nat such that
A11: k = len r + j by NAT_1:10;
k-len r = j by A11;
then
A12: (r^q).k = q.j by A4,A6,A10,Th24;
j <> 0 by A10,A11;
then
A13: 0+1 <= j by NAT_1:13;
j <= len q by A2,A3,A6,A11,XREAL_1:6;
then j in Seg m by A3,A13;
then j in dom q by A3,Def3;
hence p.k = (r^q).k by A3,A11,A12;
end;
hence p.k = (r^q).k by A7;
end;
hence thesis by A4,Th14;
end;
:: from GOBOARD1, PRALG_1, 2007.04.06, A.T
registration
let D be non empty set;
cluster non empty for FinSequence of D;
existence
proof set x = the Element of D;
take <*x*>;
thus thesis;
end;
end;
registration
let D be non empty set;
cluster non empty D-valued for FinSequence;
existence
proof set x = the Element of D;
take <*x*>;
thus thesis;
end;
end;
:: Added by AK, 2007.11.07
definition
let p,q be FinSequence;
redefine pred p = q means :: redefines = (FUNCT_1, redefinition) → = (RELAT_1, redefinition) → = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
len p = len q & for k st 1 <= k & k <= len p holds p.k = q.k;
compatibility by Th14;
end;
:: from GROEB_2, 2008.10.08, A.T.
theorem
for x,y,z being object holds
1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*>
proof
let x,y,z be object;
len <*x,y,z*> = 3 by Th45; then
dom <*x,y,z*> = Seg 3 by Def3;
hence thesis;
end;
theorem
for p being FinSequence, n,m being Nat st m <= n holds p|n|m = p|m
by Th5,RELAT_1:74;
:: from CARD_5, 2008.10.08, A.T.
theorem
Seg n = (n+1) \ {0}
proof
A1: n+1 = {m: m < n+1} by AXIOMS:4;
thus Seg n c= (n+1) \ {0}
proof
let x be object;
assume x in Seg n;
then consider k being Nat such that
A2: x = k and
A3: 1 <= k and
A4: k <= n;
k < n+1 by A4,NAT_1:13;
then
A5: x in n+1 by A1,A2;
not x in {0} by A2,A3,TARSKI:def 1;
hence thesis by A5,XBOOLE_0:def 5;
end;
let x be object;
assume
A6: x in (n+1) \ {0};
then
A7: x in n+1;
A8: not x in {0} by A6,XBOOLE_0:def 5;
consider m such that
A9: x = m and
A10: m < n+1 by A1,A7;
A11: x <> 0 by A8,TARSKI:def 1;
0+1 = 1;
then
A12: 1 <= m by A9,A11,NAT_1:13;
m <= n by A10,NAT_1:13;
hence thesis by A9,A12;
end;
:: from CIRCCOMB, 2009.03.27, A.T.
registration
let n be natural Number;
cluster n-element for FinSequence;
existence
proof
A1: n is Nat by TARSKI:1;
set p = Seg n --> {};
dom p = Seg n by FUNCOP_1:13;
then reconsider p as FinSequence by A1,Def2;
take p;
Seg len p = dom p by Def3;
hence len p = n by Th6,FUNCOP_1:13;
end;
end;
:: from FACIRC_1, 2009.02.16, A.T.
registration
let x be object;
cluster <*x*> -> 1-element;
coherence;
let y be object;
cluster <*x,y*> -> 2-element;
coherence by Th44;
let z be object;
cluster <*x,y,z*> -> 3-element;
coherence by Th45;
end;
:: new, 2009.08.24, A.T.
definition let X be set;
attr X is FinSequence-membered means :Def18:
x in X implies x is FinSequence;
end;
registration
cluster empty -> FinSequence-membered for set;
coherence;
end;
registration
cluster {{}} -> FinSequence-membered;
coherence by TARSKI:def 1;
end;
registration
cluster non empty FinSequence-membered for set;
existence
proof
take X = {{}};
thus thesis;
end;
end;
::: moved from HILB10_7
registration let X,Y be FinSequence-membered set;
cluster X \/ Y -> FinSequence-membered;
coherence
proof
let x be object;
assume x in X \/ Y; then
x in X or x in Y by XBOOLE_0:def 3;
hence thesis by Def18;
end;
end;
registration let X be set;
cluster X* -> FinSequence-membered;
coherence by Def11;
end;
theorem
for f being Function st f in D* & x in dom f holds f.x in D
proof let f be Function such that
A1: f in D* and
A2: x in dom f;
f is FinSequence of D by A1,Def11;
then rng f c= D by Def4;
hence f.x in D by A2,FUNCT_1:3;
end;
registration
cluster FinSequence-membered -> functional for set;
coherence;
end;
theorem
for X being FinSequence-membered set ex Y being non empty set st X c= Y*
proof
let X be FinSequence-membered set;
set Z = {rng f where f is Element of X: f in X};
take Y = succ union Z;
let x be object;
assume
A1: x in X;
then reconsider x as FinSequence by Def18;
rng x in {rng f where f is Element of X: f in X} by A1;
then rng x c= Y by ORDINAL3:1,SETFAM_1:41;
then x is FinSequence of Y by Def4;
hence thesis by Def11;
end;
registration
let X be FinSequence-membered set;
cluster -> FinSequence-like for Element of X;
coherence
proof
let e be Element of X;
X is empty or X is non empty;
hence thesis by Def18,SUBSET_1:def 1;
end;
end;
registration let X be FinSequence-membered set;
cluster -> FinSequence-membered for Subset of X;
coherence;
end;
:: from TREES_1, 2009.09.09, A.T.
theorem
for p,q being FinSequence st q = p|Seg n holds len q <= n
proof
let p,q be FinSequence;
assume q = p|Seg n;
then A1: dom q = dom p /\ Seg n by RELAT_1:61;
Seg len q = dom q by Def3;
hence thesis by Th5,A1,XBOOLE_1:17;
end;
theorem
for p,q being FinSequence st p = p^q or p = q^p holds q = {}
proof
let p,q be FinSequence such that
A1: p = p^q or p = q^p;
len(p^q) = len p + len q & len(q^p) = len q + len p by Th22;
hence thesis by A1;
end;
theorem
for p,q being FinSequence st p^q = <*x*> holds
p = <*x*> & q = {} or p = {} & q = <*x*>
proof
let p,q be FinSequence;
assume
A1: p^q = <*x*>;
then A2: 1 = len(p^q) by Th40
.= len p + len q by Th22;
A3: now
assume len p = 0;
thus
then p = {};
hence q = <*x*> by A1,Th34;
end;
now
assume len p <> 0;
then A4: 0+1 <= len p by NAT_1:13;
len p <= 1 by A2,NAT_1:11;
then len p = 1 by A4,XXREAL_0:1;
thus
then q = {} by A2;
hence p = <*x*> by A1,Th34;
end;
hence thesis by A3;
end;
:: missing, 2009.09.26, A.T.
theorem Th88:
for f being n-element FinSequence holds dom f = Seg n
proof let f be n-element FinSequence;
len f = n by CARD_1:def 7;
hence dom f = Seg n by Def3;
end;
registration let n,m be natural Number;
let f be n-element FinSequence, g be m-element FinSequence;
cluster f^g -> (n+m)-element;
coherence
proof
len f = n & len g = m by CARD_1:def 7;
hence len(f^g) = n+m by Th22;
end;
end;
:: from JORDAN7, 2010.02.26, A.T
registration
cluster NAT-defined increasing -> one-to-one for real-valued Function;
coherence
proof
let f be real-valued Function;
assume that
A0: f is NAT-defined and
A1: f is increasing;
let x,y be object;
assume that
A2: x in dom f & y in dom f and
A3: f.x = f.y;
dom f c= NAT by A0,RELAT_1:def 18;
then reconsider x,y as Element of NAT by A2;
x <= y & x >= y by A1,A2,A3,VALUED_0:def 13;
hence thesis by XXREAL_0:1;
end;
end;
:: from AMI_6, 2010.04.07, A.T.
theorem
for x, y being object st x in dom <*y*> holds x = 1
proof
let x, y be object;
assume x in dom <*y*>;
then x in Seg 1 by Th38;
hence thesis by Th2,TARSKI:def 1;
end;
:: from FOMODEL0, 2011.06.12, A.T.
registration let X;
cluster X-valued for FinSequence;
existence
proof
take <*>X;
thus thesis;
end;
end;
:: new, 2011.10.03, A.K.
registration
let D be FinSequence-membered set;
let f be D-valued Function;
let x be object;
cluster f.x -> FinSequence-like;
coherence
proof
per cases;
suppose x in dom f;
then
A1: f.x in rng f by FUNCT_1:def 3;
rng f c= D by RELAT_1:def 19;
hence thesis by A1;
end;
suppose not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
end;
end;
theorem
x in Seg n implies x = 1 or ... or x = n by Lm5;
theorem
dom <*x,y*> = { 1,2 }
proof
thus dom <*x,y*> = Seg len <*x,y*> by Def3
.= {1,2} by Th2,Th44;
end;
begin :: Fixed ordering of a finite set into a finite sequence
registration
let A be finite set;
cluster onto one-to-one for FinSequence of A;
existence
proof
consider n such that
A1: A,Seg n are_equipotent by Th56;
consider f being Function such that
A2: f is one-to-one and
A3: dom f = Seg n and
A4: rng f = A by A1,WELLORD2:def 4;
f is FinSequence by A3,Def2;
then reconsider f as FinSequence of A by A4,Def4;
take f;
thus thesis by A2,A4,FUNCT_2:def 3;
end;
end;
definition
let A be finite set;
func canFS A -> FinSequence equals
the one-to-one onto FinSequence of A;
coherence;
end;
definition
let A be finite set;
redefine func canFS A -> FinSequence of A; :: redefines canFS (FINSEQ_1, definition)
coherence;
end;
registration
let A be finite set;
cluster canFS A -> one-to-one onto for FinSequence of A;
coherence;
end;
theorem Th92:
for A being finite set holds len canFS A = card A
proof
let A be finite set;
thus card canFS A = card dom canFS A by CARD_1:62
.= card rng canFS A by CARD_1:70
.= card A by FUNCT_2:def 3;
end;
registration
let A be finite non empty set;
cluster canFS A -> non empty;
coherence
proof
len canFS A = card A by Th92;
hence thesis;
end;
end;
theorem
for a being object holds canFS({a}) = <* a *>
proof
let a be object;
A1: rng canFS({a}) = {a} by FUNCT_2:def 3;
len canFS({a}) = card {a} by Th92
.= 1 by CARD_1:30;
hence thesis by A1,Th39;
end;
theorem
for A being finite set holds (canFS A)" is Function of A, Seg card A
proof
let A be finite set;
len canFS A = card A by Th92;
then dom canFS A = Seg card A by Def3;
then
A1: rng ((canFS A)") = Seg card A by FUNCT_1:33;
rng canFS A = A by FUNCT_2:def 3;
then dom ((canFS A)") = A by FUNCT_1:33;
hence thesis by A1,FUNCT_2:1;
end;
:: from PNPROC_1, 2012.02.20, A.T.
theorem
i > 0 implies {[i,x]} is FinSubsequence
proof
assume
A1: i > 0;
A2: dom {[i,x]} = {i} by RELAT_1:9;
{i} c= Seg i
proof
let x be object;
assume x in {i};
then x = i by TARSKI:def 1;
hence thesis by A1,Th3;
end;
hence thesis by A2,Def12;
end;
Lm6: for p being FinSubsequence st Seq p = {} holds p = {}
proof
let p be FinSubsequence such that
A1: Seq p = {};
rng Sgm dom p = dom p by Th50;
then Sgm dom p = {} by A1,RELAT_1:27;
then dom p = rng {} by Th50;
hence thesis;
end;
theorem
for q being FinSubsequence holds q = {} iff Seq q = {} by Lm6;
registration
cluster -> finite for FinSubsequence;
coherence
proof
let q be FinSubsequence;
ex n being Nat st dom q c= Seg n by Def12;
hence thesis by FINSET_1:10;
end;
end;
reserve x1,x2,y1,y2 for object;
theorem
{[x1,y1], [x2,y2]} is FinSequence implies x1 = 1 & x2 = 1 & y1 = y2 or
x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1
proof
assume {[x1,y1], [x2,y2]} is FinSequence;
then reconsider p = {[x1,y1], [x2,y2]} as FinSequence;
A1: dom p = {x1,x2} by RELAT_1:10;
then
A2: x1 in dom p by TARSKI:def 2;
A3: x2 in dom p by A1,TARSKI:def 2;
A4: [x1,y1] in p by TARSKI:def 2;
A5: [x2,y2] in p by TARSKI:def 2;
A6: p.x1 = y1 by A4,FUNCT_1:1;
A7: p.x2 = y2 by A5,FUNCT_1:1;
A8: dom p = Seg len p by Def3;
A9: len p <= 1+1 by CARD_2:50;
A10: len p >= 0 qua Nat+1 by NAT_1:13;
A11: now
assume len p = 1;
hence x1 = 1 & x2 = 1 by A2,A3,A8,Th2,TARSKI:def 1;
hence y1 = y2 by A5,A6,FUNCT_1:1;
end;
now
assume
A12: len p = 2;
A13: x1 = x2 implies p = {[x1,y1]} by A6,A7,ENUMSET1:29;
x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1 or x1 = 1 & x2 = 1 or x1 = 2 & x2 = 2
by A2,A3,A8,A12,Th2,TARSKI:def 2;
hence x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1 by A12,A13,CARD_1:30;
end;
hence thesis by A9,A10,A11,NAT_1:9;
end;
theorem
<*x1,x2*> = {[1,x1], [2,x2]}
proof
reconsider f={[1,x1], [2,x2]} as Function by GRFUNC_1:8;
A1: dom f = {1,2} by RELAT_1:10;
then
A2: dom <*x1,x2*> = dom f by Th2,Th88;
now
let x be object;
assume
A3: x in {1,2};
per cases by A3,TARSKI:def 2;
suppose
A4: x = 1;
then
A5: <*x1,x2*>.x = x1;
[x,x1] in f by A4,TARSKI:def 2;
hence f.x = <*x1,x2*>.x by A5,FUNCT_1:1;
end;
suppose
A6: x = 2;
then
A7: <*x1,x2*>.x = x2;
[x,x2] in f by A6,TARSKI:def 2;
hence f.x = <*x1,x2*>.x by A7,FUNCT_1:1;
end;
end;
hence thesis by A1,A2,FUNCT_1:2;
end;
theorem
for q being FinSubsequence holds dom Seq q = dom Sgm dom q
proof
let q be FinSubsequence;
rng Sgm dom q = dom q by Th50;
hence thesis by RELAT_1:27;
end;
theorem
for q being FinSubsequence holds rng q = rng Seq q
proof
let q be FinSubsequence;
dom q = rng Sgm dom q by Th50;
hence thesis by RELAT_1:28;
end;
registration
cluster one-to-one for FinSequence;
existence
proof
take {};
thus thesis;
end;
end;
registration
let D;
cluster one-to-one for FinSequence of D;
existence
proof
take <*>D;
thus thesis;
end;
end;
registration
cluster non empty natural-valued for FinSequence;
existence
proof
<*0*> is natural-valued & <*0*> is non empty;
hence thesis;
end;
end;
theorem
for f being D-valued FinSequence holds f is FinSequence of D by LL;
theorem
for f being natural-valued FinSequence holds f is FinSequence of NAT
proof
let f be natural-valued FinSequence;
thus rng f c= NAT by VALUED_0:def 6;
end;
theorem
for f being integer-valued FinSequence holds f is FinSequence of INT
proof
let f be integer-valued FinSequence;
thus rng f c= INT by VALUED_0:def 5;
end;
theorem
for f being rational-valued FinSequence holds f is FinSequence of RAT
proof
let f be rational-valued FinSequence;
thus rng f c= RAT by VALUED_0:def 4;
end;
theorem
for f being real-valued FinSequence holds f is FinSequence of REAL
proof
let f be real-valued FinSequence;
thus rng f c= REAL by VALUED_0:def 3;
end;
theorem
for f being complex-valued FinSequence holds f is FinSequence of COMPLEX
proof
let f be complex-valued FinSequence;
thus rng f c= COMPLEX by VALUED_0:def 1;
end;
theorem
for f being ext-real-valued FinSequence holds f is FinSequence of ExtREAL
proof
let f be ext-real-valued FinSequence;
thus rng f c= ExtREAL by VALUED_0:def 2;
end;
registration
let n be Nat;
let f be natural-valued FinSequence;
cluster f|n -> natural-valued;
coherence;
end;
registration
let n be Nat;
let f be NAT-valued FinSequence;
cluster f|n -> NAT-valued;
coherence;
end;
registration
let n be Nat;
let f be integer-valued FinSequence;
cluster f|n -> integer-valued;
coherence;
end;
registration
let n be Nat;
let f be INT-valued FinSequence;
cluster f|n -> INT-valued;
coherence;
end;
registration
let n be Nat;
let f be rational-valued FinSequence;
cluster f|n -> rational-valued;
coherence;
end;
registration
let n be Nat;
let f be RAT-valued FinSequence;
cluster f|n -> RAT-valued;
coherence;
end;
registration
let n be Nat;
let f be real-valued FinSequence;
cluster f|n -> real-valued;
coherence;
end;
registration
let n be Nat;
let f be REAL-valued FinSequence;
cluster f|n -> REAL-valued;
coherence;
end;
registration
let n be Nat;
let f be complex-valued FinSequence;
cluster f|n -> complex-valued;
coherence;
end;
registration
let n be Nat;
let f be COMPLEX-valued FinSequence;
cluster f|n -> COMPLEX-valued;
coherence;
end;
registration
let n be Nat;
let f be ext-real-valued FinSequence;
cluster f|n -> ext-real-valued;
coherence;
end;
registration
let n be Nat;
let f be ExtREAL-valued FinSequence;
cluster f|n -> ExtREAL-valued;
coherence;
end;
registration
let I be set;
let p,q be I-valued FinSequence;
cluster p^q -> I-valued;
coherence
proof
rng p c= I & rng q c= I by RELAT_1:def 19;
then rng (p^q) = rng p \/ rng q c= I by Th31,XBOOLE_1:8;
hence rng (p^q) c= I;
end;
end;
registration
let f,g be natural-valued FinSequence;
cluster f^g -> natural-valued;
coherence;
end;
registration
let f,g be integer-valued FinSequence;
cluster f^g -> integer-valued;
coherence;
end;
registration
let f,g be rational-valued FinSequence;
cluster f^g -> rational-valued;
coherence;
end;
registration
let f,g be real-valued FinSequence;
cluster f^g -> real-valued;
coherence;
end;
registration
let f,g be complex-valued FinSequence;
cluster f^g -> complex-valued;
coherence;
end;
registration
let f,g be ext-real-valued FinSequence;
cluster f^g -> ext-real-valued;
coherence;
end;
registration
let n be natural Number;
cluster <*n*> -> natural-valued;
coherence
proof
set f = <*n*>;
let x be object such that
A1: x in dom f;
dom f = {1} by Def8,Th2;
then x = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
let i be Integer;
cluster <*i*> -> integer-valued;
coherence
proof
set f = <*i*>;
let x be object such that
A1: x in dom f;
dom f = {1} by Def8,Th2;
then x = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
let r be Rational;
cluster <*r*> -> rational-valued;
coherence
proof
set f = <*r*>;
let x be object such that
A1: x in dom f;
dom f = {1} by Def8,Th2;
then x = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
let r be Real;
cluster <*r*> -> real-valued;
coherence
proof
set f = <*r*>;
let x be object such that
A1: x in dom f;
dom f = {1} by Def8,Th2;
then x = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
let c be Complex;
cluster <*c*> -> complex-valued;
coherence
proof
set f = <*c*>;
let x be object such that
A1: x in dom f;
dom f = {1} by Def8,Th2;
then x = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
let e be ExtReal;
cluster <*e*> -> ext-real-valued;
coherence
proof
set f = <*e*>;
let x be object such that
A1: x in dom f;
dom f = {1} by Def8,Th2;
then x = 1 by A1,TARSKI:def 1;
hence thesis;
end;
end;
registration
cluster -> natural-valued for FinSequence of NAT;
coherence;
cluster -> integer-valued for FinSequence of INT;
coherence;
cluster -> rational-valued for FinSequence of RAT;
coherence;
cluster -> real-valued for FinSequence of REAL;
coherence;
cluster -> complex-valued for FinSequence of COMPLEX;
coherence;
cluster -> ext-real-valued for FinSequence of ExtREAL;
coherence;
end;
:: registration
:: let D be non empty set;
:: let x1 be Element of D;
:: cluster <*x1*> -> D-valued;
:: coherence;
:: let x2 be Element of D;
:: cluster <*x1,x2*> -> D-valued;
:: coherence;
:: let x3 be Element of D;
:: cluster <*x1,x2,x3*> -> D-valued;
:: coherence;
:: end;
theorem
for A being included_in_Seg set, B being set st B c= A holds
B is included_in_Seg by LL1;
:: added by SK, 15.11.2024
registration let p be FinSequence;
cluster disjoin p -> FinSequence-like;
coherence
proof
consider n being Nat such that
A1: dom p = Seg n by Def2;
dom disjoin p = dom p by CARD_3:def 3;
hence thesis by A1;
end;
end;