theorem :: FVSUM_1:76

for i being Nat
for K being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for R1, R2 being Element of i -tuples_on the carrier of K holds Sum (R1 + R2) = (Sum R1) + (Sum R2) by Th8, SETWOP_2:35;