k in X by A1;
then ex f being Function of Omega,Omega2 st
( f = k & f is_random_variable_on F,F2 ) by A1;
hence k is Function of Omega,Omega2 ; :: thesis: verum