for Omega1, Omega2 being non empty set
for S1 being SigmaField of Omega1
for S2 being SigmaField of Omega2
for F being random_variable of S1,S2 holds
( { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } c= S1 & { x where x is Subset of Omega1 : ex y being Element of S2 st x = F " y } is SigmaField of Omega1 )