theorem NF320: :: BINPACK1:17

for a being non empty FinSequence of REAL
for f being FinSequence of NAT st dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) holds
[/(Sum a)\] <= card (rng f)