let G be left-distributive doubleLoop; :: thesis: for b, a being Element of G holds (- b) * a = - (b * a)
let b, a be Element of G; :: thesis: (- b) * a = - (b * a)
(b * a) + ((- b) * a) = (b + (- b)) * a by VECTSP_1:def 12
.= (0. G) * a by Def7
.= 0. G by ALGSTR_1:34 ;
hence (- b) * a = - (b * a) by Def7; :: thesis: verum