theorem Th26: :: MEASUR14:26

for X, Y being non empty set
for S being SigmaField of X
for T being Function of X,Y
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is_simple_func_in S & f is nonnegative holds
integral' ((CopyMeasure (T,M)),g) = integral' (M,f)