theorem :: FINANCE6:20

for Prob being Probability of Special_SigmaField2
for r being Real st r > 0 holds
for jpi being pricefunction ex G being sequence of (set_of_random_variables_on (Special_SigmaField2,Borel_Sets)) st
for d being Nat holds
( G . d = {1,2,3,4} --> ((jpi . d) * (1 + r)) & Change_Element_to_Func (G,d) is_integrable_on P2M Prob & Change_Element_to_Func (G,d) is_simple_func_in Special_SigmaField2 )