begin
theorem Th1:
theorem
theorem
canceled;
theorem Th4:
theorem
theorem
theorem Th7:
theorem Th8:
theorem Th9:
theorem
Lm1:
for D9, D, E being non empty set
for i being Nat
for F being Function of [:D,D9:],E
for T9 being Tuple of i,D9
for T being Tuple of 0 ,D holds F .: T,T9 = <*> E
Lm2:
for D, D9, E being non empty set
for d being Element of D
for F being Function of [:D,D9:],E
for T9 being Tuple of 0 ,D9 holds F [;] d,T9 = <*> E
Lm3:
for D9, D, E being non empty set
for d9 being Element of D9
for F being Function of [:D,D9:],E
for T being Tuple of 0 ,D holds F [:] T,d9 = <*> E
theorem Th11:
theorem
for
E,
D,
D9 being non
empty set for
i,
j being
Nat for
F being
Function of
[:D,D9:],
E for
T being
Tuple of
i,
D for
T9 being
Tuple of
i,
D9 for
S being
Tuple of
j,
D for
S9 being
Tuple of
j,
D9 holds
F .: (T ^ S),
(T9 ^ S9) = (F .: T,T9) ^ (F .: S,S9)
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,D 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,
f9 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,f9) = H .: (h * f),
(h * f9)
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,
D 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 :
for D being non empty set
for u being UnOp of D
for F being BinOp of D holds
( u is_an_inverseOp_wrt F iff for d being Element of D holds
( F . d,(u . d) = the_unity_wrt F & F . (u . d),d = the_unity_wrt F ) );
:: deftheorem Def2 defines having_an_inverseOp FINSEQOP:def 2 :
for D being non empty set
for F being BinOp of D holds
( F is having_an_inverseOp iff ex u being UnOp of D st u is_an_inverseOp_wrt F );
:: deftheorem Def3 defines the_inverseOp_wrt FINSEQOP:def 3 :
for D being non empty set
for F being BinOp of D st F is having_a_unity & F is associative & F is having_an_inverseOp holds
for b3 being UnOp of D holds
( b3 = the_inverseOp_wrt F iff b3 is_an_inverseOp_wrt F );
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 :
for F, f, g being Function holds F * f,g = F * [:f,g:];
theorem
canceled;
theorem Th82:
theorem
theorem Th84:
for
D,
D9,
E,
C,
C9 being non
empty set for
F being
Function of
[:D,D9:],
E for
f being
Function of
C,
D for
g being
Function of
C9,
D9 holds
F * f,
g is
Function of
[:C,C9:],
E
theorem
theorem Th86:
for
D,
D9,
E,
C,
C9 being non
empty set for
c being
Element of
C for
c9 being
Element of
C9 for
F being
Function of
[:D,D9:],
E for
f being
Function of
C,
D for
g being
Function of
C9,
D9 holds
(F * f,g) . c,
c9 = F . (f . c),
(g . c9)
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)