let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL
for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds
Integral M,f = Sum x
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL
for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds
Integral M,f = Sum x
let f be PartFunc of X,REAL ; :: thesis: for M being sigma_Measure of S
for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL
for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds
Integral M,f = Sum x
let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S
for a being FinSequence of REAL
for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds
Integral M,f = Sum x
let F be Finite_Sep_Sequence of S; :: thesis: for a being FinSequence of REAL
for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds
Integral M,f = Sum x
let a be FinSequence of REAL ; :: thesis: for x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) holds
Integral M,f = Sum x
let x be FinSequence of ExtREAL ; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative & dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F & ( for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ) implies Integral M,f = Sum x )
assume that
A1: ( f is_simple_func_in S & dom f <> {} ) and
A2: f is nonnegative and
A3: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & dom x = dom F ) and
A4: for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ; :: thesis: Integral M,f = Sum x
B1: ( R_EAL f is_simple_func_in S & dom (R_EAL f) <> {} ) by A1, MESFUNC6:49;
B2: for x being set st x in dom (R_EAL f) holds
0 <= (R_EAL f) . x by MESFUNC6:51, A2;
reconsider a0 = a as FinSequence of ExtREAL by MESFUNC3:11;
B3: F,a0 are_Re-presentation_of R_EAL f by MESFUNC3:def 1, A3;
B5: for n being Nat st n in dom x holds
x . n = (a0 . n) * ((M * F) . n)

proof

let n be Nat; :: thesis: ( n in dom x implies x . n = (a0 . n) * ((M * F) . n) )
assume n in dom x ; :: thesis: x . n = (a0 . n) * ((M * F) . n)
then x . n = (R_EAL (a . n)) * ((M * F) . n) by A4;
hence x . n = (a0 . n) * ((M * F) . n) ; :: thesis: verum

end;

thus Integral M,f = integral' M,(R_EAL f) by A2, A1, MESFUNC6:83
.= integral X,S,M,(R_EAL f) by A1, MESFUNC5:def 14
.= Sum x by A3, B1, B2, B3, B5, MESFUNC4:3 ; :: thesis: verum