theorem Th6: :: VECTSP_1:10

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