:: Segments of Natural Numbers and Finite Sequences
:: by Grzegorz Bancerek and Krzysztof Hryniewiecki
::
:: Received April 1, 1989
:: Copyright (c) 1990-2016 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;
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,
XXREAL_0, FUNCT_2, INT_1, VALUED_0;
constructors WELLORD2, FUNCOP_1, FUNCT_4, XXREAL_0, XREAL_0, NAT_1, CARD_1,
RELSET_1, XCMPLX_0, INT_1, VALUED_0, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1,
XXREAL_0, XREAL_0, NAT_1, CARD_1, NUMBERS, VALUED_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
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
:: FINSEQ_1:def 1
{ k where k is Nat: 1 <= k & k <= n };
end;
definition
let n be Nat;
redefine func Seg n -> Subset of NAT;
end;
theorem :: FINSEQ_1:1
for a,b being natural Number holds a in Seg b iff 1 <= a & a <= b;
registration let n be zero natural Number;
cluster Seg n -> empty;
end;
theorem :: FINSEQ_1:2
Seg 1 = { 1 } & Seg 2 = { 1,2 };
theorem :: FINSEQ_1:3
for a being natural Number holds a = 0 or a in Seg a;
registration let n be non zero natural Number;
cluster Seg n -> non empty;
end;
theorem :: FINSEQ_1:4
for a being natural Number holds a+1 in Seg(a+1);
theorem :: FINSEQ_1:5
for a,b being natural Number holds a <= b iff Seg a c= Seg b;
theorem :: FINSEQ_1:6
for a,b being natural Number holds Seg a = Seg b implies a = b;
theorem :: FINSEQ_1:7
for a,b,c being natural Number holds
c <= a implies Seg c = Seg a /\ Seg c;
theorem :: FINSEQ_1:8
for a,c being natural Number holds
Seg c = Seg c /\ Seg a implies c <= a;
theorem :: FINSEQ_1:9
for a being natural Number holds Seg a \/ { a+1 } = Seg (a+1);
theorem :: FINSEQ_1:10
for k being natural Number holds Seg k = Seg(k + 1) \ {k + 1};
:: Finite Sequences
definition
let IT be Relation;
attr IT is FinSequence-like means
:: FINSEQ_1:def 2
ex n st dom IT = Seg n;
end;
registration
cluster empty -> FinSequence-like for Relation;
end;
definition
mode FinSequence is FinSequence-like Function;
end;
reserve p,q,r,s,t for FinSequence;
registration
let n be natural Number;
cluster Seg n -> finite;
end;
registration
cluster FinSequence-like -> finite for Function;
end;
registration let n be natural Number;
cluster Seg n -> n-element;
end;
notation
let p;
synonym len p for card p;
end;
definition
let p;
redefine func len p -> Element of NAT means
:: FINSEQ_1:def 3
Seg it = dom p;
end;
definition
let p;
redefine func dom p -> Subset of NAT;
end;
theorem :: FINSEQ_1:11
(ex k st dom f c= Seg k) implies ex p st f c= p;
scheme :: FINSEQ_1:sch 1
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
for k st k in Seg A() ex x st P[k,x];
scheme :: FINSEQ_1:sch 2
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);
theorem :: FINSEQ_1:12
z in p implies ex k st k in dom p & z=[k,p.k];
theorem :: FINSEQ_1:13
dom p = dom q & (for k st k in dom p holds p.k = q.k) implies p=q;
theorem :: FINSEQ_1:14
len p = len q & (for k st 1 <= k & k <= len p holds p.k = q.k) implies p=q;
theorem :: FINSEQ_1:15
p|(Seg a) is FinSequence;
theorem :: FINSEQ_1:16
rng p c= dom f implies f*p is FinSequence;
theorem :: FINSEQ_1:17
a <= len p & q = p|(Seg a) implies len q = a & dom q = Seg a;
:: ::
:: FinSequences of D ::
:: ::
definition
let D be set;
mode FinSequence of D -> FinSequence means
:: FINSEQ_1:def 4
rng it c= D;
end;
registration
let D be set;
cluster -> D-valued for FinSequence of D;
end;
registration
cluster empty -> FinSequence-like for Relation;
end;
registration
let D be set;
cluster FinSequence-like for PartFunc of NAT,D;
end;
definition
let D be set;
redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT,D;
end;
reserve D for set;
theorem :: FINSEQ_1:18
for p being FinSequence of D holds p|(Seg a) is FinSequence of D;
theorem :: FINSEQ_1:19
for D being non empty set ex p being FinSequence of D st len p = a;
theorem :: FINSEQ_1:20
p <> {} iff len p >= 1;
definition
let x be object;
func <*x*> -> set equals
:: FINSEQ_1:def 5
{ [1,x] };
end;
definition
let D be set;
func <*>D -> FinSequence of D equals
:: FINSEQ_1:def 6
{};
end;
registration
let D be set;
cluster <*>D -> empty;
end;
registration
let D be set;
cluster empty for FinSequence of D;
end;
definition
let p,q;
func p^q -> FinSequence means
:: FINSEQ_1:def 7
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;
end;
theorem :: FINSEQ_1:21
p = (p ^ q) | (dom p);
theorem :: FINSEQ_1:22
len(p^q) = len p + len q;
theorem :: FINSEQ_1:23
for k being Nat st
len p + 1 <= k & k <= len p + len q holds (p^q).k=q.(k-len p);
theorem :: FINSEQ_1:24
for k being Nat st len p < k & k <= len(p^q) holds (p^q).k = q.(k - len p);
theorem :: FINSEQ_1:25
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 );
theorem :: FINSEQ_1:26
dom p c= dom(p^q);
theorem :: FINSEQ_1:27
x in dom q implies ex k st k=x & len p + k in dom(p^q);
theorem :: FINSEQ_1:28
k in dom q implies len p + k in dom(p^q);
theorem :: FINSEQ_1:29
rng p c= rng(p^q);
theorem :: FINSEQ_1:30
rng q c= rng(p^q);
theorem :: FINSEQ_1:31
rng(p^q) = rng p \/ rng q;
theorem :: FINSEQ_1:32
p^q^r = p^(q^r);
theorem :: FINSEQ_1:33
p^r = q^r or r^p = r^q implies p = q;
theorem :: FINSEQ_1:34
p^{} = p & {}^p = p;
theorem :: FINSEQ_1:35
p^q = {} implies p={} & q={};
definition
let D be set;
let p,q be FinSequence of D;
redefine func p^q -> FinSequence of D;
end;
definition
let x be object;
redefine func <*x*> -> Function means
:: FINSEQ_1:def 8
dom it = Seg 1 & it.1 = x;
end;
registration
let x be object;
cluster <*x*> -> Function-like Relation-like;
end;
registration
let x be object;
cluster <*x*> -> FinSequence-like;
end;
theorem :: FINSEQ_1:36
p^q is FinSequence of D implies p is FinSequence of D & q is FinSequence of D
;
definition
let x,y be object;
func <*x,y*> -> set equals
:: FINSEQ_1:def 9
<*x*>^<*y*>;
let z be object;
func <*x,y,z*> -> set equals
:: FINSEQ_1:def 10
<*x*>^<*y*>^<*z*>;
end;
registration
let x,y be object;
cluster <*x,y*> -> Function-like Relation-like;
let z be object;
cluster <*x,y,z*> -> Function-like Relation-like;
end;
registration
let x,y be object;
cluster <*x,y*> -> FinSequence-like;
let z be object;
cluster <*x,y,z*> -> FinSequence-like;
end;
theorem :: FINSEQ_1:37
for x being object holds <*x*> = { [1,x] };
theorem :: FINSEQ_1:38
for x being object holds p=<*x*> iff dom p = Seg 1 & rng p = {x};
theorem :: FINSEQ_1:39
for x being object holds p=<*x*> iff len p = 1 & rng p = {x};
theorem :: FINSEQ_1:40
for x being object holds p = <*x*> iff len p = 1 & p.1 = x;
theorem :: FINSEQ_1:41
for x being object holds (<*x*>^p).1 = x;
theorem :: FINSEQ_1:42
for x being object holds (p^<*x*>).(len p + 1)=x;
theorem :: FINSEQ_1:43
for x,y,z being object
holds <*x,y,z*>=<*x*>^<*y,z*> & <*x,y,z*>=<*x,y*>^<*z*>;
theorem :: FINSEQ_1:44
for x,y being object holds p = <*x,y*> iff len p = 2 & p.1=x & p.2=y;
theorem :: FINSEQ_1:45
for x,y,z being object
holds p = <*x,y,z*> iff len p = 3 & p.1 = x & p.2 = y & p.3 = z;
theorem :: FINSEQ_1:46
for x being object holds p <> {} implies ex q,x st p=q^<*x*>;
definition
let D be non empty set;
let x be Element of D;
redefine func <*x*> -> FinSequence of D;
end;
:: scheme of induction for finite sequences ::
scheme :: FINSEQ_1:sch 3
IndSeq{P[FinSequence]}: for p holds P[p]
provided
P[{}] and
for p,x st P[p] holds P[p^<*x*>];
theorem :: FINSEQ_1:47
for p,q,r,s being FinSequence st p^q = r^s & len p <= len r
ex t being FinSequence st p^t = r;
registration
cluster -> NAT-defined for FinSequence;
end;
definition
let D be set;
func D* -> set means
:: FINSEQ_1:def 11
x in it iff x is FinSequence of D;
end;
registration
let D be set;
cluster D* -> non empty;
end;
theorem :: FINSEQ_1:48
rng p = rng q & p is one-to-one & q is one-to-one implies len p = len q;
theorem :: FINSEQ_1:49
{} in D*;
scheme :: FINSEQ_1:sch 4
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;
:: ::
:: Subsequences ::
:: ::
definition
let IT be Function;
attr IT is FinSubsequence-like means
:: FINSEQ_1:def 12
ex k st dom IT c= Seg k;
end;
registration
cluster FinSubsequence-like for Function;
end;
definition
mode FinSubsequence is FinSubsequence-like Function;
end;
registration
cluster FinSequence-like -> FinSubsequence-like for Function;
let p be FinSubsequence, X be set;
cluster p|X -> FinSubsequence-like;
cluster X|`p -> FinSubsequence-like;
end;
registration
cluster -> NAT-defined for FinSubsequence;
end;
reserve p9 for FinSubsequence;
definition
let X;
given k being Nat such that
X c= Seg k;
func Sgm X -> FinSequence of NAT means
:: FINSEQ_1:def 13
rng it = X & for l,m,k1,k2 being Nat st 1 <= l & l < m & m <= len it &
k1=it.l & k2=it.m holds k1 < k2;
end;
theorem :: FINSEQ_1:50
rng Sgm dom p9 = dom p9;
definition
let p9;
func Seq p9 -> Function equals
:: FINSEQ_1:def 14
p9* Sgm(dom p9);
end;
registration
let p9;
cluster Seq p9 -> FinSequence-like;
end;
theorem :: FINSEQ_1:51
for X st ex k st X c= Seg k holds Sgm X = {} iff X = {};
begin :: from FINSET_1, 1998
theorem :: FINSEQ_1:52 :: FINSET_1:def 1
D is finite iff ex p st D = rng p;
begin :: Moved from CARD_1, 1999
theorem :: FINSEQ_1:53
Seg n,Seg m are_equipotent implies n = m;
theorem :: FINSEQ_1:54
Seg n,n are_equipotent;
theorem :: FINSEQ_1:55
card Seg n = card n;
theorem :: FINSEQ_1:56
X is finite implies ex n st X,Seg n are_equipotent;
theorem :: FINSEQ_1:57
for n being Nat holds card Seg n = n;
begin :: Addenda
:: from FINSEQ_5
registration
let x be object;
cluster <*x*> -> non empty;
end;
:: From SPRECT_1
registration
cluster non empty for FinSequence;
end;
:: From FUNCT_7, actually from GOBOARD4
registration
let f1 be FinSequence, f2 be non empty FinSequence;
cluster f1^f2 -> non empty;
cluster f2^f1 -> non empty;
end;
registration
let x,y be object;
cluster <*x,y*> -> non empty;
let z be object;
cluster <*x,y,z*> -> non empty;
end;
:: from MATRIX_2
scheme :: FINSEQ_1:sch 5
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
for k st k in Seg A() ex x being Element of D() st P[k,x];
:: from TOPREAL1
reserve D for set,
p for FinSequence of D,
m for Nat;
definition
let m;
let p be FinSequence;
func p|m -> FinSequence equals
:: FINSEQ_1:def 15
p|Seg m;
end;
definition
let D,m,p;
redefine func p|m -> FinSequence of D;
end;
registration
let f be FinSequence;
cluster f|0 -> empty;
end;
theorem :: FINSEQ_1:58
len q <= i implies q|i = q;
theorem :: FINSEQ_1:59
i <= len q implies len(q|i) = i;
:: from FSM_1
theorem :: FINSEQ_1:60
i in Seg n implies i+m in Seg (n+m);
theorem :: FINSEQ_1:61
i>0 & i+m in Seg (n+m) implies i in Seg n & i in Seg (n+m);
:: from LANG1
definition
let R be Relation;
func R[*] -> Relation means
:: FINSEQ_1:def 16
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;
end;
theorem :: FINSEQ_1:62
for D1,D2 being set st D1 c= D2 holds D1* c= D2*;
:: 2005.05.13, A.T.
registration
let D be set;
cluster D* -> functional;
end;
:: from SCMFSA_7, 2005.11.21, A.T.
theorem :: FINSEQ_1:63
for p,q being FinSequence st p c= q holds len p <= len q;
theorem :: FINSEQ_1:64
for p,q being FinSequence, i being Nat st
1 <= i & i <= len p holds (p ^ q).i = p.i;
theorem :: FINSEQ_1:65
for p,q being FinSequence, i being Nat st
1 <= i & i <= len q holds (p ^ q).(len p + i) = q.i;
:: from GRAPH_2, 2006.01.09, A.T.
scheme :: FINSEQ_1:sch 6
FinSegRng{n() -> Nat, F(set)->set, P[set]}:
{F(i) where i is Nat: i<=n() & P[i]} is finite;
theorem :: FINSEQ_1:66
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;
theorem :: FINSEQ_1:67
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;
theorem :: FINSEQ_1:68
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;
theorem :: FINSEQ_1:69
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;
theorem :: FINSEQ_1:70
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;
theorem :: FINSEQ_1:71
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;
:: from SCMFSA_7, 2006.03.14, A.T.
theorem :: FINSEQ_1:72
for p being FinSequence holds p | Seg 0 = {};
theorem :: FINSEQ_1:73
for f,g being FinSequence holds f | Seg 0 = g | Seg 0;
theorem :: FINSEQ_1:74
for D being non empty set, x being Element of D holds
<* x *> is FinSequence of D;
theorem :: FINSEQ_1:75
for D being set, p,q being FinSequence of D holds p ^ q is FinSequence of D;
:: from GROUP_7, 2007.02.10, AK
reserve a, b, c, d, e, f for object;
theorem :: FINSEQ_1:76
<*a*> = <*b*> implies a = b;
theorem :: FINSEQ_1:77
<*a,b*> = <*c,d*> implies a = c & b = d;
theorem :: FINSEQ_1:78
<*a,b,c*> = <*d,e,f*> implies a = d & b = e & c = f;
:: from PRVECT_1, 2007.03.09, A.T
registration
cluster non empty non-empty for FinSequence;
end;
theorem :: FINSEQ_1:79
for p,q being FinSequence st q = p|Seg n holds len q <= len p;
theorem :: FINSEQ_1:80
for p,r being FinSequence st r = p|Seg n ex q being FinSequence st p = r^q;
:: from GOBOARD1, PRALG_1, 2007.04.06, A.T
registration
let D be non empty set;
cluster non empty for FinSequence of D;
end;
:: Added by AK, 2007.11.07
definition
let p,q be FinSequence;
redefine pred p = q means
:: FINSEQ_1:def 17
len p = len q & for k st 1 <= k & k <= len p holds p.k = q.k;
end;
:: from GROEB_2, 2008.10.08, A.T.
::$CT
theorem :: FINSEQ_1:82
for p being FinSequence, n,m being Nat st m <= n holds p|n|m = p|m;
:: from CARD_5, 2008.10.08, A.T.
reserve m for Nat;
theorem :: FINSEQ_1:83
Seg n = (n+1) \ {0};
:: from CIRCCOMB, 2009.03.27, A.T.
registration
let n be natural Number;
cluster n-element for FinSequence;
end;
:: from FACIRC_1, 2009.02.16, A.T.
registration
let x be object;
cluster <*x*> -> 1-element;
let y be object;
cluster <*x,y*> -> 2-element;
let z be object;
cluster <*x,y,z*> -> 3-element;
end;
:: new, 2009.08.24, A.T.
definition let X be set;
attr X is FinSequence-membered means
:: FINSEQ_1:def 18
x in X implies x is FinSequence;
end;
registration
cluster empty -> FinSequence-membered for set;
end;
registration
cluster non empty FinSequence-membered for set;
end;
registration let X be set;
cluster X* -> FinSequence-membered;
end;
theorem :: FINSEQ_1:84
for f being Function st f in D* & x in dom f holds f.x in D;
registration
cluster FinSequence-membered -> functional for set;
end;
theorem :: FINSEQ_1:85
for X being FinSequence-membered set ex Y being non empty set st X c= Y*;
registration
let X be FinSequence-membered set;
cluster -> FinSequence-like for Element of X;
end;
registration let X be FinSequence-membered set;
cluster -> FinSequence-membered for Subset of X;
end;
:: from TREES_1, 2009.09.09, A.T.
theorem :: FINSEQ_1:86
for p,q being FinSequence st q = p|Seg n holds len q <= n;
theorem :: FINSEQ_1:87
for p,q being FinSequence st p = p^q or p = q^p holds q = {};
theorem :: FINSEQ_1:88
for p,q being FinSequence st p^q = <*x*> holds
p = <*x*> & q = {} or p = {} & q = <*x*>;
:: missing, 2009.09.26, A.T.
theorem :: FINSEQ_1:89
for f being n-element FinSequence holds dom f = Seg n;
registration let n,m be natural Number;
let f be n-element FinSequence, g be m-element FinSequence;
cluster f^g -> (n+m)-element;
end;
:: from JORDAN7, 2010.02.26, A.T
registration
cluster increasing -> one-to-one for real-valued FinSequence;
end;
:: from AMI_6, 2010.04.07, A.T.
theorem :: FINSEQ_1:90
for x, y being object st x in dom <*y*> holds x = 1;
:: from FOMODEL0, 2011.06.12, A.T.
registration let X;
cluster X-valued for FinSequence;
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;
end;
theorem :: FINSEQ_1:91
x in Seg n implies x = 1 or ... or x = n;
theorem :: FINSEQ_1:92
dom <*x,y*> = { 1,2 };
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;
end;
definition
let A be finite set;
func canFS A -> FinSequence of A equals
:: FINSEQ_1:def 19
the one-to-one onto FinSequence of A;
end;
registration
let A be finite set;
cluster canFS A -> one-to-one onto;
end;
theorem :: FINSEQ_1:93
for A being finite set holds len canFS A = card A;
registration
let A be finite non empty set;
cluster canFS A -> non empty;
end;
theorem :: FINSEQ_1:94
for a being object holds canFS({a}) = <* a *>;
theorem :: FINSEQ_1:95
for A being finite set holds (canFS A)" is Function of A, Seg card A;
:: from PNPROC_1, 2012.02.20, A.T.
theorem :: FINSEQ_1:96
i > 0 implies {[i,x]} is FinSubsequence;
theorem :: FINSEQ_1:97
for q being FinSubsequence holds q = {} iff Seq q = {};
registration
cluster -> finite for FinSubsequence;
end;
reserve x1,x2,y1,y2 for set;
theorem :: FINSEQ_1:98
{[x1,y1], [x2,y2]} is FinSequence implies x1 = 1 & x2 = 1 & y1 = y2 or
x1 = 1 & x2 = 2 or x1 = 2 & x2 = 1;
theorem :: FINSEQ_1:99
<*x1,x2*> = {[1,x1], [2,x2]};
reserve j for Nat;
theorem :: FINSEQ_1:100
for q being FinSubsequence holds dom Seq q = dom Sgm dom q;
theorem :: FINSEQ_1:101
for q being FinSubsequence holds rng q = rng Seq q;