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);

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_{1}( 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_{1}(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_{2}( 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_{2}(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

.= 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

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

then A23: G1,b are_Re-presentation_of f | A by A5, A19, A10, Th36;

deffunc H_{3}( 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_{3}(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 ;

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);

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

consider G1 being FinSequence such that

A8: ( len G1 = len G & ( for k being Nat st k in dom G1 holds

G1 . k = H

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

deffunc H
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;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

consider G2 being FinSequence such that

A11: ( len G2 = len G & ( for k being Nat st k in dom G2 holds

G2 . k = H

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

A14: dom G =
Seg (len G2)
by A11, FINSEQ_1:def 3
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;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

.= 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

then
(f | (A \/ B)) | B = f | B
by A15, FUNCT_1:2;
let x be object ; :: 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: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: verum

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

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

then
(f | (A \/ B)) | A = f | A
by A20, FUNCT_1:2;
let x be object ; :: 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: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: verum

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

then A23: G1,b are_Re-presentation_of f | A by A5, A19, A10, Th36;

deffunc H

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

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)) <> {} )
;

end;

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

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

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

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;

end;then A30: integral' (M,(f | (A \/ B))) = Sum y by A29, Def14;

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

end;

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

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;.= ((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: for x being object st x in dom (f | (A \/ B)) holds

(f | (A \/ B)) . x = (f | B) . x

then A34:
f | (A \/ B) = f | B
by A32, FUNCT_1:2;(f | (A \/ B)) . x = (f | B) . x

let x be object ; :: 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:47;

hence (f | (A \/ B)) . x = (f | B) . x by A32, A33, FUNCT_1:47; :: thesis: verum

end;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:47;

hence (f | (A \/ B)) . x = (f | B) . x by A32, A33, FUNCT_1:47; :: thesis: verum

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

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

end;

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

end;

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

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;.= ((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: for x being object st x in dom (f | (A \/ B)) holds

(f | (A \/ B)) . x = (f | A) . x

then A39:
f | (A \/ B) = f | A
by A37, FUNCT_1:2;(f | (A \/ B)) . x = (f | A) . x

let x be object ; :: 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:47;

hence (f | (A \/ B)) . x = (f | A) . x by A37, A38, FUNCT_1:47; :: thesis: verum

end;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:47;

hence (f | (A \/ B)) . x = (f | A) . x by A37, A38, FUNCT_1:47; :: thesis: verum

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

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

aa:
f | B is nonnegative
by A2, Th15;

deffunc H_{4}( 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_{4}(j) ) )
from FINSEQ_2:sch 1();

A43: for k being Nat st k in dom y2 holds

0 <= y2 . k

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}

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_{5}( 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_{5}(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)

0 <= y1 . k

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}

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

end;deffunc H

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

A43: for k being Nat st k in dom y2 holds

0 <= y2 . k

proof

then
for k being object st k in dom y2 holds
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: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 ;

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

end;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: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 ;

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

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

for x being object holds not x in y2 " {-infty}
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;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

proof

then A53:
y2 " {-infty} = {}
by XBOOLE_0:def 1;
let x be object ; :: 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 7; :: thesis: verum

end;( 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: verum

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

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

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

A74:
for k being Nat st k in dom y1 holds
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;

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;

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

end;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 :: thesis: for v being object st v in G . n holds

v in A \/ B

then
G . n c= A \/ B
;v in A \/ B

let v be object ; :: 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: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: verum

end;assume A62: v in G . n ; :: thesis: v in A \/ B

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

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: not G1 . n meets G2 . n

A71:
n in dom y1
by A57, A59, XBOOLE_0:def 4;assume
G1 . n meets G2 . n
; :: thesis: contradiction

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

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

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

0 <= y1 . k

proof

then
for x being object st x in dom y1 holds
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: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 ;

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

end;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: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 ;

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

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

for x being object holds not x in y1 " {-infty}
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;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

proof

then
y1 " {-infty} = {}
by XBOOLE_0:def 1;
let x be object ; :: 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 7; :: thesis: verum

end;( 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: verum

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