let R be domRing; :: thesis: for V being RightMod of R
for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let V be RightMod of R; :: thesis: for L being Linear_Combination of V holds Sum (- L) = - (Sum L)
let L be Linear_Combination of V; :: thesis: Sum (- L) = - (Sum L)
thus Sum (- L) = (Sum L) * (- (1_ R)) by Th59
.= - (Sum L) by VECTSP_2:32 ; :: thesis: verum