theorem :: FVSUM_1:56

for i being Nat
for K being non empty distributive doubleLoopStr
for a being Element of K
for R1, R2 being Element of i -tuples_on the carrier of K holds a * (R1 + R2) = (a * R1) + (a * R2) by Th12, FINSEQOP:51;