theorem :: VECTSP_6:48

for GF being non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr
for a being Element of GF holds (- (1. GF)) * a = - a by Lm2;