let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds

integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds

integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds

integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative implies integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g)) )

assume that

A1: ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) and

A2: f is nonnegative and

A3: g is nonnegative ; :: thesis: integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that

A4: for n being Nat holds

( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) and

A5: for n being Nat holds F1 . 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

(F1 . n) . x <= (F1 . m) . x and

A7: for x being Element of X st x in dom f holds

( F1 # x is convergent & lim (F1 # x) = f . x ) and

A8: for n being Nat holds K1 . n = integral' (M,(F1 . n)) and

K1 is convergent and

A9: integral+ (M,f) = lim K1 by A1, A2, Def15;

A10: f + g is nonnegative by A2, A3, Th19;

consider A being Element of S such that

A11: A = dom f and

A12: A = dom g and

A13: f is A -measurable and

A14: g is A -measurable by A1;

A = (dom f) /\ (dom g) by A11, A12;

then A15: A = dom (f + g) by A2, A3, Th16;

A16: for n, m being Nat st n <= m holds

K1 . n <= K1 . m

A29: for n being Nat holds

( F2 . n is_simple_func_in S & dom (F2 . n) = dom g ) and

A30: for n being Nat holds F2 . n is nonnegative and

A31: for n, m being Nat st n <= m holds

for x being Element of X st x in dom g holds

(F2 . n) . x <= (F2 . m) . x and

A32: for x being Element of X st x in dom g holds

( F2 # x is convergent & lim (F2 # x) = g . x ) and

A33: for n being Nat holds K2 . n = integral' (M,(F2 . n)) and

K2 is convergent and

A34: integral+ (M,g) = lim K2 by A1, A3, Def15;

deffunc H_{1}( Nat) -> Element of bool [:X,ExtREAL:] = (F1 . $1) + (F2 . $1);

consider F being Functional_Sequence of X,ExtREAL such that

A35: for n being Nat holds F . n = H_{1}(n)
from SEQFUNC:sch 1();

A36: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom (f + g) & F . n is nonnegative )

for x being Element of X st x in dom (f + g) holds

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

deffunc H_{2}( Nat) -> Element of ExtREAL = integral' (M,(F . $1));

consider K being ExtREAL_sequence such that

A55: for n being Element of NAT holds K . n = H_{2}(n)
from FUNCT_2:sch 4();

K2 . n <= K2 . m

then A81: lim K = (lim K1) + (lim K2) by A16, A54, A66, A57, Th61;

A82: for x being Element of X st x in dom (f + g) holds

( F # x is convergent & lim (F # x) = (f + g) . x )

K is convergent by A80, A16, A54, A66, A57, Th61;

hence integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g)) by A9, A34, A97, A15, A10, A56, A36, A45, A82, A81, Def15; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds

integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds

integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative holds

integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) & f is nonnegative & g is nonnegative implies integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g)) )

assume that

A1: ex A being Element of S st

( A = dom f & A = dom g & f is A -measurable & g is A -measurable ) and

A2: f is nonnegative and

A3: g is nonnegative ; :: thesis: integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g))

consider F1 being Functional_Sequence of X,ExtREAL, K1 being ExtREAL_sequence such that

A4: for n being Nat holds

( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) and

A5: for n being Nat holds F1 . 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

(F1 . n) . x <= (F1 . m) . x and

A7: for x being Element of X st x in dom f holds

( F1 # x is convergent & lim (F1 # x) = f . x ) and

A8: for n being Nat holds K1 . n = integral' (M,(F1 . n)) and

K1 is convergent and

A9: integral+ (M,f) = lim K1 by A1, A2, Def15;

A10: f + g is nonnegative by A2, A3, Th19;

consider A being Element of S such that

A11: A = dom f and

A12: A = dom g and

A13: f is A -measurable and

A14: g is A -measurable by A1;

A = (dom f) /\ (dom g) by A11, A12;

then A15: A = dom (f + g) by A2, A3, Th16;

A16: for n, m being Nat st n <= m holds

K1 . n <= K1 . m

proof

consider F2 being Functional_Sequence of X,ExtREAL, K2 being ExtREAL_sequence such that
let n, m be Nat; :: thesis: ( n <= m implies K1 . n <= K1 . m )

assume A17: n <= m ; :: thesis: K1 . n <= K1 . m

A18: dom (F1 . m) = dom f by A4;

A19: dom (F1 . n) = dom f by A4;

A22: F1 . n is nonnegative by A5;

A23: K1 . m = integral' (M,(F1 . m)) by A8;

A24: K1 . n = integral' (M,(F1 . n)) by A8;

A25: F1 . m is_simple_func_in S by A4;

A26: F1 . n is_simple_func_in S by A4;

then A27: dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A25, A22, A21, A20, Th69;

then A28: (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m by A19, A18, GRFUNC_1:23;

(F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n by A19, A18, A27, GRFUNC_1:23;

hence K1 . n <= K1 . m by A24, A23, A26, A25, A22, A21, A20, A28, Th70; :: thesis: verum

end;assume A17: n <= m ; :: thesis: K1 . n <= K1 . m

A18: dom (F1 . m) = dom f by A4;

A19: dom (F1 . n) = dom f by A4;

A20: now :: thesis: for x being object st x in dom ((F1 . m) - (F1 . n)) holds

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

A21:
F1 . m is nonnegative
by A5;(F1 . n) . x <= (F1 . m) . x

let x be object ; :: thesis: ( x in dom ((F1 . m) - (F1 . n)) implies (F1 . n) . x <= (F1 . m) . x )

assume x in dom ((F1 . m) - (F1 . n)) ; :: thesis: (F1 . n) . x <= (F1 . m) . x

then x in ((dom (F1 . m)) /\ (dom (F1 . n))) \ ((((F1 . m) " {+infty}) /\ ((F1 . n) " {+infty})) \/ (((F1 . m) " {-infty}) /\ ((F1 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F1 . m)) /\ (dom (F1 . n)) by XBOOLE_0:def 5;

hence (F1 . n) . x <= (F1 . m) . x by A6, A17, A19, A18; :: thesis: verum

end;assume x in dom ((F1 . m) - (F1 . n)) ; :: thesis: (F1 . n) . x <= (F1 . m) . x

then x in ((dom (F1 . m)) /\ (dom (F1 . n))) \ ((((F1 . m) " {+infty}) /\ ((F1 . n) " {+infty})) \/ (((F1 . m) " {-infty}) /\ ((F1 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F1 . m)) /\ (dom (F1 . n)) by XBOOLE_0:def 5;

hence (F1 . n) . x <= (F1 . m) . x by A6, A17, A19, A18; :: thesis: verum

A22: F1 . n is nonnegative by A5;

A23: K1 . m = integral' (M,(F1 . m)) by A8;

A24: K1 . n = integral' (M,(F1 . n)) by A8;

A25: F1 . m is_simple_func_in S by A4;

A26: F1 . n is_simple_func_in S by A4;

then A27: dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A25, A22, A21, A20, Th69;

then A28: (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m by A19, A18, GRFUNC_1:23;

(F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n by A19, A18, A27, GRFUNC_1:23;

hence K1 . n <= K1 . m by A24, A23, A26, A25, A22, A21, A20, A28, Th70; :: thesis: verum

A29: for n being Nat holds

( F2 . n is_simple_func_in S & dom (F2 . n) = dom g ) and

A30: for n being Nat holds F2 . n is nonnegative and

A31: for n, m being Nat st n <= m holds

for x being Element of X st x in dom g holds

(F2 . n) . x <= (F2 . m) . x and

A32: for x being Element of X st x in dom g holds

( F2 # x is convergent & lim (F2 # x) = g . x ) and

A33: for n being Nat holds K2 . n = integral' (M,(F2 . n)) and

K2 is convergent and

A34: integral+ (M,g) = lim K2 by A1, A3, Def15;

deffunc H

consider F being Functional_Sequence of X,ExtREAL such that

A35: for n being Nat holds F . n = H

A36: for n being Nat holds

( F . n is_simple_func_in S & dom (F . n) = dom (f + g) & F . n is nonnegative )

proof

A45:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: ( F . n is_simple_func_in S & dom (F . n) = dom (f + g) & F . n is nonnegative )

A37: dom (F1 . n) = dom f by A4;

A38: F2 . n is_simple_func_in S by A29;

A39: F2 . n is nonnegative by A30;

A40: F . n = (F1 . n) + (F2 . n) by A35;

A41: F1 . n is_simple_func_in S by A4;

hence F . n is_simple_func_in S by A38, A40, Th38; :: thesis: ( dom (F . n) = dom (f + g) & F . n is nonnegative )

A42: dom (F2 . n) = dom g by A29;

F1 . n is nonnegative by A5;

then dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n)) by A41, A38, A39, A40, Th65;

hence dom (F . n) = dom (f + g) by A2, A3, A37, A42, Th16; :: thesis: F . n is nonnegative

A43: F2 . n is nonnegative by A30;

A44: F . n = (F1 . n) + (F2 . n) by A35;

F1 . n is nonnegative by A5;

hence F . n is nonnegative by A43, A44, Th19; :: thesis: verum

end;A37: dom (F1 . n) = dom f by A4;

A38: F2 . n is_simple_func_in S by A29;

A39: F2 . n is nonnegative by A30;

A40: F . n = (F1 . n) + (F2 . n) by A35;

A41: F1 . n is_simple_func_in S by A4;

hence F . n is_simple_func_in S by A38, A40, Th38; :: thesis: ( dom (F . n) = dom (f + g) & F . n is nonnegative )

A42: dom (F2 . n) = dom g by A29;

F1 . n is nonnegative by A5;

then dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n)) by A41, A38, A39, A40, Th65;

hence dom (F . n) = dom (f + g) by A2, A3, A37, A42, Th16; :: thesis: F . n is nonnegative

A43: F2 . n is nonnegative by A30;

A44: F . n = (F1 . n) + (F2 . n) by A35;

F1 . n is nonnegative by A5;

hence F . n is nonnegative by A43, A44, Th19; :: thesis: verum

for x being Element of X st x in dom (f + g) holds

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

proof

let n, m be Nat; :: thesis: ( n <= m implies for x being Element of X st x in dom (f + g) holds

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

assume A46: n <= m ; :: thesis: for x being Element of X st x in dom (f + g) holds

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

dom ((F1 . m) + (F2 . m)) = dom (F . m) by A35;

then A47: dom ((F1 . m) + (F2 . m)) = dom (f + g) by A36;

dom ((F1 . n) + (F2 . n)) = dom (F . n) by A35;

then A48: dom ((F1 . n) + (F2 . n)) = dom (f + g) by A36;

let x be Element of X; :: thesis: ( x in dom (f + g) implies (F . n) . x <= (F . m) . x )

assume A49: x in dom (f + g) ; :: thesis: (F . n) . x <= (F . m) . x

then A50: (F2 . n) . x <= (F2 . m) . x by A31, A12, A15, A46;

(F . m) . x = ((F1 . m) + (F2 . m)) . x by A35;

then A51: (F . m) . x = ((F1 . m) . x) + ((F2 . m) . x) by A49, A47, MESFUNC1:def 3;

(F . n) . x = ((F1 . n) + (F2 . n)) . x by A35;

then A52: (F . n) . x = ((F1 . n) . x) + ((F2 . n) . x) by A49, A48, MESFUNC1:def 3;

(F1 . n) . x <= (F1 . m) . x by A6, A11, A15, A46, A49;

hence (F . n) . x <= (F . m) . x by A52, A51, A50, XXREAL_3:36; :: thesis: verum

end;(F . n) . x <= (F . m) . x )

assume A46: n <= m ; :: thesis: for x being Element of X st x in dom (f + g) holds

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

dom ((F1 . m) + (F2 . m)) = dom (F . m) by A35;

then A47: dom ((F1 . m) + (F2 . m)) = dom (f + g) by A36;

dom ((F1 . n) + (F2 . n)) = dom (F . n) by A35;

then A48: dom ((F1 . n) + (F2 . n)) = dom (f + g) by A36;

let x be Element of X; :: thesis: ( x in dom (f + g) implies (F . n) . x <= (F . m) . x )

assume A49: x in dom (f + g) ; :: thesis: (F . n) . x <= (F . m) . x

then A50: (F2 . n) . x <= (F2 . m) . x by A31, A12, A15, A46;

(F . m) . x = ((F1 . m) + (F2 . m)) . x by A35;

then A51: (F . m) . x = ((F1 . m) . x) + ((F2 . m) . x) by A49, A47, MESFUNC1:def 3;

(F . n) . x = ((F1 . n) + (F2 . n)) . x by A35;

then A52: (F . n) . x = ((F1 . n) . x) + ((F2 . n) . x) by A49, A48, MESFUNC1:def 3;

(F1 . n) . x <= (F1 . m) . x by A6, A11, A15, A46, A49;

hence (F . n) . x <= (F . m) . x by A52, A51, A50, XXREAL_3:36; :: thesis: verum

now :: thesis: for n being set st n in dom K2 holds

-infty < K2 . n

then A54:
K2 is ()
by Th10;-infty < K2 . n

let n be set ; :: thesis: ( n in dom K2 implies -infty < K2 . n )

assume n in dom K2 ; :: thesis: -infty < K2 . n

then reconsider n1 = n as Element of NAT ;

A53: F2 . n1 is_simple_func_in S by A29;

K2 . n1 = integral' (M,(F2 . n1)) by A33;

hence -infty < K2 . n by A30, A53, Th68; :: thesis: verum

end;assume n in dom K2 ; :: thesis: -infty < K2 . n

then reconsider n1 = n as Element of NAT ;

A53: F2 . n1 is_simple_func_in S by A29;

K2 . n1 = integral' (M,(F2 . n1)) by A33;

hence -infty < K2 . n by A30, A53, Th68; :: thesis: verum

deffunc H

consider K being ExtREAL_sequence such that

A55: for n being Element of NAT holds K . n = H

A56: now :: thesis: for n being Nat holds K . n = H_{2}(n)

A57:
for n being Nat holds K . n = (K1 . n) + (K2 . n)
let n be Nat; :: thesis: K . n = H_{2}(n)

n in NAT by ORDINAL1:def 12;

hence K . n = H_{2}(n)
by A55; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence K . n = H

proof

A66:
for n, m being Nat st n <= m holds
let n be Nat; :: thesis: K . n = (K1 . n) + (K2 . n)

A58: F1 . n is nonnegative by A5;

A59: F . n = (F1 . n) + (F2 . n) by A35;

A60: dom (F1 . n) = dom f by A4

.= dom (F2 . n) by A29, A11, A12 ;

A61: F2 . n is_simple_func_in S by A29;

A62: K . n = integral' (M,(F . n)) by A56;

A63: F2 . n is nonnegative by A30;

A64: F1 . n is_simple_func_in S by A4;

then dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n)) by A58, A61, A63, A59, Th65;

then K . n = (integral' (M,((F1 . n) | (dom (F1 . n))))) + (integral' (M,((F2 . n) | (dom (F2 . n))))) by A64, A58, A61, A63, A59, A60, A62, Th65;

then K . n = (integral' (M,(F1 . n))) + (integral' (M,((F2 . n) | (dom (F2 . n))))) by GRFUNC_1:23;

then A65: K . n = (integral' (M,(F1 . n))) + (integral' (M,(F2 . n))) by GRFUNC_1:23;

K2 . n = integral' (M,(F2 . n)) by A33;

hence K . n = (K1 . n) + (K2 . n) by A8, A65; :: thesis: verum

end;A58: F1 . n is nonnegative by A5;

A59: F . n = (F1 . n) + (F2 . n) by A35;

A60: dom (F1 . n) = dom f by A4

.= dom (F2 . n) by A29, A11, A12 ;

A61: F2 . n is_simple_func_in S by A29;

A62: K . n = integral' (M,(F . n)) by A56;

A63: F2 . n is nonnegative by A30;

A64: F1 . n is_simple_func_in S by A4;

then dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n)) by A58, A61, A63, A59, Th65;

then K . n = (integral' (M,((F1 . n) | (dom (F1 . n))))) + (integral' (M,((F2 . n) | (dom (F2 . n))))) by A64, A58, A61, A63, A59, A60, A62, Th65;

then K . n = (integral' (M,(F1 . n))) + (integral' (M,((F2 . n) | (dom (F2 . n))))) by GRFUNC_1:23;

then A65: K . n = (integral' (M,(F1 . n))) + (integral' (M,(F2 . n))) by GRFUNC_1:23;

K2 . n = integral' (M,(F2 . n)) by A33;

hence K . n = (K1 . n) + (K2 . n) by A8, A65; :: thesis: verum

K2 . n <= K2 . m

proof

let n, m be Nat; :: thesis: ( n <= m implies K2 . n <= K2 . m )

assume A67: n <= m ; :: thesis: K2 . n <= K2 . m

A68: dom (F2 . m) = dom g by A29;

A69: dom (F2 . n) = dom g by A29;

A72: F2 . n is nonnegative by A30;

A73: K2 . m = integral' (M,(F2 . m)) by A33;

A74: K2 . n = integral' (M,(F2 . n)) by A33;

A75: F2 . m is_simple_func_in S by A29;

A76: F2 . n is_simple_func_in S by A29;

then A77: dom ((F2 . m) - (F2 . n)) = (dom (F2 . m)) /\ (dom (F2 . n)) by A75, A72, A71, A70, Th69;

then A78: (F2 . m) | (dom ((F2 . m) - (F2 . n))) = F2 . m by A69, A68, GRFUNC_1:23;

(F2 . n) | (dom ((F2 . m) - (F2 . n))) = F2 . n by A69, A68, A77, GRFUNC_1:23;

hence K2 . n <= K2 . m by A74, A73, A76, A75, A72, A71, A70, A78, Th70; :: thesis: verum

end;assume A67: n <= m ; :: thesis: K2 . n <= K2 . m

A68: dom (F2 . m) = dom g by A29;

A69: dom (F2 . n) = dom g by A29;

A70: now :: thesis: for x being object st x in dom ((F2 . m) - (F2 . n)) holds

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

A71:
F2 . m is nonnegative
by A30;(F2 . n) . x <= (F2 . m) . x

let x be object ; :: thesis: ( x in dom ((F2 . m) - (F2 . n)) implies (F2 . n) . x <= (F2 . m) . x )

assume x in dom ((F2 . m) - (F2 . n)) ; :: thesis: (F2 . n) . x <= (F2 . m) . x

then x in ((dom (F2 . m)) /\ (dom (F2 . n))) \ ((((F2 . m) " {+infty}) /\ ((F2 . n) " {+infty})) \/ (((F2 . m) " {-infty}) /\ ((F2 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F2 . m)) /\ (dom (F2 . n)) by XBOOLE_0:def 5;

hence (F2 . n) . x <= (F2 . m) . x by A31, A67, A69, A68; :: thesis: verum

end;assume x in dom ((F2 . m) - (F2 . n)) ; :: thesis: (F2 . n) . x <= (F2 . m) . x

then x in ((dom (F2 . m)) /\ (dom (F2 . n))) \ ((((F2 . m) " {+infty}) /\ ((F2 . n) " {+infty})) \/ (((F2 . m) " {-infty}) /\ ((F2 . n) " {-infty}))) by MESFUNC1:def 4;

then x in (dom (F2 . m)) /\ (dom (F2 . n)) by XBOOLE_0:def 5;

hence (F2 . n) . x <= (F2 . m) . x by A31, A67, A69, A68; :: thesis: verum

A72: F2 . n is nonnegative by A30;

A73: K2 . m = integral' (M,(F2 . m)) by A33;

A74: K2 . n = integral' (M,(F2 . n)) by A33;

A75: F2 . m is_simple_func_in S by A29;

A76: F2 . n is_simple_func_in S by A29;

then A77: dom ((F2 . m) - (F2 . n)) = (dom (F2 . m)) /\ (dom (F2 . n)) by A75, A72, A71, A70, Th69;

then A78: (F2 . m) | (dom ((F2 . m) - (F2 . n))) = F2 . m by A69, A68, GRFUNC_1:23;

(F2 . n) | (dom ((F2 . m) - (F2 . n))) = F2 . n by A69, A68, A77, GRFUNC_1:23;

hence K2 . n <= K2 . m by A74, A73, A76, A75, A72, A71, A70, A78, Th70; :: thesis: verum

now :: thesis: for n being set st n in dom K1 holds

-infty < K1 . n

then A80:
K1 is ()
by Th10;-infty < K1 . n

let n be set ; :: thesis: ( n in dom K1 implies -infty < K1 . n )

assume n in dom K1 ; :: thesis: -infty < K1 . n

then reconsider n1 = n as Element of NAT ;

A79: F1 . n1 is_simple_func_in S by A4;

K1 . n1 = integral' (M,(F1 . n1)) by A8;

hence -infty < K1 . n by A5, A79, Th68; :: thesis: verum

end;assume n in dom K1 ; :: thesis: -infty < K1 . n

then reconsider n1 = n as Element of NAT ;

A79: F1 . n1 is_simple_func_in S by A4;

K1 . n1 = integral' (M,(F1 . n1)) by A8;

hence -infty < K1 . n by A5, A79, Th68; :: thesis: verum

then A81: lim K = (lim K1) + (lim K2) by A16, A54, A66, A57, Th61;

A82: for x being Element of X st x in dom (f + g) holds

( F # x is convergent & lim (F # x) = (f + g) . x )

proof

A97:
f + g is A -measurable
by A2, A3, A13, A14, Th31;
let x be Element of X; :: thesis: ( x in dom (f + g) implies ( F # x is convergent & lim (F # x) = (f + g) . x ) )

assume A87: x in dom (f + g) ; :: thesis: ( F # x is convergent & lim (F # x) = (f + g) . x )

then (lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (lim (F2 # x)) by A7, A11, A15;

then (lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (g . x) by A32, A12, A15, A87;

then A88: (lim (F1 # x)) + (lim (F2 # x)) = (f + g) . x by A87, MESFUNC1:def 3;

hence ( F # x is convergent & lim (F # x) = (f + g) . x ) by A95, A86, A92, A89, A88, Th61; :: thesis: verum

end;A83: now :: thesis: for n being set holds

( ( n in dom (F1 # x) implies -infty < (F1 # x) . n ) & ( n in dom (F2 # x) implies -infty < (F2 # x) . n ) )

then A86:
F2 # x is ()
by Th10;( ( n in dom (F1 # x) implies -infty < (F1 # x) . n ) & ( n in dom (F2 # x) implies -infty < (F2 # x) . n ) )

let n be set ; :: thesis: ( ( n in dom (F1 # x) implies -infty < (F1 # x) . n ) & ( n in dom (F2 # x) implies -infty < (F2 # x) . n ) )

then reconsider n1 = n as Element of NAT ;

A85: (F2 # x) . n1 = (F2 . n1) . x by Def13;

F2 . n1 is nonnegative by A30;

hence -infty < (F2 # x) . n by A85, Def5; :: thesis: verum

end;hereby :: thesis: ( n in dom (F2 # x) implies -infty < (F2 # x) . n )

assume
n in dom (F2 # x)
; :: thesis: -infty < (F2 # x) . nassume
n in dom (F1 # x)
; :: thesis: -infty < (F1 # x) . n

then reconsider n1 = n as Element of NAT ;

A84: (F1 # x) . n1 = (F1 . n1) . x by Def13;

F1 . n1 is nonnegative by A5;

hence -infty < (F1 # x) . n by A84, Def5; :: thesis: verum

end;then reconsider n1 = n as Element of NAT ;

A84: (F1 # x) . n1 = (F1 . n1) . x by Def13;

F1 . n1 is nonnegative by A5;

hence -infty < (F1 # x) . n by A84, Def5; :: thesis: verum

then reconsider n1 = n as Element of NAT ;

A85: (F2 # x) . n1 = (F2 . n1) . x by Def13;

F2 . n1 is nonnegative by A30;

hence -infty < (F2 # x) . n by A85, Def5; :: thesis: verum

assume A87: x in dom (f + g) ; :: thesis: ( F # x is convergent & lim (F # x) = (f + g) . x )

then (lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (lim (F2 # x)) by A7, A11, A15;

then (lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (g . x) by A32, A12, A15, A87;

then A88: (lim (F1 # x)) + (lim (F2 # x)) = (f + g) . x by A87, MESFUNC1:def 3;

A89: now :: thesis: for n, m being Nat st n <= m holds

(F2 # x) . n <= (F2 # x) . m

(F2 # x) . n <= (F2 # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (F2 # x) . n <= (F2 # x) . m )

assume A90: n <= m ; :: thesis: (F2 # x) . n <= (F2 # x) . m

A91: (F2 # x) . m = (F2 . m) . x by Def13;

(F2 # x) . n = (F2 . n) . x by Def13;

hence (F2 # x) . n <= (F2 # x) . m by A31, A12, A15, A87, A90, A91; :: thesis: verum

end;assume A90: n <= m ; :: thesis: (F2 # x) . n <= (F2 # x) . m

A91: (F2 # x) . m = (F2 . m) . x by Def13;

(F2 # x) . n = (F2 . n) . x by Def13;

hence (F2 # x) . n <= (F2 # x) . m by A31, A12, A15, A87, A90, A91; :: thesis: verum

A92: now :: thesis: for n, m being Nat st n <= m holds

(F1 # x) . n <= (F1 # x) . m

(F1 # x) . n <= (F1 # x) . m

let n, m be Nat; :: thesis: ( n <= m implies (F1 # x) . n <= (F1 # x) . m )

assume A93: n <= m ; :: thesis: (F1 # x) . n <= (F1 # x) . m

A94: (F1 # x) . m = (F1 . m) . x by Def13;

(F1 # x) . n = (F1 . n) . x by Def13;

hence (F1 # x) . n <= (F1 # x) . m by A6, A11, A15, A87, A93, A94; :: thesis: verum

end;assume A93: n <= m ; :: thesis: (F1 # x) . n <= (F1 # x) . m

A94: (F1 # x) . m = (F1 . m) . x by Def13;

(F1 # x) . n = (F1 . n) . x by Def13;

hence (F1 # x) . n <= (F1 # x) . m by A6, A11, A15, A87, A93, A94; :: thesis: verum

A95: now :: thesis: for n being Nat holds (F # x) . n = ((F1 # x) . n) + ((F2 # x) . n)

F1 # x is ()
by A83, Th10;let n be Nat; :: thesis: (F # x) . n = ((F1 # x) . n) + ((F2 # x) . n)

(F # x) . n = (F . n) . x by Def13;

then A96: (F # x) . n = ((F1 . n) + (F2 . n)) . x by A35;

dom ((F1 . n) + (F2 . n)) = dom (F . n) by A35

.= dom (f + g) by A36 ;

then (F # x) . n = ((F1 . n) . x) + ((F2 . n) . x) by A87, A96, MESFUNC1:def 3;

then (F # x) . n = ((F1 # x) . n) + ((F2 . n) . x) by Def13;

hence (F # x) . n = ((F1 # x) . n) + ((F2 # x) . n) by Def13; :: thesis: verum

end;(F # x) . n = (F . n) . x by Def13;

then A96: (F # x) . n = ((F1 . n) + (F2 . n)) . x by A35;

dom ((F1 . n) + (F2 . n)) = dom (F . n) by A35

.= dom (f + g) by A36 ;

then (F # x) . n = ((F1 . n) . x) + ((F2 . n) . x) by A87, A96, MESFUNC1:def 3;

then (F # x) . n = ((F1 # x) . n) + ((F2 . n) . x) by Def13;

hence (F # x) . n = ((F1 # x) . n) + ((F2 # x) . n) by Def13; :: thesis: verum

hence ( F # x is convergent & lim (F # x) = (f + g) . x ) by A95, A86, A92, A89, A88, Th61; :: thesis: verum

K is convergent by A80, A16, A54, A66, A57, Th61;

hence integral+ (M,(f + g)) = (integral+ (M,f)) + (integral+ (M,g)) by A9, A34, A97, A15, A10, A56, A36, A45, A82, A81, Def15; :: thesis: verum