:: deftheorem Def13 defines ProdSigmaMesFinSeq MEASUR13:def 13 :
for m being non zero Nat
for X being non-empty b₁ -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for b₅ being sigmaMeasureFamily of ProdSigmaFldFinSeq S holds
( b₅ = ProdSigmaMesFinSeq M iff ( b₅ . 1 = M . 1 & ( for i being non zero Nat st i < m holds
ex Mi being sigma_Measure of (Prod_Field (SubFin (S,i))) st
( Mi = b₅ . i & b₅ . (i + 1) = product_sigma_Measure (Mi,(ElmFin (M,(i + 1)))) ) ) ) );