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 st T is bijective & g = f * (T ") holds
( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )
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 st T is bijective & g = f * (T ") holds
( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )
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 st T is bijective & g = f * (T ") holds
( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )
let f be PartFunc of X,ExtREAL; :: thesis: for g being PartFunc of Y,ExtREAL st T is bijective & g = f * (T ") holds
( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )
let g be PartFunc of Y,ExtREAL; :: thesis: ( T is bijective & g = f * (T ") implies ( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) ) )
assume A1: ( T is bijective & g = f * (T ") ) ; :: thesis: ( f is_integrable_on M iff g is_integrable_on CopyMeasure (T,M) )

hereby :: thesis: ( g is_integrable_on CopyMeasure (T,M) implies f is_integrable_on M )

assume A2: f is_integrable_on M ; :: thesis: g is_integrable_on CopyMeasure (T,M)
then A3: ( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty ) by MESFUNC5:def 17;
consider A being Element of S such that
A4: ( A = dom f & f is A -measurable ) by A2, MESFUNC5:def 17;
consider B being Element of CopyField (T,S) such that
A5: ( B = T .: A & B = dom g & g is B -measurable ) by A1, A4, Th28;
( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) ) by A4, Th31, A1;
hence g is_integrable_on CopyMeasure (T,M) by A3, A5, MESFUNC5:def 17; :: thesis: verum

end;

assume A6: g is_integrable_on CopyMeasure (T,M) ; :: thesis: f is_integrable_on M
then A7: ( integral+ ((CopyMeasure (T,M)),(max+ g)) < +infty & integral+ ((CopyMeasure (T,M)),(max- g)) < +infty ) by MESFUNC5:def 17;
consider B being Element of CopyField (T,S) such that
A8: ( B = dom g & g is B -measurable ) by A6, MESFUNC5:def 17;
consider H being Function of Y,X such that
A9: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) by Th17, A1;
dom (.: H) = bool Y by FUNCT_2:def 1;
then (.: H) . B in S by A9, FUNCT_1:def 6;
then reconsider A = H .: B as Element of S by A9, Th1;
.: T is bijective by A1, Th1;
then A10: rng (.: T) = bool Y by FUNCT_2:def 3;
T .: A = (.: T) . A by A1, Th1;
then T .: A = (.: T) . ((.: H) . B) by A9, Th1;
then T .: A = B by A10, A9, FUNCT_1:35;
then A11: f is A -measurable by Th20, A1, A8;
dom f in bool X ;
then A12: dom f in dom (.: T) by FUNCT_2:def 1;
B = (T ") " (dom f) by A1, A8, RELAT_1:147;
then B = T .: (dom f) by A1, FUNCT_1:84;
then B = (.: T) . (dom f) by A1, Th1;
then (.: H) . B = dom f by A9, A12, FUNCT_1:34;
then A13: A = dom f by A9, Th1;
then ( integral+ (M,(max+ f)) = integral+ ((CopyMeasure (T,M)),(max+ g)) & integral+ (M,(max- f)) = integral+ ((CopyMeasure (T,M)),(max- g)) ) by Th31, A1, A11;
hence f is_integrable_on M by MESFUNC5:def 17, A7, A11, A13; :: thesis: verum