let F be non empty right_complementable add-associative right_zeroed right-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)
(x * y) + (x * (- y)) = x * (y + (- y)) by Def2
.= x * (0. F) by RLVECT_1:def 10
.= 0. F ;
hence x * (- y) = - (x * y) by RLVECT_1:def 10; :: thesis: verum