set g = {1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL));
{1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL)) is random_variable of Special_SigmaField2 , Borel_Sets by FINANCE3:10;
then {1,2,3,4} --> (In (((jpi . d) * (1 + r)),REAL)) in { f where f is Function of {1,2,3,4},REAL : f is Special_SigmaField2 , Borel_Sets -random_variable-like } ;
hence RVfirst ((jpi . d) * (1 + r)) is Element of set_of_random_variables_on (Special_SigmaField2,Borel_Sets) ; :: thesis: verum