theorem Th4: :: VECTSP_1:8

for F being non empty right_complementable add-associative right_zeroed right-distributive doubleLoopStr
for x, y being Element of F holds x * (- y) = - (x * y)