for p being Nat
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for G being sequence of (set_of_random_variables_on (F,F2)) holds Element_Of (F,F2,G,p) is random_variable of F,F2