theorem Th21: :: FVSUM_1:21

for i being Nat
for K being non empty left_zeroed Abelian right_zeroed addLoopStr
for R being Element of i -tuples_on the carrier of K holds
( R + (i |-> (0. K)) = R & R = (i |-> (0. K)) + R )