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₁( 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₁(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₁[ 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 = {}

proof

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;

A16: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A17: S₁[i] ; :: thesis: S₁[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;

A22: S₁[ 0 ] by A11;
for i being Nat holds S₁[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