theorem Th56: :: MESFUN18:56

for n being non zero Nat
for D being b₁ + 1 -element FinSequence
for f being PartFunc of (CarProduct ((Seg (n + 1)) --> RNS_Real)),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 f = g & g0 = g & ( for i being Nat st i in Seg (n + 1) holds
D . i is closed_interval Subset of REAL ) & f is_continuous_on CarProduct D & dom f = CarProduct D holds
( 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 ((Prod_Measure (L-Meas n)),L-Meas)),g0) )