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 f is_simple_func_in S & 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 f is_simple_func_in S & 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 f is_simple_func_in S & 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 f is_simple_func_in S & 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: ( f is_simple_func_in S & f is nonnegative & A misses B implies integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B)) )
assume that
A1: f is_simple_func_in S and
A2: f is nonnegative and
A3: A misses B ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))
set g2 = f | B;
set g1 = f | A;
set g = f | (A \/ B);
f | (A \/ B) is nonnegative by A2, Th21;
then A4: for x being set st x in dom (f | (A \/ B)) holds
0 <= (f | (A \/ B)) . x by SUPINF_2:70;
then 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, Th40, MESFUNC3:14;
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: ( k in dom G implies G1 . k = (G . k) /\ A )
assume k in dom G ; :: thesis: G1 . k = (G . k) /\ A
then k in Seg (len G) by FINSEQ_1:def 3;
hence G1 . k = (G . k) /\ A by A8, A9; :: thesis: verum

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: ( k in dom G implies G2 . k = (G . k) /\ B )
assume k in dom G ; :: thesis: G2 . k = (G . k) /\ B
then k in Seg (len G) by FINSEQ_1:def 3;
hence G2 . k = (G . k) /\ B by A11, A12; :: thesis: verum

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, Th41;
A15: dom ((f | (A \/ B)) | B) = (dom (f | (A \/ B))) /\ B by RELAT_1:90
.= ((dom f) /\ (A \/ B)) /\ B by RELAT_1:90
.= (dom f) /\ ((A \/ B) /\ B) by XBOOLE_1:16
.= (dom f) /\ B by XBOOLE_1:21
.= dom (f | B) by RELAT_1:90 ;
for x being set st x in dom ((f | (A \/ B)) | B) holds
((f | (A \/ B)) | B) . x = (f | B) . x

proof

let x be set ; :: thesis: ( x in dom ((f | (A \/ B)) | B) implies ((f | (A \/ B)) | B) . x = (f | B) . x )
assume A16: x in dom ((f | (A \/ B)) | B) ; :: thesis: ((f | (A \/ B)) | B) . x = (f | B) . x
then x in (dom (f | (A \/ B))) /\ B by RELAT_1:90;
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:70
.= f . x by A17, FUNCT_1:70 ;
hence ((f | (A \/ B)) | B) . x = (f | B) . x by A15, A16, FUNCT_1:70; :: thesis: verum

end;

then (f | (A \/ B)) | B = f | B by A15, FUNCT_1:9;
then A18: G2,b are_Re-presentation_of f | B by A5, A14, A13, Th42;
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, Th41;
A20: dom ((f | (A \/ B)) | A) = (dom (f | (A \/ B))) /\ A by RELAT_1:90
.= ((dom f) /\ (A \/ B)) /\ A by RELAT_1:90
.= (dom f) /\ ((A \/ B) /\ A) by XBOOLE_1:16
.= (dom f) /\ A by XBOOLE_1:21
.= dom (f | A) by RELAT_1:90 ;
for x being set st x in dom ((f | (A \/ B)) | A) holds
((f | (A \/ B)) | A) . x = (f | A) . x

proof

let x be set ; :: thesis: ( x in dom ((f | (A \/ B)) | A) implies ((f | (A \/ B)) | A) . x = (f | A) . x )
assume A21: x in dom ((f | (A \/ B)) | A) ; :: thesis: ((f | (A \/ B)) | A) . x = (f | A) . x
then x in (dom (f | (A \/ B))) /\ A by RELAT_1:90;
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:70
.= f . x by A22, FUNCT_1:70 ;
hence ((f | (A \/ B)) | A) . x = (f | A) . x by A20, A21, FUNCT_1:70; :: thesis: verum

end;

then (f | (A \/ B)) | A = f | A by A20, FUNCT_1:9;
then A23: G1,b are_Re-presentation_of f | A by A5, A19, A10, Th42;
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 ( dom (f | (A \/ B)) = {} or dom (f | (A \/ B)) <> {} ) ;

suppose A26: dom (f | (A \/ B)) = {} ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))

(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:90;
then dom (f | B) c= dom (f | (A \/ B)) by RELAT_1:90;
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:90;
then dom (f | A) c= dom (f | (A \/ B)) by RELAT_1:90;
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: verum

end;

suppose A29: dom (f | (A \/ B)) <> {} ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))

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

per cases ( dom (f | A) = {} or dom (f | A) <> {} ) ;

suppose A31: dom (f | A) = {} ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))

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

now

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

end;

then A34: f | (A \/ B) = f | B by A32, FUNCT_1:9;
integral' M,(f | A) = 0 by A31, Def14;
hence integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B)) by A34, XXREAL_3:4; :: thesis: verum

end;

suppose A35: dom (f | A) <> {} ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))

per cases ( dom (f | B) = {} or dom (f | B) <> {} ) ;

suppose A36: dom (f | B) = {} ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))

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

now

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

end;

