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 H_{1}( Nat) -> Element of bool [:X,ExtREAL:] = (F0 . $1) | B;

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

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

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

( FA # x is convergent & lim (FA # x) = (f | A) . x )

( FB # x is convergent & lim (FB # x) = (f | B) . x )

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

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 H_{3}( 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_{3}(n)
from SEQFUNC:sch 1();

A47: for n being Nat holds

( FA . n is nonnegative & FB . n is nonnegative )

for x being Element of X st x in dom (f | B) holds

(FB . n) . x <= (FB . m) . x_{4}( 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_{4}(n)
from FUNCT_2:sch 4();

deffunc H_{5}( 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_{5}(n)
from FUNCT_2:sch 4();

( ( n in dom KA implies -infty < KA . n ) & ( n in dom KB implies -infty < KB . n ) )

deffunc H_{6}( 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_{6}(n)
from FUNCT_2:sch 4();

for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x

( KA . n <= KA . m & KB . n <= KB . m )

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

KAB . n <= KAB . m

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

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 H

deffunc H

consider FA being Functional_Sequence of X,ExtREAL such that

A8: for n being Nat holds FA . n = H

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

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

then A16:
f | (E /\ B) = f | B
by A12, A13, FUNCT_1:2, RELAT_1:61;
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;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

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

then A21:
f | (E /\ A) = f | A
by A17, A18, FUNCT_1:2, RELAT_1:61;
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;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

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

A26:
for x being Element of X st x in dom (f | A) holds
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;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

( FA # x is convergent & lim (FA # x) = (f | A) . x )

proof

A31:
for x being Element of X st x in dom (f | B) holds
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 )

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

then A29:
FA # x = F0 # x
by FUNCT_2:63;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;(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

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

( FB # x is convergent & lim (FB # x) = (f | B) . x )

proof

set C = E /\ (A \/ B);
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 )

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

then A34:
FB # x = F0 # x
by FUNCT_2:63;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;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

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

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

then A40:
f | (A \/ B) = f | (E /\ (A \/ B))
by A38, FUNCT_1:2;
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;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

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 H

consider FAB being Functional_Sequence of X,ExtREAL such that

A46: for n being Nat holds FAB . n = H

A47: for n being Nat holds

( FA . n is nonnegative & FB . n is nonnegative )

proof

A49:
for n, m being Nat st n <= m holds
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;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

for x being Element of X st x in dom (f | B) holds

(FB . n) . x <= (FB . m) . x

proof

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

consider KA being ExtREAL_sequence such that

A56: for n being Element of NAT holds KA . n = H

deffunc H

consider KB being ExtREAL_sequence such that

A57: for n being Element of NAT holds KB . n = H

A58: now :: thesis: for n being Nat holds KB . n = H_{5}(n)

let n be Nat; :: thesis: KB . n = H_{5}(n)

n in NAT by ORDINAL1:def 12;

hence KB . n = H_{5}(n)
by A57; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence KB . n = H

A59: now :: thesis: for n being Nat holds KA . n = H_{4}(n)

A60:
for n being set holds let n be Nat; :: thesis: KA . n = H_{4}(n)

n in NAT by ORDINAL1:def 12;

hence KA . n = H_{4}(n)
by A56; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence KA . n = H

( ( n in dom KA implies -infty < KA . n ) & ( n in dom KB implies -infty < KB . n ) )

proof

then A63:
KB is ()
by Th10;
let n be set ; :: thesis: ( ( n in dom KA implies -infty < KA . n ) & ( n in dom KB implies -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;hereby :: thesis: ( n in dom KB implies -infty < KB . n )

assume
n in dom KB
; :: thesis: -infty < KB . nassume
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;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

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

deffunc H

consider KAB being ExtREAL_sequence such that

A64: for n being Element of NAT holds KAB . n = H

A65: now :: thesis: for n being Nat holds KAB . n = H_{6}(n)

A66:
for n being Nat holds KAB . n = (KA . n) + (KB . n)
let n be Nat; :: thesis: KAB . n = H_{6}(n)

n in NAT by ORDINAL1:def 12;

hence KAB . n = H_{6}(n)
by A64; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence KAB . n = H

proof

A71:
for n, m being Nat st n <= m holds
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;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

for x being Element of X st x in dom (f | A) holds

(FA . n) . x <= (FA . m) . x

proof

A78:
for n, m being Nat st n <= m holds
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;(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

( KA . n <= KA . m & KB . n <= KB . m )

proof

then A102:
for n, m being Nat st n <= m holds
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

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

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

A85:
FA . m is nonnegative
by A47;
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;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

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

A98:
FB . n is_simple_func_in S
by A22;
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;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

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

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

for n, m being Nat st n <= m holds 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 ) ) )

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

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

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

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

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

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 )

( 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

(FAB . n) . x <= (FAB . m) . x ; :: thesis: verum

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

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

(FAB . n) . x <= (FAB . m) . x ; :: thesis: verum

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;

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

then
FAB # x = F0 # x
by FUNCT_2:63;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;thus (FAB # x) . n = (FAB . n) . x by Def13

.= (F0 . n) . x by A106, A112

.= (F0 # x) . n by Def13 ; :: thesis: verum

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

KAB . n <= KAB . m

proof

then A127:
KAB is convergent
by Th54;
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

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

A119:
KAB . m = integral' (M,(FAB . m))
by A65;
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;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

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

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