theorem Th30: :: MEASUR13:30

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 & M is sigma_finite holds
SubFin (M,n) is sigma_finite