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

proof end;

theorem Th11: :: FINSEQ_2:11

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

proof end;

theorem Th12: :: FINSEQ_2:12

canceled;

theorem Th13: :: FINSEQ_2:13

for b₁ being Nat
for b₂ being set
for b₃ being FinSequence of b₂ st b₁ in dom b₃ holds
b₃ . b₁ in b₂

proof end;

E8: now

let c₁ be natural number ;
assume E9: c₁ <> 0 ;
let c₂ be Element of Seg c₁;
reconsider c₃ = c₁ as Nat by ORDINAL2:def 21;
Seg c₃ is non empty Subset of NAT by E9, FINSEQ_1:5;
hence c₂ in Seg c₁ ;

end;

theorem Th14: :: FINSEQ_2:14

for b₁ being FinSequence
for b₂ being set st ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ in b₂ ) holds
b₁ is FinSequence of b₂

proof end;

Lemma10: for b₁, b₂ being set holds rng <*b₁,b₂*> = {b₁,b₂}

proof end;

theorem Th15: :: FINSEQ_2:15

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds <*b₂,b₃*> is FinSequence of b₁

proof end;

Lemma12: for b₁, b₂, b₃ being set holds rng <*b₁,b₂,b₃*> = {b₁,b₂,b₃}

proof end;

theorem Th16: :: FINSEQ_2:16

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds <*b₂,b₃,b₄*> is FinSequence of b₁

proof end;

theorem Th17: :: FINSEQ_2:17

canceled;

theorem Th18: :: FINSEQ_2:18

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

proof end;

theorem Th19: :: FINSEQ_2:19

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

proof end;

theorem Th20: :: FINSEQ_2:20

for b₁, b₂ being set
for b₃, b₄ being FinSequence st b₃ ^ <*b₁*> = b₄ ^ <*b₂*> holds
( b₃ = b₄ & b₁ = b₂ )

proof end;

theorem Th21: :: FINSEQ_2:21

for b₁ being Nat
for b₂ being FinSequence st len b₂ = b₁ + 1 holds
ex b₃ being FinSequenceex b₄ being set st b₂ = b₃ ^ <*b₄*>

proof end;

theorem Th22: :: FINSEQ_2:22

for b₁ being non empty set
for b₂ being FinSequence of b₁ st len b₂ <> 0 holds
ex b₃ being FinSequence of b₁ex b₄ being Element of b₁ st b₂ = b₃ ^ <*b₄*>

proof end;

theorem Th23: :: FINSEQ_2:23

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

proof end;

theorem Th24: :: FINSEQ_2:24

for b₁ being Nat
for b₂, b₃ being FinSequence st b₂ = b₃ | (Seg b₁) holds
len b₂ = min b₁,(len b₃)

proof end;

theorem Th25: :: FINSEQ_2:25

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

proof end;

theorem Th26: :: FINSEQ_2:26

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st len b₄ = b₁ + b₂ holds
ex b₅, b₆ being FinSequence of b₃ st
( len b₅ = b₁ & len b₆ = b₂ & b₄ = b₅ ^ b₆ )

proof end;

scheme :: FINSEQ_2:sch 1
s1{ F₁() -> Nat, F₂() -> non empty set , F₃( set ) -> Element of F₂() } :

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

proof end;

scheme :: FINSEQ_2:sch 2
s2{ F₁() -> non empty set , P₁[ set ] } :

for b₁ being FinSequence of F₁() holds P₁[b₁]

provided

E21: P₁[ <*> F₁()] and
E22: for b₁ being FinSequence of F₁()
for b₂ being Element of F₁() st P₁[b₁] holds
P₁[b₁ ^ <*b₂*>]

proof end;

theorem Th27: :: FINSEQ_2:27

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃ being FinSequence of b₂ holds b₃ is FinSequence of b₁

proof end;

theorem Th28: :: FINSEQ_2:28

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function of Seg b₁,b₂ holds b₃ is FinSequence of b₂

proof end;

theorem Th29: :: FINSEQ_2:29

canceled;

theorem Th30: :: FINSEQ_2:30

for b₁ being non empty set
for b₂ being FinSequence of b₁ holds b₂ is Function of dom b₂,b₁

proof end;

theorem Th31: :: FINSEQ_2:31

for b₁ being Nat
for b₂ being non empty set
for b₃ being Function of NAT ,b₂ holds b₃ | (Seg b₁) is FinSequence of b₂

