:: deftheorem Def78 defines Set3_for_RandomVariable FINANCE3:def 20 :
for k2, k3, k4 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( k = 2 implies Set3_for_RandomVariable (k2,k3,k4,k) = k2 ) & ( not k = 2 implies Set3_for_RandomVariable (k2,k3,k4,k) = Set4_for_RandomVariable (k3,k4,k) ) );