:: Segments of Natural Numbers and Finite Sequences
:: by Grzegorz Bancerek and Krzysztof Hryniewiecki
::
:: Received April 1, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

:: Segments of Natural Numbers
definition
let n be Nat;
func Seg n ->  set  equals :: FINSEQ_1:def 1
 {  k where k is Element of NAT : ( 1 <= k &amp; k <= n )  }  ;
correctness
coherence
{  k where k is Element of NAT : ( 1 <= k &amp; k <= n )  }  is set ;
;
end;

:: deftheorem  defines Seg FINSEQ_1:def_1_:_
 for n being Nat holds Seg n =  {  k where k is Element of NAT : ( 1 <= k &amp; k <= n )  }  ;

definition
let n be Nat;
:: original:Seg
redefine func Seg n ->  Subset of NAT;
coherence
 Seg n is Subset of NAT
proofend;
end;

theorem Th1: :: FINSEQ_1:1
for a, b being Nat holds
( a in Seg b iff ( 1 <= a &amp; a <= b ) )
proofend;

registration
let n be zero Nat;
cluster Seg n ->  empty ;
coherence
 Seg n is empty
proofend;
end;

theorem Th2: :: FINSEQ_1:2
( Seg 1 = {1} &amp; Seg 2 = {1,2} )
proofend;

theorem Th3: :: FINSEQ_1:3
for a being Nat holds
( a = 0 or a in Seg a )
proofend;

registration
let n be non zero Nat;
cluster Seg n ->  non empty ;
coherence
 not Seg n is empty by Th3;
end;

theorem :: FINSEQ_1:4
for a being Nat holds a + 1 in Seg (a + 1) by Th3;

theorem Th5: :: FINSEQ_1:5
for a, b being Nat holds
( a <= b iff Seg a c= Seg b )
proofend;

theorem Th6: :: FINSEQ_1:6
for a, b being Nat st Seg a = Seg b holds
a = b
proofend;

theorem Th7: :: FINSEQ_1:7
for c, a being Nat st c <= a holds
Seg c = (Seg a) /\ (Seg c)
proofend;

theorem :: FINSEQ_1:8
for c, a being Nat st Seg c = (Seg c) /\ (Seg a) holds
c <= a by Th6, Th7;

theorem Th9: :: FINSEQ_1:9
for a being Nat holds (Seg a) \/ {(a + 1)} = Seg (a + 1)
proofend;

theorem :: FINSEQ_1:10
for k being Nat holds Seg k = (Seg (k + 1)) \ {(k + 1)}
proofend;

:: Finite Sequences
definition
let IT be Relation;
attrIT is FinSequence-like  means :Def2: :: FINSEQ_1:def 2
 ex n being Nat st dom IT = Seg n;
end;

:: deftheorem Def2 defines FinSequence-like FINSEQ_1:def_2_:_
 for IT being Relation holds
( IT is FinSequence-like iff ex n being Nat st dom IT = Seg n );

registration
cluster Relation-like empty  ->  FinSequence-like for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is FinSequence-like
proofend;
end;

definition
mode FinSequence is FinSequence-like Function;
end;

defpred S1[ set , set ] means  ex k being Nat st
( $1 = k &amp; $2 = k + 1 );

registration
let n be Nat;
cluster Seg n ->  finite ;
coherence
 Seg n is finite
proofend;
end;

registration
cluster Relation-like Function-like FinSequence-like  ->  finite for set ;
coherence
 for b1 being Function st b1 is FinSequence-like holds
b1 is finite
proofend;
end;

Lm1:  for n being Nat holds Seg n,n are_equipotent
proofend;

Lm2:  for n being Nat holds card (Seg n) = card n
proofend;

registration
let n be Nat;
cluster Seg n -> n -element ;
coherence
 Seg n is n -element
proofend;
end;

notation
let p be FinSequence;
synonym  len p for  card p;
end;

definition
let p be FinSequence;
:: original:len
redefine func len p ->  Element of NAT  means :Def3: :: FINSEQ_1:def 3
 Seg it = dom p;
coherence
 len p is Element of NAT
proofend;
compatibility
 for b1 being Element of NAT holds
( b1 = len p iff Seg b1 = dom p )
proofend;
end;

:: deftheorem Def3 defines len FINSEQ_1:def_3_:_
 for p being FinSequence
for b2 being Element of NAT holds
( b2 = len p iff Seg b2 = dom p );

definition
let p be FinSequence;
:: original:dom
redefine func dom p ->  Subset of NAT;
coherence
 dom p is Subset of NAT
proofend;
end;

theorem :: FINSEQ_1:11
for f being Function st ex k being Nat st dom f c= Seg k holds
ex p being FinSequence st f c= p
proofend;

scheme :: FINSEQ_1:sch 1
SeqEx{ F1() ->  Nat, P1[ set , set ] } :
 ex p being FinSequence st
