:: deftheorem Def770 defines Conv2_constant_RV FINANCE6:def 11 :
for Omega being non empty set
for F being SigmaField of Omega
for ConstFuncs being sequence of (set_of_constant_RV F)
for w being Element of Omega
for b₅ being Function of NAT,REAL holds
( b₅ = Conv2_constant_RV (ConstFuncs,w) iff for n being Nat holds b₅ . n = (Conv_constant_RV (ConstFuncs,n)) . w );