theorem Th22: :: MEASUR13:22

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
(ProdSigmaMesFinSeq M) . n is sigma_Measure of (Prod_Field (SubFin (S,n)))