begin
Lm1:
for K being non empty multMagma
for a, b being Element of K holds ( the multF of K [;] (b,(id the carrier of K))) . a = b * a
begin
Lm2:
for i being Element of NAT
for K being non empty left_zeroed right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (i |-> (0. K)) = R
Lm3:
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds R + (- R) = i |-> (0. K)
Lm4:
for i being Element of NAT
for K being non empty right_complementable left_zeroed add-associative right_zeroed addLoopStr
for R1, R, R2 being Element of i -tuples_on the carrier of K st R1 + R = R2 + R holds
R1 = R2
Lm5:
for K being non empty multMagma
for a1, a2, b1, b2 being Element of K holds mlt (<*a1,a2*>,<*b1,b2*>) = <*(a1 * b1),(a2 * b2)*>
begin
begin
Lm6:
for K being non empty commutative well-unital multLoopStr holds Product (<*> the carrier of K) = 1. K
begin
:: Some Operations on the i-tuples on Element of K
::