:: deftheorem defines Seq BINPACK1:def 1 :
for D being non empty set
for f being b₁ -valued FinSequence
for I being set holds Seq (f,I) = Seq (f | I);