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 bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is_measurable_on E ) 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 bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is_measurable_on E ) 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 bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is_measurable_on E ) holds
f is_integrable_on M
let f be PartFunc of X,REAL ; :: thesis: ( dom f <> {} & rng f is bounded & M . (dom f) < +infty & ex E being Element of S st
( E = dom f & f is_measurable_on E ) implies f is_integrable_on M )
assume that
A0: ( dom f <> {} & rng f is bounded ) and
A1: M . (dom f) < +infty and
A2: ex E being Element of S st
( E = dom f & f is_measurable_on E ) ; :: thesis: f is_integrable_on M
consider E being Element of S such that
A3: ( E = dom f & f is_measurable_on E ) by A2;
A4: rng (R_EAL f) is non empty Subset of ExtREAL by RELAT_1:65, A0;
B1: R_EAL f is_measurable_on E by A3, MESFUNC6:def 6;
B2: chi E,X is_integrable_on M by A1, A3, MESFUNC7:24;
B4: chi E,X is V44() by MESFUNC2:31;
B51: (dom (R_EAL f)) /\ (dom (chi E,X)) = E /\ X by A3, FUNCT_3:def 3;
(dom (R_EAL f)) /\ (dom (chi E,X)) = E by B51, XBOOLE_1:28;
then B6: ((R_EAL f) (#) (chi E,X)) | E is_integrable_on M by A4, A0, B1, B2, B4, MESFUNC7:17;
B7: dom ((R_EAL f) (#) (chi E,X)) = (dom (R_EAL f)) /\ (dom (chi E,X)) by MESFUNC1:def 5
.= E by B51, XBOOLE_1:28 ;
then B8: dom (((R_EAL f) (#) (chi E,X)) | E) = dom f by A3, RELAT_1:91;

now

let x be set ; :: thesis: ( x in dom f implies (((R_EAL f) (#) (chi E,X)) | E) . x = f . x )
assume AA3: x in dom f ; :: thesis: (((R_EAL f) (#) (chi E,X)) | E) . x = f . x
P02: ((R_EAL f) (#) (chi E,X)) . x = ((R_EAL f) . x) * ((chi E,X) . x) by MESFUNC1:def 5, B7, A3, AA3;
((R_EAL f) (#) (chi E,X)) . x = ((R_EAL f) . x) * (R_EAL 1) by P02, A3, AA3, FUNCT_3:def 3
.= f . x by XXREAL_3:92 ;
hence (((R_EAL f) (#) (chi E,X)) | E) . x = f . x by B7, RELAT_1:97; :: thesis: verum

end;

then ((R_EAL f) (#) (chi E,X)) | E = f by B8, FUNCT_1:9;
hence f is_integrable_on M by B6, MESFUNC6:def 9; :: thesis: verum