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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 X,S,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 <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 X,S,M,f = Sum x
let a, x be FinSequence of ExtREAL ; :: thesis: ( f is_simple_func_in S & dom f <> {} & ( for x being set st x in dom f holds
0. <= f . x ) & 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 X,S,M,f = Sum x )
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: for x being set st x in dom f holds
0. <= f . x and
A4: F,a are_Re-presentation_of f and
A5: dom x = dom F and
A6: for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) ; :: thesis: integral X,S,M,f = Sum x
len F = len F ;
hence integral X,S,M,f = Sum x by A1, A2, A3, A4, A5, A6, Th2; :: thesis: verum