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) ) )

proof

deffunc H₁( 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₁(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;

then consider x being FinSequence of ExtREAL such that
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