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

begin

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 :: FINSEQ_1:1

canceled;

theorem :: FINSEQ_1:2

canceled;

theorem Th3: :: FINSEQ_1:3

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 Th4: :: FINSEQ_1:4

( Seg 1 = {1} & Seg 2 = {1,2} )

proof end;

theorem Th5: :: FINSEQ_1:5

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 Th5;

end;

theorem :: FINSEQ_1:6

for a being Nat holds a + 1 in Seg (a + 1) by Th5;

theorem Th7: :: FINSEQ_1:7

for a, b being Nat holds
( a <= b iff Seg a c= Seg b )

proof end;

theorem Th8: :: FINSEQ_1:8

for a, b being Nat st Seg a = Seg b holds
a = b

proof end;

theorem Th9: :: FINSEQ_1:9

for c, a being Nat st c <= a holds
Seg c = (Seg a) /\ (Seg c)

proof end;

theorem :: FINSEQ_1:10

for c, a being Nat st Seg c = (Seg c) /\ (Seg a) holds
c <= a by Th8, Th9;

theorem Th11: :: FINSEQ_1:11

for a being Nat holds (Seg a) \/ {(a + 1)} = Seg (a + 1)

proof end;

theorem :: FINSEQ_1:12

for k being Nat holds Seg k = (Seg (k + 1)) \ {(k + 1)}

proof end;

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 set ;
coherence
for b₁ being Relation st b₁ is empty holds
b₁ is FinSequence-like

proof end;

end;

definition

mode FinSequence is FinSequence-like Function;

end;

defpred S₁[ 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 set ;
coherence
for b₁ being Function st b₁ is FinSequence-like holds
b₁ 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 b₁ being Element of NAT holds
( b₁ = len p iff Seg b₁ = dom p )

proof end;

end;

:: deftheorem Def3 defines len FINSEQ_1:def 3 :
for p being FinSequence
for b₂ being Element of NAT holds
( b₂ = len p iff Seg b₂ = dom p );

definition

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

proof end;

end;

theorem :: FINSEQ_1:13

canceled;

theorem :: FINSEQ_1:14

canceled;

theorem :: FINSEQ_1:15

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{ F₁() -> Nat, P₁[ set , set ] } :

ex p being FinSequence st
( dom p = Seg F₁() & ( for k being Nat st k in Seg F₁() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Seg F₁() holds
ex x being set st P₁[k,x]

proof end;

scheme :: FINSEQ_1:sch 2
SeqLambda{ F₁() -> Nat, F₂( set ) -> set } :

ex p being FinSequence st
( len p = F₁() & ( for k being Nat st k in dom p holds
p . k = F₂(k) ) )

proof end;

theorem :: FINSEQ_1:16

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 Th17: :: FINSEQ_1:17

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 Th18: :: FINSEQ_1:18

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 Th19: :: FINSEQ_1:19

for a being Nat
for p being FinSequence holds p | (Seg a) is FinSequence

proof end;

theorem :: FINSEQ_1:20

for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence

proof end;

theorem Th21: :: FINSEQ_1:21

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;

definition

let D be set ;
mode FinSequence of D -> FinSequence means :Def4: :: FINSEQ_1:def 4
rng it c= D;
existence
ex b₁ being FinSequence st rng b₁ c= D

proof end;

end;

:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :
for D being set
for b₂ being FinSequence holds
( b₂ is FinSequence of D iff rng b₂ c= D );

registration

let D be set ;
cluster -> D -valued FinSequence of D;
coherence
for b₁ being FinSequence of D holds b₁ 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 set ;
coherence
for b₁ being Relation st b₁ is empty holds
b₁ is FinSequence-like ;

end;

registration

let D be set ;
cluster Relation-like NAT -defined D -valued Function-like FinSequence-like Element of bool [:NAT,D:];
existence
ex b₁ being PartFunc of NAT,D st b₁ 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 b₁ being FinSequence of D holds b₁ is FinSequence-like PartFunc of NAT,D by Lm3;

end;

theorem :: FINSEQ_1:22

canceled;

theorem Th23: :: FINSEQ_1:23

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:24

for a being Nat
for D being non empty set ex p being FinSequence of D st len p = a

proof end;

theorem :: FINSEQ_1:25

canceled;

theorem :: FINSEQ_1:26

canceled;

theorem :: FINSEQ_1:27

canceled;

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

theorem :: FINSEQ_1:28

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 FinSequence of D;
existence
ex b₁ being FinSequence of D st b₁ is empty

proof end;

end;

theorem :: FINSEQ_1:29

canceled;

theorem :: FINSEQ_1:30

canceled;

theorem :: FINSEQ_1:31

canceled;

theorem :: FINSEQ_1:32

canceled;

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 b₁ being FinSequence st
( dom b₁ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₁ . k = p . k ) & ( for k being Nat st k in dom q holds
b₁ . ((len p) + k) = q . k ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence st dom b₁ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₁ . k = p . k ) & ( for k being Nat st k in dom q holds
b₁ . ((len p) + k) = q . k ) & dom b₂ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₂ . k = p . k ) & ( for k being Nat st k in dom q holds
b₂ . ((len p) + k) = q . k ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :
for p, q being FinSequence
for b₃ being FinSequence holds
( b₃ = p ^ q iff ( dom b₃ = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
b₃ . k = p . k ) & ( for k being Nat st k in dom q holds
b₃ . ((len p) + k) = q . k ) ) );

theorem Th33: :: FINSEQ_1:33

for p, q being FinSequence holds p = (p ^ q) | (dom p)

proof end;

theorem :: FINSEQ_1:34

canceled;

theorem Th35: :: FINSEQ_1:35

for p, q being FinSequence holds len (p ^ q) = (len p) + (len q)

proof end;

theorem Th36: :: FINSEQ_1:36

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 Th37: :: FINSEQ_1:37

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 Th38: :: FINSEQ_1:38

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 Th39: :: FINSEQ_1:39

for p, q being FinSequence holds dom p c= dom (p ^ q)

proof end;

theorem Th40: :: FINSEQ_1:40

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 Th41: :: FINSEQ_1:41

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 Th42: :: FINSEQ_1:42

for p, q being FinSequence holds rng p c= rng (p ^ q)

proof end;

theorem Th43: :: FINSEQ_1:43

for q, p being FinSequence holds rng q c= rng (p ^ q)

proof end;

theorem Th44: :: FINSEQ_1:44

for p, q being FinSequence holds rng (p ^ q) = (rng p) \/ (rng q)

proof end;

theorem Th45: :: FINSEQ_1:45

for p, q, r being FinSequence holds (p ^ q) ^ r = p ^ (q ^ r)

proof end;

theorem :: FINSEQ_1:46

for p, r, q being FinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q

proof end;

theorem Th47: :: FINSEQ_1:47

for p being FinSequence holds
( p ^ {} = p & {} ^ p = p )

proof end;

theorem Th48: :: FINSEQ_1:48

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 b₁ being Function holds
( b₁ = <*x*> iff ( dom b₁ = Seg 1 & b₁ . 1 = x ) )

proof end;

end;

:: deftheorem Def8 defines <* FINSEQ_1:def 8 :
for x being set
for b₂ being Function holds
( b₂ = <*x*> iff ( dom b₂ = Seg 1 & b₂ . 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 :: FINSEQ_1:49

canceled;

theorem Th50: :: FINSEQ_1:50

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:51

canceled;

theorem :: FINSEQ_1:52

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

theorem :: FINSEQ_1:53

canceled;

theorem :: FINSEQ_1:54

canceled;

theorem Th55: :: FINSEQ_1:55

for x being set
for p being FinSequence holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )

proof end;

theorem Th56: :: FINSEQ_1:56

for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & rng p = {x} ) )

proof end;

theorem Th57: :: FINSEQ_1:57

for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )

proof end;

theorem :: FINSEQ_1:58

for x being set
for p being FinSequence holds (<*x*> ^ p) . 1 = x

proof end;

theorem Th59: :: FINSEQ_1:59

for x being set
for p being FinSequence holds (p ^ <*x*>) . ((len p) + 1) = x

proof end;

theorem :: FINSEQ_1:60

for x, y, z being set holds
( <*x,y,z*> = <*x*> ^ <*y,z*> & <*x,y,z*> = <*x,y*> ^ <*z*> ) by Th45;

theorem Th61: :: FINSEQ_1:61

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 Th62: :: FINSEQ_1:62

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 Th63: :: FINSEQ_1:63

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 :: FINSEQ_1:sch 3
IndSeq{ P₁[ FinSequence] } :

for p being FinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being FinSequence
for x being set st P₁[p] holds
P₁[p ^ <*x*>]

proof end;

