:: by Czes{\l}aw Byli\'nski

::

:: Received March 1, 1990

:: Copyright (c) 1990-2021 Association of Mizar Users

::$CT

:: Additional propositions related to Finite Sequences

theorem :: FINSEQ_2:9

for p, q being FinSequence st len p = len q & ( for j being Nat st j in dom p holds

p . j = q . j ) holds

p = q

p . j = q . j ) holds

p = q

proof end;

theorem Th8: :: FINSEQ_2:10

for b being object

for p being FinSequence st b in rng p holds

ex i being Nat st

( i in dom p & p . i = b )

for p being FinSequence st b in rng p holds

ex i being Nat st

( i in dom p & p . i = b )

proof end;

theorem Th9: :: FINSEQ_2:11

for i being natural Number

for D being set

for p being FinSequence of D st i in dom p holds

p . i in D

for D being set

for p being FinSequence of D st i in dom p holds

p . i in D

proof end;

theorem Th10: :: FINSEQ_2:12

for p being FinSequence

for D being set st ( for i being Nat st i in dom p holds

p . i in D ) holds

p is FinSequence of D

for D being set st ( for i being Nat st i in dom p holds

p . i in D ) holds

p is FinSequence of D

proof end;

Lm1: for x1, x2 being object holds rng <*x1,x2*> = {x1,x2}

proof end;

Lm2: for x1, x2, x3 being object holds rng <*x1,x2,x3*> = {x1,x2,x3}

proof end;

theorem :: FINSEQ_2:18

for i being natural Number

for p being FinSequence st len p = i + 1 holds

ex q being FinSequence ex a being object st p = q ^ <*a*> by CARD_1:27, FINSEQ_1:46;

for p being FinSequence st len p = i + 1 holds

ex q being FinSequence ex a being object st p = q ^ <*a*> by CARD_1:27, FINSEQ_1:46;

theorem Th17: :: FINSEQ_2:19

for A being set

for p being FinSequence of A st len p <> 0 holds

ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>

for p being FinSequence of A st len p <> 0 holds

ex q being FinSequence of A ex d being Element of A st p = q ^ <*d*>

proof end;

theorem :: FINSEQ_2:21

for i being natural Number

for p, q being FinSequence st q = p | (Seg i) holds

len q = min (i,(len p))

for p, q being FinSequence st q = p | (Seg i) holds

len q = min (i,(len p))

proof end;

theorem Th20: :: FINSEQ_2:22

for i, j being natural Number

for r being FinSequence st len r = i + j holds

ex p, q being FinSequence st

( len p = i & len q = j & r = p ^ q )

for r being FinSequence st len r = i + j holds

ex p, q being FinSequence st

( len p = i & len q = j & r = p ^ q )

proof end;

theorem Th21: :: FINSEQ_2:23

for i, j being natural Number

for D being non empty set

for r being FinSequence of D st len r = i + j holds

ex p, q being FinSequence of D st

( len p = i & len q = j & r = p ^ q )

for D being non empty set

for r being FinSequence of D st len r = i + j holds

ex p, q being FinSequence of D st

( len p = i & len q = j & r = p ^ q )

proof end;

scheme :: FINSEQ_2:sch 2

IndSeqD{ F_{1}() -> set , P_{1}[ set ] } :

provided

