let Omega be non empty finite set ; :: thesis: for P being Probability of Trivial-SigmaField Omega
for X being Real-Valued-Random-Variable of (Trivial-SigmaField Omega) holds X is_integrable_on P
let P be Probability of Trivial-SigmaField Omega; :: thesis: for X being Real-Valued-Random-Variable of (Trivial-SigmaField Omega) holds X is_integrable_on P
let X be Real-Valued-Random-Variable of (Trivial-SigmaField Omega); :: thesis: X is_integrable_on P
set M = P2M P;
A1: jj in REAL by XREAL_0:def 1;
dom X = Omega by FUNCT_2:def 1;
then (P2M P) . (dom X) = jj by PROB_1:def 8;
then (P2M P) . (dom X) < +infty by XXREAL_0:9, A1;
then X is_integrable_on P2M P by Lm5, Th6;
hence X is_integrable_on P ; :: thesis: verum