let X, Y be non empty set ; :: thesis: 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)) )
let S be SigmaField of X; :: thesis: 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)) )
let T be Function of X,Y; :: thesis: 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)) )
let M be sigma_Measure of S; :: thesis: 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)) )
let f be PartFunc of X,ExtREAL; :: thesis: 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)) )
let g be PartFunc of Y,ExtREAL; :: thesis: 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)) )
let A be Element of S; :: thesis: ( T is bijective & g = f * (T ") & A = dom f & f is A -measurable implies ( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) ) )
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: A = dom f and
A4: f is A -measurable ; :: thesis: ( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) )
A5: ( A = dom (max+ f) & A = dom (max- f) ) by A3, MESFUNC2:def 2, MESFUNC2:def 3;
A6: ( max+ f is A -measurable & max- f is A -measurable ) by A3, A4, MESFUNC2:25, MESFUNC2:26;
A7: ( max+ g = (max+ f) * (T ") & max- g = (max- f) * (T ") ) by A1, A2, Th27;
A8: for x being Element of X holds 0. <= (max+ f) . x by MESFUNC2:12;
for x being Element of X holds 0. <= (max- f) . x by MESFUNC2:13;
hence ( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) ) by A7, A8, Th29, A1, A5, A6, SUPINF_2:39; :: thesis: verum