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,ExtREAL
for A, B being Element of S st dom f = A \/ B & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st dom f = A \/ B & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A, B being Element of S st dom f = A \/ B & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let f be PartFunc of X,ExtREAL; :: thesis: for A, B being Element of S st dom f = A \/ B & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) holds
Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let A, B be Element of S; :: thesis: ( dom f = A \/ B & f is A \/ B -measurable & A misses B & ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) implies Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
assume that
A1: dom f = A \/ B and
A2: f is A \/ B -measurable and
A3: A misses B and
A4: ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
A5: Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16;
A6: ( max+ f is A \/ B -measurable & max- f is A \/ B -measurable ) by A1, A2, MESFUNC2:25, MESFUNC2:26;
A7: ( A \/ B = dom (max+ f) & A \/ B = dom (max- f) ) by A1, MESFUNC2:def 2, MESFUNC2:def 3;
then A8: ( integral+ (M,(max+ f)) >= 0 & integral+ (M,(max- f)) >= 0 ) by A6, MESFUNC5:79, MESFUN11:5;
A9: ( (max+ f) | A is nonnegative & (max+ f) | B is nonnegative & (max- f) | A is nonnegative & (max- f) | B is nonnegative ) by MESFUNC5:15, MESFUN11:5;
A10: ( dom ((max+ f) | A) = (dom (max+ f)) /\ A & dom ((max+ f) | B) = (dom (max+ f)) /\ B & dom ((max- f) | A) = (dom (max- f)) /\ A & dom ((max- f) | B) = (dom (max- f)) /\ B ) by RELAT_1:61;
A11: ( max+ f is A -measurable & max+ f is B -measurable & max- f is A -measurable & max- f is B -measurable ) by A6, XBOOLE_1:7, MESFUNC1:30;
( A = (A \/ B) /\ A & B = (A \/ B) /\ B ) by XBOOLE_1:21;
then A12: ( integral+ (M,((max+ f) | A)) >= 0 & integral+ (M,((max+ f) | B)) >= 0 & integral+ (M,((max- f) | A)) >= 0 & integral+ (M,((max- f) | B)) >= 0 ) by A9, A10, A7, A11, MESFUNC5:42, MESFUNC5:79;
A13: ( integral+ (M,((max+ f) | (A \/ B))) = (integral+ (M,((max+ f) | A))) + (integral+ (M,((max+ f) | B))) & integral+ (M,((max- f) | (A \/ B))) = (integral+ (M,((max- f) | A))) + (integral+ (M,((max- f) | B))) ) by A3, A6, A7, MESFUNC5:81, MESFUN11:5;
A14: Integral (M,(f | A)) = (integral+ (M,(max+ (f | A)))) - (integral+ (M,(max- (f | A)))) by MESFUNC5:def 16
.= (integral+ (M,((max+ f) | A))) - (integral+ (M,(max- (f | A)))) by MESFUNC5:28
.= (integral+ (M,((max+ f) | A))) - (integral+ (M,((max- f) | A))) by MESFUNC5:28 ;
A15: Integral (M,(f | B)) = (integral+ (M,(max+ (f | B)))) - (integral+ (M,(max- (f | B)))) by MESFUNC5:def 16
.= (integral+ (M,((max+ f) | B))) - (integral+ (M,(max- (f | B)))) by MESFUNC5:28
.= (integral+ (M,((max+ f) | B))) - (integral+ (M,((max- f) | B))) by MESFUNC5:28 ;
A16: ( integral+ (M,(max+ f)) < +infty implies ( integral+ (M,((max+ f) | A)) in REAL & integral+ (M,((max+ f) | B)) in REAL ) )

proof

assume integral+ (M,(max+ f)) < +infty ; :: thesis: ( integral+ (M,((max+ f) | A)) in REAL & integral+ (M,((max+ f) | B)) in REAL )
then A17: integral+ (M,(max+ f)) in REAL by A8, XXREAL_0:14;

now :: thesis: not integral+ (M,((max+ f) | A)) = +infty

assume A18: integral+ (M,((max+ f) | A)) = +infty ; :: thesis: contradiction
( integral+ (M,((max+ f) | B)) in REAL or integral+ (M,((max+ f) | B)) = +infty ) by A12, XXREAL_0:14;
hence contradiction by A13, A17, A18, A7; :: thesis: verum

end;

hence integral+ (M,((max+ f) | A)) in REAL by A12, XXREAL_0:14; :: thesis: integral+ (M,((max+ f) | B)) in REAL

now :: thesis: not integral+ (M,((max+ f) | B)) = +infty

assume A19: integral+ (M,((max+ f) | B)) = +infty ; :: thesis: contradiction
( integral+ (M,((max+ f) | A)) in REAL or integral+ (M,((max+ f) | A)) = +infty ) by A12, XXREAL_0:14;
hence contradiction by A13, A17, A19, A7; :: thesis: verum

end;

hence integral+ (M,((max+ f) | B)) in REAL by A12, XXREAL_0:14; :: thesis: verum

end;

A20: ( integral+ (M,(max- f)) < +infty implies ( integral+ (M,((max- f) | A)) in REAL & integral+ (M,((max- f) | B)) in REAL ) )

proof

assume integral+ (M,(max- f)) < +infty ; :: thesis: ( integral+ (M,((max- f) | A)) in REAL & integral+ (M,((max- f) | B)) in REAL )
then A21: integral+ (M,(max- f)) in REAL by A8, XXREAL_0:14;

now :: thesis: not integral+ (M,((max- f) | A)) = +infty

assume A22: integral+ (M,((max- f) | A)) = +infty ; :: thesis: contradiction
( integral+ (M,((max- f) | B)) in REAL or integral+ (M,((max- f) | B)) = +infty ) by A12, XXREAL_0:14;
hence contradiction by A13, A21, A22, A7; :: thesis: verum

end;

hence integral+ (M,((max- f) | A)) in REAL by A12, XXREAL_0:14; :: thesis: integral+ (M,((max- f) | B)) in REAL

now :: thesis: not integral+ (M,((max- f) | B)) = +infty

assume A23: integral+ (M,((max- f) | B)) = +infty ; :: thesis: contradiction
( integral+ (M,((max- f) | A)) in REAL or integral+ (M,((max- f) | A)) = +infty ) by A12, XXREAL_0:14;
hence contradiction by A13, A21, A23, A7; :: thesis: verum

end;

hence integral+ (M,((max- f) | B)) in REAL by A12, XXREAL_0:14; :: thesis: verum

end;

per cases ( integral+ (M,(max+ f)) < +infty or integral+ (M,(max- f)) < +infty ) by A4;

suppose A24: integral+ (M,(max+ f)) < +infty ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

then integral+ (M,(max+ f)) in REAL by A8, XXREAL_0:14;
then reconsider IP = integral+ (M,(max+ f)) as Real ;
reconsider IPA = integral+ (M,((max+ f) | A)), IPB = integral+ (M,((max+ f) | B)) as Real by A24, A16;

per cases ( integral+ (M,(max- f)) = +infty or integral+ (M,(max- f)) in REAL ) by A8, XXREAL_0:14;

suppose A25: integral+ (M,(max- f)) = +infty ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

then A26: Integral (M,f) = -infty by A24, A5, XXREAL_3:13;
( integral+ (M,((max- f) | A)) = +infty or integral+ (M,((max- f) | B)) = +infty ) by A13, A7, A25, XXREAL_3:16;
then A27: ( Integral (M,(f | A)) = -infty or Integral (M,(f | B)) = -infty ) by A14, A15, A24, A16, XXREAL_3:13;
( Integral (M,(f | A)) <> +infty & Integral (M,(f | B)) <> +infty ) by A24, A16, A12, A14, A15, XXREAL_3:18;
hence Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A26, A27, XXREAL_3:def 2; :: thesis: verum

end;

suppose A28: integral+ (M,(max- f)) in REAL ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

then reconsider IM = integral+ (M,(max- f)) as Real ;
A29: - (integral+ (M,(max- f))) = - IM by XXREAL_3:def 3;
A30: Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16
.= (integral+ (M,(max+ f))) + (- (integral+ (M,(max- f)))) by XXREAL_3:def 4
.= IP + (- IM) by A29, XXREAL_3:def 2 ;
integral+ (M,((max- f) | A)) <> +infty by A28, A13, A7, A12, XXREAL_3:def 2;
then integral+ (M,((max- f) | A)) in REAL by A12, XXREAL_0:14;
then reconsider IMA = integral+ (M,((max- f) | A)) as Real ;
integral+ (M,((max- f) | B)) <> +infty by A28, A13, A7, A12, XXREAL_3:def 2;
then integral+ (M,((max- f) | B)) in REAL by A12, XXREAL_0:14;
then reconsider IMB = integral+ (M,((max- f) | B)) as Real ;
A31: ( IP = IPA + IPB & IM = IMA + IMB ) by A13, A7, XXREAL_3:def 2;
A32: ( - (integral+ (M,((max- f) | A))) = - IMA & - (integral+ (M,((max- f) | B))) = - IMB ) by XXREAL_3:def 3;
A33: Integral (M,(f | A)) = (integral+ (M,((max+ f) | A))) + (- (integral+ (M,((max- f) | A)))) by A14, XXREAL_3:def 4
.= IPA + (- IMA) by A32, XXREAL_3:def 2 ;
Integral (M,(f | B)) = (integral+ (M,((max+ f) | B))) + (- (integral+ (M,((max- f) | B)))) by A15, XXREAL_3:def 4
.= IPB + (- IMB) by A32, XXREAL_3:def 2 ;
then (Integral (M,(f | A))) + (Integral (M,(f | B))) = (IPA - IMA) + (IPB - IMB) by A33, XXREAL_3:def 2;
hence Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A30, A31; :: thesis: verum

end;

end;

end;

suppose A34: integral+ (M,(max- f)) < +infty ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

then integral+ (M,(max- f)) in REAL by A8, XXREAL_0:14;
then reconsider IP = integral+ (M,(max- f)) as Real ;
reconsider IPA = integral+ (M,((max- f) | A)), IPB = integral+ (M,((max- f) | B)) as Real by A34, A20;

per cases ( integral+ (M,(max+ f)) = +infty or integral+ (M,(max+ f)) in REAL ) by A8, XXREAL_0:14;

suppose A35: integral+ (M,(max+ f)) = +infty ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

then A36: Integral (M,f) = +infty by A5, A34, XXREAL_3:13;
( integral+ (M,((max+ f) | A)) = +infty or integral+ (M,((max+ f) | B)) = +infty ) by A13, A7, A35, XXREAL_3:16;
then A37: ( Integral (M,(f | A)) = +infty or Integral (M,(f | B)) = +infty ) by A14, A15, A34, A20, XXREAL_3:13;
( Integral (M,(f | A)) <> -infty & Integral (M,(f | B)) <> -infty ) by A34, A20, A12, A14, A15, XXREAL_3:19;
hence Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A36, A37, XXREAL_3:def 2; :: thesis: verum

end;

suppose A38: integral+ (M,(max+ f)) in REAL ; :: thesis: Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B)))

then reconsider IM = integral+ (M,(max+ f)) as Real ;
A39: - (integral+ (M,(max- f))) = - IP by XXREAL_3:def 3;
A40: Integral (M,f) = (integral+ (M,(max+ f))) - (integral+ (M,(max- f))) by MESFUNC5:def 16
.= (integral+ (M,(max+ f))) + (- (integral+ (M,(max- f)))) by XXREAL_3:def 4
.= IM + (- IP) by A39, XXREAL_3:def 2 ;
integral+ (M,((max+ f) | A)) <> +infty by A38, A13, A7, A12, XXREAL_3:def 2;
then integral+ (M,((max+ f) | A)) in REAL by A12, XXREAL_0:14;
then reconsider IMA = integral+ (M,((max+ f) | A)) as Real ;
integral+ (M,((max+ f) | B)) <> +infty by A38, A13, A7, A12, XXREAL_3:def 2;
then integral+ (M,((max+ f) | B)) in REAL by A12, XXREAL_0:14;
then reconsider IMB = integral+ (M,((max+ f) | B)) as Real ;
A41: ( IP = IPA + IPB & IM = IMA + IMB ) by A13, A7, XXREAL_3:def 2;
A42: ( - (integral+ (M,((max- f) | A))) = - IPA & - (integral+ (M,((max- f) | B))) = - IPB ) by XXREAL_3:def 3;
A43: Integral (M,(f | A)) = (integral+ (M,((max+ f) | A))) + (- (integral+ (M,((max- f) | A)))) by A14, XXREAL_3:def 4
.= IMA + (- IPA) by A42, XXREAL_3:def 2 ;
Integral (M,(f | B)) = (integral+ (M,((max+ f) | B))) + (- (integral+ (M,((max- f) | B)))) by A15, XXREAL_3:def 4
.= IMB + (- IPB) by A42, XXREAL_3:def 2 ;
then (Integral (M,(f | A))) + (Integral (M,(f | B))) = (IMA - IPA) + (IMB - IPB) by A43, XXREAL_3:def 2;
hence Integral (M,f) = (Integral (M,(f | A))) + (Integral (M,(f | B))) by A40, A41; :: thesis: verum

end;

end;

end;

end;