theorem Th28: :: MESFUN17:28

for I, J being non empty closed_interval Subset of REAL
for K being Subset of REAL
for z being Element of REAL
for f being PartFunc of [:[:RNS_Real,RNS_Real:],RNS_Real:],RNS_Real
for g being PartFunc of [:[:REAL,REAL:],REAL:],REAL
for Pg2 being PartFunc of [:REAL,REAL:],REAL st z in K & dom f = [:[:I,J:],K:] & f is_continuous_on [:[:I,J:],K:] & f = g & Pg2 = ProjPMap2 (|.(R_EAL g).|,z) holds
( Pg2 is_integrable_on Prod_Measure (L-Meas,L-Meas) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = Integral ((Prod_Measure (L-Meas,L-Meas)),(ProjPMap2 (|.(R_EAL g).|,z))) & Integral ((Prod_Measure (L-Meas,L-Meas)),Pg2) = (Integral1 ((Prod_Measure (L-Meas,L-Meas)),|.(R_EAL g).|)) . z )