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