let V be RealLinearSpace; :: 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) = (- 1) * (Sum L) by Th2
.= - (Sum L) by RLVECT_1:16 ; :: thesis: verum