let GF be non empty right_complementable associative well-unital distributive Abelian add-associative right_zeroed 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:27
.= ((0. GF) * a) - ((1. GF) * a) by VECTSP_1:45
.= (0. GF) - ((1. GF) * a) by VECTSP_1:39
.= - ((1. GF) * a) by RLVECT_1:27
.= - a by VECTSP_1:def 19 ; :: thesis: verum