let R be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of R holds (- 1) '*' a = - a
let a be Element of R; :: thesis: (- 1) '*' a = - a
(- 1) '*' a = - (1 * a) by Def2
.= - a by BINOM:13 ;
hence (- 1) '*' a = - a ; :: thesis: verum