(1 / (1 + r)) (#) RV is random_variable of F, Borel_Sets by RANDOM_3:7;
hence RV (#) (1 / (1 + r)) is Real-Valued-Random-Variable of F ; :: thesis: verum