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