:: deftheorem Def10 defines ElmFin MEASUR13:def 10 :
for m, n being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S st n <= m holds
ElmFin (M,n) = M . n;