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 that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: A misses B ; :: thesis:
set g2 = f | B;
set g1 = f | A;
set g = f | (A \/ B);
a4: f | (A \/ B) is nonnegative by A2, Th15;
consider G being Finite_Sep_Sequence of S, b being FinSequence of ExtREAL such that
A5: G,b are_Re-presentation_of f | (A \/ B) and
A6: b . 1 = 0 and
A7: for n being Nat st 2 <= n & n in dom b holds
( 0 < b . n & b . n < +infty ) by A1, Th34, MESFUNC3:14, a4;
deffunc H₁( Nat) -> Element of bool X = (G . $1) /\ A;
consider G1 being FinSequence such that
A8: ( len G1 = len G & ( for k being Nat st k in dom G1 holds
G1 . k = H₁(k) ) ) from FINSEQ_1:sch 2();
A9: dom G1 = Seg (len G) by A8, FINSEQ_1:def 3;
A10: for k being Nat st k in dom G holds
G1 . k = (G . k) /\ A

proof

let k be Nat; :: thesis:
assume k in dom G ; :: thesis:
then k in Seg (len G) by FINSEQ_1:def 3;
hence G1 . k = (G . k) /\ A by A8, A9; :: thesis:

end;

deffunc H₂( Nat) -> Element of bool X = (G . $1) /\ B;
consider G2 being FinSequence such that
A11: ( len G2 = len G & ( for k being Nat st k in dom G2 holds
G2 . k = H₂(k) ) ) from FINSEQ_1:sch 2();
A12: dom G2 = Seg (len G) by A11, FINSEQ_1:def 3;
A13: for k being Nat st k in dom G holds
G2 . k = (G . k) /\ B

proof

let k be Nat; :: thesis:
assume k in dom G ; :: thesis:
then k in Seg (len G) by FINSEQ_1:def 3;
hence G2 . k = (G . k) /\ B by A11, A12; :: thesis:

end;

A14: dom G = Seg (len G2) by A11, FINSEQ_1:def 3
.= dom G2 by FINSEQ_1:def 3 ;
then reconsider G2 = G2 as Finite_Sep_Sequence of S by A13, Th35;
A15: dom ((f | (A \/ B)) | B) = (dom (f | (A \/ B))) /\ B by RELAT_1:61
.= ((dom f) /\ (A \/ B)) /\ B by RELAT_1:61
.= (dom f) /\ ((A \/ B) /\ B) by XBOOLE_1:16
.= (dom f) /\ B by XBOOLE_1:21
.= dom (f | B) by RELAT_1:61 ;
for x being object st x in dom ((f | (A \/ B)) | B) holds
((f | (A \/ B)) | B) . x = (f | B) . x

proof

let x be object ; :: thesis:
assume A16: x in dom ((f | (A \/ B)) | B) ; :: thesis:
then x in (dom (f | (A \/ B))) /\ B by RELAT_1:61;
then A17: x in dom (f | (A \/ B)) by XBOOLE_0:def 4;
((f | (A \/ B)) | B) . x = (f | (A \/ B)) . x by A16, FUNCT_1:47
.= f . x by A17, FUNCT_1:47 ;
hence ((f | (A \/ B)) | B) . x = (f | B) . x by A15, A16, FUNCT_1:47; :: thesis:

end;

then (f | (A \/ B)) | B = f | B by A15, FUNCT_1:2;
then A18: G2,b are_Re-presentation_of f | B by A5, A14, A13, Th36;
A19: dom G = Seg (len G1) by A8, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then reconsider G1 = G1 as Finite_Sep_Sequence of S by A10, Th35;
A20: dom ((f | (A \/ B)) | A) = (dom (f | (A \/ B))) /\ A by RELAT_1:61
.= ((dom f) /\ (A \/ B)) /\ A by RELAT_1:61
.= (dom f) /\ ((A \/ B) /\ A) by XBOOLE_1:16
.= (dom f) /\ A by XBOOLE_1:21
.= dom (f | A) by RELAT_1:61 ;
for x being object st x in dom ((f | (A \/ B)) | A) holds
((f | (A \/ B)) | A) . x = (f | A) . x

proof

let x be object ; :: thesis:
assume A21: x in dom ((f | (A \/ B)) | A) ; :: thesis:
then x in (dom (f | (A \/ B))) /\ A by RELAT_1:61;
then A22: x in dom (f | (A \/ B)) by XBOOLE_0:def 4;
((f | (A \/ B)) | A) . x = (f | (A \/ B)) . x by A21, FUNCT_1:47
.= f . x by A22, FUNCT_1:47 ;
hence ((f | (A \/ B)) | A) . x = (f | A) . x by A20, A21, FUNCT_1:47; :: thesis:

end;

then (f | (A \/ B)) | A = f | A by A20, FUNCT_1:2;
then A23: G1,b are_Re-presentation_of f | A by A5, A19, A10, Th36;
deffunc H₃( Nat) -> Element of ExtREAL = (b . $1) * ((M * G) . $1);
consider y being FinSequence of ExtREAL such that
A24: ( len y = len G & ( for j being Nat st j in dom y holds
y . j = H₃(j) ) ) from FINSEQ_2:sch 1();
A25: dom y = Seg (len y) by FINSEQ_1:def 3
.= dom G by A24, FINSEQ_1:def 3 ;

per cases ;

suppose A26: dom (f | (A \/ B)) = {} ; :: thesis:

(dom f) /\ B c= (dom f) /\ (A \/ B) by XBOOLE_1:7, XBOOLE_1:26;
then dom (f | B) c= (dom f) /\ (A \/ B) by RELAT_1:61;
then dom (f | B) c= dom (f | (A \/ B)) by RELAT_1:61;
then dom (f | B) = {} by A26;
then A27: integral' (M,(f | B)) = 0 by Def14;
(dom f) /\ A c= (dom f) /\ (A \/ B) by XBOOLE_1:7, XBOOLE_1:26;
then dom (f | A) c= (dom f) /\ (A \/ B) by RELAT_1:61;
then dom (f | A) c= dom (f | (A \/ B)) by RELAT_1:61;
then dom (f | A) = {} by A26;
then A28: integral' (M,(f | A)) = 0 by Def14;
integral' (M,(f | (A \/ B))) = 0 by A26, Def14;
hence integral' (M,(f | (A \/ B))) = (integral' (M,(f | A))) + (integral' (M,(f | B))) by A28, A27; :: thesis:

end;

suppose A29: dom (f | (A \/ B)) <> {} ; :: thesis:

then integral (M,(f | (A \/ B))) = Sum y by A1, a4, A5, A24, A25, Th34, MESFUNC4:3;
then A30: integral' (M,(f | (A \/ B))) = Sum y by A29, Def14;

per cases ;

suppose A31: dom (f | A) = {} ; :: thesis:

A32: dom (f | (A \/ B)) = (dom f) /\ (A \/ B) by RELAT_1:61
.= ((dom f) /\ A) \/ ((dom f) /\ B) by XBOOLE_1:23
.= (dom (f | A)) \/ ((dom f) /\ B) by RELAT_1:61
.= dom (f | B) by A31, RELAT_1:61 ;

now :: thesis:

let x be object ; :: thesis:
assume A33: x in dom (f | (A \/ B)) ; :: thesis:
then (f | (A \/ B)) . x = f . x by FUNCT_1:47;
hence (f | (A \/ B)) . x = (f | B) . x by A32, A33, FUNCT_1:47; :: thesis:

end;

end;

suppose A35: dom (f | A) <> {} ; :: thesis:

per cases ;

suppose A36: dom (f | B) = {} ; :: thesis:

A37: dom (f | (A \/ B)) = (dom f) /\ (A \/ B) by RELAT_1:61
.= ((dom f) /\ B) \/ ((dom f) /\ A) by XBOOLE_1:23
.= (dom (f | B)) \/ ((dom f) /\ A) by RELAT_1:61
.= dom (f | A) by A36, RELAT_1:61 ;

now :: thesis:

let x be object ; :: thesis:
assume A38: x in dom (f | (A \/ B)) ; :: thesis:
then (f | (A \/ B)) . x = f . x by FUNCT_1:47;
hence (f | (A \/ B)) . x = (f | A) . x by A37, A38, FUNCT_1:47; :: thesis:

end;

end;

suppose A40: dom (f | B) <> {} ; :: thesis:

aa: f | B is nonnegative by A2, Th15;
deffunc H₄( Nat) -> Element of ExtREAL = (b . $1) * ((M * G2) . $1);
consider y2 being FinSequence of ExtREAL such that
A42: ( len y2 = len G2 & ( for j being Nat st j in dom y2 holds
y2 . j = H₄(j) ) ) from FINSEQ_2:sch 1();
A43: for k being Nat st k in dom y2 holds
0 <= y2 . k

proof

let k be Nat; :: thesis:
assume A44: k in dom y2 ; :: thesis:
then k in Seg (len y2) by FINSEQ_1:def 3;
then A45: 1 <= k by FINSEQ_1:1;
A46: dom b = dom G by A5, MESFUNC3:def 1
.= Seg (len y2) by A11, A42, FINSEQ_1:def 3
.= dom y2 by FINSEQ_1:def 3 ;

A47: now :: thesis:

per cases ;

suppose k = 1 ; :: thesis:

hence 0 <= b . k by A6; :: thesis:

end;

suppose k <> 1 ; :: thesis:

then 1 < k by A45, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence 0 <= b . k by A7, A44, A46; :: thesis:

end;

k in Seg (len G2) by A42, A44, FINSEQ_1:def 3;
then A48: k in dom G2 by FINSEQ_1:def 3;
then A49: (M * G2) . k = M . (G2 . k) by FUNCT_1:13;
G2 . k in rng G2 by A48, FUNCT_1:3;
then reconsider G2k = G2 . k as Element of S ;
A50: 0 <= M . G2k by SUPINF_2:39;
y2 . k = (b . k) * ((M * G2) . k) by A42, A44;
hence 0 <= y2 . k by A47, A49, A50; :: thesis:

end;

then for k being object st k in dom y2 holds
0 <= y2 . k ;
then cc: y2 is nonnegative by SUPINF_2:52;
A51: for x being set st x in dom y2 holds
not y2 . x in {-infty}

proof

let x be set ; :: thesis:
assume A52: x in dom y2 ; :: thesis:
then reconsider x = x as Element of NAT ;
0 <= y2 . x by A43, A52;
hence not y2 . x in {-infty} by TARSKI:def 1; :: thesis:

end;

for x being object holds not x in y2 " {-infty}

proof

let x be object ; :: thesis:
( not x in dom y2 or not y2 . x in {-infty} ) by A51;
hence not x in y2 " {-infty} by FUNCT_1:def 7; :: thesis:

end;

then A53: y2 " {-infty} = {} by XBOOLE_0:def 1;
dom y2 = Seg (len G2) by A42, FINSEQ_1:def 3
.= dom G2 by FINSEQ_1:def 3 ;
then integral (M,(f | B)) = Sum y2 by A1, A18, A40, A42, Th34, MESFUNC4:3, aa;
then A54: integral' (M,(f | B)) = Sum y2 by A40, Def14;
ac: f | A is nonnegative by A2, Th15;
deffunc H₅( Nat) -> Element of ExtREAL = (b . $1) * ((M * G1) . $1);
consider y1 being FinSequence of ExtREAL such that
A56: ( len y1 = len G1 & ( for j being Nat st j in dom y1 holds
y1 . j = H₅(j) ) ) from FINSEQ_2:sch 1();
A57: dom y = (Seg (len G)) /\ (Seg (len G)) by A25, FINSEQ_1:def 3
.= (dom y1) /\ (Seg (len G2)) by A8, A11, A56, FINSEQ_1:def 3
.= (dom y1) /\ (dom y2) by A42, FINSEQ_1:def 3 ;
A58: for n being Element of NAT st n in dom y holds
y . n = (y1 . n) + (y2 . n)

proof

let n be Element of NAT ; :: thesis:
assume A59: n in dom y ; :: thesis:
then n in Seg (len G) by A24, FINSEQ_1:def 3;
then A60: n in dom G by FINSEQ_1:def 3;
then A61: G2 . n = (G . n) /\ B by A13;

now :: thesis:

let v be object ; :: thesis:
assume A62: v in G . n ; :: thesis:
G . n in rng G by A60, FUNCT_1:3;
then v in union (rng G) by A62, TARSKI:def 4;
then v in dom (f | (A \/ B)) by A5, MESFUNC3:def 1;
then v in (dom f) /\ (A \/ B) by RELAT_1:61;
hence v in A \/ B by XBOOLE_0:def 4; :: thesis:

end;

then G . n c= A \/ B ;
then A63: G . n = (G . n) /\ (A \/ B) by XBOOLE_1:28
.= ((G . n) /\ A) \/ ((G . n) /\ B) by XBOOLE_1:23
.= (G1 . n) \/ (G2 . n) by A10, A60, A61 ;
A64: n in dom y2 by A57, A59, XBOOLE_0:def 4;
then n in Seg (len G2) by A42, FINSEQ_1:def 3;
then A65: n in dom G2 by FINSEQ_1:def 3;
then G2 . n in rng G2 by FUNCT_1:3;
then reconsider G2n = G2 . n as Element of S ;
0 <= M . G2n by MEASURE1:def 2;
then A66: ( 0 = (M * G2) . n or 0 < (M * G2) . n ) by A65, FUNCT_1:13;

A67: now :: thesis:

assume G1 . n meets G2 . n ; :: thesis:
then consider v being object such that
A68: v in G1 . n and
A69: v in G2 . n by XBOOLE_0:3;
v in (G . n) /\ B by A13, A60, A69;
then A70: v in B by XBOOLE_0:def 4;
v in (G . n) /\ A by A10, A60, A68;
then v in A by XBOOLE_0:def 4;
hence contradiction by A3, A70, XBOOLE_0:3; :: thesis:

end;

A71: n in dom y1 by A57, A59, XBOOLE_0:def 4;
then n in Seg (len G1) by A56, FINSEQ_1:def 3;
then A72: n in dom G1 by FINSEQ_1:def 3;
then G1 . n in rng G1 by FUNCT_1:3;
then reconsider G1n = G1 . n as Element of S ;
0 <= M . G1n by MEASURE1:def 2;
then A73: ( 0 = (M * G1) . n or 0 < (M * G1) . n ) by A72, FUNCT_1:13;
(M * G) . n = M . (G . n) by A60, FUNCT_1:13
.= (M . G1n) + (M . G2n) by A63, A67, MEASURE1:30
.= ((M * G1) . n) + (M . (G2 . n)) by A72, FUNCT_1:13
.= ((M * G1) . n) + ((M * G2) . n) by A65, FUNCT_1:13 ;
then (b . n) * ((M * G) . n) = ((b . n) * ((M * G1) . n)) + ((b . n) * ((M * G2) . n)) by A73, A66, XXREAL_3:96;
then y . n = ((b . n) * ((M * G1) . n)) + ((b . n) * ((M * G2) . n)) by A24, A59;
then y . n = (y1 . n) + ((b . n) * ((M * G2) . n)) by A56, A71;
hence y . n = (y1 . n) + (y2 . n) by A42, A64; :: thesis:

end;

A74: for k being Nat st k in dom y1 holds
0 <= y1 . k

proof

let k be Nat; :: thesis:
assume A75: k in dom y1 ; :: thesis:
then k in Seg (len y1) by FINSEQ_1:def 3;
then A76: 1 <= k by FINSEQ_1:1;
A77: dom b = dom G by A5, MESFUNC3:def 1
.= Seg (len y1) by A8, A56, FINSEQ_1:def 3
.= dom y1 by FINSEQ_1:def 3 ;

A78: now :: thesis:

per cases ;

suppose k = 1 ; :: thesis:

hence 0 <= b . k by A6; :: thesis:

end;

suppose k <> 1 ; :: thesis:

then 1 < k by A76, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
hence 0 <= b . k by A7, A75, A77; :: thesis:

end;

k in Seg (len G1) by A56, A75, FINSEQ_1:def 3;
then A79: k in dom G1 by FINSEQ_1:def 3;
then A80: (M * G1) . k = M . (G1 . k) by FUNCT_1:13;
G1 . k in rng G1 by A79, FUNCT_1:3;
then reconsider G1k = G1 . k as Element of S ;
A81: 0 <= M . G1k by SUPINF_2:39;
y1 . k = (b . k) * ((M * G1) . k) by A56, A75;
hence 0 <= y1 . k by A78, A80, A81; :: thesis:

end;

then for x being object st x in dom y1 holds
0. <= y1 . x ;
then ab: y1 is nonnegative by SUPINF_2:52;
A82: for x being set st x in dom y1 holds
not y1 . x in {-infty}

proof

let x be set ; :: thesis:
assume A83: x in dom y1 ; :: thesis:
then reconsider x = x as Element of NAT ;
0 <= y1 . x by A74, A83;
hence not y1 . x in {-infty} by TARSKI:def 1; :: thesis:

end;

for x being object holds not x in y1 " {-infty}

proof

let x be object ; :: thesis:
( not x in dom y1 or not y1 . x in {-infty} ) by A82;
hence not x in y1 " {-infty} by FUNCT_1:def 7; :: thesis:

end;

then y1 " {-infty} = {} by XBOOLE_0:def 1;
then dom y = ((dom y1) /\ (dom y2)) \ (((y1 " {-infty}) /\ (y2 " {+infty})) \/ ((y1 " {+infty}) /\ (y2 " {-infty}))) by A53, A57;
then A84: y = y1 + y2 by A58, MESFUNC1:def 3;
dom y1 = Seg (len G1) by A56, FINSEQ_1:def 3
.= dom G1 by FINSEQ_1:def 3 ;
then integral (M,(f | A)) = Sum y1 by A1, A23, A35, A56, Th34, MESFUNC4:3, ac;
then A85: integral' (M,(f | A)) = Sum y1 by A35, Def14;
dom y1 = Seg (len y2) by A8, A11, A56, A42, FINSEQ_1:def 3
.= dom y2 by FINSEQ_1:def 3 ;
hence integral' (M,(f | (A \/ B))) = (integral' (M,(f | A))) + (integral' (M,(f | B))) by A30, A85, A54, A84, MESFUNC4:1, ab, cc; :: thesis:

end;