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

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