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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) & 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 E -measurable ) 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 H1( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | B;
deffunc H2( 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 = H2(n) from SEQFUNC:sch 1();
 consider E being Element of S such that
A9: E = dom f and
A10: f is E -measurable by A1;
consider FB being Functional_Sequence of X,ExtREAL such that
A11: for n being Nat holds FB . n = H1(n) from SEQFUNC:sch 1();
 set DB = E /\ B;
A12: E /\ B = dom (f | B) by A9, RELAT_1:61;
then A13: (dom f) /\ (E /\ B) = E /\ B by RELAT_1:60, XBOOLE_1:28;
then A14: dom (f | (E /\ B)) = dom (f | B) by A12, RELAT_1:61;
for x being object st x in dom (f | (E /\ B)) holds
(f | (E /\ B)) . x = (f | B) . x
proof
let x be object ; :: 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:47;
hence (f | (E /\ B)) . x = (f | B) . x by A15, FUNCT_1:47; :: thesis: verum
end;
then A16: f | (E /\ B) = f | B by A12, A13, FUNCT_1:2, RELAT_1:61;
set DA = E /\ A;
A17: E /\ A = dom (f | A) by A9, RELAT_1:61;
then A18: (dom f) /\ (E /\ A) = E /\ A by RELAT_1:60, XBOOLE_1:28;
then A19: dom (f | (E /\ A)) = dom (f | A) by A17, RELAT_1:61;
for x being object st x in dom (f | (E /\ A)) holds
(f | (E /\ A)) . x = (f | A) . x
proof
let x be object ; :: 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:47;
hence (f | (E /\ A)) . x = (f | A) . x by A20, FUNCT_1:47; :: thesis: verum
end;
then A21: f | (E /\ A) = f | A by A17, A18, FUNCT_1:2, RELAT_1:61;
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 12;
A23: FB . n1 = (F0 . n1) | B by A11;
then A24: dom (FB . n) = (dom (F0 . n)) /\ B by RELAT_1:61;
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, Th34; :: thesis: ( dom (FA . n) = dom (f | A) & dom (FB . n) = dom (f | B) )
dom (FA . n) = (dom (F0 . n)) /\ A by A25, RELAT_1:61;
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 :: thesis: for n being Element of NAT holds (FA # x) . n = (F0 # x) . n
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:47;
hence (FA # x) . n = (F0 # x) . n by Def13; :: thesis: verum
end;
then A29: FA # x = F0 # x by FUNCT_2:63;
x in (dom f) /\ A by A27, RELAT_1:61;
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:47; :: 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 :: thesis: for n being Element of NAT holds (FB # x) . n = (F0 # x) . n
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:47
.= (F0 # x) . n by Def13 ; :: thesis: verum
end;
then A34: FB # x = F0 # x by FUNCT_2:63;
x in (dom f) /\ B by A32, RELAT_1:61;
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:47; :: 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:61;
then A38: dom (f | (A \/ B)) = dom (f | (E /\ (A \/ B))) by A36, RELAT_1:61;
for x being object st x in dom (f | (A \/ B)) holds
(f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x
proof
let x be object ; :: 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:47;
hence (f | (A \/ B)) . x = (f | (E /\ (A \/ B))) . x by A38, A39, FUNCT_1:47; :: thesis: verum
end;
then A40: f | (A \/ B) = f | (E /\ (A \/ B)) by A38, FUNCT_1:2;
f is E /\ (A \/ B) -measurable by A10, MESFUNC1:30, XBOOLE_1:17;
then A41: f | (A \/ B) is E /\ (A \/ B) -measurable by A36, A40, Th42;
f is E /\ B -measurable by A10, MESFUNC1:30, XBOOLE_1:17;
then A42: f | B is E /\ B -measurable by A13, A16, Th42;
A43: f | B is nonnegative by A2, Th15;
f is E /\ A -measurable by A10, MESFUNC1:30, XBOOLE_1:17;
then A44: f | A is E /\ A -measurable by A18, A21, Th42;
A45: f | A is nonnegative by A2, Th15;
deffunc H3( 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 = H3(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 12;
A48: (F0 . n) | B is nonnegative by A5, Th15;
(F0 . n) | A is nonnegative by A5, Th15;
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 12;
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:61;
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:47;
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:47;
hence (FB . n) . x <= (FB . m) . x by A6, A50, A52, A54; :: thesis: verum
end;
deffunc H4( 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 = H4(n) from FUNCT_2:sch 4();
 deffunc H5( 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 = H5(n) from FUNCT_2:sch 4();
A58: now :: thesis: for n being Nat holds KB . n = H5(n)
let n be Nat; :: thesis: KB . n = H5(n)
n in NAT by ORDINAL1:def 12;
hence KB . n = H5(n) by A57; :: thesis: verum
end;
A59: now :: thesis: for n being Nat holds KA . n = H4(n)
let n be Nat; :: thesis: KA . n = H4(n)
n in NAT by ORDINAL1:def 12;
hence KA . n = H4(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, Th68; :: 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, Th68; :: thesis: verum
end;
then A63: KB is () by Th10;
deffunc H6( 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 = H6(n) from FUNCT_2:sch 4();
A65: now :: thesis: for n being Nat holds KAB . n = H6(n)
let n be Nat; :: thesis: KAB . n = H6(n)
n in NAT by ORDINAL1:def 12;
hence KAB . n = H6(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 12;
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, Th67;
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 12;
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:61;
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:47;
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:47;
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 object st x in dom ((FA . m) - (FA . n)) holds
(FA . n) . x <= (FA . m) . x
proof
let x be object ; :: 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, Th69;
then A89: (FA . m) | (dom ((FA . m) - (FA . n))) = FA . m by A82, A80, GRFUNC_1:23;
A90: (FA . n) | (dom ((FA . m) - (FA . n))) = FA . n by A82, A80, A88, GRFUNC_1:23;
integral' (M,((FA . n) | (dom ((FA . m) - (FA . n))))) <= integral' (M,((FA . m) | (dom ((FA . m) - (FA . n))))) by A87, A79, A86, A85, A84, Th70;
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 object st x in dom ((FB . m) - (FB . n)) holds
(FB . n) . x <= (FB . m) . x
proof
let x be object ; :: 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, Th69;
then A100: (FB . m) | (dom ((FB . m) - (FB . n))) = FB . m by A96, A95, GRFUNC_1:23;
A101: (FB . n) | (dom ((FB . m) - (FB . n))) = FB . n by A96, A95, A99, GRFUNC_1:23;
integral' (M,((FB . n) | (dom ((FB . m) - (FB . n))))) <= integral' (M,((FB . m) | (dom ((FB . m) - (FB . n))))) by A98, A91, A92, A93, A97, Th70;
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 Th54;
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, Th34; :: 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:61
.= (dom f) /\ (A \/ B) by A4
.= dom (f | (A \/ B)) by RELAT_1:61 ; :: 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:47; :: 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 12;
(F0 . n1) | (A \/ B) is nonnegative by A5, Th15;
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 :: thesis: for x being Element of X st x in dom (f | (A \/ B)) holds
(FAB . n) . x <= (FAB . m) . x
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:61;
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:61;
then A113: x in dom f by XBOOLE_0:def 4;
A114: now :: thesis: for n being Element of NAT holds (FAB # x) . n = (F0 # x) . n
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:63;
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:63
.= f . x by A7, A113
.= (f | (A \/ B)) . x by A112, FUNCT_1:47 ; :: 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 12;
A116: dom (FAB . m) = dom (f | (A \/ B)) by A104;
A117: dom (FAB . n) = dom (f | (A \/ B)) by A104;
A118: for x being object st x in dom ((FAB . m) - (FAB . n)) holds
(FAB . n) . x <= (FAB . m) . x
proof
let x be object ; :: 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, Th69;
then A125: (FAB . m) | (dom ((FAB . m) - (FAB . n))) = FAB . m by A117, A116, GRFUNC_1:23;
A126: (FAB . n) | (dom ((FAB . m) - (FAB . n))) = FAB . n by A117, A116, A124, GRFUNC_1:23;
integral' (M,((FAB . n) | (dom ((FAB . m) - (FAB . n))))) <= integral' (M,((FAB . m) | (dom ((FAB . m) - (FAB . n))))) by A123, A120, A122, A121, A118, Th70;
hence KAB . n <= KAB . m by A65, A119, A125, A126; :: thesis: verum
end;
then A127: KAB is convergent by Th54;
A128: for n, m being Nat st n <= m holds
KB . n <= KB . m by A78;
then KB is convergent by Th54;
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, Th15;
then A130: integral+ (M,(f | (A \/ B))) = lim KAB by A37, A41, A65, A104, A127, Def15;
KA is () by A60, Th10;
hence integral+ (M,(f | (A \/ B))) = (integral+ (M,(f | A))) + (integral+ (M,(f | B))) by A130, A102, A128, A103, A129, A66, A63, Th61; :: thesis: verum