proof end;

theorem Th32: :: FINSEQ_2:32

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence
for b₄ being Function of NAT ,b₂ st b₃ = b₄ | (Seg b₁) holds
len b₃ = b₁

proof end;

theorem Th33: :: FINSEQ_2:33

for b₁, b₂ being FinSequence
for b₃ being Function st rng b₁ c= dom b₃ & b₂ = b₃ * b₁ holds
len b₂ = len b₁

proof end;

theorem Th34: :: FINSEQ_2:34

for b₁ being Nat
for b₂ being non empty set st b₂ = Seg b₁ holds
for b₃ being FinSequence
for b₄ being FinSequence of b₂ st b₁ <= len b₃ holds
b₃ * b₄ is FinSequence

proof end;

theorem Th35: :: FINSEQ_2:35

for b₁ being Nat
for b₂, b₃ being non empty set st b₂ = Seg b₁ holds
for b₄ being FinSequence of b₃
for b₅ being FinSequence of b₂ st b₁ <= len b₄ holds
b₄ * b₅ is FinSequence of b₃

proof end;

theorem Th36: :: FINSEQ_2:36

for b₁, b₂ being set
for b₃ being FinSequence of b₁
for b₄ being Function of b₁,b₂ holds b₄ * b₃ is FinSequence of b₂

proof end;

theorem Th37: :: FINSEQ_2:37

for b₁ being set
for b₂ being non empty set
for b₃ being FinSequence
for b₄ being FinSequence of b₁
for b₅ being Function of b₁,b₂ st b₃ = b₅ * b₄ holds
len b₃ = len b₄

proof end;

theorem Th38: :: FINSEQ_2:38

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂ holds b₃ * (<*> b₁) = <*> b₂

proof end;

theorem Th39: :: FINSEQ_2:39

for b₁ being set
for b₂, b₃ being non empty set
for b₄ being FinSequence of b₂
for b₅ being Function of b₂,b₃ st b₄ = <*b₁*> holds
b₅ * b₄ = <*(b₅ . b₁)*>

proof end;

theorem Th40: :: FINSEQ_2:40

for b₁, b₂ being set
for b₃, b₄ being non empty set
for b₅ being FinSequence of b₃
for b₆ being Function of b₃,b₄ st b₅ = <*b₁,b₂*> holds
b₆ * b₅ = <*(b₆ . b₁),(b₆ . b₂)*>

proof end;

theorem Th41: :: FINSEQ_2:41

for b₁, b₂, b₃ being set
for b₄, b₅ being non empty set
for b₆ being FinSequence of b₄
for b₇ being Function of b₄,b₅ st b₆ = <*b₁,b₂,b₃*> holds
b₇ * b₆ = <*(b₇ . b₁),(b₇ . b₂),(b₇ . b₃)*>

proof end;

theorem Th42: :: FINSEQ_2:42

for b₁, b₂ being Nat
for b₃ being FinSequence
for b₄ being Function of Seg b₁, Seg b₂ st ( b₂ = 0 implies b₁ = 0 ) & b₂ <= len b₃ holds
b₃ * b₄ is FinSequence

proof end;

theorem Th43: :: FINSEQ_2:43

for b₁ being Nat
for b₂ being FinSequence
for b₃ being Function of Seg b₁, Seg b₁ st b₁ <= len b₂ holds
b₂ * b₃ is FinSequence

proof end;

theorem Th44: :: FINSEQ_2:44

for b₁ being FinSequence
for b₂ being Function of dom b₁, dom b₁ holds b₁ * b₂ is FinSequence

proof end;

theorem Th45: :: FINSEQ_2:45

for b₁ being Nat
for b₂, b₃ being FinSequence
for b₄ being Function of Seg b₁, Seg b₁ st rng b₄ = Seg b₁ & b₁ <= len b₂ & b₃ = b₂ * b₄ holds
len b₃ = b₁

proof end;

theorem Th46: :: FINSEQ_2:46

for b₁, b₂ being FinSequence
for b₃ being Function of dom b₁, dom b₁ st rng b₃ = dom b₁ & b₂ = b₁ * b₃ holds
len b₂ = len b₁

proof end;

theorem Th47: :: FINSEQ_2:47

for b₁ being Nat
for b₂, b₃ being FinSequence
for b₄ being Permutation of Seg b₁ st b₁ <= len b₂ & b₃ = b₂ * b₄ holds
len b₃ = b₁

