:: deftheorem defines Sum RFUNCT_3:def 14 :
for D being non empty set
for F being PartFunc of D,REAL
for X being set holds Sum (F,X) = Sum (FinS (F,X));