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,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,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,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,0)))) = 0 )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative ; :: thesis: integral' (M,(f | (eq_dom (f,0)))) = 0

set A = dom f;

set g = f | ((dom f) /\ (eq_dom (f,0)));

for x being object st x in eq_dom (f,0) holds

x in dom f by MESFUNC1:def 15;

then eq_dom (f,0) c= dom f ;

then A3: f | ((dom f) /\ (eq_dom (f,0))) = f | (eq_dom (f,0)) by XBOOLE_1:28;

A4: ex G being Finite_Sep_Sequence of S st

( dom (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) )

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

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

then A22: f | ((dom f) /\ (eq_dom (f,0))) is_simple_func_in S by A4, MESFUNC2:def 4;

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,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,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,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,0)))) = 0 )

assume that

A1: f is_simple_func_in S and

A2: f is nonnegative ; :: thesis: integral' (M,(f | (eq_dom (f,0)))) = 0

set A = dom f;

set g = f | ((dom f) /\ (eq_dom (f,0)));

for x being object st x in eq_dom (f,0) holds

x in dom f by MESFUNC1:def 15;

then eq_dom (f,0) c= dom f ;

then A3: f | ((dom f) /\ (eq_dom (f,0))) = f | (eq_dom (f,0)) by XBOOLE_1:28;

A4: ex G being Finite_Sep_Sequence of S st

( dom (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) )

proof

for x being object st x in dom (f | ((dom f) /\ (eq_dom (f,0)))) holds
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 4;

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

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

consider G being FinSequence such that

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

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

f is A -measurable by A1, MESFUNC2:34;

then A /\ (less_dom (f,0)) in S by MESFUNC1:def 16;

then A \ (A /\ (less_dom (f,0))) in S by PROB_1:6;

then reconsider A1 = A /\ (great_eq_dom (f,0.)) as Element of S by MESFUNC1:14;

f is A1 -measurable by A1, MESFUNC2:34;

then (A /\ (great_eq_dom (f,0))) /\ (less_eq_dom (f,0)) in S by MESFUNC1:28;

then reconsider A2 = A /\ (eq_dom (f,0)) as Element of S by MESFUNC1:18;

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, Th35;

take G ; :: thesis: ( dom (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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,0)))) 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) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . 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) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) ) by A11; :: thesis: verum

end;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 4;

deffunc H

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

consider G being FinSequence such that

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

G . n = H

f is A -measurable by A1, MESFUNC2:34;

then A /\ (less_dom (f,0)) in S by MESFUNC1:def 16;

then A \ (A /\ (less_dom (f,0))) in S by PROB_1:6;

then reconsider A1 = A /\ (great_eq_dom (f,0.)) as Element of S by MESFUNC1:14;

f is A1 -measurable by A1, MESFUNC2:34;

then (A /\ (great_eq_dom (f,0))) /\ (less_eq_dom (f,0)) in S by MESFUNC1:28;

then reconsider A2 = A /\ (eq_dom (f,0)) as Element of S by MESFUNC1:18;

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, Th35;

take G ; :: thesis: ( dom (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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,0)))) 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) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y

proof

hence
( dom (f | ((dom f) /\ (eq_dom (f,0)))) = 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) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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:3;

then x in dom (f | ((dom f) /\ (eq_dom (f,0)))) by A11, A13, TARSKI:def 4;

then A18: (f | ((dom f) /\ (eq_dom (f,0)))) . x = f . x by FUNCT_1:47;

y in dom (f | ((dom f) /\ (eq_dom (f,0)))) by A11, A14, A17, TARSKI:def 4;

then A19: (f | ((dom f) /\ (eq_dom (f,0)))) . y = f . y by FUNCT_1:47;

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

