theorem Th31: :: MEASUR14:31

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