let x be object ; :: according to FUNCT_1:def 13 :: thesis: ( not x in set_of_random_variables_on (F,F2) or x is set )
assume x in set_of_random_variables_on (F,F2) ; :: thesis: x is set
then consider z being Function of Omega,Omega2 such that
A5: ( z = x & z is F,F2 -random_variable-like ) ;
x is Function by A5;
hence x is set ; :: thesis: verum