IndSeqD{ F

provided

A1:
P_{1}[ <*> F_{1}()]
and

A2: for p being FinSequence of F_{1}()

for x being Element of F_{1}() st P_{1}[p] holds

P_{1}[p ^ <*x*>]

A2: for p being FinSequence of F

for x being Element of F

P

proof end;

theorem Th23: :: FINSEQ_2:25

for i being natural Number

for D being non empty set

for f being Function of (Seg i),D holds f is FinSequence of D

for D being non empty set

for f being Function of (Seg i),D holds f is FinSequence of D

proof end;

theorem :: FINSEQ_2:27

for i being natural Number

for D being non empty set

for f being sequence of D holds f | (Seg i) is FinSequence of D

for D being non empty set

for f being sequence of D holds f | (Seg i) is FinSequence of D

proof end;

theorem :: FINSEQ_2:28

for i being natural Number

for D being non empty set

for q being FinSequence

for f being sequence of D st q = f | (Seg i) holds

len q = i

for D being non empty set

for q being FinSequence

for f being sequence of D st q = f | (Seg i) holds

len q = i

proof end;

theorem Th28: :: FINSEQ_2:30

for i being natural Number

for D being non empty set st D = Seg i holds

for p being FinSequence

for q being FinSequence of D st i <= len p holds

p * q is FinSequence

for D being non empty set st D = Seg i holds

for p being FinSequence

for q being FinSequence of D st i <= len p holds

p * q is FinSequence

proof end;

theorem :: FINSEQ_2:31

for i being natural Number

for D, D9 being non empty set st D = Seg i holds

for p being FinSequence of D9

for q being FinSequence of D st i <= len p holds

p * q is FinSequence of D9

for D, D9 being non empty set st D = Seg i holds

for p being FinSequence of D9

for q being FinSequence of D st i <= len p holds

p * q is FinSequence of D9

proof end;

theorem Th30: :: FINSEQ_2:32

for A, D being set

for p being FinSequence of A

for f being Function of A,D holds f * p is FinSequence of D

for p being FinSequence of A

for f being Function of A,D holds f * p is FinSequence of D

proof end;

theorem Th31: :: FINSEQ_2:33

for A being set

for D9 being non empty set

for q being FinSequence

for p being FinSequence of A

for f being Function of A,D9 st q = f * p holds

len q = len p

for D9 being non empty set

for q being FinSequence

for p being FinSequence of A

for f being Function of A,D9 st q = f * p holds

len q = len p

proof end;

theorem :: FINSEQ_2:35

for x1 being object

for D, D9 being non empty set

for p being FinSequence of D

for f being Function of D,D9 st p = <*x1*> holds

f * p = <*(f . x1)*>

for D, D9 being non empty set

for p being FinSequence of D

for f being Function of D,D9 st p = <*x1*> holds

f * p = <*(f . x1)*>

proof end;

theorem Th34: :: FINSEQ_2:36

for x1, x2 being object

for D, D9 being non empty set

for p being FinSequence of D

for f being Function of D,D9 st p = <*x1,x2*> holds

f * p = <*(f . x1),(f . x2)*>

for D, D9 being non empty set

for p being FinSequence of D

for f being Function of D,D9 st p = <*x1,x2*> holds

f * p = <*(f . x1),(f . x2)*>

proof end;

theorem Th35: :: FINSEQ_2:37

for x1, x2, x3 being object

for D, D9 being non empty set

for p being FinSequence of D

for f being Function of D,D9 st p = <*x1,x2,x3*> holds

f * p = <*(f . x1),(f . x2),(f . x3)*>

for D, D9 being non empty set

for p being FinSequence of D

for f being Function of D,D9 st p = <*x1,x2,x3*> holds

f * p = <*(f . x1),(f . x2),(f . x3)*>

proof end;

theorem Th36: :: FINSEQ_2:38

for i, j being natural Number

for p being FinSequence

for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds

p * f is FinSequence

for p being FinSequence

for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds

p * f is FinSequence

proof end;

theorem :: FINSEQ_2:39

theorem Th39: :: FINSEQ_2:41

for i being natural Number

for p, q being FinSequence

for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds

len q = i

for p, q being FinSequence

for f being Function of (Seg i),(Seg i) st rng f = Seg i & i <= len p & q = p * f holds

len q = i

proof end;

theorem Th40: :: FINSEQ_2:42

for p, q being FinSequence

for f being Function of (dom p),(dom p) st rng f = dom p & q = p * f holds

len q = len p

for f being Function of (dom p),(dom p) st rng f = dom p & q = p * f holds

len q = len p

proof end;

theorem Th41: :: FINSEQ_2:43

for i being natural Number

for p, q being FinSequence

for f being Permutation of (Seg i) st i <= len p & q = p * f holds

len q = i

for p, q being FinSequence

for f being Permutation of (Seg i) st i <= len p & q = p * f holds

len q = i

proof end;

theorem Th43: :: FINSEQ_2:45

for i, j being natural Number

for D being non empty set

for p being FinSequence of D

for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds

p * f is FinSequence of D

for D being non empty set

for p being FinSequence of D

for f being Function of (Seg i),(Seg j) st ( j = 0 implies i = 0 ) & j <= len p holds

p * f is FinSequence of D

proof end;

theorem :: FINSEQ_2:46

theorem Th45: :: FINSEQ_2:47

for D being non empty set

for p being FinSequence of D

for f being Function of (dom p),(dom p) holds p * f is FinSequence of D

for p being FinSequence of D

for f being Function of (dom p),(dom p) holds p * f is FinSequence of D

proof end;

theorem :: FINSEQ_2:49

registration
end;

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

for i being natural Number

for a being object holds i |-> a = (Seg i) --> a;

for i being natural Number

for a being object holds i |-> a = (Seg i) --> a;

registration
end;

theorem :: FINSEQ_2:57

theorem Th61: :: FINSEQ_2:63

for D being non empty set

for d being Element of D

for k being natural Number holds k |-> d is FinSequence of D

for d being Element of D

for k being natural Number holds k |-> d is FinSequence of D

proof end;

Lm3: for i being natural Number

for p, q being FinSequence

for F being Function st [:(rng p),(rng q):] c= dom F & i = min ((len p),(len q)) holds

dom (F .: (p,q)) = Seg i

proof end;

theorem Th62: :: FINSEQ_2:64

for p, q being FinSequence

for F being Function st [:(rng p),(rng q):] c= dom F holds

F .: (p,q) is FinSequence

for F being Function st [:(rng p),(rng q):] c= dom F holds

F .: (p,q) is FinSequence

proof end;

theorem Th63: :: FINSEQ_2:65

for p, q, r being FinSequence

for F being Function st [:(rng p),(rng q):] c= dom F & r = F .: (p,q) holds

len r = min ((len p),(len q))

for F being Function st [:(rng p),(rng q):] c= dom F & r = F .: (p,q) holds

len r = min ((len p),(len q))

proof end;

Lm4: for a being object

for p being FinSequence

for F being Function st [:{a},(rng p):] c= dom F holds

dom (F [;] (a,p)) = dom p

proof end;

theorem Th64: :: FINSEQ_2:66

for a being object

for p being FinSequence

for F being Function st [:{a},(rng p):] c= dom F holds

F [;] (a,p) is FinSequence

for p being FinSequence

for F being Function st [:{a},(rng p):] c= dom F holds

F [;] (a,p) is FinSequence

proof end;

theorem Th65: :: FINSEQ_2:67

for a being object

for p, r being FinSequence

for F being Function st [:{a},(rng p):] c= dom F & r = F [;] (a,p) holds

len r = len p

for p, r being FinSequence

for F being Function st [:{a},(rng p):] c= dom F & r = F [;] (a,p) holds

len r = len p

proof end;

Lm5: for a being object

for p being FinSequence

for F being Function st [:(rng p),{a}:] c= dom F holds

dom (F [:] (p,a)) = dom p

proof end;

theorem Th66: :: FINSEQ_2:68

for a being object

for p being FinSequence

for F being Function st [:(rng p),{a}:] c= dom F holds

F [:] (p,a) is FinSequence

for p being FinSequence

for F being Function st [:(rng p),{a}:] c= dom F holds

F [:] (p,a) is FinSequence

proof end;

theorem Th67: :: FINSEQ_2:69

for a being object

for p, r being FinSequence

for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] (p,a) holds

