:: deftheorem defines is_integrable_on RANDOM_1:def 2 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Real-Valued-Random-Variable of Sigma
for P being Probability of Sigma holds
( f is_integrable_on P iff f is_integrable_on P2M P );