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,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is E -measurable ) holds
f is_integrable_on M
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is E -measurable ) holds
f is_integrable_on M
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,REAL st dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is E -measurable ) holds
f is_integrable_on M
let f be PartFunc of X,REAL; :: thesis: ( dom f <> {} & rng f is real-bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is E -measurable ) implies f is_integrable_on M )
assume that
A1: dom f <> {} and
A2: rng f is real-bounded and
A3: M . (dom f) < +infty and
A4: ex E being Element of S st
( E = dom f & f is E -measurable ) ; :: thesis: f is_integrable_on M
consider E being Element of S such that
A5: E = dom f and
A6: f is E -measurable by A4;
A7: (dom (R_EAL f)) /\ (dom (chi (E,X))) = E /\ X by A5, FUNCT_3:def 3;
then A8: ( chi (E,X) is real-valued & (dom (R_EAL f)) /\ (dom (chi (E,X))) = E ) by MESFUNC2:28, XBOOLE_1:28;
A9: dom ((R_EAL f) (#) (chi (E,X))) = (dom (R_EAL f)) /\ (dom (chi (E,X))) by MESFUNC1:def 5
.= E by A7, XBOOLE_1:28 ;

A10: now :: thesis: for x being object st x in dom f holds
(((R_EAL f) (#) (chi (E,X))) | E) . x = f . x

let x be object ; :: thesis: ( x in dom f implies (((R_EAL f) (#) (chi (E,X))) | E) . x = f . x )
assume A11: x in dom f ; :: thesis: (((R_EAL f) (#) (chi (E,X))) | E) . x = f . x
then ((R_EAL f) (#) (chi (E,X))) . x = ((R_EAL f) . x) * ((chi (E,X)) . x) by A5, A9, MESFUNC1:def 5;
then ((R_EAL f) (#) (chi (E,X))) . x = ((R_EAL f) . x) * 1 by A5, A11, FUNCT_3:def 3
.= f . x by XXREAL_3:81 ;
hence (((R_EAL f) (#) (chi (E,X))) | E) . x = f . x by A9; :: thesis: verum

end;

A12: R_EAL f is E -measurable by A6;
A13: rng (R_EAL f) is non empty Subset of ExtREAL by A1, RELAT_1:42;
dom (((R_EAL f) (#) (chi (E,X))) | E) = dom f by A5, A9;
then A14: ((R_EAL f) (#) (chi (E,X))) | E = f by A10, FUNCT_1:2;
chi (E,X) is_integrable_on M by A3, A5, MESFUNC7:24;
then ((R_EAL f) (#) (chi (E,X))) | E is_integrable_on M by A2, A13, A12, A8, MESFUNC7:17;
hence f is_integrable_on M by A14; :: thesis: verum