len r = len p

for p, r being FinSequence

for F being Function st [:(rng p),{a}:] c= dom F & r = F [:] (p,a) holds

len r = len p

proof end;

theorem Th68: :: FINSEQ_2:70

for D, D9, E being non empty set

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 holds F .: (p,q) is FinSequence of E

proof end;

theorem Th69: :: FINSEQ_2:71

for D, D9, E being non empty set

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st r = F .: (p,q) holds

len r = min ((len p),(len q))

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st r = F .: (p,q) holds

len r = min ((len p),(len q))

proof end;

theorem Th70: :: FINSEQ_2:72

for D, D9, E being non empty set

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds

( len r = len p & len r = len q )

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st len p = len q & r = F .: (p,q) holds

( len r = len p & len r = len q )

proof end;

theorem :: FINSEQ_2:73

for D, D9, E being non empty set

for F being Function of [:D,D9:],E

for p being FinSequence of D

for p9 being FinSequence of D9 holds

( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )

for F being Function of [:D,D9:],E

for p being FinSequence of D

for p9 being FinSequence of D9 holds

( F .: ((<*> D),p9) = <*> E & F .: (p,(<*> D9)) = <*> E )

proof end;

theorem :: FINSEQ_2:74

for D, D9, E being non empty set

for d1 being Element of D