theorem :: FINSEQ_1:64

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;

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 b₁ being set st
for x being set holds
( x in b₁ iff x is FinSequence of D )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being set holds
( x in b₁ iff x is FinSequence of D ) ) & ( for x being set holds
( x in b₂ iff x is FinSequence of D ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines * FINSEQ_1:def 11 :
for D, b₂ being set holds
( b₂ = D * iff for x being set holds
( x in b₂ 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:65

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:66

for D being set holds {} in D *

proof end;

scheme :: FINSEQ_1:sch 4
SepSeq{ F₁() -> non empty set , P₁[ FinSequence] } :

ex X being set st
for x being set holds
( x in X iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )

proof end;

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 set ;
existence
ex b₁ being Function st b₁ is FinSubsequence-like

proof end;

end;

definition

mode FinSubsequence is FinSubsequence-like Function;

end;

registration

cluster Relation-like Function-like FinSequence-like -> FinSubsequence-like set ;
coherence
for b₁ being Function st b₁ is FinSequence-like holds
b₁ 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;

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 b₁ being FinSequence of NAT st
( rng b₁ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of NAT st rng b₁ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₁ & k1 = b₁ . l & k2 = b₁ . m holds
k1 < k2 ) & rng b₂ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) holds
b₁ = b₂

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 b₂ being FinSequence of NAT holds
( b₂ = Sgm X iff ( rng b₂ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) ) );

theorem :: FINSEQ_1:67

canceled;

theorem :: FINSEQ_1:68

canceled;

theorem :: FINSEQ_1:69

canceled;

theorem :: FINSEQ_1:70

canceled;

theorem Th71: :: FINSEQ_1:71

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:72

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:73

for D being set holds
( D is finite iff ex p being FinSequence st D = rng p )

proof end;

begin

theorem :: FINSEQ_1:74

for n, m being Nat st Seg n, Seg m are_equipotent holds
n = m

proof end;

theorem :: FINSEQ_1:75

for n being Nat holds Seg n,n are_equipotent by Lm1;

theorem :: FINSEQ_1:76

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

theorem :: FINSEQ_1:77

for X being set st X is finite holds
ex n being Nat st X, Seg n are_equipotent

proof end;

theorem :: FINSEQ_1:78

for n being Nat holds card (Seg n) = n

proof end;

begin

registration

let x be set ;
cluster <*x*> -> non empty ;
coherence
not <*x*> is empty ;

end;

registration

cluster Relation-like Function-like non empty finite FinSequence-like FinSubsequence-like set ;
existence
not for b₁ being FinSequence holds b₁ is empty

proof end;

end;

registration

let f1 be FinSequence;
let f2 be non empty FinSequence;
cluster f1 ^ f2 -> non empty ;
coherence
not f1 ^ f2 is empty by Th48;
cluster f2 ^ f1 -> non empty ;
coherence
not f2 ^ f1 is empty by Th48;

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;

scheme :: FINSEQ_1:sch 5
SeqDEx{ F₁() -> non empty set , F₂() -> Nat, P₁[ set , set ] } :

ex p being FinSequence of F₁() st
( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₁[k,x]

proof end;

definition

let p be FinSequence;
let m be Nat;
func p | m -> FinSequence equals :: FINSEQ_1:def 15
p | (Seg m);
coherence
p | (Seg m) is FinSequence by Th19;

end;

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

definition

let D be set ;
let p be FinSequence of D;
let m be Nat;
:: original: |
redefine func p | m -> FinSequence of D;
coherence
p | m is FinSequence of D by Th23;

end;

registration

let f be FinSequence;
cluster f | 0 -> empty ;
coherence
f | 0 is empty ;

end;

theorem :: FINSEQ_1:79

for i being Nat
for q being FinSequence st len q <= i holds
q | i = q

proof end;

theorem :: FINSEQ_1:80

for i being Nat
for q being FinSequence st i <= len q holds
len (q | i) = i

proof end;

theorem :: FINSEQ_1:81

for i, n, m being Nat st i in Seg n holds
i + m in Seg (n + m)

proof end;

theorem :: FINSEQ_1:82

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;

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 b₁ being Relation st
for x, y being set holds
( [x,y] in b₁ 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 b₁, b₂ being Relation st ( for x, y being set holds
( [x,y] in b₁ 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 b₂ 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
b₁ = b₂

proof end;

end;

:: deftheorem defines [*] FINSEQ_1:def 16 :
for R, b₂ being Relation holds
( b₂ = R [*] iff for x, y being set holds
( [x,y] in b₂ 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:83

for D1, D2 being set st D1 c= D2 holds
D1 * c= D2 *

proof end;

registration

let D be set ;
cluster D * -> functional ;
coherence
D * is functional

proof end;

end;

theorem :: FINSEQ_1:84

for p, q being FinSequence st p c= q holds
len p <= len q

proof end;

theorem :: FINSEQ_1:85

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:86

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;

scheme :: FINSEQ_1:sch 6
FinSegRng{ F₁() -> Nat, F₂() -> Nat, F₃( set ) -> set , P₁[ set ] } :

{ F₃(i) where i is Element of NAT : ( F₁() <= i & i <= F₂() & P₁[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 Th87: :: FINSEQ_1:87

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 Th88: :: FINSEQ_1:88

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 Th89: :: FINSEQ_1:89

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 Th90: :: FINSEQ_1:90

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 Th91: :: FINSEQ_1:91

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:92

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;

theorem :: FINSEQ_1:93

for p being FinSequence holds p | (Seg 0) = {} ;

theorem :: FINSEQ_1:94

for f, g being FinSequence holds f | (Seg 0) = g | (Seg 0) ;

theorem :: FINSEQ_1:95

for D being non empty set
for x being Element of D holds <*x*> is FinSequence of D ;

theorem :: FINSEQ_1:96

for D being set
for p, q being FinSequence of D holds p ^ q is FinSequence of D ;

theorem :: FINSEQ_1:97

for a, b being set st <*a*> = <*b*> holds
a = b

proof end;

theorem :: FINSEQ_1:98

for a, b, c, d being set st <*a,b*> = <*c,d*> holds
( a = c & b = d )

proof end;

theorem :: FINSEQ_1:99

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;

registration

cluster Relation-like non-empty Function-like non empty finite FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st
( not b₁ is empty & b₁ is non-empty )

proof end;

end;

theorem Th100: :: FINSEQ_1:100

for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= len p

proof end;

theorem :: FINSEQ_1:101

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;

registration

let D be non empty set ;
cluster Relation-like NAT -defined D -valued Function-like non empty finite FinSequence-like FinSubsequence-like FinSequence of D;
existence
not for b₁ being FinSequence of D holds b₁ is empty

proof end;

end;

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 Th18;

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

theorem :: FINSEQ_1:102

for M1, M2 being set st card M1 = 0 & card M2 = 0 holds
M1 = M2

proof end;

registration

let n be non zero Nat;
cluster Seg n -> non empty ;
coherence
not Seg n is empty ;

end;

theorem :: FINSEQ_1:103

for p being FinSequence
for n, m being Nat st m <= n holds
(p | n) | m = p | m

proof end;

theorem :: FINSEQ_1:104

for n being Nat holds Seg n = (n + 1) \ {0}

proof end;

registration

let n be Nat;
cluster Relation-like Function-like finite n -element FinSequence-like FinSubsequence-like set ;
existence
ex b₁ being FinSequence st b₁ is n -element

proof end;

end;

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;

definition

let X be set ;
canceled;
attr X is FinSequence-membered means :Def19: :: FINSEQ_1:def 19
for x being set st x in X holds
x is FinSequence;

end;

:: deftheorem FINSEQ_1:def 18 :
canceled;

:: deftheorem Def19 defines FinSequence-membered FINSEQ_1:def 19 :
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 set ;
coherence
for b₁ being set st b₁ is empty holds
b₁ is FinSequence-membered

proof end;

end;

registration

cluster non empty FinSequence-membered set ;
existence
ex b₁ being set st
( not b₁ is empty & b₁ 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:105

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 set ;
coherence
for b₁ being set st b₁ is FinSequence-membered holds
b₁ is functional

proof end;

end;

theorem :: FINSEQ_1:106

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 Element of X;
coherence
for b₁ being Element of X holds b₁ is FinSequence-like

proof end;

end;

registration

let X be FinSequence-membered set ;
cluster -> FinSequence-membered Element of bool X;
coherence
for b₁ being Subset of X holds b₁ is FinSequence-membered

proof end;

end;

theorem :: FINSEQ_1:107

for n being Nat
for p, q being FinSequence st q = p | (Seg n) holds
len q <= n

proof end;

theorem :: FINSEQ_1:108

for p, q being FinSequence st ( p = p ^ q or p = q ^ p ) holds
q = {}

proof end;

theorem :: FINSEQ_1:109

for x being set
for p, q being FinSequence holds
( not p ^ q = <*x*> or ( p = <*x*> & q = {} ) or ( p = {} & q = <*x*> ) )

proof end;

theorem :: FINSEQ_1:110

for n being Nat
for f being b₁ -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;

registration

cluster Relation-like Function-like real-valued increasing FinSequence-like -> one-to-one real-valued set ;
coherence
for b₁ being real-valued FinSequence st b₁ is increasing holds
b₁ is one-to-one

proof end;

end;

theorem :: FINSEQ_1:111

for x, y being set st x in dom <*y*> holds
x = 1

proof end;