proof end;

theorem Th48: :: FINSEQ_2:48

for b₁, b₂ being FinSequence
for b₃ being Permutation of dom b₁ st b₂ = b₁ * b₃ holds
len b₂ = len b₁

proof end;

theorem Th49: :: FINSEQ_2:49

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃
for b₅ being Function of Seg b₁, Seg b₂ st ( b₂ = 0 implies b₁ = 0 ) & b₂ <= len b₄ holds
b₄ * b₅ is FinSequence of b₃

proof end;

theorem Th50: :: FINSEQ_2:50

for b₁ being Nat
for b₂ being non empty set
for b₃ being FinSequence of b₂
for b₄ being Function of Seg b₁, Seg b₁ st b₁ <= len b₃ holds
b₃ * b₄ is FinSequence of b₂

proof end;

theorem Th51: :: FINSEQ_2:51

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃ being Function of dom b₂, dom b₂ holds b₂ * b₃ is FinSequence of b₁

proof end;

theorem Th52: :: FINSEQ_2:52

for b₁ being natural number holds id (Seg b₁) is FinSequence of NAT

proof end;

definition

let c₁ be natural number ;
func idseq c₁ -> FinSequence equals :: FINSEQ_2:def 1
id (Seg a₁);
coherence by Th52;

end;

:: deftheorem Def1 defines idseq FINSEQ_2:def 1 :

theorem Th53: :: FINSEQ_2:53

canceled;

theorem Th54: :: FINSEQ_2:54

for b₁ being natural number holds dom (idseq b₁) = Seg b₁ by RELAT_1:71;

theorem Th55: :: FINSEQ_2:55

for b₁ being natural number holds len (idseq b₁) = b₁

proof end;

theorem Th56: :: FINSEQ_2:56

for b₁, b₂ being Nat st b₁ in Seg b₂ holds
(idseq b₂) . b₁ = b₁ by FUNCT_1:35;

theorem Th57: :: FINSEQ_2:57

for b₁ being Nat st b₁ <> 0 holds
for b₂ being Element of Seg b₁ holds (idseq b₁) . b₂ = b₂

proof end;

theorem Th58: :: FINSEQ_2:58

idseq 0 = {}

proof end;

theorem Th59: :: FINSEQ_2:59

idseq 1 = <*1*>

proof end;

theorem Th60: :: FINSEQ_2:60

for b₁ being Nat holds idseq (b₁ + 1) = (idseq b₁) ^ <*(b₁ + 1)*>

proof end;

theorem Th61: :: FINSEQ_2:61

idseq 2 = <*1,2*>

proof end;

theorem Th62: :: FINSEQ_2:62

idseq 3 = <*1,2,3*>

proof end;

theorem Th63: :: FINSEQ_2:63

for b₁ being natural number
for b₂ being FinSequence holds b₂ * (idseq b₁) = b₂ | (Seg b₁) by RELAT_1:94;

theorem Th64: :: FINSEQ_2:64

for b₁ being natural number
for b₂ being FinSequence st len b₂ <= b₁ holds
b₂ * (idseq b₁) = b₂

proof end;

theorem Th65: :: FINSEQ_2:65

for b₁ being natural number holds idseq b₁ is Permutation of Seg b₁ ;

theorem Th66: :: FINSEQ_2:66

for b₁ being natural number
for b₂ being set holds (Seg b₁) --> b₂ is FinSequence

proof end;

definition

let c₁ be natural number ;
let c₂ be set ;
func c₁ |-> c₂ -> FinSequence equals :: FINSEQ_2:def 2
(Seg a₁) --> a₂;
coherence by Th66;

end;

:: deftheorem Def2 defines |-> FINSEQ_2:def 2 :

theorem Th67: :: FINSEQ_2:67

canceled;

theorem Th68: :: FINSEQ_2:68

for b₁ being natural number
for b₂ being set holds dom (b₁ |-> b₂) = Seg b₁ by FUNCOP_1:19;

theorem Th69: :: FINSEQ_2:69

for b₁ being natural number
for b₂ being set holds len (b₁ |-> b₂) = b₁

proof end;

theorem Th70: :: FINSEQ_2:70

for b₁ being natural number
for b₂, b₃ being set st b₂ in Seg b₁ holds
(b₁ |-> b₃) . b₂ = b₃ by FUNCOP_1:13;

theorem Th71: :: FINSEQ_2:71

