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 ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
integral+ M,(f | (A \/ B)) = (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 ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
integral+ M,(f | (A \/ B)) = (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 ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B))
let f be PartFunc of X,ExtREAL ; :: thesis: for A, B being Element of S st ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B holds
integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B))
let A, B be Element of S; :: thesis: ( ex E being Element of S st
( E = dom f & f is_measurable_on E ) & f is nonnegative & A misses B implies integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B)) )
assume that
A1: ex E being Element of S st
( E = dom f & f is_measurable_on E ) and
A2: f is nonnegative and
A3: A misses B ; :: thesis: integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B))
consider F0 being Functional_Sequence of X,ExtREAL , K0 being ExtREAL_sequence such that
A4: for n being Nat holds
( F0 . n is_simple_func_in S & dom (F0 . n) = dom f ) and
A5: for n being Nat holds F0 . n is nonnegative and
A6: 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 and
A7: for x being Element of X st x in dom f holds
( F0 # x is convergent & lim (F0 # x) = f . x ) and
for n being Nat holds K0 . n = integral' M,(F0 . n) and
K0 is convergent and
integral+ M,f = lim K0 by A1, A2, Def15;
deffunc H₁( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | B;
deffunc H₂( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | A;
consider FA being Functional_Sequence of X,ExtREAL such that
A8: for n being Nat holds FA . n = H₂(n) from SEQFUNC:sch 1();
consider E being Element of S such that
A9: E = dom f and
A10: f is_measurable_on E by A1;
consider FB being Functional_Sequence of X,ExtREAL such that
A11: for n being Nat holds FB . n = H₁(n) from SEQFUNC:sch 1();
set DB = E /\ B;
A12: E /\ B = dom (f | B) by A9, RELAT_1:90;
then A13: (dom f) /\ (E /\ B) = E /\ B by RELAT_1:89, XBOOLE_1:28;
then A14: dom (f | (E /\ B)) = dom (f | B) by A12, RELAT_1:90;
for x being set st x in dom (f | (E /\ B)) holds
(f | (E /\ B)) . x = (f | B) . x

proof

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

end;

then A16: f | (E /\ B) = f | B by A12, A13, FUNCT_1:9, RELAT_1:90;
set DA = E /\ A;
A17: E /\ A = dom (f | A) by A9, RELAT_1:90;
then A18: (dom f) /\ (E /\ A) = E /\ A by RELAT_1:89, XBOOLE_1:28;
then A19: dom (f | (E /\ A)) = dom (f | A) by A17, 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: ( x in dom (f | (E /\ A)) implies (f | (E /\ A)) . x = (f | A) . x )
assume A20: x in dom (f | (E /\ A)) ; :: thesis: (f | (E /\ A)) . x = (f | A) . x
then (f | A) . x = f . x by A19, FUNCT_1:70;
hence (f | (E /\ A)) . x = (f | A) . x by A20, FUNCT_1:70; :: thesis: verum

end;

then A21: f | (E /\ A) = f | A by A17, A18, FUNCT_1:9, RELAT_1:90;
A22: 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: ( 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) )
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
A23: FB . n1 = (F0 . n1) | B by A11;
then A24: dom (FB . n) = (dom (F0 . n)) /\ B by RELAT_1:90;
A25: FA . n1 = (F0 . n1) | A by A8;
hence ( FA . n is_simple_func_in S & FB . n is_simple_func_in S ) by A4, A23, Th40; :: thesis: ( dom (FA . n) = dom (f | A) & dom (FB . n) = dom (f | B) )
dom (FA . n) = (dom (F0 . n)) /\ A by A25, RELAT_1:90;
hence ( dom (FA . n) = dom (f | A) & dom (FB . n) = dom (f | B) ) by A9, A4, A17, A12, A24; :: thesis: verum

end;

A26: 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: ( x in dom (f | A) implies ( FA # x is convergent & lim (FA # x) = (f | A) . x ) )
assume A27: x in dom (f | A) ; :: thesis: ( FA # x is convergent & lim (FA # x) = (f | A) . x )

now

let n be Element of NAT ; :: thesis: (FA # x) . n = (F0 # x) . n
(FA # x) . n = (FA . n) . x by Def13;
then A28: (FA # x) . n = ((F0 . n) | A) . x by A8;
dom ((F0 . n) | A) = dom (FA . n) by A8
.= dom (f | A) by A22 ;
then (FA # x) . n = (F0 . n) . x by A27, A28, FUNCT_1:70;
hence (FA # x) . n = (F0 # x) . n by Def13; :: thesis: verum

end;

then A29: FA # x = F0 # x by FUNCT_2:113;
x in (dom f) /\ A by A27, RELAT_1:90;
then A30: x in dom f by XBOOLE_0:def 4;
then lim (F0 # x) = f . x by A7;
hence ( FA # x is convergent & lim (FA # x) = (f | A) . x ) by A7, A27, A30, A29, FUNCT_1:70; :: thesis: verum

end;

A31: 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: ( x in dom (f | B) implies ( FB # x is convergent & lim (FB # x) = (f | B) . x ) )
assume A32: x in dom (f | B) ; :: thesis: ( FB # x is convergent & lim (FB # x) = (f | B) . x )

now

let n be Element of NAT ; :: thesis: (FB # x) . n = (F0 # x) . n
A33: dom ((F0 . n) | B) = dom (FB . n) by A11
.= dom (f | B) by A22 ;
thus (FB # x) . n = (FB . n) . x by Def13
.= ((F0 . n) | B) . x by A11
.= (F0 . n) . x by A32, A33, FUNCT_1:70
.= (F0 # x) . n by Def13 ; :: thesis: verum

end;

then A34: FB # x = F0 # x by FUNCT_2:113;
x in (dom f) /\ B by A32, RELAT_1:90;
then A35: x in dom f by XBOOLE_0:def 4;
then lim (F0 # x) = f . x by A7;
hence ( FB # x is convergent & lim (FB # x) = (f | B) . x ) by A7, A32, A35, A34, FUNCT_1:70; :: thesis: verum

end;

set C = E /\ (A \/ B);
A36: E /\ (A \/ B) = (dom f) /\ (E /\ (A \/ B)) by A9, XBOOLE_1:17, XBOOLE_1:28;
A37: dom (f | (A \/ B)) = E /\ (A \/ B) by A9, RELAT_1:90;
then A38: dom (f | (A \/ B)) = dom (f | (E /\ (A \/ B))) by A36, 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: ( x in dom (f | (A \/ B)) implies (f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x )
assume A39: x in dom (f | (A \/ B)) ; :: thesis: (f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x
then (f | (A \/ B)) . x = f . x by FUNCT_1:70;
hence (f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x by A38, A39, FUNCT_1:70; :: thesis: verum

end;

then A40: f | (A \/ B) = f | (E /\ (A \/ B)) by A38, FUNCT_1:9;
f is_measurable_on E /\ (A \/ B) by A10, MESFUNC1:34, XBOOLE_1:17;
then A41: f | (A \/ B) is_measurable_on E /\ (A \/ B) by A36, A40, Th48;
f is_measurable_on E /\ B by A10, MESFUNC1:34, XBOOLE_1:17;
then A42: f | B is_measurable_on E /\ B by A13, A16, Th48;
A43: f | B is nonnegative by A2, Th21;
f is_measurable_on E /\ A by A10, MESFUNC1:34, XBOOLE_1:17;
then A44: f | A is_measurable_on E /\ A by A18, A21, Th48;
A45: f | A is nonnegative by A2, Th21;
deffunc H₃( Nat) -> Element of bool [:X,ExtREAL :] = (F0 . $1) | (A \/ B);
consider FAB being Functional_Sequence of X,ExtREAL such that
A46: for n being Nat holds FAB . n = H₃(n) from SEQFUNC:sch 1();
A47: for n being Nat holds
( FA . n is nonnegative & FB . n is nonnegative )

proof

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

end;

A49: 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: ( n <= m implies for x being Element of X st x in dom (f | B) holds
(FB . n) . x <= (FB . m) . x )
assume A50: n <= m ; :: thesis: for x being Element of X st x in dom (f | B) holds
(FB . n) . x <= (FB . m) . x
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
let x be Element of X; :: thesis: ( x in dom (f | B) implies (FB . n) . x <= (FB . m) . x )
assume A51: x in dom (f | B) ; :: thesis: (FB . n) . x <= (FB . m) . x
then x in (dom f) /\ B by RELAT_1:90;
then A52: x in dom f by XBOOLE_0:def 4;
dom ((F0 . m) | B) = dom (FB . m) by A11;
then A53: dom ((F0 . m) | B) = dom (f | B) by A22;
(FB . m) . x = ((F0 . m) | B) . x by A11;
then A54: (FB . m) . x = (F0 . m) . x by A51, A53, FUNCT_1:70;
dom ((F0 . n) | B) = dom (FB . n) by A11;
then A55: dom ((F0 . n) | B) = dom (f | B) by A22;
(FB . n) . x = ((F0 . n) | B) . x by A11;
then (FB . n) . x = (F0 . n) . x by A51, A55, FUNCT_1:70;
hence (FB . n) . x <= (FB . m) . x by A6, A50, A52, A54; :: thesis: verum

end;

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

A58: now

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

end;

A59: now

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

end;

A60: 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: ( ( n in dom KA implies -infty < KA . n ) & ( n in dom KB implies -infty < KB . n ) )

hereby :: thesis: ( n in dom KB implies -infty < KB . n )

assume n in dom KA ; :: thesis: -infty < KA . n
then reconsider n1 = n as Element of NAT ;
A61: FA . n1 is_simple_func_in S by A22;
KA . n1 = integral' M,(FA . n1) by A59;
hence -infty < KA . n by A47, A61, Th74; :: thesis: verum

end;

assume n in dom KB ; :: thesis: -infty < KB . n
then reconsider n1 = n as Element of NAT ;
A62: FB . n1 is_simple_func_in S by A22;
KB . n1 = integral' M,(FB . n1) by A58;
hence -infty < KB . n by A47, A62, Th74; :: thesis: verum

end;

then A63: KB is without-infty by Th16;
deffunc H₆( Nat) -> Element of ExtREAL = integral' M,(FAB . $1);
consider KAB being ExtREAL_sequence such that
A64: for n being Element of NAT holds KAB . n = H₆(n) from FUNCT_2:sch 4();

A65: now

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

end;

A66: for n being Nat holds KAB . n = (KA . n) + (KB . n)

proof

let n be Nat; :: thesis: KAB . n = (KA . n) + (KB . n)
reconsider n = n as Element of NAT by ORDINAL1:def 13;
A67: FA . n = (F0 . n) | A by A8;
A68: FB . n = (F0 . n) | B by A11;
A69: KAB . n = integral' M,(FAB . n) by A65
.= integral' M,((F0 . n) | (A \/ B)) by A46 ;
A70: KA . n = integral' M,(FA . n) by A59;
F0 . n is_simple_func_in S by A4;
then integral' M,((F0 . n) | (A \/ B)) = (integral' M,(FA . n)) + (integral' M,(FB . n)) by A3, A5, A67, A68, Th73;
hence KAB . n = (KA . n) + (KB . n) by A58, A69, A70; :: thesis: verum

end;

A71: 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: ( n <= m implies for x being Element of X st x in dom (f | A) holds
(FA . n) . x <= (FA . m) . x )
assume A72: n <= m ; :: thesis: for x being Element of X st x in dom (f | A) holds
(FA . n) . x <= (FA . m) . x
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
let x be Element of X; :: thesis: ( x in dom (f | A) implies (FA . n) . x <= (FA . m) . x )
assume A73: x in dom (f | A) ; :: thesis: (FA . n) . x <= (FA . m) . x
then x in (dom f) /\ A by RELAT_1:90;
then A74: x in dom f by XBOOLE_0:def 4;
dom ((F0 . m) | A) = dom (FA . m) by A8;
then A75: dom ((F0 . m) | A) = dom (f | A) by A22;
(FA . m) . x = ((F0 . m) | A) . x by A8;
then A76: (FA . m) . x = (F0 . m) . x by A73, A75, FUNCT_1:70;
dom ((F0 . n) | A) = dom (FA . n) by A8;
then A77: dom ((F0 . n) | A) = dom (f | A) by A22;
(FA . n) . x = ((F0 . n) | A) . x by A8;
then (FA . n) . x = (F0 . n) . x by A73, A77, FUNCT_1:70;
hence (FA . n) . x <= (FA . m) . x by A6, A72, A74, A76; :: thesis: verum

end;

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

proof

let n, m be Nat; :: thesis: ( n <= m implies ( KA . n <= KA . m & KB . n <= KB . m ) )
A79: FA . m is_simple_func_in S by A22;
A80: dom (FA . m) = dom (f | A) by A22;
A81: KA . m = integral' M,(FA . m) by A59;
A82: dom (FA . n) = dom (f | A) by A22;
assume A83: n <= m ; :: thesis: ( KA . n <= KA . m & KB . n <= KB . m )
A84: 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: ( x in dom ((FA . m) - (FA . n)) implies (FA . n) . x <= (FA . m) . x )
assume x in dom ((FA . m) - (FA . n)) ; :: thesis: (FA . n) . x <= (FA . m) . x
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 A71, A83, A82, A80; :: thesis: verum

end;

A85: FA . m is nonnegative by A47;
A86: FA . n is nonnegative by A47;
A87: FA . n is_simple_func_in S by A22;
then A88: dom ((FA . m) - (FA . n)) = (dom (FA . m)) /\ (dom (FA . n)) by A79, A86, A85, A84, Th75;
then A89: (FA . m) | (dom ((FA . m) - (FA . n))) = FA . m by A82, A80, GRFUNC_1:64;
A90: (FA . n) | (dom ((FA . m) - (FA . n))) = FA . n by A82, A80, A88, GRFUNC_1:64;
integral' M,((FA . n) | (dom ((FA . m) - (FA . n)))) <= integral' M,((FA . m) | (dom ((FA . m) - (FA . n)))) by A87, A79, A86, A85, A84, Th76;
hence KA . n <= KA . m by A59, A81, A89, A90; :: thesis: KB . n <= KB . m
A91: FB . m is_simple_func_in S by A22;
A92: FB . n is nonnegative by A47;
A93: FB . m is nonnegative by A47;
A94: KB . m = integral' M,(FB . m) by A58;
A95: dom (FB . m) = dom (f | B) by A22;
A96: dom (FB . n) = dom (f | B) by A22;
A97: 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: ( x in dom ((FB . m) - (FB . n)) implies (FB . n) . x <= (FB . m) . x )
assume x in dom ((FB . m) - (FB . n)) ; :: thesis: (FB . n) . x <= (FB . m) . x
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 A49, A83, A96, A95; :: thesis: verum

end;

A98: FB . n is_simple_func_in S by A22;
then A99: dom ((FB . m) - (FB . n)) = (dom (FB . m)) /\ (dom (FB . n)) by A91, A92, A93, A97, Th75;
then A100: (FB . m) | (dom ((FB . m) - (FB . n))) = FB . m by A96, A95, GRFUNC_1:64;
A101: (FB . n) | (dom ((FB . m) - (FB . n))) = FB . n by A96, A95, A99, GRFUNC_1:64;
integral' M,((FB . n) | (dom ((FB . m) - (FB . n)))) <= integral' M,((FB . m) | (dom ((FB . m) - (FB . n)))) by A98, A91, A92, A93, A97, Th76;
hence KB . n <= KB . m by A58, A94, A100, A101; :: thesis: verum

end;

then A102: for n, m being Nat st n <= m holds
KA . n <= KA . m ;
then KA is convergent by Th60;
then A103: integral+ M,(f | A) = lim KA by A17, A44, A45, A22, A47, A71, A26, A59, Def15;
A104: ( ( 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: ( ( 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 ) ) )

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

end;

hereby :: thesis: ( ( 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 ) ) )

let n be Nat; :: thesis: for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x = (F0 . n) . x
let x be Element of X; :: thesis: ( x in dom (f | (A \/ B)) implies (FAB . n) . x = (F0 . n) . x )
assume x in dom (f | (A \/ B)) ; :: thesis: (FAB . n) . x = (F0 . n) . x
then A107: x in dom (FAB . n) by A105;
FAB . n = (F0 . n) | (A \/ B) by A46;
hence (FAB . n) . x = (F0 . n) . x by A107, FUNCT_1:70; :: thesis: verum

end;

hereby :: thesis: ( ( 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 ) ) )

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

end;

hereby :: thesis: 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 )

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x <= (FAB . m) . x )
assume A108: n <= m ; :: thesis: for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x <= (FAB . m) . x

now

let x be Element of X; :: thesis: ( x in dom (f | (A \/ B)) implies (FAB . n) . x <= (FAB . m) . x )
assume A109: x in dom (f | (A \/ B)) ; :: thesis: (FAB . n) . x <= (FAB . m) . x
then A110: (FAB . m) . x = (F0 . m) . x by A106;
x in (dom f) /\ (A \/ B) by A109, RELAT_1:90;
then A111: x in dom f by XBOOLE_0:def 4;
(FAB . n) . x = (F0 . n) . x by A106, A109;
hence (FAB . n) . x <= (FAB . m) . x by A6, A108, A111, A110; :: thesis: verum

end;

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

end;

hereby :: thesis: verum

let x be Element of X; :: thesis: ( x in dom (f | (A \/ B)) implies ( FAB # x is convergent & lim (FAB # x) = (f | (A \/ B)) . x ) )
assume A112: x in dom (f | (A \/ B)) ; :: thesis: ( FAB # x is convergent & lim (FAB # x) = (f | (A \/ B)) . x )
then x in (dom f) /\ (A \/ B) by RELAT_1:90;
then A113: x in dom f by XBOOLE_0:def 4;

A114: now

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

end;

then FAB # x = F0 # x by FUNCT_2:113;
hence FAB # x is convergent by A7, A113; :: thesis: lim (FAB # x) = (f | (A \/ B)) . x
thus lim (FAB # x) = lim (F0 # x) by A114, FUNCT_2:113
.= f . x by A7, A113
.= (f | (A \/ B)) . x by A112, FUNCT_1:70 ; :: thesis: verum

end;

end;

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

proof

let n, m be Nat; :: thesis: ( n <= m implies KAB . n <= KAB . m )
assume A115: n <= m ; :: thesis: KAB . n <= KAB . m
reconsider n = n, m = m as Element of NAT by ORDINAL1:def 13;
A116: dom (FAB . m) = dom (f | (A \/ B)) by A104;
A117: dom (FAB . n) = dom (f | (A \/ B)) by A104;
A118: 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: ( x in dom ((FAB . m) - (FAB . n)) implies (FAB . n) . x <= (FAB . m) . x )
assume x in dom ((FAB . m) - (FAB . n)) ; :: thesis: (FAB . n) . x <= (FAB . m) . x
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 A104, A115, A117, A116; :: thesis: verum

end;

A119: KAB . m = integral' M,(FAB . m) by A65;
A120: FAB . m is_simple_func_in S by A104;
A121: FAB . m is nonnegative by A104;
A122: FAB . n is nonnegative by A104;
A123: FAB . n is_simple_func_in S by A104;
then A124: dom ((FAB . m) - (FAB . n)) = (dom (FAB . m)) /\ (dom (FAB . n)) by A120, A122, A121, A118, Th75;
then A125: (FAB . m) | (dom ((FAB . m) - (FAB . n))) = FAB . m by A117, A116, GRFUNC_1:64;
A126: (FAB . n) | (dom ((FAB . m) - (FAB . n))) = FAB . n by A117, A116, A124, GRFUNC_1:64;
integral' M,((FAB . n) | (dom ((FAB . m) - (FAB . n)))) <= integral' M,((FAB . m) | (dom ((FAB . m) - (FAB . n)))) by A123, A120, A122, A121, A118, Th76;
hence KAB . n <= KAB . m by A65, A119, A125, A126; :: thesis: verum

end;

then A127: KAB is convergent by Th60;
A128: for n, m being Nat st n <= m holds
KB . n <= KB . m by A78;
then KB is convergent by Th60;
then A129: integral+ M,(f | B) = lim KB by A12, A42, A43, A22, A47, A49, A31, A58, Def15;
f | (A \/ B) is nonnegative by A2, Th21;
then A130: integral+ M,(f | (A \/ B)) = lim KAB by A37, A41, A65, A104, A127, Def15;
KA is without-infty by A60, Th16;
hence integral+ M,(f | (A \/ B)) = (integral+ M,(f | A)) + (integral+ M,(f | B)) by A130, A102, A128, A103, A129, A66, A63, Th67; :: thesis: verum