( dom p = Seg F1() &amp; ( for k being Nat st k in Seg F1() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in Seg F1() holds
ex x being set st P1[k,x]
proofend;

scheme :: FINSEQ_1:sch 2
SeqLambda{ F1() ->  Nat, F2( set ) ->  set } :
 ex p being FinSequence st
( len p = F1() &amp; ( for k being Nat st k in dom p holds
p . k = F2(k) ) )
proofend;

theorem :: FINSEQ_1:12
for z being set
for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p &amp; z = [k,(p . k)] )
proofend;

theorem Th13: :: FINSEQ_1:13
for p, q being FinSequence st dom p = dom q &amp; ( for k being Nat st k in dom p holds
p . k = q . k ) holds
p = q
proofend;

theorem Th14: :: FINSEQ_1:14
for p, q being FinSequence st len p = len q &amp; ( for k being Nat st 1 <= k &amp; k <= len p holds
p . k = q . k ) holds
p = q
proofend;

theorem Th15: :: FINSEQ_1:15
for a being Nat
for p being FinSequence holds p | (Seg a) is FinSequence
proofend;

theorem :: FINSEQ_1:16
for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence
proofend;

theorem Th17: :: FINSEQ_1:17
for a being Nat
for p, q being FinSequence st a <= len p &amp; q = p | (Seg a) holds
( len q = a &amp; dom q = Seg a )
proofend;

:: ::
:: FinSequences of D ::
:: ::
definition
let D be set ;
mode FinSequence of D ->  FinSequence means :Def4: :: FINSEQ_1:def 4
 rng it c= D;
existence
 ex b1 being FinSequence st rng b1 c= D
proofend;
end;

:: deftheorem Def4 defines FinSequence FINSEQ_1:def_4_:_
 for D being set
for b2 being FinSequence holds
( b2 is FinSequence of D iff rng b2 c= D );

registration
let D be set ;
cluster  -> D -valued for FinSequence of D;
coherence
 for b1 being FinSequence of D holds b1 is D -valued
proofend;
end;

Lm3:  for D being set
for f being FinSequence of D holds f is PartFunc of NAT,D
proofend;

registration
cluster Relation-like empty  ->  FinSequence-like for set ;
coherence
 for b1 being Relation st b1 is empty holds
b1 is FinSequence-like ;
end;

registration
let D be set ;
cluster Relation-like NAT -defined D -valued Function-like FinSequence-like for Element of bool [:NAT,D:];
existence
 ex b1 being PartFunc of NAT,D st b1 is FinSequence-like
proofend;
end;

definition
let D be set ;
:: original:FinSequence
redefine mode FinSequence of D ->  FinSequence-like PartFunc of NAT,D;
coherence
 for b1 being FinSequence of D holds b1 is FinSequence-like PartFunc of NAT,D by Lm3;
end;

theorem Th18: :: FINSEQ_1:18
for a being Nat
for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D
proofend;

theorem :: FINSEQ_1:19
for a being Nat
for D being non empty set ex p being FinSequence of D st len p = a
proofend;

Lm4:  for q being FinSequence holds
( q = {} iff len q = 0 )
;

theorem :: FINSEQ_1:20
for p being FinSequence holds
( p <> {} iff len p >= 1 )
proofend;

definition
let x be set ;
func<*x*> ->  set  equals :: FINSEQ_1:def 5
{[1,x]};
coherence
 {[1,x]} is set ;
end;

:: deftheorem  defines <* FINSEQ_1:def_5_:_
 for x being set holds <*x*> = {[1,x]};

definition
let D be set ;
func <*> D ->  FinSequence of D equals :: FINSEQ_1:def 6
 {} ;
coherence
 {} is FinSequence of D
proofend;
end;

:: deftheorem  defines <*> FINSEQ_1:def_6_:_
 for D being set holds <*> D = {} ;

registration
let D be set ;
cluster <*> D ->  empty ;
coherence
 <*> D is empty ;
end;

registration
let D be set ;
cluster Relation-like NAT -defined D -valued Function-like empty finite FinSequence-like for FinSequence of D;
existence
 ex b1 being FinSequence of D st b1 is empty
proofend;
end;

definition
let p, q be FinSequence;
funcp ^ q ->  FinSequence means :Def7: :: FINSEQ_1:def 7
( dom it = Seg ((len p) + (len q)) &amp; ( for k being Nat st k in dom p holds
it . k = p . k ) &amp; ( for k being Nat st k in dom q holds
it . ((len p) + k) = q . k ) );
existence
 ex b1 being FinSequence st
( dom b1 = Seg ((len p) + (len q)) &amp; ( for k being Nat st k in dom p holds
b1 . k = p . k ) &amp; ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) )
proofend;
uniqueness
 for b1, b2 being FinSequence st dom b1 = Seg ((len p) + (len q)) &amp; ( for k being Nat st k in dom p holds
b1 . k = p . k ) &amp; ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) &amp; dom b2 = Seg ((len p) + (len q)) &amp; ( for k being Nat st k in dom p holds
b2 . k = p . k ) &amp; ( for k being Nat st k in dom q holds
b2 . ((len p) + k) = q . k ) holds
b1 = b2
proofend;
end;

