theorem :: RFUNCT_3:82

for D being non empty set
for F being PartFunc of D,REAL
for d being Element of D st d in dom F holds
Sum (F,{d}) = F . d