theorem Th25: :: MEASUR13:25

for n being non zero Nat
for X being non-empty b₁ + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Measure M = product_sigma_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))