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 E being Element of Prod_Field S
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
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 E being Element of Prod_Field S
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
let S be sigmaFieldFamily of X; :: thesis: for M being sigmaMeasureFamily of S
for f being PartFunc of (CarProduct X),ExtREAL
for E being Element of Prod_Field S
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
let M be sigmaMeasureFamily of S; :: thesis: for f being PartFunc of (CarProduct X),ExtREAL
for E being Element of Prod_Field S
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
let f be PartFunc of (CarProduct X),ExtREAL; :: thesis: for E being Element of Prod_Field S
for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
let E be Element of Prod_Field S; :: thesis: for g being PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL st M is sigma_finite & E = dom f & f is E -measurable & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
let g be PartFunc of [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):],ExtREAL; :: thesis: ( M is sigma_finite & E = dom f & f is E -measurable & f = g implies ( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty ) )
assume that
A1: M is sigma_finite and
A2: E = dom f and
A3: f is E -measurable and
A4: f = g ; :: thesis: ( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty )
A5: CarProduct X = [:(CarProduct (SubFin (X,n))),(ElmFin (X,(n + 1))):] by Th6;
A6: Prod_Field S = sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) by Th34;
reconsider E1 = E as Element of sigma (measurable_rectangles ((Prod_Field (SubFin (S,n))),(ElmFin (S,(n + 1))))) by Th34;
n <= n + 1 by NAT_1:12;
then A7: Prod_Measure (SubFin (M,n)) is sigma_finite by Th30, A1, Th29;
ElmFin (M,(n + 1)) is sigma_finite by Th31, A1;
hence ( g is_integrable_on Prod_Measure ((Prod_Measure (SubFin (M,n))),(ElmFin (M,(n + 1)))) iff Integral ((Prod_Measure (SubFin (M,n))),(Integral2 ((ElmFin (M,(n + 1))),|.g.|))) < +infty ) by MESFUN13:11, A3, A5, A6, A4, A2, A7; :: thesis: verum