:: deftheorem Def7 defines ^ FINSEQ_1:def_7_:_
 for p, q being FinSequence
for b3 being FinSequence holds
( b3 = p ^ q iff ( dom b3 = Seg ((len p) + (len q)) &amp; ( for k being Nat st k in dom p holds
b3 . k = p . k ) &amp; ( for k being Nat st k in dom q holds
b3 . ((len p) + k) = q . k ) ) );

theorem Th21: :: FINSEQ_1:21
for p, q being FinSequence holds p = (p ^ q) | (dom p)
proofend;

theorem Th22: :: FINSEQ_1:22
for p, q being FinSequence holds len (p ^ q) = (len p) + (len q)
proofend;

theorem Th23: :: FINSEQ_1:23
for p, q being FinSequence
for k being Nat st (len p) + 1 <= k &amp; k <= (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))
proofend;

theorem Th24: :: FINSEQ_1:24
for p, q being FinSequence
for k being Nat st len p < k &amp; k <= len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))
proofend;

theorem Th25: :: FINSEQ_1:25
for p, q being FinSequence
for k being Nat holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q &amp; k = (len p) + n ) )
proofend;

theorem Th26: :: FINSEQ_1:26
for p, q being FinSequence holds dom p c= dom (p ^ q)
proofend;

theorem Th27: :: FINSEQ_1:27
for x being set
for q, p being FinSequence st x in dom q holds
ex k being Nat st
( k = x &amp; (len p) + k in dom (p ^ q) )
proofend;

theorem Th28: :: FINSEQ_1:28
for k being Nat
for q, p being FinSequence st k in dom q holds
(len p) + k in dom (p ^ q)
proofend;

theorem Th29: :: FINSEQ_1:29
for p, q being FinSequence holds rng p c= rng (p ^ q)
proofend;

theorem Th30: :: FINSEQ_1:30
for q, p being FinSequence holds rng q c= rng (p ^ q)
proofend;

theorem Th31: :: FINSEQ_1:31
for p, q being FinSequence holds rng (p ^ q) = (rng p) \/ (rng q)
proofend;

theorem Th32: :: FINSEQ_1:32
for p, q, r being FinSequence holds (p ^ q) ^ r = p ^ (q ^ r)
proofend;

theorem :: FINSEQ_1:33
for p, r, q being FinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q
proofend;

theorem Th34: :: FINSEQ_1:34
for p being FinSequence holds
( p ^ {} = p &amp; {} ^ p = p )
proofend;

theorem Th35: :: FINSEQ_1:35
for p, q being FinSequence st p ^ q = {} holds
( p = {} &amp; q = {} )
proofend;

definition
let D be set ;
let p, q be FinSequence of D;
:: original:^
redefine funcp ^ q ->  FinSequence of D;
coherence
 p ^ q is FinSequence of D
proofend;
end;

Lm5:  for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 &amp; y = y1 )
proofend;

definition
let x be set ;
:: original:<*
redefine func<*x*> ->  Function means :Def8: :: FINSEQ_1:def 8
( dom it = Seg 1 &amp; it . 1 = x );
coherence
 <*x*> is Function ;
compatibility
 for b1 being Function holds
( b1 = <*x*> iff ( dom b1 = Seg 1 &amp; b1 . 1 = x ) )
proofend;
end;

:: deftheorem Def8 defines <* FINSEQ_1:def_8_:_
 for x being set
for b2 being Function holds
( b2 = <*x*> iff ( dom b2 = Seg 1 &amp; b2 . 1 = x ) );

registration
let x be set ;
cluster<*x*> ->  Relation-like Function-like ;
coherence
 ( <*x*> is Function-like &amp; <*x*> is Relation-like ) ;
end;

registration
let x be set ;
cluster<*x*> ->  FinSequence-like ;
coherence
 <*x*> is FinSequence-like
proofend;
end;

theorem Th36: :: FINSEQ_1:36
for p, q being FinSequence
for D being set st p ^ q is FinSequence of D holds
( p is FinSequence of D &amp; q is FinSequence of D )
proofend;

definition
let x, y be set ;
func<*x,y*> ->  set  equals :: FINSEQ_1:def 9
<*x*> ^ <*y*>;
correctness
coherence
<*x*> ^ <*y*> is set ;
;
let z be set ;
func<*x,y,z*> ->  set  equals :: FINSEQ_1:def 10
(<*x*> ^ <*y*>) ^ <*z*>;
correctness
coherence
(<*x*> ^ <*y*>) ^ <*z*> is set ;
;
end;

