let V be RealLinearSpace; :: thesis: for L1, L2 being Linear_Combination of V holds sum (L1 - L2) = (sum L1) - (sum L2)
let L1, L2 be Linear_Combination of V; :: thesis: sum (L1 - L2) = (sum L1) - (sum L2)
thus sum (L1 - L2) = (sum L1) + (sum ((- 1) * L2)) by Th34
.= (sum L1) + ((- 1) * (sum L2)) by Th35
.= (sum L1) - (sum L2) ; :: thesis: verum