theorem :: GCD_1:48

for F being non empty right_complementable distributive Abelian add-associative right_zeroed doubleLoopStr
for x, y being Element of F holds
( (- x) * y = - (x * y) & x * (- y) = - (x * y) ) by VECTSP_1:8, VECTSP_1:9;