for a being non empty positive FinSequence of REAL
for f being FinSequence of NAT
for s being set holds 0 <= SumBin (a,f,s)