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 A1, A2, MESFUNC3:def 2;
A9: f is_simple_func_in COM (S,M) by A1, Th33;
reconsider F1 = F as Finite_Sep_Sequence of COM (S,M) by Th32;
A10: dom f = union (rng F1) by A3, MESFUNC3:def 1;
A11: dom F1 = dom a by A3, MESFUNC3:def 1;
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 A3, MESFUNC3:def 1;
then A12: F1,a are_Re-presentation_of f by A10, A11, MESFUNC3:def 1;
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 A6, FUNCT_1:13;
then (M * F) . n = (COM M) . (F1 . n) by Th35;
then (M * F) . n = ((COM M) * F1) . n by A13, A6, FUNCT_1:13;
hence x . n = (a . n) * (((COM M) * F1) . n) by A7, A13; :: thesis: verum

end;

hence integral (M,f) = integral ((COM M),f) by A8, A9, A2, A12, A4, A5, A6, MESFUNC3:def 2; :: thesis: verum