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;

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 = {} )
;

end;

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

hence f is_integrable_on M by MESFUNC6:def 4; :: thesis: verum

end;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

then
R_EAL f is_integrable_on M
by A6, A5, A10, A11, MESFUNC5:102;
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;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

hence f is_integrable_on M by MESFUNC6:def 4; :: thesis: verum

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;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