then A39: f | (A \/ B) = f | A by A37, FUNCT_1:9;
integral' M,(f | B) = 0 by A36, Def14;
hence integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B)) by A39, XXREAL_3:4; :: thesis: verum

end;

suppose A40: dom (f | B) <> {} ; :: thesis: integral' M,(f | (A \/ B)) = (integral' M,(f | A)) + (integral' M,(f | B))

f | B is nonnegative by A2, Th21;
then A41: for x being set st x in dom (f | B) holds
0 <= (f | B) . x by SUPINF_2:70;
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: ( k in dom y2 implies 0 <= y2 . k )
assume A44: k in dom y2 ; :: thesis: 0 <= y2 . k
then k in Seg (len y2) by FINSEQ_1:def 3;
then A45: 1 <= k by FINSEQ_1:3;
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

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: 0 <= b . k

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

end;

suppose k <> 1 ; :: thesis: 0 <= b . k

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: verum

end;

end;

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:23;
G2 . k in rng G2 by A48, FUNCT_1:12;
then reconsider G2k = G2 . k as Element of S ;
A50: 0 <= M . G2k by SUPINF_2:58;
y2 . k = (b . k) * ((M * G2) . k) by A42, A44;
hence 0 <= y2 . k by A47, A49, A50; :: thesis: verum

end;

A51: for x being set st x in dom y2 holds
not y2 . x in {-infty }

proof

let x be set ; :: thesis: ( x in dom y2 implies not y2 . x in {-infty } )
assume A52: x in dom y2 ; :: thesis: not y2 . x in {-infty }
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: verum

end;

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

proof

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

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 X,S,M,(f | B) = Sum y2 by A1, A18, A40, A41, A42, Th40, MESFUNC4:3;
then A54: integral' M,(f | B) = Sum y2 by A40, Def14;
f | A is nonnegative by A2, Th21;
then A55: for x being set st x in dom (f | A) holds
0 <= (f | A) . x by SUPINF_2:70;
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: ( n in dom y implies y . n = (y1 . n) + (y2 . n) )
assume A59: n in dom y ; :: thesis: y . n = (y1 . n) + (y2 . n)
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

let v be set ; :: thesis: ( v in G . n implies v in A \/ B )
assume A62: v in G . n ; :: thesis: v in A \/ B
G . n in rng G by A60, FUNCT_1:12;
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:90;
hence v in A \/ B by XBOOLE_0:def 4; :: thesis: verum

end;

then G . n c= A \/ B by TARSKI:def 3;
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:12;
then reconsider G2n = G2 . n as Element of S ;
0 <= M . G2n by MEASURE1:def 4;
then A66: ( 0 = (M * G2) . n or 0 < (M * G2) . n ) by A65, FUNCT_1:23;

A67: now

assume G1 . n meets G2 . n ; :: thesis: contradiction
then consider v being set 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: verum

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:12;
then reconsider G1n = G1 . n as Element of S ;
0 <= M . G1n by MEASURE1:def 4;
then A73: ( 0 = (M * G1) . n or 0 < (M * G1) . n ) by A72, FUNCT_1:23;
(M * G) . n = M . (G . n) by A60, FUNCT_1:23
.= (M . G1n) + (M . G2n) by A63, A67, MEASURE1:61
.= ((M * G1) . n) + (M . (G2 . n)) by A72, FUNCT_1:23
.= ((M * G1) . n) + ((M * G2) . n) by A65, FUNCT_1:23 ;
then (b . n) * ((M * G) . n) = ((b . n) * ((M * G1) . n)) + ((b . n) * ((M * G2) . n)) by A73, A66, XXREAL_3:107;
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: verum

end;

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

proof

let k be Nat; :: thesis: ( k in dom y1 implies 0 <= y1 . k )
assume A75: k in dom y1 ; :: thesis: 0 <= y1 . k
then k in Seg (len y1) by FINSEQ_1:def 3;
then A76: 1 <= k by FINSEQ_1:3;
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

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: 0 <= b . k

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

end;

suppose k <> 1 ; :: thesis: 0 <= b . k

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: verum

end;

end;

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:23;
G1 . k in rng G1 by A79, FUNCT_1:12;
then reconsider G1k = G1 . k as Element of S ;
A81: 0 <= M . G1k by SUPINF_2:58;
y1 . k = (b . k) * ((M * G1) . k) by A56, A75;
hence 0 <= y1 . k by A78, A80, A81; :: thesis: verum

end;

A82: for x being set st x in dom y1 holds
not y1 . x in {-infty }

proof

let x be set ; :: thesis: ( x in dom y1 implies not y1 . x in {-infty } )
assume A83: x in dom y1 ; :: thesis: not y1 . x in {-infty }
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: verum

end;

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

proof

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

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 X,S,M,(f | A) = Sum y1 by A1, A23, A35, A55, A56, Th40, MESFUNC4:3;
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, A74, A43, A84, MESFUNC4:1; :: thesis: verum

end;

end;

end;

end;

end;

end;