for b₁ being natural number
for b₂ being non empty set
for b₃ being Element of b₂ st b₁ <> 0 holds
for b₄ being Element of Seg b₁ holds (b₁ |-> b₃) . b₄ = b₃

proof end;

theorem Th72: :: FINSEQ_2:72

for b₁ being set holds 0 |-> b₁ = {}

proof end;

theorem Th73: :: FINSEQ_2:73

for b₁ being set holds 1 |-> b₁ = <*b₁*>

proof end;

theorem Th74: :: FINSEQ_2:74

for b₁ being Nat
for b₂ being set holds (b₁ + 1) |-> b₂ = (b₁ |-> b₂) ^ <*b₂*>

proof end;

theorem Th75: :: FINSEQ_2:75

for b₁ being set holds 2 |-> b₁ = <*b₁,b₁*>

proof end;

theorem Th76: :: FINSEQ_2:76

for b₁ being set holds 3 |-> b₁ = <*b₁,b₁,b₁*>

proof end;

theorem Th77: :: FINSEQ_2:77

for b₁ being natural number
for b₂ being non empty set
for b₃ being Element of b₂ holds b₁ |-> b₃ is FinSequence of b₂

proof end;

Lemma54: for b₁ being Nat
for b₂, b₃ being FinSequence
for b₄ being Function st [:(rng b₂),(rng b₃):] c= dom b₄ & b₁ = min (len b₂),(len b₃) holds
dom (b₄ .: b₂,b₃) = Seg b₁

proof end;

theorem Th78: :: FINSEQ_2:78

for b₁, b₂ being FinSequence
for b₃ being Function st [:(rng b₁),(rng b₂):] c= dom b₃ holds
b₃ .: b₁,b₂ is FinSequence

proof end;

theorem Th79: :: FINSEQ_2:79

for b₁, b₂, b₃ being FinSequence
for b₄ being Function st [:(rng b₁),(rng b₂):] c= dom b₄ & b₃ = b₄ .: b₁,b₂ holds
len b₃ = min (len b₁),(len b₂)

proof end;

Lemma57: for b₁ being set
for b₂ being FinSequence
for b₃ being Function st [:{b₁},(rng b₂):] c= dom b₃ holds
dom (b₃ [;] b₁,b₂) = dom b₂

proof end;

theorem Th80: :: FINSEQ_2:80

for b₁ being set
for b₂ being FinSequence
for b₃ being Function st [:{b₁},(rng b₂):] c= dom b₃ holds
b₃ [;] b₁,b₂ is FinSequence

proof end;

theorem Th81: :: FINSEQ_2:81

for b₁ being set
for b₂, b₃ being FinSequence
for b₄ being Function st [:{b₁},(rng b₂):] c= dom b₄ & b₃ = b₄ [;] b₁,b₂ holds
len b₃ = len b₂

proof end;

Lemma60: for b₁ being set
for b₂ being FinSequence
for b₃ being Function st [:(rng b₂),{b₁}:] c= dom b₃ holds
dom (b₃ [:] b₂,b₁) = dom b₂

proof end;

theorem Th82: :: FINSEQ_2:82

for b₁ being set
for b₂ being FinSequence
for b₃ being Function st [:(rng b₂),{b₁}:] c= dom b₃ holds
b₃ [:] b₂,b₁ is FinSequence

proof end;

theorem Th83: :: FINSEQ_2:83

for b₁ being set
for b₂, b₃ being FinSequence
for b₄ being Function st [:(rng b₂),{b₁}:] c= dom b₄ & b₃ = b₄ [:] b₂,b₁ holds
len b₃ = len b₂

proof end;

theorem Th84: :: FINSEQ_2:84

for b₁, b₂, b₃ being non empty set
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being FinSequence of b₁
for b₆ being FinSequence of b₂ holds b₄ .: b₅,b₆ is FinSequence of b₃

proof end;

theorem Th85: :: FINSEQ_2:85

for b₁, b₂, b₃ being non empty set
for b₄ being FinSequence
for b₅ being Function of [:b₁,b₂:],b₃
for b₆ being FinSequence of b₁
for b₇ being FinSequence of b₂ st b₄ = b₅ .: b₆,b₇ holds
len b₄ = min (len b₆),(len b₇)

proof end;

theorem Th86: :: FINSEQ_2:86