hence (f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y by A6, A10, A12, A16, A18, A19; :: thesis: verum

end;(f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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,0)))) . x = (f | ((dom f) /\ (eq_dom (f,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:3;

then x in dom (f | ((dom f) /\ (eq_dom (f,0)))) by A11, A13, TARSKI:def 4;

then A18: (f | ((dom f) /\ (eq_dom (f,0)))) . x = f . x by FUNCT_1:47;

y in dom (f | ((dom f) /\ (eq_dom (f,0)))) by A11, A14, A17, TARSKI:def 4;

then A19: (f | ((dom f) /\ (eq_dom (f,0)))) . y = f . y by FUNCT_1:47;

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

hence (f | ((dom f) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y by A6, A10, A12, A16, A18, A19; :: 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) /\ (eq_dom (f,0)))) . x = (f | ((dom f) /\ (eq_dom (f,0)))) . y ) ) by A11; :: thesis: verum

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

proof

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

assume A21: x in dom (f | ((dom f) /\ (eq_dom (f,0)))) ; :: thesis: 0 <= (f | ((dom f) /\ (eq_dom (f,0)))) . x

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

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

end;assume A21: x in dom (f | ((dom f) /\ (eq_dom (f,0)))) ; :: thesis: 0 <= (f | ((dom f) /\ (eq_dom (f,0)))) . x

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

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

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

then A22: f | ((dom f) /\ (eq_dom (f,0))) is_simple_func_in S by A4, MESFUNC2:def 4;

now :: thesis: ( dom (f | ((dom f) /\ (eq_dom (f,0)))) <> {} implies integral' (M,(f | (eq_dom (f,0)))) = 0 )

hence
integral' (M,(f | (eq_dom (f,0)))) = 0
by A3, Def14; :: thesis: verumconsider 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,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 (M,(f | ((dom f) /\ (eq_dom (f,0))))) = Sum x by a2, A22, MESFUNC3:def 2;

A27: for x being set st x in dom (f | ((dom f) /\ (eq_dom (f,0)))) holds

(f | ((dom f) /\ (eq_dom (f,0)))) . x = 0

( not n in dom F or a . n = 0 or F . n = {} )

x . n = 0

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

end;A23: F,a are_Re-presentation_of f | ((dom f) /\ (eq_dom (f,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 (M,(f | ((dom f) /\ (eq_dom (f,0))))) = Sum x by a2, A22, MESFUNC3:def 2;

A27: for x being set st x in dom (f | ((dom f) /\ (eq_dom (f,0)))) holds

(f | ((dom f) /\ (eq_dom (f,0)))) . x = 0

proof

A29:
for n being Nat holds
let x be set ; :: thesis: ( x in dom (f | ((dom f) /\ (eq_dom (f,0)))) implies (f | ((dom f) /\ (eq_dom (f,0)))) . x = 0 )

assume A28: x in dom (f | ((dom f) /\ (eq_dom (f,0)))) ; :: thesis: (f | ((dom f) /\ (eq_dom (f,0)))) . x = 0

then x in (dom f) /\ ((dom f) /\ (eq_dom (f,0))) by RELAT_1:61;

then x in (dom f) /\ (eq_dom (f,0)) by XBOOLE_0:def 4;

then x in eq_dom (f,0) by XBOOLE_0:def 4;

then 0 = f . x by MESFUNC1:def 15;

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

end;assume A28: x in dom (f | ((dom f) /\ (eq_dom (f,0)))) ; :: thesis: (f | ((dom f) /\ (eq_dom (f,0)))) . x = 0

then x in (dom f) /\ ((dom f) /\ (eq_dom (f,0))) by RELAT_1:61;

then x in (dom f) /\ (eq_dom (f,0)) by XBOOLE_0:def 4;

then x in eq_dom (f,0) by XBOOLE_0:def 4;

then 0 = f . x by MESFUNC1:def 15;

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

( not n in dom F or a . n = 0 or F . n = {} )

proof

A32:
for n being Nat st n in dom x holds
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 = {} )

end;assume A30: n in dom F ; :: thesis: ( a . n = 0 or F . n = {} )

now :: thesis: ( not F . n <> {} or a . n = 0 or F . n = {} )

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

then consider x being object such that

A31: x in F . n by XBOOLE_0:def 1;

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

then x in union (rng F) by A31, TARSKI:def 4;

then x in dom (f | ((dom f) /\ (eq_dom (f,0)))) by A23, MESFUNC3:def 1;

then (f | ((dom f) /\ (eq_dom (f,0)))) . x = 0 by A27;

hence ( a . n = 0 or F . n = {} ) by A23, A30, A31, MESFUNC3:def 1; :: thesis: verum

end;then consider x being object such that

A31: x in F . n by XBOOLE_0:def 1;

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

then x in union (rng F) by A31, TARSKI:def 4;

then x in dom (f | ((dom f) /\ (eq_dom (f,0)))) by A23, MESFUNC3:def 1;

then (f | ((dom f) /\ (eq_dom (f,0)))) . x = 0 by A27;

hence ( a . n = 0 or F . n = {} ) by A23, A30, A31, MESFUNC3:def 1; :: thesis: verum

x . n = 0

proof

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

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

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

proof

assume
dom (f | ((dom f) /\ (eq_dom (f,0)))) <> {}
; :: thesis: integral' (M,(f | (eq_dom (f,0)))) = 0
consider sumx being sequence of ExtREAL such that

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

A36: sumx . 0 = 0 and

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

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

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

A36: sumx . 0 = 0 and

A37: 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 A35, A36, CARD_1:27; :: thesis: verumdefpred S_{1}[ Nat] means ( $1 <= len x implies sumx . $1 = 0 );

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

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

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

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

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

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

A38: for k being Nat st S

S

proof

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

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

assume A40: 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 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;assume A39: S

assume A40: 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 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

for i being Nat holds S

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

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