:: deftheorem defines Set1_for_RandomVariable FINANCE3:def 18 :
for k1, k2 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( ( k = 1 or k = 2 ) implies Set1_for_RandomVariable (k1,k2,k) = k1 ) & ( k = 1 or k = 2 or Set1_for_RandomVariable (k1,k2,k) = k2 ) );