let X, Y be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let T be Function of X,Y; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let g be PartFunc of Y,ExtREAL; :: thesis:
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: f is_simple_func_in S and
A4: f is nonnegative ; :: thesis:
set L = CopyMeasure (T,M);
A5: dom T = X by FUNCT_2:def 1;
A6: dom f c= X ;
g * T = f * ((T ") * T) by A2, RELAT_1:36;
then g * T = f * (id (dom T)) by A1, FUNCT_1:39;
then A7: g * T = f by RELAT_1:51, A5, A6;

suppose A8: dom f = {} ; :: thesis:

assume dom g <> {} ; :: thesis:
then ex x being object st x in dom g by XBOOLE_0:def 1;
hence contradiction by A8, A2, FUNCT_1:11; :: thesis:

end;

then integral' ((CopyMeasure (T,M)),g) = 0. by MESFUNC5:def 14;
hence integral' ((CopyMeasure (T,M)),g) = integral' (M,f) by A8, MESFUNC5:def 14; :: thesis:

end;

suppose A9: dom f <> {} ; :: thesis:

then ex x being object st x in dom f by XBOOLE_0:def 1;
then dom g <> {} by A7, FUNCT_1:11;
then integral' ((CopyMeasure (T,M)),g) = integral ((CopyMeasure (T,M)),g) by MESFUNC5:def 14;
then integral' ((CopyMeasure (T,M)),g) = integral (M,f) by A1, A2, A3, A4, Th25;
hence integral' ((CopyMeasure (T,M)),g) = integral' (M,f) by MESFUNC5:def 14, A9; :: thesis:

end;

end;