theorem :: FVSUM_1:58

for i being Nat
for K being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (0. K) * R = i |-> (0. K)