for d19 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st p = <*d1*> & q = <*d19*> holds

F .: (p,q) = <*(F . (d1,d19))*>

for d1 being Element of D

for d19 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st p = <*d1*> & q = <*d19*> holds

F .: (p,q) = <*(F . (d1,d19))*>

proof end;

theorem :: FINSEQ_2:75

for D, D9, E being non empty set

for d1, d2 being Element of D

for d19, d29 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st p = <*d1,d2*> & q = <*d19,d29*> holds

F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*>

for d1, d2 being Element of D

for d19, d29 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st p = <*d1,d2*> & q = <*d19,d29*> holds

F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29))*>

proof end;

theorem :: FINSEQ_2:76

for D, D9, E being non empty set

for d1, d2, d3 being Element of D

for d19, d29, d39 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st p = <*d1,d2,d3*> & q = <*d19,d29,d39*> holds

F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*>

for d1, d2, d3 being Element of D

for d19, d29, d39 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D

for q being FinSequence of D9 st p = <*d1,d2,d3*> & q = <*d19,d29,d39*> holds

F .: (p,q) = <*(F . (d1,d19)),(F . (d2,d29)),(F . (d3,d39))*>

proof end;

theorem Th75: :: FINSEQ_2:77

for D, D9, E being non empty set

for d being Element of D

for F being Function of [:D,D9:],E

for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E

for d being Element of D

for F being Function of [:D,D9:],E

for p being FinSequence of D9 holds F [;] (d,p) is FinSequence of E

proof end;

theorem Th76: :: FINSEQ_2:78

for D, D9, E being non empty set

for d being Element of D

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st r = F [;] (d,p) holds

len r = len p

for d being Element of D

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st r = F [;] (d,p) holds

len r = len p

proof end;

theorem :: FINSEQ_2:79

for D, D9, E being non empty set

for d being Element of D

for F being Function of [:D,D9:],E holds F [;] (d,(<*> D9)) = <*> E

for d being Element of D

for F being Function of [:D,D9:],E holds F [;] (d,(<*> D9)) = <*> E

proof end;

theorem :: FINSEQ_2:80

for D, D9, E being non empty set

for d being Element of D

for d19 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st p = <*d19*> holds

F [;] (d,p) = <*(F . (d,d19))*>

for d being Element of D

for d19 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st p = <*d19*> holds

F [;] (d,p) = <*(F . (d,d19))*>

proof end;

theorem :: FINSEQ_2:81

for D, D9, E being non empty set

for d being Element of D

for d19, d29 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st p = <*d19,d29*> holds

F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29))*>

for d being Element of D

for d19, d29 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st p = <*d19,d29*> holds

F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29))*>

proof end;

theorem :: FINSEQ_2:82

for D, D9, E being non empty set

for d being Element of D

for d19, d29, d39 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st p = <*d19,d29,d39*> holds

F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*>

for d being Element of D

for d19, d29, d39 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D9 st p = <*d19,d29,d39*> holds

F [;] (d,p) = <*(F . (d,d19)),(F . (d,d29)),(F . (d,d39))*>

proof end;

theorem Th81: :: FINSEQ_2:83

for D, D9, E being non empty set

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D holds F [:] (p,d9) is FinSequence of E

proof end;

theorem Th82: :: FINSEQ_2:84

for D, D9, E being non empty set

for d9 being Element of D9

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D st r = F [:] (p,d9) holds

len r = len p

for d9 being Element of D9

for r being FinSequence

for F being Function of [:D,D9:],E

for p being FinSequence of D st r = F [:] (p,d9) holds

len r = len p

proof end;

theorem :: FINSEQ_2:85

for D, D9, E being non empty set

for d9 being Element of D9

for F being Function of [:D,D9:],E holds F [:] ((<*> D),d9) = <*> E

for d9 being Element of D9

for F being Function of [:D,D9:],E holds F [:] ((<*> D),d9) = <*> E

proof end;

theorem :: FINSEQ_2:86

for D, D9, E being non empty set

for d1 being Element of D

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D st p = <*d1*> holds

F [:] (p,d9) = <*(F . (d1,d9))*>

for d1 being Element of D

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D st p = <*d1*> holds

F [:] (p,d9) = <*(F . (d1,d9))*>

proof end;

theorem :: FINSEQ_2:87

for D, D9, E being non empty set

for d1, d2 being Element of D

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D st p = <*d1,d2*> holds

F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*>

for d1, d2 being Element of D

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D st p = <*d1,d2*> holds

F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9))*>

proof end;

theorem :: FINSEQ_2:88

for D, D9, E being non empty set

for d1, d2, d3 being Element of D

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D st p = <*d1,d2,d3*> holds

F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*>

for d1, d2, d3 being Element of D

for d9 being Element of D9

for F being Function of [:D,D9:],E

for p being FinSequence of D st p = <*d1,d2,d3*> holds

F [:] (p,d9) = <*(F . (d1,d9)),(F . (d2,d9)),(F . (d3,d9))*>

proof end;

:: Tuples

definition

let D be set ;

ex b_{1} being set st

for a being object st a in b_{1} holds

a is FinSequence of D

end;
mode FinSequenceSet of D -> set means :Def3: :: FINSEQ_2:def 3

for a being object st a in it holds

a is FinSequence of D;

existence for a being object st a in it holds

a is FinSequence of D;

ex b

for a being object st a in b

a is FinSequence of D

proof end;

:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def 3 :

for D, b_{2} being set holds

( b_{2} is FinSequenceSet of D iff for a being object st a in b_{2} holds

a is FinSequence of D );

for D, b

( b

a is FinSequence of D );

definition

let D be set ;

let S be FinSequenceSet of D;

:: original: Element

redefine mode Element of S -> FinSequence of D;

coherence

for b_{1} being Element of S holds b_{1} is FinSequence of D

end;
let S be FinSequenceSet of D;

:: original: Element

redefine mode Element of S -> FinSequence of D;

coherence

for b

proof end;

registration
end;

definition

let D be set ;

:: original: *

redefine func D * -> FinSequenceSet of D;

coherence

D * is FinSequenceSet of D by Th87;

end;
:: original: *

redefine func D * -> FinSequenceSet of D;

coherence

D * is FinSequenceSet of D by Th87;

theorem :: FINSEQ_2:91

for D being non empty set

for D9 being Subset of D

for S being FinSequenceSet of D9 holds S is FinSequenceSet of D

for D9 being Subset of D

for S being FinSequenceSet of D9 holds S is FinSequenceSet of D

proof end;

registration

let i be natural Number ;

let D be non empty set ;

ex b_{1} being FinSequence of D st b_{1} is i -element

end;
let D be non empty set ;

cluster Relation-like omega -defined D -valued Function-like V49() i -element FinSequence-like FinSubsequence-like countable for FinSequence of D;

existence ex b

proof end;

definition
end;

definition

let i be natural Number ;

let D be set ;

{ s where s is Element of D * : len s = i } is FinSequenceSet of D

end;
let D be set ;

func i -tuples_on D -> FinSequenceSet of D equals :: FINSEQ_2:def 4

{ s where s is Element of D * : len s = i } ;

coherence { s where s is Element of D * : len s = i } ;

{ s where s is Element of D * : len s = i } is FinSequenceSet of D

proof end;

:: deftheorem defines -tuples_on FINSEQ_2:def 4 :

for i being natural Number

for D being set holds i -tuples_on D = { s where s is Element of D * : len s = i } ;

for i being natural Number

for D being set holds i -tuples_on D = { s where s is Element of D * : len s = i } ;

registration
end;

registration

let D be non empty set ;

let i be natural Number ;

coherence

for b_{1} being Element of i -tuples_on D holds b_{1} is i -element

end;
let i be natural Number ;

coherence

for b

proof end;

