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