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

proof

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;

A20: now :: thesis: for x being object st x in dom ((F1 . m) - (F1 . n)) holds
(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;

A21: F1 . m is nonnegative by A5;
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;

consider F2 being Functional_Sequence of X,ExtREAL, K2 being ExtREAL_sequence such that
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₁( 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₁(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 )

proof

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;

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

now :: thesis: for n being set st n in dom K2 holds
-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;

then A54: K2 is () by Th10;
deffunc H₂( 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₂(n) from FUNCT_2:sch 4();

A56: now :: thesis: for n being Nat holds K . n = H₂(n)

let n be Nat; :: thesis: K . n = H₂(n)
n in NAT by ORDINAL1:def 12;
hence K . n = H₂(n) by A55; :: thesis: verum

end;

A57: for n being Nat holds K . n = (K1 . n) + (K2 . n)

proof

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;

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

A70: now :: thesis: for x being object st x in dom ((F2 . m) - (F2 . n)) holds
(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;

A71: F2 . m is nonnegative by A30;
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;

now :: thesis: for n being set st n in dom K1 holds
-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;

then A80: K1 is () by Th10;
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

let x be Element of X; :: thesis: ( x in dom (f + g) implies ( F # x is convergent & lim (F # x) = (f + g) . x ) )

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

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

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

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

assume n in dom (F2 # x) ; :: thesis: -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;

then A86: F2 # x is () by Th10;
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

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;

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

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

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;

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

end;

A97: f + g is A -measurable by A2, A3, A13, A14, Th31;
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