consider g being Function of {1,2,3,4},REAL such that
A1: ( g = {1,2,3,4} --> (In (r,REAL)) & g is_random_variable_on Special_SigmaField1 , Borel_Sets ) by FINANCE3:10;
g in { f where f is Function of {1,2,3,4},REAL : f is_random_variable_on Special_SigmaField1 , Borel_Sets } by A1;
hence {1,2,3,4} --> r is Element of set_of_random_variables_on (Special_SigmaField1,Borel_Sets) by A1; :: thesis: verum