begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
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 , 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) )
theorem