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

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = {} holds

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

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = {} holds

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

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

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

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

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & dom f = {} implies ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 ) )

assume that

A1: f is_simple_func_in S and

A2: dom f = {} ; :: thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

for x being object st x in dom f holds

0 <= f . x by A2;

then f is nonnegative by SUPINF_2:52;

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

A3: F,a are_Re-presentation_of f and

A4: a . 1 = 0 and

A5: for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) by A1, MESFUNC3:14;

deffunc H_{1}( Nat) -> Element of ExtREAL = (a . $1) * ((M * F) . $1);

consider x being FinSequence of ExtREAL such that

A6: len x = len F and

A7: for n being Nat st n in dom x holds

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

A8: dom x = Seg (len F) by A6, FINSEQ_1:def 3;

then A9: dom x = dom F by FINSEQ_1:def 3;

take F ; :: thesis: ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

take a ; :: thesis: ex x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

take x ; :: thesis: ( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

consider sumx being sequence of ExtREAL such that

A10: Sum x = sumx . (len x) and

A11: sumx . 0 = 0 and

A12: for i being Nat st i < len x holds

sumx . (i + 1) = (sumx . i) + (x . (i + 1)) by EXTREAL1:def 2;

defpred S_{1}[ Nat] means ( $1 <= len x implies sumx . $1 = 0 );

A13: union (rng F) = {} by A2, A3, MESFUNC3:def 1;

A14: for n being Nat st n in dom F holds

F . n = {}_{1}[i] holds

S_{1}[i + 1]
_{1}[ 0 ]
by A11;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A22, A16);

hence ( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 ) by A3, A4, A5, A7, A8, A10, FINSEQ_1:def 3; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = {} holds

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

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL st f is_simple_func_in S & dom f = {} holds

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

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

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

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

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

let f be PartFunc of X,ExtREAL; :: thesis: ( f is_simple_func_in S & dom f = {} implies ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 ) )

assume that

A1: f is_simple_func_in S and

A2: dom f = {} ; :: thesis: ex F being Finite_Sep_Sequence of S ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

for x being object st x in dom f holds

0 <= f . x by A2;

then f is nonnegative by SUPINF_2:52;

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

A3: F,a are_Re-presentation_of f and

A4: a . 1 = 0 and

A5: for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) by A1, MESFUNC3:14;

deffunc H

consider x being FinSequence of ExtREAL such that

A6: len x = len F and

A7: for n being Nat st n in dom x holds

x . n = H

A8: dom x = Seg (len F) by A6, FINSEQ_1:def 3;

then A9: dom x = dom F by FINSEQ_1:def 3;

take F ; :: thesis: ex a, x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

take a ; :: thesis: ex x being FinSequence of ExtREAL st

( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

take x ; :: thesis: ( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 )

consider sumx being sequence of ExtREAL such that

A10: Sum x = sumx . (len x) and

A11: sumx . 0 = 0 and

A12: for i being Nat st i < len x holds

sumx . (i + 1) = (sumx . i) + (x . (i + 1)) by EXTREAL1:def 2;

defpred S

A13: union (rng F) = {} by A2, A3, MESFUNC3:def 1;

A14: for n being Nat st n in dom F holds

F . n = {}

proof

A16:
for i being Nat st S
let n be Nat; :: thesis: ( n in dom F implies F . n = {} )

assume n in dom F ; :: thesis: F . n = {}

then A15: F . n in rng F by FUNCT_1:3;

assume F . n <> {} ; :: thesis: contradiction

then ex v being object st v in F . n by XBOOLE_0:def 1;

hence contradiction by A13, A15, TARSKI:def 4; :: thesis: verum

end;assume n in dom F ; :: thesis: F . n = {}

then A15: F . n in rng F by FUNCT_1:3;

assume F . n <> {} ; :: thesis: contradiction

then ex v being object st v in F . n by XBOOLE_0:def 1;

hence contradiction by A13, A15, TARSKI:def 4; :: thesis: verum

S

proof

A22:
S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A17: S_{1}[i]
; :: thesis: S_{1}[i + 1]

assume A18: i + 1 <= len x ; :: thesis: sumx . (i + 1) = 0

reconsider i = i as Element of NAT by ORDINAL1:def 12;

i < len x by A18, NAT_1:13;

then A19: sumx . (i + 1) = (sumx . i) + (x . (i + 1)) by A12;

1 <= i + 1 by NAT_1:11;

then A20: i + 1 in dom x by A18, FINSEQ_3:25;

then F . (i + 1) = {} by A9, A14;

then M . (F . (i + 1)) = 0 by VALUED_0:def 19;

then A21: (M * F) . (i + 1) = 0 by A9, A20, FUNCT_1:13;

x . (i + 1) = (a . (i + 1)) * ((M * F) . (i + 1)) by A7, A20

.= 0 by A21 ;

hence sumx . (i + 1) = 0 by A17, A18, A19, NAT_1:13; :: thesis: verum

end;assume A17: S

assume A18: i + 1 <= len x ; :: thesis: sumx . (i + 1) = 0

reconsider i = i as Element of NAT by ORDINAL1:def 12;

i < len x by A18, NAT_1:13;

then A19: sumx . (i + 1) = (sumx . i) + (x . (i + 1)) by A12;

1 <= i + 1 by NAT_1:11;

then A20: i + 1 in dom x by A18, FINSEQ_3:25;

then F . (i + 1) = {} by A9, A14;

then M . (F . (i + 1)) = 0 by VALUED_0:def 19;

then A21: (M * F) . (i + 1) = 0 by A9, A20, FUNCT_1:13;

x . (i + 1) = (a . (i + 1)) * ((M * F) . (i + 1)) by A7, A20

.= 0 by A21 ;

hence sumx . (i + 1) = 0 by A17, A18, A19, NAT_1:13; :: thesis: verum

for i being Nat holds S

hence ( F,a are_Re-presentation_of f & a . 1 = 0 & ( for n being Nat st 2 <= n & n in dom a holds

( 0 < a . n & a . n < +infty ) ) & dom x = dom F & ( for n being Nat st n in dom x holds

x . n = (a . n) * ((M * F) . n) ) & Sum x = 0 ) by A3, A4, A5, A7, A8, A10, FINSEQ_1:def 3; :: thesis: verum