theorem :: RFUNCT_3:84

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 & dom (F | X) misses dom (F | Y) holds
Sum (F,(X \/ Y)) = (Sum (F,X)) + (Sum (F,Y))