let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL holds
( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL holds
( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )
let f be PartFunc of X,ExtREAL; ( f is_integrable_on M iff ( max+ f is_integrable_on M & max- f is_integrable_on M ) )
hereby ( max+ f is_integrable_on M & max- f is_integrable_on M implies f is_integrable_on M )
assume A1:
f is_integrable_on M
;
( max+ f is_integrable_on M & max- f is_integrable_on M )then consider E being
Element of
S such that A2:
(
E = dom f &
f is
E -measurable )
by MESFUNC5:def 17;
A3:
(
integral+ (
M,
(max+ f))
< +infty &
integral+ (
M,
(max- f))
< +infty )
by A1, MESFUNC5:def 17;
A4:
(
E = dom (max+ f) &
E = dom (max- f) )
by A2, MESFUNC2:def 2, MESFUNC2:def 3;
A5:
(
max+ f is
E -measurable &
max- f is
E -measurable )
by A2, MESFUN11:10;
A6:
(
max+ f is
nonnegative &
max- f is
nonnegative )
by MESFUN11:5;
then A7:
(
integral+ (
M,
(max+ (max+ f)))
< +infty &
integral+ (
M,
(max+ (max- f)))
< +infty )
by A3, MESFUN11:31;
(
integral+ (
M,
(max- (max+ f)))
< +infty &
integral+ (
M,
(max- (max- f)))
< +infty )
by A4, A5, A6, MESFUN11:53;
hence
(
max+ f is_integrable_on M &
max- f is_integrable_on M )
by A4, A5, A7, MESFUNC5:def 17;
verum
end;
assume that
A8:
max+ f is_integrable_on M
and
A9:
max- f is_integrable_on M
; f is_integrable_on M
consider E1 being Element of S such that
A10:
( E1 = dom (max+ f) & max+ f is E1 -measurable )
by A8, MESFUNC5:def 17;
consider E2 being Element of S such that
A11:
( E2 = dom (max- f) & max- f is E2 -measurable )
by A9, MESFUNC5:def 17;
A12:
E1 = dom f
by A10, MESFUNC2:def 2;
then
E1 = E2
by A11, MESFUNC2:def 3;
then A13:
f is E1 -measurable
by A10, A11, A12, MESFUN11:10;
( max+ f is nonnegative & max- f is nonnegative )
by MESFUN11:5;
then
( max+ (max+ f) = max+ f & max+ (max- f) = max- f )
by MESFUN11:31;
then
( integral+ (M,(max+ f)) < +infty & integral+ (M,(max- f)) < +infty )
by A8, A9, MESFUNC5:def 17;
hence
f is_integrable_on M
by A12, A13, MESFUNC5:def 17; verum