begin
Lm1:
for i being Nat holds Seg i is Element of Fin NAT
by FINSUB_1:def 5;
theorem Th9:
for
C,
D being non
empty set for
B being
Element of
Fin C for
e being
Element of
D for
F,
G being
BinOp of
D for
f,
f9 being
Function of
C,
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) holds
G . (
(F $$ (B,f)),
(F $$ (B,f9)))
= F $$ (
B,
(G .: (f,f9)))
Lm3:
for D being non empty set
for F being BinOp of D st F is commutative & F is associative holds
for d1, d2, d3, d4 being Element of D holds F . ((F . (d1,d2)),(F . (d3,d4))) = F . ((F . (d1,d3)),(F . (d2,d4)))
theorem
for
C,
D being non
empty set for
B being
Element of
Fin C for
F,
G being
BinOp of
D for
f,
f9 being
Function of
C,
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
G . (
(F $$ (B,f)),
(F $$ (B,f9)))
= F $$ (
B,
(G .: (f,f9)))
Lm4:
for D being non empty set
for e being Element of D
for F being BinOp of D
for p, q being FinSequence of D st len p = len q & F . (e,e) = e holds
F .: (([#] (p,e)),([#] (q,e))) = [#] ((F .: (p,q)),e)
Lm5:
for D being non empty set
for e, d being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (e,d) = e holds
F [:] (([#] (p,e)),d) = [#] ((F [:] (p,d)),e)
Lm6:
for D being non empty set
for d, e being Element of D
for F being BinOp of D
for p being FinSequence of D st F . (d,e) = e holds
F [;] (d,([#] (p,e))) = [#] ((F [;] (d,p)),e)
theorem Th32:
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
p,
q being
FinSequence of
D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) &
len p = len q holds
G . (
(F "**" p),
(F "**" q))
= F "**" (G .: (p,q))
theorem Th33:
for
D being non
empty set for
e being
Element of
D for
F,
G being
BinOp of
D for
i being
Nat for
T1,
T2 being
Element of
i -tuples_on D st
F is
commutative &
F is
associative &
F is
having_a_unity &
e = the_unity_wrt F &
G . (
e,
e)
= e & ( for
d1,
d2,
d3,
d4 being
Element of
D holds
F . (
(G . (d1,d2)),
(G . (d3,d4)))
= G . (
(F . (d1,d3)),
(F . (d2,d4))) ) holds
G . (
(F "**" T1),
(F "**" T2))
= F "**" (G .: (T1,T2))