let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f be PartFunc of X,ExtREAL ; :: thesis:
let A, B be Element of S; :: thesis:
assume A1: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B ) ; :: thesis:
then consider E being Element of S such that
A2: E = dom f and
A3: f is_measurable_on E ;
set C = E /\ (A \/ B);
A4: dom (f | (A \/ B)) = E /\ (A \/ B) by A2, RELAT_1:90;
A5: E /\ (A \/ B) = (dom f) /\ (E /\ (A \/ B)) by A2, XBOOLE_1:17, XBOOLE_1:28;
then A6: dom (f | (A \/ B)) = dom (f | (E /\ (A \/ B))) by A4, RELAT_1:90;
for x being set st x in dom (f | (A \/ B)) holds
(f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x

proof

let x be set ; :: thesis:
assume A7: x in dom (f | (A \/ B)) ; :: thesis:
then (f | (A \/ B)) . x = f . x by FUNCT_1:70;
hence (f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x by A6, A7, FUNCT_1:70; :: thesis:

end;

then A8: f | (A \/ B) = f | (E /\ (A \/ B)) by A6, FUNCT_1:9;
f is_measurable_on E /\ (A \/ B) by A3, MESFUNC1:34, XBOOLE_1:17;
then A9: f | (A \/ B) is_measurable_on E /\ (A \/ B) by A5, A8, Th48;
A10: f | (A \/ B) is nonnegative by A1, Th21;
consider F0 being Functional_Sequence of X,ExtREAL , K0 being ExtREAL_sequence such that
A11: ( ( for n being Nat holds
( F0 . n is_simple_func_in S & dom (F0 . n) = dom f ) ) & ( for n being Nat holds F0 . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom f holds
(F0 . n) . x <= (F0 . m) . x ) & ( for x being Element of X st x in dom f holds
( F0 # x is convergent & lim (F0 # x) = f . x ) ) & ( for n being Nat holds K0 . n = integral' M,(F0 . n) ) & K0 is convergent & integral+ M,f = lim K0 ) by A1, Def15;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | (A \/ B);
consider FAB being Functional_Sequence of X,ExtREAL such that
A12: for n being Nat holds FAB . n = H₁(n) from SEQFUNC:sch 1();
deffunc H₂( Nat) -> Element of ExtREAL = integral' M,(FAB . $1);
consider KAB being ExtREAL_sequence such that
A13: for n being Element of NAT holds KAB . n = H₂(n) from FUNCT_2:sch 4();

A14: now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence KAB . n = H₂(n) by A13; :: thesis:

end;

A15: ( ( for n being Nat holds
( FAB . n is_simple_func_in S & dom (FAB . n) = dom (f | (A \/ B)) ) ) & ( for n being Nat
for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x = (F0 . n) . x ) & ( for n being Nat holds FAB . n is nonnegative ) & ( for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x <= (FAB . m) . x ) & ( for x being Element of X st x in dom (f | (A \/ B)) holds
( FAB # x is convergent & lim (FAB # x) = (f | (A \/ B)) . x ) ) )

proof

hereby :: thesis:

let n be Nat; :: thesis:
A17: FAB . n = (F0 . n) | (A \/ B) by A12;
F0 . n is_simple_func_in S by A11;
hence FAB . n is_simple_func_in S by A17, Th40; :: thesis:
thus dom (FAB . n) = dom ((F0 . n) | (A \/ B)) by A12
.= (dom (F0 . n)) /\ (A \/ B) by RELAT_1:90
.= (dom f) /\ (A \/ B) by A11
.= dom (f | (A \/ B)) by RELAT_1:90 ; :: thesis:

end;

hereby :: thesis:

let n be Nat; :: thesis:
let x be Element of X; :: thesis:
assume x in dom (f | (A \/ B)) ; :: thesis:
then A19: x in dom (FAB . n) by A16;
FAB . n = (F0 . n) | (A \/ B) by A12;
hence (FAB . n) . x = (F0 . n) . x by A19, FUNCT_1:70; :: thesis:

end;

hereby :: thesis:

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
F0 . n is nonnegative by A11;
then (F0 . n1) | (A \/ B) is nonnegative by Th21;
hence FAB . n is nonnegative by A12; :: thesis:

end;

hereby :: thesis:

let n, m be Nat; :: thesis:
assume A20: n <= m ; :: thesis:

now

let x be Element of X; :: thesis:
assume A21: x in dom (f | (A \/ B)) ; :: thesis:
then x in (dom f) /\ (A \/ B) by RELAT_1:90;
then A22: x in dom f by XBOOLE_0:def 4;
( (FAB . n) . x = (F0 . n) . x & (FAB . m) . x = (F0 . m) . x ) by A18, A21;
hence (FAB . n) . x <= (FAB . m) . x by A11, A20, A22; :: thesis:

end;

hence for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x <= (FAB . m) . x ; :: thesis:

end;

hereby :: thesis:

let x be Element of X; :: thesis:
assume A23: x in dom (f | (A \/ B)) ; :: thesis:
then x in (dom f) /\ (A \/ B) by RELAT_1:90;
then A24: x in dom f by XBOOLE_0:def 4;

A25: now

let n be Element of NAT ; :: thesis:
thus (FAB # x) . n = (FAB . n) . x by Def13
.= (F0 . n) . x by A18, A23
.= (F0 # x) . n by Def13 ; :: thesis:

end;

then FAB # x = F0 # x by FUNCT_2:113;
hence FAB # x is convergent by A11, A24; :: thesis:
thus lim (FAB # x) = lim (F0 # x) by A25, FUNCT_2:113
.= f . x by A11, A24
.= (f | (A \/ B)) . x by A23, FUNCT_1:70 ; :: thesis:

end;

for n, m being Nat st n <= m holds
KAB . n <= KAB . m

proof

let n, m be Nat; :: thesis:
assume A26: n <= m ; :: thesis:
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
A27: ( FAB . n is_simple_func_in S & FAB . m is_simple_func_in S & dom (FAB . n) = dom (f | (A \/ B)) & dom (FAB . m) = dom (f | (A \/ B)) & FAB . n is nonnegative & FAB . m is nonnegative ) by A15;
A28: KAB . m = integral' M,(FAB . m) by A14;
A29: for x being set st x in dom ((FAB . m) - (FAB . n)) holds
(FAB . n) . x <= (FAB . m) . x

proof

let x be set ; :: thesis:
assume x in dom ((FAB . m) - (FAB . n)) ; :: thesis:
then x in ((dom (FAB . m)) /\ (dom (FAB . n))) \ ((((FAB . m) " {+infty }) /\ ((FAB . n) " {+infty })) \/ (((FAB . m) " {-infty }) /\ ((FAB . n) " {-infty }))) by MESFUNC1:def 4;
then x in (dom (FAB . m)) /\ (dom (FAB . n)) by XBOOLE_0:def 5;
hence (FAB . n) . x <= (FAB . m) . x by A15, A26, A27; :: thesis:

end;

then A30: integral' M,((FAB . n) | (dom ((FAB . m) - (FAB . n)))) <= integral' M,((FAB . m) | (dom ((FAB . m) - (FAB . n)))) by A27, Th76;
dom ((FAB . m) - (FAB . n)) = (dom (FAB . m)) /\ (dom (FAB . n)) by A27, A29, Th75;
then ( (FAB . m) | (dom ((FAB . m) - (FAB . n))) = FAB . m & (FAB . n) | (dom ((FAB . m) - (FAB . n))) = FAB . n ) by A27, GRFUNC_1:64;
hence KAB . n <= KAB . m by A14, A28, A30; :: thesis:

end;

then KAB is convergent by Th60;
then A31: integral+ M,(f | (A \/ B)) = lim KAB by A4, A9, A10, A14, A15, Def15;
set DA = E /\ A;
set DB = E /\ B;
A32: ( f is_measurable_on E /\ A & f is_measurable_on E /\ B ) by A3, MESFUNC1:34, XBOOLE_1:17;
A33: ( E /\ A = dom (f | A) & E /\ B = dom (f | B) ) by A2, RELAT_1:90;
then A34: ( (dom f) /\ (E /\ A) = E /\ A & (dom f) /\ (E /\ B) = E /\ B ) by RELAT_1:89, XBOOLE_1:28;
then A35: ( dom (f | (E /\ A)) = dom (f | A) & dom (f | (E /\ B)) = dom (f | B) ) by A33, RELAT_1:90;
for x being set st x in dom (f | (E /\ A)) holds
(f | (E /\ A)) . x = (f | A) . x

proof

let x be set ; :: thesis:
assume A36: x in dom (f | (E /\ A)) ; :: thesis:
then (f | A) . x = f . x by A35, FUNCT_1:70;
hence (f | (E /\ A)) . x = (f | A) . x by A36, FUNCT_1:70; :: thesis:

end;

proof

let x be set ; :: thesis:
assume A38: x in dom (f | (E /\ B)) ; :: thesis:
then (f | B) . x = f . x by A35, FUNCT_1:70;
hence (f | (E /\ B)) . x = (f | B) . x by A38, FUNCT_1:70; :: thesis:

end;

then f | (E /\ B) = f | B by A34, A33, FUNCT_1:9, RELAT_1:90;
then A39: f | B is_measurable_on E /\ B by A32, A34, Th48;
A40: ( f | A is nonnegative & f | B is nonnegative ) by A1, Th21;
deffunc H₃( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | A;
consider FA being Functional_Sequence of X,ExtREAL such that
A41: for n being Nat holds FA . n = H₃(n) from SEQFUNC:sch 1();
deffunc H₄( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | B;
consider FB being Functional_Sequence of X,ExtREAL such that
A42: for n being Nat holds FB . n = H₄(n) from SEQFUNC:sch 1();
A43: for n being Nat holds
( FA . n is_simple_func_in S & FB . n is_simple_func_in S & dom (FA . n) = dom (f | A) & dom (FB . n) = dom (f | B) )

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A44: ( F0 . n is_simple_func_in S & F0 . n is nonnegative ) by A11;
A45: ( FA . n1 = (F0 . n1) | A & FB . n1 = (F0 . n1) | B ) by A41, A42;
hence ( FA . n is_simple_func_in S & FB . n is_simple_func_in S ) by A44, Th40; :: thesis:
( dom (FA . n) = (dom (F0 . n)) /\ A & dom (FB . n) = (dom (F0 . n)) /\ B ) by A45, RELAT_1:90;
hence ( dom (FA . n) = dom (f | A) & dom (FB . n) = dom (f | B) ) by A2, A11, A33; :: thesis:

end;

A46: for n being Nat holds
( FA . n is nonnegative & FB . n is nonnegative )

proof

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;
F0 . n is nonnegative by A11;
then ( (F0 . n) | A is nonnegative & (F0 . n) | B is nonnegative ) by Th21;
hence ( FA . n is nonnegative & FB . n is nonnegative ) by A41, A42; :: thesis:

end;

A47: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | A) holds
(FA . n) . x <= (FA . m) . x

proof

let n, m be Nat; :: thesis:
assume A48: n <= m ; :: thesis:
let x be Element of X; :: thesis:
assume A49: x in dom (f | A) ; :: thesis:
then x in (dom f) /\ A by RELAT_1:90;
then A50: x in dom f by XBOOLE_0:def 4;
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
( dom ((F0 . n) | A) = dom (FA . n) & dom ((F0 . m) | A) = dom (FA . m) ) by A41;
then A51: ( dom ((F0 . n) | A) = dom (f | A) & dom ((F0 . m) | A) = dom (f | A) ) by A43;
( (FA . n) . x = ((F0 . n) | A) . x & (FA . m) . x = ((F0 . m) | A) . x ) by A41;
then ( (FA . n) . x = (F0 . n) . x & (FA . m) . x = (F0 . m) . x ) by A49, A51, FUNCT_1:70;
hence (FA . n) . x <= (FA . m) . x by A11, A48, A50; :: thesis:

end;

A52: for n, m being Nat st n <= m holds
for x being Element of X st x in dom (f | B) holds
(FB . n) . x <= (FB . m) . x

proof

let n, m be Nat; :: thesis:
assume A53: n <= m ; :: thesis:
let x be Element of X; :: thesis:
assume A54: x in dom (f | B) ; :: thesis:
then x in (dom f) /\ B by RELAT_1:90;
then A55: x in dom f by XBOOLE_0:def 4;
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
( dom ((F0 . n) | B) = dom (FB . n) & dom ((F0 . m) | B) = dom (FB . m) ) by A42;
then A56: ( dom ((F0 . n) | B) = dom (f | B) & dom ((F0 . m) | B) = dom (f | B) ) by A43;
( (FB . n) . x = ((F0 . n) | B) . x & (FB . m) . x = ((F0 . m) | B) . x ) by A42;
then ( (FB . n) . x = (F0 . n) . x & (FB . m) . x = (F0 . m) . x ) by A54, A56, FUNCT_1:70;
hence (FB . n) . x <= (FB . m) . x by A11, A53, A55; :: thesis:

end;

A57: for x being Element of X st x in dom (f | A) holds
( FA # x is convergent & lim (FA # x) = (f | A) . x )

proof

let x be Element of X; :: thesis:
assume A58: x in dom (f | A) ; :: thesis:
then x in (dom f) /\ A by RELAT_1:90;
then A59: x in dom f by XBOOLE_0:def 4;

now

let n be Element of NAT ; :: thesis:
A60: dom ((F0 . n) | A) = dom (FA . n) by A41
.= dom (f | A) by A43 ;
(FA # x) . n = (FA . n) . x by Def13;
then (FA # x) . n = ((F0 . n) | A) . x by A41;
then (FA # x) . n = (F0 . n) . x by A58, A60, FUNCT_1:70;
hence (FA # x) . n = (F0 # x) . n by Def13; :: thesis:

end;

then A61: FA # x = F0 # x by FUNCT_2:113;
( F0 # x is convergent & lim (F0 # x) = f . x ) by A11, A59;
hence ( FA # x is convergent & lim (FA # x) = (f | A) . x ) by A58, A61, FUNCT_1:70; :: thesis:

end;

A62: for x being Element of X st x in dom (f | B) holds
( FB # x is convergent & lim (FB # x) = (f | B) . x )

proof

let x be Element of X; :: thesis:
assume A63: x in dom (f | B) ; :: thesis:
then x in (dom f) /\ B by RELAT_1:90;
then A64: x in dom f by XBOOLE_0:def 4;

now

let n be Element of NAT ; :: thesis:
A65: dom ((F0 . n) | B) = dom (FB . n) by A42
.= dom (f | B) by A43 ;
thus (FB # x) . n = (FB . n) . x by Def13
.= ((F0 . n) | B) . x by A42
.= (F0 . n) . x by A63, A65, FUNCT_1:70
.= (F0 # x) . n by Def13 ; :: thesis:

end;

then A66: FB # x = F0 # x by FUNCT_2:113;
( F0 # x is convergent & lim (F0 # x) = f . x ) by A11, A64;
hence ( FB # x is convergent & lim (FB # x) = (f | B) . x ) by A63, A66, FUNCT_1:70; :: thesis:

end;

deffunc H₅( Nat) -> Element of ExtREAL = integral' M,(FA . $1);
consider KA being ExtREAL_sequence such that
A67: for n being Element of NAT holds KA . n = H₅(n) from FUNCT_2:sch 4();

A68: now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence KA . n = H₅(n) by A67; :: thesis:

end;

deffunc H₆( Nat) -> Element of ExtREAL = integral' M,(FB . $1);
consider KB being ExtREAL_sequence such that
A69: for n being Element of NAT holds KB . n = H₆(n) from FUNCT_2:sch 4();

A70: now

let n be Nat; :: thesis:
n in NAT by ORDINAL1:def 13;
hence KB . n = H₆(n) by A69; :: thesis:

end;

for n, m being Nat st n <= m holds
( KA . n <= KA . m & KB . n <= KB . m )

proof

let n, m be Nat; :: thesis:
assume A71: n <= m ; :: thesis:
A72: ( FA . n is_simple_func_in S & FA . m is_simple_func_in S & FB . n is_simple_func_in S & FB . m is_simple_func_in S & dom (FA . n) = dom (f | A) & dom (FA . m) = dom (f | A) & dom (FB . n) = dom (f | B) & dom (FB . m) = dom (f | B) ) by A43;
A73: ( FA . n is nonnegative & FA . m is nonnegative & FB . n is nonnegative & FB . m is nonnegative ) by A46;
A74: ( KA . m = integral' M,(FA . m) & KB . m = integral' M,(FB . m) ) by A68, A70;
A75: for x being set st x in dom ((FA . m) - (FA . n)) holds
(FA . n) . x <= (FA . m) . x

proof

let x be set ; :: thesis:
assume x in dom ((FA . m) - (FA . n)) ; :: thesis:
then x in ((dom (FA . m)) /\ (dom (FA . n))) \ ((((FA . m) " {+infty }) /\ ((FA . n) " {+infty })) \/ (((FA . m) " {-infty }) /\ ((FA . n) " {-infty }))) by MESFUNC1:def 4;
then x in (dom (FA . m)) /\ (dom (FA . n)) by XBOOLE_0:def 5;
hence (FA . n) . x <= (FA . m) . x by A47, A71, A72; :: thesis:

end;

then A76: integral' M,((FA . n) | (dom ((FA . m) - (FA . n)))) <= integral' M,((FA . m) | (dom ((FA . m) - (FA . n)))) by A72, A73, Th76;
dom ((FA . m) - (FA . n)) = (dom (FA . m)) /\ (dom (FA . n)) by A72, A73, A75, Th75;
then ( (FA . m) | (dom ((FA . m) - (FA . n))) = FA . m & (FA . n) | (dom ((FA . m) - (FA . n))) = FA . n ) by A72, GRFUNC_1:64;
hence KA . n <= KA . m by A68, A74, A76; :: thesis:
A77: for x being set st x in dom ((FB . m) - (FB . n)) holds
(FB . n) . x <= (FB . m) . x

proof

let x be set ; :: thesis:
assume x in dom ((FB . m) - (FB . n)) ; :: thesis:
then x in ((dom (FB . m)) /\ (dom (FB . n))) \ ((((FB . m) " {+infty }) /\ ((FB . n) " {+infty })) \/ (((FB . m) " {-infty }) /\ ((FB . n) " {-infty }))) by MESFUNC1:def 4;
then x in (dom (FB . m)) /\ (dom (FB . n)) by XBOOLE_0:def 5;
hence (FB . n) . x <= (FB . m) . x by A52, A71, A72; :: thesis:

end;

then A78: integral' M,((FB . n) | (dom ((FB . m) - (FB . n)))) <= integral' M,((FB . m) | (dom ((FB . m) - (FB . n)))) by A72, A73, Th76;
dom ((FB . m) - (FB . n)) = (dom (FB . m)) /\ (dom (FB . n)) by A72, A73, A77, Th75;
then ( (FB . m) | (dom ((FB . m) - (FB . n))) = FB . m & (FB . n) | (dom ((FB . m) - (FB . n))) = FB . n ) by A72, GRFUNC_1:64;
hence KB . n <= KB . m by A70, A74, A78; :: thesis:

end;

then A79: ( ( for n, m being Nat st n <= m holds
KA . n <= KA . m ) & ( for n, m being Nat st n <= m holds
KB . n <= KB . m ) ) ;
then ( KA is convergent & KB is convergent ) by Th60;
then A80: ( integral+ M,(f | A) = lim KA & integral+ M,(f | B) = lim KB ) by A33, A37, A39, A40, A43, A46, A47, A52, A57, A62, A68, A70, Def15;
A81: for n being Nat holds KAB . n = (KA . n) + (KB . n)

proof

let n be Nat; :: thesis:
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A82: ( F0 . n is_simple_func_in S & F0 . n is nonnegative ) by A11;
( FA . n = (F0 . n) | A & FB . n = (F0 . n) | B ) by A41, A42;
then A83: integral' M,((F0 . n) | (A \/ B)) = (integral' M,(FA . n)) + (integral' M,(FB . n)) by A1, A82, Th73;
A84: KAB . n = integral' M,(FAB . n) by A14
.= integral' M,((F0 . n) | (A \/ B)) by A12 ;
KA . n = integral' M,(FA . n) by A68;
hence KAB . n = (KA . n) + (KB . n) by A70, A83, A84; :: thesis:

end;

for n being set holds
( ( n in dom KA implies -infty < KA . n ) & ( n in dom KB implies -infty < KB . n ) )

proof

let n be set ; :: thesis:

hereby :: thesis:

assume n in dom KA ; :: thesis:
then reconsider n1 = n as Element of NAT ;
( KA . n1 = integral' M,(FA . n1) & FA . n1 is_simple_func_in S ) by A43, A68;
hence -infty < KA . n by A46, Th74; :: thesis:

end;

assume n in dom KB ; :: thesis:
then reconsider n1 = n as Element of NAT ;
( KB . n1 = integral' M,(FB . n1) & FB . n1 is_simple_func_in S ) by A43, A70;
hence -infty < KB . n by A46, Th74; :: thesis:

end;

then ( KA is without-infty & KB is without-infty ) by Th16;
hence integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B)) by A31, A79, A80, A81, Th67; :: thesis: