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)

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

hence
integral (M,f) = integral ((COM M),f)
by A8, A9, A2, A12, A4, A5, A6, MESFUNC3:def 2; :: thesis: verum
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;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