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