theorem :: FINSEQ_2:95

Lm6: for i being natural Number

for D being non empty set

for z being Tuple of i,D holds z in i -tuples_on D

proof end;

theorem Th100: :: FINSEQ_2:102

for D being non empty set holds 3 -tuples_on D = { <*d1,d2,d3*> where d1, d2, d3 is Element of D : verum }

proof end;

theorem :: FINSEQ_2:103

for D being non empty set

for z being Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>

for z being Tuple of 3,D ex d1, d2, d3 being Element of D st z = <*d1,d2,d3*>

proof end;

theorem Th103: :: FINSEQ_2:105

for i, j being natural Number

for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }

for D being non empty set holds (i + j) -tuples_on D = { (z ^ t) where z is Tuple of i,D, t is Tuple of j,D : verum }

proof end;

theorem Th104: :: FINSEQ_2:106

for i, j being natural Number

for D being non empty set

for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t

for D being non empty set

for s being Tuple of i + j,D ex z being Element of i -tuples_on D ex t being Element of j -tuples_on D st s = z ^ t

proof end;

theorem :: FINSEQ_2:107

theorem :: FINSEQ_2:109

for i being natural Number

for D being non empty set

for D9 being non empty Subset of D

for z being Tuple of i,D9 holds z is Element of i -tuples_on D

for D being non empty set

for D9 being non empty Subset of D

for z being Tuple of i,D9 holds z is Element of i -tuples_on D

proof end;

Lm7: for i being natural Number

for A being set

for x being object st x in i -tuples_on A holds

x is b

proof end;

theorem :: FINSEQ_2:110

for i, j being natural Number

for A being set

for D being non empty set st i -tuples_on D = j -tuples_on A holds

i = j

for A being set

for D being non empty set st i -tuples_on D = j -tuples_on A holds

i = j

proof end;

theorem Th110: :: FINSEQ_2:112

for i being natural Number

for D being non empty set

for d being Element of D holds i |-> d is Element of i -tuples_on D

for D being non empty set

for d being Element of D holds i |-> d is Element of i -tuples_on D

proof end;

theorem :: FINSEQ_2:113

for i being natural Number

for D, D9 being non empty set

for z being Tuple of i,D

for f being Function of D,D9 holds f * z is Element of i -tuples_on D9

for D, D9 being non empty set

for z being Tuple of i,D

for f being Function of D,D9 holds f * z is Element of i -tuples_on D9

proof end;

theorem Th112: :: FINSEQ_2:114

for i being natural Number

for D being non empty set

for z being Tuple of i,D

for f being Function of (Seg i),(Seg i) st rng f = Seg i holds

z * f is Element of i -tuples_on D

for D being non empty set

for z being Tuple of i,D

for f being Function of (Seg i),(Seg i) st rng f = Seg i holds

z * f is Element of i -tuples_on D

proof end;

theorem :: FINSEQ_2:115

for i being natural Number

for D being non empty set

for z being Tuple of i,D

for f being Permutation of (Seg i) holds z * f is Tuple of i,D

for D being non empty set

for z being Tuple of i,D

for f being Permutation of (Seg i) holds z * f is Tuple of i,D

proof end;

theorem :: FINSEQ_2:116

for i being natural Number

for D being non empty set

for z being Tuple of i,D

for d being Element of D holds (z ^ <*d*>) . (i + 1) = d

for D being non empty set

for z being Tuple of i,D

for d being Element of D holds (z ^ <*d*>) . (i + 1) = d

proof end;

theorem :: FINSEQ_2:117

for i being natural Number

for D being non empty set

for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>

for D being non empty set

for z being Tuple of i + 1,D ex t being Element of i -tuples_on D ex d being Element of D st z = t ^ <*d*>

proof end;

theorem :: FINSEQ_2:118

for i being natural Number

for D being non empty set

for z being Tuple of i,D holds z * (idseq i) = z

for D being non empty set

for z being Tuple of i,D holds z * (idseq i) = z

proof end;

theorem :: FINSEQ_2:119

for i being natural Number

for D being non empty set

for z1, z2 being Tuple of i,D st ( for j being Nat st j in Seg i holds

z1 . j = z2 . j ) holds

z1 = z2

