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 = product_sigma_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 = product_sigma_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 = product_sigma_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
let M be sigmaMeasureFamily of S; :: thesis: Prod_Measure M = product_sigma_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))
A1: n < n + 1 by NAT_1:13;
then ex Mn being sigma_Measure of (Prod_Field (SubFin (S,n))) st
( Mn = (ProdSigmaMesFinSeq M) . n & Prod_Measure M = product_sigma_Measure (Mn,(ElmFin (M,(n + 1)))) ) by Def13;
hence Prod_Measure M = product_sigma_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) by A1, Th24; :: thesis: verum