for D being non empty set
for F being PartFunc of D,REAL holds Sum (F,{}) = 0 by Th68, RVSUM_1:72;