reconsider p = p as Element of NAT by ORDINAL1:def 12;
G . p in { f where f is Function of Omega,Omega2 : f is_random_variable_on F,F2 } by T1;
then ex f being Function of Omega,Omega2 st
( f = G . p & f is_random_variable_on F,F2 ) ;
hence G . p is Function of Omega,Omega2 ; :: thesis: verum