:: deftheorem  defines <* FINSEQ_1:def_9_:_
 for x, y being set holds <*x,y*> = <*x*> ^ <*y*>;

:: deftheorem  defines <* FINSEQ_1:def_10_:_
 for x, y, z being set holds <*x,y,z*> = (<*x*> ^ <*y*>) ^ <*z*>;

registration
let x, y be set ;
cluster<*x,y*> ->  Relation-like Function-like ;
coherence
 ( <*x,y*> is Function-like &amp; <*x,y*> is Relation-like ) ;
let z be set ;
cluster<*x,y,z*> ->  Relation-like Function-like ;
coherence
 ( <*x,y,z*> is Function-like &amp; <*x,y,z*> is Relation-like ) ;
end;

registration
let x, y be set ;
cluster<*x,y*> ->  FinSequence-like ;
coherence
 <*x,y*> is FinSequence-like ;
let z be set ;
cluster<*x,y,z*> ->  FinSequence-like ;
coherence
 <*x,y,z*> is FinSequence-like ;
end;

theorem :: FINSEQ_1:37
for x being set holds <*x*> = {[1,x]} ;

theorem Th38: :: FINSEQ_1:38
for x being set
for p being FinSequence holds
( p = <*x*> iff ( dom p = Seg 1 &amp; rng p = {x} ) )
proofend;

theorem Th39: :: FINSEQ_1:39
for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 &amp; rng p = {x} ) )
proofend;

theorem Th40: :: FINSEQ_1:40
for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 &amp; p . 1 = x ) )
proofend;

theorem :: FINSEQ_1:41
for x being set
for p being FinSequence holds (<*x*> ^ p) . 1 = x
proofend;

theorem Th42: :: FINSEQ_1:42
for x being set
for p being FinSequence holds (p ^ <*x*>) . ((len p) + 1) = x
proofend;

theorem :: FINSEQ_1:43
for x, y, z being set holds
( <*x,y,z*> = <*x*> ^ <*y,z*> &amp; <*x,y,z*> = <*x,y*> ^ <*z*> ) by Th32;

theorem Th44: :: FINSEQ_1:44
for x, y being set
for p being FinSequence holds
( p = <*x,y*> iff ( len p = 2 &amp; p . 1 = x &amp; p . 2 = y ) )
proofend;

theorem Th45: :: FINSEQ_1:45
for x, y, z being set
for p being FinSequence holds
( p = <*x,y,z*> iff ( len p = 3 &amp; p . 1 = x &amp; p . 2 = y &amp; p . 3 = z ) )
proofend;

theorem Th46: :: FINSEQ_1:46
for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being set st p = q ^ <*x*>
proofend;

definition
let D be non empty set ;
let x be Element of D;
:: original:<*
redefine func<*x*> ->  FinSequence of D;
coherence
 <*x*> is FinSequence of D
proofend;
end;

:: scheme of induction for finite sequences ::
scheme :: FINSEQ_1:sch 3
IndSeq{ P1[ FinSequence] } :
 for p being FinSequence holds P1[p]
provided
A1: P1[ {} ] and
A2: for p being FinSequence
for x being set st P1[p] holds
P1[p ^ <*x*>]
proofend;

theorem :: FINSEQ_1:47
for p, q, r, s being FinSequence st p ^ q = r ^ s &amp; len p <= len r holds
ex t being FinSequence st p ^ t = r
proofend;

registration
cluster Relation-like Function-like FinSequence-like  ->  NAT -defined for set ;
coherence
 for b1 being FinSequence holds b1 is NAT -defined
proofend;
end;

definition
let D be set ;
funcD *  ->  set  means :Def11: :: FINSEQ_1:def 11
 for x being set holds
