begin
theorem
for
X being non
empty set for
S being
SigmaField of
X for
M being
sigma_Measure of
S for
f,
g being
PartFunc of
X,
ExtREAL st
f is_simple_func_in S &
dom f <> {} & ( for
x being
set st
x in dom f holds
0. <= f . x ) &
g is_simple_func_in S &
dom g = dom f & ( for
x being
set st
x in dom g holds
0. <= g . x ) holds
(
f + g is_simple_func_in S &
dom (f + g) <> {} & ( for
x being
set st
x in dom (f + g) holds
0. <= (f + g) . x ) &
integral (
X,
S,
M,
(f + g))
= (integral (X,S,M,f)) + (integral (X,S,M,g)) )