let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL ; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis:
set A = dom f;
set g = f | ((dom f) /\ (eq_dom f,(R_EAL 0 )));
A3: f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) is_simple_func_in S

proof

A4: f is real-valued by A1, MESFUNC2:def 5;
ex G being Finite_Sep_Sequence of S st
( dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) = union (rng G) & ( for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y ) )

proof

consider F being Finite_Sep_Sequence of S such that
A8: ( dom f = union (rng F) & ( for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) by A1, MESFUNC2:def 5;
deffunc H₁( Nat) -> Element of bool X = (F . $1) /\ ((dom f) /\ (eq_dom f,(R_EAL 0 )));
reconsider A = dom f as Element of S by A8, MESFUNC2:34;
f is_measurable_on A by A1, MESFUNC2:37;
then A /\ (less_dom f,(R_EAL 0 )) in S by MESFUNC1:def 17;
then A \ (A /\ (less_dom f,(R_EAL 0 ))) in S by PROB_1:44;
then reconsider A1 = A /\ (great_eq_dom f,0. ) as Element of S by MESFUNC1:18;
f is_measurable_on A1 by A1, MESFUNC2:37;
then (A /\ (great_eq_dom f,(R_EAL 0 ))) /\ (less_eq_dom f,(R_EAL 0 )) in S by MESFUNC1:32;
then reconsider A2 = A /\ (eq_dom f,(R_EAL 0 )) as Element of S by MESFUNC1:22;
consider G being FinSequence such that
A9: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A10: dom G = Seg (len F) by A9, FINSEQ_1:def 3;
dom G = Seg (len F) by A9, FINSEQ_1:def 3;
then A11: dom G = dom F by FINSEQ_1:def 3;
dom F = Seg (len F) by FINSEQ_1:def 3;
then for i being Nat st i in dom F holds
G . i = (F . i) /\ A2 by A9, A10;
then reconsider G = G as Finite_Sep_Sequence of S by A11, Th41;
take G ; :: thesis:
for i being Nat st i in dom G holds
G . i = A2 /\ (F . i) by A9;
then A12: union (rng G) = A2 /\ (dom f) by A8, A11, MESFUNC3:6
.= dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) by RELAT_1:90 ;
for i being Nat
for x, y being Element of X st i in dom G & x in G . i & y in G . i holds
(f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y

proof

let i be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume A13: ( i in dom G & x in G . i & y in G . i ) ; :: thesis:
then G . i = (F . i) /\ A2 by A9;
then A14: ( x in F . i & y in F . i ) by A13, XBOOLE_0:def 4;
G . i in rng G by A13, FUNCT_1:12;
then ( x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) & y in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) ) by A12, A13, TARSKI:def 4;
then ( (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = f . x & (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y = f . y ) by FUNCT_1:70;
hence (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y by A8, A11, A13, A14; :: thesis:

end;

hence ( dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) = union (rng G) & ( for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y ) ) by A12; :: thesis:

end;

hence f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) is_simple_func_in S by A4, MESFUNC2:def 5; :: thesis:

end;

A15: for x being set st x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) holds
0 <= (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x

proof

let x be set ; :: thesis:
assume A16: x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) ; :: thesis:
0 <= f . x by A2, SUPINF_2:70;
hence 0 <= (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x by A16, FUNCT_1:70; :: thesis:

end;

for x being set st x in eq_dom f,(R_EAL 0 ) holds
x in dom f by MESFUNC1:def 16;
then eq_dom f,(R_EAL 0 ) c= dom f by TARSKI:def 3;
then A17: f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) = f | (eq_dom f,(R_EAL 0 )) by XBOOLE_1:28;

now

assume A18: dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) <> {} ; :: thesis:
then consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A19: ( F,a are_Re-presentation_of f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) & 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) ) & integral X,S,M,(f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) = Sum x ) by A3, A15, MESFUNC3:def 2;
A20: for x being set st x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) holds
(f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = 0

proof

let x be set ; :: thesis:
assume A21: x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) ; :: thesis:
then x in (dom f) /\ ((dom f) /\ (eq_dom f,(R_EAL 0 ))) by RELAT_1:90;
then ( x in dom f & x in (dom f) /\ (eq_dom f,(R_EAL 0 )) ) by XBOOLE_0:def 4;
then x in eq_dom f,(R_EAL 0 ) by XBOOLE_0:def 4;
then 0 = f . x by MESFUNC1:def 16;
hence (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = 0 by A21, FUNCT_1:70; :: thesis:

end;

A22: for n being Nat holds
( not n in dom F or a . n = 0 or F . n = {} )

proof

let n be Nat; :: thesis:
assume A23: n in dom F ; :: thesis:

now

assume F . n <> {} ; :: thesis:
then consider x being set such that
A24: x in F . n by XBOOLE_0:def 1;
F . n in rng F by A23, FUNCT_1:12;
then x in union (rng F) by A24, TARSKI:def 4;
then x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) by A19, MESFUNC3:def 1;
then (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = 0 by A20;
hence ( a . n = 0 or F . n = {} ) by A19, A23, A24, MESFUNC3:def 1; :: thesis:

end;

hence ( a . n = 0 or F . n = {} ) ; :: thesis:

end;

A25: for n being Nat st n in dom x holds
x . n = 0

proof

let n be Nat; :: thesis:
assume A26: n in dom x ; :: thesis:

per cases by A19, A22, A26;

suppose a . n = 0 ; :: thesis:

then (a . n) * ((M * F) . n) = 0 ;
hence x . n = 0 by A19, A26; :: thesis:

end;

suppose F . n = {} ; :: thesis:

then M . (F . n) = 0 by VALUED_0:def 19;
then (M * F) . n = 0 by A19, A26, FUNCT_1:23;
then (a . n) * ((M * F) . n) = 0 ;
hence x . n = 0 by A19, A26; :: thesis:

end;

Sum x = 0

proof

consider sumx being Function of NAT ,ExtREAL such that
A27: ( Sum x = sumx . (len x) & sumx . 0 = 0 & ( for i being Element of NAT st i < len x holds
sumx . (i + 1) = (sumx . i) + (x . (i + 1)) ) ) by CONVFUN1:def 5;

now

assume x <> {} ; :: thesis:
defpred S₁[ Nat] means ( $1 <= len x implies sumx . $1 = 0 );
A28: S₁[ 0 ] by A27;
A29: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A30: S₁[k] ; :: thesis:
assume A31: k + 1 <= len x ; :: thesis:
reconsider k = k as Element of NAT by ORDINAL1:def 13;
k < len x by A31, NAT_1:13;
then A32: sumx . (k + 1) = (sumx . k) + (x . (k + 1)) by A27;
1 <= k + 1 by NAT_1:11;
then k + 1 in Seg (len x) by A31;
then k + 1 in dom x by FINSEQ_1:def 3;
then x . (k + 1) = 0 by A25;
hence sumx . (k + 1) = 0 by A30, A31, A32, NAT_1:13; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A28, A29);
hence Sum x = 0 by A27; :: thesis:

end;

hence Sum x = 0 by A27, CARD_1:47; :: thesis:

end;

hence integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0 by A17, A18, A19, Def14; :: thesis:

end;

hence integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0 by A17, Def14; :: thesis: