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

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