let K be non empty right_complementable right-distributive right_unital add-associative right_zeroed doubleLoopStr ; :: thesis: for a being Element of K holds a * (- (1. K)) = - a
let x be Element of K; :: thesis: x * (- (1. K)) = - x
thus x * (- (1. K)) = x * ((0. K) - (1. K)) by RLVECT_1:27
.= (x * (0. K)) - (x * (1. K)) by VECTSP_1:43
.= (0. K) - (x * (1. K)) by VECTSP_1:36
.= - (x * (1. K)) by RLVECT_1:27
.= - x by VECTSP_1:def 13 ; :: thesis: verum