theorem Th5: :: VECTSP_1:9

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