theorem :: FVSUM_1:83

for i, j being Nat
for K being non empty associative commutative well-unital doubleLoopStr
for a being Element of K holds Product ((i + j) |-> a) = (Product (i |-> a)) * (Product (j |-> a)) by SETWOP_2:26;