:: Some Properties of Restrictions of Finite Sequences
:: by Czes\law Byli\'nski
::
:: Received January 25, 1995
:: Copyright (c) 1995 Association of Mizar Users
theorem Th1: :: FINSEQ_5:1
theorem Th2: :: FINSEQ_5:2
theorem Th3: :: FINSEQ_5:3
theorem :: FINSEQ_5:4
theorem :: FINSEQ_5:5
theorem Th6: :: FINSEQ_5:6
theorem :: FINSEQ_5:7
theorem Th8: :: FINSEQ_5:8
theorem :: FINSEQ_5:9
canceled;
theorem :: FINSEQ_5:10
theorem Th11: :: FINSEQ_5:11
theorem Th12: :: FINSEQ_5:12
theorem :: FINSEQ_5:13
theorem Th14: :: FINSEQ_5:14
theorem Th15: :: FINSEQ_5:15
theorem Th16: :: FINSEQ_5:16
Lm1:
for i being Nat
for D being non empty set
for f, g being FinSequence of D st i in dom f holds
(f ^ g) /. i = f /. i
theorem :: FINSEQ_5:17
canceled;
theorem Th18: :: FINSEQ_5:18
theorem Th19: :: FINSEQ_5:19
theorem Th20: :: FINSEQ_5:20
theorem Th21: :: FINSEQ_5:21
theorem :: FINSEQ_5:22
canceled;
theorem Th23: :: FINSEQ_5:23
theorem :: FINSEQ_5:24
Lm2:
for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f | i is one-to-one
theorem Th25: :: FINSEQ_5:25
theorem :: FINSEQ_5:26
theorem :: FINSEQ_5:27
theorem :: FINSEQ_5:28
theorem Th29: :: FINSEQ_5:29
theorem Th30: :: FINSEQ_5:30
theorem Th31: :: FINSEQ_5:31
theorem :: FINSEQ_5:32
theorem :: FINSEQ_5:33
theorem Th34: :: FINSEQ_5:34
theorem Th35: :: FINSEQ_5:35
theorem Th36: :: FINSEQ_5:36
Lm3:
for i being Nat
for D being non empty set
for f being FinSequence of D st f is one-to-one holds
f /^ i is one-to-one
theorem Th37: :: FINSEQ_5:37
theorem :: FINSEQ_5:38
theorem Th39: :: FINSEQ_5:39
theorem :: FINSEQ_5:40
theorem Th41: :: FINSEQ_5:41
theorem Th42: :: FINSEQ_5:42
theorem :: FINSEQ_5:43
theorem :: FINSEQ_5:44
:: deftheorem defines -: FINSEQ_5:def 1 :
theorem Th45: :: FINSEQ_5:45
theorem Th46: :: FINSEQ_5:46
theorem :: FINSEQ_5:47
theorem :: FINSEQ_5:48
theorem :: FINSEQ_5:49
theorem :: FINSEQ_5:50
theorem :: FINSEQ_5:51
:: deftheorem defines :- FINSEQ_5:def 2 :
theorem Th52: :: FINSEQ_5:52
theorem Th53: :: FINSEQ_5:53
theorem Th54: :: FINSEQ_5:54
theorem Th55: :: FINSEQ_5:55
theorem :: FINSEQ_5:56
theorem :: FINSEQ_5:57
theorem :: FINSEQ_5:58
theorem :: FINSEQ_5:59
:: deftheorem Def3 defines Rev FINSEQ_5:def 3 :
theorem Th60: :: FINSEQ_5:60
theorem Th61: :: FINSEQ_5:61
theorem Th62: :: FINSEQ_5:62
theorem :: FINSEQ_5:63
theorem :: FINSEQ_5:64
theorem Th65: :: FINSEQ_5:65
theorem Th66: :: FINSEQ_5:66
theorem :: FINSEQ_5:67
theorem :: FINSEQ_5:68
theorem :: FINSEQ_5:69
:: deftheorem defines Ins FINSEQ_5:def 4 :
theorem :: FINSEQ_5:70
theorem Th71: :: FINSEQ_5:71
theorem :: FINSEQ_5:72
theorem Th73: :: FINSEQ_5:73
theorem :: FINSEQ_5:74
theorem Th75: :: FINSEQ_5:75
theorem :: FINSEQ_5:76
theorem :: FINSEQ_5:77
theorem :: FINSEQ_5:78
theorem :: FINSEQ_5:79
theorem :: FINSEQ_5:80
theorem :: FINSEQ_5:81
theorem :: FINSEQ_5:82
theorem :: FINSEQ_5:83
theorem :: FINSEQ_5:84
theorem Th85: :: FINSEQ_5:85
theorem Th86: :: FINSEQ_5:86
theorem :: FINSEQ_5:87