for b₁, b₂, b₃ being non empty set
for b₄ being FinSequence
for b₅ being Function of [:b₁,b₂:],b₃
for b₆ being FinSequence of b₁
for b₇ being FinSequence of b₂ st len b₆ = len b₇ & b₄ = b₅ .: b₆,b₇ holds
( len b₄ = len b₆ & len b₄ = len b₇ )

proof end;

theorem Th87: :: FINSEQ_2:87

for b₁, b₂, b₃ being non empty set
for b₄ being Function of [:b₁,b₂:],b₃
for b₅ being FinSequence of b₁
for b₆ being FinSequence of b₂ holds
( b₄ .: (<*> b₁),b₆ = <*> b₃ & b₄ .: b₅,(<*> b₂) = <*> b₃ )

proof end;

theorem Th88: :: FINSEQ_2:88

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Function of [:b₁,b₂:],b₃
for b₇ being FinSequence of b₁
for b₈ being FinSequence of b₂ st b₇ = <*b₄*> & b₈ = <*b₅*> holds
b₆ .: b₇,b₈ = <*(b₆ . b₄,b₅)*>

proof end;

theorem Th89: :: FINSEQ_2:89

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being Element of b₁
for b₆, b₇ being Element of b₂
for b₈ being Function of [:b₁,b₂:],b₃
for b₉ being FinSequence of b₁
for b₁₀ being FinSequence of b₂ st b₉ = <*b₄,b₅*> & b₁₀ = <*b₆,b₇*> holds
b₈ .: b₉,b₁₀ = <*(b₈ . b₄,b₆),(b₈ . b₅,b₇)*>

proof end;

theorem Th90: :: FINSEQ_2:90

for b₁, b₂, b₃ being non empty set
for b₄, b₅, b₆ being Element of b₁
for b₇, b₈, b₉ being Element of b₂
for b₁₀ being Function of [:b₁,b₂:],b₃
for b₁₁ being FinSequence of b₁
for b₁₂ being FinSequence of b₂ st b₁₁ = <*b₄,b₅,b₆*> & b₁₂ = <*b₇,b₈,b₉*> holds
b₁₀ .: b₁₁,b₁₂ = <*(b₁₀ . b₄,b₇),(b₁₀ . b₅,b₈),(b₁₀ . b₆,b₉)*>

proof end;

theorem Th91: :: FINSEQ_2:91

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Function of [:b₁,b₂:],b₃
for b₆ being FinSequence of b₂ holds b₅ [;] b₄,b₆ is FinSequence of b₃

proof end;

theorem Th92: :: FINSEQ_2:92

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being FinSequence
for b₆ being Function of [:b₁,b₂:],b₃
for b₇ being FinSequence of b₂ st b₅ = b₆ [;] b₄,b₇ holds
len b₅ = len b₇

proof end;

theorem Th93: :: FINSEQ_2:93

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Function of [:b₁,b₂:],b₃ holds b₅ [;] b₄,(<*> b₂) = <*> b₃

proof end;

theorem Th94: :: FINSEQ_2:94

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Function of [:b₁,b₂:],b₃
for b₇ being FinSequence of b₂ st b₇ = <*b₅*> holds
b₆ [;] b₄,b₇ = <*(b₆ . b₄,b₅)*>

proof end;

theorem Th95: :: FINSEQ_2:95

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅, b₆ being Element of b₂
for b₇ being Function of [:b₁,b₂:],b₃
for b₈ being FinSequence of b₂ st b₈ = <*b₅,b₆*> holds
b₇ [;] b₄,b₈ = <*(b₇ . b₄,b₅),(b₇ . b₄,b₆)*>

proof end;

theorem Th96: :: FINSEQ_2:96

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅, b₆, b₇ being Element of b₂
for b₈ being Function of [:b₁,b₂:],b₃
for b₉ being FinSequence of b₂ st b₉ = <*b₅,b₆,b₇*> holds
b₈ [;] b₄,b₉ = <*(b₈ . b₄,b₅),(b₈ . b₄,b₆),(b₈ . b₄,b₇)*>

proof end;

theorem Th97: :: FINSEQ_2:97

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₂
for b₅ being Function of [:b₁,b₂:],b₃
for b₆ being FinSequence of b₁ holds b₅ [:] b₆,b₄ is FinSequence of b₃

proof end;

theorem Th98: :: FINSEQ_2:98

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₂
for b₅ being FinSequence
for b₆ being Function of [:b₁,b₂:],b₃
for b₇ being FinSequence of b₁ st b₅ = b₆ [:] b₇,b₄ holds
len b₅ = len b₇

