for n being non zero Nat
for f being Function
for X being b₁ -element FinSequence st f in product X holds
f is b₁ -element FinSequence