let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & 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 E being Element of S
for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & f is E -measurable holds
f is_integrable_on M
let M be sigma_Measure of S; :: thesis: for E being Element of S
for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & f is E -measurable holds
f is_integrable_on M
let E be Element of S; :: thesis: for f being PartFunc of X,REAL st E = dom f & M . E < +infty & f is bounded & f is E -measurable holds
f is_integrable_on M
let f be PartFunc of X,REAL; :: thesis: ( E = dom f & M . E < +infty & f is bounded & f is E -measurable implies f is_integrable_on M )
assume that
A1: E = dom f and
A2: M . E < +infty and
A3: f is bounded and
A4: f is E -measurable ; :: thesis: f is_integrable_on M
A5: E = dom (R_EAL f) by A1, MESFUNC5:def 7;
A6: R_EAL f is E -measurable by A4, MESFUNC6:def 1;
A7: rng f is real-bounded by A3, INTEGRA1:15;

per cases ( E <> {} or E = {} ) ;

suppose E <> {} ; :: thesis: f is_integrable_on M

then A8: rng f <> {} by A1, RELAT_1:42;
then reconsider LB = inf (rng f) as Real by A7;
reconsider UB = sup (rng f) as Real by A7, A8;
set r = max (|.LB.|,|.UB.|);
reconsider g = chi (E,X) as PartFunc of X,ExtREAL by RELSET_1:7, NUMBERS:31;
dom g = X by FUNCT_3:def 3;
then A9: dom ((max (|.LB.|,|.UB.|)) (#) g) = X by MESFUNC1:def 6;
g is_integrable_on M by A2, MESFUNC7:24;
then (max (|.LB.|,|.UB.|)) (#) g is_integrable_on M by MESFUNC5:110;
then A10: ((max (|.LB.|,|.UB.|)) (#) g) | E is_integrable_on M by MESFUNC5:112;
A11: dom (((max (|.LB.|,|.UB.|)) (#) g) | E) = (dom ((max (|.LB.|,|.UB.|)) (#) g)) /\ E by RELAT_1:61
.= (dom g) /\ E by MESFUNC1:def 6
.= X /\ E by FUNCT_3:def 3
.= E by XBOOLE_1:28 ;
for x being Element of X st x in dom (R_EAL f) holds
|.((R_EAL f) . x).| <= (((max (|.LB.|,|.UB.|)) (#) g) | E) . x

proof

let x be Element of X; :: thesis: ( x in dom (R_EAL f) implies |.((R_EAL f) . x).| <= (((max (|.LB.|,|.UB.|)) (#) g) | E) . x )
assume A12: x in dom (R_EAL f) ; :: thesis: |.((R_EAL f) . x).| <= (((max (|.LB.|,|.UB.|)) (#) g) | E) . x
then x in dom f by MESFUNC5:def 7;
then A13: ( LB <= f . x & f . x <= UB ) by XXREAL_2:3, XXREAL_2:4, FUNCT_1:3;
A14: ( max (|.LB.|,|.UB.|) >= |.UB.| & max (|.LB.|,|.UB.|) >= |.LB.| & - (max (|.LB.|,|.UB.|)) <= - |.LB.| ) by XXREAL_0:25, XREAL_1:24;
A15: R_EAL f = f by MESFUNC5:def 7;
( - |.LB.| <= LB & UB <= |.UB.| ) by ABSVALUE:4;
then ( - |.LB.| <= f . x & f . x <= |.UB.| ) by A13, XXREAL_0:2;
then ( - (max (|.LB.|,|.UB.|)) <= f . x & f . x <= max (|.LB.|,|.UB.|) ) by A14, XXREAL_0:2;
then A16: |.(f . x).| <= max (|.LB.|,|.UB.|) by ABSVALUE:5;
A17: g . x = 1 by A12, A5, FUNCT_3:def 3;
(((max (|.LB.|,|.UB.|)) (#) g) | E) . x = ((max (|.LB.|,|.UB.|)) (#) g) . x by A12, A11, A5, FUNCT_1:47
.= (max (|.LB.|,|.UB.|)) * (g . x) by A9, MESFUNC1:def 6
.= (max (|.LB.|,|.UB.|)) * 1 by A17, XXREAL_3:def 5 ;
hence |.((R_EAL f) . x).| <= (((max (|.LB.|,|.UB.|)) (#) g) | E) . x by A16, A15, EXTREAL1:12; :: thesis: verum

end;

then R_EAL f is_integrable_on M by A6, A5, A10, A11, MESFUNC5:102;
hence f is_integrable_on M by MESFUNC6:def 4; :: thesis: verum

end;

suppose A18: E = {} ; :: thesis: f is_integrable_on M

A19: ( dom (max+ (R_EAL f)) = E & dom (max- (R_EAL f)) = E ) by A5, MESFUNC2:def 2, MESFUNC2:def 3;
for x being Element of X st x in dom (max+ (R_EAL f)) holds
(max+ (R_EAL f)) . x = 0 by A18, A5, MESFUNC2:def 2;
then A20: integral+ (M,(max+ (R_EAL f))) = 0 by A19, A6, MESFUNC2:25, MESFUNC5:87;
for x being Element of X st x in dom (max- (R_EAL f)) holds
(max- (R_EAL f)) . x = 0 by A18, A5, MESFUNC2:def 3;
then integral+ (M,(max- (R_EAL f))) = 0 by A19, A6, A5, MESFUNC2:26, MESFUNC5:87;
hence f is_integrable_on M by A6, A5, A20, MESFUNC5:def 17, MESFUNC6:def 4; :: thesis: verum

end;

end;