for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for k being Nat
for R1 being real-valued FinSequence st dom f = dom a & rng f = Seg k & len R1 = k & ( for j being Nat st j in dom R1 holds
R1 . j = SumBin (a,f,{j}) ) holds
Sum R1 = SumBin (a,f,(rng f))