let n be non zero Nat; :: thesis:
let X be non-empty n + 1 -element FinSequence; :: thesis:
let S be sigmaFieldFamily of X; :: thesis:
let M be sigmaMeasureFamily of S; :: thesis:
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis:
assume A1: f is_integrable_on Prod_Measure M ; :: thesis:
A2: Prod_Measure M = Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) by Th28;
reconsider g = f as PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL by Th6;
take g ; :: thesis:
thus f = g ; :: thesis:
A3: n < n + 1 by NAT_1:13;
A4: len X = n + 1 by CARD_1:def 7;
SubFin (X,(n + 1)) = X | (n + 1) by Def5;
then A5: X = SubFin (X,(n + 1)) by A4, FINSEQ_1:58;
A6: len S = n + 1 by CARD_1:def 7;
SubFin (S,(n + 1)) = S | (n + 1) by Def6;
then S = SubFin (S,(n + 1)) by A6, FINSEQ_1:58;
then A7: Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) by A5, A3, Th21;
hence g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) by A1, A2, Th6; :: thesis:
thus Integral ((Prod_Measure M),f) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),g) by A7, A2, Th6; :: thesis: