begin
:: deftheorem Def1 defines "**" FINSOP_1:def 1 :
theorem
canceled;
theorem
theorem
Lm1:
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F >= 1 & g is associative & g is commutative holds
g "**" F = g $$ (findom F),((NAT --> (the_unity_wrt g)) +* F)
Lm2:
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & g is associative & g is commutative holds
g "**" F = g $$ (findom F),((NAT --> (the_unity_wrt g)) +* F)
theorem
Lm3:
for D being non empty set
for g being BinOp of D st g is having_a_unity holds
g "**" (<*> D) = the_unity_wrt g
Lm4:
for D being non empty set
for d being Element of D
for g being BinOp of D holds g "**" <*d*> = d
Lm5:
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st len F >= 1 holds
g "**" (F ^ <*d*>) = g . (g "**" F),d
Lm6:
for D being non empty set
for d being Element of D
for F being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 holds
g "**" (F ^ <*d*>) = g . (g "**" F),d
theorem Th5:
theorem Th6:
theorem Th7:
Lm7:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative holds
for f being Permutation of dom F st len F >= 1 & len F = len G & ( for i being Element of NAT st i in dom G holds
G . i = F . (f . i) ) holds
g "**" F = g "**" G
Lm8:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D
for P being Permutation of dom F st g is having_a_unity & len F = 0 & G = F * P holds
g "**" F = g "**" G
theorem Th8:
Lm9:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & F is one-to-one & G is one-to-one & rng F = rng G & len F >= 1 holds
g "**" F = g "**" G
Lm10:
for D being non empty set
for F, G being FinSequence of D
for g being BinOp of D st len F = 0 & g is having_a_unity & F is one-to-one & G is one-to-one & rng F = rng G holds
g "**" F = g "**" G
theorem
Lm11:
for D being non empty set
for F being FinSequence of D
for g being BinOp of D st len F = 1 holds
g "**" F = F . 1
Lm12:
for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is associative & g is commutative & len F >= 1 & len F = len G & len F = len H & ( for k being Element of NAT st k in dom F holds
H . k = g . (F . k),(G . k) ) holds
g "**" H = g . (g "**" F),(g "**" G)
Lm13:
for D being non empty set
for F, G, H being FinSequence of D
for g being BinOp of D st g is having_a_unity & len F = 0 & len F = len G & len F = len H holds
g "**" F = g . (g "**" G),(g "**" H)
theorem
theorem
theorem
theorem Th13:
theorem
theorem Th15:
theorem
theorem Th17:
theorem
theorem Th19:
theorem
theorem
theorem