:: deftheorem Def9 defines Element_Of FINANCE1:def 9 :
for p being Nat
for Omega, Omega2 being non empty set
for F being SigmaField of Omega
for F2 being SigmaField of Omega2
for X being set st X = set_of_random_variables_on (F,F2) holds
for G being sequence of X holds Element_Of (F,F2,G,p) = G . p;