G . q in set_of_random_variables_on (F,Borel_Sets) ;
then ex f being Function of Omega,REAL st
( f = G . q & f is_random_variable_on F, Borel_Sets ) ;
hence G . q is Real-Valued-Random-Variable of F by RANDOM_3:7; :: thesis: verum