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);

for x being object st x in dom (f | ((dom f) /\ B)) holds

0 <= (f | ((dom f) /\ B)) . x

A6: 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 ) )

then A22: dom (f | ((dom f) /\ B)) = ((dom f) /\ (dom f)) /\ B by XBOOLE_1:16;

then A23: dom (f | ((dom f) /\ B)) = dom (f | B) by RELAT_1:61;

for x being object st x in dom (f | ((dom f) /\ B)) holds

(f | ((dom f) /\ B)) . x = (f | B) . x

f is real-valued by A1, MESFUNC2:def 4;

then A26: f | ((dom f) /\ B) is_simple_func_in S by A6, MESFUNC2:def 4;

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);

for x being object st x in dom (f | ((dom f) /\ B)) holds

0 <= (f | ((dom f) /\ B)) . x

proof

then a4:
f | ((dom f) /\ B) is nonnegative
by SUPINF_2:52;
let x be object ; :: thesis: ( x in dom (f | ((dom f) /\ B)) implies 0 <= (f | ((dom f) /\ B)) . x )

assume A5: x in dom (f | ((dom f) /\ B)) ; :: thesis: 0 <= (f | ((dom f) /\ B)) . x

0 <= f . x by A3, SUPINF_2:51;

hence 0 <= (f | ((dom f) /\ B)) . x by A5, FUNCT_1:47; :: thesis: verum

end;assume A5: x in dom (f | ((dom f) /\ B)) ; :: thesis: 0 <= (f | ((dom f) /\ B)) . x

0 <= f . x by A3, SUPINF_2:51;

hence 0 <= (f | ((dom f) /\ B)) . x by A5, FUNCT_1:47; :: thesis: verum

A6: 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

dom (f | ((dom f) /\ B)) = (dom f) /\ ((dom f) /\ B)
by RELAT_1:61;
consider F being Finite_Sep_Sequence of S such that

A7: dom f = union (rng F) and

A8: 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 4;

deffunc H_{1}( Nat) -> Element of bool X = (F . $1) /\ ((dom f) /\ B);

reconsider A = dom f as Element of S by A7, MESFUNC2:31;

reconsider A2 = A /\ B as Element of S ;

consider G being FinSequence such that

A9: ( len G = len F & ( for n being Nat st n in dom G holds

G . n = H_{1}(n) ) )
from FINSEQ_1:sch 2();

A10: dom F = Seg (len F) by FINSEQ_1:def 3;

dom G = Seg (len F) by A9, FINSEQ_1:def 3;

then A11: for i being Nat st i in dom F holds

G . i = (F . i) /\ A2 by A9, A10;

dom G = Seg (len F) by A9, FINSEQ_1:def 3;

then A12: dom G = dom F by FINSEQ_1:def 3;

then reconsider G = G as Finite_Sep_Sequence of S by A11, Th35;

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 A9;

then A13: union (rng G) = A2 /\ (dom f) by A7, A12, MESFUNC3:6

.= dom (f | ((dom f) /\ B)) by RELAT_1:61 ;

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

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;A7: dom f = union (rng F) and

A8: 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 4;

deffunc H

reconsider A = dom f as Element of S by A7, MESFUNC2:31;

reconsider A2 = A /\ B as Element of S ;

consider G being FinSequence such that