proof end;

theorem Th99: :: FINSEQ_2:99

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₂
for b₅ being Function of [:b₁,b₂:],b₃ holds b₅ [:] (<*> b₁),b₄ = <*> b₃

proof end;

theorem Th100: :: FINSEQ_2:100

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₁
for b₅ being Element of b₂
for b₆ being Function of [:b₁,b₂:],b₃
for b₇ being FinSequence of b₁ st b₇ = <*b₄*> holds
b₆ [:] b₇,b₅ = <*(b₆ . b₄,b₅)*>

proof end;

theorem Th101: :: FINSEQ_2:101

for b₁, b₂, b₃ being non empty set
for b₄, b₅ being Element of b₁
for b₆ being Element of b₂
for b₇ being Function of [:b₁,b₂:],b₃
for b₈ being FinSequence of b₁ st b₈ = <*b₄,b₅*> holds
b₇ [:] b₈,b₆ = <*(b₇ . b₄,b₆),(b₇ . b₅,b₆)*>

proof end;

theorem Th102: :: FINSEQ_2:102

for b₁, b₂, b₃ being non empty set
for b₄, b₅, b₆ being Element of b₁
for b₇ being Element of b₂
for b₈ being Function of [:b₁,b₂:],b₃
for b₉ being FinSequence of b₁ st b₉ = <*b₄,b₅,b₆*> holds
b₈ [:] b₉,b₇ = <*(b₈ . b₄,b₇),(b₈ . b₅,b₇),(b₈ . b₆,b₇)*>

proof end;

definition

let c₁ be set ;
mode FinSequenceSet of c₁ -> set means :Def3: :: FINSEQ_2:def 3
for b₁ being set st b₁ in a₂ holds
b₁ is FinSequence of a₁;
existence

proof end;

end;

:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def 3 :

registration

let c₁ be set ;
cluster non empty FinSequenceSet of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode FinSequence-DOMAIN of a₁ is non empty FinSequenceSet of a₁;

end;

theorem Th103: :: FINSEQ_2:103

canceled;

theorem Th104: :: FINSEQ_2:104

for b₁ being set holds b₁ * is FinSequence-DOMAIN of b₁

proof end;

definition

let c₁ be set ;
redefine func * as c₁ * -> FinSequence-DOMAIN of a₁;
coherence by Th104;

end;

theorem Th105: :: FINSEQ_2:105

for b₁ being set
for b₂ being FinSequence-DOMAIN of b₁ holds b₂ c= b₁ *

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence-DOMAIN of c₁;
redefine mode Element as Element of c₂ -> FinSequence of a₁;
coherence by Def3;

end;

theorem Th106: :: FINSEQ_2:106

canceled;

theorem Th107: :: FINSEQ_2:107

for b₁ being non empty set
for b₂ being non empty Subset of b₁
for b₃ being FinSequence-DOMAIN of b₂ holds b₃ is FinSequence-DOMAIN of b₁

proof end;

definition

let c₁ be natural number ;
let c₂ be set ;
func c₁ -tuples_on c₂ -> FinSequenceSet of a₂ equals :: FINSEQ_2:def 4
{ b₁ where B is Element of a₂ * : len b₁ = a₁ } ;
coherence

proof end;

end;

:: deftheorem Def4 defines -tuples_on FINSEQ_2:def 4 :

registration

let c₁ be natural number ;
let c₂ be non empty set ;
cluster a₁ -tuples_on a₂ -> non empty ;
coherence

proof end;

end;

theorem Th108: :: FINSEQ_2:108

canceled;

theorem Th109: :: FINSEQ_2:109

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₁ -tuples_on b₂ holds len b₃ = b₁

proof end;

theorem Th110: :: FINSEQ_2:110

for b₁ being set
for b₂ being FinSequence of b₁ holds b₂ is Element of (len b₂) -tuples_on b₁

proof end;

theorem Th111: :: FINSEQ_2:111

for b₁ being Nat
for b₂ being non empty set holds b₁ -tuples_on b₂ = Funcs (Seg b₁),b₂

proof end;

theorem Th112: :: FINSEQ_2:112

for b₁ being set holds 0 -tuples_on b₁ = {(<*> b₁)}

proof end;

theorem Th113: :: FINSEQ_2:113

