:: deftheorem Def11 defines modetrans RANDOM_3:def 11 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for P being set st P is Probability of Sigma holds
modetrans (P,Sigma) = P;