:: deftheorem defines Real_RV FINANCE6:def 24 :
for Omega being non empty set
for F being SigmaField of Omega
for RV being Real-Valued-Random-Variable of F
for d being Nat
for r being Real holds Real_RV (d,r,RV) = RV (#) (1 / (1 + r));