for b₁ being set
for b₂ being Element of 0 -tuples_on b₁ holds b₂ = <*> b₁

proof end;

theorem Th114: :: FINSEQ_2:114

for b₁ being set holds <*> b₁ is Element of 0 -tuples_on b₁

proof end;

theorem Th115: :: FINSEQ_2:115

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of 0 -tuples_on b₂
for b₄ being Element of b₁ -tuples_on b₂ holds
( b₃ ^ b₄ = b₄ & b₄ ^ b₃ = b₄ )

proof end;

theorem Th116: :: FINSEQ_2:116

for b₁ being non empty set holds 1 -tuples_on b₁ = { <*b₂*> where B is Element of b₁ : verum }

proof end;

theorem Th117: :: FINSEQ_2:117

for b₁ being non empty set
for b₂ being Element of 1 -tuples_on b₁ ex b₃ being Element of b₁ st b₂ = <*b₃*>

proof end;

theorem Th118: :: FINSEQ_2:118

for b₁ being non empty set
for b₂ being Element of b₁ holds <*b₂*> is Element of 1 -tuples_on b₁

proof end;

theorem Th119: :: FINSEQ_2:119

for b₁ being non empty set holds 2 -tuples_on b₁ = { <*b₂,b₃*> where B is Element of b₁, B is Element of b₁ : verum }

proof end;

theorem Th120: :: FINSEQ_2:120

for b₁ being non empty set
for b₂ being Element of 2 -tuples_on b₁ ex b₃, b₄ being Element of b₁ st b₂ = <*b₃,b₄*>

proof end;

theorem Th121: :: FINSEQ_2:121

for b₁ being non empty set
for b₂, b₃ being Element of b₁ holds <*b₂,b₃*> is Element of 2 -tuples_on b₁

proof end;

theorem Th122: :: FINSEQ_2:122

for b₁ being non empty set holds 3 -tuples_on b₁ = { <*b₂,b₃,b₄*> where B is Element of b₁, B is Element of b₁, B is Element of b₁ : verum }

proof end;

theorem Th123: :: FINSEQ_2:123

for b₁ being non empty set
for b₂ being Element of 3 -tuples_on b₁ ex b₃, b₄, b₅ being Element of b₁ st b₂ = <*b₃,b₄,b₅*>

proof end;

theorem Th124: :: FINSEQ_2:124

for b₁ being non empty set
for b₂, b₃, b₄ being Element of b₁ holds <*b₂,b₃,b₄*> is Element of 3 -tuples_on b₁

proof end;

theorem Th125: :: FINSEQ_2:125

for b₁, b₂ being Nat
for b₃ being non empty set holds (b₁ + b₂) -tuples_on b₃ = { (b₄ ^ b₅) where B is Element of b₁ -tuples_on b₃, B is Element of b₂ -tuples_on b₃ : verum }

proof end;

theorem Th126: :: FINSEQ_2:126

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Element of (b₁ + b₂) -tuples_on b₃ ex b₅ being Element of b₁ -tuples_on b₃ex b₆ being Element of b₂ -tuples_on b₃ st b₄ = b₅ ^ b₆

proof end;

theorem Th127: :: FINSEQ_2:127

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being Element of b₁ -tuples_on b₃
for b₅ being Element of b₂ -tuples_on b₃ holds b₄ ^ b₅ is Element of (b₁ + b₂) -tuples_on b₃

proof end;

theorem Th128: :: FINSEQ_2:128

for b₁ being non empty set holds b₁ * = union { (b₂ -tuples_on b₁) where B is Nat : verum }

proof end;

theorem Th129: :: FINSEQ_2:129

for b₁ being Nat
for b₂ being non empty set
for b₃ being non empty Subset of b₂
for b₄ being Element of b₁ -tuples_on b₃ holds b₄ is Element of b₁ -tuples_on b₂

proof end;

theorem Th130: :: FINSEQ_2:130

for b₁, b₂ being Nat
for b₃ being non empty set st b₁ -tuples_on b₃ = b₂ -tuples_on b₃ holds
b₁ = b₂

proof end;

theorem Th131: :: FINSEQ_2:131

for b₁ being Nat holds idseq b₁ is Element of b₁ -tuples_on NAT

proof end;

theorem Th132: :: FINSEQ_2:132

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₂ holds b₁ |-> b₃ is Element of b₁ -tuples_on b₂

proof end;

