theorem Th17: :: MEASUR13:17

for m, n, k 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 k <= n & n <= m holds
ElmFin (M,k) = ElmFin ((SubFin (M,n)),k)