theorem :: VECTSP_2:28

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