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 ((CopyMeasure (T,M)),g) = Integral (M,f)
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 ((CopyMeasure (T,M)),g) = Integral (M,f)
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 ((CopyMeasure (T,M)),g) = Integral (M,f)
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 ((CopyMeasure (T,M)),g) = Integral (M,f)
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 ((CopyMeasure (T,M)),g) = Integral (M,f)
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 ((CopyMeasure (T,M)),g) = Integral (M,f)
let A be Element of S; :: thesis: ( T is bijective & g = f * (T ") & A = dom f & f is A -measurable implies Integral ((CopyMeasure (T,M)),g) = Integral (M,f) )
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: A = dom f and
A4: f is A -measurable ; :: thesis: Integral ((CopyMeasure (T,M)),g) = Integral (M,f)
A5: ( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) ) by A1, A2, A3, A4, Th31;
Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16;
hence Integral ((CopyMeasure (T,M)),g) = Integral (M,f) by A5, MESFUNC5:def 16; :: thesis: verum