theorem NF200: :: BINPACK1:8

for a being non empty FinSequence of REAL
for f being FinSequence of NAT
for j, b being Nat st (len f) + 1 <= len a & b = j holds
SumBin (a,(f ^ <*b*>),{j}) = (SumBin (a,f,{j})) + (a . ((len f) + 1))