let G be Abelian right-distributive doubleLoop; :: thesis: for a, b being Element of G holds a * (- b) = - (a * b)
let a, b be Element of G; :: thesis: a * (- b) = - (a * b)
(a * b) + (a * (- b)) = a * (b + (- b)) by VECTSP_1:def 2
.= a * (0. G) by Def1
.= 0. G by ALGSTR_1:16 ;
hence a * (- b) = - (a * b) by Def1; :: thesis: verum