let K be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for p being FinSequence of the carrier of K holds Sum (- p) = - (Sum p)
let p be FinSequence of the carrier of K; :: thesis: Sum (- p) = - (Sum p)
( the addF of K is having_an_inverseOp & the_inverseOp_wrt the addF of K = comp K ) by Th14, Th15;
hence Sum (- p) = (comp K) . (Sum p) by Th8, SETWOP_2:31
.= - (Sum p) by VECTSP_1:def 13 ;
:: thesis: verum