let n be non zero Nat; :: thesis: for X being non-empty n + 1 -element FinSequence
for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
let X be non-empty n + 1 -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S holds Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S holds Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
let M be sigmaMeasureFamily of S; :: thesis: Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
Prod_Measure M = product_sigma_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) by Th25;
hence Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) by MESFUN12:def 9; :: thesis: verum