theorem :: FVSUM_1:87

for i being Nat
for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K
for R1 being Element of i -tuples_on the carrier of K holds Product (a * R1) = (Product (i |-> a)) * (Product R1)