theorem Th86: :: FVSUM_1:86

for i being Nat
for K being non empty associative commutative well-unital doubleLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Product (mlt (R1,R2)) = (Product R1) * (Product R2) by SETWOP_2:35;