:: 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 & k <= n ) } ;
correctness
coherence
{ k where k is Element of NAT : ( 1 <= k & 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 & k <= n ) } ;

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

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

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

theorem Th2: :: FINSEQ_1:2
( Seg 1 = {1} & Seg 2 = {1,2} )
proof end;

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

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 )
proof end;

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

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

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)
proof end;

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

:: Finite Sequences
definition
let IT be Relation;
attr IT 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
proof end;
end;

definition
mode FinSequence is FinSequence-like Function;
end;

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

registration
let n be Nat;
cluster Seg n -> finite ;
coherence
Seg n is finite
proof end;
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
proof end;
end;

Lm1: for n being Nat holds Seg n,n are_equipotent
proof end;

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

registration
let n be Nat;
cluster Seg n -> n -element ;
coherence
Seg n is n -element
proof end;
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
proof end;
compatibility
for b1 being Element of NAT holds
( b1 = len p iff Seg b1 = dom p )
proof end;
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
proof end;
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
proof end;

scheme :: FINSEQ_1:sch 1
SeqEx{ F1() -> Nat, P1[ set , set ] } :
ex p being FinSequence st
( dom p = Seg F1() & ( 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]
proof end;

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

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 & z = [k,(p . k)] )
proof end;

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

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

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

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

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

:: ::
:: 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
proof end;
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
proof end;
end;

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

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
proof end;
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
proof end;

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

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 )
proof end;

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
proof end;
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
proof end;
end;

definition
let p, q be FinSequence;
func p ^ q -> FinSequence means :Def7: :: FINSEQ_1:def 7
( dom it = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
it . k = p . k ) & ( 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)) & ( for k being Nat st k in dom p holds
b1 . k = p . k ) & ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) )
proof end;
uniqueness
for b1, b2 being FinSequence st dom b1 = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b1 . k = p . k ) & ( for k being Nat st k in dom q holds
b1 . ((len p) + k) = q . k ) & dom b2 = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b2 . k = p . k ) & ( for k being Nat st k in dom q holds
b2 . ((len p) + k) = q . k ) holds
b1 = b2
proof end;
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)) & ( for k being Nat st k in dom p holds
b3 . k = p . k ) & ( 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)
proof end;

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

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

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

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 & k = (len p) + n ) )
proof end;

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

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 & (len p) + k in dom (p ^ q) )
proof end;

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)
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

registration
let x be set ;
cluster <*x*> -> FinSequence-like ;
coherence
<*x*> is FinSequence-like
proof end;
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 & q is FinSequence of D )
proof end;

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 & <*x,y*> is Relation-like ) ;
let z be set ;
cluster <*x,y,z*> -> Relation-like Function-like ;
coherence
( <*x,y,z*> is Function-like & <*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 & rng p = {x} ) )
proof end;

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

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

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

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

theorem :: FINSEQ_1:43
for x, y, z being set holds
( <*x,y,z*> = <*x*> ^ <*y,z*> & <*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 & p . 1 = x & p . 2 = y ) )
proof end;

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

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

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
proof end;
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*>]
proof end;

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

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

definition
let D be set ;
func D * -> 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 )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is FinSequence of D ) ) & ( for x being set holds
( x in b2 iff x is FinSequence of D ) ) holds
b1 = b2
proof end;
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 ;
cluster D * -> non empty ;
coherence
not D * is empty
proof end;
end;

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

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

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() * & P1[p] & x = p ) )
proof end;

:: ::
:: Subsequences ::
:: ::
definition
let IT be Function;
attr IT 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
proof end;
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
proof end;
let p be FinSubsequence;
let X be set ;
cluster p | X -> FinSubsequence-like ;
coherence
p | X is FinSubsequence-like
proof end;
cluster X |` p -> FinSubsequence-like ;
coherence
X |` p is FinSubsequence-like
proof end;
end;

registration
cluster Relation-like Function-like FinSubsequence-like -> NAT -defined for set ;
coherence
for b1 being FinSubsequence holds b1 is NAT -defined
proof end;
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 & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );
existence
ex b1 being FinSequence of NAT st
( rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) )
proof end;
uniqueness
for b1, b2 being FinSequence of NAT st rng b1 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b1 & k1 = b1 . l & k2 = b1 . m holds
k1 < k2 ) & rng b2 = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) holds
b1 = b2
proof end;
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 & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b2 & k1 = b2 . l & k2 = b2 . m holds
k1 < k2 ) ) );

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

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
proof end;
end;

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

begin

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

begin

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

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
proof end;

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

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
proof end;
end;

:: From FUNCT_7, actually from GOBOARD4
registration
let f1 be FinSequence;
let f2 be non empty FinSequence;
cluster f1 ^ f2 -> non empty ;
coherence
not f1 ^ f2 is empty by Th35;
cluster f2 ^ 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() & ( 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]
proof end;

definition
let m be Nat;
let p be FinSequence;
func p | 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 func p | m -> FinSequence of D;
coherence
p | m is FinSequence of D by Th18;
end;

registration
let f be FinSequence;
cluster f | 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
proof end;

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

:: 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)
proof end;

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

:: from LANG1
definition
let R be Relation;
func R [*] -> Relation means :: FINSEQ_1:def 16
 for x, y being set 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
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 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 ) ) ) )
proof end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 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 ) ) ) ) ) & ( for x, y being set holds
( [x,y] in b2 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 ) ) ) ) ) holds
b1 = b2
proof end;
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 & 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 ) ) ) ) );

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

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

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

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

:: 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 & i <= F2() & P1[i] ) } is finite
proof end;

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

Lm7: 3 in Seg 3
;

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

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

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

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

Lm12: 5 in Seg 5
;

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

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

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

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

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

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

Lm19: 7 in Seg 7
;

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

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

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

Lm23: ( 7 in Seg 8 & 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 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
proof end;

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 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
proof end;

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 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 )
proof end;

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 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 & p . 6 = x6 & p . 7 = x7 )
proof end;

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 & 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 end;

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 & 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 end;

:: 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
proof end;

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

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

:: 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 & b1 is non-empty )
proof end;
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
proof end;

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
proof end;

:: 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
proof end;
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 being Nat st 1 <= k & k <= len p holds
p . k = q . k ) );
compatibility
( p = q iff ( len p = len q & ( for k being Nat st 1 <= k & 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 & ( for k being Nat st 1 <= k & 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 & card M2 = 0 holds
M1 = M2
proof end;

:: 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
proof end;

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

:: 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
proof end;
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
proof end;
let z be set ;
cluster <*x,y,z*> -> 3 -element ;
coherence
<*x,y,z*> is 3 -element
proof end;
end;

:: new, 2009.08.24, A.T.
definition
let X be set ;
attr X 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
proof end;
end;

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

registration
let X be set ;
cluster X * -> FinSequence-membered ;
coherence
X * is FinSequence-membered
proof end;
end;

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

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

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

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
proof end;
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
proof end;
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
proof end;

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

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

:: 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
proof end;

registration
let n be Nat;
let m be Element of NAT ;
let f be n -element FinSequence;
let g be m -element FinSequence;
cluster f ^ g -> n + m -element ;
coherence
f ^ g is n + m -element
proof end;
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
proof end;
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
proof end;

:: 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
proof end;
end;

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