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

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

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

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

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

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

let F be Finite_Sep_Sequence of S; :: thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) implies integral (M,f) = Sum x )

A1: len F = len F ;

assume ( f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) ) ; :: thesis: integral (M,f) = Sum x

hence integral (M,f) = Sum x by A1, Th2; :: thesis: verum

for f being PartFunc of X,ExtREAL

for M being sigma_Measure of S

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

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

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

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

for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

let M be sigma_Measure of S; :: thesis: for F being Finite_Sep_Sequence of S

for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

let F be Finite_Sep_Sequence of S; :: thesis: for a, x being FinSequence of ExtREAL st f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) holds

integral (M,f) = Sum x

let a, x be FinSequence of ExtREAL ; :: thesis: ( f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) implies integral (M,f) = Sum x )

A1: len F = len F ;

assume ( f is_simple_func_in S & dom f <> {} & f is nonnegative & 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) ) ) ; :: thesis: integral (M,f) = Sum x

hence integral (M,f) = Sum x by A1, Th2; :: thesis: verum