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:
A5: ( g is_simple_func_in CopyField (T,S) & g is nonnegative ) by A1, A2, A3, A4, Th23, Th22;
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A6: ( F,a are_Re-presentation_of f & a . 1 = 0. & ( for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x ) by A3, A4, MESFUNC3:def 2;
consider G being Finite_Sep_Sequence of CopyField (T,S) such that
A7: ( G = ((.: T) | S) * F & G,a are_Re-presentation_of g ) by A1, A2, A6, Th24;
set L = CopyMeasure (T,M);
set H = (.: T) | S;
for n being Nat st n in dom x holds
x . n = (a . n) * (((CopyMeasure (T,M)) * G) . n)

let n be Nat; :: thesis:
assume A8: n in dom x ; :: thesis:
then A9: x . n = (a . n) * ((M * F) . n) by A6;
A10: (M * F) . n = M . (F . n) by A8, A6, FUNCT_1:13;
A11: ((CopyMeasure (T,M)) * G) . n = (CopyMeasure (T,M)) . (G . n) by A8, A6, A7, FUNCT_1:13;
reconsider Gn = G . n as Element of CopyField (T,S) ;
consider Kn being Element of S such that
A12: ( Gn = T .: Kn & (CopyMeasure (T,M)) . Gn = M . Kn ) by A1, Def4;
A13: Gn = (.: T) . Kn by A12, A1, Th1;
A14: .: T is one-to-one by A1;
A15: dom (.: T) = bool X by FUNCT_2:def 1;
G . n = ((.: T) | S) . (F . n) by A7, A8, A6, FUNCT_1:13;
then G . n = (.: T) . (F . n) by FUNCT_1:49;
hence x . n = (a . n) * (((CopyMeasure (T,M)) * G) . n) by A9, A10, A11, A12, A13, A14, A15; :: thesis:

end;