for D being non empty set

for z1, z2 being Tuple of i,D st ( for j being Nat st j in Seg i holds

z1 . j = z2 . j ) holds

z1 = z2

proof end;

theorem :: FINSEQ_2:120

for i being natural Number

for D, D9, E being non empty set

for F being Function of [:D,D9:],E

for z1 being Tuple of i,D

for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E

for D, D9, E being non empty set

for F being Function of [:D,D9:],E

for z1 being Tuple of i,D

for z2 being Tuple of i,D9 holds F .: (z1,z2) is Element of i -tuples_on E

proof end;

theorem :: FINSEQ_2:121

for i being natural Number

for D, D9, E being non empty set

for d being Element of D

for F being Function of [:D,D9:],E

for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E

for D, D9, E being non empty set

for d being Element of D

for F being Function of [:D,D9:],E

for z being Tuple of i,D9 holds F [;] (d,z) is Element of i -tuples_on E

proof end;

theorem :: FINSEQ_2:122

for i being natural Number

for D, D9, E being non empty set

for d9 being Element of D9

for F being Function of [:D,D9:],E

for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E

for D, D9, E being non empty set

for d9 being Element of D9

for F being Function of [:D,D9:],E

for z being Tuple of i,D holds F [:] (z,d9) is Element of i -tuples_on E

proof end;

:: Addendum, 2002.07.08

theorem :: FINSEQ_2:125

for f being Function

for x, y being set st x in dom f & y in dom f holds

f * <*x,y*> = <*(f . x),(f . y)*>

for x, y being set st x in dom f & y in dom f holds

f * <*x,y*> = <*(f . x),(f . y)*>

proof end;

theorem :: FINSEQ_2:126

for f being Function

for x, y, z being set st x in dom f & y in dom f & z in dom f holds

f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>

for x, y, z being set st x in dom f & y in dom f & z in dom f holds

f * <*x,y,z*> = <*(f . x),(f . y),(f . z)*>

proof end;

:: from SCMFSA_7, 2005.11.21, A.T.

theorem :: FINSEQ_2:130

for D being non empty set

for s being FinSequence of D st s <> {} holds

ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w

for s being FinSequence of D st s <> {} holds

ex w being FinSequence of D ex n being Element of D st s = <*n*> ^ w

proof end;

:: Moved from AMISTD_2 by AK, 2008.02.02

registration
end;

:: from FINSOP_1, 2009.05.23, AT

definition

let D be non empty set ;

let n be natural Number ;

let d be Element of D;

:: original: |->

redefine func n |-> d -> Element of n -tuples_on D;

coherence

n |-> d is Element of n -tuples_on D by Th110;

end;
let n be natural Number ;

let d be Element of D;

:: original: |->

redefine func n |-> d -> Element of n -tuples_on D;

coherence

n |-> d is Element of n -tuples_on D by Th110;

:: new, 2009.08.15, A.T.

theorem :: FINSEQ_2:131

for i being natural Number

for D being non empty set

for z being set holds

( z is Tuple of i,D iff z in i -tuples_on D )

for D being non empty set

for z being set holds

( z is Tuple of i,D iff z in i -tuples_on D )

proof end;

:: from CATALG_1, 2009.09.08, A.T.

theorem Th130: :: FINSEQ_2:132

for A being set

for i being Element of NAT

for p being FinSequence holds

( p in i -tuples_on A iff ( len p = i & rng p c= A ) )

for i being Element of NAT

for p being FinSequence holds

( p in i -tuples_on A iff ( len p = i & rng p c= A ) )

proof end;

theorem :: FINSEQ_2:133

for A being set

for i being Element of NAT

for p being FinSequence of A holds

( p in i -tuples_on A iff len p = i )

for i being Element of NAT

for p being FinSequence of A holds

( p in i -tuples_on A iff len p = i )

proof end;

theorem Th133: :: FINSEQ_2:135

for A being set

for x being object holds

( x in 1 -tuples_on A iff ex a being set st

( a in A & x = <*a*> ) )

for x being object holds

( x in 1 -tuples_on A iff ex a being set st

( a in A & x = <*a*> ) )

proof end;

theorem Th135: :: FINSEQ_2:137

for A being set

