:: deftheorem Def1 defines ElmFin MEASUR13:def 1 :
for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence st n <= m holds
ElmFin (X,n) = X . n;