reconsider p = p as Element of NAT by ORDINAL1:def 12;

G . p in { f where f is Function of Omega,Omega2 : f is F,F2 -random_variable-like } by A1;

then ex f being Function of Omega,Omega2 st

( f = G . p & f is F,F2 -random_variable-like ) ;

hence G . p is Function of Omega,Omega2 ; :: thesis: verum

G . p in { f where f is Function of Omega,Omega2 : f is F,F2 -random_variable-like } by A1;

then ex f being Function of Omega,Omega2 st

( f = G . p & f is F,F2 -random_variable-like ) ;

hence G . p is Function of Omega,Omega2 ; :: thesis: verum