theorem Th133: :: FINSEQ_2:133

for b₁ being Nat
for b₂, b₃ being non empty set
for b₄ being Element of b₁ -tuples_on b₂
for b₅ being Function of b₂,b₃ holds b₅ * b₄ is Element of b₁ -tuples_on b₃

proof end;

theorem Th134: :: FINSEQ_2:134

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₁ -tuples_on b₂
for b₄ being Function of Seg b₁, Seg b₁ st rng b₄ = Seg b₁ holds
b₃ * b₄ is Element of b₁ -tuples_on b₂

proof end;

theorem Th135: :: FINSEQ_2:135

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₁ -tuples_on b₂
for b₄ being Permutation of Seg b₁ holds b₃ * b₄ is Element of b₁ -tuples_on b₂

proof end;

theorem Th136: :: FINSEQ_2:136

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₁ -tuples_on b₂
for b₄ being Element of b₂ holds (b₃ ^ <*b₄*>) . (b₁ + 1) = b₄

proof end;

theorem Th137: :: FINSEQ_2:137

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of (b₁ + 1) -tuples_on b₂ ex b₄ being Element of b₁ -tuples_on b₂ex b₅ being Element of b₂ st b₃ = b₄ ^ <*b₅*>

proof end;

theorem Th138: :: FINSEQ_2:138

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₁ -tuples_on b₂ holds b₃ * (idseq b₁) = b₃

proof end;

theorem Th139: :: FINSEQ_2:139

for b₁ being Nat
for b₂ being non empty set
for b₃, b₄ being Element of b₁ -tuples_on b₂ st ( for b₅ being Nat st b₅ in Seg b₁ holds
b₃ . b₅ = b₄ . b₅ ) holds
b₃ = b₄

proof end;

theorem Th140: :: FINSEQ_2:140

for b₁ being Nat
for b₂, b₃, b₄ being non empty set
for b₅ being Function of [:b₂,b₃:],b₄
for b₆ being Element of b₁ -tuples_on b₂
for b₇ being Element of b₁ -tuples_on b₃ holds b₅ .: b₆,b₇ is Element of b₁ -tuples_on b₄

proof end;

theorem Th141: :: FINSEQ_2:141

for b₁ being Nat
for b₂, b₃, b₄ being non empty set
for b₅ being Element of b₂
for b₆ being Function of [:b₂,b₃:],b₄
for b₇ being Element of b₁ -tuples_on b₃ holds b₆ [;] b₅,b₇ is Element of b₁ -tuples_on b₄

proof end;

theorem Th142: :: FINSEQ_2:142

for b₁ being Nat
for b₂, b₃, b₄ being non empty set
for b₅ being Element of b₃
for b₆ being Function of [:b₂,b₃:],b₄
for b₇ being Element of b₁ -tuples_on b₂ holds b₆ [:] b₇,b₅ is Element of b₁ -tuples_on b₄

proof end;

theorem Th143: :: FINSEQ_2:143

for b₁, b₂ being Nat
for b₃ being set holds (b₁ + b₂) |-> b₃ = (b₁ |-> b₃) ^ (b₂ |-> b₃)

proof end;

theorem Th144: :: FINSEQ_2:144

for b₁ being Nat
for b₂ being non empty set
for b₃ being Element of b₁ -tuples_on b₂ holds dom b₃ = Seg b₁

proof end;

theorem Th145: :: FINSEQ_2:145

for b₁ being Function
for b₂, b₃ being set st b₂ in dom b₁ & b₃ in dom b₁ holds
b₁ * <*b₂,b₃*> = <*(b₁ . b₂),(b₁ . b₃)*>

proof end;

theorem Th146: :: FINSEQ_2:146

for b₁ being Function
for b₂, b₃, b₄ being set st b₂ in dom b₁ & b₃ in dom b₁ & b₄ in dom b₁ holds
b₁ * <*b₂,b₃,b₄*> = <*(b₁ . b₂),(b₁ . b₃),(b₁ . b₄)*>

proof end;

theorem Th147: :: FINSEQ_2:147

for b₁, b₂ being set holds rng <*b₁,b₂*> = {b₁,b₂} by Lemma10;

theorem Th148: :: FINSEQ_2:148

for b₁, b₂, b₃ being set holds rng <*b₁,b₂,b₃*> = {b₁,b₂,b₃} by Lemma12;

theorem Th149: :: FINSEQ_2:149

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

proof end;