:: deftheorem Def1211 defines FunctionRV1 FINANCE3:def 22 :
for I being non empty real-membered set st I = {1,2,3} holds
for i being Element of I st ( i = 2 or i = 3 ) holds
for Omega being non empty set st Omega = {1,2,3,4} holds
for Sigma being SigmaField of Omega st Sigma = bool Omega holds
for f1 being Function of Omega,REAL st f1 . 1 = 60 & f1 . 2 = 80 & f1 . 3 = 100 & f1 . 4 = 120 holds
for f2 being Function of Omega,REAL st f2 . 1 = 80 & f2 . 2 = 80 & f2 . 3 = 120 & f2 . 4 = 120 holds
for f3 being Function of Omega,REAL holds
( ( i = 2 implies FunctionRV1 (i,Sigma,f1,f2,f3) = f2 ) & ( not i = 2 implies FunctionRV1 (i,Sigma,f1,f2,f3) = f1 ) );