let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral (M,f) = integral ((COM M),f)

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral (M,f) = integral ((COM M),f)

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral (M,f) = integral ((COM M),f)

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & f is nonnegative implies integral (M,f) = integral ((COM M),f) )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis: integral (M,f) = integral ((COM M),f)
consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A3: F,a are_Re-presentation_of f and
A4: a . 1 = 0. and
A5: for n being Nat st 2 <= n & n in dom a holds
( 0. < a . n & a . n < +infty ) and
A6: dom x = dom F and
A7: for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) and
A8: integral (M,f) = Sum x by ;
A9: f is_simple_func_in COM (S,M) by ;
reconsider F1 = F as Finite_Sep_Sequence of COM (S,M) by Th32;
A10: dom f = union (rng F1) by ;
A11: dom F1 = dom a by ;
for n being Nat st n in dom F1 holds
for x being object st x in F1 . n holds
f . x = a . n by ;
then A12: F1,a are_Re-presentation_of f by ;
for n being Nat st n in dom x holds
x . n = (a . n) * (((COM M) * F1) . n)
proof
let n be Nat; :: thesis: ( n in dom x implies x . n = (a . n) * (((COM M) * F1) . n) )
assume A13: n in dom x ; :: thesis: x . n = (a . n) * (((COM M) * F1) . n)
then (M * F) . n = M . (F . n) by ;
then (M * F) . n = (COM M) . (F1 . n) by Th35;
then (M * F) . n = ((COM M) * F1) . n by ;
hence x . n = (a . n) * (((COM M) * F1) . n) by ; :: thesis: verum
end;
hence integral (M,f) = integral ((COM M),f) by ; :: thesis: verum