let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for a being Element of GF holds (- (1. GF)) * a = - a
let a be Element of GF; :: thesis: (- (1. GF)) * a = - a
thus (- (1. GF)) * a = ((0. GF) - (1. GF)) * a by RLVECT_1:14
.= ((0. GF) * a) - ((1. GF) * a) by VECTSP_1:13
.= (0. GF) - ((1. GF) * a)
.= - ((1. GF) * a) by RLVECT_1:14
.= - a ; :: thesis: verum