:: deftheorem Def77 defines Set2_for_RandomVariable FINANCE3:def 21 :
for k1, k2, k3, k4 being Element of REAL
for Omega being non empty set
for k being Element of Omega holds
( ( k = 1 implies Set2_for_RandomVariable (k1,k2,k3,k4,k) = k1 ) & ( not k = 1 implies Set2_for_RandomVariable (k1,k2,k3,k4,k) = Set3_for_RandomVariable (k2,k3,k4,k) ) );