let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for B being Element of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & M . B = 0 & f is nonnegative holds
integral' M,(f | B) = 0
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for B being Element of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & M . B = 0 & f is nonnegative holds
integral' M,(f | B) = 0
let M be sigma_Measure of S; :: thesis: for B being Element of S
for f being PartFunc of X,ExtREAL st f is_simple_func_in S & M . B = 0 & f is nonnegative holds
integral' M,(f | B) = 0
let B be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S & M . B = 0 & f is nonnegative holds
integral' M,(f | B) = 0
let f be PartFunc of X,ExtREAL ; :: thesis: ( f is_simple_func_in S & M . B = 0 & f is nonnegative implies integral' M,(f | B) = 0 )
assume that
A1: f is_simple_func_in S and
A2: M . B = 0 and
A3: f is nonnegative ; :: thesis: integral' M,(f | B) = 0
set A = dom f;
set g = f | ((dom f) /\ B);
A4: f | ((dom f) /\ B) is_simple_func_in S

proof

A5: f is real-valued by A1, MESFUNC2:def 5;
ex G being Finite_Sep_Sequence of S st
( dom (f | ((dom f) /\ B)) = 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) /\ B)) . x = (f | ((dom f) /\ B)) . y ) )

proof

consider F being Finite_Sep_Sequence of S such that
A9: ( 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) /\ B);
reconsider A = dom f as Element of S by A9, MESFUNC2:34;
reconsider A2 = A /\ B as Element of S ;
consider G being FinSequence such that
A10: ( len G = len F & ( for n being Nat st n in dom G holds
G . n = H₁(n) ) ) from FINSEQ_1:sch 2();
A11: dom G = Seg (len F) by A10, FINSEQ_1:def 3;
dom G = Seg (len F) by A10, FINSEQ_1:def 3;
then A12: 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 A10, A11;
then reconsider G = G as Finite_Sep_Sequence of S by A12, Th41;
take G ; :: thesis: ( dom (f | ((dom f) /\ B)) = 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) /\ B)) . x = (f | ((dom f) /\ B)) . y ) )
for i being Nat st i in dom G holds
G . i = A2 /\ (F . i) by A10;
then A13: union (rng G) = A2 /\ (dom f) by A9, A12, MESFUNC3:6
.= dom (f | ((dom f) /\ B)) 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) /\ B)) . x = (f | ((dom f) /\ B)) . 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) /\ B)) . x = (f | ((dom f) /\ B)) . 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) /\ B)) . x = (f | ((dom f) /\ B)) . y )
assume A14: ( i in dom G & x in G . i & y in G . i ) ; :: thesis: (f | ((dom f) /\ B)) . x = (f | ((dom f) /\ B)) . y
then G . i = (F . i) /\ A2 by A10;
then A15: ( x in F . i & y in F . i ) by A14, XBOOLE_0:def 4;
G . i in rng G by A14, FUNCT_1:12;
then ( x in dom (f | ((dom f) /\ B)) & y in dom (f | ((dom f) /\ B)) ) by A13, A14, TARSKI:def 4;
then ( (f | ((dom f) /\ B)) . x = f . x & (f | ((dom f) /\ B)) . y = f . y ) by FUNCT_1:70;
hence (f | ((dom f) /\ B)) . x = (f | ((dom f) /\ B)) . y by A9, A12, A14, A15; :: thesis: verum

end;

hence ( dom (f | ((dom f) /\ B)) = 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) /\ B)) . x = (f | ((dom f) /\ B)) . y ) ) by A13; :: thesis: verum

end;

hence f | ((dom f) /\ B) is_simple_func_in S by A5, MESFUNC2:def 5; :: thesis: verum

end;

A16: for x being set st x in dom (f | ((dom f) /\ B)) holds
0 <= (f | ((dom f) /\ B)) . x

proof

let x be set ; :: thesis: ( x in dom (f | ((dom f) /\ B)) implies 0 <= (f | ((dom f) /\ B)) . x )
assume A17: x in dom (f | ((dom f) /\ B)) ; :: thesis: 0 <= (f | ((dom f) /\ B)) . x
0 <= f . x by A3, SUPINF_2:70;
hence 0 <= (f | ((dom f) /\ B)) . x by A17, FUNCT_1:70; :: thesis: verum

