theorem Th29: :: MEASUR14:29

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 A being Element of S
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") & f is nonnegative & A = dom f & f is A -measurable holds
integral+ ((CopyMeasure (T,M)),g) = integral+ (M,f)