:: deftheorem Def79 defines Set4_for_RandomVariable FINANCE3:def 19 :
for k1, k2 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( k = 3 implies Set4_for_RandomVariable (k1,k2,k) = k1 ) & ( not k = 3 implies Set4_for_RandomVariable (k1,k2,k) = k2 ) );