:: Finite Sequences and Tuples of Elements of a Non-empty Sets
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem :: FINSEQ_2:1
theorem Th2: :: FINSEQ_2:2
theorem Th3: :: FINSEQ_2:3
theorem Th4: :: FINSEQ_2:4
theorem :: FINSEQ_2:5
theorem :: FINSEQ_2:6
theorem :: FINSEQ_2:7
canceled;
theorem :: FINSEQ_2:8
theorem :: FINSEQ_2:9
theorem :: FINSEQ_2:10
theorem Th11: :: FINSEQ_2:11
theorem :: FINSEQ_2:12
canceled;
theorem Th13: :: FINSEQ_2:13
theorem Th14: :: FINSEQ_2:14
Lm2:
for x1, x2 being set holds rng <*x1,x2*> = {x1,x2}
theorem Th15: :: FINSEQ_2:15
Lm3:
for x1, x2, x3 being set holds rng <*x1,x2,x3*> = {x1,x2,x3}
theorem Th16: :: FINSEQ_2:16
theorem :: FINSEQ_2:17
canceled;
theorem Th18: :: FINSEQ_2:18
theorem Th19: :: FINSEQ_2:19
theorem :: FINSEQ_2:20
theorem :: FINSEQ_2:21
theorem Th22: :: FINSEQ_2:22
theorem Th23: :: FINSEQ_2:23
theorem :: FINSEQ_2:24
theorem Th25: :: FINSEQ_2:25
theorem Th26: :: FINSEQ_2:26
theorem Th27: :: FINSEQ_2:27
theorem Th28: :: FINSEQ_2:28
theorem :: FINSEQ_2:29
canceled;
theorem :: FINSEQ_2:30
theorem :: FINSEQ_2:31
theorem :: FINSEQ_2:32
theorem Th33: :: FINSEQ_2:33
theorem Th34: :: FINSEQ_2:34
theorem :: FINSEQ_2:35
theorem Th36: :: FINSEQ_2:36
theorem Th37: :: FINSEQ_2:37
theorem :: FINSEQ_2:38
theorem :: FINSEQ_2:39
theorem Th40: :: FINSEQ_2:40
theorem Th41: :: FINSEQ_2:41
theorem Th42: :: FINSEQ_2:42
theorem :: FINSEQ_2:43
theorem :: FINSEQ_2:44
theorem Th45: :: FINSEQ_2:45
theorem Th46: :: FINSEQ_2:46
theorem Th47: :: FINSEQ_2:47
theorem :: FINSEQ_2:48
theorem Th49: :: FINSEQ_2:49
theorem :: FINSEQ_2:50
theorem Th51: :: FINSEQ_2:51
theorem Th52: :: FINSEQ_2:52
:: deftheorem defines idseq FINSEQ_2:def 1 :
theorem :: FINSEQ_2:53
canceled;
theorem :: FINSEQ_2:54
canceled;
theorem Th55: :: FINSEQ_2:55
theorem :: FINSEQ_2:56
canceled;
theorem :: FINSEQ_2:57
theorem :: FINSEQ_2:58
theorem Th59: :: FINSEQ_2:59
theorem Th60: :: FINSEQ_2:60
theorem Th61: :: FINSEQ_2:61
theorem :: FINSEQ_2:62
theorem :: FINSEQ_2:63
canceled;
theorem Th64: :: FINSEQ_2:64
theorem :: FINSEQ_2:65
theorem Th66: :: FINSEQ_2:66
:: deftheorem defines |-> FINSEQ_2:def 2 :
theorem :: FINSEQ_2:67
canceled;
theorem :: FINSEQ_2:68
canceled;
theorem Th69: :: FINSEQ_2:69
theorem :: FINSEQ_2:70
canceled;
theorem :: FINSEQ_2:71
theorem :: FINSEQ_2:72
theorem Th73: :: FINSEQ_2:73
theorem Th74: :: FINSEQ_2:74
theorem Th75: :: FINSEQ_2:75
theorem :: FINSEQ_2:76
theorem Th77: :: FINSEQ_2:77
Lm4:
for i being Nat
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
theorem Th78: :: FINSEQ_2:78
theorem Th79: :: FINSEQ_2:79
Lm5:
for a being set
for p being FinSequence
for F being Function st [:{a},(rng p):] c= dom F holds
dom (F [;] a,p) = dom p
theorem Th80: :: FINSEQ_2:80
theorem Th81: :: FINSEQ_2:81
Lm6:
for a being set
for p being FinSequence
for F being Function st [:(rng p),{a}:] c= dom F holds
dom (F [:] p,a) = dom p
theorem Th82: :: FINSEQ_2:82
theorem Th83: :: FINSEQ_2:83
theorem Th84: :: FINSEQ_2:84
theorem Th85: :: FINSEQ_2:85
theorem Th86: :: FINSEQ_2:86
theorem :: FINSEQ_2:87
theorem :: FINSEQ_2:88
theorem :: FINSEQ_2:89
for
D,
D',
E being non
empty set for
d1,
d2 being
Element of
D for
d1',
d2' being
Element of
D' for
F being
Function of
[:D,D':],
E for
p being
FinSequence of
D for
q being
FinSequence of
D' st
p = <*d1,d2*> &
q = <*d1',d2'*> holds
F .: p,
q = <*(F . d1,d1'),(F . d2,d2')*>
theorem :: FINSEQ_2:90
for
D,
D',
E being non
empty set for
d1,
d2,
d3 being
Element of
D for
d1',
d2',
d3' being
Element of
D' for
F being
Function of
[:D,D':],
E for
p being
FinSequence of
D for
q being
FinSequence of
D' st
p = <*d1,d2,d3*> &
q = <*d1',d2',d3'*> holds
F .: p,
q = <*(F . d1,d1'),(F . d2,d2'),(F . d3,d3')*>
theorem Th91: :: FINSEQ_2:91
theorem Th92: :: FINSEQ_2:92
theorem :: FINSEQ_2:93
theorem :: FINSEQ_2:94
theorem :: FINSEQ_2:95
for
D,
D',
E being non
empty set for
d being
Element of
D for
d1',
d2' being
Element of
D' for
F being
Function of
[:D,D':],
E for
p being
FinSequence of
D' st
p = <*d1',d2'*> holds
F [;] d,
p = <*(F . d,d1'),(F . d,d2')*>
theorem :: FINSEQ_2:96
for
D,
D',
E being non
empty set for
d being
Element of
D for
d1',
d2',
d3' being
Element of
D' for
F being
Function of
[:D,D':],
E for
p being
FinSequence of
D' st
p = <*d1',d2',d3'*> holds
F [;] d,
p = <*(F . d,d1'),(F . d,d2'),(F . d,d3')*>
theorem Th97: :: FINSEQ_2:97
theorem Th98: :: FINSEQ_2:98
theorem :: FINSEQ_2:99
theorem :: FINSEQ_2:100
theorem :: FINSEQ_2:101
for
D,
D',
E being non
empty set for
d1,
d2 being
Element of
D for
d' being
Element of
D' for
F being
Function of
[:D,D':],
E for
p being
FinSequence of
D st
p = <*d1,d2*> holds
F [:] p,
d' = <*(F . d1,d'),(F . d2,d')*>
theorem :: FINSEQ_2:102
for
D,
D',
E being non
empty set for
d1,
d2,
d3 being
Element of
D for
d' being
Element of
D' for
F being
Function of
[:D,D':],
E for
p being
FinSequence of
D st
p = <*d1,d2,d3*> holds
F [:] p,
d' = <*(F . d1,d'),(F . d2,d'),(F . d3,d')*>
:: deftheorem Def3 defines FinSequenceSet FINSEQ_2:def 3 :
theorem :: FINSEQ_2:103
canceled;
theorem Th104: :: FINSEQ_2:104
theorem :: FINSEQ_2:105
theorem :: FINSEQ_2:106
canceled;
theorem :: FINSEQ_2:107
:: deftheorem defines -tuples_on FINSEQ_2:def 4 :
theorem :: FINSEQ_2:108
canceled;
theorem Th109: :: FINSEQ_2:109
theorem Th110: :: FINSEQ_2:110
theorem :: FINSEQ_2:111
theorem Th112: :: FINSEQ_2:112
theorem Th113: :: FINSEQ_2:113
theorem :: FINSEQ_2:114
theorem :: FINSEQ_2:115
theorem Th116: :: FINSEQ_2:116
theorem Th117: :: FINSEQ_2:117
theorem :: FINSEQ_2:118
theorem Th119: :: FINSEQ_2:119
theorem :: FINSEQ_2:120
theorem :: FINSEQ_2:121
theorem Th122: :: FINSEQ_2:122
theorem :: FINSEQ_2:123
theorem :: FINSEQ_2:124
theorem Th125: :: FINSEQ_2:125
theorem Th126: :: FINSEQ_2:126
theorem :: FINSEQ_2:127
theorem :: FINSEQ_2:128
theorem :: FINSEQ_2:129
theorem :: FINSEQ_2:130
theorem :: FINSEQ_2:131
theorem :: FINSEQ_2:132
theorem :: FINSEQ_2:133
theorem Th134: :: FINSEQ_2:134
theorem :: FINSEQ_2:135
theorem :: FINSEQ_2:136
theorem :: FINSEQ_2:137
theorem :: FINSEQ_2:138
theorem :: FINSEQ_2:139
theorem :: FINSEQ_2:140
theorem :: FINSEQ_2:141
theorem :: FINSEQ_2:142
theorem :: FINSEQ_2:143
theorem :: FINSEQ_2:144
theorem :: FINSEQ_2:145
theorem :: FINSEQ_2:146
theorem :: FINSEQ_2:147
theorem :: FINSEQ_2:148
theorem :: FINSEQ_2:149
theorem :: FINSEQ_2:150