let p be Nat; :: thesis: 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
let Omega, Omega2 be non empty set ; :: thesis: 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
let F be SigmaField of Omega; :: thesis: 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
let F2 be SigmaField of Omega2; :: thesis: 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
let G be sequence of (set_of_random_variables_on (F,F2)); :: thesis: Element_Of (F,F2,G,p) is random_variable of F,F2
G . p in set_of_random_variables_on (F,F2) ;
then consider Y being Function of Omega,Omega2 such that
A2: ( G . p = Y & Y is F,F2 -random_variable-like ) ;
Element_Of (F,F2,G,p) = Y by FINANCE1:def 9, A2;
hence Element_Of (F,F2,G,p) is random_variable of F,F2 by A2; :: thesis: verum