consider RV being Function of Omega,Omega2 such that
A0: ( Stoch . k = RV & RV is_random_variable_on Sigma,Sigma2 ) by Def30000;
thus Stoch . k is random_variable of Sigma,Sigma2 by A0, RANDOM_3:def 1; :: thesis: verum