for x being object holds

( x in 2 -tuples_on A iff ex a, b being object st

( a in A & b in A & x = <*a,b*> ) )

for x being object holds

( x in 2 -tuples_on A iff ex a, b being object st

( a in A & b in A & x = <*a,b*> ) )

proof end;

theorem Th137: :: FINSEQ_2:139

for A being set

for x being object holds

( x in 3 -tuples_on A iff ex a, b, c being object st

( a in A & b in A & c in A & x = <*a,b,c*> ) )

for x being object holds

( x in 3 -tuples_on A iff ex a, b, c being object st

( a in A & b in A & c in A & x = <*a,b,c*> ) )

proof end;

theorem :: FINSEQ_2:140

for A being set

for a, b, c being object st <*a,b,c*> in 3 -tuples_on A holds

( a in A & b in A & c in A )

for a, b, c being object st <*a,b,c*> in 3 -tuples_on A holds

( a in A & b in A & c in A )

proof end;

theorem :: FINSEQ_2:141

for i being natural Number

for A being set

for x being object st x in i -tuples_on A holds

x is b_{1} -element FinSequence by Lm7;

for A being set

for x being object st x in i -tuples_on A holds

x is b

:: from MSUALG_1, 2009.09.18, A.T.

:: from AMISTD_3, 2010.01.10, A.T.

definition

let I be set ;

let M be ManySortedSet of I;

ex b_{1} being ManySortedSet of I * st

for i being Element of I * holds b_{1} . i = product (M * i)

for b_{1}, b_{2} being ManySortedSet of I * st ( for i being Element of I * holds b_{1} . i = product (M * i) ) & ( for i being Element of I * holds b_{2} . i = product (M * i) ) holds

b_{1} = b_{2}

end;
let M be ManySortedSet of I;

func M # -> ManySortedSet of I * means :Def5: :: FINSEQ_2:def 5

for i being Element of I * holds it . i = product (M * i);

existence for i being Element of I * holds it . i = product (M * i);

ex b

for i being Element of I * holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines # FINSEQ_2:def 5 :

for I being set

for M being ManySortedSet of I

for b_{3} being ManySortedSet of I * holds

( b_{3} = M # iff for i being Element of I * holds b_{3} . i = product (M * i) );

for I being set

for M being ManySortedSet of I

for b

( b

registration
end;

definition

let a be set ;

ex b_{1} being sequence of ({a} *) st

for n being Nat holds b_{1} . n = n |-> a

for b_{1}, b_{2} being sequence of ({a} *) st ( for n being Nat holds b_{1} . n = n |-> a ) & ( for n being Nat holds b_{2} . n = n |-> a ) holds

b_{1} = b_{2}

end;
func *--> a -> sequence of ({a} *) means :Def6: :: FINSEQ_2:def 6

for n being Nat holds it . n = n |-> a;

existence for n being Nat holds it . n = n |-> a;

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def6 defines *--> FINSEQ_2:def 6 :

for a being set

for b_{2} being sequence of ({a} *) holds

( b_{2} = *--> a iff for n being Nat holds b_{2} . n = n |-> a );

for a being set

for b

( b

theorem :: FINSEQ_2:145

for D being non empty set

for n being Nat

for a being set

for M being ManySortedSet of {a} st M = a .--> D holds

((M #) * (*--> a)) . n = Funcs ((Seg n),D)

for n being Nat

for a being set

for M being ManySortedSet of {a} st M = a .--> D holds

((M #) * (*--> a)) . n = Funcs ((Seg n),D)

proof end;

registration
end;

:: new, 2011.10.03, A.K.

registration

let D be set ;

coherence

for b_{1} being FinSequenceSet of D holds b_{1} is FinSequence-membered

end;
coherence

for b

proof end;

definition

let D be set ;

let F be FinSequenceSet of D;

let f be sequence of F;

let n be natural Number ;

:: original: .

redefine func f . n -> FinSequence of D;

coherence

f . n is FinSequence of D

end;
let F be FinSequenceSet of D;

let f be sequence of F;

let n be natural Number ;

:: original: .

redefine func f . n -> FinSequence of D;

coherence

f . n is FinSequence of D

proof end;

::$CT