:: deftheorem defines at_most_one BINPACK1:def 3 :
for a being FinSequence of REAL holds
( a is at_most_one iff for i being Nat st 1 <= i & i <= len a holds
a . i <= 1 );