( x in it iff x is FinSequence of D );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff x is FinSequence of D )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is FinSequence of D ) ) &amp; ( for x being set holds
( x in b2 iff x is FinSequence of D ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines * FINSEQ_1:def_11_:_
 for D, b2 being set holds
( b2 = D * iff for x being set holds
( x in b2 iff x is FinSequence of D ) );

registration
let D be set ;
clusterD *  ->  non empty ;
coherence
 not D * is empty
proofend;
end;

theorem :: FINSEQ_1:48
for p, q being FinSequence st rng p = rng q &amp; p is one-to-one &amp; q is one-to-one holds
len p = len q
proofend;

theorem :: FINSEQ_1:49
for D being set holds {} in D *
proofend;

scheme :: FINSEQ_1:sch 4
SepSeq{ F1() ->  non empty set , P1[ FinSequence] } :
 ex X being set st
for x being set holds
( x in X iff ex p being FinSequence st
( p in F1() * &amp; P1[p] &amp; x = p ) )
proofend;

:: ::
:: Subsequences ::
:: ::
definition
let IT be Function;
attrIT is FinSubsequence-like  means :Def12: :: FINSEQ_1:def 12
 ex k being Nat st dom IT c= Seg k;
end;

:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def_12_:_
 for IT being Function holds
( IT is FinSubsequence-like iff ex k being Nat st dom IT c= Seg k );

registration
cluster Relation-like Function-like FinSubsequence-like for set ;
existence
 ex b1 being Function st b1 is FinSubsequence-like
proofend;
end;

definition
mode FinSubsequence is FinSubsequence-like Function;
end;

registration
cluster Relation-like Function-like FinSequence-like  ->  FinSubsequence-like for set ;
coherence
 for b1 being Function st b1 is FinSequence-like holds
b1 is FinSubsequence-like
proofend;
let p be FinSubsequence;
let X be set ;
clusterp | X ->  FinSubsequence-like ;
coherence
 p | X is FinSubsequence-like
proofend;
clusterX |` p ->  FinSubsequence-like ;
coherence
 X |` p is FinSubsequence-like
proofend;
end;

registration
cluster Relation-like Function-like FinSubsequence-like  ->  NAT -defined for set ;
coherence
 for b1 being FinSubsequence holds b1 is NAT -defined
proofend;
end;

definition
let X be set ;
given k being Nat such that A1: X c= Seg k ;
func Sgm X ->  FinSequence of NAT  means :Def13: :: FINSEQ_1:def 13
( rng it = X &amp; ( for l, m, k1, k2 being Nat st 1 <= l &amp; l < m &amp; m <= len it &amp; k1 = it . l &amp; k2 = it . m holds
k1 < k2 ) );
existence
 ex b1 being FinSequence of NAT st
( rng b1 = X &amp; ( for l, m, k1, k2 being Nat st 1 <= l &amp; l < m &amp; m <= len b1 &amp; k1 = b1 . l &amp; k2 = b1 . m holds
k1 < k2 ) )
proofend;
uniqueness
 for b1, b2 being FinSequence of NAT st rng b1 = X &amp; ( for l, m, k1, k2 being Nat st 1 <= l &amp; l < m &amp; m <= len b1 &amp; k1 = b1 . l &amp; k2 = b1 . m holds
k1 < k2 ) &amp; rng b2 = X &amp; ( for l, m, k1, k2 being Nat st 1 <= l &amp; l < m &amp; m <= len b2 &amp; k1 = b2 . l &amp; k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines Sgm FINSEQ_1:def_13_:_
 for X being set st ex k being Nat st X c= Seg k holds
for b2 being FinSequence of NAT holds
( b2 = Sgm X iff ( rng b2 = X &amp; ( for l, m, k1, k2 being Nat st 1 <= l &amp; l < m &amp; m <= len b2 &amp; k1 = b2 . l &amp; k2 = b2 . m holds
k1 < k2 ) ) );

theorem Th50: :: FINSEQ_1:50
for p9 being FinSubsequence holds rng (Sgm (dom p9)) = dom p9
proofend;

definition
let p9 be FinSubsequence;
func Seq p9 ->  Function equals :: FINSEQ_1:def 14
p9 * (Sgm (dom p9));
coherence
 p9 * (Sgm (dom p9)) is Function ;
end;

:: deftheorem  defines Seq FINSEQ_1:def_14_:_
 for p9 being FinSubsequence holds Seq p9 = p9 * (Sgm (dom p9));

registration
let p9 be FinSubsequence;
cluster Seq p9 ->  FinSequence-like ;
coherence
 Seq p9 is FinSequence-like
proofend;
end;

theorem :: FINSEQ_1:51
for X being set st ex k being Nat st X c= Seg k holds
( Sgm X = {} iff X = {} )
proofend;

begin

theorem :: FINSEQ_1:52
for D being set holds
( D is finite iff ex p being FinSequence st D = rng p )
proofend;

begin

theorem :: FINSEQ_1:53
for n, m being Nat st Seg n, Seg m are_equipotent holds
n = m
proofend;

theorem :: FINSEQ_1:54
for n being Nat holds Seg n,n are_equipotent by Lm1;

theorem :: FINSEQ_1:55
for n being Nat holds card (Seg n) = card n by Lm2;

theorem :: FINSEQ_1:56
for X being set st X is finite holds
ex n being Nat st X, Seg n are_equipotent
proofend;

theorem :: FINSEQ_1:57
for n being Nat holds card (Seg n) = n
proofend;

begin

:: from FINSEQ_5
registration
let x be set ;
cluster<*x*> ->  non empty ;
coherence
 not <*x*> is empty ;
end;

:: From SPRECT_1
registration
cluster Relation-like NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like for set ;
existence
 not for b1 being FinSequence holds b1 is empty
proofend;
end;

:: From FUNCT_7, actually from GOBOARD4
registration
let f1 be FinSequence;
let f2 be non empty FinSequence;
clusterf1 ^ f2 ->  non empty ;
coherence
 not f1 ^ f2 is empty by Th35;
clusterf2 ^ f1 ->  non empty ;
coherence
 not f2 ^ f1 is empty by Th35;
end;

registration
let x, y be set ;
cluster<*x,y*> ->  non empty ;
coherence
 not <*x,y*> is empty ;
let z be set ;
cluster<*x,y,z*> ->  non empty ;
coherence
 not <*x,y,z*> is empty ;
end;

:: from MATRIX_2
scheme :: FINSEQ_1:sch 5
SeqDEx{ F1() ->  non empty set , F2() ->  Nat, P1[ set , set ] } :
 ex p being FinSequence of F1() st
( dom p = Seg F2() &amp; ( for k being Nat st k in Seg F2() holds
P1[k,p . k] ) )
provided
A1: for k being Nat st k in Seg F2() holds
ex x being Element of F1() st P1[k,x]
proofend;

definition
let m be Nat;
let p be FinSequence;
funcp | m ->  FinSequence equals :: FINSEQ_1:def 15
p | (Seg m);
coherence
 p | (Seg m) is FinSequence by Th15;
end;

:: deftheorem  defines | FINSEQ_1:def_15_:_
 for m being Nat
for p being FinSequence holds p | m = p | (Seg m);

definition
let D be set ;
let m be Nat;
let p be FinSequence of D;
:: original:|
redefine funcp | m ->  FinSequence of D;
coherence
 p | m is FinSequence of D by Th18;
end;

registration
let f be FinSequence;
clusterf | 0 ->  empty ;
coherence
 f | 0 is empty ;
end;

theorem :: FINSEQ_1:58
for i being Nat
for q being FinSequence st len q <= i holds
q | i = q
proofend;

theorem :: FINSEQ_1:59
for i being Nat
for q being FinSequence st i <= len q holds
len (q | i) = i
proofend;

:: from FSM_1
theorem :: FINSEQ_1:60
for i, n, m being Nat st i in Seg n holds
i + m in Seg (n + m)
proofend;

theorem :: FINSEQ_1:61
for i, n, m being Nat st i > 0 &amp; i + m in Seg (n + m) holds
( i in Seg n &amp; i in Seg (n + m) )
proofend;

:: from LANG1
definition
let R be Relation;
funcR [*]  ->  Relation means :: FINSEQ_1:def 16
 for x, y being set holds
( [x,y] in it iff ( x in field R &amp; y in field R &amp; ex p being FinSequence st
( len p >= 1 &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for i being Nat st i >= 1 &amp; i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) );
existence
 ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in field R &amp; y in field R &amp; ex p being FinSequence st
( len p >= 1 &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for i being Nat st i >= 1 &amp; i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) )
proofend;
uniqueness
 for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in field R &amp; y in field R &amp; ex p being FinSequence st
( len p >= 1 &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for i being Nat st i >= 1 &amp; i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) &amp; ( for x, y being set holds
( [x,y] in b2 iff ( x in field R &amp; y in field R &amp; ex p being FinSequence st
( len p >= 1 &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for i being Nat st i >= 1 &amp; i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines [*] FINSEQ_1:def_16_:_
 for R, b2 being Relation holds
( b2 = R [*] iff for x, y being set holds
( [x,y] in b2 iff ( x in field R &amp; y in field R &amp; ex p being FinSequence st
( len p >= 1 &amp; p . 1 = x &amp; p . (len p) = y &amp; ( for i being Nat st i >= 1 &amp; i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) ) );

theorem :: FINSEQ_1:62
for D1, D2 being set st D1 c= D2 holds
D1 * c= D2 *
proofend;

:: 2005.05.13, A.T.
registration
let D be set ;
clusterD *  ->  functional ;
coherence
 D * is functional
proofend;
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
proofend;

theorem :: FINSEQ_1:64
for p, q being FinSequence
for i being Nat st 1 <= i &amp; i <= len p holds
(p ^ q) . i = p . i
proofend;

theorem :: FINSEQ_1:65
for p, q being FinSequence
for i being Nat st 1 <= i &amp; i <= len q holds
(p ^ q) . ((len p) + i) = q . i
proofend;

:: from GRAPH_2, 2006.01.09, A.T.
scheme :: FINSEQ_1:sch 6
FinSegRng{ F1() ->  Nat, F2() ->  Nat, F3( set ) ->  set , P1[ set ] } :
  {  F3(i) where i is Element of NAT : ( F1() <= i &amp; i <= F2() &amp; P1[i] )  }  is finite
proofend;

Lm6:  ( 1 in Seg 3 &amp; 2 in Seg 3 )
;

Lm7:  3 in Seg 3
;

Lm8:  ( 1 in Seg 4 &amp; 2 in Seg 4 )
;

Lm9:  ( 3 in Seg 4 &amp; 4 in Seg 4 )
;

Lm10:  ( 1 in Seg 5 &amp; 2 in Seg 5 )
;

Lm11:  ( 3 in Seg 5 &amp; 4 in Seg 5 )
;

Lm12:  5 in Seg 5
;

Lm13:  ( 1 in Seg 6 &amp; 2 in Seg 6 )
;

Lm14:  ( 3 in Seg 6 &amp; 4 in Seg 6 )
;

Lm15:  ( 5 in Seg 6 &amp; 6 in Seg 6 )
;

Lm16:  ( 1 in Seg 7 &amp; 2 in Seg 7 )
;

Lm17:  ( 3 in Seg 7 &amp; 4 in Seg 7 )
;

Lm18:  ( 5 in Seg 7 &amp; 6 in Seg 7 )
;

Lm19:  7 in Seg 7
;

Lm20:  ( 1 in Seg 8 &amp; 2 in Seg 8 )
;

Lm21:  ( 3 in Seg 8 &amp; 4 in Seg 8 )
;

Lm22:  ( 5 in Seg 8 &amp; 6 in Seg 8 )
;

Lm23:  ( 7 in Seg 8 &amp; 8 in Seg 8 )
;

theorem Th66: :: FINSEQ_1:66
for x1, x2, x3, x4 being set
for p being FinSequence st p = ((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*> holds
( len p = 4 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 )
proofend;

theorem Th67: :: FINSEQ_1:67
for x1, x2, x3, x4, x5 being set
for p being FinSequence st p = (((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*> holds
( len p = 5 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 &amp; p . 5 = x5 )
proofend;

theorem Th68: :: FINSEQ_1:68
for x1, x2, x3, x4, x5, x6 being set
for p being FinSequence st p = ((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*> holds
( len p = 6 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 &amp; p . 5 = x5 &amp; p . 6 = x6 )
proofend;

theorem Th69: :: FINSEQ_1:69
for x1, x2, x3, x4, x5, x6, x7 being set
for p being FinSequence st p = (((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*> holds
( len p = 7 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 &amp; p . 5 = x5 &amp; p . 6 = x6 &amp; p . 7 = x7 )
proofend;

theorem Th70: :: FINSEQ_1:70
for x1, x2, x3, x4, x5, x6, x7, x8 being set
for p being FinSequence st p = ((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*> holds
( len p = 8 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 &amp; p . 5 = x5 &amp; p . 6 = x6 &amp; p . 7 = x7 &amp; p . 8 = x8 )
proofend;

theorem :: FINSEQ_1:71
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set
for p being FinSequence st p = (((((((<*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*> holds
( len p = 9 &amp; p . 1 = x1 &amp; p . 2 = x2 &amp; p . 3 = x3 &amp; p . 4 = x4 &amp; p . 5 = x5 &amp; p . 6 = x6 &amp; p . 7 = x7 &amp; p . 8 = x8 &amp; p . 9 = x9 )
proofend;

:: 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
for x being Element of D holds <*x*> is FinSequence of D ;

theorem :: FINSEQ_1:75
for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D ;

theorem :: FINSEQ_1:76
for a, b being set st <*a*> = <*b*> holds
a = b
proofend;

theorem :: FINSEQ_1:77
for a, b, c, d being set st <*a,b*> = <*c,d*> holds
( a = c &amp; b = d )
proofend;

theorem :: FINSEQ_1:78
for a, b, c, d, e, f being set st <*a,b,c*> = <*d,e,f*> holds
( a = d &amp; b = e &amp; c = f )
proofend;

:: from PRVECT_1, 2007.03.09, A.T
registration
cluster Relation-like non-empty NAT -defined Function-like non empty finite FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st
( not b1 is empty &amp; b1 is non-empty )
proofend;
end;

theorem Th79: :: FINSEQ_1:79
for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p
proofend;

theorem :: FINSEQ_1:80
for n being Nat
for p, r being FinSequence st r = p | (Seg n) holds
ex q being FinSequence st p = r ^ q
proofend;

:: from GOBOARD1, PRALG_1, 2007.04.06, A.T
registration
let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like for FinSequence of D;
existence
 not for b1 being FinSequence of D holds b1 is empty
proofend;
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 &amp; ( for k being Nat st 1 <= k &amp; k <= len p holds
p . k = q . k ) );
compatibility
 ( p = q iff ( len p = len q &amp; ( for k being Nat st 1 <= k &amp; k <= len p holds
p . k = q . k ) ) ) by Th14;
end;

:: deftheorem  defines = FINSEQ_1:def_17_:_
 for p, q being FinSequence holds
( p = q iff ( len p = len q &amp; ( for k being Nat st 1 <= k &amp; k <= len p holds
p . k = q . k ) ) );

:: from MATRIX_1, 2007.07.22, A.T generalized
theorem :: FINSEQ_1:81
for M1, M2 being set st card M1 = 0 &amp; card M2 = 0 holds
M1 = M2
proofend;

:: from CHAIN_1, 2008.08.31, A.K.
registration
let n be non zero Nat;
cluster Seg n ->  non empty ;
coherence
 not Seg n is empty ;
end;

:: from GROEB_2, 2008.10.08, A.T.
theorem :: FINSEQ_1:82
for p being FinSequence
for n, m being Nat st m <= n holds
(p | n) | m = p | m
proofend;

theorem :: FINSEQ_1:83
for n being Nat holds Seg n = (n + 1) \ {0}
proofend;

:: from CIRCCOMB, 2009.03.27, A.T.
registration
let n be Nat;
cluster Relation-like NAT -defined Function-like finite n -element FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st b1 is n -element
proofend;
end;

:: from FACIRC_1, 2009.02.16, A.T.
registration
let x be set ;
cluster<*x*> -> 1 -element ;
coherence
 <*x*> is 1 -element ;
let y be set ;
cluster<*x,y*> -> 2 -element ;
coherence
 <*x,y*> is 2 -element
proofend;
let z be set ;
cluster<*x,y,z*> -> 3 -element ;
coherence
 <*x,y,z*> is 3 -element
proofend;
end;

:: new, 2009.08.24, A.T.
definition
let X be set ;
attrX is FinSequence-membered  means :Def18: :: FINSEQ_1:def 18
 for x being set st x in X holds
x is FinSequence;
end;

:: deftheorem Def18 defines FinSequence-membered FINSEQ_1:def_18_:_
 for X being set holds
( X is FinSequence-membered iff for x being set st x in X holds
x is FinSequence );

registration
cluster empty  ->  FinSequence-membered for set ;
coherence
 for b1 being set st b1 is empty holds
b1 is FinSequence-membered
proofend;
end;

registration
cluster non empty FinSequence-membered for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is FinSequence-membered )
proofend;
end;

registration
let X be set ;
clusterX *  ->  FinSequence-membered ;
coherence
 X * is FinSequence-membered
proofend;
end;

theorem :: FINSEQ_1:84
for x, D being set
for f being Function st f in D * &amp; x in dom f holds
f . x in D
proofend;

registration
cluster FinSequence-membered  ->  functional for set ;
coherence
 for b1 being set st b1 is FinSequence-membered holds
b1 is functional
proofend;
end;

theorem :: FINSEQ_1:85
for X being FinSequence-membered set ex Y being non empty set st X c= Y *
proofend;

registration
let X be FinSequence-membered set ;
cluster  ->  FinSequence-like for Element of X;
coherence
 for b1 being Element of X holds b1 is FinSequence-like
proofend;
end;

registration
let X be FinSequence-membered set ;
cluster  ->  FinSequence-membered for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is FinSequence-membered
proofend;
end;

:: from TREES_1, 2009.09.09, A.T.
theorem :: FINSEQ_1:86
for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= n
proofend;

theorem :: FINSEQ_1:87
for p, q being FinSequence st ( p = p ^ q or p = q ^ p ) holds
q = {}
proofend;

theorem :: FINSEQ_1:88
for x being set
for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> &amp; q = {} ) or ( p = {} &amp; q = <*x*> ) )
proofend;

:: missing, 2009.09.26, A.T.
theorem :: FINSEQ_1:89
for n being Nat
for f being b1 -element FinSequence holds dom f = Seg n
proofend;

registration
let n be Nat;
let m be Element of NAT ;
let f be n -element FinSequence;
let g be m -element FinSequence;
clusterf ^ g -> n + m -element ;
coherence
 f ^ g is n + m -element
proofend;
end;

:: from JORDAN7, 2010.02.26, A.T
registration
cluster Relation-like Function-like real-valued increasing FinSequence-like  ->  one-to-one real-valued for set ;
coherence
 for b1 being real-valued FinSequence st b1 is increasing holds
b1 is one-to-one
proofend;
end;

:: from AMI_6, 2010.04.07, A.T.
theorem :: FINSEQ_1:90
for x, y being set st x in dom <*y*> holds
x = 1
proofend;

:: from FOMODEL0, 2011.06.12, A.T.
registration
let X be set ;
cluster Relation-like NAT -defined X -valued Function-like finite FinSequence-like FinSubsequence-like for set ;
existence
 ex b1 being FinSequence st b1 is X -valued
proofend;
end;

:: new, 2011.10.03, A.K.
registration
let D be FinSequence-membered set ;
let f be D -valued Function;
let x be set ;
clusterf . x ->  FinSequence-like ;
coherence
 f . x is FinSequence-like
proofend;
end;