let X be non empty set ; :: thesis: for S being SigmaField of X

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

let f be PartFunc of X,ExtREAL; :: thesis: for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

let M be sigma_Measure of S; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative implies ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x ) )

assume that

A1: f is_simple_func_in S and

A2: ( dom f <> {} & f is nonnegative ) ; :: thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that

A3: F,a are_Re-presentation_of f by A1, MESFUNC3:12;

ex x being FinSequence of ExtREAL st

( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) )

A5: ( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) ) ;

integral (M,f) = Sum x by A1, A2, A3, A5, Th3;

hence ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x ) by A3, A5; :: thesis: verum

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

let f be PartFunc of X,ExtREAL; :: thesis: for M being sigma_Measure of S st f is_simple_func_in S & dom f <> {} & f is nonnegative holds

ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

let M be sigma_Measure of S; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative implies ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x ) )

assume that

A1: f is_simple_func_in S and

A2: ( dom f <> {} & f is nonnegative ) ; :: thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x )

consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that

A3: F,a are_Re-presentation_of f by A1, MESFUNC3:12;

ex x being FinSequence of ExtREAL st

( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) )

proof

then consider x being FinSequence of ExtREAL such that
deffunc H_{1}( Nat) -> Element of ExtREAL = (a . $1) * ((M * F) . $1);

consider x being FinSequence of ExtREAL such that

A4: ( len x = len F & ( for k being Nat st k in dom x holds

x . k = H_{1}(k) ) )
from FINSEQ_2:sch 1();

take x ; :: thesis: ( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) )

dom x = Seg (len F) by A4, FINSEQ_1:def 3

.= dom F by FINSEQ_1:def 3 ;

hence ( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) ) by A4; :: thesis: verum

end;consider x being FinSequence of ExtREAL such that

A4: ( len x = len F & ( for k being Nat st k in dom x holds

x . k = H

take x ; :: thesis: ( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) )

dom x = Seg (len F) by A4, FINSEQ_1:def 3

.= dom F by FINSEQ_1:def 3 ;

hence ( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) ) by A4; :: thesis: verum

A5: ( dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) ) ;

integral (M,f) = Sum x by A1, A2, A3, A5, Th3;

hence ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & integral (M,f) = Sum x ) by A3, A5; :: thesis: verum