let V be Z_Module; :: thesis: for L1, L2 being Z_Linear_Combination of V holds Sum (L1 - L2) = (Sum L1) - (Sum L2)
let L1, L2 be Z_Linear_Combination of V; :: thesis: Sum (L1 - L2) = (Sum L1) - (Sum L2)
thus Sum (L1 - L2) = (Sum L1) + (Sum (- L2)) by Th52
.= (Sum L1) - (Sum L2) by Th54 ; :: thesis: verum