let i be Element of NAT ; :: thesis: for K being non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr
for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R
let K be non empty right_complementable commutative add-associative right_zeroed distributive left_unital doubleLoopStr ; :: thesis: for R being Element of i -tuples_on the carrier of K holds (- (1. K)) * R = - R
let R be Element of i -tuples_on the carrier of K; :: thesis: (- (1. K)) * R = - R
A1: ( (comp K) . (1. K) = - (1. K) & the_unity_wrt the multF of K = 1. K ) by Th7, VECTSP_1:def 25;
A2: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th17, Th18;
( the multF of K is having_a_unity & the addF of K is having_a_unity ) by Th10, Th11;
hence (- (1. K)) * R = - R by A1, A2, Th12, FINSEQOP:72; :: thesis: verum