begin
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
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))
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 Th37:
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 Th48:
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 Th79:
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 Th81:
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 Th82:
for
D being non
empty set for
d1,
d2 being
Element of
D for
F being
BinOp of
D for
u being
Function of
D,
D holds
(
(F * ((id D),u)) . (
d1,
d2)
= F . (
d1,
(u . d2)) &
(F * (u,(id D))) . (
d1,
d2)
= F . (
(u . d1),
d2) )
theorem
for
D being non
empty set for
i being
Nat for
T1,
T2 being
Tuple of
i,
D for
F being
BinOp of
D for
u being
UnOp of
D holds
(F * ((id D),u)) .: (
T1,
T2)
= F .: (
T1,
(u * T2))
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)))