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

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let A be Element of S; :: thesis: ( ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 implies integral+ (M,(f | A)) = 0 )

assume that

A1: ex E being Element of S st

( E = dom f & f is E -measurable ) and

A2: f is nonnegative and

A3: M . A = 0 ; :: thesis: integral+ (M,(f | A)) = 0

consider F0 being Functional_Sequence of X,ExtREAL, K0 being ExtREAL_sequence such that

A4: for n being Nat holds

( F0 . n is_simple_func_in S & dom (F0 . n) = dom f ) and

A5: for n being Nat holds F0 . n is nonnegative and

A6: for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F0 . n) . x <= (F0 . m) . x and

A7: for x being Element of X st x in dom f holds

( F0 # x is convergent & lim (F0 # x) = f . x ) and

for n being Nat holds K0 . n = integral' (M,(F0 . n)) and

K0 is convergent and

integral+ (M,f) = lim K0 by A1, A2, Def15;

deffunc H_{1}( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | A;

consider FA being Functional_Sequence of X,ExtREAL such that

A8: for n being Nat holds FA . n = H_{1}(n)
from SEQFUNC:sch 1();

consider E being Element of S such that

A9: E = dom f and

A10: f is E -measurable by A1;

set C = E /\ A;

A11: f | A is nonnegative by A2, Th15;

A12: (dom f) /\ (E /\ A) = E /\ A by A9, XBOOLE_1:17, XBOOLE_1:28;

then A13: dom (f | (E /\ A)) = E /\ A by RELAT_1:61;

then A14: dom (f | (E /\ A)) = dom (f | A) by A9, RELAT_1:61;

for x being object st x in dom (f | A) holds

(f | A) . x = (f | (E /\ A)) . x

f is E /\ A -measurable by A10, MESFUNC1:30, XBOOLE_1:17;

then A17: f | A is E /\ A -measurable by A12, A16, Th42;

A18: for n being Nat holds FA . n is nonnegative_{2}( Nat) -> Element of ExtREAL = integral' (M,(FA . $1));

consider KA being ExtREAL_sequence such that

A19: for n being Element of NAT holds KA . n = H_{2}(n)
from FUNCT_2:sch 4();

A23: E /\ A = dom (f | A) by A9, RELAT_1:61;

A24: for n being Nat holds

( FA . n is_simple_func_in S & dom (FA . n) = dom (f | A) )

( FA # x is convergent & lim (FA # x) = (f | A) . x )

for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x

hence integral+ (M,(f | A)) = 0 by A17, A20, A23, A11, A24, A18, A30, A25, A22, Def15; :: thesis: verum

for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f being PartFunc of X,ExtREAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL

for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 holds

integral+ (M,(f | A)) = 0

let A be Element of S; :: thesis: ( ex E being Element of S st

( E = dom f & f is E -measurable ) & f is nonnegative & M . A = 0 implies integral+ (M,(f | A)) = 0 )

assume that

A1: ex E being Element of S st

( E = dom f & f is E -measurable ) and

A2: f is nonnegative and

A3: M . A = 0 ; :: thesis: integral+ (M,(f | A)) = 0

consider F0 being Functional_Sequence of X,ExtREAL, K0 being ExtREAL_sequence such that

A4: for n being Nat holds

( F0 . n is_simple_func_in S & dom (F0 . n) = dom f ) and

A5: for n being Nat holds F0 . n is nonnegative and

A6: for n, m being Nat st n <= m holds

for x being Element of X st x in dom f holds

(F0 . n) . x <= (F0 . m) . x and

A7: for x being Element of X st x in dom f holds

( F0 # x is convergent & lim (F0 # x) = f . x ) and

for n being Nat holds K0 . n = integral' (M,(F0 . n)) and

K0 is convergent and

integral+ (M,f) = lim K0 by A1, A2, Def15;

deffunc H

consider FA being Functional_Sequence of X,ExtREAL such that

A8: for n being Nat holds FA . n = H

consider E being Element of S such that

A9: E = dom f and

A10: f is E -measurable by A1;

set C = E /\ A;

A11: f | A is nonnegative by A2, Th15;

A12: (dom f) /\ (E /\ A) = E /\ A by A9, XBOOLE_1:17, XBOOLE_1:28;

then A13: dom (f | (E /\ A)) = E /\ A by RELAT_1:61;

then A14: dom (f | (E /\ A)) = dom (f | A) by A9, RELAT_1:61;

for x being object st x in dom (f | A) holds

(f | A) . x = (f | (E /\ A)) . x

proof

then A16:
f | A = f | (E /\ A)
by A9, A13, FUNCT_1:2, RELAT_1:61;
let x be object ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | (E /\ A)) . x )

assume A15: x in dom (f | A) ; :: thesis: (f | A) . x = (f | (E /\ A)) . x

then (f | A) . x = f . x by FUNCT_1:47;

hence (f | A) . x = (f | (E /\ A)) . x by A14, A15, FUNCT_1:47; :: thesis: verum

end;assume A15: x in dom (f | A) ; :: thesis: (f | A) . x = (f | (E /\ A)) . x

then (f | A) . x = f . x by FUNCT_1:47;

hence (f | A) . x = (f | (E /\ A)) . x by A14, A15, FUNCT_1:47; :: thesis: verum

f is E /\ A -measurable by A10, MESFUNC1:30, XBOOLE_1:17;

then A17: f | A is E /\ A -measurable by A12, A16, Th42;

A18: for n being Nat holds FA . n is nonnegative

proof

deffunc H
let n be Nat; :: thesis: FA . n is nonnegative

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

(F0 . n) | A is nonnegative by A5, Th15;

hence FA . n is nonnegative by A8; :: thesis: verum

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

(F0 . n) | A is nonnegative by A5, Th15;

hence FA . n is nonnegative by A8; :: thesis: verum

consider KA being ExtREAL_sequence such that

A19: for n being Element of NAT holds KA . n = H

A20: now :: thesis: for n being Nat holds KA . n = H_{2}(n)

A21:
for n being Nat holds KA . n = 0
let n be Nat; :: thesis: KA . n = H_{2}(n)

n in NAT by ORDINAL1:def 12;

hence KA . n = H_{2}(n)
by A19; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence KA . n = H

proof

then A22:
lim KA = 0
by Th60;
let n be Nat; :: thesis: KA . n = 0

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

F0 . n is_simple_func_in S by A4;

then integral' (M,((F0 . n) | A)) = 0 by A3, A5, Th73;

then integral' (M,(FA . n)) = 0 by A8;

hence KA . n = 0 by A20; :: thesis: verum

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

F0 . n is_simple_func_in S by A4;

then integral' (M,((F0 . n) | A)) = 0 by A3, A5, Th73;

then integral' (M,(FA . n)) = 0 by A8;

hence KA . n = 0 by A20; :: thesis: verum

A23: E /\ A = dom (f | A) by A9, RELAT_1:61;

A24: for n being Nat holds

( FA . n is_simple_func_in S & dom (FA . n) = dom (f | A) )

proof

A25:
for x being Element of X st x in dom (f | A) holds
let n be Nat; :: thesis: ( FA . n is_simple_func_in S & dom (FA . n) = dom (f | A) )

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

FA . n1 = (F0 . n1) | A by A8;

hence FA . n is_simple_func_in S by A4, Th34; :: thesis: dom (FA . n) = dom (f | A)

dom (FA . n1) = dom ((F0 . n1) | A) by A8;

then dom (FA . n) = (dom (F0 . n)) /\ A by RELAT_1:61;

hence dom (FA . n) = dom (f | A) by A9, A4, A23; :: thesis: verum

end;reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

FA . n1 = (F0 . n1) | A by A8;

hence FA . n is_simple_func_in S by A4, Th34; :: thesis: dom (FA . n) = dom (f | A)

dom (FA . n1) = dom ((F0 . n1) | A) by A8;

then dom (FA . n) = (dom (F0 . n)) /\ A by RELAT_1:61;

hence dom (FA . n) = dom (f | A) by A9, A4, A23; :: thesis: verum

( FA # x is convergent & lim (FA # x) = (f | A) . x )

proof

A30:
for n, m being Nat st n <= m holds
let x be Element of X; :: thesis: ( x in dom (f | A) implies ( FA # x is convergent & lim (FA # x) = (f | A) . x ) )

assume A26: x in dom (f | A) ; :: thesis: ( FA # x is convergent & lim (FA # x) = (f | A) . x )

x in (dom f) /\ A by A26, RELAT_1:61;

then A29: x in dom f by XBOOLE_0:def 4;

then lim (F0 # x) = f . x by A7;

hence ( FA # x is convergent & lim (FA # x) = (f | A) . x ) by A7, A26, A29, A28, FUNCT_1:47; :: thesis: verum

end;assume A26: x in dom (f | A) ; :: thesis: ( FA # x is convergent & lim (FA # x) = (f | A) . x )

now :: thesis: for n being Element of NAT holds (FA # x) . n = (F0 # x) . n

then A28:
FA # x = F0 # x
by FUNCT_2:63;let n be Element of NAT ; :: thesis: (FA # x) . n = (F0 # x) . n

A27: dom ((F0 . n) | A) = dom (FA . n) by A8

.= dom (f | A) by A24 ;

thus (FA # x) . n = (FA . n) . x by Def13

.= ((F0 . n) | A) . x by A8

.= (F0 . n) . x by A26, A27, FUNCT_1:47

.= (F0 # x) . n by Def13 ; :: thesis: verum

end;A27: dom ((F0 . n) | A) = dom (FA . n) by A8

.= dom (f | A) by A24 ;

thus (FA # x) . n = (FA . n) . x by Def13

.= ((F0 . n) | A) . x by A8

.= (F0 . n) . x by A26, A27, FUNCT_1:47

.= (F0 # x) . n by Def13 ; :: thesis: verum

x in (dom f) /\ A by A26, RELAT_1:61;

then A29: x in dom f by XBOOLE_0:def 4;

then lim (F0 # x) = f . x by A7;

hence ( FA # x is convergent & lim (FA # x) = (f | A) . x ) by A7, A26, A29, A28, FUNCT_1:47; :: thesis: verum

for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x

proof

KA is convergent
by A21, Th60;
let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x )

assume A31: n <= m ; :: thesis: for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x

let x be Element of X; :: thesis: ( x in dom (f | A) implies (FA . n) . x <= (FA . m) . x )

reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;

assume A32: x in dom (f | A) ; :: thesis: (FA . n) . x <= (FA . m) . x

then x in (dom f) /\ A by RELAT_1:61;

then A33: x in dom f by XBOOLE_0:def 4;

dom ((F0 . m) | A) = dom (FA . m) by A8;

then A34: dom ((F0 . m) | A) = dom (f | A) by A24;

(FA . m) . x = ((F0 . m) | A) . x by A8;

then A35: (FA . m) . x = (F0 . m) . x by A32, A34, FUNCT_1:47;

dom ((F0 . n) | A) = dom (FA . n) by A8;

then A36: dom ((F0 . n) | A) = dom (f | A) by A24;

(FA . n) . x = ((F0 . n) | A) . x by A8;

then (FA . n) . x = (F0 . n) . x by A32, A36, FUNCT_1:47;

hence (FA . n) . x <= (FA . m) . x by A6, A31, A33, A35; :: thesis: verum

end;(FA . n) . x <= (FA . m) . x )

assume A31: n <= m ; :: thesis: for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x

let x be Element of X; :: thesis: ( x in dom (f | A) implies (FA . n) . x <= (FA . m) . x )

reconsider n = n, m = m as Element of NAT by ORDINAL1:def 12;

assume A32: x in dom (f | A) ; :: thesis: (FA . n) . x <= (FA . m) . x

then x in (dom f) /\ A by RELAT_1:61;

then A33: x in dom f by XBOOLE_0:def 4;

dom ((F0 . m) | A) = dom (FA . m) by A8;

then A34: dom ((F0 . m) | A) = dom (f | A) by A24;

(FA . m) . x = ((F0 . m) | A) . x by A8;

then A35: (FA . m) . x = (F0 . m) . x by A32, A34, FUNCT_1:47;

dom ((F0 . n) | A) = dom (FA . n) by A8;

then A36: dom ((F0 . n) | A) = dom (f | A) by A24;

(FA . n) . x = ((F0 . n) | A) . x by A8;

then (FA . n) . x = (F0 . n) . x by A32, A36, FUNCT_1:47;

hence (FA . n) . x <= (FA . m) . x by A6, A31, A33, A35; :: thesis: verum

hence integral+ (M,(f | A)) = 0 by A17, A20, A23, A11, A24, A18, A30, A25, A22, Def15; :: thesis: verum