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