theorem Th26: :: FVSUM_1:26

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