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