for n being Nat
for X being non empty set
for f being Function st f = (Seg n) --> X holds
f is non-empty b₁ -element FinSequence