theorem :: MESFUN18:64

for n being non zero Nat
for D being b₁ + 1 -element FinSequence
for f being PartFunc of (REAL-NS (n + 1)),RNS_Real
for G being PartFunc of (CarProduct ((Seg (n + 1)) --> REAL)),REAL
for g0 being PartFunc of [:(CarProduct ((Seg n) --> REAL)),REAL:],REAL st ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on product D & dom f = product D & G = f * (CarProd ((Seg (n + 1)) --> REAL)) & g0 = G holds
( ( for x being Element of CarProduct ((Seg n) --> REAL) holds (Integral2 (L-Meas,|.(R_EAL g0).|)) . x < +infty ) & ( for x being Element of CarProduct ((Seg n) --> REAL) holds ProjPMap1 ((R_EAL g0),x) is_integrable_on L-Meas ) & ( for U being Element of Prod_Field (L-Field n) holds Integral2 (L-Meas,(R_EAL g0)) is U -measurable ) & Integral2 (L-Meas,(R_EAL g0)) is_integrable_on Prod_Measure (L-Meas n) & Integral ((Prod_Measure (L-Meas (n + 1))),G) = Integral ((Prod_Measure (L-Meas n)),(Integral2 (L-Meas,(R_EAL g0)))) )