theorem :: MESFUN18:65

for n being non zero Nat
for D being b₁ + 1 -element FinSequence
for D1 being b₁ -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
for Dk1 being non empty closed_interval Subset of REAL
for x being Element of CarProduct ((Seg n) --> REAL)
for Pg being PartFunc of REAL,REAL st D1 = D | n & ( for i being Nat st i in Seg (n + 1) holds
D . i is Subset of REAL ) & f is_continuous_on product D & dom f = product D & G = f * (CarProd ((Seg (n + 1)) --> REAL)) & g0 = G & Dk1 = D . (n + 1) & x in CarProduct D1 & Pg = ProjPMap1 (|.(R_EAL g0).|,x) holds
( dom (ProjPMap1 (|.(R_EAL g0).|,x)) = D . (n + 1) & Pg | Dk1 is continuous & Pg | Dk1 is bounded & Pg is_integrable_on Dk1 & ProjPMap1 (|.(R_EAL g0).|,x) is_integrable_on L-Meas & Integral (L-Meas,(ProjPMap1 (|.(R_EAL g0).|,x))) = integral (Pg,Dk1) & (Integral2 (L-Meas,|.(R_EAL g0).|)) . x = integral (Pg,Dk1) )