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

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