theorem :: RFUNCT_3:79

for D being non empty set
for F, G being PartFunc of D,REAL
for X being set st dom (F | X) is finite & dom (F | X) = dom (G | X) holds
Sum ((F - G),X) = (Sum (F,X)) - (Sum (G,X))