:: Binary Operations Applied to Finite Sequences
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990 Association of Mizar Users
theorem Th1: :: FINSEQOP:1
theorem :: FINSEQOP:2
theorem :: FINSEQOP:3
canceled;
theorem Th4: :: FINSEQOP:4
theorem :: FINSEQOP:5
theorem :: FINSEQOP:6
theorem Th7: :: FINSEQOP:7
theorem Th8: :: FINSEQOP:8
theorem Th9: :: FINSEQOP:9
theorem :: FINSEQOP:10
Lm1:
for C, D being non empty set
for f being Function of C,D
for T being Element of 0 -tuples_on C holds f * T = <*> D
Lm2:
for D', D, E being non empty set
for i being Nat
for F being Function of [:D,D':],E
for T' being Element of i -tuples_on D'
for T being Element of 0 -tuples_on D holds F .: T,T' = <*> E
Lm3:
for D, D', E being non empty set
for d being Element of D
for F being Function of [:D,D':],E
for T' being Element of 0 -tuples_on D' holds F [;] d,T' = <*> E
Lm4:
for D', D, E being non empty set
for d' being Element of D'
for F being Function of [:D,D':],E
for T being Element of 0 -tuples_on D holds F [:] T,d' = <*> E
theorem Th11: :: FINSEQOP:11
theorem :: FINSEQOP:12
theorem Th13: :: FINSEQOP:13
theorem :: FINSEQOP:14
theorem Th15: :: FINSEQOP:15
theorem :: FINSEQOP:16
theorem :: FINSEQOP:17
theorem Th18: :: FINSEQOP:18
theorem :: FINSEQOP:19
theorem :: FINSEQOP:20
theorem :: FINSEQOP:21
theorem :: FINSEQOP:22
theorem :: FINSEQOP:23
theorem :: FINSEQOP:24
Lm5:
for D being non empty set
for i being Nat
for T being Element of i -tuples_on D holds T is Function of Seg i,D
theorem Th25: :: FINSEQOP:25
theorem Th26: :: FINSEQOP:26
theorem :: FINSEQOP:27
theorem :: FINSEQOP:28
theorem :: FINSEQOP:29
theorem :: FINSEQOP:30
theorem :: FINSEQOP:31
theorem :: FINSEQOP:32
theorem :: FINSEQOP:33
theorem :: FINSEQOP:34
theorem :: FINSEQOP:35
theorem Th36: :: FINSEQOP:36
theorem Th37: :: FINSEQOP:37
theorem Th38: :: FINSEQOP:38
for
C,
E,
D being non
empty set for
f,
f' being
Function of
C,
D for
h being
Function of
D,
E for
F being
BinOp of
D for
H being
BinOp of
E st ( for
d1,
d2 being
Element of
D holds
h . (F . d1,d2) = H . (h . d1),
(h . d2) ) holds
h * (F .: f,f') = H .: (h * f),
(h * f')
theorem Th39: :: FINSEQOP:39
theorem Th40: :: FINSEQOP:40
theorem :: FINSEQOP:41
theorem :: FINSEQOP:42
theorem :: FINSEQOP:43
theorem Th44: :: FINSEQOP:44
theorem Th45: :: FINSEQOP:45
theorem Th46: :: FINSEQOP:46
theorem :: FINSEQOP:47
theorem :: FINSEQOP:48
theorem Th49: :: FINSEQOP:49
theorem Th50: :: FINSEQOP:50
theorem Th51: :: FINSEQOP:51
theorem :: FINSEQOP:52
theorem :: FINSEQOP:53
theorem :: FINSEQOP:54
theorem :: FINSEQOP:55
theorem :: FINSEQOP:56
theorem :: FINSEQOP:57
theorem :: FINSEQOP:58
theorem :: FINSEQOP:59
:: deftheorem Def1 defines is_an_inverseOp_wrt FINSEQOP:def 1 :
:: deftheorem Def2 defines having_an_inverseOp FINSEQOP:def 2 :
:: deftheorem Def3 defines the_inverseOp_wrt FINSEQOP:def 3 :
theorem :: FINSEQOP:60
canceled;
theorem :: FINSEQOP:61
canceled;
theorem :: FINSEQOP:62
canceled;
theorem Th63: :: FINSEQOP:63
theorem Th64: :: FINSEQOP:64
theorem Th65: :: FINSEQOP:65
theorem Th66: :: FINSEQOP:66
theorem Th67: :: FINSEQOP:67
theorem Th68: :: FINSEQOP:68
theorem Th69: :: FINSEQOP:69
theorem Th70: :: FINSEQOP:70
theorem Th71: :: FINSEQOP:71
theorem :: FINSEQOP:72
theorem :: FINSEQOP:73
theorem :: FINSEQOP:74
theorem Th75: :: FINSEQOP:75
theorem Th76: :: FINSEQOP:76
theorem :: FINSEQOP:77
theorem :: FINSEQOP:78
theorem Th79: :: FINSEQOP:79
theorem :: FINSEQOP:80
:: deftheorem defines * FINSEQOP:def 4 :
theorem :: FINSEQOP:81
canceled;
theorem Th82: :: FINSEQOP:82
theorem :: FINSEQOP:83
theorem Th84: :: FINSEQOP:84
for
D,
D',
E,
C,
C' being non
empty set for
F being
Function of
[:D,D':],
E for
f being
Function of
C,
D for
g being
Function of
C',
D' holds
F * f,
g is
Function of
[:C,C':],
E
theorem :: FINSEQOP:85
theorem Th86: :: FINSEQOP:86
for
D,
D',
E,
C,
C' being non
empty set for
c being
Element of
C for
c' being
Element of
C' for
F being
Function of
[:D,D':],
E for
f being
Function of
C,
D for
g being
Function of
C',
D' holds
(F * f,g) . c,
c' = F . (f . c),
(g . c')
theorem Th87: :: FINSEQOP:87
theorem Th88: :: FINSEQOP:88
theorem :: FINSEQOP:89
theorem :: FINSEQOP:90
theorem :: FINSEQOP:91
theorem :: FINSEQOP:92
theorem :: FINSEQOP:93
theorem :: FINSEQOP:94
for
D being non
empty set for
F,
G being
BinOp of
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
F is
having_an_inverseOp &
G = F * (id D),
(the_inverseOp_wrt F) holds
for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (G . d1,d2),
(G . d3,d4) = G . (F . d1,d3),
(F . d2,d4)