begin
theorem Th1:
theorem
theorem
canceled;
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
Lm1:
for D', D, E being non empty set
for i being Nat
for F being Function of [:D,D':],E
for T' being Tuple of i,
for T being Tuple of 0 , holds F .: T,T' = <*> E
Lm2:
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 Tuple of 0 , holds F [;] d,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 Tuple of 0 , holds F [:] T,d' = <*> E
theorem Th11:
theorem
for
E,
D,
D' being non
empty set for
i,
j being
Nat for
F being
Function of
[:D,D':],
E for
T being
Tuple of
i,
for
T' being
Tuple of
i,
for
S being
Tuple of
j,
for
S' being
Tuple of
j, holds
F .: (T ^ S),
(T' ^ S') = (F .: T,T') ^ (F .: S,S')
theorem Th13:
theorem
theorem Th15:
theorem
theorem
theorem Th18:
theorem
theorem
theorem
theorem
theorem
theorem
Lm4:
for D being non empty set
for i being Nat
for T being Tuple of i, holds T is Function of Seg i,D
theorem Th25:
theorem Th26:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th36:
theorem Th37:
theorem Th38:
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:
theorem Th40:
theorem
theorem
theorem
theorem Th44:
theorem Th45:
theorem Th46:
theorem
theorem
theorem Th49:
for
E,
D being non
empty set for
i being
Nat for
h being
Function of
D,
E for
T1,
T2 being
Tuple of
i,
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 .: T1,T2) = H .: (h * T1),
(h * T2)
theorem Th50:
theorem Th51:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem Th69:
theorem Th70:
theorem Th71:
theorem
theorem
theorem
theorem Th75:
theorem Th76:
theorem
theorem
theorem Th79:
theorem
:: deftheorem defines * FINSEQOP:def 4 :
theorem
canceled;
theorem Th82:
theorem
theorem Th84:
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
theorem Th86:
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:
theorem Th88:
theorem
theorem
theorem
theorem
theorem
theorem
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)