theorem :: RFUNCT_3:83

for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds
Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))