G . q is random_variable of F, Borel_Sets by Lemacik;
hence G . q is Real-Valued-Random-Variable of F by RANDOM_3:7; :: thesis: verum