:: deftheorem defines probability RANDOM_3:def 7 :
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for P being Probability of S1
for F being random_variable of S1,S2 holds probability (F,P) = M2P (image_measure (F,(P2M P)));