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 & f is nonnegative holds
integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 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 & f is nonnegative holds
integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & f is nonnegative holds
integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0
let f be PartFunc of X,ExtREAL ; :: thesis: ( f is_simple_func_in S & f is nonnegative implies integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0 )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative ; :: thesis: integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0
set A = dom f;
set g = f | ((dom f) /\ (eq_dom f,(R_EAL 0 )));
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 A3: f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) = f | (eq_dom f,(R_EAL 0 )) by XBOOLE_1:28;
A4: 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
A5: dom f = union (rng F) and
A6: 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 A5, MESFUNC2:34;
consider G being FinSequence such that
A7: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H₁(n) ) ) from FINSEQ_1:sch 2();
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:12;
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;
A8: dom F = Seg (len F) by FINSEQ_1:def 3;
dom G = Seg (len F) by A7, FINSEQ_1:def 3;
then A9: for i being Nat st i in dom F holds
G . i = (F . i) /\ A2 by A7, A8;
dom G = Seg (len F) by A7, FINSEQ_1:def 3;
then A10: dom G = dom F by FINSEQ_1:def 3;
then reconsider G = G as Finite_Sep_Sequence of S by A9, Th41;
take G ; :: thesis: ( 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 ) )
for i being Nat st i in dom G holds
G . i = A2 /\ (F . i) by A7;
then A11: union (rng G) = A2 /\ (dom f) by A5, A10, 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: 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
let x, y be Element of X; :: thesis: ( i in dom G & x in G . i & y in G . i implies (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y )
assume that
A12: i in dom G and
A13: x in G . i and
A14: y in G . i ; :: thesis: (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y
A15: G . i = (F . i) /\ A2 by A7, A12;
then A16: y in F . i by A14, XBOOLE_0:def 4;
A17: G . i in rng G by A12, FUNCT_1:12;
then x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) by A11, A13, TARSKI:def 4;
then A18: (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = f . x by FUNCT_1:70;
y in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) by A11, A14, A17, TARSKI:def 4;
then A19: (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y = f . y by FUNCT_1:70;
x in F . i by A13, A15, XBOOLE_0:def 4;
hence (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . y by A6, A10, A12, A16, A18, A19; :: thesis: verum

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 A11; :: thesis: verum

end;

A20: 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: ( x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) implies 0 <= (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x )
assume A21: x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) ; :: thesis: 0 <= (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x
0 <= f . x by A2, SUPINF_2:70;
hence 0 <= (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x by A21, FUNCT_1:70; :: thesis: verum

end;

f is V61() by A1, MESFUNC2:def 5;
then A22: f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) is_simple_func_in S by A4, MESFUNC2:def 5;

now

consider F being Finite_Sep_Sequence of S, a, x being FinSequence of ExtREAL such that
A23: F,a are_Re-presentation_of f | ((dom f) /\ (eq_dom f,(R_EAL 0 ))) and
a . 1 = 0 and
for n being Nat st 2 <= n & n in dom a holds
( 0 < a . n & a . n < +infty ) and
A24: dom x = dom F and
A25: for n being Nat st n in dom x holds
x . n = (a . n) * ((M * F) . n) and
A26: integral X,S,M,(f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) = Sum x by A22, A20, MESFUNC3:def 2;
A27: 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: ( x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) implies (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = 0 )
assume A28: x in dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) ; :: thesis: (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) . x = 0
then x in (dom f) /\ ((dom f) /\ (eq_dom f,(R_EAL 0 ))) by RELAT_1:90;
then 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 A28, FUNCT_1:70; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( not n in dom F or a . n = 0 or F . n = {} )
assume A30: n in dom F ; :: thesis: ( a . n = 0 or F . n = {} )

now

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

end;

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

end;

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

proof

let n be Nat; :: thesis: ( n in dom x implies x . n = 0 )
assume A33: n in dom x ; :: thesis: x . n = 0

per cases ( a . n = 0 or F . n = {} ) by A24, A29, A33;

suppose a . n = 0 ; :: thesis: x . n = 0

then (a . n) * ((M * F) . n) = 0 ;
hence x . n = 0 by A25, A33; :: thesis: verum

end;

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

then M . (F . n) = 0 by VALUED_0:def 19;
then (M * F) . n = 0 by A24, A33, FUNCT_1:23;
then (a . n) * ((M * F) . n) = 0 ;
hence x . n = 0 by A25, A33; :: thesis: verum

end;

end;

end;

A34: Sum x = 0

proof

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

now

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

proof

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

end;

A42: S₁[ 0 ] by A36;
for i being Nat holds S₁[i] from NAT_1:sch 2(A42, A38);
hence Sum x = 0 by A35; :: thesis: verum

end;

hence Sum x = 0 by A35, A36, CARD_1:47; :: thesis: verum

end;

assume dom (f | ((dom f) /\ (eq_dom f,(R_EAL 0 )))) <> {} ; :: thesis: integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0
hence integral' M,(f | (eq_dom f,(R_EAL 0 ))) = 0 by A3, A26, A34, Def14; :: thesis: verum

end;

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