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 holds

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

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 holds

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

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 holds

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

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 holds

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

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

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

assume that

A1: ex E being Element of S st

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

A2: f is nonnegative ; :: thesis: 0 <= integral+ (M,(f | A))

consider E being Element of S such that

A3: E = dom f and

A4: f is E -measurable by A1;

set C = E /\ A;

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

A6: dom (f | A) = E /\ A by A3, RELAT_1:61

.= (dom f) /\ (E /\ A) by A3, XBOOLE_1:17, XBOOLE_1:28

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

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

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

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

then f | (E /\ A) is E /\ A -measurable by A9, Th42;

then f | A is E /\ A -measurable by A6, A7, FUNCT_1:2;

hence 0 <= integral+ (M,(f | A)) by A2, A5, Th15, Th79; :: 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 holds

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

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 holds

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

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 holds

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

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 holds

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

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

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

assume that

A1: ex E being Element of S st

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

A2: f is nonnegative ; :: thesis: 0 <= integral+ (M,(f | A))

consider E being Element of S such that

A3: E = dom f and

A4: f is E -measurable by A1;

set C = E /\ A;

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

A6: dom (f | A) = E /\ A by A3, RELAT_1:61

.= (dom f) /\ (E /\ A) by A3, XBOOLE_1:17, XBOOLE_1:28

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

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

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

proof

A9:
(dom f) /\ (E /\ A) = E /\ A
by A3, XBOOLE_1:17, XBOOLE_1:28;
let x be object ; :: thesis: ( x in dom (f | A) implies (f | A) . x = (f | (E /\ A)) . x )

assume A8: 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 A6, A8, FUNCT_1:47; :: thesis: verum

end;assume A8: 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 A6, A8, FUNCT_1:47; :: thesis: verum

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

then f | (E /\ A) is E /\ A -measurable by A9, Th42;

then f | A is E /\ A -measurable by A6, A7, FUNCT_1:2;

hence 0 <= integral+ (M,(f | A)) by A2, A5, Th15, Th79; :: thesis: verum