for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for s being set st s misses rng f holds
SumBin (a,f,s) = 0