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

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