:: deftheorem Def5 defines SubFin MEASUR13:def 5 :
for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence st n <= m holds
SubFin (X,n) = X | n;