A9: ( len G = len F & ( for n being Nat st n in dom G holds

G . n = H

A10: dom F = Seg (len F) by FINSEQ_1:def 3;

dom G = Seg (len F) by A9, FINSEQ_1:def 3;

then A11: for i being Nat st i in dom F holds

G . i = (F . i) /\ A2 by A9, A10;

dom G = Seg (len F) by A9, FINSEQ_1:def 3;

then A12: dom G = dom F by FINSEQ_1:def 3;

then reconsider G = G as Finite_Sep_Sequence of S by A11, Th35;

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 A9;

then A13: union (rng G) = A2 /\ (dom f) by A7, A12, MESFUNC3:6

.= dom (f | ((dom f) /\ B)) by RELAT_1:61 ;

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

hence
( dom (f | ((dom f) /\ B)) = union (rng G) & ( for n being Nat
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 that

A14: i in dom G and

A15: x in G . i and

A16: y in G . i ; :: thesis: (f | ((dom f) /\ B)) . x = (f | ((dom f) /\ B)) . y

A17: G . i = (F . i) /\ A2 by A9, A14;

then A18: y in F . i by A16, XBOOLE_0:def 4;

A19: G . i in rng G by A14, FUNCT_1:3;

then x in dom (f | ((dom f) /\ B)) by A13, A15, TARSKI:def 4;

then A20: (f | ((dom f) /\ B)) . x = f . x by FUNCT_1:47;

y in dom (f | ((dom f) /\ B)) by A13, A16, A19, TARSKI:def 4;

then A21: (f | ((dom f) /\ B)) . y = f . y by FUNCT_1:47;

x in F . i by A15, A17, XBOOLE_0:def 4;

hence (f | ((dom f) /\ B)) . x = (f | ((dom f) /\ B)) . y by A8, A12, A14, A18, A20, A21; :: thesis: verum

end;(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 that

A14: i in dom G and

A15: x in G . i and

A16: y in G . i ; :: thesis: (f | ((dom f) /\ B)) . x = (f | ((dom f) /\ B)) . y

A17: G . i = (F . i) /\ A2 by A9, A14;

then A18: y in F . i by A16, XBOOLE_0:def 4;

A19: G . i in rng G by A14, FUNCT_1:3;

then x in dom (f | ((dom f) /\ B)) by A13, A15, TARSKI:def 4;

then A20: (f | ((dom f) /\ B)) . x = f . x by FUNCT_1:47;

y in dom (f | ((dom f) /\ B)) by A13, A16, A19, TARSKI:def 4;

then A21: (f | ((dom f) /\ B)) . y = f . y by FUNCT_1:47;

x in F . i by A15, A17, XBOOLE_0:def 4;

hence (f | ((dom f) /\ B)) . x = (f | ((dom f) /\ B)) . y by A8, A12, A14, A18, A20, A21; :: thesis: verum

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

then A22: dom (f | ((dom f) /\ B)) = ((dom f) /\ (dom f)) /\ B by XBOOLE_1:16;

then A23: dom (f | ((dom f) /\ B)) = dom (f | B) by RELAT_1:61;

for x being object st x in dom (f | ((dom f) /\ B)) holds

(f | ((dom f) /\ B)) . x = (f | B) . x

proof

then A25:
f | ((dom f) /\ B) = f | B
by A23, FUNCT_1:2;
let x be object ; :: thesis: ( x in dom (f | ((dom f) /\ B)) implies (f | ((dom f) /\ B)) . x = (f | B) . x )

assume A24: 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:47;

hence (f | ((dom f) /\ B)) . x = (f | B) . x by A23, A24, FUNCT_1:47; :: thesis: verum

end;assume A24: 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:47;

hence (f | ((dom f) /\ B)) . x = (f | B) . x by A23, A24, FUNCT_1:47; :: thesis: verum

f is real-valued by A1, MESFUNC2:def 4;

then A26: f | ((dom f) /\ B) is_simple_func_in S by A6, MESFUNC2:def 4;

now :: thesis: integral' (M,(f | B)) = 0 end;

hence
integral' (M,(f | B)) = 0
; :: thesis: verumper cases
( dom (f | ((dom f) /\ B)) = {} or dom (f | ((dom f) /\ B)) <> {} )
;

end;

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

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

A28: F,a are_Re-presentation_of f | ((dom f) /\ B) and

a . 1 = 0 and

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

( 0 < a . n & a . n < +infty ) and

A29: dom x = dom F and

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

x . n = (a . n) * ((M * F) . n) and

A31: integral (M,(f | ((dom f) /\ B))) = Sum x by A26, MESFUNC3:def 2, a4;

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

M . (F . n) = 0

x . n = 0

end;A28: F,a are_Re-presentation_of f | ((dom f) /\ B) and

a . 1 = 0 and

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

( 0 < a . n & a . n < +infty ) and

A29: dom x = dom F and

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

x . n = (a . n) * ((M * F) . n) and

A31: integral (M,(f | ((dom f) /\ B))) = Sum x by A26, MESFUNC3:def 2, a4;

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

M . (F . n) = 0

proof

A37:
for n being Nat st n in dom x holds
reconsider BB = B as measure_zero of M by A2, MEASURE1:def 7;

let n be Nat; :: thesis: ( n in dom F implies M . (F . n) = 0 )

A33: dom (f | ((dom f) /\ B)) c= B by A22, XBOOLE_1:17;

assume A34: n in dom F ; :: thesis: M . (F . n) = 0

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

then reconsider FF = F . n as Element of S ;

for v being object st v in F . n holds

v in union (rng F)

union (rng F) = dom (f | ((dom f) /\ B)) by A28, MESFUNC3:def 1;

then FF c= BB by A36, A33;

then F . n is measure_zero of M by MEASURE1:36;

hence M . (F . n) = 0 by MEASURE1:def 7; :: thesis: verum

end;let n be Nat; :: thesis: ( n in dom F implies M . (F . n) = 0 )

A33: dom (f | ((dom f) /\ B)) c= B by A22, XBOOLE_1:17;

assume A34: n in dom F ; :: thesis: M . (F . n) = 0

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

then reconsider FF = F . n as Element of S ;

for v being object st v in F . n holds

v in union (rng F)

proof

then A36:
F . n c= union (rng F)
;
let v be object ; :: thesis: ( v in F . n implies v in union (rng F) )

assume A35: v in F . n ; :: thesis: v in union (rng F)

F . n in rng F by A34, FUNCT_1:3;

hence v in union (rng F) by A35, TARSKI:def 4; :: thesis: verum

end;assume A35: v in F . n ; :: thesis: v in union (rng F)

F . n in rng F by A34, FUNCT_1:3;

hence v in union (rng F) by A35, TARSKI:def 4; :: thesis: verum

union (rng F) = dom (f | ((dom f) /\ B)) by A28, MESFUNC3:def 1;

then FF c= BB by A36, A33;

then F . n is measure_zero of M by MEASURE1:36;

hence M . (F . n) = 0 by MEASURE1:def 7; :: thesis: verum

x . n = 0

proof

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

assume A38: n in dom x ; :: thesis: x . n = 0

then M . (F . n) = 0 by A29, A32;

then (M * F) . n = 0 by A29, A38, FUNCT_1:13;

then (a . n) * ((M * F) . n) = 0 ;

hence x . n = 0 by A30, A38; :: thesis: verum

end;assume A38: n in dom x ; :: thesis: x . n = 0

then M . (F . n) = 0 by A29, A32;

then (M * F) . n = 0 by A29, A38, FUNCT_1:13;

then (a . n) * ((M * F) . n) = 0 ;

hence x . n = 0 by A30, A38; :: thesis: verum

proof

hence
integral' (M,(f | B)) = 0
by A25, A27, A31, Def14; :: thesis: verum
consider sumx being sequence of ExtREAL such that

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

A40: sumx . 0 = 0 and

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

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

end;A39: Sum x = sumx . (len x) and

A40: sumx . 0 = 0 and

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

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

now :: thesis: ( x <> {} implies Sum x = 0 )

hence
Sum x = 0
by A39, A40, CARD_1:27; :: thesis: verumdefpred S_{1}[ Nat] means ( $1 <= len x implies sumx . $1 = 0 );

assume x <> {} ; :: thesis: Sum x = 0

A42: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A40;

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

hence Sum x = 0 by A39; :: thesis: verum

end;assume x <> {} ; :: thesis: Sum x = 0

A42: for k being Nat st S

S

proof

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

assume A43: S_{1}[k]
; :: thesis: S_{1}[k + 1]

assume A44: k + 1 <= len x ; :: thesis: sumx . (k + 1) = 0

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

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len x) by A44;

then k + 1 in dom x by FINSEQ_1:def 3;

then A45: x . (k + 1) = 0 by A37;

k < len x by A44, NAT_1:13;

then sumx . (k + 1) = (sumx . k) + (x . (k + 1)) by A41;

hence sumx . (k + 1) = 0 by A43, A44, A45, NAT_1:13; :: thesis: verum

end;assume A43: S

assume A44: k + 1 <= len x ; :: thesis: sumx . (k + 1) = 0

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

1 <= k + 1 by NAT_1:11;

then k + 1 in Seg (len x) by A44;

then k + 1 in dom x by FINSEQ_1:def 3;

then A45: x . (k + 1) = 0 by A37;

k < len x by A44, NAT_1:13;

then sumx . (k + 1) = (sumx . k) + (x . (k + 1)) by A41;

hence sumx . (k + 1) = 0 by A43, A44, A45, NAT_1:13; :: thesis: verum

for i being Nat holds S

hence Sum x = 0 by A39; :: thesis: verum