let G be addGroup; :: 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)
thus (- a) * b = (- (a + b)) + (- (- b)) by Th16
.= - ((- b) + (a + b)) by Th16
.= - (a * b) by RLVECT_1:def 3 ; :: thesis: verum