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:14
.= (x * (0. K)) - (x * (1. K)) by VECTSP_1:11
.= (0. K) - (x * (1. K))
.= - (x * (1. K)) by RLVECT_1:14
.= - x ; :: thesis: verum