theorem :: FINANCE6:9
ex G being sequence of (set_of_random_variables_on (Special_SigmaField1,Borel_Sets)) st
( G . 0 = {1,2,3,4} --> 1 & G . 1 = {1,2,3,4} --> 5 & ( for k being Nat st k > 1 holds
G . k = {1,2,3,4} --> 0 ) )