let V be Z_Module; :: thesis: for L being Z_Linear_Combination of V holds Sum (- L) = - (Sum L)
let L be Z_Linear_Combination of V; :: thesis: Sum (- L) = - (Sum L)
thus Sum (- L) = (- 1) * (Sum L) by Th53
.= - (Sum L) by ZMODUL01:2 ; :: thesis: verum