end;

dom (f | ((dom f) /\ B)) = (dom f) /\ ((dom f) /\ B) by RELAT_1:90;
then A18: dom (f | ((dom f) /\ B)) = ((dom f) /\ (dom f)) /\ B by XBOOLE_1:16;
then A19: dom (f | ((dom f) /\ B)) = dom (f | B) by RELAT_1:90;
for x being set st x in dom (f | ((dom f) /\ B)) holds
(f | ((dom f) /\ B)) . x = (f | B) . x

proof

let x be set ; :: thesis: ( x in dom (f | ((dom f) /\ B)) implies (f | ((dom f) /\ B)) . x = (f | B) . x )
assume A20: x in dom (f | ((dom f) /\ B)) ; :: thesis: (f | ((dom f) /\ B)) . x = (f | B) . x
then (f | ((dom f) /\ B)) . x = f . x by FUNCT_1:70;
hence (f | ((dom f) /\ B)) . x = (f | B) . x by A19, A20, FUNCT_1:70; :: thesis: verum

end;

then A21: f | ((dom f) /\ B) = f | B by A19, FUNCT_1:9;

now

per cases ( dom (f | ((dom f) /\ B)) = {} or dom (f | ((dom f) /\ B)) <> {} ) ;

suppose dom (f | ((dom f) /\ B)) = {} ; :: thesis: integral' M,(f | B) = 0

hence integral' M,(f | B) = 0 by A19, Def14; :: thesis: verum

end;

suppose A22: dom (f | ((dom f) /\ B)) <> {} ; :: thesis: integral' M,(f | B) = 0

then 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) /\ B) & 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) /\ B)) = Sum x ) by A4, A16, MESFUNC3:def 2;
A24: for n being Nat st n in dom F holds
M . (F . n) = 0

proof

let n be Nat; :: thesis: ( n in dom F implies M . (F . n) = 0 )
assume A25: n in dom F ; :: thesis: M . (F . n) = 0
reconsider BB = B as measure_zero of M by A2, MEASURE1:def 13;
A26: union (rng F) = dom (f | ((dom f) /\ B)) by A23, MESFUNC3:def 1;
A27: F . n c= union (rng F)

proof

for v being set st v in F . n holds
v in union (rng F)

proof

let v be set ; :: thesis: ( v in F . n implies v in union (rng F) )
assume A28: v in F . n ; :: thesis: v in union (rng F)
F . n in rng F by A25, FUNCT_1:12;
hence v in union (rng F) by A28, TARSKI:def 4; :: thesis: verum

end;

hence F . n c= union (rng F) by TARSKI:def 3; :: thesis: verum

end;

( F . n in rng F & rng F c= S ) by A25, FUNCT_1:12;
then reconsider FF = F . n as Element of S ;
dom (f | ((dom f) /\ B)) c= B by A18, XBOOLE_1:17;
then FF c= BB by A26, A27, XBOOLE_1:1;
then F . n is measure_zero of M by MEASURE1:69;
hence M . (F . n) = 0 by MEASURE1:def 13; :: thesis: verum

end;

A29: 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 A30: n in dom x ; :: thesis: x . n = 0
then M . (F . n) = 0 by A23, A24;
then (M * F) . n = 0 by A23, A30, FUNCT_1:23;
then (a . n) * ((M * F) . n) = 0 ;
hence x . n = 0 by A23, A30; :: thesis: verum

end;

Sum x = 0

proof

consider sumx being Function of NAT ,ExtREAL such that
A31: ( 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: Sum x = 0
defpred S₁[ Nat] means ( $1 <= len x implies sumx . $1 = 0 );
A32: S₁[ 0 ] by A31;
A33: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A32, A33);
hence Sum x = 0 by A31; :: thesis: verum

end;

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

end;

hence integral' M,(f | B) = 0 by A21, A22, A23, Def14; :: thesis: verum

end;

end;

end;

hence integral' M,(f | B) = 0 ; :: thesis: verum