let K be non empty right_complementable distributive left_unital add-associative right_zeroed doubleLoopStr ; :: thesis: (- (1. K)) * (- (1. K)) = 1. K
thus (- (1. K)) * (- (1. K)) = (1. K) * (1. K) by VECTSP_1:10
.= 1. K ; :: thesis: verum