let F be non empty right_complementable add-associative right_zeroed distributive doubleLoopStr ; :: thesis: for x, y being Element of F holds (- x) * (- y) = x * y
let x, y be Element of F; :: thesis: (- x) * (- y) = x * y
thus (- x) * (- y) = - (x * (- y)) by Th5
.= - (- (x * y)) by Th4
.= x * y by RLVECT_1:17 ; :: thesis: verum