G . p in set_of_random_variables_on (F,F2) by A1;
then consider Y being Function of Omega,Omega2 such that
A2: ( G . p = Y & Y is_random_variable_on F,F2 ) ;
Element_Of (F,F2,G,p) = Y by A1, FINANCE1:def 9, A2;
hence Element_Of (F,F2,G,p) is random_variable of F,F2 by A2, RANDOM_3:def 1; :: thesis: verum