k in X
by A1;

then ex f being Function of Omega,Omega2 st

( f = k & f is F,F2 -random_variable-like ) by A1;

hence k is Function of Omega,Omega2 ; :: thesis: verum

then ex f being Function of Omega,Omega2 st

( f = k & f is F,F2 -random_variable-like ) by A1;

hence k is Function of Omega,Omega2 ; :: thesis: verum