:: FINSEQ_1 semantic presentation

definition

let c₁ be natural number ;
func Seg c₁ -> set equals :: FINSEQ_1:def 1
{ b₁ where B is Nat : ( 1 <= b₁ & b₁ <= a₁ ) } ;
correctness ;

end;

:: deftheorem Def1 defines Seg FINSEQ_1:def 1 :

definition

let c₁ be natural number ;
redefine func Seg as Seg c₁ -> Subset of NAT ;
coherence

proof end;

end;

theorem Th1: :: FINSEQ_1:1

canceled;

theorem Th2: :: FINSEQ_1:2

canceled;

theorem Th3: :: FINSEQ_1:3

for b₁, b₂ being natural number holds
( b₁ in Seg b₂ iff ( 1 <= b₁ & b₁ <= b₂ ) )

proof end;

theorem Th4: :: FINSEQ_1:4

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

proof end;

theorem Th5: :: FINSEQ_1:5

for b₁ being natural number holds
( b₁ = 0 or b₁ in Seg b₁ )

proof end;

theorem Th6: :: FINSEQ_1:6

for b₁ being natural number holds b₁ + 1 in Seg (b₁ + 1) by Th5;

theorem Th7: :: FINSEQ_1:7

for b₁, b₂ being natural number holds
( b₁ <= b₂ iff Seg b₁ c= Seg b₂ )

proof end;

theorem Th8: :: FINSEQ_1:8

for b₁, b₂ being natural number st Seg b₁ = Seg b₂ holds
b₁ = b₂

proof end;

theorem Th9: :: FINSEQ_1:9

for b₁, b₂ being natural number st b₁ <= b₂ holds
Seg b₁ = (Seg b₂) /\ (Seg b₁)

proof end;

theorem Th10: :: FINSEQ_1:10

for b₁, b₂ being natural number st Seg b₁ = (Seg b₁) /\ (Seg b₂) holds
b₁ <= b₂

proof end;

theorem Th11: :: FINSEQ_1:11

for b₁ being natural number holds (Seg b₁) \/ {(b₁ + 1)} = Seg (b₁ + 1)

proof end;

theorem Th12: :: FINSEQ_1:12

for b₁ being natural number holds Seg b₁ = (Seg (b₁ + 1)) \ {(b₁ + 1)}

proof end;

definition

let c₁ be Relation;
attr a₁ is FinSequence-like means :Def2: :: FINSEQ_1:def 2
ex b₁ being Nat st dom a₁ = Seg b₁;

end;

:: deftheorem Def2 defines FinSequence-like FINSEQ_1:def 2 :

registration

cluster FinSequence-like set ;
existence

proof end;

end;

definition

mode FinSequence is FinSequence-like Function;

end;

defpred S₁[ set , set ] means ex b₁ being Nat st
( a₁ = b₁ & a₂ = b₁ + 1 );

registration

let c₁ be natural number ;
cluster Seg a₁ -> finite ;
coherence

proof end;

end;

registration

cluster FinSequence-like -> finite set ;
coherence

proof end;

end;

Lemma9: for b₁ being Nat holds Seg b₁,b₁ are_equipotent

proof end;

Lemma10: for b₁ being Nat holds Card (Seg b₁) = Card b₁

proof end;

notation

let c₁ be FinSequence;
synonym len c₁ for Card c₁;

end;

definition

let c₁ be FinSequence;
redefine func len as len c₁ -> Nat means :Def3: :: FINSEQ_1:def 3
Seg a₂ = dom a₁;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def3 defines len FINSEQ_1:def 3 :

definition

let c₁ be FinSequence;
redefine func dom as dom c₁ -> Subset of NAT ;
coherence

proof end;

end;

theorem Th13: :: FINSEQ_1:13

canceled;

theorem Th14: :: FINSEQ_1:14

{} is FinSequence

proof end;

theorem Th15: :: FINSEQ_1:15

for b₁ being Function st ex b₂ being Nat st dom b₁ c= Seg b₂ holds
ex b₂ being FinSequence st b₁ c= b₂

proof end;

scheme :: FINSEQ_1:sch 1
s1{ F₁() -> Nat, P₁[ set , set ] } :

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

provided

E13: for b₁ being Nat
for b₂, b₃ being set st b₁ in Seg F₁() & P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃ and
E14: for b₁ being Nat st b₁ in Seg F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

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

