:: deftheorem Def6 defines image_measure RANDOM_3:def 6 :
for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for M being Measure of S1
for F being random_variable of S1,S2
for b₇ being Measure of S2 holds
( b₇ = image_measure (F,M) iff for y being Element of S2 holds b₇ . y = M . (F " y) );