begin
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))
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)
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
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
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))