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
for f being PartFunc of (CarProduct X),ExtREAL
for f1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL
for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = f1 & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),f1)))
let X be non-empty n + 1 -element FinSequence; :: thesis: for S being sigmaFieldFamily of X
for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for f1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL
for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = f1 & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),f1)))
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for f1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL
for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = f1 & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),f1)))
let M be sigmaMeasureFamily of S; :: thesis: for f being PartFunc of (CarProduct X),ExtREAL
for f1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL
for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = f1 & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),f1)))
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis: for f1 being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL
for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = f1 & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.f1.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),f1)))
let g be PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL; :: thesis: for f2 being PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL st M is sigma_finite & f = g & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.g.|)) . x < +infty ) holds
Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),g)))
let f2 be PartFunc of (CarProduct (SubFin (X,(n + 1)))),ExtREAL; :: thesis: ( M is sigma_finite & f = g & f = f2 & f is_integrable_on Prod_Measure M & ( for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.g.|)) . x < +infty ) implies Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),g))) )
assume that
A1: M is sigma_finite and
A2: f = g and
A3: f = f2 and
A4: f is_integrable_on Prod_Measure M and
A5: for x being Element of CarProduct (SubFin (X,n)) holds (Integral2 ((ElmFin (M,(n + 1))),|.g.|)) . x < +infty ; :: thesis: Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),g)))
A6: ( Integral ((Prod_Measure M),f) = Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),g) & ( for x being Element of CarProduct (SubFin (X,n)) holds ProjPMap1 (g,x) is_integrable_on ElmFin (M,(n + 1)) ) & ( for U being Element of Prod_Field (SubFin (S,n)) holds Integral2 ((ElmFin (M,(n + 1))),g) is U -measurable ) & Integral2 ((ElmFin (M,(n + 1))),g) is_integrable_on Prod_Measure (SubFin (M,n)) & Integral ((Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1))))),g) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),g))) & Integral2 ((ElmFin (M,(n + 1))),g) in L1_Functions (Prod_Measure (SubFin (M,n))) ) by A1, A2, A5, A4, Th35;
reconsider h = Integral2 ((ElmFin (M,(n + 1))),g) as Function of (CarProduct (SubFin (X,n))),ExtREAL ;
( len X = n + 1 & len S = n + 1 & len M = n + 1 ) by CARD_1:def 7;
then A7: ( X = X | (n + 1) & S = S | (n + 1) & M = M | (n + 1) ) by FINSEQ_1:58;
then ( X = SubFin (X,(n + 1)) & S = SubFin (S,(n + 1)) ) by Def5, Def6;
hence Integral ((Prod_Measure (SubFin (M,(n + 1)))),f2) = Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),g))) by A3, A6, A7, Def9; :: thesis: verum