for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for s, t being set st s misses t holds
SumBin (a,f,(s \/ t)) = (SumBin (a,f,s)) + (SumBin (a,f,t))