let i be Nat; :: thesis: for K being non empty right_complementable commutative distributive left_unital add-associative right_zeroed 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 distributive left_unital add-associative right_zeroed 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 Th5, VECTSP_1:def 13;
A2: ( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
( the multF of K is having_a_unity & the addF of K is having_a_unity ) by Th8;
hence (- (1. K)) * R = - R by A1, A2, Th10, FINSEQOP:68; :: thesis: verum