theorem :: MESFUN18:55

for n being non zero Nat
for D being b₁ -element FinSequence
for I being Subset of (CarProduct ((Seg n) --> RNS_Real))
for J being closed_interval Subset of REAL
for f being PartFunc of [:(CarProduct ((Seg n) --> RNS_Real)),RNS_Real:],RNS_Real
for g being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg n holds
D . i is closed_interval Subset of REAL ) & I = CarProduct D & [:I,J:] = dom f & f is_continuous_on [:I,J:] & f = g holds
( g is_integrable_on Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas) & ( for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g).|)) . x < +infty ) & ( for y being Element of REAL holds (Integral1 ((Prod_Measure (L-Meas n)),|.(R_EAL g).|)) . y < +infty ) & ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g)) is U -measurable ) & ( for V being Element of L-Field holds Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is V -measurable ) & Integral2 (L-Meas,(R_EAL g)) is_integrable_on Prod_Measure (L-Meas n) & Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)) is_integrable_on L-Meas & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g)))) & Integral ((Prod_Measure ((Prod_Measure (L-Meas n)),L-Meas)),g) = Integral (L-Meas,(Integral1 ((Prod_Measure (L-Meas n)),(R_EAL g)))) ) by Lm3, Lm4;