ex b₁ being FinSequence st
( len b₁ = F₁() & ( for b₂ being Nat st b₂ in Seg F₁() holds
b₁ . b₂ = F₂(b₂) ) )

proof end;

theorem Th16: :: FINSEQ_1:16

for b₁ being set
for b₂ being FinSequence st b₁ in b₂ holds
ex b₃ being Nat st
( b₃ in dom b₂ & b₁ = [b₃,(b₂ . b₃)] )

proof end;

theorem Th17: :: FINSEQ_1:17

for b₁, b₂ being FinSequence st dom b₁ = dom b₂ & ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th18: :: FINSEQ_1:18

for b₁, b₂ being FinSequence st len b₁ = len b₂ & ( for b₃ being Nat st 1 <= b₃ & b₃ <= len b₁ holds
b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th19: :: FINSEQ_1:19

for b₁ being natural number
for b₂ being FinSequence holds b₂ | (Seg b₁) is FinSequence

proof end;

theorem Th20: :: FINSEQ_1:20

for b₁ being Function
for b₂ being FinSequence st rng b₂ c= dom b₁ holds
b₁ * b₂ is FinSequence

proof end;

theorem Th21: :: FINSEQ_1:21

for b₁ being natural number
for b₂, b₃ being FinSequence st b₁ <= len b₂ & b₃ = b₂ | (Seg b₁) holds
( len b₃ = b₁ & dom b₃ = Seg b₁ )

proof end;

definition

let c₁ be set ;
mode FinSequence of c₁ -> FinSequence means :Def4: :: FINSEQ_1:def 4
rng a₂ c= a₁;
existence

proof end;

end;

:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :

Lemma17: for b₁ being set
for b₂ being FinSequence of b₁ holds b₂ is PartFunc of NAT ,b₁

proof end;

registration

cluster {} -> FinSequence-like ;
coherence by Th14;

end;

registration

let c₁ be set ;
cluster finite FinSequence-like M5( NAT ,a₁);
existence

proof end;

end;

definition

let c₁ be set ;
redefine mode FinSequence as FinSequence of c₁ -> FinSequence-like PartFunc of NAT ,a₁;
coherence by Lemma17;

end;

theorem Th22: :: FINSEQ_1:22

canceled;

theorem Th23: :: FINSEQ_1:23

for b₁ being natural number
for b₂ being set
for b₃ being FinSequence of b₂ holds b₃ | (Seg b₁) is FinSequence of b₂

proof end;

theorem Th24: :: FINSEQ_1:24

for b₁ being natural number
for b₂ being non empty set ex b₃ being FinSequence of b₂ st len b₃ = b₁

proof end;

Lemma19: for b₁ being FinSequence holds
( b₁ = {} iff len b₁ = 0 )

proof end;

registration

cluster empty finite set ;
existence by Th14;

end;

theorem Th25: :: FINSEQ_1:25

for b₁ being FinSequence holds
( len b₁ = 0 iff b₁ = {} ) by Lemma19;

theorem Th26: :: FINSEQ_1:26

for b₁ being FinSequence holds
( b₁ = {} iff dom b₁ = {} ) by RELAT_1:60, RELAT_1:64;

theorem Th27: :: FINSEQ_1:27

for b₁ being FinSequence holds
( b₁ = {} iff rng b₁ = {} ) by RELAT_1:60, RELAT_1:64;

theorem Th28: :: FINSEQ_1:28

canceled;

theorem Th29: :: FINSEQ_1:29

for b₁ being set holds {} is FinSequence of b₁

proof end;

registration

let c₁ be set ;
cluster empty finite FinSequence-like FinSequence of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
func <*c₁*> -> set equals :: FINSEQ_1:def 5
{[1,a₁]};
coherence ;

end;

:: deftheorem Def5 defines <* FINSEQ_1:def 5 :

definition

let c₁ be set ;
func <*> c₁ -> empty FinSequence of a₁ equals :: FINSEQ_1:def 6
{} ;
coherence by Th29;

end;

:: deftheorem Def6 defines <*> FINSEQ_1:def 6 :

theorem Th30: :: FINSEQ_1:30

canceled;

theorem Th31: :: FINSEQ_1:31

canceled;

theorem Th32: :: FINSEQ_1:32

for b₁ being FinSequence
for b₂ being set holds
( b₁ = <*> b₂ iff len b₁ = 0 ) by Lemma19;

definition

let c₁, c₂ be FinSequence;
func c₁ ^ c₂ -> FinSequence means :Def7: :: FINSEQ_1:def 7
( dom a₃ = Seg ((len a₁) + (len a₂)) & ( for b₁ being Nat st b₁ in dom a₁ holds
a₃ . b₁ = a₁ . b₁ ) & ( for b₁ being Nat st b₁ in dom a₂ holds
a₃ . ((len a₁) + b₁) = a₂ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :

theorem Th33: :: FINSEQ_1:33

for b₁, b₂ being FinSequence holds b₁ = (b₁ ^ b₂) | (dom b₁)

proof end;

theorem Th34: :: FINSEQ_1:34

canceled;

theorem Th35: :: FINSEQ_1:35

for b₁, b₂ being FinSequence holds len (b₁ ^ b₂) = (len b₁) + (len b₂)

proof end;

theorem Th36: :: FINSEQ_1:36

for b₁, b₂ being FinSequence
for b₃ being natural number st (len b₁) + 1 <= b₃ & b₃ <= (len b₁) + (len b₂) holds
(b₁ ^ b₂) . b₃ = b₂ . (b₃ - (len b₁))

proof end;

theorem Th37: :: FINSEQ_1:37

for b₁, b₂ being FinSequence
for b₃ being natural number st len b₁ < b₃ & b₃ <= len (b₁ ^ b₂) holds
(b₁ ^ b₂) . b₃ = b₂ . (b₃ - (len b₁))

proof end;

theorem Th38: :: FINSEQ_1:38

for b₁, b₂ being FinSequence
for b₃ being Nat holds
( not b₃ in dom (b₁ ^ b₂) or b₃ in dom b₁ or ex b₄ being Nat st
( b₄ in dom b₂ & b₃ = (len b₁) + b₄ ) )

proof end;

theorem Th39: :: FINSEQ_1:39

for b₁, b₂ being FinSequence holds dom b₁ c= dom (b₁ ^ b₂)

proof end;

theorem Th40: :: FINSEQ_1:40

for b₁ being set
for b₂, b₃ being FinSequence st b₁ in dom b₂ holds
ex b₄ being Nat st
( b₄ = b₁ & (len b₃) + b₄ in dom (b₃ ^ b₂) )

proof end;

theorem Th41: :: FINSEQ_1:41

for b₁ being Nat
for b₂, b₃ being FinSequence st b₁ in dom b₂ holds
(len b₃) + b₁ in dom (b₃ ^ b₂)

proof end;

theorem Th42: :: FINSEQ_1:42

for b₁, b₂ being FinSequence holds rng b₁ c= rng (b₁ ^ b₂)

proof end;

theorem Th43: :: FINSEQ_1:43

for b₁, b₂ being FinSequence holds rng b₁ c= rng (b₂ ^ b₁)

proof end;

theorem Th44: :: FINSEQ_1:44

for b₁, b₂ being FinSequence holds rng (b₁ ^ b₂) = (rng b₁) \/ (rng b₂)

proof end;

theorem Th45: :: FINSEQ_1:45

for b₁, b₂, b₃ being FinSequence holds (b₁ ^ b₂) ^ b₃ = b₁ ^ (b₂ ^ b₃)

proof end;

theorem Th46: :: FINSEQ_1:46

for b₁, b₂, b₃ being FinSequence st ( b₁ ^ b₂ = b₃ ^ b₂ or b₂ ^ b₁ = b₂ ^ b₃ ) holds
b₁ = b₃

proof end;

theorem Th47: :: FINSEQ_1:47

for b₁ being FinSequence holds
( b₁ ^ {} = b₁ & {} ^ b₁ = b₁ )

proof end;

theorem Th48: :: FINSEQ_1:48

for b₁, b₂ being FinSequence st b₁ ^ b₂ = {} holds
( b₁ = {} & b₂ = {} )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be FinSequence of c₁;
redefine func ^ as c₂ ^ c₃ -> FinSequence of a₁;
coherence

proof end;

end;

Lemma35: for b₁, b₂ being set holds {[b₁,b₂]} is Function

proof end;

Lemma36: for b₁, b₂, b₃, b₄ being set st [b₁,b₂] in {[b₃,b₄]} holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

definition

let c₁ be set ;
redefine func <* as <*c₁*> -> Function means :Def8: :: FINSEQ_1:def 8
( dom a₂ = Seg 1 & a₂ . 1 = a₁ );
coherence by Lemma35;
compatibility

proof end;

end;

:: deftheorem Def8 defines <* FINSEQ_1:def 8 :

registration

let c₁ be set ;
cluster <*a₁*> -> Relation-like Function-like ;
coherence ;

end;

registration

let c₁ be set ;
cluster <*a₁*> -> Relation-like Function-like finite FinSequence-like ;
coherence

proof end;

end;

theorem Th49: :: FINSEQ_1:49

canceled;

theorem Th50: :: FINSEQ_1:50

for b₁, b₂ being FinSequence
for b₃ being set st b₁ ^ b₂ is FinSequence of b₃ holds
( b₁ is FinSequence of b₃ & b₂ is FinSequence of b₃ )

proof end;

definition

let c₁, c₂ be set ;
func <*c₁,c₂*> -> set equals :: FINSEQ_1:def 9
<*a₁*> ^ <*a₂*>;
correctness ;
let c₃ be set ;
func <*c₁,c₂,c₃*> -> set equals :: FINSEQ_1:def 10
(<*a₁*> ^ <*a₂*>) ^ <*a₃*>;
correctness ;

end;

:: deftheorem Def9 defines <* FINSEQ_1:def 9 :

:: deftheorem Def10 defines <* FINSEQ_1:def 10 :

registration

let c₁, c₂ be set ;
cluster <*a₁,a₂*> -> Relation-like Function-like ;
coherence ;
let c₃ be set ;
cluster <*a₁,a₂,a₃*> -> Relation-like Function-like ;
coherence ;

end;

registration

let c₁, c₂ be set ;
cluster <*a₁,a₂*> -> Relation-like Function-like finite FinSequence-like ;
coherence ;
let c₃ be set ;
cluster <*a₁,a₂,a₃*> -> Relation-like Function-like finite FinSequence-like ;
coherence ;

end;

theorem Th51: :: FINSEQ_1:51

canceled;

theorem Th52: :: FINSEQ_1:52

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

theorem Th53: :: FINSEQ_1:53

canceled;

theorem Th54: :: FINSEQ_1:54

canceled;

theorem Th55: :: FINSEQ_1:55

for b₁ being set
for b₂ being FinSequence holds
( b₂ = <*b₁*> iff ( dom b₂ = Seg 1 & rng b₂ = {b₁} ) )

proof end;

theorem Th56: :: FINSEQ_1:56

for b₁ being set
for b₂ being FinSequence holds
( b₂ = <*b₁*> iff ( len b₂ = 1 & rng b₂ = {b₁} ) )

proof end;

theorem Th57: :: FINSEQ_1:57

for b₁ being set
for b₂ being FinSequence holds
( b₂ = <*b₁*> iff ( len b₂ = 1 & b₂ . 1 = b₁ ) )

proof end;

theorem Th58: :: FINSEQ_1:58

for b₁ being set
for b₂ being FinSequence holds (<*b₁*> ^ b₂) . 1 = b₁

proof end;

theorem Th59: :: FINSEQ_1:59

for b₁ being set
for b₂ being FinSequence holds (b₂ ^ <*b₁*>) . ((len b₂) + 1) = b₁

proof end;

theorem Th60: :: FINSEQ_1:60

for b₁, b₂, b₃ being set holds
( <*b₁,b₂,b₃*> = <*b₁*> ^ <*b₂,b₃*> & <*b₁,b₂,b₃*> = <*b₁,b₂*> ^ <*b₃*> ) by Th45;

theorem Th61: :: FINSEQ_1:61

for b₁, b₂ being set
for b₃ being FinSequence holds
( b₃ = <*b₁,b₂*> iff ( len b₃ = 2 & b₃ . 1 = b₁ & b₃ . 2 = b₂ ) )

proof end;

theorem Th62: :: FINSEQ_1:62

for b₁, b₂, b₃ being set
for b₄ being FinSequence holds
( b₄ = <*b₁,b₂,b₃*> iff ( len b₄ = 3 & b₄ . 1 = b₁ & b₄ . 2 = b₂ & b₄ . 3 = b₃ ) )

proof end;

theorem Th63: :: FINSEQ_1:63

for b₁ being FinSequence st b₁ <> {} holds
ex b₂ being FinSequenceex b₃ being set st b₁ = b₂ ^ <*b₃*>

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func <* as <*c₂*> -> FinSequence of a₁;
coherence

proof end;

end;

scheme :: FINSEQ_1:sch 3
s3{ P₁[ FinSequence] } :

for b₁ being FinSequence holds P₁[b₁]

provided

E46: P₁[ {} ] and
E47: for b₁ being FinSequence
for b₂ being set st P₁[b₁] holds
P₁[b₁ ^ <*b₂*>]

proof end;

theorem Th64: :: FINSEQ_1:64

for b₁, b₂, b₃, b₄ being FinSequence st b₁ ^ b₂ = b₃ ^ b₄ & len b₁ <= len b₃ holds
ex b₅ being FinSequence st b₁ ^ b₅ = b₃

proof end;

definition

let c₁ be set ;
func c₁ * -> set means :Def11: :: FINSEQ_1:def 11
for b₁ being set holds
( b₁ in a₂ iff b₁ is FinSequence of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines * FINSEQ_1:def 11 :

registration

let c₁ be set ;
cluster a₁ * -> non empty ;
coherence

proof end;

end;

theorem Th65: :: FINSEQ_1:65

for b₁, b₂ being FinSequence st rng b₁ = rng b₂ & b₁ is one-to-one & b₂ is one-to-one holds
len b₁ = len b₂

proof end;

theorem Th66: :: FINSEQ_1:66

for b₁ being set holds {} in b₁ *

proof end;

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

ex b₁ being set st
for b₂ being set holds
( b₂ in b₁ iff ex b₃ being FinSequence st
( b₃ in F₁() * & P₁[b₃] & b₂ = b₃ ) )

proof end;

definition

let c₁ be Function;
attr a₁ is FinSubsequence-like means :Def12: :: FINSEQ_1:def 12
ex b₁ being Nat st dom a₁ c= Seg b₁;

end;

:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def 12 :

registration

cluster FinSubsequence-like set ;
existence

proof end;

end;

definition

mode FinSubsequence is FinSubsequence-like Function;

end;

theorem Th67: :: FINSEQ_1:67

canceled;

theorem Th68: :: FINSEQ_1:68

for b₁ being FinSequence holds b₁ is FinSubsequence

proof end;

theorem Th69: :: FINSEQ_1:69

for b₁ being set
for b₂ being FinSequence holds
( b₂ | b₁ is FinSubsequence & b₁ | b₂ is FinSubsequence )

proof end;

definition

let c₁ be set ;
given c₂ being natural number such that E48: c₁ c= Seg c₂ ;
func Sgm c₁ -> FinSequence of NAT means :Def13: :: FINSEQ_1:def 13
( rng a₂ = a₁ & ( for b₁, b₂, b₃, b₄ being natural number st 1 <= b₁ & b₁ < b₂ & b₂ <= len a₂ & b₃ = a₂ . b₁ & b₄ = a₂ . b₂ holds
b₃ < b₄ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Sgm FINSEQ_1:def 13 :

theorem Th70: :: FINSEQ_1:70

canceled;

theorem Th71: :: FINSEQ_1:71

for b₁ being FinSubsequence holds rng (Sgm (dom b₁)) = dom b₁

proof end;

definition

let c₁ be FinSubsequence;
func Seq c₁ -> Function equals :: FINSEQ_1:def 14
a₁ * (Sgm (dom a₁));
coherence ;

end;

:: deftheorem Def14 defines Seq FINSEQ_1:def 14 :

registration

let c₁ be FinSubsequence;
cluster Seq a₁ -> finite FinSequence-like ;
coherence

proof end;

end;

theorem Th72: :: FINSEQ_1:72

for b₁ being set st ex b₂ being Nat st b₁ c= Seg b₂ holds
( Sgm b₁ = {} iff b₁ = {} )

proof end;

theorem Th73: :: FINSEQ_1:73

for b₁ being set holds
( b₁ is finite iff ex b₂ being FinSequence st b₁ = rng b₂ )

proof end;

registration

cluster empty finite set ;
existence

proof end;

end;

registration

cluster non empty finite set ;
existence

proof end;

end;

registration

let c₁ be finite Relation;
cluster rng a₁ -> finite ;
coherence

proof end;

end;

theorem Th74: :: FINSEQ_1:74

for b₁, b₂ being Nat st Seg b₁, Seg b₂ are_equipotent holds
b₁ = b₂

proof end;

theorem Th75: :: FINSEQ_1:75

for b₁ being Nat holds Seg b₁,b₁ are_equipotent by Lemma9;

theorem Th76: :: FINSEQ_1:76

for b₁ being Nat holds Card (Seg b₁) = Card b₁ by Lemma10;

theorem Th77: :: FINSEQ_1:77

for b₁ being set st b₁ is finite holds
ex b₂ being Nat st b₁, Seg b₂ are_equipotent

proof end;

theorem Th78: :: FINSEQ_1:78

( ( for b₁ being natural number holds card (Seg b₁) = b₁ ) & ( for b₁ being Nat holds
( card b₁ = b₁ & card (Card b₁) = b₁ ) ) )

proof end;

registration

let c₁ be set ;
cluster <*a₁*> -> non empty Relation-like Function-like finite FinSequence-like ;
coherence ;

end;

registration

cluster non empty finite set ;
existence

proof end;

end;

registration

let c₁ be FinSequence;
let c₂ be non empty FinSequence;
cluster a₁ ^ a₂ -> non empty finite ;
coherence by Th48;
cluster a₂ ^ a₁ -> non empty finite ;
coherence by Th48;

end;

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

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

provided

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

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃ be natural number ;
func c₂ | c₃ -> FinSequence of a₁ equals :: FINSEQ_1:def 15
a₂ | (Seg a₃);
coherence by Th23;

end;

:: deftheorem Def15 defines | FINSEQ_1:def 15 :

registration

let c₁ be set ;
let c₂ be FinSequence of c₁;
cluster a₂ | 0 -> empty finite FinSequence-like ;
coherence by Th4, RELAT_1:110;

end;

theorem Th79: :: FINSEQ_1:79

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being natural number st len b₂ <= b₃ holds
b₂ | b₃ = b₂

proof end;

theorem Th80: :: FINSEQ_1:80

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being natural number st b₃ <= len b₂ holds
len (b₂ | b₃) = b₃

proof end;

theorem Th81: :: FINSEQ_1:81

for b₁ being Nat
for b₂, b₃ being natural number st b₂ in Seg b₁ holds
b₂ + b₃ in Seg (b₁ + b₃)

proof end;

theorem Th82: :: FINSEQ_1:82

for b₁ being Nat
for b₂, b₃ being natural number st b₂ > 0 & b₂ + b₃ in Seg (b₁ + b₃) holds
( b₂ in Seg b₁ & b₂ in Seg (b₁ + b₃) )

proof end;

definition

let c₁ be Relation;
func c₁ [*] -> Relation means :: FINSEQ_1:def 16
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ( b₁ in field a₁ & b₂ in field a₁ & ex b₃ being FinSequence st
( len b₃ >= 1 & b₃ . 1 = b₁ & b₃ . (len b₃) = b₂ & ( for b₄ being Nat st b₄ >= 1 & b₄ < len b₃ holds
[(b₃ . b₄),(b₃ . (b₄ + 1))] in a₁ ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines [*] FINSEQ_1:def 16 :

theorem Th83: :: FINSEQ_1:83

for b₁, b₂ being set st b₁ c= b₂ holds
b₁ * c= b₂ *

proof end;

registration

let c₁ be set ;
cluster a₁ * -> non empty functional ;
coherence

proof end;

end;

registration

let c₁ be finite Function;
cluster dom a₁ -> finite ;
coherence by FINSET_1:29;

end;

registration

let c₁ be finite Function;
let c₂ be set ;
cluster a₁ " a₂ -> finite ;
coherence

proof end;

end;

theorem Th84: :: FINSEQ_1:84

for b₁, b₂ being FinSequence st b₁ c= b₂ holds
len b₁ <= len b₂

proof end;

theorem Th85: :: FINSEQ_1:85

for b₁, b₂ being FinSequence
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₁ holds
(b₁ ^ b₂) . b₃ = b₁ . b₃

proof end;

theorem Th86: :: FINSEQ_1:86

for b₁, b₂ being FinSequence
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₂ holds
(b₁ ^ b₂) . ((len b₁) + b₃) = b₂ . b₃

proof end;