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 A be Element of S; :: thesis:
let g be PartFunc of Y,ExtREAL; :: thesis:
assume that
A1: T is bijective and
A2: g = f * (T ") and
A3: f is nonnegative and
A4: A = dom f and
A5: f is A -measurable ; :: thesis:
dom (.: T) = bool X by FUNCT_2:def 1;
then (.: T) . A in (.: T) .: S by FUNCT_1:def 6;
then (.: T) . A in CopyField (T,S) by A1, Def2;
then reconsider B = T .: A as Element of CopyField (T,S) by A1, Th1;
A6: g is B -measurable by A1, A2, A5, Th20;
A7: g is nonnegative by Th23, A1, A2, A3;
dom g = (T ") " (dom f) by A2, RELAT_1:147;
then A8: dom g = B by A4, A1, FUNCT_1:84;
consider F being Functional_Sequence of X,ExtREAL, K being ExtREAL_sequence such that
A9: ( ( for n being Nat holds
( F . n is_simple_func_in S & dom (F . n) = dom f ) ) & ( for n being Nat holds F . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F . n) . x <= (F . m) . x ) & ( for x being Element of X st x in dom f holds
( F # x is convergent & lim (F # x) = f . x ) ) & ( for n being Nat holds K . n = integral' (M,(F . n)) ) & K is convergent & integral+ (M,f) = lim K ) by A4, A3, A5, MESFUNC5:def 15;
A10: ( dom T = X & rng T = Y ) by A1, FUNCT_2:def 1, FUNCT_2:def 3;
A11: ( rng T = dom (T ") & dom T = rng (T ") ) by A1, FUNCT_1:33;
then reconsider H = T " as Function of Y,X by A10, FUNCT_2:1;
consider H being Function of Y,X such that
A12: ( H is bijective & H = T " & H " = T & .: H = (.: T) " & (.: H) .: (CopyField (T,S)) = S & CopyField (H,(CopyField (T,S))) = S ) by Th17, A1;
for x being object holds
( x in T .: (dom f) iff x in dom g )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume x in T .: (dom f) ; :: thesis:
then consider t being object such that
A13: ( t in dom T & t in dom f & x = T . t ) by FUNCT_1:def 6;
A14: x in dom H by A12, A10, A13, A11, FUNCT_2:5;
H . x = t by A12, A13, FUNCT_1:34;
hence x in dom g by A12, A2, A13, A14, FUNCT_1:11; :: thesis:

end;

assume A15: x in dom g ; :: thesis:
then A16: ( x in dom H & H . x in dom f ) by A12, A2, FUNCT_1:11;
T . (H . x) = x by A12, A10, A15, FUNCT_1:35;
hence x in T .: (dom f) by A10, A16, FUNCT_1:def 6; :: thesis:

end;

then A17: T .: (dom f) = dom g by TARSKI:2;
A18: for n being Nat holds dom ((F . n) * H) = T .: (dom (F . n))

proof

let n be Nat; :: thesis:
for x being object holds
( x in dom ((F . n) * H) iff x in T .: (dom (F . n)) )

proof

let x be object ; :: thesis:

hereby :: thesis:

assume A19: x in dom ((F . n) * H) ; :: thesis:
then ( x in dom H & H . x in dom (F . n) ) by FUNCT_1:11;
then T . (H . x) in T .: (dom (F . n)) by A10, FUNCT_1:def 6;
hence x in T .: (dom (F . n)) by A12, A10, A19, FUNCT_1:35; :: thesis:

end;

assume x in T .: (dom (F . n)) ; :: thesis:
then consider t being object such that
A20: ( t in dom T & t in dom (F . n) & x = T . t ) by FUNCT_1:def 6;
A21: x in dom H by A12, A10, A11, A20, FUNCT_2:5;
H . x = t by A12, FUNCT_1:34, A20;
hence x in dom ((F . n) * H) by A20, A21, FUNCT_1:11; :: thesis:

end;

hence dom ((F . n) * H) = T .: (dom (F . n)) by TARSKI:2; :: thesis:

end;

deffunc H₁( Nat) -> Element of bool [:Y,ExtREAL:] = (F . $1) * H;
consider G being Functional_Sequence of Y,ExtREAL such that
A22: for n being Nat holds G . n = H₁(n) from SEQFUNC:sch 1();
set L = CopyMeasure (T,M);
A23: for n being Nat holds
( G . n is_simple_func_in CopyField (T,S) & dom (G . n) = dom g )

proof

let n be Nat; :: thesis:
A24: ( F . n is_simple_func_in S & dom (F . n) = dom f ) by A9;
A25: G . n = (F . n) * H by A22;
hence G . n is_simple_func_in CopyField (T,S) by A12, Th22, A1, A24; :: thesis:
thus dom (G . n) = dom g by A17, A18, A24, A25; :: thesis:

end;

A26: for n being Nat holds G . n is nonnegative

proof

let n be Nat; :: thesis:
A27: F . n is nonnegative by A9;
G . n = (F . n) * H by A22;
hence G . n is nonnegative by A12, A1, Th23, A27; :: thesis:

end;

A28: for n, m being Nat st n <= m holds
for y being Element of Y st y in dom g holds
(G . n) . y <= (G . m) . y

proof

let n, m be Nat; :: thesis:
assume A29: n <= m ; :: thesis:
let y be Element of Y; :: thesis:
assume y in dom g ; :: thesis:
then A30: ( y in dom H & H . y in dom f ) by A12, A2, FUNCT_1:11;
reconsider x = H . y as Element of X ;
A31: (F . n) . x <= (F . m) . x by A9, A29, A30;
A32: ( G . n = (F . n) * H & G . m = (F . m) * H ) by A22;
then (F . n) . x = (G . n) . y by A30, FUNCT_1:13;
hence (G . n) . y <= (G . m) . y by A31, A32, A30, FUNCT_1:13; :: thesis:

end;

A33: for y being Element of Y st y in dom g holds
( G # y is convergent & lim (G # y) = g . y )

proof

let y be Element of Y; :: thesis:
assume y in dom g ; :: thesis:
then A34: ( y in dom H & H . y in dom f ) by A12, A2, FUNCT_1:11;
reconsider x = H . y as Element of X ;
A35: ( F # x is convergent & lim (F # x) = f . x ) by A34, A9;
for n being Element of NAT holds (F # x) . n = (G # y) . n

proof

let n be Element of NAT ; :: thesis:
reconsider m = n as Nat ;
A36: (F # x) . m = (F . m) . x by MESFUNC5:def 13;
A37: (G # y) . m = (G . m) . y by MESFUNC5:def 13;
( G . n = (F . n) * H & G . m = (F . m) * H ) by A22;
hence (F # x) . n = (G # y) . n by A36, A37, A34, FUNCT_1:13; :: thesis:

end;

then F # x = G # y by FUNCT_2:def 7;
hence ( G # y is convergent & lim (G # y) = g . y ) by A35, A2, A12, A34, FUNCT_1:13; :: thesis:

end;

for n being Nat holds K . n = integral' ((CopyMeasure (T,M)),(G . n))

proof

let n be Nat; :: thesis:
A38: K . n = integral' (M,(F . n)) by A9;
A39: G . n = (F . n) * H by A22;
F . n is_simple_func_in S by A9;
hence K . n = integral' ((CopyMeasure (T,M)),(G . n)) by A9, A38, A39, A12, A1, Th26; :: thesis:

end;

hence integral+ ((CopyMeasure (T,M)),g) = integral+ (M,f) by A6, A7, A8, A9, A23, A26, A28, A33, MESFUNC5:def 15; :: thesis: