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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) & 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_measurable_on A & g is_measurable_on A ) and
A2: ( f is nonnegative & 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
A3: ( ( for n being Nat holds
( F1 . n is_simple_func_in S & dom (F1 . n) = dom f ) ) & ( for n being Nat holds F1 . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom f holds
( F1 # x is convergent & lim (F1 # x) = f . x ) ) & ( for n being Nat holds K1 . n = integral' M,(F1 . n) ) & K1 is convergent & integral+ M,f = lim K1 ) by A1, A2, Def15;
consider F2 being Functional_Sequence of X,ExtREAL , K2 being ExtREAL_sequence such that
A4: ( ( for n being Nat holds
( F2 . n is_simple_func_in S & dom (F2 . n) = dom g ) ) & ( for n being Nat holds F2 . n is nonnegative ) & ( 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 ) & ( for x being Element of X st x in dom g holds
( F2 # x is convergent & lim (F2 # x) = g . x ) ) & ( for n being Nat holds K2 . n = integral' M,(F2 . n) ) & K2 is convergent & integral+ M,g = lim K2 ) by A1, A2, Def15;
now
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 ;
( K1 . n1 = integral' M,(F1 . n1) & F1 . n1 is_simple_func_in S & F1 . n1 is nonnegative ) by A3;
hence -infty < K1 . n by Th74; :: thesis: verum
end;
then A5: K1 is without-infty by Th16;
A6: 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 A7: n <= m ; :: thesis: K1 . n <= K1 . m
A8: ( K1 . n = integral' M,(F1 . n) & K1 . m = integral' M,(F1 . m) & dom (F1 . n) = dom f & F1 . n is_simple_func_in S & F1 . m is_simple_func_in S & dom (F1 . m) = dom f & F1 . n is nonnegative & F1 . m is nonnegative ) by A3;
A9: now
let x be set ; :: 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 A3, A7, A8; :: thesis: verum
end;
then dom ((F1 . m) - (F1 . n)) = (dom (F1 . m)) /\ (dom (F1 . n)) by A8, Th75;
then ( (F1 . n) | (dom ((F1 . m) - (F1 . n))) = F1 . n & (F1 . m) | (dom ((F1 . m) - (F1 . n))) = F1 . m ) by A8, GRFUNC_1:64;
hence K1 . n <= K1 . m by A8, A9, Th76; :: thesis: verum
end;
now
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 ;
( K2 . n1 = integral' M,(F2 . n1) & F2 . n1 is_simple_func_in S & F2 . n1 is nonnegative ) by A4;
hence -infty < K2 . n by Th74; :: thesis: verum
end;
then A10: K2 is without-infty by Th16;
A11: 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 A12: n <= m ; :: thesis: K2 . n <= K2 . m
A13: ( K2 . n = integral' M,(F2 . n) & K2 . m = integral' M,(F2 . m) & dom (F2 . n) = dom g & F2 . n is_simple_func_in S & F2 . m is_simple_func_in S & dom (F2 . m) = dom g & F2 . n is nonnegative & F2 . m is nonnegative ) by A4;
A14: now
let x be set ; :: 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 A4, A12, A13; :: thesis: verum
end;
then dom ((F2 . m) - (F2 . n)) = (dom (F2 . m)) /\ (dom (F2 . n)) by A13, Th75;
then ( (F2 . n) | (dom ((F2 . m) - (F2 . n))) = F2 . n & (F2 . m) | (dom ((F2 . m) - (F2 . n))) = F2 . m ) by A13, GRFUNC_1:64;
hence K2 . n <= K2 . m by A13, A14, Th76; :: thesis: verum
end;
consider A being Element of S such that
A15: ( A = dom f & A = dom g & f is_measurable_on A & g is_measurable_on A ) by A1;
A17: f + g is_measurable_on A by A15, Th37, A2;
A = (dom f) /\ (dom g) by A15;
then A18: A = dom (f + g) by A2, Th22;
A19: f + g is nonnegative by A2, Th25;
deffunc H1( Nat) -> Element of bool [:X,ExtREAL :] = (F1 . $1) + (F2 . $1);
consider F being Functional_Sequence of X,ExtREAL such that
A20: for n being Nat holds F . n = H1(n) from SEQFUNC:sch 1();
 deffunc H2( Nat) -> Element of ExtREAL = integral' M,(F . $1);
consider K being ExtREAL_sequence such that
A21: for n being Element of NAT holds K . n = H2(n) from FUNCT_2:sch 4();
A22: now
let n be Nat; :: thesis: K . n = H2(n)
n in NAT by ORDINAL1:def 13;
hence K . n = H2(n) by A21; :: thesis: verum
end;
A23: 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 )
A24: ( dom (F1 . n) = dom f & F1 . n is_simple_func_in S & F1 . n is nonnegative ) by A3;
A25: ( dom (F2 . n) = dom g & F2 . n is_simple_func_in S & F2 . n is nonnegative ) by A4;
A26: F . n = (F1 . n) + (F2 . n) by A20;
hence F . n is_simple_func_in S by A24, A25, Th44; :: thesis: ( dom (F . n) = dom (f + g) & F . n is nonnegative )
dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n)) by A24, A25, A26, Th71;
hence dom (F . n) = dom (f + g) by A2, A24, A25, Th22; :: thesis: F . n is nonnegative
( F1 . n is nonnegative & F2 . n is nonnegative & F . n = (F1 . n) + (F2 . n) ) by A3, A4, A20;
hence F . n is nonnegative by Th25; :: thesis: verum
end;
A27: 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 A28: n <= m ; :: thesis: for x being Element of X st x in dom (f + g) holds
(F . n) . x <= (F . m) . x
let x be Element of X; :: thesis: ( x in dom (f + g) implies (F . n) . x <= (F . m) . x )
assume A29: x in dom (f + g) ; :: thesis: (F . n) . x <= (F . m) . x
( dom ((F1 . n) + (F2 . n)) = dom (F . n) & dom ((F1 . m) + (F2 . m)) = dom (F . m) ) by A20;
then A30: ( dom ((F1 . n) + (F2 . n)) = dom (f + g) & dom ((F1 . m) + (F2 . m)) = dom (f + g) ) by A23;
( (F . n) . x = ((F1 . n) + (F2 . n)) . x & (F . m) . x = ((F1 . m) + (F2 . m)) . x ) by A20;
then A31: ( (F . n) . x = ((F1 . n) . x) + ((F2 . n) . x) & (F . m) . x = ((F1 . m) . x) + ((F2 . m) . x) ) by A29, A30, MESFUNC1:def 3;
( (F1 . n) . x <= (F1 . m) . x & (F2 . n) . x <= (F2 . m) . x ) by A3, A4, A15, A18, A28, A29;
hence (F . n) . x <= (F . m) . x by A31, XXREAL_3:38; :: thesis: verum
end;
A33: 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 ) )
assume A34: x in dom (f + g) ; :: thesis: ( F # x is convergent & lim (F # x) = (f + g) . x )
A35: now
let n be Nat; :: thesis: (F # x) . n = ((F1 # x) . n) + ((F2 # x) . n)
A36: dom ((F1 . n) + (F2 . n)) = dom (F . n) by A20
.= dom (f + g) by A23 ;
(F # x) . n = (F . n) . x by Def13;
then (F # x) . n = ((F1 . n) + (F2 . n)) . x by A20;
then (F # x) . n = ((F1 . n) . x) + ((F2 . n) . x) by A34, A36, 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;
now
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 ;
B37: F1 . n1 is nonnegative by A3;
(F1 # x) . n1 = (F1 . n1) . x by Def13;
hence -infty < (F1 # x) . n by B37, Def5; :: thesis: verum
end;
assume n in dom (F2 # x) ; :: thesis: -infty < (F2 # x) . n
then reconsider n1 = n as Element of NAT ;
B38: F2 . n1 is nonnegative by A4;
(F2 # x) . n1 = (F2 . n1) . x by Def13;
hence -infty < (F2 # x) . n by B38, Def5; :: thesis: verum
end;
then A39: ( F1 # x is without-infty & F2 # x is without-infty ) by Th16;
A40: now
let n, m be Nat; :: thesis: ( n <= m implies (F1 # x) . n <= (F1 # x) . m )
assume A41: n <= m ; :: thesis: (F1 # x) . n <= (F1 # x) . m
( (F1 # x) . n = (F1 . n) . x & (F1 # x) . m = (F1 . m) . x ) by Def13;
hence (F1 # x) . n <= (F1 # x) . m by A3, A15, A18, A34, A41; :: thesis: verum
end;
A42: now
let n, m be Nat; :: thesis: ( n <= m implies (F2 # x) . n <= (F2 # x) . m )
assume A43: n <= m ; :: thesis: (F2 # x) . n <= (F2 # x) . m
( (F2 # x) . n = (F2 . n) . x & (F2 # x) . m = (F2 . m) . x ) by Def13;
hence (F2 # x) . n <= (F2 # x) . m by A4, A15, A18, A34, A43; :: thesis: verum
end;
(lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (lim (F2 # x)) by A3, A15, A18, A34;
then (lim (F1 # x)) + (lim (F2 # x)) = (f . x) + (g . x) by A4, A15, A18, A34;
then (lim (F1 # x)) + (lim (F2 # x)) = (f + g) . x by A34, MESFUNC1:def 3;
hence ( F # x is convergent & lim (F # x) = (f + g) . x ) by A35, A39, A40, A42, Th67; :: thesis: verum
end;
for n being Nat holds K . n = (K1 . n) + (K2 . n)
proof
let n be Nat; :: thesis: K . n = (K1 . n) + (K2 . n)
A44: ( F1 . n is_simple_func_in S & F1 . n is nonnegative ) by A3;
A45: ( F2 . n is_simple_func_in S & F2 . n is nonnegative ) by A4;
A46: F . n = (F1 . n) + (F2 . n) by A20;
A47: dom (F1 . n) = dom f by A3
.= dom (F2 . n) by A4, A15 ;
A48: K2 . n = integral' M,(F2 . n) by A4;
A49: dom (F . n) = (dom (F1 . n)) /\ (dom (F2 . n)) by A44, A45, A46, Th71;
K . n = integral' M,(F . n) by A22;
then K . n = (integral' M,((F1 . n) | (dom (F1 . n)))) + (integral' M,((F2 . n) | (dom (F2 . n)))) by A44, A45, A46, A47, A49, Th71;
then K . n = (integral' M,(F1 . n)) + (integral' M,((F2 . n) | (dom (F2 . n)))) by GRFUNC_1:64;
then K . n = (integral' M,(F1 . n)) + (integral' M,(F2 . n)) by GRFUNC_1:64;
hence K . n = (K1 . n) + (K2 . n) by A3, A48; :: thesis: verum
end;
then ( K is convergent & lim K = (lim K1) + (lim K2) ) by A5, A6, A10, A11, Th67;
hence integral+ M,(f + g) = (integral+ M,f) + (integral+ M,g) by A3, A4, A17, A18, A19, A22, A23, A27, A33, Def15; :: thesis: verum