theorem :: RANDOM_1:7

for Omega being non empty finite set
for M being sigma_Measure of (Trivial-SigmaField Omega)
for f being PartFunc of Omega,REAL st dom f <> {} & M . (dom f) < +infty holds
f is_integrable_on M by Lm5, Th6;