theorem :: VECTSP_2:29

for K being non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr
for a being Element of K holds (- (1. K)) * a = - a