theorem NF300: :: BINPACK1:14

for a being non empty at_most_one FinSequence of REAL ex k being Nat ex f being non empty FinSequence of NAT st
( dom f = dom a & ( for j being Nat st j in rng f holds
SumBin (a,f,{j}) <= 1 ) & k = card (rng f) )