:: deftheorem defines SumBin BINPACK1:def 2 :
for a being non empty FinSequence of REAL
for f being Function
for s being set holds SumBin (a,f,s) = Sum (Seq (a,(f " s)));