theorem NF315: :: BINPACK1:2

for D being set
for p being FinSequence st ( for i being Nat st i in dom p holds
p . i in D ) holds
p is FinSequence of D