:: deftheorem Def1212 defines FunctionRV2 FINANCE3:def 23 :
for I being non empty real-membered set st I = {1,2,3} holds
for i being Element of I
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, f2, f3 being Function of Omega,REAL st f3 . 1 = 100 & f3 . 2 = 100 & f3 . 3 = 100 & f3 . 4 = 100 holds
( ( ( i = 2 or i = 3 ) implies FunctionRV2 (i,Sigma,f1,f2,f3) = FunctionRV1 (i,Sigma,f1,f2,f3) ) & ( i = 2 or i = 3 or FunctionRV2 (i,Sigma,f1,f2,f3) = f3 ) );